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.mdgives the compact project overview.Cargo.tomldefines the Rust workspace and shared build profiles.limine.confconfigures the bootloader entry used by the ISO.docs/roadmap.mdrecords long-range stages and broad feature direction.- Live task state – the selected milestone (
selected_milestoneproject 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 theloopyardCLI. The retireddocs/tasks/file ledger is preserved only in git history;REVIEW_FINDINGS.mdis a tombstone for pre-migration links. REVIEW.mddefines review expectations.Makefilebuilds pinned tools, userspace binaries, manifests, ISO images, QEMU targets, formatting checks, generated-code checks, and policy checks.rust-toolchain.tomldeclares the Rust nightly channel, required targets, andrust-src; it does not pin an exact nightly by date or commit..cargo/config.tomlsets the default bare-metal target and useful cargo aliases.
Schema and Shared ABIs
docs/abi-evolution-policy.mddefines compatibility classes, schema ordinal rules, ring-layout rules, version negotiation, and deprecation windows for externally visible ABI changes.schema/capos.capnpdefines capability interfaces, manifest structures, exceptions, ProcessSpawner, ProcessHandle, and transfer-related schema.capos-abi/src/lib.rsdefines small no_std ABI/policy constants shared by crates that should not depend on schema/config internals, including process quotas, credential policy limits, and theAuditLog.recordtext/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.rsdefines the host and no_std manifest model.capos-config/src/validation.rsowns manifest graph and bootstrap validation policy.capos-config/build.rsinvokes the shared Cap’n Proto code-generation and no_std patching helper.capos-config/src/ring.rsdefinesCapRingHeader, SQE/CQE structures, opcodes, flags, and transport error constants shared by kernel and userspace.capos-config/src/capset.rsdefines the read-only bootstrap CapSet ABI.capos-config/src/cue.rssupports evaluated CUE-style manifest data.capos-config/src/credential_policy.rsre-exports credential policy limits; full PHC parsing is enabled by thecredential-validationfeature for bootstrap validators that need credential checks.capos-config/tests/ring_loom.rsmodels 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.rsparses ELF64 images for kernel loading and host tests.capos-lib/src/cap_table.rsimplementsCapId, capability-table storage, stale-generation checks, grant preparation, transfer transaction helpers, commit, rollback, and the CapTable quota constants sourced fromcapos-abi.capos-lib/src/credential_admission.rsis 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 kernelkernel/src/cap/credential_store.rscomposes it with the real arena. Its WebUI-ingress counterpart,WebUiIngressLedgerindemos/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 effectiveIngressProfilefields (host-tested;make webui-login-peer-logic-test). The siblingSessionBudgetLedgerin 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 inmain.rsdrives both ledgers live and emits balanced quiescentcloudboot-evidence: webui-ingress-ledger/webui-session-budgetlines the L4 gate asserts (make run-cloud-prod-remote-session-web-ui-l4).capos-lib/src/cloud_store_bridge.rsimplements the bounded, scope-bound provider-neutral local fake behind theCloudStoreBridgeABI: 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.rsimplements the host-testable physical frame bitmap core.capos-lib/src/frame_ledger.rscontains a bounded frame-grant helper kept for host-test coverage; current MemoryObject accounting chargesCapTable::ResourceLedger.capos-lib/src/lazy_buffer.rsprovides bounded lazy buffers used by ring scratch paths.capos-lib/src/ninep.rsimplements 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, andRlerror, 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 serveDirectory/Filecapabilities; fuzz targetninep_reply_decodeexercises reply decoding.capos-lib/src/transport_seed.rsdecides where the userspace network stack’s smoltcprandom_seedcomes from: theTransportSeedprovenance type (per-boot entropy vs named proof fixture, with a value-redactingDebug), the domain-separated SHA-256 derivation of the listener seed, the DHCP-client seed, and the publishable per-boot witness from oneEntropySourcedraw, and the fail-closedProductionEntropyRefusalvocabulary the serving path reports when production entropy is missing, dead, short, or degenerate.capos-lib/src/iso9660.rsis the pure ISO 9660 primary-volume-descriptor and directory-record parser the kernel boot-ISO driver (kernel/src/iso/) delegates to; fuzz targetiso9660_volume.capos-lib/src/storage_format.rsholds the pureCAPOSRO1(rofs),CAPOSST1(disk_store), andCAPOSWF1(writable_fs) mount parsers the kernel storage cap backers delegate to, including the shared record-layout constants the kernel writers reuse; fuzz targetsstorage_rofs_mount,storage_disk_store_mount,storage_writable_fs_mount.capos-lib/src/recordstore.rsis theCAPOSRS1transactional WAL record store: atomic multi-record commit frames over the abstractBlockIoblock 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 targetrecordstore_mount. TheBlockDevicewiring lands the seam in-system:demos/record-store-blockdevice(capos-demo-record-store-blockdevice) persists this WAL through the typedBlockDevicecap 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 bydemos/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.rsbuilds and verifies X.509 paths over the vendoredrustls-webpki, returningVerificationOutcome/ValidChain;trust.rsis the RAM-only anchor set seeded from vendoredwebpki-roots;cert.rsis the typed field surface over a DER certificate, including thenotBefore/notAfterwalk (fuzz targetx509_validity).capos-tls/src/pki_algs.rsisp256_sha256_algorithms, ECDSA P-256/SHA-256 over thep256crate – the whole signature-verification surface capOS accepts today. The verifier core is crypto-provider-free and takessupported_algsas a parameter, so this is the set a bare-metal caller passes; the wider ring-backedalgorithmsset inlib.rsis gated behind the host-test-onlywebpki-ringfeature, becauseringdoes not build forx86_64-unknown-none.capos-tls/src/key.rsholds the RAM-only key cores:RamSymmetricKey,RamPrivateKey/PublicKey(P-256/ES256),RamKeyVaulthandle custody, and the development-onlyDevelopmentSoftwareKeySource. No raw private-key export path exists on any of them; that absence is the custody property.capos-tls/src/entropy.rsisDrawnEntropy, the bridge between anEntropySourcecap and the infalliblerand_coretraits 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 fromtry_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 theTlsServerSignerseam so the key never enters the handshake types.tls13/alert.rsowns 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 onehandshake_failure, and deprotection failure says onlybad_record_mac.TlsServerHandshake::take_alerthands the consumer the fatal alert a failedfeedowes;close_notifycloses a completed connection cleanly.capos-tls/src/selfsigned.rsissues development self-signedserverAuthcertificates 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.rsis the local RFC 8555 account/order/finalize client plus the bounded token-scopedHttp01ChallengeSolverand theLocalAcmeDirectoryproof fixture.capos-tls/src/der.rsis 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 incert.rsand the vendoredrustls-webpki; this side only encodes.capos-tls/src/certstore.rsis the rotation seam: a stable handle names the chain a TLS server presents,putreplaces it in one step and notifieswatchsubscribers, andgetresolves 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.rsisRenewalPolicy, the pure “is it due” decision: a lead beforenotAfterso a failed issuance can be retried while the current chain is still servable, distinguishingDuefromExpired. No clock and no ACME client; the caller suppliesnowand 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.lddefines the higher-half kernel layout and exported section boundaries used by paging.kernel/src/main.rsis the boot entry point, hardware setup sequence, manifest parsing path, and boot-launched service creation path.run_initresolves PID 1 from the kernel-embeddedboot::INIT_ELFwheninitConfig.init.binary == capos_config::RESERVED_INIT_BINARY_NAME("init") and otherwise fromSystemManifest.binaries; for the embedded case it also injects the embedded image into theProcessSpawnerbinary set under the reserved name so child spawns ofinitresolve.kernel/src/boot.rsexposesboot::INIT_ELF: &[u8], the PID 1 init image packaged at build time.kernel/build.rsreads the prebuiltinit/artifact (CAPOS_INIT_ELF, with a conventional-path fallback) and generates theinclude_bytes!static;init/stays a standalone crate (byte packaging, not linker merging).kernel/src/spawn.rsloads user ELF images, creates process state, maps bootstrap pages, and enqueues spawned processes.kernel/src/process.rsdefinesProcess,Thread,ThreadState, per-thread kernel stacks, park waiter storage, and userspace CPU context.kernel/src/session_context.rsdefines immutable per-process invocation session metadata.kernel/src/sched.rsimplements the single-CPU scheduler, timer-driven preemption, blockingcap_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 theCrashKindand faulting instruction pointer; the process teardown path emits the redacted[audit] event=crashrecord after cap revocation, so no record can observe live authority. A plannedexitnotes nothing and produces no record. Proofmake run-crash-disconnect.kernel/src/serial.rsimplements COM1/COM2 UART setup, manifest-driven console-vs-terminal routing, and kernel print macros.kernel/src/pci.rsimplements 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.rsrecords 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.rsholds the kernel-owned, fixed-size DMA pool accounting ledgers. The net-keyedVIRTIO_NET_DMA_POOLbacks virtio-net’sDmaPagepath. The single-request-queue devices share oneSingleQueueDmaLedger<C, PAGES>shape (reusing the sharedActivePage/QueueAccounttypes, same generation-checked handle and scrub-before-free invariants), instantiated per device through aSingleQueuePoolConfigthat supplies the owner/pool audit strings, the legal queue index, and the depth budget:VirtioBlkPoolConfigbacks the virtio-blk request buffer andVirtio9pPoolConfigthe 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’sVirtqueueDmaseam 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 indocs/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 undercfg(feature = "qemu")inqemu_full.rs; the MMIO-only surface used bycap::device_mmioexists in both builds, dispatching tostub.rs(one-slot parked-regionDeviceMmiorecord) in the production non-qemubuild.kernel/src/nvme_storage_backend.rs(cfg(not(feature = "qemu"))) is the fail-closed activation gate for the always-built NVMeBlockDeviceread arm: modeled ondma_backend, it resolves a production handle only when a brokered controller was discovered and a livedevice_mmiogrant is staged, otherwise theblock_devicegrant 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 theqemu-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 remainqemu-only; the explicitvirtio_9p_host_fixturefeature compiles only the shared split-ring scaffold and 9p driver into anot(qemu)proof build, which includes and re-exports the typed-negativekernel/src/virtio_stub.rsnetwork façade. A build with neither feature mapsmod virtiodirectly to that stub. Itspub(crate) mod transportis the device-generic layer: split-ring/common-config constants, theMmioRegionaccessor, theVirtqueueDescriptorTracker, theVirtqueueDmaDMA/notify seam, the seam-drivenVirtqueue/DmaPagewith their poll/submit/complete loop and the multi-descriptorsubmit_request_chain, and the device-id-parameterizeddiscover_modern_transport. virtio-net is one seam caller (VirtioNetDma); virtio-blk is a second (VirtioBlkDma+VirtioBlkDriver,diagnose_virtio_blk_transport, theblock_device_*request API behind theBlockDevicecap); virtio-9p is a third (Virtio9pDma+Virtio9pDriver,diagnose_virtio_9p_transport), a polled host-directory fixture that completes aTversion/Tattachhandshake through thecapos_lib::ninepcodec and then serves a bounded read subset (Twalk/Tlopen/Tgetattr/Treaddir/Tread/Tclunk) behind theninep_bound/ninep_list_root/ninep_stat/ninep_readfaçade, plus a bounded write subset (Tlcreate/Twrite/Tfsync/Trename/Tunlinkat) behind the separateninep_create/ninep_write/ninep_fsync/ninep_rename/ninep_unlinkfaçade that only the writable cap types call. Each call is one complete walk-op-clunk transaction under the driver lock (proofsmake test-virtio-9p-bringup,make test-virtio-9p-fs, andmake test-virtio-9p-write; the composable co-boot proof ismake test-virtio-9p-net-coboot; provenance mapdocs/devices/virtio-9p.md). Net-specific provider/proof methods stay in the parent module asimpl 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. Undernvme_iommu_translation_proofit also runsdiagnose_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/ACQat programmed IOVAs,CC.EN/CSTS.RDY, one IDENTIFY CONTROLLER per phase, polled completions – used to measure that QEMU’s emulatednvmecontroller 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. Proofmake test-nvme-iommu-translation; provenance mapdocs/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_bufferinstalls manager-owned queue pages,mappingexports active domain IOVAs, andowns_mappingplusunmap_bufferkeep active or quarantined pages out of the allocator until invalidation succeeds.teardownrefuses a live mapping ledger before disabling translation and freeing its tables. Proofmake test-nvme-model-b-provider-iova; provenance mapdocs/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 boundedread_sectors(lba, count, buf)over polled-PIOREAD(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 servesopen_file(name) -> (lba, size)under/boot/bins/, validating every directory record and derived extent against the volume size before use (fail-closedBadVolume/NotFound/NotDirectory).boot_read_proof()reads the PVD (CD001) andboot_fs_proof()walks to/boot/bins/PAYLOAD.BINand verifies its content, both behindboot_iso_readas themake run-boot-iso-readproof. Theboot_sourcesubmodule (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_initandProcessSpawnerCapconsume it so theboot_isokernel loads binaries from the ISO instead of embeddedNamedBlob.data. Proofs:make run-boot-isoand the defaultmake run-smoke. Undercfg(qemu)the always-onAtapiDevice/IsoFssurface (plus a qemu-gatedblock_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.rssets up kernel/user segments and TSS state.kernel/src/arch/x86_64/idt.rshandles exceptions and timer interrupts; CPL3 #PF/#GP/#UD/#DB/#BP faults terminate the whole owning process throughsched::exit_current_thread_terminating_process(deferred whole-process termination when sibling threads are live; proofmake run-user-fault), while CPL0 faults still halt the machine.kernel/src/arch/x86_64/syscall.rsimplements syscall MSR setup and entry.kernel/src/arch/x86_64/context.rsdefines timer context-switch state.kernel/src/arch/x86_64/pic.rsandpit.rsconfigure legacy interrupt hardware.kernel/src/arch/x86_64/ioapic.rsmaps MADT I/O APICs and programs masked legacy IRQ routes from interrupt-source overrides.kernel/src/arch/x86_64/lapic.rsprograms the xAPIC LAPIC timer and IPIs.kernel/src/arch/x86_64/smap.rsenables SMEP/SMAP and brackets user memory access.kernel/src/arch/x86_64/tls.rshandles FS-base/TLS support.kernel/src/arch/x86_64/pci_config.rsprovides 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, andtlb.rsprovide per-CPU data, AP startup, and TLB shootdown for the SMP scheduler.
Kernel Memory
kernel/src/mem/frame.rswraps the shared frame bitmap with Limine memory map initialization and global kernel access.kernel/src/mem/paging.rsmanages page tables, address spaces, permissions, user mappings, W^X enforcement, and address-space teardown.kernel/src/mem/heap.rsinitializes the kernel heap, sizes it against its standing reservations (notably the argon2 login arena), and reports used/free viastats().kernel/src/mem/validate.rsvalidates user buffers before kernel access.
Related docs: DMA Isolation, Trusted Build Inputs.
Kernel Capabilities
kernel/src/cap/mod.rsinitializes kernel capabilities and builds the first service’s kernel-sourced bootstrap capability table.kernel/src/cap/table.rsre-exports shared capability-table logic and owns the kernel-global table.kernel/src/cap/ring.rsvalidates and dispatches ring SQEs. Promise pipelining uses bounded per-drainRingScratchrecords 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.rsvalidates transfer descriptors and prepares transfer transactions.kernel/src/cap/endpoint.rsimplements Endpoint CALL, RECV, RETURN, queued state, cleanup, and cancellation behavior.kernel/src/cap/console.rsimplements serial Console.kernel/src/cap/terminal_session.rsimplements the session-scoped TerminalSession line-oriented terminal with boundedreadLine, echo modes, and cancellation.kernel/src/cap/boot_package.rsimplements the read-only BootPackage manifest-size/chunked-read capability.kernel/src/cap/manual.rsimplements the read-only Manual capability: it parses the boot-packagedManualCorpusblob (carried as themanual-corpusnamed binary) and answerspage/apropos/topics/section/describe/buildInfo.load_manual_corpusinkernel/src/cap/mod.rsresolves the blob’s bytes for themanualgrant source, following the same split as the spawner’s binaries: the residentNamedBlob.datawherever it is real, and an on-demand digest-verified/boot/bins/read underboot_iso, the one layout that leaves that data empty at cap-resolution time.kernel/src/cap/log.rsimplements the Phase 1 monitoring log surface:LogSink(write) andLogReader(read) over a shared bounded, drop-oldest kernel recent-record ring. The sink drops records below the boot-seededSystemConfig.logLevelthreshold and forwards accepted records to serial; the reader returns records at/after a cursor withLogFilter(minLevel/componentPrefix),nextCursor, anddropped(docs/proposals/system-monitoring-proposal.md).kernel/src/cap/block_device.rsimplements theBlockDeviceCapObject(readBlocks/writeBlocks/info/flush). In the non-qemuproduction build theblock_devicesource resolves to the userspace-brokered NVMe arm (BlockDeviceBackend::NvmeBrokered, gated bykernel/src/nvme_storage_backend.rs); theqemubuild routes bounded inline-Datasector I/O to the kernel-owned virtio-blk driver inkernel/src/virtio.rsas a named fixture, not production storage (proofmake run-virtio-blk). The cap is scoped to onedevice_index: theblock_devicesource reaches the resolved non-target boot/storage disk, andblock_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 todevice_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>overVIRTIO_BLK_DMA_POOLS[DEV]);kernel/src/pci.rsenumerates each device with a device index (proofmake 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.rsimplements the read-only filesystem service:ReadOnlyFsDirectoryCap/ReadOnlyFsFileCapparse a fixedCAPOSRO1on-disk layout read through the kernel-owned virtio-blk driver and serveDirectory.list/open+File.read/stat; every mutating method fails closed. Granted via theread_only_fs_rootKernelCapSource(returns a rootDirectorycap; qemu-gated, mounts at grant resolution and fails closed on a malformed/absent image). Host image buildertools/mkstore-image --readonly-fs; proofmake run-storage-fs. An entry name only has to be non-empty UTF-8 without/, so names reach a consumer unsanitized:--readonly-fs-hostilebuilds the same image plus render-attack entries formake 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) andVirtio9pFileCap(validated name + size observed atopen, no server-side fid) implementDirectory.list/open+File.read/stat/closeover thecrate::virtioninep_*façade; every mutating method fails closed and these types call nothing in the driver’s write façade.Virtio9pWritableDirectoryCap/Virtio9pWritableFileCapare the separate writable pair: they delegate the read side to the types above and additionally serveDirectory.create/remove/renameandFile.write/syncoverninep_create/ninep_unlink/ninep_rename/ninep_write/ninep_fsync.mkdir/sub/truncateand anopencarryingCREATE/TRUNCATEfail closed on both pairs (noTmkdir/Tsetattrin 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_nameadmits exactly one ordinary path element on every façade entry point, so the export cannot be traversed out of. Granted via thevirtio_9p_root/virtio_9p_root_writableKernelCapSources, whichmount_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 writableFileresults takeNonTransferableholds rather than the read-only views’Copy/SameSession. Share buildertools/mk-virtio-9p-share.sh; consumersdemos/virtio-9p-fsanddemos/virtio-9p-write; proofsmake test-virtio-9p-fsandmake test-virtio-9p-write(the latter verifies the resulting bytes on the host and proves areadonly=onshare refuses the writable cap at the server), plusmake test-virtio-9p-net-cobootfor the Phase C Nic + writable 9p composition.kernel/src/cap/persistent_store.rsimplements the disk-backed persistentStore:DiskStoreCapserves theStoreinterface (put/get/has/delete) over a fixedCAPOSST1on-disk layout read and written through a read+writeBlockSourceseam.putbump-allocates a data extent, writes the blob and entry record, then rewrites the superblock last as the durability commit point;deletetombstones the entry slot, and a later space-exhaustingputcompacts 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. TheVirtioBlockSource(qemu kernel) routes to the kernel-owned virtio-blk driver byte-identically (folding in thedata_region_base_lba()offset) and mounts eagerly at grant resolution; theNvmeBlockSource(built undercloud_persistent_store_over_nvme_proof) reads/writes through a granted NVMeBlockDevicewindow op and defers its mount-parse to the firstStorecall. Granted via thepersistent_storeKernelCapSource(virtio arm qemu-gated; the third NVMe-proof arm resolves the livedevice_mmiohandle). Host image buildertools/mkstore-image; reboot proofmake run-storage-persist(two QEMU passes on one disk image); NVMe put-then-get proofmake run-cloud-provider-persistent-store-over-nvmeviakernel/src/cap/persistent_store_over_nvme_proof.rs.kernel/src/cap/writable_fs.rsimplements the disk-backed writable filesystem service:WritableDirectoryCapserveslist/open/mkdir/remove/rename/createandWritableFileCapservesread/write/stat/truncate/sync/closeover a fixedCAPOSWF1on-disk layout (a flat node-record array with parent pointers + a bump-allocated data region) written through aBlockSourceseam. 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. TheVirtioBlockSource(qemu/installable kernels) routes to the kernel-owned virtio-blk driver byte-identically (folding thedata_region_base_lba()offset) and mounts the singleton eagerly; theNvmeBlockSource(built undercloud_writable_fs_over_nvme_proof) reads/writes through a granted NVMeBlockDevicewindow op and defers the singleton mount-parse to the firstDirectory/Filecall. Granted via thewritable_fs_rootKernelCapSource(virtio arm qemu-gated; the third NVMe-proof arm resolves the livedevice_mmiohandle), 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-nvmeviakernel/src/cap/writable_fs_over_nvme_proof.rs, which supersedes and drops the persistent-store-over-NVMe proof) exercises bothBlockDevicearms with the single-writer policy intact. The combined image buildertools/mkstore-image --writableco-locates theCAPOSST1Storesub-volume (LBA 0) and theCAPOSWF1filesystem sub-volume on one disk; reboot proofmake 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 bumpednode_countis observed, so a poweroff in the record-written / superblock-pending window leaves an orphan slot the mount ignores. The proof-onlystorage_writable_recoveryfeature arms an induced forced poweroff in exactly that window (recovery_crash_after_record); bounded recovery proofmake run-storage-writable-recovery(pass 1 commits then iskill -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 NVMeBlockDevicearm bymake run-cloud-provider-writable-fs-over-nvme-recoveryviakernel/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); thecloud_writable_fs_over_nvme_recovery_prooffeature widens thestorage_writable_recoverycrash-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@20seed).writable_fs::mount_config_root(qemu-gated) scopes a writableDirectoryto thesystem/configsubtree for the boot-time data-region grant below.kernel/src/cap/installable_image.rsimplements the read-only install-source fixture (Installable System track item 5b):InstallableImageDirectoryCapserveslist/openandInstallableImageFileCapservesread/stat/closeover the booted CD-ROM ISO 9660/boot/bins/tree, reading through thekernel/src/iso/boot_isoATAPI/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’svalidate_extent/read_sectorsrange checks. Granted via the qemu-gatedinstallable_image_sourceKernelCapSource(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 demodemos/installable-image-source/; manifestmanifests/system-installable-image-source.cue; proofmake run-installable-image-source.demos/installable-system-install/implementscapos-system-install, the Installable System install flow (track item 6): under the read-onlyinstallable_image_sourceDirectoryand the target-scopedblock_device_targetBlockDeviceselected 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 fixedcap::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.pysplits the mkdiskimage boot image into the head + backup GPT so only the populated prefix is packaged. Pass-1 installer manifestmanifests/system-installable-install.cue; pass-2 installed manifest (baked into the boot region)manifests/system-installable-install-target.cue; harnesstools/qemu-installable-install-smoke.sh; proofmake run-installable-install(pass 1 installs into a second virtio-blk disk, pass 2 boots it standalone).kernel/src/cap/mod.rsgrant_data_region(proof-onlyinstallable_data_regionfeature) is the Installable System boot-time data-region mount:run_initbest-effort grants init asystem/configDirectory(data-config) plus the persistentStore(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 missingsystem/config. No new cap type or schema change. Proofmake 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
SystemConfigOverlaycapnp object +SystemManifest.extensionPoints(ManifestExtensionPoints) live inschema/capos.capnp; the typed decode, content-hash check, andcompose_ontoprecedence (base-pins-win / overlay-adds-within-declared-extension-points / no-new-authority) live incapos-config/src/manifest.rs.init/src/main.rsapply_config_overlayreadssystem/config/overlay.binfrom the granteddata-configDirectory, composes the overlay over the base plan, and falls closed to the base floor with[init] overlay rejected: <reason>. Thetools/mkmanifestmkoverlaybin encodes overlays (filling the canonical hash) andtools/mkstore-image --writable --seed-overlayseeds them. Proofmake run-installable-overlay. - Installable System generations + rollback + failed-boot auto-fallback (track
item 4): userspace-only over the already-granted Store + writable
system/configDirectory, no schema or kernel change.init/src/main.rsrun_generation_rollback_checks(gated by a base service namedgeneration-proof) represents system-config generations as content-addressedStoreobjects keyed by SHA-256, tracks the known-goodactivepointer and a staged/attemptingcandidatepointer 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-undecodablegen-candidatemarker (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 corruptgen-activemarker takes a distinct loud FATAL refuse-to-boot path (the known-good generation is genuinely unknown). Manifestmanifests/system-installable-generation.cue; proofmake run-installable-generationboots a--seed-configdisk 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_diskfeature, impliesinstallable_data_region): one disk carries the boot ESP (GPT partition 1) and the co-locatedCAPOSST1Store +CAPOSWF1writable data region (GPT partition 2).kernel/src/cap/mod.rsdata_region_base_lbareturns the fixed partition-2 base LBA (264192) under the feature (0 otherwise), applied at the singlepersistent_store/writable_fsread_range/write_rangechoke 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-bytesfold thetools/mkstore-image --writableimage 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). Manifestmanifests/system-installable-disk.cue; proofmake run-installable-diskboots 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.rsimplements FrameAllocator and MemoryObject, plusprove_final_release_tlb_ordering(thememoryobject_final_release_ordering_proofboot-time-smp 2proof that a same-drain final unmap + release returns frames only after the remote TLB acknowledgement;make run-memoryobject-final-release-ordering) andprove_tlb_frame_reuse_ordering(thetlb_frame_reuse_ordering_proofboot-time-smp 2proof that a real anonymous-page unmap +defer_frame_freereturns the frame – and reuses it at the same host physical address – only after the remote acknowledgement, the ordered flush-then-free contractVirtualMemory.decommit/unmapand commit rollback share;make run-tlb-frame-reuse-ordering).kernel/src/cap/virtual_memory.rsimplements per-process anonymous memory operations.kernel/src/cap/timer.rsimplements monotonicnowand boundedsleep.kernel/src/cap/wall_clock.rsimplements the read-onlyWallClock.wallTimecap: UTC over a fixed boot base layered on the monotonic timebase, reporting the fail-closeduntrustedClockProvenance(Phase 1 fixed-boot-base variant;docs/proposals/time-and-clock-proposal.md).kernel/src/cap/park_space.rsimplements the process-local ParkSpace marker capability used by compact park (CAP_OP_PARK/CAP_OP_UNPARK) opcodes.kernel/src/cap/notification.rsimplements the Stage 6 IPCNotificationsignal/wait object: a latched-pending +revokedshared cell plus a global waiter table, delivered by the per-tickpoll_waitersdriver. Upholds no-lost-wake (signalracing ahead ofwaitis latched) and no-wake-after- drop (revoke/last-capDroprelease blocked waiters fail-closed). Minted fresh pernotificationgrant; proofmake run-notification-object.kernel/src/cap/network.rsimplements the qemu-only NetworkManager, TcpListener, TcpSocket, and UdpSocket fixture caps. The kernel no longer depends onsmoltcp; non-qemumanifests reject the kernelnetwork_manager/tcp_listen_authoritygrant sources (fail closed), and the production socket path is the Phase C userspace network-stack process. The socket-backedSocketTerminalSessionshim is retired:TcpSocket.intoTerminalSessionfails closed in every dispatch path.kernel/src/cap/process_spawner.rsimplements ProcessSpawner and ProcessHandle.ProcessHandle.createDebugSessionis the owner-consented debug-attach mint (Debug and Trace Authority, Phase 1): it mints a redacted, read-onlyDebugSessionresult cap scoped to the child, audited to the kernel audit log, failing closed (audited denial) once the target exits.kernel/src/cap/process_control.rsimplements theProcessControlcap (Live Upgrade, Phase 1):retargetCapsre-homes every endpoint-owner slot a process serves onto a successor process, all-or-nothing, for stateless (Case 1) upgrades. Targets are named byProcessHandlecaps 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:CapIdidentity, service scope, and queued calls survive by construction.gracefulfails closed unlessoldis 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 takingold’s table lock);forcedisconnects in-flight callers withCAP_ERR_SERVER_DIED. Every attempt is audited (AuditEventType::Retarget).docs/proposals/live-upgrade-proposal.md;gracefulproofmake run-cap-retarget,forceproofmake run-cap-retarget-force(graceful refuses and force succeeds at one non-quiesced state; the in-flight caller observesCAP_ERR_SERVER_DIED, itsCapIdstays valid, and the retry is served by the successor).kernel/src/cap/debug_session.rsimplements theDebugSessioncap (Debug and Trace Authority, Phase 1):capTableSnapshotreturns a bounded, redacted read-onlyCapTableSnapshotof the target’s cap slots (slot index, interface id, generation, label, state) transferring zero result caps – no invokable handle or badge – anddetach. Every snapshot is audited and gated on a live-target generation check;docs/proposals/debug-trace-authority-proposal.md; proofmake run-debug-session.kernel/src/cap/provider_cap_waiter_proof.rs(non-qemu,cloud_provider_cap_waiter_proofCargo feature) stages a fully-programmed-route bootstrapInterruptgrant source and theInterruptCapWaiterProofcap whoseInterrupt.waitinjects onedevice_interrupt::handle_lapic_deliverydispatch and whoseInterrupt.acknowledgeretires the deferred LAPIC EOI; the cap’son_releaseruns the masked-no-wake + reassign + stale-handle assertion chain before emittingcloudboot-evidence: provider-cap-waiter <token>. Mutually exclusive withcap::interrupt_grant_source_prod(default cloudboot path) and skipscap::provider_nic_bind_proof/cap::storage_bind_proofto 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_proofCargo feature; mutually exclusive withcloud_provider_cap_waiter_proofand the userspace selected-write handshake proof) drives the bounded virtio status sequence kernel-side over the picked virtio-net PCI function (vendor0x1af4, device0x1000/0x1041): resolves the modern virtio PCI transport regions throughvirtio_transport::parse_modern_pci_transport_capabilities, maps the common configuration window throughpci::map_bar_region, and drives reset → ACKNOWLEDGE → DRIVER → feature discovery + driver-feature selection (VIRTIO_F_VERSION_1only) → FEATURES_OK → DRIVER_OK with a trailing reset on every exit path. Inline assertions gate the headlinecloudboot-evidence: virtio-net-device-bringup <token>on the negotiated feature set,COMMON_NUM_QUEUES >= 2, DRIVER_OK observation, and the final reset returningdevice_statusto 0. Marker carriesqueue_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; proofmake run-cloud-prod-nic-driver-userspace-features-ok) is Phase C slice 1 of the userspace NIC relocation track. It makescap::devicemmio_grant_source_prodstage the picked virtio-net modern common-config window as a selected-writeDeviceMmiocap withregisterWrite=selected-write-common-config-handshake; the userspace smoke drives reset -> ACKNOWLEDGE -> DRIVER -> FEATURES_OK overDeviceMmio.write32and 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 thecloud_nvme_readonly_bind_proofdescendant chain because both stage a proof-specific productionDeviceMmiogrant source.kernel/src/cap/virtio_net_tx_authority_bundle_proof.rs,kernel/src/cap/virtio_net_tx_queue_materialization_proof.rs, andkernel/src/cap/virtio_net_msix_function_enable_proof.rsare the decomposed userspace-TX track. Each is non-qemuand gated by its own focused-proof Cargo feature (cloud_virtio_net_tx_authority_bundle_proof,cloud_virtio_net_tx_queue_materialization_proof, andcloud_virtio_net_msix_function_enable_proofrespectively; 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 throughDRIVER_OKand 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 (setFUNCTION_MASK, thenENABLE, 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>, andcloudboot-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, gatedcloud_virtio_net_userspace_rx_bringup_proof) drives the first real RX DMA from the shim-owned vring:post_rx_descriptorwrites the RX descriptor- avail over the shim’s retained RX vring physes at
DMABuffer.submitDescriptortime, anddrive_rx_dma(reached from the now-liveprovider_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 retainedenabledflags to release the ring-buffer pins). Self-contained byte-level vring helpers are duplicated fromvirtio_net_polled_providerto protectrun-net. The notify region is mapped kernel-side + the per-queue notify slot offsets captured bycap::devicemmio_grant_source_prod(rx_dma_notify_state). Proofmake run-cloud-prod-nic-driver-userspace-rx-bringup(extended).
- avail over the shim’s retained RX vring physes at
kernel/src/cap/null.rsimplements the measurement-only NullCap.kernel/src/cap/park_bench.rsimplements the measurement-only ParkBench authority used bymake 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. Itslinker.lddefines the standalone userspace image layout; the nesteddemos/workspace uses its owndemos/linker.ld. -
capos-rt/src/entry.rsowns the runtime entry path and bootstrap validation. -
capos-rt/src/alloc.rsinitializes the userspace heap. -
capos-rt/src/syscall.rsprovides raw syscall wrappers. -
capos-rt/src/capset.rsprovides typed CapSet lookup helpers. -
capos-rt/src/ring.rsimplements 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/PromiseIdvalues over a process-local answer-id allocator, andRingClient::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.rsimplements typed clients for Console, TerminalSession, BootPackage, ProcessSpawner, ProcessHandle, and Timer. The client-side methods are generic overTransport; result-cap-adopting methods stay on the concreteRuntimeRingClient. -
capos-rt/src/transport.rsdefines theTransportseam (the client-sideCALL/completion/RELEASEring operations) and the in-systemRingTransport(RingClientviewed through the seam). A host remote transport is a later slice; seedocs/backlog/capos-sdk-dual-transport.md. -
capos/is the front-door SDK facade crate: for the defaultringfeature it re-exports thecapos-rtruntime, typed clients, theentry_point!macro, and aprelude. Theremotefeature is reserved. Standalone, likecapos-rt. -
capos-python/is the host-only pyo3 (abi3-py39) cdylib that maturin packages as thecaposPyPI distribution (Cargo[lib].name = "capos"). It is the working base for the host-side SDK:capos.Clientbindstools/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.pyis the live hello-world (drives a real gateway and prints the kernel’s response; recorded underdocs/assets/casts/);examples/holds the other runnable scripts;tests/test_capos.pyis a VM-free host pytest of the binding surface. It depends only on host crates (never the bare-metal ones); the transitivecapos-configbuild script runs the pinned capnp compiler, which the release workflow’s wheel job builds in-container. Its.cargo/config.tomloverrides the repo-root bare-metal target to the host glibc target, and.github/workflows/python-release.ymlpublishes it onpython-v*tags via PyPI trusted publishing. -
capos-js/is the host-only pure-TypeScript/ESMcaposnpm distribution: a dependency-free Node (>=20) client over theremote-session-uiloopback bridge’s HTTP API.src/client.tsClientbootstraps 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.tsmirrors the bridge’s camelCase view-model DTOs;index.tsaddshello()/VERSION.examples/hello.mjsis a VM-free runnable script;test/client.test.mjsis a hostnode --testsuite over an in-process mock bridge. Built withtsctodist/; talks only HTTP (no native addon, no capnp build). Not a workspace member. -
capos-rt/src/pollselect.rsis the pure POSIXpoll/selectbridge:SocketReadiness->pollrevents(POLLIN/POLLOUT/POLLHUP/POLLERR/POLLNVAL) andselectset membership, plusunsupported_request_bitsfor fail-closed flag handling. Shared by thelibcapos-posixC surface and theposix-socket-poll-select-smokeproof. Proof:make run-posix-socket-poll-select. -
capos-rt/src/console_text.rsis the pure console-render charset every userspace renderer of producer-supplied text applies before writing through aConsole/TerminalSessioncap. Both functions emit only printable ASCII (0x20..=0x7E) and differ in what they do with the rest.sanitize_console_textis 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’slogbuiltin (shell/src/main.rs), the task-coordinator HTTP adapter (demos/task-coordinator-api-logic, re-exported assanitize_log_text), and the task-coordinator service (demos/task-coordinator-service, applied at itswrite_consoleseam because its own key/worker validation is length-only) – diagnostic fields that are ASCII by protocol.escape_console_textis 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 aDirectorylisting 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 textcatexists 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_boundedis 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’sls/catactually call (shell/src/main.rsescape_for_line), because escaping expands – up to 10x perchar– while the kernel rejects aTerminalSession.writeLineoverMAX_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/catrenderDirectory-supplied entry names and file bytes, and this path has no upstream sanitizer – the kernel cut below coversLogReaderrecords only – so these renderers are both the only cut and the only bound.
The kernel
LogSinkapplies the lossy charset independently atLogEntry::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.rsprovides the emergency Console panic output path. -
capos-rt/src/bin/smoke.rsis the runtime smoke binary used by focused runtime proofs rather than the default boot manifest. -
capos-service/src/lib.rsis the standaloneno_stdservice lifecycle layer abovecapos-rt; slice 1 exposesServiceMain,ServiceRuntime, and ordered initialize/dependency-wait/ready/run/drain/shutdown/cleanup phases.demos/task-coordinator-api-serviceexercises that complete order in QEMU;tools/qemu-task-coordinator-api-smoke.shasserts the marker sequence undermake run-task-coordinator-api. -
shell/src/main.rsis the native capability shell, built as the standalonecapos-shellcrate and packaged bysystem.cue,manifests/system-shell.cue, and the focused login manifests. Operator commands read only through granted caps:date/uptimeover grantedWallClock/Timer,ls/catover a granted read-onlyDirectory(root), andlogover a granted read-onlyLogReader(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/buildslibcapos.a, ano_stdRust staticlib exposing the capos-rt syscall/ring/CapSet path and typedConsole/Timer/WallClock/EntropySource/VirtualMemorywrappers plus C heap shims to C consumers. Public header atlibcapos/include/capos/capos.h. No POSIX surface.libcapos-posix/buildslibcapos_posix.a, ano_stdRust staticlib layering a POSIX adapter overlibcapos: per-process fd table, errno cell, historical UDP socket wrappers over the retired qemu-only kernelUdpSocketcap, clock overTimer,pipe/dupoverPipe,poll/select(poll.rs,<poll.h>/<sys/select.h>) over thecapos-rt::pollselectreadiness bridge with fail-closed unsupported-flag /EBADF/EINVALhandling, andfork/execve/waitpidvia the recording-shim ProcessSpawner Move-grant path.subprocess.rslayerssystem()and Pipe-backedpopen()/pclose()on that shell-spawn path, with focused QEMU proofmake 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-localewchar/wctypemultibyte (wchar.rs), theenvironpointer, and thesys_siglistarray. C headers (the namespaced source of truth) underlibcapos-posix/include/capos/posix/– including the dash-neededsys/types.h,termios.h,sys/resource.h,sys/times.h,wchar.h,wctype.h,locale.h,inttypes.h, and the decl-onlysys/ioctl.h/sys/mman.h/arpa/inet.h/getopt.h/paths.h/sys/param.h.libcapos-posix/sysroot/include/is the-nostdincbare-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’sCAPOS_C_SYSROOT_INCLUDEflags on thecapos-c-multitu-elfrule. Focused sysroot proofmake run-c-libc-surface.capos-wasm/is theno_stdWASI host adapter: awasmi-backedRuntime, thewasm-hostuserspace binary, the Preview 1 import resolver, and the manifest-supplied wasm payload reader.vendor/wasmi-no_std/andvendor/dns-c-wahern/are static-pinned, no-patches upstream snapshots consumed bycapos-wasm/and the POSIX DNS smoke; do not patch them in place (refresh procedure in eachVENDORED_FROM.md).vendor/dash/is the mirror-as-is dash0.5.13.4snapshot (src/stays byte-identical; capOS deviations live underpatches/). Its capOS build pipeline lives outside the mirror undervendor/dash/capos/: the pinnedconfig.handgen-tables.sh(stages a patched source copy + runs the six host table generators). The Makefiledashtarget buildstarget/dash/dash.elfthroughcapos-c-multitu-elfagainstlibcapos.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-wanderercapos-chat,chat-bot,chat-client,chat-servercapset-bootstrap,console-paths,credential-storeendpoint-queue-limit-smoke,endpoint-roundtrip,ipc-server,ipc-client,in-flight-call-limit-smokeframe-allocator-cleanup,memoryobject-shared-child,memoryobject-shared-parentpaperclips,paperclips-contentrevocable-read,revocation-observerring-corruption,ring-reserved-opcodes,ring-nop,ring-fairnessservice-common,shell-spawn-test,shell-typed-calltask-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 ProtoEndpointprotocol with its own schema underdemos/task-coordinator-proto/schema/, the coordinator service, and the acceptance client). Without astatecap the service is in-memory (make run-task-coordinator). With a spawn-granted writable 9pDirectory, 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, andmake test-task-coordinator-9pprove reload over two boots and host-visible state.task-coordinator-logicowns both persistence seams:TaskSnapshot,Coordinator::snapshot/snapshots, boot rebuild throughrestore_task, the fail-closed record codecencode_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 overBlockDevice. Drives the realtask-coordinator-logiccoordinator write-through onto thecapos-libCAPOSRS1WAL record store – each mutation commits the task’s snapshot as one atomic frame keyed bytask:<key>, secondary-indexed bystatus:<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 loopyardtask-source/lock wire shapes, and the thin adapter service over the Phase C userspace network-stack listener – the first in-treecapos-servicelifecycle consumer; host harnesstools/qemu-task-coordinator-api-smoke.sh,make run-task-coordinator-api,make task-coordinator-logic-test). The persistent composition inmanifests/system-task-coordinator-api-9p.cuekeeps the same userspaceNicand adapter topology while granting a writable 9pstatecap only to the coordinator.tools/qemu-task-coordinator-api-9p-smoke.shandmake test-task-coordinator-api-9pprove 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 bymake test-task-backend-vibe-adapter-9p:tools/capos-task-backend-adapter.pymaps the installed vibe-loop task-source and fenced-lock command contracts onto the loopback API, whiletools/test_capos_task_backend_adapter.pyprovides the bounded host contract tests run bymake task-backend-vibe-adapter-test.notification-object(Stage 6 IPCNotificationsignal/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 onecap_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 aDebugSessionover a spawned child viaProcessHandle.createDebugSession, reads a redactedcapTableSnapshotcross-checked againstCapabilityManager.listand 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-strangertimer-smoke,timer-floodtls-smoke,unprivileged-stranger,virtual-memoryuser-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.cueis the default init-owned boot manifest source. It imports the shared defaults package, boot-launches standaloneinit, and lets init start the shell, remote-session CapSet gateway, and resident services.manifests/system-spawn.cueis the ProcessSpawner smoke manifest source.manifests/system-smoke.cueis the scripted focused shell-led login/shell smoke manifest source.manifests/system-chat.cue,manifests/system-adventure.cue, andmanifests/system-paperclips.cueare focused resident-service and terminal-demo manifest sources.manifests/system-memoryobject-shared.cue,manifests/system-revocable-read.cue, andmanifests/system-measure.cueare focused regression/measurement manifest sources.manifests/system-session-context.cue,manifests/system-local-users.cue, andmanifests/system-ipc-zerocopy.cueare the focused session-context, local operator, and zero-copy IPC proof manifests.manifests/system-shell.cueis the focused anonymous-shell manifest source (no verifier, shell stays anonymous).manifests/system-terminal.cueis the focused TerminalSession proof manifest source.manifests/system-credential.cueis the focused CredentialStore proof manifest source.manifests/system-credential-setup-authority.cueis the focused proof that credential creation authority (ConsoleSetup) is strictly narrower than credential status/verify authority (CredentialStore): theConsoleSetupcap installs the first password while aCredentialStoreholder’s retired method-3 dispatch fails closed (make run-credential-setup-authority).manifests/system-login.cueis the focused password-login proof manifest source.manifests/system-login-setup.cueis 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 providescue-to-capnpfor schema-aware CUE-authored data-message conversion. Its siblingmkoverlaybin encodes aSystemConfigOverlayfrom CUE into thesystem/config/overlay.binbytes (filling the canonical content hash) for the installable-system config-overlay proof.tools/manualc/is the System Manual corpus compiler: it parsesschema/capos.capnpfor section-2 interface pages, reads the authored man corpus underdocs/manual/man<section>/*.man, and emits the boot-packagedManualCorpusblob. 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 bymanualc(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.cueis 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.shverifies checked-in generated schema output.loopyard vibe worklogemits per-task commit spans (from each task’scommitslist, falling back to commit history) for the development timeline/Gantt;scripts/validate_backfill_tasks.pyvalidates backfilled task frontmatter against the chunk’s real SHAs;scripts/check-md-links.pyis the pre-commit broken-relative-link gate over all.md.tools/githooks/is the repocore.hooksPath(enabled withmake hooks):prepare-commit-msgstamps provenance trailers (Plan-Item/Run-Id/Agent-Kind) onto run-driven commits, alongside the git-lfs hooks.tools/qemu-net-harness.shruns the current QEMU net harness, withtools/qemu-net-smoke.shasserting 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: aDockerfilecarrying distribution packages only (base image digest-pinned), andcapos-container-build.sh, which bind-mounts the worktree at/buildand 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.shis 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). Seedocs/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, theCAPOSRO1/CAPOSST1/CAPOSWF1storage mount parsers, and thecapos-tlsX.509 validity walk.
Validation: cargo test-mkmanifest, make generated-code-check,
make fuzz-build, make fuzz-smoke.
Documentation
docs/capability-model.mdis the current capability architecture reference.docs/architecture/threading.mdanddocs/architecture/park.mdrecord the accepted contracts and first implementation for in-process thread ownership and private ParkSpace authority.docs/*-design.mdfiles record targeted implemented or accepted designs.docs/proposals/contains accepted, future, exploratory, and rejected designs.docs/research/summarizes prior art (thecapability-systems-survey.mdsynthesis plus per-system deep-dive reports).docs/proposals/mdbook-docs-site-proposal.mddefines the documentation site structure and status vocabulary used by the orientation pages.