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

Repository Map

This map names the main source locations for the current system. It is not an ownership file; use it to find the code behind architecture and validation claims.

Root Files

  • README.md gives the compact project overview.
  • Cargo.toml defines the Rust workspace and shared build profiles.
  • limine.conf configures the bootloader entry used by the ISO.
  • docs/roadmap.md records long-range stages and broad feature direction.
  • Live task state – the selected milestone (selected_milestone project setting), task lifecycle records (candidate, on-hold, active, review, done), and open review-finding remediation – lives in the loopyard task backend (board: https://tasks.cap-os.dev/p/capos/board), driven by the loopyard CLI. The retired docs/tasks/ file ledger is preserved only in git history; REVIEW_FINDINGS.md is a tombstone for pre-migration links.
  • REVIEW.md defines review expectations.
  • Makefile builds pinned tools, userspace binaries, manifests, ISO images, QEMU targets, formatting checks, generated-code checks, and policy checks.
  • rust-toolchain.toml declares the Rust nightly channel, required targets, and rust-src; it does not pin an exact nightly by date or commit.
  • .cargo/config.toml sets the default bare-metal target and useful cargo aliases.

Schema and Shared ABIs

  • docs/abi-evolution-policy.md defines compatibility classes, schema ordinal rules, ring-layout rules, version negotiation, and deprecation windows for externally visible ABI changes.
  • schema/capos.capnp defines capability interfaces, manifest structures, exceptions, ProcessSpawner, ProcessHandle, and transfer-related schema.
  • capos-abi/src/lib.rs defines small no_std ABI/policy constants shared by crates that should not depend on schema/config internals, including process quotas, credential policy limits, and the AuditLog.record text/id bounds (MAX_AUDIT_TEXT_BYTES / MAX_AUDIT_ID_BYTES) that a userspace caller must clamp request-derived text to before recording.
  • capos-config/src/manifest.rs defines the host and no_std manifest model.
  • capos-config/src/validation.rs owns manifest graph and bootstrap validation policy.
  • capos-config/build.rs invokes the shared Cap’n Proto code-generation and no_std patching helper.
  • capos-config/src/ring.rs defines CapRingHeader, SQE/CQE structures, opcodes, flags, and transport error constants shared by kernel and userspace.
  • capos-config/src/capset.rs defines the read-only bootstrap CapSet ABI.
  • capos-config/src/cue.rs supports evaluated CUE-style manifest data.
  • capos-config/src/credential_policy.rs re-exports credential policy limits; full PHC parsing is enabled by the credential-validation feature for bootstrap validators that need credential checks.
  • capos-config/tests/ring_loom.rs models bounded ring protocol behavior with Loom.

Validation: cargo test-config, cargo test-ring-loom, make generated-code-check.

Shared Pure Logic

  • capos-lib/src/elf.rs parses ELF64 images for kernel loading and host tests.
  • capos-lib/src/cap_table.rs implements CapId, capability-table storage, stale-generation checks, grant preparation, transfer transaction helpers, commit, rollback, and the CapTable quota constants sourced from capos-abi.
  • capos-lib/src/credential_admission.rs is the pure fair bounded admission arbiter that fronts the single credential-hash executor: a protected local-recovery lane reserve, an anonymous-remote lane pool, per-connection outstanding bounds keyed on opaque non-peer connection tokens, an aggregate backstop, absolute-deadline reaping, work-conserving aging/randomized cross-connection selection, exact move-only reservation/release, typed overload with bounded retry guidance, and bounded diagnostic counters. The kernel kernel/src/cap/credential_store.rs composes it with the real arena. Its WebUI-ingress counterpart, WebUiIngressLedger in demos/remote-session-web-ui/src/lib.rs, applies the same fair-admission core to pre-identity anonymous/protected-lane ingress and decouples the WebUI application-slot, backlog, and release-debt capacities onto independent effective IngressProfile fields (host-tested; make webui-login-peer-logic-test). The sibling SessionBudgetLedger in the same file is the strictly separate post-authentication pool: an authenticated session opens an explicit donated budget at login (open_session) and every authenticated request draws one move-only unit against it (charge), released exactly once on completion/cancel/close; it holds no ingress reservation and never retroactively reclassifies pre-identity work. The serve loop in main.rs drives both ledgers live and emits balanced quiescent cloudboot-evidence: webui-ingress-ledger / webui-session-budget lines the L4 gate asserts (make run-cloud-prod-remote-session-web-ui-l4).
  • capos-lib/src/cloud_store_bridge.rs implements the bounded, scope-bound provider-neutral local fake behind the CloudStoreBridge ABI: create-only mutable puts, exact version/hash compare-and-set, strict append-only ledger chains, explicit schema/size/count limits, and deterministic record hashes.
  • capos-lib/src/frame_bitmap.rs implements the host-testable physical frame bitmap core.
  • capos-lib/src/frame_ledger.rs contains a bounded frame-grant helper kept for host-test coverage; current MemoryObject accounting charges CapTable::ResourceLedger.
  • capos-lib/src/lazy_buffer.rs provides bounded lazy buffers used by ring scratch paths.
  • capos-lib/src/ninep.rs implements the side-effect-free, bounded 9P2000.L read/write-subset client codec: caller-buffer request encoding and borrowed reply decoding for session, walk, open/create, read/write, readdir, getattr, fsync, rename, unlink, clunk, and Rlerror, with negotiated-size, tag, reply-type, counted-payload, directory-entry, attribute-mask, and write-count validation. It performs no transport I/O and does not serve Directory/File capabilities; fuzz target ninep_reply_decode exercises reply decoding.
  • capos-lib/src/transport_seed.rs decides where the userspace network stack’s smoltcp random_seed comes from: the TransportSeed provenance type (per-boot entropy vs named proof fixture, with a value-redacting Debug), the domain-separated SHA-256 derivation of the listener seed, the DHCP-client seed, and the publishable per-boot witness from one EntropySource draw, and the fail-closed ProductionEntropyRefusal vocabulary the serving path reports when production entropy is missing, dead, short, or degenerate.
  • capos-lib/src/iso9660.rs is the pure ISO 9660 primary-volume-descriptor and directory-record parser the kernel boot-ISO driver (kernel/src/iso/) delegates to; fuzz target iso9660_volume.
  • capos-lib/src/storage_format.rs holds the pure CAPOSRO1 (rofs), CAPOSST1 (disk_store), and CAPOSWF1 (writable_fs) mount parsers the kernel storage cap backers delegate to, including the shared record-layout constants the kernel writers reuse; fuzz targets storage_rofs_mount, storage_disk_store_mount, storage_writable_fs_mount.
  • capos-lib/src/recordstore.rs is the CAPOSRS1 transactional WAL record store: atomic multi-record commit frames over the abstract BlockIo block seam, checksum-chained bounded-prefix recovery with ordered tail invalidation, fail-stop remount semantics after indeterminate I/O, fail-closed frame/record geometry validation, and secondary-key lookup (self-hosted task-backend phase 3, first increment); fuzz target recordstore_mount. The BlockDevice wiring lands the seam in-system: demos/record-store-blockdevice (capos-demo-record-store-blockdevice) persists this WAL through the typed BlockDevice cap and proves reboot durability plus a bounded torn-write forced-poweroff crash recovery across three boots of one disk image (make run-record-store, tools/qemu-record-store-smoke.sh, manifests/system-record-store.cue). The compaction-capable format (RecordStore::format_compacting / compact: an A/B superblock plus two log segments that folds the live set into a fresh generation to reclaim log space, crash-safe via the generation/epoch fence) is proven in-system by demos/record-store-compaction-proof (capos-demo-record-store-compaction-proof) across three boots for reboot log-space reclamation and a bounded forced-poweroff in the compaction flip window (make run-record-store-compaction, tools/qemu-record-store-compaction-smoke.sh, manifests/system-record-store-compaction.cue).

Validation: cargo test-lib, cargo miri-lib, make kani-lib, fuzz targets under fuzz/fuzz_targets/.

TLS and PKI (capos-tls/)

no_std + alloc userspace cores. No certificate or path-building logic runs in the kernel, and the crate carries no served CapObject.

  • capos-tls/src/verify.rs builds and verifies X.509 paths over the vendored rustls-webpki, returning VerificationOutcome / ValidChain; trust.rs is the RAM-only anchor set seeded from vendored webpki-roots; cert.rs is the typed field surface over a DER certificate, including the notBefore/notAfter walk (fuzz target x509_validity).
  • capos-tls/src/pki_algs.rs is p256_sha256_algorithms, ECDSA P-256/SHA-256 over the p256 crate – the whole signature-verification surface capOS accepts today. The verifier core is crypto-provider-free and takes supported_algs as a parameter, so this is the set a bare-metal caller passes; the wider ring-backed algorithms set in lib.rs is gated behind the host-test-only webpki-ring feature, because ring does not build for x86_64-unknown-none.
  • capos-tls/src/key.rs holds the RAM-only key cores: RamSymmetricKey, RamPrivateKey/PublicKey (P-256/ES256), RamKeyVault handle custody, and the development-only DevelopmentSoftwareKeySource. No raw private-key export path exists on any of them; that absence is the custody property.
  • capos-tls/src/entropy.rs is DrawnEntropy, the bridge between an EntropySource cap and the infallible rand_core traits the P-256 and handshake code require: the consumer draws a bounded budget up front (TLS_SERVER_HANDSHAKE_ENTROPY_BYTES, one buffer per accepted connection) where a failed ring call can still be handled, and the buffer never wraps, regenerates, or falls back to a weaker source. Exhaustion fails closed – a panic on the infallible path, an error from try_fill_bytes – rather than silently emitting predictable randomness; a host test pins real consumption against the constant.
  • capos-tls/src/tls13/ is the TLS 1.3 server handshake core (TlsServerHandshake, TlsServerCertChain), signing through the TlsServerSigner seam so the key never enters the handshake types. tls13/alert.rs owns the RFC 8446 §6 map from an internal failure to the description a peer is told, which is the disclosure decision for everything the core says to an unauthenticated peer: the bounded-surface refusals collapse onto one handshake_failure, and deprotection failure says only bad_record_mac. TlsServerHandshake::take_alert hands the consumer the fatal alert a failed feed owes; close_notify closes a completed connection cleanly.
  • capos-tls/src/selfsigned.rs issues development self-signed serverAuth certificates over a runtime key’s own public key – the local-proof stand-in for a publicly trusted chain, which must come from ACME.
  • capos-tls/src/acme.rs is the local RFC 8555 account/order/finalize client plus the bounded token-scoped Http01ChallengeSolver and the LocalAcmeDirectory proof fixture.
  • capos-tls/src/der.rs is a minimal DER writer surface (SEQUENCE, INTEGER, OBJECT IDENTIFIER, ECDSA signature values) shared by the ACME CSR encoder and the self-signed issuer, which emit the same structures. Parsing lives in cert.rs and the vendored rustls-webpki; this side only encodes.
  • capos-tls/src/certstore.rs is the rotation seam: a stable handle names the chain a TLS server presents, put replaces it in one step and notifies watch subscribers, and get resolves only inside the stored chain’s validity window (unknown, deleted, expired, and not-yet-valid all fail closed). Entries hold public certificate bytes only, which is what keeps a chain rotation from being a key rotation.
  • capos-tls/src/renewal.rs is RenewalPolicy, the pure “is it due” decision: a lead before notAfter so a failed issuance can be retried while the current chain is still servable, distinguishing Due from Expired. No clock and no ACME client; the caller supplies now and owns its provenance.

Validation: cargo test-tls; make run-cloud-tls-webui-terminated proves the served endpoint and its renewal-driven chain rotation in QEMU.

Kernel

  • kernel/linker-x86_64.ld defines the higher-half kernel layout and exported section boundaries used by paging.
  • kernel/src/main.rs is the boot entry point, hardware setup sequence, manifest parsing path, and boot-launched service creation path. run_init resolves PID 1 from the kernel-embedded boot::INIT_ELF when initConfig.init.binary == capos_config::RESERVED_INIT_BINARY_NAME ("init") and otherwise from SystemManifest.binaries; for the embedded case it also injects the embedded image into the ProcessSpawner binary set under the reserved name so child spawns of init resolve.
  • kernel/src/boot.rs exposes boot::INIT_ELF: &[u8], the PID 1 init image packaged at build time. kernel/build.rs reads the prebuilt init/ artifact (CAPOS_INIT_ELF, with a conventional-path fallback) and generates the include_bytes! static; init/ stays a standalone crate (byte packaging, not linker merging).
  • kernel/src/spawn.rs loads user ELF images, creates process state, maps bootstrap pages, and enqueues spawned processes.
  • kernel/src/process.rs defines Process, Thread, ThreadState, per-thread kernel stacks, park waiter storage, and userspace CPU context.
  • kernel/src/session_context.rs defines immutable per-process invocation session metadata.
  • kernel/src/sched.rs implements the single-CPU scheduler, timer-driven preemption, blocking cap_enter, direct IPC handoff, ParkSpace wait/wake, and deferred cancellation wakeups.
  • kernel/src/crash_record.rs (Crash Recovery and Supervision, Phase 1) is the bounded note-then-emit table for unplanned process deaths. The CPL3 fault handler notes the CrashKind and faulting instruction pointer; the process teardown path emits the redacted [audit] event=crash record after cap revocation, so no record can observe live authority. A planned exit notes nothing and produces no record. Proof make run-crash-disconnect.
  • kernel/src/serial.rs implements COM1/COM2 UART setup, manifest-driven console-vs-terminal routing, and kernel print macros.
  • kernel/src/pci.rs implements early PCI config-space access through legacy I/O ports and ACPI MCFG/PCIe ECAM, with QEMU diagnostics for the current virtio-net and Q35 discovery paths, plus reusable memory-BAR subregion validation, kernel MMIO mapping helpers for in-kernel drivers, and MSI/MSI-X capability metadata discovery plus typed MSI-X table programming.
  • kernel/src/device_interrupt.rs records the current kernel-owned virtio-net MSI-X config/RX/TX sources, their generation ids, route state, in-kernel driver owner, lock-free bounded device MSI vector-pool dispatch slots, and claimed-route reassignment/release without exposing userspace interrupt authority.
  • kernel/src/device_dma.rs holds the kernel-owned, fixed-size DMA pool accounting ledgers. The net-keyed VIRTIO_NET_DMA_POOL backs virtio-net’s DmaPage path. The single-request-queue devices share one SingleQueueDmaLedger<C, PAGES> shape (reusing the shared ActivePage/QueueAccount types, same generation-checked handle and scrub-before-free invariants), instantiated per device through a SingleQueuePoolConfig that supplies the owner/pool audit strings, the legal queue index, and the depth budget: VirtioBlkPoolConfig backs the virtio-blk request buffer and Virtio9pPoolConfig the virtio-9p request/reply buffers. Each configuration is a distinct ledger type, so a page handle minted against one pool never validates against another. Each device’s VirtqueueDma seam impl delegates to its own pool’s keyed API.
  • kernel/src/dma_backend.rs (always compiled) records the boot-time IOMMU probe verdict and resolves the fail-closed DMA backend selection (direct IOMMU remapping only with a verified probe, else kernel-owned bounce buffers) per the “Cloud DMA Backend” contract in docs/dma-isolation-design.md, emitting the boot proof line.
  • kernel/src/device_manager/ holds bounded in-kernel PCI device ownership records. The full DDF surface (device records, DMA pools/buffers, MSI-X interrupts, NVMe brokered controller registers, IOMMU domain ledgers, virtio ring publication, proofs) compiles only under cfg(feature = "qemu") in qemu_full.rs; the MMIO-only surface used by cap::device_mmio exists in both builds, dispatching to stub.rs (one-slot parked-region DeviceMmio record) in the production non-qemu build.
  • kernel/src/nvme_storage_backend.rs (cfg(not(feature = "qemu"))) is the fail-closed activation gate for the always-built NVMe BlockDevice read arm: modeled on dma_backend, it resolves a production handle only when a brokered controller was discovered and a live device_mmio grant is staged, otherwise the block_device grant fails closed with a typed error.
  • kernel/src/virtio_transport.rs (always compiled) is the device-agnostic virtio modern-PCI transport host surface: capability/region discovery constants and bounded volatile MMIO accessors usable outside the qemu-gated legacy virtio path.
  • kernel/src/virtio.rs (cfg(any(qemu, virtio_9p_host_fixture))) holds the in-kernel virtio fixture transport. The full net/blk/rng drivers and DDF/IOMMU proof consumers remain qemu-only; the explicit virtio_9p_host_fixture feature compiles only the shared split-ring scaffold and 9p driver into a not(qemu) proof build, which includes and re-exports the typed-negative kernel/src/virtio_stub.rs network façade. A build with neither feature maps mod virtio directly to that stub. Its pub(crate) mod transport is the device-generic layer: split-ring/common-config constants, the MmioRegion accessor, the VirtqueueDescriptorTracker, the VirtqueueDma DMA/notify seam, the seam-driven Virtqueue/DmaPage with their poll/submit/complete loop and the multi-descriptor submit_request_chain, and the device-id-parameterized discover_modern_transport. virtio-net is one seam caller (VirtioNetDma); virtio-blk is a second (VirtioBlkDma + VirtioBlkDriver, diagnose_virtio_blk_transport, the block_device_* request API behind the BlockDevice cap); virtio-9p is a third (Virtio9pDma + Virtio9pDriver, diagnose_virtio_9p_transport), a polled host-directory fixture that completes a Tversion/Tattach handshake through the capos_lib::ninep codec and then serves a bounded read subset (Twalk/Tlopen/Tgetattr/Treaddir/Tread/Tclunk) behind the ninep_bound/ninep_list_root/ninep_stat/ninep_read façade, plus a bounded write subset (Tlcreate/Twrite/Tfsync/Trename/Tunlinkat) behind the separate ninep_create/ninep_write/ninep_fsync/ninep_rename/ ninep_unlink façade that only the writable cap types call. Each call is one complete walk-op-clunk transaction under the driver lock (proofs make test-virtio-9p-bringup, make test-virtio-9p-fs, and make test-virtio-9p-write; the composable co-boot proof is make test-virtio-9p-net-coboot; provenance map docs/devices/virtio-9p.md). Net-specific provider/proof methods stay in the parent module as impl Virtqueue<VirtioNetDma>.
  • kernel/src/iommu.rs (cfg(qemu)) programs the Intel VT-d legacy-mode remapping tables, drives the hardware-DMA translation/fault proof, and runs the register-based invalidation revocation cycle. Under nvme_iommu_translation_proof it also runs diagnose_nvme_iommu_translation, the NVMe-lane cycle over the same machinery.
  • kernel/src/nvme_iommu_proof.rs (cfg(nvme_iommu_translation_proof)) is a minimal NVMe admin-queue driver – reset, AQA/ASQ/ACQ at programmed IOVAs, CC.EN/CSTS.RDY, one IDENTIFY CONTROLLER per phase, polled completions – used to measure that QEMU’s emulated nvme controller honors VT-d translation. This is the platform precondition of the Model-B NVMe DMA authority lane, not an authority surface: the kernel authors every device-visible value and publishes no address to userspace. Proof make test-nvme-iommu-translation; provenance map docs/devices/nvme.md §9.
  • kernel/src/nvme_model_b_iommu.rs (cfg(nvme_model_b_provider_iova_proof)) owns the proof lane’s requester- scoped VT-d domain. map_buffer installs manager-owned queue pages, mapping exports active domain IOVAs, and owns_mapping plus unmap_buffer keep active or quarantined pages out of the allocator until invalidation succeeds. teardown refuses a live mapping ledger before disabling translation and freeing its tables. Proof make test-nvme-model-b-provider-iova; provenance map docs/devices/nvme.md §9.
  • kernel/src/iso/ (cfg(boot_iso_read) / cfg(boot_iso) / cfg(qemu)) is the boot-time ISO reader for the Boot Binary ISO Layout track. AtapiDevice (gate 1) locates the legacy IDE ATAPI device and exposes a bounded read_sectors(lba, count, buf) over polled-PIO READ(12) packet commands with range/length validation. IsoFs (gate 2) is a read-only ISO 9660 driver layered on it: it parses the primary volume descriptor, walks directory records, and serves open_file(name) -> (lba, size) under /boot/bins/, validating every directory record and derived extent against the volume size before use (fail-closed BadVolume/NotFound/NotDirectory). boot_read_proof() reads the PVD (CD001) and boot_fs_proof() walks to /boot/bins/PAYLOAD.BIN and verifies its content, both behind boot_iso_read as the make run-boot-iso-read proof. The boot_source submodule (gate 4, cfg(boot_iso)) builds a validated (name, lba, size) registry from every declared manifest binary name (mapping each name to the ISO 9660 d-character form, e.g. capos-shell -> /boot/bins/CAPOS_SHELL) and reads ELF bytes on demand behind a device mutex; run_init and ProcessSpawnerCap consume it so the boot_iso kernel loads binaries from the ISO instead of embedded NamedBlob.data. Proofs: make run-boot-iso and the default make run-smoke. Under cfg(qemu) the always-on AtapiDevice/IsoFs surface (plus a qemu-gated block_size()/list_boot_bins() enumeration helper) also backs the read-only install-source fixture cap (kernel/src/cap/installable_image.rs).

Validation: cargo build --features qemu, make run-smoke, make run-spawn, make run-net, make run-iommu-remapping.

Kernel Architecture

  • kernel/src/arch/x86_64/gdt.rs sets up kernel/user segments and TSS state.
  • kernel/src/arch/x86_64/idt.rs handles exceptions and timer interrupts; CPL3 #PF/#GP/#UD/#DB/#BP faults terminate the whole owning process through sched::exit_current_thread_terminating_process (deferred whole-process termination when sibling threads are live; proof make run-user-fault), while CPL0 faults still halt the machine.
  • kernel/src/arch/x86_64/syscall.rs implements syscall MSR setup and entry.
  • kernel/src/arch/x86_64/context.rs defines timer context-switch state.
  • kernel/src/arch/x86_64/pic.rs and pit.rs configure legacy interrupt hardware.
  • kernel/src/arch/x86_64/ioapic.rs maps MADT I/O APICs and programs masked legacy IRQ routes from interrupt-source overrides.
  • kernel/src/arch/x86_64/lapic.rs programs the xAPIC LAPIC timer and IPIs.
  • kernel/src/arch/x86_64/smap.rs enables SMEP/SMAP and brackets user memory access.
  • kernel/src/arch/x86_64/tls.rs handles FS-base/TLS support.
  • kernel/src/arch/x86_64/pci_config.rs provides legacy PCI config I/O used by the higher-level PCI module alongside its ECAM backend.
  • kernel/src/arch/x86_64/percpu.rs, smp.rs, and tlb.rs provide per-CPU data, AP startup, and TLB shootdown for the SMP scheduler.

Kernel Memory

  • kernel/src/mem/frame.rs wraps the shared frame bitmap with Limine memory map initialization and global kernel access.
  • kernel/src/mem/paging.rs manages page tables, address spaces, permissions, user mappings, W^X enforcement, and address-space teardown.
  • kernel/src/mem/heap.rs initializes the kernel heap, sizes it against its standing reservations (notably the argon2 login arena), and reports used/free via stats().
  • kernel/src/mem/validate.rs validates user buffers before kernel access.

Related docs: DMA Isolation, Trusted Build Inputs.

Kernel Capabilities

  • kernel/src/cap/mod.rs initializes kernel capabilities and builds the first service’s kernel-sourced bootstrap capability table.
  • kernel/src/cap/table.rs re-exports shared capability-table logic and owns the kernel-global table.
  • kernel/src/cap/ring.rs validates and dispatches ring SQEs. Promise pipelining uses bounded per-drain RingScratch records for kernel-served antecedents and a fixed cross-drain table for endpoint antecedents. Endpoint records are generation- and epoch-bound to the caller and retain the originating batch’s frozen SQ tail. Resolution always uses kernel-owned result-cap records rather than the caller’s result buffer.
  • kernel/src/cap/transfer.rs validates transfer descriptors and prepares transfer transactions.
  • kernel/src/cap/endpoint.rs implements Endpoint CALL, RECV, RETURN, queued state, cleanup, and cancellation behavior.
  • kernel/src/cap/console.rs implements serial Console.
  • kernel/src/cap/terminal_session.rs implements the session-scoped TerminalSession line-oriented terminal with bounded readLine, echo modes, and cancellation.
  • kernel/src/cap/boot_package.rs implements the read-only BootPackage manifest-size/chunked-read capability.
  • kernel/src/cap/manual.rs implements the read-only Manual capability: it parses the boot-packaged ManualCorpus blob (carried as the manual-corpus named binary) and answers page/apropos/topics/section/describe/ buildInfo. load_manual_corpus in kernel/src/cap/mod.rs resolves the blob’s bytes for the manual grant source, following the same split as the spawner’s binaries: the resident NamedBlob.data wherever it is real, and an on-demand digest-verified /boot/bins/ read under boot_iso, the one layout that leaves that data empty at cap-resolution time.
  • kernel/src/cap/log.rs implements the Phase 1 monitoring log surface: LogSink (write) and LogReader (read) over a shared bounded, drop-oldest kernel recent-record ring. The sink drops records below the boot-seeded SystemConfig.logLevel threshold and forwards accepted records to serial; the reader returns records at/after a cursor with LogFilter (minLevel/componentPrefix), nextCursor, and dropped (docs/proposals/system-monitoring-proposal.md).
  • kernel/src/cap/block_device.rs implements the BlockDevice CapObject (readBlocks/writeBlocks/info/flush). In the non-qemu production build the block_device source resolves to the userspace-brokered NVMe arm (BlockDeviceBackend::NvmeBrokered, gated by kernel/src/nvme_storage_backend.rs); the qemu build routes bounded inline-Data sector I/O to the kernel-owned virtio-blk driver in kernel/src/virtio.rs as a named fixture, not production storage (proof make run-virtio-blk). The cap is scoped to one device_index: the block_device source reaches the resolved non-target boot/storage disk, and block_device_target (KernelCapSource.blockDeviceTarget @44) reaches the manifest-selected PCI identity when it names a bound non-boot virtio-blk disk. A cap for one disk grants no authority over another. The kernel binds up to device_dma::MAX_VIRTIO_BLK_DEVICES (currently 2) virtio-blk devices, each with an independent driver/DMA-pool/interrupt-route instance (VirtioBlkDriver<const DEV> / VirtioBlkDma<const DEV> over VIRTIO_BLK_DMA_POOLS[DEV]); kernel/src/pci.rs enumerates each device with a device index (proof make run-multi-virtio-blk). Target grants fail closed when the selector is absent, mismatched, or names the resolved boot disk. Counts are bounded to one bounce-buffer page.
  • kernel/src/cap/readonly_fs.rs implements the read-only filesystem service: ReadOnlyFsDirectoryCap / ReadOnlyFsFileCap parse a fixed CAPOSRO1 on-disk layout read through the kernel-owned virtio-blk driver and serve Directory.list/open + File.read/stat; every mutating method fails closed. Granted via the read_only_fs_root KernelCapSource (returns a root Directory cap; qemu-gated, mounts at grant resolution and fails closed on a malformed/absent image). Host image builder tools/mkstore-image --readonly-fs; proof make run-storage-fs. An entry name only has to be non-empty UTF-8 without /, so names reach a consumer unsanitized: --readonly-fs-hostile builds the same image plus render-attack entries for make run-shell-fs.
  • kernel/src/cap/virtio_9p_fs.rs (cfg(any(qemu, virtio_9p_host_fixture))) serves the attached virtio-9p host share through the same interfaces: Virtio9pDirectoryCap (stateless) and Virtio9pFileCap (validated name + size observed at open, no server-side fid) implement Directory.list/open + File.read/stat/close over the crate::virtio ninep_* façade; every mutating method fails closed and these types call nothing in the driver’s write façade. Virtio9pWritableDirectoryCap/Virtio9pWritableFileCap are the separate writable pair: they delegate the read side to the types above and additionally serve Directory.create/remove/rename and File.write/sync over ninep_create/ninep_unlink/ninep_rename/ninep_write/ninep_fsync. mkdir/sub/truncate and an open carrying CREATE/TRUNCATE fail closed on both pairs (no Tmkdir/Tsetattr in the driver subset). Attenuation is structural – no rights flag, and no method turns one pair into the other – so a read-only export cannot be upgraded at runtime. validate_9p_name admits exactly one ordinary path element on every façade entry point, so the export cannot be traversed out of. Granted via the virtio_9p_root / virtio_9p_root_writable KernelCapSources, which mount_root() / mount_root_writable() resolve only when a device is bound; a kernel with neither fixture feature compiles no such module and resolves both sources to an error. The writable source and writable File results take NonTransferable holds rather than the read-only views’ Copy/SameSession. Share builder tools/mk-virtio-9p-share.sh; consumers demos/virtio-9p-fs and demos/virtio-9p-write; proofs make test-virtio-9p-fs and make test-virtio-9p-write (the latter verifies the resulting bytes on the host and proves a readonly=on share refuses the writable cap at the server), plus make test-virtio-9p-net-coboot for the Phase C Nic + writable 9p composition.
  • kernel/src/cap/persistent_store.rs implements the disk-backed persistent Store: DiskStoreCap serves the Store interface (put/get/has/ delete) over a fixed CAPOSST1 on-disk layout read and written through a read+write BlockSource seam. put bump-allocates a data extent, writes the blob and entry record, then rewrites the superblock last as the durability commit point; delete tombstones the entry slot, and a later space-exhausting put compacts live entries through a shadow generation before recommitting the canonical front generation; the mount validates the superblock and every entry extent in-bounds and fails closed on a malformed image. The Virtio BlockSource (qemu kernel) routes to the kernel-owned virtio-blk driver byte-identically (folding in the data_region_base_lba() offset) and mounts eagerly at grant resolution; the Nvme BlockSource (built under cloud_persistent_store_over_nvme_proof) reads/writes through a granted NVMe BlockDevice window op and defers its mount-parse to the first Store call. Granted via the persistent_store KernelCapSource (virtio arm qemu-gated; the third NVMe-proof arm resolves the live device_mmio handle). Host image builder tools/mkstore-image; reboot proof make run-storage-persist (two QEMU passes on one disk image); NVMe put-then-get proof make run-cloud-provider-persistent-store-over-nvme via kernel/src/cap/persistent_store_over_nvme_proof.rs.
  • kernel/src/cap/writable_fs.rs implements the disk-backed writable filesystem service: WritableDirectoryCap serves list/open/mkdir/remove/rename/ create and WritableFileCap serves read/write/stat/truncate/sync/ close over a fixed CAPOSWF1 on-disk layout (a flat node-record array with parent pointers + a bump-allocated data region) written through a BlockSource seam. The RAM tree is the working copy; each mutation write-through-commits in the order data sector → node-record sector → superblock. A filesystem-wide fail-closed single-writer policy admits one writer at a time. The Virtio BlockSource (qemu/installable kernels) routes to the kernel-owned virtio-blk driver byte-identically (folding the data_region_base_lba() offset) and mounts the singleton eagerly; the Nvme BlockSource (built under cloud_writable_fs_over_nvme_proof) reads/writes through a granted NVMe BlockDevice window op and defers the singleton mount-parse to the first Directory/File call. Granted via the writable_fs_root KernelCapSource (virtio arm qemu-gated; the third NVMe-proof arm resolves the live device_mmio handle), which mounts the process-wide singleton volume once and hands each grant a distinct writer id; fails closed on a malformed image. The NVMe write-then-read durability proof (make run-cloud-provider-writable-fs-over-nvme via kernel/src/cap/writable_fs_over_nvme_proof.rs, which supersedes and drops the persistent-store-over-NVMe proof) exercises both BlockDevice arms with the single-writer policy intact. The combined image builder tools/mkstore-image --writable co-locates the CAPOSST1 Store sub-volume (LBA 0) and the CAPOSWF1 filesystem sub-volume on one disk; reboot proof make run-storage-writable (two QEMU passes: mutate then verify both the filesystem and the store survive). A slot becomes live on the next mount only once the superblock’s bumped node_count is observed, so a poweroff in the record-written / superblock-pending window leaves an orphan slot the mount ignores. The proof-only storage_writable_recovery feature arms an induced forced poweroff in exactly that window (recovery_crash_after_record); bounded recovery proof make run-storage-writable-recovery (pass 1 commits then is kill -9d mid-allocation, pass 2 verifies recovery to a consistent tree with the interrupted allocation atomically absent). The same crash window is proven over the NVMe BlockDevice arm by make run-cloud-provider-writable-fs-over-nvme-recovery via kernel/src/cap/writable_fs_over_nvme_recovery_proof.rs (a recovery cap-waiter clone that implies and supersedes the happy-path proof module/route/init); the cloud_writable_fs_over_nvme_recovery_proof feature widens the storage_writable_recovery crash-window cfg gate, and the host-built NVMe image (tools/mkstore-image --writable-nvme, empty superblock + root-only node table) is booted twice with -device nvme (no @20 seed). writable_fs::mount_config_root (qemu-gated) scopes a writable Directory to the system/config subtree for the boot-time data-region grant below.
  • kernel/src/cap/installable_image.rs implements the read-only install-source fixture (Installable System track item 5b): InstallableImageDirectoryCap serves list/open and InstallableImageFileCap serves read/stat/close over the booted CD-ROM ISO 9660 /boot/bins/ tree, reading through the kernel/src/iso/ boot_iso ATAPI/ISO 9660 driver behind a single shared-device mutex (so PIO does not interleave across CPUs). Every mutating method fails closed; a past-EOF read clamps to empty and an absent name is rejected, reusing the driver’s validate_extent/read_sectors range checks. Granted via the qemu-gated installable_image_source KernelCapSource (mounts the ATAPI volume and validates /boot/bins/ at grant resolution, failing the spawn closed on an absent/malformed medium). Physically scoped to the ATAPI CD-ROM, so it cannot reach the writable virtio-blk target disk (block_device_target/writable_fs_root). Consumer demo demos/installable-image-source/; manifest manifests/system-installable-image-source.cue; proof make run-installable-image-source.
  • demos/installable-system-install/ implements capos-system-install, the Installable System install flow (track item 6): under the read-only installable_image_source Directory and the target-scoped block_device_target BlockDevice selected by manifest PCI identity, it copies the packaged bootable boot-region head (BOOTHEAD.BIN) to LBA 0, writes the backup GPT (BOOTGPT.BIN) at the LBA read from the primary GPT header, and initializes an empty data region (DATAIMG.BIN, tools/mkstore-image --writable --empty-config) at the fixed cap::data_region_base_lba, validating ranges and verifying the read-back. It reads packaged files in 32 KiB windows (under the read-path reply scratch bound; see storage-file-read-reply-scratch-clamp) and zero-skips the FAT free space. tools/split-boot-region.py splits the mkdiskimage boot image into the head + backup GPT so only the populated prefix is packaged. Pass-1 installer manifest manifests/system-installable-install.cue; pass-2 installed manifest (baked into the boot region) manifests/system-installable-install-target.cue; harness tools/qemu-installable-install-smoke.sh; proof make run-installable-install (pass 1 installs into a second virtio-blk disk, pass 2 boots it standalone).
  • kernel/src/cap/mod.rs grant_data_region (proof-only installable_data_region feature) is the Installable System boot-time data-region mount: run_init best-effort grants init a system/config Directory (data-config) plus the persistent Store (data-store) over the auto-attached data disk, failing closed wholesale to the base manifest (caps unchanged, “no data region; base floor” diagnostic) when the disk is absent, malformed, or missing system/config. No new cap type or schema change. Proof make run-installable-data-region (seeded disk prints resolved contents; no disk and zeroed-superblock disk hit the base floor).
  • Installable System config-overlay compose/merge (track item 3): the SystemConfigOverlay capnp object + SystemManifest.extensionPoints (ManifestExtensionPoints) live in schema/capos.capnp; the typed decode, content-hash check, and compose_onto precedence (base-pins-win / overlay-adds-within-declared-extension-points / no-new-authority) live in capos-config/src/manifest.rs. init/src/main.rs apply_config_overlay reads system/config/overlay.bin from the granted data-config Directory, composes the overlay over the base plan, and falls closed to the base floor with [init] overlay rejected: <reason>. The tools/mkmanifest mkoverlay bin encodes overlays (filling the canonical hash) and tools/mkstore-image --writable --seed-overlay seeds them. Proof make run-installable-overlay.
  • Installable System generations + rollback + failed-boot auto-fallback (track item 4): userspace-only over the already-granted Store + writable system/config Directory, no schema or kernel change. init/src/main.rs run_generation_rollback_checks (gated by a base service named generation-proof) represents system-config generations as content-addressed Store objects keyed by SHA-256, tracks the known-good active pointer and a staged/attempting candidate pointer as monotonic-epoch marker files (gen-active/gen-candidate) in the writable config region, records a boot attempt durably before applying a candidate, auto-falls-back to the known-good generation when a candidate is left unconfirmed (the brick-proofing guarantee), promotes a confirmed candidate, rolls config back to a retained prior generation, and rejects a stale/replayed (lower-or-equal-epoch) pointer. A present-but-undecodable gen-candidate marker (the torn size-0 file a poweroff inside the CREATE|TRUNCATE rewrite window leaves, or garbage bytes) is discarded with a loud diagnostic and boot falls back to the known-good generation, while a corrupt gen-active marker takes a distinct loud FATAL refuse-to-boot path (the known-good generation is genuinely unknown). Manifest manifests/system-installable-generation.cue; proof make run-installable-generation boots a --seed-config disk three times (boot 1 exercises the mechanism and leaves an unconfirmed candidate; boot 2 proves across-reboot auto-fallback to the known-good generation, then leaves a torn size-0 candidate marker; boot 3 proves torn-marker recovery).
  • Installable System integrated bootable disk (track item 5, proof-only installable_disk feature, implies installable_data_region): one disk carries the boot ESP (GPT partition 1) and the co-located CAPOSST1 Store + CAPOSWF1 writable data region (GPT partition 2). kernel/src/cap/mod.rs data_region_base_lba returns the fixed partition-2 base LBA (264192) under the feature (0 otherwise), applied at the single persistent_store/ writable_fs read_range/write_range choke points so the kernel reads the region at that fixed tool/kernel-contract LBA without parsing the GPT. tools/mkdiskimage.sh --data-image/--data-offset-bytes fold the tools/mkstore-image --writable image into partition 2 and derive the ESP size from --esp-sectors (integrated disk uses the same 128 MiB ESP as the raw disk-image targets so a debug kernel fits). Manifest manifests/system-installable-disk.cue; proof make run-installable-disk boots one virtio-blk disk and asserts the data region mounts from the boot disk and a data-region-only overlay service runs.
  • kernel/src/cap/frame_alloc.rs implements FrameAllocator and MemoryObject, plus prove_final_release_tlb_ordering (the memoryobject_final_release_ordering_proof boot-time -smp 2 proof that a same-drain final unmap + release returns frames only after the remote TLB acknowledgement; make run-memoryobject-final-release-ordering) and prove_tlb_frame_reuse_ordering (the tlb_frame_reuse_ordering_proof boot-time -smp 2 proof that a real anonymous-page unmap + defer_frame_free returns the frame – and reuses it at the same host physical address – only after the remote acknowledgement, the ordered flush-then-free contract VirtualMemory.decommit/unmap and commit rollback share; make run-tlb-frame-reuse-ordering).
  • kernel/src/cap/virtual_memory.rs implements per-process anonymous memory operations.
  • kernel/src/cap/timer.rs implements monotonic now and bounded sleep.
  • kernel/src/cap/wall_clock.rs implements the read-only WallClock.wallTime cap: UTC over a fixed boot base layered on the monotonic timebase, reporting the fail-closed untrusted ClockProvenance (Phase 1 fixed-boot-base variant; docs/proposals/time-and-clock-proposal.md).
  • kernel/src/cap/park_space.rs implements the process-local ParkSpace marker capability used by compact park (CAP_OP_PARK/CAP_OP_UNPARK) opcodes.
  • kernel/src/cap/notification.rs implements the Stage 6 IPC Notification signal/wait object: a latched-pending + revoked shared cell plus a global waiter table, delivered by the per-tick poll_waiters driver. Upholds no-lost-wake (signal racing ahead of wait is latched) and no-wake-after- drop (revoke/last-cap Drop release blocked waiters fail-closed). Minted fresh per notification grant; proof make run-notification-object.
  • kernel/src/cap/network.rs implements the qemu-only NetworkManager, TcpListener, TcpSocket, and UdpSocket fixture caps. The kernel no longer depends on smoltcp; non-qemu manifests reject the kernel network_manager / tcp_listen_authority grant sources (fail closed), and the production socket path is the Phase C userspace network-stack process. The socket-backed SocketTerminalSession shim is retired: TcpSocket.intoTerminalSession fails closed in every dispatch path.
  • kernel/src/cap/process_spawner.rs implements ProcessSpawner and ProcessHandle. ProcessHandle.createDebugSession is the owner-consented debug-attach mint (Debug and Trace Authority, Phase 1): it mints a redacted, read-only DebugSession result cap scoped to the child, audited to the kernel audit log, failing closed (audited denial) once the target exits.
  • kernel/src/cap/process_control.rs implements the ProcessControl cap (Live Upgrade, Phase 1): retargetCaps re-homes every endpoint-owner slot a process serves onto a successor process, all-or-nothing, for stateless (Case 1) upgrades. Targets are named by ProcessHandle caps in the caller’s own table and bound to the generation those handles were minted for, so only a spawner can retarget its own children and a recycled pid cannot inherit them. Client slots are never touched: CapId identity, service scope, and queued calls survive by construction. graceful fails closed unless old is quiesced on every endpoint moved – no call in flight (it could no longer RETURN it) and no RECV parked (a concurrent CALL would be delivered into it without taking old’s table lock); force disconnects in-flight callers with CAP_ERR_SERVER_DIED. Every attempt is audited (AuditEventType::Retarget). docs/proposals/live-upgrade-proposal.md; graceful proof make run-cap-retarget, force proof make run-cap-retarget-force (graceful refuses and force succeeds at one non-quiesced state; the in-flight caller observes CAP_ERR_SERVER_DIED, its CapId stays valid, and the retry is served by the successor).
  • kernel/src/cap/debug_session.rs implements the DebugSession cap (Debug and Trace Authority, Phase 1): capTableSnapshot returns a bounded, redacted read-only CapTableSnapshot of the target’s cap slots (slot index, interface id, generation, label, state) transferring zero result caps – no invokable handle or badge – and detach. Every snapshot is audited and gated on a live-target generation check; docs/proposals/debug-trace-authority-proposal.md; proof make run-debug-session.
  • kernel/src/cap/provider_cap_waiter_proof.rs (non-qemu, cloud_provider_cap_waiter_proof Cargo feature) stages a fully-programmed-route bootstrap Interrupt grant source and the InterruptCapWaiterProof cap whose Interrupt.wait injects one device_interrupt::handle_lapic_delivery dispatch and whose Interrupt.acknowledge retires the deferred LAPIC EOI; the cap’s on_release runs the masked-no-wake + reassign + stale-handle assertion chain before emitting cloudboot-evidence: provider-cap-waiter <token>. Mutually exclusive with cap::interrupt_grant_source_prod (default cloudboot path) and skips cap::provider_nic_bind_proof / cap::storage_bind_proof to keep the bound route live for the userspace cap-waiter handoff. Proof: make run-cloud-provider-cap-waiter.
  • kernel/src/cap/virtio_net_device_bringup_proof.rs (non-qemu, cloud_virtio_net_device_bringup_proof Cargo feature; mutually exclusive with cloud_provider_cap_waiter_proof and the userspace selected-write handshake proof) drives the bounded virtio status sequence kernel-side over the picked virtio-net PCI function (vendor 0x1af4, device 0x1000 / 0x1041): resolves the modern virtio PCI transport regions through virtio_transport::parse_modern_pci_transport_capabilities, maps the common configuration window through pci::map_bar_region, and drives reset → ACKNOWLEDGE → DRIVER → feature discovery + driver-feature selection (VIRTIO_F_VERSION_1 only) → FEATURES_OK → DRIVER_OK with a trailing reset on every exit path. Inline assertions gate the headline cloudboot-evidence: virtio-net-device-bringup <token> on the negotiated feature set, COMMON_NUM_QUEUES >= 2, DRIVER_OK observation, and the final reset returning device_status to 0. Marker carries queue_setup=not-attempted, tx_descriptor=not-published, userspace_cap=not-issued, msix_function_enable=not-toggled, device_autonomous_raise=not-attempted, live_cloud=not-attempted. Proof: make run-cloud-provider-virtio-net-bringup.
  • cloud_virtio_net_userspace_features_ok_proof (non-qemu; proof make run-cloud-prod-nic-driver-userspace-features-ok) is Phase C slice 1 of the userspace NIC relocation track. It makes cap::devicemmio_grant_source_prod stage the picked virtio-net modern common-config window as a selected-write DeviceMmio cap with registerWrite=selected-write-common-config-handshake; the userspace smoke drives reset -> ACKNOWLEDGE -> DRIVER -> FEATURES_OK over DeviceMmio.write32 and proves queue-address writes remain fail-closed. It is mutually exclusive with the kernel-owned virtio-net bringup, bundle, and queue-materialization proof chain over the same BDF/grant path, and with the cloud_nvme_readonly_bind_proof descendant chain because both stage a proof-specific production DeviceMmio grant source.
  • kernel/src/cap/virtio_net_tx_authority_bundle_proof.rs, kernel/src/cap/virtio_net_tx_queue_materialization_proof.rs, and kernel/src/cap/virtio_net_msix_function_enable_proof.rs are the decomposed userspace-TX track. Each is non-qemu and gated by its own focused-proof Cargo feature (cloud_virtio_net_tx_authority_bundle_proof, cloud_virtio_net_tx_queue_materialization_proof, and cloud_virtio_net_msix_function_enable_proof respectively; the last implies the second so the bundle observer + production grant-source pickers + userspace bundle smoke stay compiled in across the chain). The bundle proof observes the three production grant sources (devicemmio_grant_source_prod, dmapool_grant_source_prod, interrupt_grant_source_prod) issuing one cap each into the spawned userspace bundle smoke and asserts same-BDF; the queue-materialization proof drives the kernel-side modern-virtio status sequence through DRIVER_OK and materializes one manager-owned TX virtqueue from three zeroed brokered frames, asserting register read-backs and post-reset clearance; the MSI-X function-enable proof extends that sequence with one canonical mask-first PCI MSI-X function-level enable (set FUNCTION_MASK, then ENABLE, then clear both) plus best-effort cleanup on every exit path. Each child emits its own headline marker (cloudboot-evidence: virtio-net-tx-authority-bundle <token>, cloudboot-evidence: virtio-net-tx-queue-materialization <token>, and cloudboot-evidence: virtio-net-msix-function-enable <token>); when the later feature is active the earlier markers are intentionally suppressed because their discipline labels would be inaccurate. Proofs: make run-cloud-provider-virtio-net-tx-authority-bundle, make run-cloud-provider-virtio-net-tx-queue-materialization, make run-cloud-provider-virtio-net-msix-function-enable.
  • kernel/src/cap/virtio_net_userspace_rx_dma_proof.rs (Phase C slice 4a-ii, gated cloud_virtio_net_userspace_rx_bringup_proof) drives the first real RX DMA from the shim-owned vring: post_rx_descriptor writes the RX descriptor
    • avail over the shim’s retained RX vring physes at DMABuffer.submitDescriptor time, and drive_rx_dma (reached from the now-live provider_notify_doorbell_write_for_cap) rings the RX doorbell, submits a kernel-half SLIRP TX ARP stimulus over the retained TX physes, polls one real device->host completion, and resets the device (clearing the retained enabled flags to release the ring-buffer pins). Self-contained byte-level vring helpers are duplicated from virtio_net_polled_provider to protect run-net. The notify region is mapped kernel-side + the per-queue notify slot offsets captured by cap::devicemmio_grant_source_prod (rx_dma_notify_state). Proof make run-cloud-prod-nic-driver-userspace-rx-bringup (extended).
  • kernel/src/cap/null.rs implements the measurement-only NullCap.
  • kernel/src/cap/park_bench.rs implements the measurement-only ParkBench authority used by make run-measure.

Related docs: Capability Model, Authority Accounting.

Userspace

  • init/ is the standalone init process. In the spawn smoke, it uses ProcessSpawner, grants initial child capabilities, waits on ProcessHandles, and checks hostile spawn inputs. Its linker.ld defines the standalone userspace image layout; the nested demos/ workspace uses its own demos/linker.ld.

  • capos-rt/src/entry.rs owns the runtime entry path and bootstrap validation.

  • capos-rt/src/alloc.rs initializes the userspace heap.

  • capos-rt/src/syscall.rs provides raw syscall wrappers.

  • capos-rt/src/capset.rs provides typed CapSet lookup helpers.

  • capos-rt/src/ring.rs implements the safe single-owner ring client, out-of-order completion handling, transfer descriptor packing, and result-cap parsing. It also carries the promise-pipelining client surface: AnswerId / PromiseId values over a process-local answer-id allocator, and RingClient::submit_pipelined_call_batch, which admits the answer-allocating CALL and its dependent together and publishes both with a single SQ tail store. For endpoint antecedents the kernel may resume that frozen batch after a later RETURN without admitting newer submissions into its promise scope.

  • capos-rt/src/client.rs implements typed clients for Console, TerminalSession, BootPackage, ProcessSpawner, ProcessHandle, and Timer. The client-side methods are generic over Transport; result-cap-adopting methods stay on the concrete RuntimeRingClient.

  • capos-rt/src/transport.rs defines the Transport seam (the client-side CALL/completion/RELEASE ring operations) and the in-system RingTransport (RingClient viewed through the seam). A host remote transport is a later slice; see docs/backlog/capos-sdk-dual-transport.md.

  • capos/ is the front-door SDK facade crate: for the default ring feature it re-exports the capos-rt runtime, typed clients, the entry_point! macro, and a prelude. The remote feature is reserved. Standalone, like capos-rt.

  • capos-python/ is the host-only pyo3 (abi3-py39) cdylib that maturin packages as the capos PyPI distribution (Cargo [lib].name = "capos"). It is the working base for the host-side SDK: capos.Client binds tools/remote-session-client (path dependency) to connect a running capOS, authenticate, list the forwarded CapSet, and read session metadata plus the running kernel’s hostname/version/commit/timestamp identity. examples/hello_live.py is the live hello-world (drives a real gateway and prints the kernel’s response; recorded under docs/assets/casts/); examples/ holds the other runnable scripts; tests/test_capos.py is a VM-free host pytest of the binding surface. It depends only on host crates (never the bare-metal ones); the transitive capos-config build script runs the pinned capnp compiler, which the release workflow’s wheel job builds in-container. Its .cargo/config.toml overrides the repo-root bare-metal target to the host glibc target, and .github/workflows/python-release.yml publishes it on python-v* tags via PyPI trusted publishing.

  • capos-js/ is the host-only pure-TypeScript/ESM capos npm distribution: a dependency-free Node (>=20) client over the remote-session-ui loopback bridge’s HTTP API. src/client.ts Client bootstraps the bridge session and CSRF cookies with a GET, then reproduces the Origin + CSRF double-submit guard on each POST (connect, loginAnonymous/loginPassword, listCapset, sessionInfo, systemInfo, systemMotd, authMethods, logout); src/types.ts mirrors the bridge’s camelCase view-model DTOs; index.ts adds hello()/VERSION. examples/hello.mjs is a VM-free runnable script; test/client.test.mjs is a host node --test suite over an in-process mock bridge. Built with tsc to dist/; talks only HTTP (no native addon, no capnp build). Not a workspace member.

  • capos-rt/src/pollselect.rs is the pure POSIX poll/select bridge: SocketReadiness -> poll revents (POLLIN/POLLOUT/POLLHUP/POLLERR/ POLLNVAL) and select set membership, plus unsupported_request_bits for fail-closed flag handling. Shared by the libcapos-posix C surface and the posix-socket-poll-select-smoke proof. Proof: make run-posix-socket-poll-select.

  • capos-rt/src/console_text.rs is the pure console-render charset every userspace renderer of producer-supplied text applies before writing through a Console/TerminalSession cap. Both functions emit only printable ASCII (0x20..=0x7E) and differ in what they do with the rest.

    • sanitize_console_text is lossy: everything else becomes .. It is an allowlist, not a control-character denylist, because a denylist passes the Unicode format characters a bidi-aware renderer honours (U+202E, U+200B). Source of truth for the shell’s log builtin (shell/src/main.rs), the task-coordinator HTTP adapter (demos/task-coordinator-api-logic, re-exported as sanitize_log_text), and the task-coordinator service (demos/task-coordinator-service, applied at its write_console seam because its own key/worker validation is length-only) – diagnostic fields that are ASCII by protocol.
    • escape_console_text is lossless: \ doubles, CR/LF/TAB take named forms, anything else becomes \u{<hex>}. The mapping is injective, so distinct inputs stay distinct in the render. That is what a Directory listing needs: a .-cut renders two entries that differ only outside ASCII identically, hiding a hostile near-copy of a name the operator trusts, and reduces the UTF-8 text cat exists to display to a row of dots. (Neither cut makes a non-ASCII name typeable; the claim is distinguishability, not round-tripping.)
    • escape_console_text_bounded is that same cut stopped at a byte budget, truncating between escape units so the retained prefix decodes as it would unbounded. It is the variant the shell’s ls/cat actually call (shell/src/main.rs escape_for_line), because escaping expands – up to 10x per char – while the kernel rejects a TerminalSession.writeLine over MAX_SERIAL_CAP_WRITE_BYTES (kernel/src/serial.rs) rather than truncating it, and the shell treats a failed render write as fatal. Bounding the read cannot bound the render; a renderer that escapes producer-supplied text into a bounded transport must bound the output. ls/cat render Directory-supplied entry names and file bytes, and this path has no upstream sanitizer – the kernel cut below covers LogReader records only – so these renderers are both the only cut and the only bound.

    The kernel LogSink applies the lossy charset independently at LogEntry::new (kernel/src/cap/log.rs::copy_sanitized, byte-level over a fixed record buffer); the module doc records why that copy is not shared. Proofs: make capos-rt-test, make run-shell-log, make run-shell-fs (hostile entry name and hostile file content), make run-task-coordinator-api, make run-task-coordinator.

  • capos-rt/src/panic.rs provides the emergency Console panic output path.

  • capos-rt/src/bin/smoke.rs is the runtime smoke binary used by focused runtime proofs rather than the default boot manifest.

  • capos-service/src/lib.rs is the standalone no_std service lifecycle layer above capos-rt; slice 1 exposes ServiceMain, ServiceRuntime, and ordered initialize/dependency-wait/ready/run/drain/shutdown/cleanup phases. demos/task-coordinator-api-service exercises that complete order in QEMU; tools/qemu-task-coordinator-api-smoke.sh asserts the marker sequence under make run-task-coordinator-api.

  • shell/src/main.rs is the native capability shell, built as the standalone capos-shell crate and packaged by system.cue, manifests/system-shell.cue, and the focused login manifests. Operator commands read only through granted caps: date/uptime over granted WallClock/Timer, ls/cat over a granted read-only Directory (root), and log over a granted read-only LogReader (log), each fail-soft when its cap is absent.

Validation: make capos-rt-check, make capos-rt-test, make run-smoke, make run-spawn, make run-shell, make run-shell-uptime, make run-shell-log, make run-shell-fs, make run-terminal. The former Telnet fixture is retired with the qemu-only kernel TCP listener.

Standalone C and WASI Substrates

These are standalone crates (not workspace members) built by the Makefile.

  • libcapos/ builds libcapos.a, a no_std Rust staticlib exposing the capos-rt syscall/ring/CapSet path and typed Console/Timer/WallClock/ EntropySource/VirtualMemory wrappers plus C heap shims to C consumers. Public header at libcapos/include/capos/capos.h. No POSIX surface.
  • libcapos-posix/ builds libcapos_posix.a, a no_std Rust staticlib layering a POSIX adapter over libcapos: per-process fd table, errno cell, historical UDP socket wrappers over the retired qemu-only kernel UdpSocket cap, clock over Timer, pipe/dup over Pipe, poll/select (poll.rs, <poll.h>/<sys/select.h>) over the capos-rt::pollselect readiness bridge with fail-closed unsupported-flag / EBADF / EINVAL handling, and fork/execve/waitpid via the recording-shim ProcessSpawner Move-grant path. subprocess.rs layers system() and Pipe-backed popen()/pclose() on that shell-spawn path, with focused QEMU proof make run-posix-system, plus the libc surface the dash port needs: stdio/string/stdlib/ctype helpers, strerror/qsort/umask/abort/ strtoll/strpbrk/lstat/getgroups/wait3/vfork, byte-order helpers (inet.rs), getrlimit/setrlimit (resource.rs), setlocale (locale.rs), times + tcgetattr, C-locale wchar/wctype multibyte (wchar.rs), the environ pointer, and the sys_siglist array. C headers (the namespaced source of truth) under libcapos-posix/include/capos/posix/ – including the dash-needed sys/types.h, termios.h, sys/resource.h, sys/times.h, wchar.h, wctype.h, locale.h, inttypes.h, and the decl-only sys/ioctl.h/sys/mman.h/arpa/inet.h/getopt.h/paths.h/ sys/param.h. libcapos-posix/sysroot/include/ is the -nostdinc bare-header sysroot (<stdio.h>, <unistd.h>, <sys/stat.h>, …) whose wrappers forward into that namespace; mirrored C ports (dash) build against it via the Makefile’s CAPOS_C_SYSROOT_INCLUDE flags on the capos-c-multitu-elf rule. Focused sysroot proof make run-c-libc-surface.
  • capos-wasm/ is the no_std WASI host adapter: a wasmi-backed Runtime, the wasm-host userspace binary, the Preview 1 import resolver, and the manifest-supplied wasm payload reader.
  • vendor/wasmi-no_std/ and vendor/dns-c-wahern/ are static-pinned, no-patches upstream snapshots consumed by capos-wasm/ and the POSIX DNS smoke; do not patch them in place (refresh procedure in each VENDORED_FROM.md).
  • vendor/dash/ is the mirror-as-is dash 0.5.13.4 snapshot (src/ stays byte-identical; capOS deviations live under patches/). Its capOS build pipeline lives outside the mirror under vendor/dash/capos/: the pinned config.h and gen-tables.sh (stages a patched source copy + runs the six host table generators). The Makefile dash target builds target/dash/dash.elf through capos-c-multitu-elf against libcapos.a + libcapos_posix.a.

Validation: make run-c-hello, make run-posix-pipe-smoke, make run-posix-printf, make run-wasm-host, make run-wasi-hello-rust, make run-wasi-random. The former POSIX DNS smoke is retired with the qemu-only kernel UdpSocket owner.

Demo Services

demos/ is a nested userspace smoke-test workspace. Each demo is a release-built service binary packaged into the boot manifest:

  • adventure-client, adventure-server, adventure-npc-shopkeeper, adventure-npc-wanderer
  • capos-chat, chat-bot, chat-client, chat-server
  • capset-bootstrap, console-paths, credential-store
  • endpoint-queue-limit-smoke, endpoint-roundtrip, ipc-server, ipc-client, in-flight-call-limit-smoke
  • frame-allocator-cleanup, memoryobject-shared-child, memoryobject-shared-parent
  • paperclips, paperclips-content
  • revocable-read, revocation-observer
  • ring-corruption, ring-reserved-opcodes, ring-nop, ring-fairness
  • service-common, shell-spawn-test, shell-typed-call
  • task-coordinator-logic, task-coordinator-proto, task-coordinator-service, task-coordinator-client-smoke (task-backend coordinator local proof: host-testable pure coordination rules, a demo-local Cap’n Proto Endpoint protocol with its own schema under demos/task-coordinator-proto/schema/, the coordinator service, and the acceptance client). Without a state cap the service is in-memory (make run-task-coordinator). With a spawn-granted writable 9p Directory, it uses canonical hex-encoded current/temp/backup task files with bounded fail-closed recovery; manifests/system-task-coordinator-9p.cue, tools/qemu-task-coordinator-9p-smoke.sh, and make test-task-coordinator-9p prove reload over two boots and host-visible state. task-coordinator-logic owns both persistence seams: TaskSnapshot, Coordinator::snapshot/snapshots, boot rebuild through restore_task, the fail-closed record codec encode_record/decode_record, and the 9p filename and recovery planner (make task-coordinator-logic-test)
  • task-coordinator-persist-proof (task-backend phase-3 third increment: durable coordinator persistence over BlockDevice. Drives the real task-coordinator-logic coordinator write-through onto the capos-lib CAPOSRS1 WAL record store – each mutation commits the task’s snapshot as one atomic frame keyed by task:<key>, secondary-indexed by status:<label>; boot rebuilds live state from the log. Three boots of one disk image prove reboot reload and bounded forced-poweroff torn-write recovery. manifests/system-task-coordinator-persist.cue, tools/qemu-task-coordinator-persist-smoke.sh, make run-task-coordinator-persist)
  • task-coordinator-api-logic, task-coordinator-api-service (task-backend phase-2 HTTP/JSON API surface: host-testable bounded HTTP/JSON contract rules tracking the loopyard task-source/lock wire shapes, and the thin adapter service over the Phase C userspace network-stack listener – the first in-tree capos-service lifecycle consumer; host harness tools/qemu-task-coordinator-api-smoke.sh, make run-task-coordinator-api, make task-coordinator-logic-test). The persistent composition in manifests/system-task-coordinator-api-9p.cue keeps the same userspace Nic and adapter topology while granting a writable 9p state cap only to the coordinator. tools/qemu-task-coordinator-api-9p-smoke.sh and make test-task-coordinator-api-9p prove API-visible state and fencing reload over two boots; the adapter remains storage-blind. The same harness has an opt-in host-worker mode used by make test-task-backend-vibe-adapter-9p: tools/capos-task-backend-adapter.py maps the installed vibe-loop task-source and fenced-lock command contracts onto the loopback API, while tools/test_capos_task_backend_adapter.py provides the bounded host contract tests run by make task-backend-vibe-adapter-test.
  • notification-object (Stage 6 IPC Notification signal/wait proof: one process, two threads sharing one notification cap; proves signal-wakes-waiter, wait-timeout, no-lost-wake, and revoke-releases-waiter + no-wake-after-drop; tools/qemu-notification-object-smoke.sh, make run-notification-object)
  • promise-pipeline (Stage 6 promise-pipelining proof: answer-allocating CALLs and dependent CALLs submitted as one batch and completed through one cap_enter; proves kernel-served and endpoint RETURN success, endpoint server-death failure, load-bearing result-cap ordinals, a kernel-owned answer record count that caller-buffer forgery cannot extend, and the antecedent-failed / unknown-answer / ordinal-out-of-range fail-closed paths; tools/qemu-promise-pipeline-smoke.sh, make run-promise-pipeline)
  • debug-session-parent, debug-session-child (Debug and Trace Authority, Phase 1: a supervisor mints a DebugSession over a spawned child via ProcessHandle.createDebugSession, reads a redacted capTableSnapshot cross-checked against CapabilityManager.list and proven to transfer no invokable cap, then shows attach/snapshot fail closed with audited denials once the target exits; tools/qemu-debug-session-smoke.sh, make run-debug-session)
  • terminal-session, terminal-stranger
  • timer-smoke, timer-flood
  • tls-smoke, unprivileged-stranger, virtual-memory
  • user-fault-parent, user-fault-victim (user fault containment proof, make run-user-fault)

Shared demo support lives in demos/capos-demo-support/src/lib.rs and uses capos-rt for entry, allocator, syscall, CapSet, and panic support while keeping raw ring helpers for low-level transport smokes.

Validation: make run-spawn.

Manifest and Tooling

  • system.cue is the default init-owned boot manifest source. It imports the shared defaults package, boot-launches standalone init, and lets init start the shell, remote-session CapSet gateway, and resident services.
  • manifests/system-spawn.cue is the ProcessSpawner smoke manifest source.
  • manifests/system-smoke.cue is the scripted focused shell-led login/shell smoke manifest source.
  • manifests/system-chat.cue, manifests/system-adventure.cue, and manifests/system-paperclips.cue are focused resident-service and terminal-demo manifest sources.
  • manifests/system-memoryobject-shared.cue, manifests/system-revocable-read.cue, and manifests/system-measure.cue are focused regression/measurement manifest sources.
  • manifests/system-session-context.cue, manifests/system-local-users.cue, and manifests/system-ipc-zerocopy.cue are the focused session-context, local operator, and zero-copy IPC proof manifests.
  • manifests/system-shell.cue is the focused anonymous-shell manifest source (no verifier, shell stays anonymous).
  • manifests/system-terminal.cue is the focused TerminalSession proof manifest source.
  • manifests/system-credential.cue is the focused CredentialStore proof manifest source.
  • manifests/system-credential-setup-authority.cue is the focused proof that credential creation authority (ConsoleSetup) is strictly narrower than credential status/verify authority (CredentialStore): the ConsoleSetup cap installs the first password while a CredentialStore holder’s retired method-3 dispatch fails closed (make run-credential-setup-authority).
  • manifests/system-login.cue is the focused password-login proof manifest source.
  • manifests/system-login-setup.cue is the focused first-boot setup proof manifest source.
  • tools/mkmanifest/ evaluates manifest input, embeds binaries, validates manifest shape, writes boot-manifest Cap’n Proto bytes, and provides cue-to-capnp for schema-aware CUE-authored data-message conversion. Its sibling mkoverlay bin encodes a SystemConfigOverlay from CUE into the system/config/overlay.bin bytes (filling the canonical content hash) for the installable-system config-overlay proof.
  • tools/manualc/ is the System Manual corpus compiler: it parses schema/capos.capnp for section-2 interface pages, reads the authored man corpus under docs/manual/man<section>/*.man, and emits the boot-packaged ManualCorpus blob. It fails the build if any in-tree capability interface lacks a section-2 page (i.e. a schema doc comment).
  • docs/manual/ holds the authored man-shaped corpus consumed by manualc (section 1 shell-command pages and section 7 concept pages); section-2 capability pages are generated from the schema, not stored here.
  • manifests/system-manual-smoke.cue is the focused Manual proof manifest source.
  • tools/agent-session-recaps/ contains private-session recap and raw-archive tooling for the agentic development experiment. The tools are tracked here; raw transcripts and generated recap stores stay outside the repo unless explicitly redacted and reviewed.
  • tools/check-generated-capnp.sh verifies checked-in generated schema output.
  • loopyard vibe worklog emits per-task commit spans (from each task’s commits list, falling back to commit history) for the development timeline/Gantt; scripts/validate_backfill_tasks.py validates backfilled task frontmatter against the chunk’s real SHAs; scripts/check-md-links.py is the pre-commit broken-relative-link gate over all .md.
  • tools/githooks/ is the repo core.hooksPath (enabled with make hooks): prepare-commit-msg stamps provenance trailers (Plan-Item/Run-Id/ Agent-Kind) onto run-driven commits, alongside the git-lfs hooks.
  • tools/qemu-net-harness.sh runs the current QEMU net harness, with tools/qemu-net-smoke.sh asserting virtio-net transport, MSI-X metadata selection, kernel-owned MSI-X vector-pool allocation/programming, masked route-lifecycle proof, queue vector assignment, descriptor guards, ARP, and ICMP fixture lines.
  • tools/container-build/ holds the opt-in canonical-path compile container: a Dockerfile carrying distribution packages only (base image digest-pinned), and capos-container-build.sh, which bind-mounts the worktree at /build and runs the ordinary make recipes inside for an allowlisted set of compile-only goals. The fixed mount path is what lets sccache share first-party output across worktrees, since it hashes the compile working directory unconditionally. The Rust toolchain and the pinned capnp stay host-provisioned and are bind-mounted. capos-build-mode.sh is the fail-closed guard that keeps host and container output out of one target directory – a mix yields a kernel whose compilation units disagree about their build root with no build-time signal – plus its self-test (make container-build-mode-test). See docs/backlog/containerised-build-canonical-path.md.
  • fuzz/ contains fuzz targets for manifest Cap’n Proto decoding (with the production reader-options envelope), mkmanifest JSON conversion/validation, ELF parsing, Telnet IAC filtering, terminal line discipline, ring SQE wire validation, 9P2000.L reply decoding, ISO 9660 PVD/directory-record parsing, the CAPOSRO1/CAPOSST1/CAPOSWF1 storage mount parsers, and the capos-tls X.509 validity walk.

Validation: cargo test-mkmanifest, make generated-code-check, make fuzz-build, make fuzz-smoke.

Documentation

  • docs/capability-model.md is the current capability architecture reference.
  • docs/architecture/threading.md and docs/architecture/park.md record the accepted contracts and first implementation for in-process thread ownership and private ParkSpace authority.
  • docs/*-design.md files record targeted implemented or accepted designs.
  • docs/proposals/ contains accepted, future, exploratory, and rejected designs.
  • docs/research/ summarizes prior art (the capability-systems-survey.md synthesis plus per-system deep-dive reports).
  • docs/proposals/mdbook-docs-site-proposal.md defines the documentation site structure and status vocabulary used by the orientation pages.