Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Stage 6 Capability Semantics Backlog

Detailed decompositions for Stage 6 follow-up work. Loopyard tasks link here but should not inline these subtasks.

Notification Objects

Implement a lightweight signal/wait primitive for interrupts and event delivery without full endpoint message overhead.

  • Define schema/ABI and wait semantics. The Notification interface (signal/wait(timeoutNs)/revoke) plus the NotificationOutcome enum (signaled/timedOut/revoked) landed in schema/capos.capnp; the notification KernelCapSource mints a fresh per-grant object.
  • Add kernel object plus ring operations or methods. kernel/src/cap/notification.rs holds the shared latched-pending/revoked cell and the global waiter table; the per-tick notification::poll_waiters (wired into sched::service_periodic_work) is the single deferred-completion deliverer; capos-rt’s NotificationClient is the typed client.
  • Add QEMU smoke for signal, wait, timeout, and revoke/drop cases. make run-notification-object (one process, two threads sharing one cap) proves signal-wakes-waiter, wait-timeout, no-lost-wake, and revoke-releases-waiter + no-wake-after-drop.

Promise Pipelining

Promised-answer targeting for CALL SQEs, over the stable transfer/result-cap insertion path.

Behavior complete through commit e5fb9296 (2026-07-21 12:34 UTC): one-hop pipelining resolves both kernel-served and endpoint antecedents, proven by the eleven-case foreground make run-promise-pipeline run (both endpoint cases retire inside one cap_enter). Remaining work extends that landed behavior – the race-level no-lost-wake and teardown-before-RETURN drop invariants via a cross-drain wake-latch lifecycle smoke and a Loom model of the publish-CQE-before-ready wake latch, a whitepaper evidence reconcile, and the deeper-than-one-hop ABI extension noted below – tracked as Loopyard tasks. See docs/changelog.md for the milestone report.

  • Define promised-answer IDs, dependency encoding, and failure rules. pipeline_dep is the process-local promised-answer ID allocated by the runtime, and pipeline_field is a zero-based sideband CapTransferResult record ordinal in that answer’s completion. It is not a Cap’n Proto schema field or payload path. CAP_SQE_PIPELINE_ANSWER allocates an answer, CAP_SQE_PIPELINE consumes one, and the two are mutually exclusive because pipeline_dep is a single field in a full 64-byte CapSqe. Unsupported mappings fail closed through CAP_ERR_PIPELINE_UNKNOWN_ANSWER, CAP_ERR_PIPELINE_UNRESOLVED, CAP_ERR_PIPELINE_FIELD_OUT_OF_RANGE, CAP_ERR_PIPELINE_ANTECEDENT_FAILED, CAP_ERR_PIPELINE_ANSWER_LIMIT, and CAP_ERR_PIPELINE_DUPLICATE_ANSWER. See capos-config/src/ring.rs.
  • Resolve one-hop dependency chains in the kernel without userspace round-trips. Kernel-served antecedents use per-drain RingScratch state. Endpoint antecedents use a fixed 64-entry cross-drain table, bounded by MAX_PROMISED_ANSWERS entries per caller and keyed by full caller thread generation, kernel epoch, and answer ID. The table retains the originating batch’s frozen SQ tail; after RETURN publishes the antecedent CQE the kernel wakes the submitting thread with a private CAP_ENTER_PROMISE_RETRY result, and that thread resumes the dependent only through that tail in its own cap_enter syscall context. Both paths resolve from kernel-owned result-cap records, never the caller’s result buffer. Caller teardown and endpoint cancellation/server death drop or fail the record without waking a recycled thread.
  • Add runtime placeholders and an IPC pipeline smoke. capos-rt::ring provides AnswerId/PromiseId placeholders and RingClient::submit_pipelined_call_batch, which publishes the answer-allocating CALL and its dependent with one SQ tail store. make run-promise-pipeline proves the happy path (one batch, one cap_enter, a dependent invoking a capability that did not exist when its SQE was written), that pipeline_field ordinal selection is load-bearing, that an answer’s record count is kernel-owned so a well-formed CapTransferResult forged past it in the caller’s buffer does not extend the answer, and the CAP_ERR_PIPELINE_ANTECEDENT_FAILED / CAP_ERR_PIPELINE_UNKNOWN_ANSWER / CAP_ERR_PIPELINE_FIELD_OUT_OF_RANGE fail-closed paths. The same proof also covers an endpoint RETURN followed by dependent dispatch in one cap_enter(min_complete=2) and endpoint server death, where the antecedent reports CAP_ERR_SERVER_DIED and the dependent reports CAP_ERR_PIPELINE_ANTECEDENT_FAILED.

Not implemented:

  • Chains deeper than one hop. One batch expresses a.foo() plus one pipelined call on one of its result caps; deeper chains need one batch per hop until the ABI grows a distinct answer-allocation field.

CapabilityManager

Management-only introspection, revocation, and post-spawn copy grants over one generation-bound child capability table.

  • Define list/grant schema and authority boundaries. CapabilityManager exposes list @0, revoke @1, and grant @2. The manager holder may name only a live capability in its own table; grant copies that hold into the fixed managed child, preserves interface, receiver metadata, disclosure/transfer scopes, and one-way source-revocation propagation, while the child hold receives a child-local revocation epoch. It returns the child-local slot id. It cannot move a source, copy a NonTransferable hold, relabel an interface, widen session scope, select another target, or mutate the child’s immutable CapSet page.
  • Implement read-only cap table introspection and child-scoped revocation. CapabilityManager.list returns live child-local slot descriptors; revoke invalidates the selected child grant through its shared object epoch and cancels affected endpoint state.
  • Implement generation-checked manager-mediated grant with target resource accounting and ordered kernel audit records. A stale session, exited or recycled target, revoked source, disallowed session crossing, or target cap-slot exhaustion fails closed without leaving a target slot behind.
  • Add grant smoke and hostile checks for non-manager callers. make test-capability-manager-grant starts a child with only a control endpoint, grants it Console after spawn, sends the returned slot id over that endpoint, and proves the child can invoke Console. The same proof rejects a non-transferable manager source and shows that the parent’s manager slot id carries no manager authority in the child’s local table; revoking the child hold leaves the parent’s source live; successful and denied manager operations are audited as cap_grant.

Session-Bound Invocation Context

Replace caller-selected endpoint identity with session-bound invocation context as described in docs/proposals/session-bound-invocation-context-proposal.md. The selected 2026-04-28 migration plan lives in docs/backlog/session-bound-invocation-context.md.

Current status: Gate 0 delegated-client relabeling containment, the transitional representation substrate, the synthetic service-object routing/lifecycle proof, Gate 1 process-session invariant, Gate 2 privacy-preserving endpoint caller-session metadata, and Gate 3 chat session-keyed migration have landed. Existing code still has a badge-named u64 field in several transport structs, but the active design treats that field as legacy receiver metadata, not as service capability. Commit a4655f0 at 2026-04-28 14:10 UTC completed the historical service-object routing proof with generation-checked receiver cookies, service-side object records, close/revoke rejection, stale-cookie rejection after record reuse, receiver-cookie routing despite spoofed request bytes, copy/move IPC transfer, and nested spawn delegation.

Gate 4 in docs/backlog/session-bound-invocation-context.md is implemented and verified on mainline: shared-service legacy cleanup has moved normal chat, adventure, and terminal/stdio paths off caller-selected receiver metadata. Do not continue the superseded subject/proof root-opening path from docs/backlog/service-object-identity-migration.md unless the selected milestone changes again.

Paper prerequisite. Gate 2 endpoint caller-session metadata, Gate 3 chat session-keyed migration, and Gate 4 shared-service cleanup have landed. The paper/status closeout for whitepaper claim C1 (“schema-typed methods replace parallel rights”) remains peer-owned: docs/paper/evidence-gaps.md, docs/paper/plan.md, and the matching #todo block in papers/schema-as-abi/main.typ still need to reflect the landed evidence.

Gate 0: delegated-client relabeling containment

This is the first Telnet Shell Demo blocker. It must land before shell launch can be exposed through any network-backed terminal.

  • Add hostile coverage proving an ordinary shell or delegated endpoint client cannot re-label a client endpoint by choosing a different identity in a spawn grant. Cover explicit badge N, the legacy badge-zero encoding that old omitted syntax used to produce, and current omitted shell syntax preserving the delegated source identity. Worker B checkpoint: normal shell help and smoke-help assertions no longer advertise badge N. Worker C checkpoint: init spawn hardening now mints a nonzero delegated client facet into a child init process and asserts that explicit-badge and badge-0 relabel spawn attempts fail.
  • Change ProcessSpawner so ClientEndpoint grants from delegated client facets preserve the source identity and reject attempts to set a different value. Endpoint owners and trusted parent endpoint result caps remain the only transitional paths that may mint a new client identity.
  • Remove arbitrary badge N from normal capos-shell help and smoke-help launch examples; keep legacy manifest/debug syntax only where the kernel enforcement still rejects delegated-client relabeling. The default MOTD adventure launch commands now omit explicit legacy selectors; Gate 4 in docs/backlog/session-bound-invocation-context.md still owns retiring remaining manifest-level selector compatibility after session-bound chat and adventure migration.
  • Document the containment in docs/architecture/ipc-endpoints.md and trust-boundary docs before exposing shell launch through Telnet.

Historical Gate 1: service object representation

  • Define the transitional kernel/runtime representation for existing endpoint-backed service facets: target endpoint, interface id, and legacy receiver metadata. 2026-04-25 18:31 UTC checkpoint: the first representation slice reuses CapHold { object_id, interface_id, badge } as endpoint object, service interface id, and endpoint-scoped receiver selector for existing endpoint-backed service objects. Dispatch and spawn now preserve the held metadata for ordinary delegation; explicit trusted minting remains open.
  • Complete the transitional representation replacement with explicit generation-safe receiver records and lifecycle coverage for the synthetic proof. Big Chunk 1 now covers trusted service-object minting, receiver-cookie dispatch, receiver-preserving copy/move IPC transfer and spawn, request-byte spoofing checks, generation-safe server cookies, and close/revoke/stale-generation rejection. 2026-04-28 14:10 UTC checkpoint: commit a4655f0 added generation-checked receiver cookies, service-side object records, close/revoke rejection, and stale-cookie rejection after record reuse.
  • Add the minimum trusted mint path needed for the synthetic service-object proof: endpoint owner or explicit mint authority creates the initial service object cap; ordinary clients only copy or move it. 2026-04-28 checkpoint: CapGrantMode.serviceObject lets endpoint owners mint copy-transferable endpoint-scoped service object facets for child processes while delegated service object caps cannot relabel the held interface or receiver cookie. The legacy ProcessSpawner endpoint-result facet exception remains scoped to clientEndpoint and is rejected for serviceObject.
  • Scope receiver selectors to the target endpoint and keep them out of shell syntax, manifest user fields, and service policy labels.
  • Preserve the current held receiver metadata across copy and move transfer. Ordinary transfer must not mint a sibling object.
  • Prove receiver identity preservation across copy, move, IPC transfer, and spawn in the synthetic service-object QEMU proof. 2026-04-28 checkpoint: make test-service-object-routing exercises copy-transfer and move-transfer of service object caps through IPC, nested spawn delegation, and hostile payloads that try to name the other receiver.
  • Enforce that client-held service object caps cannot use endpoint receive/return authority unless a separate server-facing interface grants that authority.
  • Deliver endpoint metadata so servers can dispatch current object-shaped calls without treating it as caller-selected identity. 2026-04-25 18:45 UTC checkpoint: trusted manifest/init minting now uses explicit CapabilityAs spawn grants to request a service interface from endpoint exports, validation rejects the same override for non-endpoint exports, and system-spawn.cue proves a non-Endpoint service interface plus selector reaches the server receive metadata.
  • Rename or wrap server delivery surfaces around receiver-selector/server- cookie terminology once the behavior is receiver-selector-only.

Gate 2: process session invariant

  • Add process-owned immutable session context with explicit system/service session support.
  • Make child spawn inherit the parent’s session by default and require trusted broker/session-manager authority for different child sessions.
  • Add host and QEMU coverage proving ordinary processes cannot inject or use a second independent session subject.

Gate 3: endpoint caller session metadata

  • Deliver opaque service-scoped caller-session references and freshness results to endpoint servers.
  • Add an explicit subject-disclosure path so global principal/profile details are not revealed to services by default.
  • Add hostile coverage proving request bytes cannot spoof session identity or force disclosure.

Gate 4: shared-service demo migration

  • Convert chat identity from legacy receiver selectors to broker-granted chat roots/facets plus service-scoped caller-session references.
  • Finish adventure NPC/service-authority cleanup and any remaining stdio/terminal child bridge paths that depend on caller-selected endpoint identity. Aurelian ordinary player state is already keyed by live endpoint caller-session metadata.
  • Retire normal user-facing badge/receiver-selector syntax after chat, adventure, stdio, and endpoint smoke paths no longer depend on it.

Scheduling Context And Resource Donation

Convert the roadmap’s priority/budget donation and session-quota ideas into a measured design before adding new scheduler policy.

  • Record current direct-switch IPC timing and priority-inversion risks. The five-run evidence is in Direct IPC Handoff Timing; reachable and fail-closed inversion shapes are recorded in Direct IPC timing and priority inversion.
  • Define scheduling-context donation metadata.
  • Define resource donation parameters for session-creating caps.

Init ELF Embedding

Done 2026-05-25 23:26 UTC. The init ELF ships inside the kernel binary via include_bytes!, not as a manifest entry or separate Limine module. kernel/build.rs reads the prebuilt init/ artifact (CAPOS_INIT_ELF, with a conventional-path fallback) and emits a kernel::boot::INIT_ELF: &[u8] static; kernel bootstrap parses it through the existing capos_lib::elf loader. Init stays a standalone crate with its own linker script and code model. Embedding is byte packaging, not linker merging.

Landed as a hybrid keyed on the reserved selector rather than an always-embedded init: initConfig.init.binary remains a generic “which binary is PID 1” selector. The shell-family manifests, including system-smoke.cue, now select standalone init; many self-contained focused proofs still select their proof binary directly. Whether that proof class remains exempt from the init mandate is tracked by init-mandate-loader-validation-rule. Embedding applies only when init.binary == capos_config::RESERVED_INIT_BINARY_NAME ("init"): then PID 1 loads from INIT_ELF with no binaries resolution, and manifest validation (capos-config/mkmanifest) rejects any binaries entry named "init". Any other selector still resolves PID 1 from SystemManifest.binaries exactly as before. The real-init manifests (system.cue via the shared _baseBinaries plus the focused init.binary == "init" manifests) drop their init binaries entry; direct-boot proof manifests continue to resolve their selected binary from SystemManifest.binaries.

Because the embedded image is the canonical init, child spawns that reference the init binary by name (e.g. system-spawn.cue’s spawn-hardening fixtures) keep working: run_init injects the embedded bytes into the ProcessSpawner binary set under the reserved name when init is embedded (the BootPackage cap serves only the serialized manifest bytes), so the spawnable set matches the pre-embedding state without init appearing in the serialized manifest.

Proof: make test-init-embedding (minimal system-init-embedding.cue: PID 1 from INIT_ELF, no reserved binaries entry) and make run-smoke (embedded standalone init launches the focused shell service). cargo test-mkmanifest / cargo test-config cover the reserved-name rejection and the init-ref skip.

Reference: docs/proposals/service-architecture-proposal.md section Init Binary Embedding.