CLAUDE.md
Capability-Based Microkernel OS
Status: v3.7 - SMP-Integrated Spec, Reviewed, with Forward-Looking Appendices Scope: v1 milestone (multi-core kernel, two services, cross-core IPC, supervisor restart with core reassignment) Audience: Contributors, reviewers, future maintainers
Table of Contents
- Purpose of This Document
- Project Identity
- Constitution: Non-Negotiable Invariants
- Architecture Overview
- Repository Structure
- Trusted Computing Base
- Capability System
- IPC
- Scheduler and SMP
- Memory Model
- Bootstrap Sequence
- Drivers and Interrupts
- Service Contracts
- Service Lifecycle
- State and Persistence
- Update Model
- Developer Workflow
- Unsafe Policy
- Debugging Model
- Performance Philosophy
- Contribution Rules
- Identity Test Suite
- First Milestone
- Glossary
- Final Principles
- Architectural Discipline
Appendices (forward-looking, mostly non-normative):
- Appendix A: Bootloader Choice (Limine)
- Appendix B: Userspace Posture
- Appendix C: Forward-Looking Vision (Non-Normative)
- Appendix D: Shell, Scripting, and Utility Ecosystem (Non-Normative, Far Future)
1. Purpose of This Document
This document is the constitution of the project. It defines the enforceable laws and concrete decisions of the OS.
It is not aspirational. It is a commitment to specific trade-offs.
It exists to:
- Ensure the system remains small, correct, and enforceable.
- Prevent contributors from introducing hidden complexity.
- Make every architectural decision traceable to a stated rationale.
- Resolve future arguments by appeal to written law rather than memory.
When this document and the code disagree, the document wins and the code is wrong. When this document and reality disagree, the document is amended and the change is recorded.
How to read this document. Each section's present-tense body is the current, canonical law - read it as settled fact. The inline Amendment YYYY-MM-DD blocks record how a rule reached its present form and why; they are ratified history, not open proposals or drafts. Where an amendment and the body it sits under read differently, the most recent amendment is the canonical state and the body is being brought up to match. You never need the git history to know the current law: it is the section body, as amended. Sections whose state changed the most over time (notably §6, the TCB) open with a short "current canonical state" box so the settled answer is available before the history that produced it.
The appendices at the end of this document collect forward-looking design notes. Appendix A documents a v1 commitment (the bootloader choice). Appendices B, C, and D are explicitly non-normative - they record design intent and discussion, not commitments. Their content does not amend the constitution.
This constitution has a human-readable distillation: COMMANDMENTS.md, the Ten Commandments of Godspeed. Each commandment is grounded in the invariants and sections it enforces here. Where a commandment and this document disagree, this document is the law and the commandment is amended to match (it is the distillation, not the source).
2. Project Identity
2.1 What This Project Is
A deliberately small, fully-understood capability microkernel, built to internalize the design discipline of capability-based systems by writing one.
2.2 What This Project Is Not
- A novel research system.
- A POSIX-compatible OS.
- A production-grade kernel.
- A general-purpose application platform.
- A competitor to seL4, Fuchsia, Hubris, Redox, or Genode.
2.3 Goals, Ranked
- Clarity over novelty. Every part of the system should be explainable in a paragraph.
- Correctness over cleverness. A boring, verifiable design beats a clever, fragile one.
- Execution over theory. Shipping a working ping/pong beats refining a perfect spec.
2.4 v1 Architectural Principles
- Isolation over performance.
- Explicit transitions over implicit mutation.
- Identity over location.
- Simplicity over cleverness.
- Loud failures over silent fallbacks.
2.5 v1 Permanent Decisions
| Capability | Status | Rationale |
|---|---|---|
| SMP | Supported (static) | Cross-core parallelism; no migration |
| Zero-copy IPC | Rejected, permanent | Violates "no shared mutable memory" |
| Live code updates | Rejected, permanent | Restart-with-reacquisition is sufficient |
Amendment 2026-10-17 (live handover): a running service may be REPLACED without stopping, by a second program - code is still never changed inside a running one. The operator asked for Erlang's upgrade-in-place. What this row rejects stays rejected: no new code is ever loaded into a running address space, so W^X holds and the bytes that run are always the bytes the supervisor checked from the disk (14.1). What is now allowed is the observable half of Erlang's feature, made out of mechanisms the system already has: the new version is a separate, isolated program, started BESIDE the running one under the same name; the running one hands it its state over IPC and ends itself (
gs::handover,docs/developer-services-design.md14). What Erlang calls code change is the successor reading the old version's state - written by the package, explicitly.What the kernel learns: one spawn flag,
SPAWN_FLAG_HANDOVER.SpawnImage(which only the supervisor can call, 14.1) may start a task beside the ONE task already running under its name; the name directory re-points to the new endpoint, and the old task's death leaves the name alone (the endpoint-id guard that already handles a respawn racing a death). No new syscall, no shared memory, no capability passed between the two except the successor's endpoint, which the supervisor sends with the offer. A name never has more than two instances. Not a seventh responsibility: it is spawning (4.3), with one refusal relaxed for one caller.What is opt-in, and what is not promised. A package declares
handover = true; without it, an upgrade stops the old version and starts the new as before. Capabilities do not travel (the successor holds its own spawn request's), a request sent to the old version after it drained its queue is lost with it - its caller'sgs::callreportsOutcomeUnknown, exactly as for a death - and the state is one message. Services only; an app's handover (its screen moving with its state) is not built.
2.6 Reference Systems
| System | What we borrow |
|---|---|
| seL4 | Capability model, synchronous IPC discipline |
| Hubris | Declarative task contracts, supervisor-driven restart |
| Fuchsia | Userspace drivers, capability handles in IPC messages |
| Genode | Composition through capability delegation |
| Redox | Rust microkernel patterns |
3. Constitution: Non-Negotiable Invariants
These are the laws that bound every design choice. Any change that violates an invariant must first amend the invariant - and amendments require a written rationale.
- No ambient authority. Every privileged action requires an explicit capability.
Amendment 2026-06-12 (H1): DMA-capable devices were an unstated exception to this invariant - a driver could direct its controller's DMA engine at any physical address, kernel-equivalent reach the capability model never granted. H1 (IOMMU confinement) closes the gap: a confined device reaches only its granted arena. See §6.4.
- No shared mutable memory by default. Services have isolated address spaces.
- All authority is explicit. Capabilities, not identity.
- Kernel remains tiny. Memory, scheduling, IPC, capabilities, interrupts, cross-core routing. Nothing else.
- Unsafe is isolated and audited. Permitted only in
arch/,memory/,capability/,smp/. - Services must be restartable (with stated TCB exceptions).
- Contracts are enforced, not interpreted.
- State must be explicit and owned. No anonymous singletons.
- No unowned global mutable state. Immutable globals are fine.
- System must remain understandable. 30-minute whiteboard rule.
- Identity is stable; location is not. Services have stable names; their core assignment may change across restarts.
- Failures are loud, never silent. No silent fallbacks at the kernel boundary.
4. Architecture Overview
4.1 Layered View
┌──────────────────────────────────────────────────┐
│ Application Services (replaceable) │
├──────────────────────────────────────────────────┤
│ System Services │
│ events · block-driver · fs │
├──────────────────────────────────────────────────┤
│ Trusted Root (trusted, restartable) │
│ supervisor (init removed; registry retired) │
├──────────────────────────────────────────────────┤
│ Kernel (mechanism, not policy) │
│ memory · scheduler · ipc · capability │
│ syscall · interrupts · smp/routing │
├──────────────────────────────────────────────────┤
│ Architecture Layer (unsafe boundary) │
│ arch/<isa> - one directory per ISA, and the │
│ ONLY place that knows which machine this is │
├──────────────────────────────────────────────────┤
│ Hardware (multi-core) │
└──────────────────────────────────────────────────┘
Amendment 2026-09-12 (multi-architecture): this document described a single-ISA system, and had stopped being true some months ago. It named
arch/x86_64in the layered view above, in the repository map (§5) and in the TCB table (§6.1), and mentioned RISC-V nowhere at all. There are now four complete ports, all verified on real hardware - x86-64 (HP T630, Dell Wyse), ARMv7 (Raspberry Pi 2), AArch64 (Raspberry Pi 4) and RISC-V 64 (StarFive VisionFive 2 Lite) - plus three stubs that boot and print (riscv32,loongarch64,s390x). The gap predates the RISC-V work; the constitution was not amended for the ARM ports either.What this amendment does NOT change is the point of it. No invariant moves, no kernel responsibility is added, and the TCB does not grow:
arch/<isa>was always the unsafe boundary (invariant 5, §18.1), and only the directory built for the machine in front of you is compiled into it. What changed is that the noun is now plural.The property that makes this affordable is worth stating as law, because it is what is actually being defended. A port is bounded to
arch/<isa>/: you write that directory and nothing else in the kernel changes. Architecture-neutral code reaches hardware only through thearch::impseam and must never name an ISA - enforced mechanically byscripts/arch_boundary_check.py(neutral layers reach hardware only through the seam) andscripts/arch_seam_check.py(every arch answers every member of it, discovered from usage rather than a hand-kept list). The RISC-V port was the first completed with no neutral kernel CODE naming the ISA - two comments inmemory/allocator.rsandtask/scheduler.rscite it as explanation, which is the honest extent of the claim and the standard the others are being brought to. For comparison, neutral code still namesarmin 8 places,aarch64in 4 andx86_64in 3.The rule the operator set for that work, recorded here because it is the bar: an ISA port is not complete when it boots. It is complete when architecture-neutral code no longer knows that the ISA was added. Where neutral code still enumerates ISAs by name - the supervisor's
#[cfg(any(...))]spawn arms, the SDK'shwclasslist - that is acknowledged debt, not the model.
Amendment 2026-09-13 (portability-hardening): the debt named above is MEASURED now, not counted by hand, and both of its examples are out of date. The amendment above states the bar correctly and then points at two things as the standing debt. One is gone and the other was never an example of it:
- The supervisor's
#[cfg(any(...))]spawn arms are gone. That file carried 49 arch-conditional sites when this branch began; it carries 4. (47 when the spawn-table work itself started - two had already gone in the commit that named the board facts. The 49 is the figuremilestones/uses, so this says the same thing they do.) The USB host table was FIVE tables, one per arch plus an empty catch-all, and is now one table whose rows are present exactly where their image is; the seven-times-repeatedany(x86_64, aarch64, riscv64)was one question - is configuration space reachable - and is now onebuild.rsfact. Three service crates went the same way, and where the ISA still answers, it is asked ONCE per fact in a build script rather than at every site that needs it.- The SDK's
hwclasslist is not an ISA enumeration and never was. It names DEVICE kinds -NIC,XHCI,EHCI,DWC2,FRAMEBUFFER- plus PCI class-code addressing. That is step D's answer to this problem, not an instance of it: a driver names a device class and the kernel resolves it, which is exactly what stops a new board needing a new name here.And the count itself was the wrong instrument. "Neutral code still names
armin 8 places,aarch64in 4 andx86_64in 3" was true when written and had drifted to 6, 4 and 2 before anybody re-measured, because a hand count is right on the day it is taken and silently wrong afterwards. Worse, nothing was watching:arch_boundary_check.pyforbids inline assembly and named arch modules outsidearch/, and a#[cfg(target_arch = "arm")]inkernel/src/task/mod.rsis neither, so the debt this paragraph names could grow without failing anything. Userspace had a ratchet (shared_surface_check.py); the neutral kernel had none.It does now - the same one, which is the honest shape since it is one property asked of two layers. The standing figure is 54 arch-conditional sites outside
arch/: 2 in the neutral kernel, 52 above it (46 and 44 when this was written; the rise is board facts inservices/supervisor/build.rsandservices/wifi-driver/build.rs- the Pi 4's radio (+1), the audio drivers (+4) and, on 2026-10-04, the VisionFive's radio and nic-driver's radio bridge as its own fact (+4) - blessed together that day; and on 2026-10-05 one fewer, when the VisionFive gained the bridge too and the bridge fact became the radio fact by derivation rather than a second test of the instruction set (-1);docs/porting.mdhas the per-file tree). It may fall freely and may not rise without a recorded reason. What is left is listed rather than implied. The neutral kernel is down to 2, and both aretarget_pointer_widthon one constant - a 32-bit address space genuinely cannot hold a 4 GiB virtual address, so the width IS the question rather than an ISA standing in for one. Above the kernel,nic-driverpicks its MAC by ISA on three of four boards and needs a kernel query to stop (backlog/21),hw-enumeratorpacks a host-bridge config selector that belongs inarch/(backlog/25), and the rest are the SDK's syscall seam, which §18.1 designates and which is the one place the ISA is genuinely the question.
4.2 SMP View (Per-Core)
Kernel (shared, concurrent)
┌────────────────────────────────────────────────┐
│ Routing Table: EndpointId → CoreId │
│ Capability Table │
└─────────────┬──────────────┬───────────────┬───┘
IPI │ IPI │ IPI │
┌─────────────▼──┐ ┌────────▼───┐ ┌────────▼───┐
│ Core 0 │ │ Core 1 │ │ Core 2 │
│ Run Queue │ │ Run Queue │ │ Run Queue │
│ Services │ │ Services │ │ Services │
└────────────────┘ └────────────┘ └────────────┘
▲ syscall ▲ syscall ▲ syscall
4.3 Kernel Scope (Strict) - MISCIS
The six, and the mnemonic for them - MISCIS, said like "misses": Memory isolation, IPC, Scheduling, Capabilities, Interrupts, SMP routing.
- Memory isolation (per-service address spaces, page tables)
- IPC (synchronous message passing, bounded queues, cross-core routing)
- Scheduling (per-core run queues, round-robin with timer preemption)
- Capability enforcement (validation on every privileged syscall, generation check)
- Interrupt routing (delivery to userspace driver services)
- SMP routing (EndpointId → CoreId map, IPI wakeup)
Leave these six bullets as plain text.
scripts/commandments.pyparses each line up to the(as the responsibility's NAME, so bolding the mnemonic letters inside them -**M**emory isolation- turned every name into something it did not recognise and failed six modules at once. Caught in seconds by the gate that reads this list, which is the argument for deriving it from here rather than copying it into config.
"Do not expand MISCIS" is therefore the short form of §4.4: a seventh responsibility is a change to
what this kernel IS, not a feature. scripts/commandments.py (I-responsibilities) derives the six
from this very list and fails on a module that serves something outside it, so the acronym and the
gate read the same source.
The list is ordered to spell the word. It previously ran memory / scheduling / IPC / ... which spells MSICIS, and the order carries no meaning - the checker builds a SET from these bullets and does not care. A mnemonic that does not match the list it names is a small trap, so the list moved rather than the mnemonic.
4.4 Kernel Anti-Scope
The kernel does not contain filesystem logic, network stack, drivers (beyond minimal arch boot), logging infrastructure, application logic, developer tooling, work-stealing scheduler, service migration, or load balancing.
Amendment 2026-06-18 (P2, file-as-capability): delegated resource capabilities do not add file logic to the kernel. The kernel gains the ability to mint, route, and revoke capabilities for resources whose meaning is defined by a service (§7.10). It still contains no filesystem logic: it tracks an opaque
ResourceIdand its owning endpoint and nothing more; the owning service (fs) alone mapsResourceId → file. "A file is a capability" thus becomes literally true while this anti-scope holds - the kernel never learns what a file is.
5. Repository Structure
os/
CLAUDE.md
README.md
Cargo.toml
kernel/
src/
main.rs
arch/ # ONE DIRECTORY PER ISA; `arch::imp` aliases the one being built
x86_64/ # complete - boot.rs, interrupts.rs, context_switch.rs, page_tables.rs, ap_boot.rs
arm/ # complete - ARMv7-A, Raspberry Pi 2 (hardware-verified)
aarch64/ # complete - Raspberry Pi 4 (hardware-verified)
riscv64/ # complete - QEMU virt + StarFive VisionFive 2 Lite (hardware-verified)
riscv32/ loongarch64/ s390x/ # stubs: boot + UART only
memory/ # frame.rs, page.rs, allocator.rs, bitmap.rs
task/ # mod.rs, state.rs, scheduler.rs (per-core)
ipc/ # message.rs, endpoint.rs, queue.rs, routing.rs, names.rs
capability/ # cap.rs, table.rs, rights.rs, generation.rs, delegated.rs
smp/ # core.rs, ipi.rs, percpu.rs, spinlock.rs, names.rs
syscall/dispatch.rs
interrupt/route.rs
invariants/assertions.rs
log.rs # kernel ring buffer
bootcon/ # boot + panic framebuffer blit (11.4) - NOT a terminal; see console/
services/
supervisor/ # restart authority + name authority (TCB); spawned directly by the kernel
# (init removed, Phase 5; registry service retired, Phase 4 - Path C §3.7)
events/
console/ # the terminal: ANSI/CSI, grid, cursor, scroll (docs/console-service.md 9)
block-driver/ # restartable (Phase D)
fs/ # restartable (Phase D); depends on block-driver
sdk/rust/ # service_context.rs, capability.rs, ipc.rs
osdev/
src/main.rs
src/validator.rs # JSON Schema validation
examples/
ping/
pong/
contracts/
schema/service.schema.json
docs/ # narrative design notes; `docs/CLAUDE.md` is the index
observability.md # the events sink: logs, traces, metrics, persistence
service-ownership.md # who owns a service: images, authority, discovery
naming-design.md # name resolution out of the kernel (Path C)
persistence.md # block driver + filesystem, file-as-capability
console-service.md # the terminal, and the kernel's boot/panic floor
... # the index lists them all
audits/ # append-only EVIDENCE, not documentation
unsafe-audit.md # every unsafe block; CI checks it matches source
kernel-audit.md security-audit.md userspace-audit.md documentation-audit.md
2026-07-15-full-trilogy-report.md # a dated run of all of them at once
tests/
qemu/
identity/ # identity test suite (§22)
harness/ # shared test infrastructure
perf/ # performance benchmarks (§22 B1-B10) - 10/10 ✅
scripts/ # THE ENFORCEMENT LAYER, and the non-x86 build paths
commandments.py # the Ten Commandments, mechanised where they can be
commandments_redteam.py # probes that BREAK each check, so a dead check is caught
contract_check.py # every contract matches its kernel service_config
unsafe_check.py # the unsafe audit matches the source
doc_refs.py # no doc points at a file that does not exist
facts_check.py # a number a doc restates matches the code that owns it
site_check.py # the 5 hand-written site pages still match the repository
arch_boundary_check.py # neutral layers reach hardware ONLY through the `arch::imp` seam
arch_seam_check.py # ...and every arch ANSWERS every member of it (the other direction)
scaffold_check.py # ...and the BOUNDED-PORT TEST: how far a fresh ISA gets with only
# `arch/<isa>/` written. The two above prove no RULE is broken; this one
# exercises the claim, because a count is a proxy and a build is not
shared_surface_check.py # ratchets arch-conditional code ABOVE the kernel (the other axis:
# `target_arch` there is usually "which BOARD am I on")
one_way_check.py # ONE way to write a service or a driver: `gs`. Ratchets, per crate, the raw
# SDK calls the standard library already covers - may fall, may not rise, and
# a NEW crate starts at zero. Counts only methods with a `gs` replacement, which
# it names; a gap in `gs` is closed in `gs` (backlog/71, 2026-10-05)
quit_wait_check.py # NO SILENT WAIT in the shell, which observes every command: each wait reads
# the command's watch or says on the line above why it cannot trap anyone
# (`// quit-ok:`), and those exceptions may fall, not rise (backlog/fixed/89)
port_scope_check.py # ...and the one the other four cannot answer: did the port EDIT anything
# outside `arch/<isa>/` and the twelve files `docs/porting.md` marks `+`.
# They all ask whether a RULE was broken; an ordinary edit to a neutral
# kernel file breaks none of them, so five ran green over exactly that
dash_check.py # no em/en dashes anywhere (§21)
foreign_word_check.py # no DOC shows a POSIX/DOS word being used as a command. `ls`
# became `dir` and the rename reached the shell, the specs and
# the help text - and missed TEN worked examples. Derived from
# the shell's own `FOREIGN_HINTS`, never a hand-kept list
line_ref_check.py # a `path.rs:NNN` citation still points at what it claims. A line
# number rots on the next edit above it, and fifteen checkers
# looked at none: Audit 7 found 7 of 11 wrong, four documents
# citing ONE dead line. `audits/` is exempt - dated evidence
doc_command_check.py # a documented INVOCATION must work. `doc_symbols_check` asks
# whether a NAME resolves and `facts_check` whether a NUMBER
# matches; nothing asked whether a documented prompt runs. `dir long /` does
# not - `long` was removed, so the shell lists a directory NAMED
# `long` and discards the path, which is a WRONG ANSWER rather
# than an error. Reads `SUBCMD_FIRST` and osdev's own `match
# suite`, so it cannot drift from either
comment_symbol_check.py # ...and the same question asked of CODE COMMENTS, which are
# 27,126 lines across 238 files - twice the documentation, inside
# the kernel, and read FIRST because they sit beside the code.
# Resolution is STRICTER than for a doc: `doc_symbols_check`
# accepts a name found anywhere in the source, comments included,
# which here would be circular - the comment would satisfy
# itself. A name cited by a comment must exist in CODE. Most of
# its baseline is permanent and correct: registers, SBI calls and
# Linux functions a driver cites on purpose (§26.14)
# WHERE THESE RUN, which until 2026-09-26 was the hole under all the others. The eight
# DOCUMENTATION checkers above (doc_refs, docs_index_check, facts_check,
# foreign_word_check, line_ref_check, site_check, backlog_check, doc_command_check) were
# on NO developer build path: they ran only in `build.yml`, which is
# `workflow_dispatch`-only and paused, and in `release.yml`, which fires on a `v*` tag.
# Documentation was therefore checked AT RELEASE - too late by construction, and v0.20.0
# is the worked example (its tag run failed late and the release shipped with no
# artefacts). They are in `osdev`'s `EXTRA_CHECKS` now, so a build runs them. ~11.5 s for
# all eight, measured. The rule this list already states about `line_ending_check.py`
# applies to itself: a checker on one build path is a checker on none.
service_embed_check.py # every managed service is really embedded in the image
embed_order_check.py # the supervisor is newer than the services it embeds
stack_fit_check.py # a service's frames fit the stack it is given (§26.6.1)
test_report.py # collate a suite run into a report
board.py # ONE way to build a bootable image for any port:
# `py scripts/board.py pi2|pi4|visionfive|x86 [--crash-window]`.
# Owns the POLICY the four ports used to state differently - a
# board image is ALWAYS release, every port takes the same flags,
# every build ends by naming the artifact and what to copy where
# (including the per-port RENAMES). The per-port scripts below do
# the work and stay callable
arm_build.py pi4_build.py riscv_build.py arm_run.py pi4_run.py riscv_run.py
utilities/ # the SPEC for every shell utility, one file each, plus 0_conventions
0_conventions.md # the 14 rules every utility obeys
website/ # the published book (mdBook); pages `{{#include}}` the
# sources above, so a doc and its page cannot drift
backlog/ # open items - recorded rather than closed (§26.7)
boot/ # per-board boot config (pi2/, pi4/)
contracts/schema/ # the JSON Schema a service contract is validated against
examples/ # 15 worked services
milestones/ # what was achieved and when; ALMANAC.md is the chronicle
bugs/ # long-form investigations of four specific hardware bugs
editors/ # syntax files for the gsh shell language
6. Trusted Computing Base
Current canonical state (as amended below). The non-restartable set is
{kernel}alone - the kernel is the only component that cannot be restarted; everything else recovers from death rather than forcing a reboot. Present-tense status of every former TCB member:
- supervisor - trusted but restartable: the kernel respawns it on death (unconditionally, forever) and it reconciles with the still-running services (§6.2).
- init - removed entirely; the kernel spawns the supervisor directly (Path C / Phase 5).
- registry - left the TCB, then the service was retired; naming is now a minimal kernel directory (naming Phase 4 / Path C).
- block-driver, fs - restartable storage services, made safe by
fs's crash-consistent recovery (Phase D); their death is a supervisor restart, not a reboot.- DMA drivers (
xhci/ehcion x86,dwc2on ARM) - all userspace services; in the TCB only on a machine with no IOMMU, where unconfined DMA is kernel-equivalent reach. Where an IOMMU confines them they are least-privilege and drop out (§6.4).The dated amendments in §6.1-§6.3 record how this floor was reached and why. They are ratified history, not proposals; this box is the settled result they add up to.
6.1 TCB Members
| Component | Trusted because |
|---|---|
| Kernel | Enforces all isolation |
arch/<isa> | Direct hardware access. The trust is per-ISA: the directory built for this machine is in the TCB, the others are not compiled |
kernel/smp | Concurrent-correctness primitives |
supervisor | Holds restart + name authority; spawned directly by the kernel (init removed, Phase 5); trusted but restartable - the kernel respawns it on death (Phase 6, §6.2), so the only non-restartable thing is the kernel itself |
xhci, ehci, dwc2 (DMA drivers) | Machine-dependent (H1, §6.4): in the TCB only on a machine with no IOMMU to confine them (DMA-anywhere = kernel-equivalent reach); dropped from it - least-privilege and restartable - wherever an IOMMU confines them to their arena. The case is reported loudly at boot (invariant 12). |
Amendment 2026-06-12 (H1): DMA-capable drivers are no longer an unconditional TCB member. Before H1 they were an implicit, unstated member: with no IOMMU a driver directs its controller's DMA engine at any physical address - kernel-equivalent power the capability model never granted (see the invariant 1 amendment). H1 makes their trust machine-dependent: confined by an IOMMU, a compromise is bounded to the granted arena, so the driver is genuinely least-privilege and restartable and leaves the TCB; on a machine with no IOMMU it stays trust-critical by necessity. The same binary, different posture, with the difference printed at boot. §6.4 is the full treatment; §22 Test 12 pins the confined case.
Amendment 2026-06-17 (Phase D / FS robustness):
block-driverandfsare no longer TCB members. They were a v1 simplification (§6.3):fsowned persistent state it could not recover after a crash, so its death - and that of theblock-driverit depends on - was a panic+reboot. The filesystem robustness program closes that gap:fsnow commits every metadata mutation through a crash-consistent redo-journal and recovers to a consistent state on mount (Phase C;docs/persistence.md§6.8). With recovery in hand, both services are restartable like any other: the kernel notifies the supervisor of their death, which respawns them;fsre-mounts (recovering via the journal) and re-registers,block-driverre-initialises the controller, and clients reacquire via the registry and retry (§14.3, §6.2).block-driverholds no persistent state and was already operationally restartable. Their boot-time spawn must still succeed to bootstrap persistence (§11.3); only their runtime death is now recovered, not fatal. Worked example of invariant 11 and the §6.3 goal reached. §22 Test 13 pins it (fssurvives its own restart). The remaining non-restartable set is now justinit+supervisor+ kernel.
Amendment 2026-07-25 (ARM/USB): the Phase D recovery guarantee is BACKEND-CONDITIONAL, and the backend reports which case it is in. Phase D (above) dropped
block-driverandfsfrom the TCB on the strength of crash-consistent recovery. Bringing up USB mass storage on the ARM32 port showed that guarantee is not a property offsalone: a redo journal is pure ordering - staged blocks durable before the commit record that authorises replaying them, that record durable before any home block moves - and ordering can only be enforced by a device that attests durability. Two cases, and the difference is a printed fact rather than a hidden assumption (exactly the §6.4 posture):
- A backend that attests durability keeps the guarantee intact.
ahciissuesFLUSH CACHE EXTwhenfsasks for it, at the journal barriers (amended 2026-08-22: it used to flush after every 512-byte sector, which cost a transaction a stack of full device flushes and made a single file write take tens of seconds on a SATA SSD; the barriersfsalready declares - staged blocks before the commit record, commit record before any home block - are what the guarantee rests on, and a per-sector flush added nothing to them). The consequence is stated plainly: unflushed FILE DATA can be lost on a power cut, while METADATA stays crash-consistent, which is exactly what this section claims and no more. after every write; SD/EMMC completes a write only after the card releases its busy line. Ordering holds,fsrecovers to a consistent state on mount, and the Phase D TCB claim stands unchanged.- A backend that cannot does not. The Pi 2's USB stick refuses
SYNCHRONIZE CACHEoutright, and FUA - which the drive does honour - costs more time per write than the driver's command budget can give it (USE_FUA, then in the in-kernelarch/arm/dwc2.rs; that file was DELETED by the 2026-08-17 amendment below and the driver isservices/dwc2now - the DEVICE's refusal is what this paragraph turns on, and it is unchanged by where the driver lives). With no barrier available, a power cut can lose the tail of a write sequence, andfssays so once per mount rather than implying a guarantee it cannot deliver. Metadata is still CRC-verified, so the failure is DETECTED loudly on read; what is lost is automatic recovery, not the ability to notice.So the honest form of the Phase D claim is:
fsis restartable everywhere; it is crash-recoverable on a backend that can be ordered. Where it cannot be,fsremains restartable (its death is still a supervisor restart, never a reboot - §6.2 is untouched) and a power loss may require a reformat. Recorded rather than closed, per §26.7: the fix is a block path that can wait out a busy device without holding the core, which is real work and not a constant.
Amendment 2026-09-23 (hardware): the amendment above is RIGHT about the rule and WRONG about its only example. The Pi 2 is not a backend that cannot be ordered - it was never tested, and when it finally was, it recovered. The 2026-07-25 amendment names the Raspberry Pi 2's USB stick as the worked case of a device that "refuses
SYNCHRONIZE CACHEoutright", and concludes that on that board a power loss may require a reformat. Both halves are contradicted by the machine.The refusal. Seven sessions across three USB stacks -
dwc2on the Pi 2,xhcion the Pi 4,xhcion the VisionFive 2, one physical stick - andfshas printed no durability warning on any of them. That warning fires at both journal barriers whenever the flush comes back false, so on every run where writes committed it ran and stayed silent: the device answeredSYNCHRONIZE CACHE(10)and accepted it. The only local evidence for the refusal was an instrument that could not tell a refusing device from a dead driver - it fired twice inbuild/pi2a.logimmediately afterblock-driver died, restarting, blaming the stick for a flush nobody was there to answer. That is fixed (Durable/Refused/NoAnswer), and three of the seven sessions ran with the corrected instrument.The consequence. On 2026-09-23 a power cut 17 s into
churn 30, on a PLAIN image with no crash-window, at a moment nobody chose, landed inside the commit-to-checkpoint window:fs: journal recovered 4 block(s) from an interrupted write churn verify: 7 file(s) checked, 0 empty, NONE torn check: 13 files, 2 dirs, 0 bad; the free count already agreed with the tree - nothing was repairedA replay of 4 blocks means the commit record was durable BEFORE any home block moved. That ordering is the whole of the guarantee, and this device enforced it. It took three attempts, which is ordinary variance.
Corrected the same day, in this amendment rather than around it: the paragraph above first read "at the ~2% per-cut odds the window's sub-millisecond life implies". That figure was wrong. It took
fs's own "normally lasts under a millisecond" comment - written about the Dell Wyse, an AHCI SSD - and applied it to a USB stick. The window IS the checkpoint, the interval between the commit record becoming durable and the last home block landing, and those writes are slow on a stick, so there it is a large fraction of each transaction rather than a sliver of it. Measured across every unassisted cut: six hits in twelve (T630 two of two, Pi 2 third of three, Pi 4 first, VisionFive first, Wyse one of five). At 2% that outcome is about 1 in 10^8, so the estimate is refuted rather than imprecise. All five boards have been cut on the same current build. Nothing else in this amendment depends on it - the evidence for the Pi 2 is the replay itself, not how many tries it took - but the number was acted on, so it is corrected where it was stated rather than left for a reader to trip over.What does NOT change, and is the reason this is an amendment rather than a retraction. The guarantee stays backend-conditional. That reasoning is sound and untouched: a redo journal is pure ordering, ordering can only be enforced by a device that attests durability, and a device that refuses or LIES about a flush cannot carry the guarantee.
fs-lyingflushmodels exactly that case in QEMU and it stays. The honest form of the Phase D claim -fsis restartable everywhere, and crash-recoverable on a backend that can be ordered - is correct as written.What changes is that the claim is about a CLASS of device, not about this board. The Pi 2 was the one named instance and it does not belong in it; the sentence naming it stands above as ratified history, and this amendment is the canonical state (§1). No board in this project is currently known to refuse the barrier. If one is found, it belongs here with the evidence that put it here - which is the standard the Pi 2 was held to only after the fact, and the point of recording this at all.
The FUA half is untouched and still true: the stick does honour FUA, and FUA costs more per write than the driver's command budget can give it. That was never the load-bearing claim - the flush is - but it is not contradicted by anything here.
Five boards, four ISAs, three storage backends, power cut 5 of 5 recovered in the strong form, and ALL FIVE cut UNASSISTED - Wyse, T630, Pi 2, Pi 4 and VisionFive 2, each landing in the commit window with no held-open pause helping the device. The Pi 4 and VisionFive also had
crash-windowcuts a day earlier; those are superseded, so no result this amendment rests on depends on a window held open for the device's convenience.docs/gsfs-carnage.md§4 carries the matrix;backlog/fixed/42carries the investigation, including the two earlier Pi 2 cuts that missed the window and what they did and did not measure.
Amendment 2026-06-09 (H11):
registryis no longer a TCB member. It became a real userspace name service (register/lookup over IPC, holding only delegated caps and deriving copies). It owns no kernel-critical state, so its runtime death degrades name resolution temporarily rather than corrupting the system, and it is now restartable (see §6.2, §6.3). Its boot-time spawn must still succeed (the name service must come up to bootstrap), which remains fatal (§11.3). Worked example of invariant 11 - identity (the name) is stable; the registry instance/location is not.
Amendment 2026-06-21 (naming Phase 4 / Path C): the
registrySERVICE is RETIRED. Moving name→endpoint resolution to the supervisor (Phases 0a-3c,docs/naming-design.md) left the registry's only remaining job - handing a client a cap to a service by name - to a minimalname → endpointrecovery directory inside the kernel (ipc::names+ the gatedAcquireSendCap). The supervisor wires every service from aname → capmap at boot and on restart; clients reacquire names through the directory. So the registry service is deleted outright (crate, config, spawn, §22 Test 11/1B moved off it). This is the bounded "one exception" of Path C (§3.7): a thin naming directory stays in the kernel - justified by §6.3 (the recovery anchor must be unkillable) - even though name policy lives in the supervisor. the registry's own design note was DELETED with the service (9a880b12, pre-public cleanup), so this amendment anddocs/naming-design.mdare the whole record. This line used to point at the file itself, which sent a reader after a document that no longer exists.
6.2 Failure Semantics
The only unkillable component is the kernel itself. Every userspace service - including the
supervisor- is restartable; its death is recovered, never a reboot.
Amendment 2026-06-21 (Path C / Phase 6): the
supervisoris restartable; its death is no longer a kernel panic. When the supervisor dies (a fault, or a deliberate kill -chaos kill-storm supervisor, the operator control channel), the kernel respawns it - the kernel is the last-resort recovery anchor, the one thing that cannot die (§3.7). The respawned supervisor re-registers its death-notification endpoint in the kernel directory (so notifications re-point to it) and reconciles: it adopts the still-running services (reacquiring each by name) rather than duplicating them, and respawns any that died. The non-restartable set is now{kernel}alone - §6.3's goal reached at its floor. (initremoved, Phase 5;registryretired, Phase 4;block-driver+fsrestartable, Phase D.) Pinned by §22 Test 15.The respawn is unbounded - deliberately. The kernel respawns the supervisor unconditionally, forever; there is no cap-then-panic. A bound would re-introduce the very reboot this eliminates (deferred from 1 death to N) and hand an attacker a trivial denial-of-service (kill the supervisor N times to force a reboot). This is not unbounded-resource behaviour (§26.6): each respawn first reclaims the dead instance's frames/kstack/caps, then allocates fresh, so the footprint is constant and reclaimed every time - only a count grows, and a count is not a resource. Each respawn is loud (logged with a running count, §26.4/§26.7), so a sustained loop is visible and an operator can intervene, but the system stays alive rather than rebooting. "Assume the worst" → always recover.
block-driver,fs, andshellare restartable. Their runtime death is recovered by the supervisor's death-notification restart loop (the kernel notifies the supervisor, which respawns them); clients see a temporaryEndpointDead/ lookup miss, reacquire by name via the kernel directory, and retry (§14.3).fsre-mounts to a consistent state via its crash-consistency journal (Phase C;docs/persistence.md§6.8). Theshellis the user's interface - a crash or a deliberatekill shellrespawns a fresh prompt (the in-flight command is lost - a re-init, not a resume, §14.2/§25 - but the session recovers) instead of leaving a dead session; closing the one service that used to stay dead-forever if killed ("nothing escapes"; invariant 6).registryleft the TCB via H11 (then the service was retired, Phase 4);block-driver+fsvia the Phase D amendment (§6.1). Only their boot-time spawn failure is fatal (§11.3).
Amendment 2026-10-11 (
ask): the death notice says HOW the task ended, because the kernel already decides it and was throwing it away. A task ends in exactly two ways: thekillsyscall, or a CPU fault in user mode (a service that panics ends as the second - its panic handler reads address 0). The kernel takes that path every time, and then told the supervisor only the name, so "why didfsrestart?" could be answered nowhere in the system: a deliberatekilland a crash looked the same.The notice now carries it: the name, a NUL, then
Kand the name of the task that calledkill, orF, a fault kind (memory, instruction fetch, illegal instruction, protection, alignment, or one the port does not classify) and the address the port has for it (task::death, the SDK'sdeath). Each port's user-fault path names the kind; x86's shared exception stub does not know its vector and says so rather than guessing. The supervisor keeps the newest per name and answerssupcmd::DEATH; its "died, restarting" line now ends- killed by shellor- memory fault at 0x0.What this does NOT add, which is why it is an amendment and not a seventh responsibility. No syscall, no capability, no new authority and no record held by the kernel: the cause rides the notice the kernel already sends, to the one task that already receives it, for exactly the tasks it already reports. The kernel learns nothing about any service; it reports a fact about its own kill path. The record - bounded, newest per name, volatile across a supervisor restart - is the supervisor's, which already recorded THAT the service died. Mechanism, not policy (26.10): whether a kill was justified is the killer's to say, and nothing here tries to.
Verified in QEMU on all four ports (a kill named on each; a fault on AArch64 through
net-stack'sel0-fault-test);osdev test identity24/0 andadv15/0.docs/ask-design.md6 recorded this as the missing contract.
Failure on any core that corrupts shared kernel state (capability table, routing table) results in kernel panic on all cores.
Silent recovery of TCB state risks undefined system state. Loud failure plus clean restart is the only safe v1 option.
6.3 Reducing TCB Over Time - goal reached, at the floor
The v2 goal was: only init, supervisor, and the kernel remain non-restartable. That goal is now
met and exceeded - the non-restartable set is {kernel} alone. registry was dropped early via
H11 (a restartable userspace name service, then retired entirely in naming Phase 4 / Path C);
block-driver and fs were dropped via the Phase D amendment (§6.1, 2026-06-17) once the
filesystem gained crash-consistent recovery (the redo-journal, docs/persistence.md §6.8) - so an
fs restart re-mounts to a consistent state rather than corrupting it. init was removed outright
(Path C / Phase 5): the kernel spawns the supervisor directly. And finally the supervisor itself
was made restartable (Path C / Phase 6, §6.2): the kernel respawns it on death - unconditionally,
forever - and it recovers from the kernel's name directory (adopting the live services). So the
kernel is the only unkillable thing (docs/naming-design.md §3.7) - DMA drivers aside, and only
on a machine without an IOMMU (§6.4). The floor is reached; there is nothing left to shrink.
6.4 DMA-Capable Drivers and the IOMMU (H1)
Amendment 2026-06-12 (H1). Adopts IOMMU DMA-confinement as the mechanism that brings DMA-capable userspace drivers into the least-privilege model (invariant 1).
DMA-capable userspace drivers (xhci, ehci) are not trusted root. Their trust
status is machine-dependent, and which case holds is reported loudly at boot
(invariant 12):
- Without an IOMMU, a DMA-capable driver holds implicit kernel-equivalent power:
it programs its controller's DMA engine with physical addresses and can therefore
read or write anywhere in RAM, regardless of the capabilities it holds. Its
compromise is unbounded, so it is trust-critical by necessity. (Boot reports
iommu: no IVRS table ... drivers stay in TCB.) - With an IOMMU confining it (H1), the device can reach only the driver's granted
DMA arena; a DMA outside it faults rather than corrupting memory. A compromise is
then bounded to the arena the capability model already granted, so the driver is
genuinely least-privilege and restartable - exactly as ordinary services are.
(Boot reports
iommu: ... confined BDF ...; out-of-arena DMA is pinned by §22 Test 12.)
This machine-dependent posture is deliberate: the same driver binary is least-privilege
on a machine whose IOMMU confines it and trust-critical on one without, and the
difference is a printed boot fact rather than a hidden assumption. Confinement is applied
per driver and only where it fits the driver's DMA shape - xhci is confined to its
arena; ehci (which legitimately reaches firmware/hub regions and a low-speed device only
through a hub's transaction translator) runs in transparent IOMMU passthrough. See
docs/iommu.md.
Operationally these drivers were already restartable (their death reclaims their IOMMU resources and the supervisor respawns them); this amendment makes the trust claim official, not the runtime behaviour.
Amendment 2026-09-12 (multi-architecture / DMA census): this section names its members as a LIST, and the list was short. The rule is restated by PROPERTY. §6.1's table and this section's opening sentence enumerate
xhci,ehcianddwc2as the DMA-capable drivers whose trust is machine-dependent. That enumeration is not the rule - the rule is the argument two paragraphs above, which turns only on a device being able to DMA: any service granted a DMA arena is trust-critical on a machine that cannot confine it. Two services meet that test and were never listed:block-driver(the AHCI command list / FIS / PRDT / data buffers) andnic-driver(the TX/RX descriptor rings and packet buffers on e1000, RTL8168, GENET and dwmac alike). Their absence understated the TCB rather than changing it - both were always in it by this section's own reasoning.What confinement actually covers today, stated as fact rather than intent:
xhciis the only confined driver in the system.ehciandblock-driverkeep a stale firmware DMA pointer that confinement would fault, so both run in deliberate passthrough (kernel/src/task/mod.rs, theconfineflag onHwClass::Pci- this cited aDeviceSpectype that has never existed, and it was introduced to replace a rotting line number on the grounds that a field name cannot drift);nic-driveris spawnedconfine=false.- AMD-Vi is x86-only. Every
iommu::entry point onarm,aarch64andriscv64is a stub andconfine_devicereturnsfalse. Three of the four shipping ports are therefore entirely in the "without an IOMMU" case, with no confined driver at all.So the honest reading of this section is: the machine-dependent posture is real and the mechanism works, but it currently bounds exactly one device on one architecture. Everything else that can DMA is trust-critical. This is recorded rather than closed (§26.7) because the remaining cases are blocked on hardware (no SMMU is wired up on any non-x86 board) and on a firmware quirk (the stale pointer), not on effort.
docs/networking.mdanddocs/ahci.mdeach carried the opposite claim for their own driver and are corrected in the same change.
Amendment 2026-10-03 (audio): there are TWO confined drivers now, and the kernel releases a confinement by the device, not by name. The amendment above says
xhciis the only confined driver in the system.audio-driver(Intel High Definition Audio,docs/audio.md) is spawned confined as well: every DMA its controller makes - the command rings, the buffer descriptor list, the ring of sound - is inside its arena, so confinement refuses nothing it does legitimately. Verified in QEMU on q35 withamd-iommu: the confinement selftest passes, the tone plays through the confined domain, and a kill and restart releases and re-confines the device (build/audio_iommu_qemu.log). Its controller uses plain MSI, so the interrupt message is in configuration space, out of the driver's reach.The kernel change it needed adds no responsibility. On a driver's death the kernel reverted the device's confinement only for
xhciandehci, named; a third confined driver would have leaked its I/O page table on every restart. It now releases for ANY task that holds a device, which is exact because the release does nothing for a device that was never confined. The bus-master clear beside it moved from a list of four names to the same per-task device record in the same change. Both are memory isolation the kernel already enforced (§4.3), now keyed on what a task holds.What does not change: AMD-Vi is still x86-only,
ehci,block-driverandnic-driverare still in passthrough, and on the T630 the audio driver does not yet use DMA at all (docs/audio.md, A6), so on real hardwarexhciis still the one confined device. The mechanism now bounds two devices, on one architecture, one of them in QEMU only.(Note 2026-10-08: the T630 confines the audio controller too - its log shows
xhciand 00:01.1 each confined with an arena - so on real hardware there were two confined devices, and they shared one IOMMU domain ID. AMD-Vi caches translations by domain ID, so that sharing was a defect; each confined device now has its own (kernel/src/arch/x86_64/iommu.rs,domain_of). Found under anxhcithat stopped completing commands in a chaos run,docs/wifi-usb.md51.)
Amendment 2026-07-16 (SEC-2): a confined USB driver's least-privilege claim is bounded by the console it drives. A USB keyboard driver is, by function, the machine's input path: it delivers keystrokes to the shell via
CONSOLE_PUSH, and keystrokes are commands. The kernel cannot distinguish a faithfully-decoded key-press from a synthesized one, so no code check can let a real keyboard type a privileged command while stopping a compromised driver from injecting the same bytes (both reach the shell through the same input ring).CONSOLE_PUSHholders are therefore inside the shell's trust perimeter - IOMMU confinement bounds the driver's DMA, not its console-injection authority. What the code can do is deny the driver any authority it does not need for that role: SEC-2 removedREBOOTfrom the USB drivers, so a compromised driver can no longer hard-reset the machine directly from any context - reboot lives only with the shell (itsrebootcommand). The residual (a keyboard can type) is inherent to being a keyboard, and is recorded here rather than papered over.audits/security-audit.mdSEC-2.Amendment 2026-07-19 (SEC-2 follow-up): Ctrl+Alt+Del is restored, routed through the shell. The chord initially became ordinary keystrokes, which removed a familiar affordance. It now works again without giving the driver back anything: the USB driver only signals the chord on the console stream (
hid::CTRL_ALT_DEL_SIGNAL, a byte outside ASCII that no typed key produces) and the shell - the principal that legitimately holdsREBOOT- makes the decision. What SEC-2 actually won is intact: a driver still cannot issue the reboot syscall, in any context, even when no shell is listening. And it grants the driver no new authority, because aCONSOLE_PUSHholder could already typereboot- the residual named just above. Scope: the chord is handled at the shell prompt; while a full-screen app owns the console the shell is not reading, so quit it first.
Amendment 2026-08-09 (Pi 4 / AArch64): the USB stack is OUT of the kernel, and the in-kernel driver is DELETED. The amendment below records that on ARM the USB drivers are in-kernel TCB members "by construction", and calls the userspace split "future work awaiting device-IRQ-to-userspace routing". On AArch64 (Raspberry Pi 4) that work is done:
kernel/src/arch/aarch64/xhci.rs(2742 lines of ring-0 code parsing descriptors supplied by whatever was plugged in) no longer exists. ThexhciSERVICE drives the controller through an MMIO capability and a DMA arena granted at spawn, reaches the console throughCONSOLE_PUSH, and serves storage over the block IPC protocol thatblock-driveralready spoke. The kernel's entire remaining involvement with USB is to establish that the controller is present and reachable and to say so.This was a feature flag first (
xhci-userspace/usb-via-xhci) so both drivers could exist while the service was proven on hardware. The flags are now deleted too: a flag that selects between a compliant and a non-compliant kernel leaves the violation one build away, and it was a genuine footgun (it had to reach three crates; setting some of them gave two drivers on one controller, or none, with every half booting fine alone). There is no build of AArch64 GodspeedOS in which the kernel drives USB. Commandment I is closed on this port, not merely satisfiable.What this does NOT buy: the driver is still a TCB member on this board (SEC-33). The Pi 4 has no IOMMU/SMMU wired up - every
iommu::entry point on aarch64 is a stub andconfine_devicereturnsfalse- and the service is granted its controller's BAR plus a DMA arena including its physical base. So it can point the controller's DMA at any address, which is kernel-equivalent reach by §6.4's own rule, exactly as an unconfined x86 driver would be. The honest statement is therefore: a buggy USB driver on the Pi 4 is now bounded; a compromised one is still kernel-equivalent.That distinction is worth being precise about, because the milestone is real but narrower than "Commandment I closed" sounds. What the move genuinely bought is (a) the ACCIDENT surface - ring-0 descriptor parsing became a restartable service, which is the whole content of SEC-29, now closed on aarch64 - and (b) ambient authority: SEC-2's no-REBOOT win travels here (unlike arm32, where an in-kernel driver implicitly holds every kernel authority), and the service holds only CONSOLE_PUSH, its log, its endpoint, its BAR and its arena. The kernel-scope violation is closed; the TRUST posture is unchanged until an SMMU confines the device. Also unmet on this port: §6.4 requires the confinement case to be "reported loudly at boot", and nothing is printed either way (SEC-34).
ARM32 (Pi 2) has since followed - see the 2026-08-17 amendment below. When this was written its DWC2 stack was still in the kernel and still a TCB member; that is no longer true, and the sentence that said the two ports "differ in exactly this" is superseded. Verified: chaos max-carnage 100 rounds, selfcheck 349, hot-plug of keyboard and mass storage in both directions, all on the userspace driver.
Amendment 2026-08-17 (ARM32 / Pi 2): the DWC2 stack is OUT of the kernel too, and
arch/arm/dwc2.rsis DELETED. The amendment below (SEC-29/SEC-30) records the in-kernel ARM USB stack as a machine-dependent posture that could not be fixed on this hardware, because ARM did not route device IRQs to userspace. It does now:services/dwc2registers forUSB_VECTOR(arch/arm/irq.rs) and is driven by the interrupt rather than the core-0 timer tick. So the two consequences that amendment draws no longer hold as stated: the memory-safety ofarch/arm/dwc2.rsis not TCB-critical because that file does not exist, and SEC-2's win DOES now travel to ARM - the ARM USB driver is a service holding only the capabilities its contract grants, so it cannot callhardware_resetand does not sit inside the kernel trust perimeter.What does NOT change, and is the same caveat the Pi 4 carries: the Pi 2 has no IOMMU/SMMU, so the driver's DMA is unconfined and a COMPROMISED driver is still kernel-equivalent by §6.4's own rule. A buggy one is now bounded and restartable; a malicious one is not. The ACCIDENT surface is what closed here, exactly as on aarch64. The residual that is inherent everywhere also stands: a keyboard's keystrokes are commands (SEC-2).
The same is now true of the DISPLAY on this port:
kernel/src/fbcon(1,172 lines of terminal emulation) left the kernel forservices/console, leaving only the §11.4 boot/panic blit (docs/console-service.md§9). Verified on hardware: chaos 50 rounds, 0 kernel panics, 0 liveness wedges, selfcheck 350/0.
[SUPERSEDED IN PART by the 2026-08-17 amendment above - read that first.] The in-kernel ARM USB stack this describes NO LONGER EXISTS:
arch/arm/dwc2.rsis deleted andservices/dwc2drives the controller from userspace onUSB_VECTOR. Kept because §1 makes an amendment ratified history - this records why ARM USB was ever a TCB member, which is what the later amendment is a reply to. What still holds is the DMA half: the Pi 2 has no IOMMU/SMMU (iommu::confine_devicereturnsfalseon this arch), so a COMPROMISED driver remains kernel-equivalent by §6.4's rule. A buggy one is now bounded and restartable. This block is placed out of date order, after the amendment that supersedes it, so it is marked rather than left to be read as current.]Amendment 2026-07-23 (SEC-29/SEC-30): on the ARM32 (Raspberry Pi 2) port the USB drivers are in-kernel TCB members - a machine/arch-dependent posture, the ARM analog of the no-IOMMU case above, and larger. The amendments above concern userspace USB drivers (
xhci/ehci) confined - or not - by an IOMMU. The ARM port has no such split yet: the DWC2 USB host driver (keyboard, CDC-ECM/smsc95xxnetworking, mass-storage) runs in the kernel (arch/arm/dwc2.rs, driven from boot + the core-0 timer tick), because ARM does not yet route device IRQs to userspace (arch/arm/CLAUDE.md, "Drivers on ARM"). So on ARM the USB stack is ring-0 code that parses untrusted device-supplied descriptors and frames, and it is a TCB member by construction. This is strictly more than the no-IOMMU x86 case: there the driver is untrusted-but-userspace with only its DMA unconfined; here the driver is the kernel. It is not fixable on this hardware - the Pi 2 has no IOMMU/SMMU to confine USB DMA regardless, and the userspace-driver split awaits device-IRQ-to-userspace routing - so, per §26.7, it is recorded rather than closed. Two consequences follow: (a) the memory-safety ofarch/arm/dwc2.rsis TCB-critical (audited:audits/unsafe-audit.md,audits/security-audit.mdAudit 2, no UB/OOB/race); (b) SEC-2's win does not travel to ARM - "REBOOT lives only with the shell, not the USB driver" is an x86 property; an in-kernel ARM driver implicitly holds all kernel authority (it could callhardware_resetdirectly), so the ARM keyboard driver sits inside the kernel trust perimeter, not merely the shell's. The residual that IS shared with x86 is inherent: a keyboard's keystrokes are commands (SEC-2).audits/security-audit.mdAudit 2 (SEC-29/30) is the full treatment.
7. Capability System
7.1 Concept
A capability is an unforgeable token granting specific rights to a specific resource at a specific generation. Holding a cap is necessary and sufficient authority for the actions it permits - provided its generation still matches the kernel's record.
7.2 Capability Structure
Capability = ResourceId + Rights + Generation
- ResourceId - identifies the target resource (endpoint, memory region, MMIO range).
- Rights - bitfield of permitted actions (READ, WRITE, SEND, RECV, GRANT, REVOKE).
- Generation - monotonic counter assigned by the kernel when the resource is created or replaced.
7.3 Properties
- Unforgeable. Only the kernel constructs valid capabilities.
- Explicit. Authority comes from holding a cap, not from identity.
- Non-escalating. Rights cannot be widened.
- Scoped. Targets a specific resource, not a class.
- Revocable. Kernel can invalidate at any time.
- Transferable (with
GRANTright). - Generationed. Stale caps fail their generation check on use.
7.4 Rights Model
| Right | Meaning |
|---|---|
READ | Read from a resource |
WRITE | Write to a resource |
SEND | Send messages to an IPC endpoint |
RECV | Receive messages from an IPC endpoint |
GRANT | Transfer this capability via IPC |
REVOKE | Revoke this capability (held by supervisor only) |
7.5 Generations
Every capability carries a generation number. Every resource in the kernel tracks its current generation.
Bumping rules:
- Restartable / destroyable resources bump their generation when they are destroyed or replaced. This invalidates all outstanding caps targeting them.
- Stable resources (kernel-owned, never reclaimed) keep generation 0 forever.
Validation on use:
syscall(cap, action, args):
if cap.resource_id not in kernel_table:
return CapNotHeld
if cap.generation != kernel_table[cap.resource_id].generation:
return CapRevoked or EndpointDead # depending on cause
if action not in cap.rights:
return CapInsufficientRights
perform action
syscall(cap, action, args)
│
├─ cap.resource_id in kernel table?
│ No ──▶ CapNotHeld
│ Yes ↓
├─ cap.generation == table generation?
│ No (destroyed) ──▶ EndpointDead
│ No (revoked) ──▶ CapRevoked
│ Yes ↓
└─ action in cap.rights?
No ──▶ CapInsufficientRights
Yes ──▶ perform action ──▶ Ok
The generation check is one atomic comparison. It is the v1 mechanism for cross-core revocation: bumping the generation on one core makes every cap on every other core stale, with no synchronous notification required.
7.6 Lifecycle
[kernel mints cap with current generation]
│
Created
│ inserted into cap table
Held ◀────── action complete ──────┐
│ syscall + rights + gen check │
Used ────────────────────────────▶─┘
│
├── send with GRANT ──▶ Transferred ──▶ Held (receiver's table)
│
└── kernel bumps resource gen ──▶ Stale
│
next use: CapRevoked / EndpointDead
7.7 Error Codes
Both error codes are kept; they share a mechanism but communicate different intent:
| Error | Meaning |
|---|---|
CapNotHeld | Cap not in calling task's table |
CapInsufficientRights | Cap held but lacks required right |
CapNotGrantable | Send embedded a cap without GRANT |
CapWrongScope | Cap targets a different resource than the action |
CapRevoked | Authority explicitly invalidated |
EndpointDead | Endpoint/service lifecycle terminated |
ReplyDead | Replier died while the caller was blocked awaiting its reply (the reply-side twin of EndpointDead; §8.6) |
Same generation-mismatch mechanism underlies CapRevoked and EndpointDead; the kernel returns the more specific code based on whether the resource was destroyed (endpoint dead) or had its cap explicitly revoked. ReplyDead shares that mechanism on the reply side: a caller blocked in a synchronous Call (§8.2) wakes with ReplyDead the instant its replier's endpoint dies (§8.6).
7.8 Capability Table Concurrency
Multiple cores may execute syscalls touching the same capability table simultaneously. v1 uses a locking discipline that guarantees:
- Reads (cap lookup, generation check) and writes take the SAME exclusive lock; nothing here is wait-free or reader-parallel.
- Writes (cap insertion on spawn, removal on death) are serialized.
- A revocation in flight on one core is visible to a syscall in flight on another core within bounded time (next memory barrier).
The exact primitive is an implementation choice, not a spec choice.
v1 implementation note: A single global lock is acceptable for the v1 milestone. Syscall-path serialization is a known performance cost; sharded or RCU-based designs are explicit v2 work and require benchmarks before adoption.
Amendment 2026-09-12: it is a
SpinLock, not anRwLock, and this section claimed a property the code never had.GLOBAL_RESOURCESis aSpinLock<GlobalResourceTable>(kernel/src/capability/table.rs); there is noRwLocktype anywhere in the kernel. So "reads are wait-free under common cases" was never true: a cap lookup takes the same exclusive lock a spawn does and can spin behind it. The bullet above is corrected. This does not weaken any guarantee - §7.8's actual requirements (reads correct, writes serialized, revocation visible within bounded time) all hold under plain mutual exclusion, and it is strictly more conservative than theRwLockthis described. What changes is the performance claim, which B7 measures.
7.9 Example
fn main(ctx: ServiceContext) -> Result<()> { let log = ctx.capability("log_write")?; let pong_send = ctx.capability("ipc_send.pong")?; log.info("ping starting")?; pong_send.send(Message::text("hello"))?; Ok(()) }
7.10 Delegated Resource Capabilities (P2 - file-as-capability)
Amendment 2026-06-18 (P2). Extends the capability model so a resource's meaning can be owned by a service while the kernel still mints, validates, routes, and revokes its caps. This is the mechanism that makes "a file is a capability" literally true (
docs/persistence.md§7.2).
The kernel mints unforgeable caps (§7.3) but has no concept of a file (§4.4). Delegated resource
capabilities bridge the two: a service owns a band of ResourceIds whose meaning only it knows,
and the kernel treats each as an opaque resource - identical machinery to an endpoint cap.
- Mint. A service asks the kernel (
resource_mint) to allocate a freshResourceIdin its band, register it (generation 0, Alive), record the service's endpoint as its owner, and mint a cap with chosenRights(READ/WRITE/GRANT). The service hands a (narrowed) copy to a client by the existing embedded-cap transfer (§8.5).fsdoes this onOpen, recordingResourceId → file. - Use = send. A holder uses the cap by
sending on it. The kernel validates it (generation + required right) and routes the message to the owning service's endpoint, badged with theResourceId- so the owner knows which resource without the kernel knowing what it means. A read/write to a file is then a first-class capability operation: validated, denied, or revoked by the same code path as any cap. - Revoke = generation bump (§7.5). The owner revokes a resource it owns (
resource_revoke); every outstanding cap to it goes stale and the next use returnsCapRevoked.fsrevokes on delete/close. - Minting is gated (§3.1).
resource_mintrequires aRESOURCE_MINTcapability, granted only to services that legitimately issue resources (e.g.fs). Delegated minting is explicit authority, never ambient.
Every §7.3 property holds for a delegated resource cap exactly as for an endpoint cap: unforgeable,
non-escalating (rights narrow on transfer), scoped (to one ResourceId), revocable, generationed.
The kernel learns nothing about files; it routes opaque resources. Pinned by §22 Test 14.
8. IPC
8.1 Model
Synchronous message passing with bounded per-endpoint queues. Endpoints are owned by services; services are pinned to cores; sending across cores goes through the kernel routing table.
8.2 Syscalls
#![allow(unused)] fn main() { send(endpoint_cap, message) -> Result<(), IpcError> // blocks if full recv(endpoint_cap) -> Result<Message, IpcError> // blocks until msg try_send(endpoint_cap, message) -> Result<(), IpcError> // non-blocking call(target_cap, reply_cap, recv_cap, message) -> Result<Message, IpcError> // send request + block for reply call_deadline(target_cap, reply_cap, recv_cap, message, secs) -> Result<Option<Message>, IpcError> // `call`, bounded }
call is the synchronous request/reply primitive (syscall 41). It sends the request to target
carrying a one-shot reply cap (the caller's own endpoint), then blocks awaiting the reply. It
wakes with the reply, or - if the replier dies before replying - with ReplyDead (§8.6), so it never
hangs. This is mechanism, not policy (§26.10): the kernel learns only about a reply cap and its
death semantics, never "request/reply" or "RPC". It is the primitive behind the SDK's
request_with_reply; the reply-side twin of the blocked-sender EndpointDead wake.
Amendment 2026-08-21 (
CallDeadline, syscall 50):callgains a BOUND, because the unbounded one was being worked around in a way that lost messages.callis the only primitive that dequeues the REPLY specifically (matched to the reply cap), leaving every other message queued - but it blocks forever, so the SDK hand-rolled a bounded variant out ofsend+ a plain endpointrecv. A plain recv takes whatever is next, and a service that SERVES clients on the endpoint it awaits replies on would therefore consume an unrelated client request, fail to match it, and drop it: the request lost outright, and the real reply arriving later as an orphan that desynced every following exchange. Observed on both the Pi 2 and the Pi 4 asfsclients hanging and the block protocol "losing step".The fix is not a workaround at the caller. It is the correct primitive made usable: same reply-cap semantics, same
call_dequeue, plus the deadline machineryRecvTimeoutalready uses. This is mechanism, not policy (§26.10) - the kernel learns a deadline, not what the caller is waiting for
- and it is what §26.6 asks of every wait in the first place.
Ok(None)means the deadline passed; the reply cap is the caller's to reclaim, exactly as on any other failure (§8.5).A new syscall is a new kernel responsibility and the surface is pinned (Commandment I), so this is recorded here rather than merely added: it is
callwith a bound, not a new capability, and the enforcement layer refused the change until this amendment existed.
8.3 Routing
The kernel maintains a routing table:
EndpointId → (CoreId, Generation, Liveness)
On every send, the kernel:
- Validates the cap (rights + generation).
- Looks up the target endpoint in the routing table.
- Enqueues into the target endpoint's queue (which lives on the target's core).
- If the receiver is blocked on
recv, sends an IPI to its core to wake it.
8.4 Send Flow
Service A (Core 0) Kernel Service B (Core 1)
│ │ │
│── send(endpoint_cap, ───▶│ │
│ message) │ validate cap │
│ │ (rights + generation) │
│◀── CapNotHeld ───────────│ cap not in table │
│◀── CapRevoked ───────────│ gen mismatch (revoked) │
│◀── EndpointDead ─────────│ gen mismatch (dead) │
│ │ │
│ [queue full] │ │
│ A blocked ─────────────│────────────────────────────│
│ in routing table │ (waiting for queue space) │
│ │ │
│ [queue has space] │ │
│ │── copy msg into B's queue ─│
│◀── Ok ───────────────────│ │
│ │── IPI Core 1 ─────────────▶│
│ │ wake B if blocked │
8.5 Message and Queue Format
- Maximum message size: 4 KiB (one page).
- Queue depth: 16 messages per endpoint, fixed in v1. Worst-case 64 KiB per endpoint queue.
- Copy semantics: kernel copies sender → receiver. Zero-copy is permanently rejected (§2.5).
- Embedded capabilities: caps inside a message are transferred (with
GRANT) and removed from sender's table.
Queue depth is not configurable per endpoint in v1. Per-endpoint depth is a v2 concern.
Transferring a capability - the three checks. Embedding a cap in a message moves authority. The kernel enforces the rules below but cannot warn you at compile time, so an author (and a reviewer) must verify all three every time a cap is sent:
- Grantable? The cap being sent must hold the
GRANTright, or the transfer is rejected withCapNotGrantable(§7.7). A copy made byderive_capcarries only the rights of its source, so a send-only cap yields a send-only copy that cannot be transferred. Do not assume a transfer succeeded; a send that embeds an un-grantable cap fails, and the receiver gets nothing (§7.4, §7.6).- Moved, not kept. A successful transfer removes the cap from the sender's table (§7.6): authority moves, it does not duplicate. Reusing that handle afterward is a use of a cap you no longer hold. And if the transfer failed, the cap stayed - reclaim it (so a table slot does not leak, §26.6). Either way, the outcome of the send decides what you may do next: never ignore it.
- Narrowed to need. Grant the least rights the receiver needs (§7.3). In particular, do not pass
GRANTonward unless the receiver is meant to re-delegate - a cap handed out withGRANTlets its holder transfer it again. Rights only narrow on transfer; widening is impossible, so the floor you set is the floor forever.
8.6 Failure Semantics
| Event | Effect |
|---|---|
| Service dies | Endpoint generation bumped; queue drained |
send to closed endpoint | Returns EndpointDead |
recv on closed endpoint | Returns EndpointDead |
| Sender already blocked when endpoint closes | Wakes with EndpointDead (cross-core IPI) |
| Send-during-restart race | Generation check catches it; returns EndpointDead |
| Replier dies while the caller is blocked awaiting its reply | Caller wakes with ReplyDead (cross-core IPI) |
Amendment 2026-06-30 (reply-side death-wake): a caller blocked awaiting a reply wakes with
ReplyDead, completing the sender side of this table. The rows above already wake a blocked sender when its target endpoint closes (EndpointDead); the reply side was the missing twin. A synchronous request/reply caller (the SDKrequest_with_reply, on whichfs'sblock_rpcrides) sends a request carrying a one-shot reply cap and then blocks awaiting the reply on its own endpoint. If the replier died after receiving the request but before replying, that blockedrecvhung forever - a reply that will never come. The kernel now tracks, for a caller blocked in a synchronous CALL, the endpoint it awaits; the endpoint-death path finds any such caller (its outstanding reply cap's holder has died) and wakes it with the newReplyDeadcode, mirroring the blocked-sender wake exactly (same generation/liveness mechanism, same cross-core IPI). This is mechanism, not policy (§26.10): the kernel learns only about a reply cap and its death semantics - never "request/reply" or "RPC". It is bounded (a blocked task has at most one in-flight call, so one tracking slot per task). It is the executable form of Commandment VIII for interdependent services: a dependent waits on its dependency's reply (truth), and a dependency that dies wakes it loudly rather than hanging it. Pinned byosdev test reply-dead(the reply-side twin of §22 Test 4).
No delivery guarantee. A successful
sendmeans the message was queued, not processed. Protocols requiring acknowledgment must build it explicitly.
8.7 Send-During-Restart Race
Without explicit handling, this race is real:
- Core 0: A reads cap to B (generation 4, alive).
- Core 1: B is killed, generation bumped to 5.
- Core 0: A's send syscall executes.
Resolution: the kernel checks A's cap generation against the routing table's current generation atomically inside the send syscall. The generation has been bumped to 5; A's cap is generation 4; send returns EndpointDead. The race is invisible to the developer.
8.8 Cross-Core IPC Cost
Cross-core sends pay one IPI to wake a blocked receiver, one memory barrier on enqueue, and cache-line bouncing on the queue's head/tail indices. These are real costs but they are bounded and predictable. v1 does not optimize cross-core IPC beyond getting it correct.
8.9 Deadlock and Mutual-Blocking Avoidance
The kernel does not detect or break deadlocks.
Design rule: In any protocol where A and B both send to each other, at least one direction MUST use
try_send. Mutual blocking sends are an anti-pattern the kernel will not detect and will not recover from. The supervisor's quantum-starvation watchdog is a last resort, not a primary mitigation.
The classic deadlock - A and B both call send to a full queue - is the developer's responsibility to prevent at the protocol level. Use try_send, structure as request/response, or apply explicit timeouts.
9. Scheduler and SMP
9.1 Model
- Multi-core in v1. Number of cores discovered at boot.
- Per-core run queues. Each core runs round-robin over its own queue.
- Static placement. Services are pinned at spawn; they never migrate.
- 10 ms preemption quantum, per core, enforced by each core's local timer.
spawn ──▶ Ready
│ scheduler selects
▼
Running ◀──────────────────────────────────────────┐
│ │
├── timer preemption (10 ms) / yield() ─────────┘
│
├── recv() on empty queue ──▶ BlockedOnRecv
│ │
│ message arrives │
│ (IPI wake) ─────┘
│
├── send() on full queue ──▶ BlockedOnSend
│ │
│ queue drains (IPI) ─┤
│ or EndpointDead ─────┘
│
└── page fault / supervisor kill ──▶ Dead
│
frames reclaimed, generation bumped
9.2 Placement (Strict)
When the supervisor spawns a service:
1. If the contract specifies [placement] core = N:
- If core N exists and is ready, spawn on N.
- Otherwise, spawn rejected with PlacementInvalid.
The supervisor logs the rejection and skips the service.
The system continues with the services that did start.
2. If no placement specified:
- Round-robin across ready cores.
3. Once placed, the service stays on that core for its lifetime.
Rationale (strict): Contracts are enforced, not interpreted (§3.7). A contract that names a core means the developer expressed deployment intent. Silently rerouting to a different core would be exactly the kind of reinterpretation a capability-based system is designed to forbid. Contracted placement is deployment-coupled by design.
On restart: the placement decision is re-evaluated from scratch using the rules above. The supervisor does not remember the previous core.
- If the contract specified a core, that core is required again. If it is unavailable, the restart fails with
PlacementInvalid- the same strict rule as initial spawn. - If the contract did not specify a core, round-robin selects a fresh core, which may differ from the previous one.
This is consistent with invariant 11 (identity is stable; location is not). Sticky placement would make location stable across restart, contradicting the principle. Mid-execution migration remains forbidden.
9.3 Yield
#![allow(unused)] fn main() { yield() -> () }
Yield is advisory. Preemption remains enforced regardless. The scheduler does not rely on cooperative behavior for correctness or fairness.
9.4 Cross-Core Wakeups
When a syscall on core 0 needs to wake a task on core 1 (e.g., send woke a blocked recv), the kernel sends an IPI to core 1. The receiving core's IPI handler re-enters the scheduler.
9.5 What v1 Does Not Have
- Work stealing
- Load balancing
- Priority scheduling
- Service migration
- Core hotplug (cores discovered at boot are fixed for system lifetime)
10. Memory Model
10.1 Isolation
Each service has a separate virtual address space established at spawn time via per-task page tables.
10.2 Limits
[resources.memory]
request = "32MiB" # minimum needed to start
limit = "64MiB" # maximum permitted
10.3 Enforcement
Service memory action
│
├── alloc within limit ─────────────▶ Memory returned ──▶ Continue
│
├── alloc beyond limit ─────────────▶ AllocDenied ──▶ Service continues (may degrade)
│
└── access outside mapped region ──▶ Page fault ──▶ Service killed
│
Supervisor decides restart
10.4 Two Failure Modes
AllocDenied is recoverable. The service knows it asked for too much and can degrade.
A protection violation is unrecoverable. The service is in undefined state and the only safe response is termination.
10.5 TLB Coherence
When a page is unmapped (service killed, memory reclaimed), the kernel issues a TLB shootdown via IPI to every core. Operations resume only after acknowledgment from all cores. v1 minimizes unmap frequency by reclaiming memory only at service death.
Amendment 2026-10-10 (backlog/fixed/80 K20): this section names the guarantee, not a mechanism, and the mechanism it named had not run for some time. The paragraph above says the kernel "issues a TLB shootdown via IPI to every core" and waits for acknowledgments. It does not. The broadcast that did that had no caller, and has been deleted. What the kernel guarantees, and has guaranteed all along, is this:
No core can use a translation into a frame after that frame has been freed.
- Reclamation waits for quiescence. A dead task's stack and page tables are not freed until no core is running it or still leaving it (
core_still_using,CORE_LEAVINGintask/scheduler.rs). Nothing is freed while a task can still execute.- Every switch invalidates on the core that switches. x86 writes CR3 (no PCID), ARMv7 issues
TLBIALLwhen TTBR0 changes, RISC-V issuessfence.vmaafter writingsatp, and AArch64 flushes on every switch. A core that ran the dead task has dropped its entries before it stops counting as "leaving" it.- Where an idle core keeps a dead root installed, the free invalidates everywhere. On AArch64 an idle core keeps the last task's root in TTBR0, and the CPU may walk it speculatively, so
free_page_table_rootissues an inner-shareable invalidate (tlbi vmalle1is) before the root goes back to the allocator. The other ports switch an idle core to the kernel's own root.- Nothing changes a mapping under a running task. User mappings are only added while a task lives; the kernel-stack guard pages are unmapped on the boot core before any other core starts; the Pi 4 framebuffer remap is boot-only and invalidates inner-shareable anyway.
- No address-space identifier is in use on any port (no PCID, ASID 0 throughout). A port that adopts one must not reuse it before the invalidation that makes the reuse safe.
What this does NOT change. Translation coherence is still a kernel responsibility, under memory isolation and SMP routing (4.3); no responsibility is added or removed, and no guarantee is weakened. Removing the broadcast removed no local invalidation. If a future feature changes a live mapping - a remap, a permission downgrade, an unmap a running task can observe - it brings the cross-core invalidation it needs with it, and is recorded here; until then that machinery would be speculative code (26.2).
Two residuals, recorded rather than closed (26.7). Both concern speculation only; the kernel makes no access through either window. (a) On every port a task that kills ITSELF still has its root installed while its lower tables are freed (the root itself is deferred,
CORE_PENDING_PML4). (b) An AArch64 idle core walks a root whose lower tables have been freed, untilfree_page_table_root's invalidate. Whether wrong-path speculation through a recycled table frame can have a visible effect - setting an accessed bit, or a speculative read of a device register through a garbage descriptor - is not checked. The smallest hardening for both, should it ever be needed, is to switch the core to the kernel root before reclaim.Pinned by P7, which no longer stands in for this property with a generation count. A task stamps a pattern into fresh pages and is killed - from another core on even cycles, by its own fault on odd ones - and a checker given the same addresses, on the same core and on another, must read only the zeroes the kernel hands out (
no_stale_translation_after_death, 32 cycles). Shown to fail when the checker is broken and when the kill path skips both its wait and its wake. Its limit, recorded: a kill path that skips ONLY the wait still passes, because the wake stops the victim before its frames are reused. The per-port proof is recorded inbacklog/fixed/80K20.
11. Bootstrap Sequence
11.1 Sequence
Limine (Bootloader)
── loads kernel image, hands off to BSP
── supplies: physical memory map, framebuffer, SMP topology, HHDM
Kernel BSP
── paging, IDT, GDT
── frame allocator, capability subsystem
── start APs (real-mode trampoline → long mode)
APs: enter idle scheduler loop
── mark all available cores ready
── spawn supervisor on Core 0 (the kernel's ONE direct spawn - no init)
supervisor (Core 0)
── spawn events on Core 0
── read boot manifest
── spawn services per placement policy (§9.2),
wiring each from its name→cap map (no kernel name resolution)
── System reaches multi-core steady state ──
Amendment 2026-06-21 (naming Phases 3b-5): the kernel spawns the
supervisordirectly;initis removed; the registry service is retired. Moving name→endpoint resolution out of the kernel (docs/naming-design.md, Path C §3.7) makes the supervisor the name authority. Phase 3b moved the name service under the supervisor; Phase 4 then retired the registry service entirely (the kernel's minimalname → endpointrecovery directory -ipc::names+ the gatedAcquireSendCap- is the namer now; the supervisor wires every service from itsname → capmap and clients reacquire by name through the directory). Phase 5 removesinit: the kernel's one direct spawn is the supervisor (task::spawn_supervisor, using the gatedSUPERVISOR_ELF), and the supervisor - not init - spawns the logger. The supervisor's boot-time spawn failure is still fatal (the kernel panics,"supervisor spawn failed", §11.3, §6.2) - now from the kernel's direct spawn rather than an init abort. The non-restartable set is now justsupervisor+ kernel.
Amendment 2026-09-12 (multi-architecture): the sequence above is the x86-64 one, and THERE IS MORE THAN ONE ENTRY PATH.
kernel_mainis called only by x86-64's_start. The ARM, AArch64 and RISC-V ports bring the machine up themselves (arm_boot_main,aarch64_boot_main, and the RISC-V S-mode entry) and then join the same neutral kernel. The consequence is a real trap rather than a pedantic one: anything added to the neutral boot path runs on x86 alone, silently, and a port that never reaches it shows no error at all. Limine, the HHDM and APIC-supplied SMP topology are x86-64 facts; the others discover memory and harts from a device tree and start secondary cores through their own mechanism (PSCI on ARM, SBI HSM on RISC-V). Everything §11 says about WHAT must be true at the end of boot holds on every port; only the route differs.
The bootloader is Limine, accessed via the Limine Boot Protocol. Limine is responsible for loading the kernel image, supplying the physical memory map, the framebuffer descriptor, kernel relocation info, and the SMP topology (APIC IDs of all available cores). See Appendix A for the bootloader rationale and installation story.
11.2 BSP and APs
- BSP (Bootstrap Processor) - the first core to execute kernel code. Responsible for kernel init and bringing APs online.
- APs (Application Processors) - secondary cores. Brought up via real-mode trampoline (
arch/x86_64/ap_boot.rs), then jump to long-mode kernel code, then enter idle.
Because Limine supplies APIC IDs directly, the kernel does not need to probe ACPI/MADT for SMP topology. This removes a non-trivial subsystem from arch/x86_64/ap_boot.rs.
11.3 Failure During Bootstrap
| Failing component | Effect |
|---|---|
| Bootloader | Hardware reset |
| Kernel BSP init | Kernel panic, halt |
| AP startup | Kernel logs warning, continues with available cores; if zero APs come up, system runs as single-core |
| supervisor spawn (by the kernel - the one direct spawn, no init) | Kernel panic, halt (TCB) - "supervisor spawn failed" |
| events spawn (by the supervisor) | Supervisor logs to kernel ring buffer, retry once |
| Application svc | Supervisor logs, may retry per policy |
| Service contracted to unavailable core | Spawn rejected with PlacementInvalid; supervisor logs and skips; system runs without that service |
11.4 Logging Before Any Service Exists
The kernel maintains a 16 KiB ring buffer (a single shared sink). Anything logged writes to the ring buffer and the serial console - always, not only before a service is up. Nothing drains it, deliberately: drain_to_events has zero callers and kernel/src/log.rs says so in its first line. (This body previously said "per-core view" - there is one static RING - and that events "drains the accumulated buffer once, at its own startup". It never has; backlog/fixed/06 is open, and the 2026-09-04 amendment below establishes non-drainage as the design.)
Amendment 2026-09-04 (
logger->events): the service is renamed, and this section's title was wrong in a second way that matters more than the name. The title read "Logging Before Logger Exists", which implies logging is something theloggerservice does once it is up, and that the kernel ring is a stand-in until then. It is not, and never was.ctx.log()is syscall 5, gated by thelog_writecapability, writing the kernel ring and serial DIRECTLY - always, for every service, for the life of the machine. No log line has ever been sent to that service; its contract declares onlyipc_receive, and its endpoint is drained with unrecognised messages dropped.The consequence is a property worth naming, because it is easy to destroy by tidying: logging does not depend on the service being up. A chaos storm that kills it loses no log output, and
ctx.log()never blocks on it and never returnsEndpointDeadfrom it. So logs must NOT be re-pointed ateventsas it grows - that would make observing a failure depend on a service that can fail, which is the same argument §15 makes about storage, one layer up. Traces and metrics ride IPC to the service; logs stay on the floor.The rename itself is the name catching up with the job. The service has held the 192-event IPC trace ring since
traceshipped, and has never held a log.eventsrather thanobservability:observealready exists as the live view, house style is one short word, and a service named after a property of a system becomes the dumping ground §4.4 and §26.2 exist to prevent. It is cheap because the capability model works -ctx.log()resolves throughlog_write_slotand the trace path through a singleSINK_NAMEconstant, so no service names its own sink.What is NOT renamed, deliberately:
log_write,log_write_slot,ctx.log(), syscall 5 andkernel/src/log.rs. Those are this section's floor, which is a separate path the service was never on. §22 Test 2's assertions are renamedlog_received/log_did_not_receivefor the same reason - they check that a log reached the floor, which is what they always checked.No kernel responsibility is added or removed. The kernel was edited (hard-coded service-name lists in
task/scheduler.rsandbuild.rs), which is re-verification rather than growth. Design note and evidence:docs/observability.md§1 and §9.
Where the machine's only output device is a display, the floor also includes a minimal framebuffer blit (kernel/src/bootcon): plain ASCII, escape sequences discarded, no character grid, no cursor, no scrollback. It is not a terminal - the terminal is the console service (docs/console-service.md §9).
Amendment 2026-08-17 (console service): the log floor covers a minimal framebuffer blit, because §11.4 was x86-shaped. This section said "serial console" because on a PC serial is always there. On a Raspberry Pi wired to a TV it may not be, and a kernel that can only speak to a serial port it does not have is mute - a boot that fails before any service exists, or a panic, produces a frozen screen and no reason on it, which is exactly the silent failure invariant 12 forbids.
The blit earns ring-0 residency by impossibility, which is the only thing that does (the bar the control channel failed to clear and the supervisor spawn clears): a panic halts every core, including the
consoleservice, so it cannot ask a service to report it. Boot output has the same shape - it precedes every service, including the one that would render it. Both are this section's existing ring-buffer argument applied to a machine with no serial port, which is why the answer is the same one: a bounded floor the kernel owns.The amendment is deliberately narrow, and the narrowness is the point. What left the kernel in the same change was 1,172 lines of terminal emulation - the ANSI/CSI state machine, the UTF-8 decoder, the shadow grid, the cursor, scrolling, reverse video - because rendering a shell prompt is policy (§26.10) and a display driver is §4.4 anti-scope by name. What the floor keeps cannot format, cannot position, and cannot scroll: reaching the bottom of the screen clears it and starts again at the top, since serial holds the full history either way. Ownership of the framebuffer transfers to the service when the kernel GRANTS it, at spawn - not when the service first renders - and returns to the kernel if that service dies, or on a panic.
§22 has no new test: the property this pins is a negative one on a machine we cannot fail on demand in QEMU. It is pinned instead by
scripts/commandments.py, which counts the kernel's modules against §4.3 and for whichfbconwas the last standing violation.
Amendment 2026-10-08 (
events log boot): the floor keeps a fixed copy of the BOOT, and it is readable. The ring above wraps, and nothing reads it - so on a busy machine the boot was gone from the kernel within seconds, and the only record of what a machine found as it came up was a serial cable that is often not attached. The kernel already held every one of those bytes and had no way to give them back.Beside the ring,
log.rsnow keeps the first 32 KiB ever logged, which fills once and then never changes. InspectKernel query 27 copies a range of it out, INTROSPECT-gated, because the boot log names every service and device on the machine; the shell shows it asevents log boot. A full record says so, and that later lines are on serial.What this does NOT change is the point of the amendment above. The record is read by COPY, never drained, so no log line depends on a reader being up, and
ctx.log()is exactly what it was. It is the floor this section already defines, made readable - not a log service in the kernel. The kernel does not parse a line, keep a line count, or know which lines matter: it keeps bytes in order and stops when the array is full. No responsibility is added (it is 4.3's memory and the existing 11.4 ring); the new query is pinned inCOMMANDMENTS.baseline.tomlbecause a query is surface. The cost is 32 KiB of kernel memory on every port.
12. Drivers and Interrupts
12.1 Model
Kernel routes interrupts. Drivers are user-space services. block-driver is restartable like any other service (§6.1, Phase D amendment 2026-06-17) - it was "trusted in v1" until fs gained crash-consistent recovery.
12.2 Routing
Hardware IRQ N (arrives on some core)
│
▼
Kernel IDT handles interrupt
│
▼
Interrupt Router dispatches by IRQ number
│
▼ IPC message to driver's interrupt endpoint
Driver Service
── recv() returns interrupt event
── handles device via MMIO capability
If the driver runs on a different core than the one receiving the IRQ, routing crosses cores via the same IPC mechanism as any other cross-core send.
12.3 Driver Capabilities
[capabilities]
hw_interrupt = [12] # IRQ line
hw_mmio = ["0xfee00000+0x1000"] # MMIO region
The kernel validates these at spawn time and grants caps only for the specified resources.
Amendment 2026-10-01 (
DevicePower, syscall 54): the device grant is RENEWABLE - a service granted a device's window may ask the kernel to cut and restore that device's power. This is not a seventh responsibility. The grant above already includes power: on the Pi 4 the kernel powers the SD domain through the firmware mailbox at boot BEFORE it can handwifi-driverthe radio's window, because a window to an unpowered device is not a grant. What the kernel could not do was renew it, and the CYW43455 made that matter: six host-side resets - I/O reset, core halt, 802.11 reset, chipcommon and PMU watchdogs, a RAM clear - each left a chip whose ROM will not boot a new firmware (docs/wifi.md45). Only cutting its power is a power-on, and every reference driver's recovery path cuts power.What the kernel learns, and what it does not. It mints
DEVICE_POWERat spawn to the one service it hands a fixed peripheral window to, where the arch layer can power the device behind it (arch::imp::device_power_control) - derived from the grant, not from a privilege bit the spawner passes, and never to anyone else, because a window has exactly one holder.DevicePower(on)checks that holding and drives the pin the arch layer names for the CALLER'S device (device_power): on the Pi 4,WL_ONon the firmware's GPIO expander, through the mailboxSET_GPIO_STATEtag - the pin Linux'smmc-pwrseq-simpletoggles for the same chip. The kernel does not know what the device is, what firmware it runs, whether it is alive, or when its power should be cut: those are the driver's (§26.10), and the hold-off and settle times are the device's and live in the driver with it. Every other port answers the seam withfalse, and the syscall reports that honestly rather than pretending. (Note 2026-10-08: the VisionFive 2 Lite answers it too - its AIC8800's power pin, by device kindWIFI_SDIO, result by read-back,arch/riscv64. Every port but those two answersfalse.)Why it is recorded. A new syscall and a new resource widen the surface Commandment I pins, and the gate refused this change until this paragraph existed - which is the gate working. The service that uses it does so as its LAST resort, after adopting the firmware it finds running (
docs/wifi.md46); the power cycle is for a firmware that has stopped, and it is what turns "reboot the machine" into "the driver recovers in a few seconds" (docs/wifi.md47). It is also the first brick of a shutdown: the grants run in reverse, with power the last thing taken.Amendment 2026-10-01 (later still): the paragraph two above overstates what was shown. It says six host-side resets "each left a chip whose ROM will not boot a new firmware" and that "only cutting its power is a power-on". Every one of those resets, and every warm power-up after them, ran with the Arm cores at their minimum clock - the Pi firmware drops them a minute after boot when no cpufreq sets one - and with the cores held at turbo (
force_turbo=1,docs/wifi.md55) every power cycle comes up cold. So the power cut is shown to WORK, not shown to be the only thing that would; whether the resets alone recover a fast host's chip is open (docs/wifi.md56). The grant itself stands on its own: cutting a device's power is still the one recovery that cannot depend on the device's cooperation.Amendment 2026-10-01 (
CpuClock, syscall 55): the kernel sets the Arm clock to one of the firmware's two ends, and a SERVICE decides which. The Pi firmware owns the Arm clock and, with no OS asking it for a rate, drops the cores to their minimum a minute after boot and leaves them there. The CYW43455's firmware traps when it is uploaded that slowly (docs/wifi.md55), so something has to be able to ask for speed. The only way to ask is the firmware mailbox, which the kernel already owns - the SD power, the GPIO expander and the radio's power cut all go through it - and a channel with one owner cannot be handed to a service as well.What the kernel learns, and what it does not.
CpuClock(max)sets the clock to the firmware's ownGET_MIN_CLOCK_RATEorGET_MAX_CLOCK_RATEand returns what it reads back. The caller cannot name a rate. It is gated byCPU_CLOCK(resource 18), a privilege bit the supervisor may delegate and grants to ONE service,power, because the clock is one machine-wide setting and a second holder would silently overwrite the first. Who may be fast, for how long, and when to go back arepower's: a LEASE of at most 30 s, the clock at its maximum while any is open and its minimum otherwise, and a lease nobody releases expiring on its own, so a holder that dies cannot pin the machine fast (docs/power.md15, 26.10). Every port but the Pi 4 answers the seam withNoneand the syscall says so.Why it is recorded. A new syscall, a new resource and a new privilege bit widen the surface Commandment I pins. This is mechanism on a channel the kernel already owns, not a seventh responsibility
- the same argument as
DevicePowerabove - and thepowerservice is where the policy, and any future power policy, lives.Amendment 2026-10-01 (later): the result follows the pin's READ-BACK.
DevicePowerused to report success whenever the firmware accepted theSET_GPIO_STATErequest, which it does whether or not the pin moved - and in QEMU, where the expander is not emulated, a cut that never happened was reported as done. It now returns success only whenWL_ONreads back at the level asked for. The spawn also logsBT_ON, the same chip's Bluetooth enable: it reads 0 on this board, soWL_ONreally is the whole of the radio's power and nothing else needs cutting (docs/wifi.md53). No syscall, resource or authority changes.Amendment 2026-10-03 (audio on the Pis): a grant may include routing the device's pins and starting its clock, and the Pis' DMA page is granted whole. The Pis' 3.5 mm jack is two PWM channels fed by the SoC's DMA engine (
docs/audio.md, "The Pis"). Two of the steps that make it usable live in SHARED blocks: every pin's function in the GPIO page, every clock in the clock manager's. So the kernel does them as part of the grant, at spawn, exactly as it powers the SD domain before granting the radio's window - routes the jack's two pins to the PWM and starts the PWM clock at a fixed rate - and the driver (pwm-audio) is granted the PWM page and the DMA engine's page, mapped side by side, and a DMA arena. The device is a new kind (HwClass::AudioPwm), present where the arch says so (fixed_device_present, renamed from audio_pwm_present by the amendment below).What this is not. No syscall, no privilege bit, no runtime role: the kernel acts once at spawn and holds no policy - the sample rate (the PWM's range), the volume and when to play are the driver's (26.10). Not a seventh responsibility: it is the grant made usable, the reasoning of the
DevicePoweramendment above.What it costs, recorded rather than hidden (26.7). The DMA engine's page holds all fifteen channels and their shared status, so the driver is granted more than the one channel it uses. It is no more REACH than it already has - on these boards no IOMMU confines any DMA-capable driver (6.4), so a driver that can point one channel anywhere can already reach all of memory - but it is more than the grant names. The alternative, a kernel-mediated "start this channel" syscall, would grow the kernel to narrow a grant that confers nothing new, and was declined for that reason. The kernel also learns one more service name (
pwm-audio, in the Pis' fixed-window table and the two restart lists), the existing name-keyed practice that step D's classes are replacing. [Superseded the same day by the amendment below: the kernel learns no service name for audio, or for any other driver.]Amendment 2026-10-03 (later): the kernel knows ONE service by name, the supervisor, and nothing it grants or reports is keyed on a name any more. The amendment above recorded the kernel learning
pwm-audioas "the existing practice". The operator asked whether that was normal, and it was not: it was debt, anddocs/service-ownership.mdhad already said why it cannot be enforced - once the supervisor supplies the images, any image started under a matching name inherits whatever a name-keyed table grants that name. Six decisions moved off the name:
- Fixed device windows (the Pis' SoC blocks) are granted by the device KIND the spawn request names (
arch::imp::map_fixed_device(pt, kind),fixed_device_present(kind)), the same trust as a PCI class code. The Pi 4 radio gained the kind it lacked,WIFI_SDIO.DevicePowerreaches the pin of the kind the caller was GRANTED, not of the name it has.- Death notification and the restart count follow
SPAWN_FLAG_WATCHED, set by the supervisor from itsMANAGEDroster. The kernel's two lists of nineteen names are gone, and with them the drift that once lefttimeandcontroluncounted;V-managed-watchedchecks the chain that replaced them.- The display is reclaimed from, and console output delivered to, the task granted the
FRAMEBUFFERkind, not whatever is calledconsole.- Two grants were removed because nothing used them: the Pi 2
block-driver's EMMC window (its disk is USB; the EMMC is the boot card) and a name-matchedconsole_pushmint that matched nothing.No responsibility moves and no authority widens: every change narrows who a grant reaches, from "anything with this name" to "the request that names this device". One spawn flag is added to a request the kernel already validates. The name the kernel still knows is
supervisor, because the kernel spawns and respawns it (6.2).docs/audio.md, "No service names in the kernel".
Amendment 2026-10-14 (
PowerOff, syscall 56): the kernel turns the machine off, now or at the ONE deadline it holds, and the OPERATOR decides when.rebootresets the machine through a channel the kernel owns on every port; turning it off uses the same channels - the Pis' power-management watchdog with the boot partition set to 63 (halt) instead of cleared, the RISC-V firmware's SRST call with the shutdown type instead of a reboot, and on x86 ACPI soft-off (S5), read from the FADT and the DSDT's\_S5package in the tables the kernel already walks for the IOMMU. Each port answers one new seam member,power_off, which returns only when the hardware did not turn off, with the reason; then every core halts throughhalt_all_coresand the last line says it is safe to switch off. A halt asked for is not a crash and is not printed as one.The deadline, and why the kernel holds it.
PowerOffturns the machine off now, or sets the machine's one pending power-off up to 24 h ahead, or cancels it. The kernel holds that deadline on the scheduler's existing tick and fires it whether or not any service is alive, because a shutdown must not be lost with the services that asked for it or count it down (the operator ruled a lost shutdown unacceptable,docs/shutdown.md4.4). It is the kernel's own scheduled action, not service state (15): no service's data is kept, nothing is keyed by name, and a reboot clears it. Earliest wins - a holder may bring a shutdown forward, never push one back - any holder may cancel, every change is logged with the caller, and the time is monotonic, never the wall clock.Who holds it.
POWER_OFF(resource 19) is a privilege bit the supervisor may delegate, granted to the SHELL alone, besideREBOOT: ending the session is the operator's, and no service has a reason to end it - a failing service is restarted, never the machine.powerholds no shutdown authority; it reads the deadline, warns and does a bounded tidy-up three seconds before it. The Commandments baseline lists the shell as the one holder, so a second (a power button) is a recorded decision. A holder acts only on its own inputs and never offers shutdown-on-request to other services, which would reopen an anonymous path one level up; the keyboard residual of SEC-2 (6.4) applies, since anything that can type can typeshutdown.Visible, deliberately. InspectKernel query 28 (the seconds left, or -1) is UNGATED, deliberately, because a deadline that outlives every service must be seen by everything that might report it, and a shutdown planted by a compromised holder must never be hidden. It discloses no task's state and confers no authority.
What it does not do, recorded rather than hidden (26.7). ACPI asks the OS to run the firmware's
\_PTSmethod before S5, which is bytecode this kernel does not interpret; a machine that gates S5 on it - the HP T630 - halts instead of powering off, and says so. The Pi 2 cannot cut its own 5 V and halts; the Pi 4's firmware cuts its rails only where its EEPROM setsPOWER_OFF_ON_HALT=1; the VisionFive's firmware cannot reach its power chip and stops inside the call, so the kernel says what to do before making it. Hardware-verified on all five boards, 2026-10-14: the Wyse powers off and the rest halt, each saying which (docs/shutdown.md5).Why it is recorded. A new syscall with three operations, a query, a resource and a seam member widen the surface Commandment I pins. It is mechanism on channels the kernel already owns -
reboot's sibling, and one more timed action - not a seventh responsibility, the argument theDevicePowerandCpuClockamendments above make. MISCIS is unchanged.Amendment 2026-10-15 (
rebooton the deadline, S6): the one deadline also holds a REBOOT. The operator asked thatreboottakeshutdown's forms -rebootcounting down from 3,reboot now,reboot 10m. A delayed reboot has exactly the problem a delayed shutdown had: held in a service, it dies with the service. So it rides the same deadline.PowerOffgains two ops, 3 (reboot insecs) and 4 (cancel it), gated byREBOOTrather thanPOWER_OFF- the right that already resets the machine, held by the shell alone (SEC-2) - and the deadline is one word holding the tick and which of the two falls due, so a set, a cancel and the tick each see both together. A reboot that falls due resets throughhardware_reset, the pathReboot(18) already takes.There is still ONE deadline, and it holds one action. While a shutdown is pending a reboot is refused, and the other way round, so neither can quietly replace the other and a shutdown can never be lost to a reboot that happened to be asked for sooner. Earliest wins within a kind, as before. Query 28 now answers
secs * 2 + kind(1 for a reboot), still ungated, so what is pending and when are one answer that cannot disagree with itself.What it does not add. No syscall, no resource, no privilege bit, no seam member: two ops on a syscall this section already records, gated by a right the shell already holds, firing a reset the kernel already performs on its existing tick. Not a seventh responsibility, for the reason the amendment above gives; MISCIS is unchanged. What grows is surface - two ops and a query's encoding - recorded here because Commandment I pins surface and the gate counts syscalls and queries, not ops, so it would not have refused this.
reboot nowand Ctrl+Alt+Del stay the immediateReboot(18). QEMU-verified 2026-10-15 (osdev test shutdown, a reboot falling due and the machine back at a prompt); hardware-verified on all five boards the same day. The Pi 4's first card cut its last line on reset; the UART wait that fixed it is inarch/, and the Pi 2 and the Pi 4's re-card show the lines whole.
13. Service Contracts
13.1 Format
name = "ping"
version = "0.1.0"
[resources.memory]
request = "32MiB"
limit = "64MiB"
[capabilities]
ipc_send = ["pong"]
ipc_receive = ["ping"]
log_write = true
[placement]
core = 0 # optional; if omitted, supervisor uses round-robin
13.2 Placement Field (Strict)
- Omitted → supervisor places via round-robin across available cores.
- Specified → supervisor requires that exact core. If unavailable, spawn is rejected with
PlacementInvalid.
Strict semantics: A contract that names a core is a deployment-intent statement. The supervisor will not silently reroute to a different core. If
placement.core = 2and core 2 didn't come up, the service does not start; the supervisor logs the rejection and continues. Contract authors should specify placement only when they have a real reason.
13.3 Request, Not Permission
The developer declares what the service needs. The OS decides whether to grant it.
13.4 Build-Time Validation
osdev validates contracts using JSON Schema applied to the TOML structure.
Guarantees: correct structure, valid capability names, valid resource declarations, valid core IDs (range check only), required fields present.
Non-guarantees: behavioral correctness, that the binary uses only declared caps, that limits are reasonable, that the requested core will be available at spawn time.
Build-time validation is structural, not behavioral. Behavioral enforcement is runtime-only in v1.
13.5 Schema
contracts/schema/service.schema.json. Versioned. Breaking changes require a major version bump and a documented migration.
13.6 Runtime Enforcement
Every syscall checks the calling task's capability table, populated at spawn time from the spawn request. The kernel does not consult the contract at runtime, and never has.
Amendment 2026-09-14: the capability table is populated from the SPAWN REQUEST, not from the contract, and this section said otherwise for long enough that it led a contributor into a change that compiles, validates, passes every checker, and does nothing.
What actually grants authority. The supervisor holds each service's image and sends the kernel a spawn request carrying its privilege word, send peers, memory limit, core and device class; the kernel mints exactly that, after refusing any privilege the supervisor does not itself hold (
SUPERVISOR_DELEGATABLE,privileges_caller_lacks) - which is what keeps delegation from being ambient authority (§3.1). The kernel's ownservice_configtable covers its ONE direct spawn, the supervisor (§11.1). Those two are the whole of it.The kernel cannot read a contract. It is
no_stdand cannot parse TOML at spawn. That is not a new fact and not an implementation shortcut -scripts/contract_check.pyhas opened with it since it was written, and that script exists PRECISELY because the.tomlis a second, human-facing declaration that can drift from the first.So what is a contract? A build-time declaration: schema-validated by
osdev validate(§13.4), and reconciled against what is really granted bycontract_check.py(memory limit, placement, send peers) and byIV-contract-authorityinscripts/commandments.py(the authority capabilities). It is the reviewable statement of what a service may do (§26.9). It is not the mechanism.Why this was worth amending rather than leaving as a near-enough shorthand. A weak model was given "let
recorderrestart a service it sees stop responding", with no mention of any checker. It addedservice_control = truetorecorder's contract and reported that the kernel would grant it at spawn - which is what this section and §14.1 both told it. The change compiled,osdev validatepassed it, and all twelve checkers stayed silent. It does not work:recorder's privilege word is0, every call is denied, and the denial is discarded twice (the SDK'srestartswallows its ownkillerror and the caller wrotelet _ = ...) while the log line printed BEFORE the call asserts a restart that never happened. A service that looks authorised on paper, cannot act, and says it did.And it had been caught before.
audits/userspace-audit.mdflagged exactly this in 2026-07-12 - quoting this section's own words back at it, that "the contract stops being the authority's source of truth" - and marked it RESOLVED. The resolution changed the CODE and left the constitution saying the wrong thing, which is how a corrected defect goes on causing the error it was corrected for. Four other documents repeated the claim and are fixed in the same change.That is this document leading someone into a silent failure, which is invariant 12 broken at the documentation layer rather than the kernel one. The gate that now catches it is
IV-contract-authority; this amendment removes the reason it would be needed a second time.
14. Service Lifecycle
14.1 Spawn
- Supervisor takes the service's image and its row in the spawn table (the contract was validated at BUILD time, §13.4 - nothing parses TOML here).
- Determines core placement (round-robin or contract override per §9.2; rejected if contracted core unavailable).
- Asks the kernel to create a new task on that core, in a spawn request carrying the privilege word, send peers, memory limit and device class.
- Kernel refuses any privilege the supervisor does not itself hold (
SUPERVISOR_DELEGATABLE), so a spawner passes on what it has and never mints. - Kernel mints capabilities per the spawn request (each tagged with current resource generation).
- Kernel maps service binary into new address space.
- Service registers any owned endpoints in the kernel name directory (
ipc::names). - Service enters main loop on its assigned core.
Supervisor ─── spawn(name, request) ───▶ Kernel
│
resolve placement (§9.2):
contract core or round-robin
│
Err(PlacementInvalid) ◀─┤ (core unavailable: stop here)
│
allocate Task + CapTable from the request
map binary into new address space
enqueue task on target core run queue
│
Supervisor ◀── Ok(task_id) ────────────────┘
│
New Service: enters execution
── registers endpoint in the kernel name directory
── service_main() ── enters work loop
Amendment 2026-09-26 (step C): step 1 above is only true because the kernel now accepts an IMAGE from userspace, and that widening was never recorded here. When the supervisor took ownership of every service image (
docs/service-ownership.md, step C), the kernel stopped holding the bytes it spawns. Its catalogue issupervisoralone. So a spawner can no longer ask for "the image you already have" - it must SUPPLY one, andSpawnImage(syscall 52) is the syscall that accepts it.Starting arbitrary bytes is a different authority from starting a known service, and it is now a different capability.
SPAWNand image-spawn were the same right until step C, which meant everySPAWNholder - the shell,chaos,control, every probe - could introduce NEW CODE under a real service's name in the window while that service was dead, and a client reacquiring that name (§14.3) would wire itself to it.SpawnImagetherefore requiresIMAGE_SPAWNon top ofSPAWN, and the kernel refuses the call when a caller holds only the latter.
IMAGE_SPAWNis deliberately NOT delegatable. It is absent fromSUPERVISOR_DELEGATABLE, so the supervisor cannot pass it on even to a service it trusts - a delegatable version would re-open the hole one grant later. The only two callers in the tree are the supervisor's ownspawn_by_imageandspawn_probe_row; everything else asks the supervisor over IPC. It stops the authority leaking to the dozen services that merely wanted to start something.What the supervisor GAINED, said plainly, because this is a real widening and not a re-labelling. Before step C the kernel held every image, so a runtime-compromised supervisor could start only code the kernel already carried - it could start the wrong service, or the right one too often, but it could not introduce code that was not in the image. After step C it can. A compromised supervisor supplies the bytes, so it can run anything under any name, and nothing before step 2 prevents that - step 2 (a signature over each image,
docs/service-ownership.md) exists precisely to close it. This does not move the TCB: the supervisor is the trusted root (§6.1) and its compromise was always systemic. It does mean the CONSEQUENCE of that compromise is strictly larger than it was, and per §26.7 a limitation that cannot be closed today is recorded rather than left for a reader to discover. The IRQ-routing half of the same concern IS closed: the kernel refuses raw vectors and raw MMIO outright, as the paragraph below describes.What the kernel refuses, so that "supplies an image" is not "supplies a machine". The request is a fixed, versioned struct, and the kernel rejects a wrong version, a wrong size, an unreadable buffer, a name outside 1..=64 bytes, a
dma_pagesover its cap, an unknown device class, a BDF on a non-PCI class, any privilege the caller does not hold itself (privileges_caller_lacks), and - the two that matter most - raw MMIO addresses and raw interrupt vectors. A driver names a device CLASS and the kernel resolves the window, the arena, the BDF and the vector against its own bus scan (§12.3). A caller cannot hand the kernel an address and be given it.Why this is recorded rather than merely implemented. It is a new kernel authority and a widened syscall surface, which Commandment I pins and §26.9 requires be traceable to the capability that granted it. The code says all of this at
kernel/src/capability/mod.rs; the constitution said none of it, anddocs/service-ownership.mdhas carried "the CLAUDE.md amendment for step C must state the widening" as an open item since. No invariant moves: authority is still explicit (§3.3) and the kernel still holds no policy - it validates a request and mints exactly what the request asks for and the spawner may give (§13.6, §26.10). The net effect on authority points BOTH ways and it is worth being exact about which: narrower for the dozenSPAWNholders, who lost the ability to introduce code at all, and wider for the supervisor alone, as the paragraph above records.
Amendment 2026-10-17 (install): the supervisor starts an image READ FROM THE DISK, for an installed package, and only after checking its signature. Step 1 above holds for every built-in service; an installed package (
godspeed install,utilities/61_godspeed.md4b) is the one exception, and it is the step-2 shape the amendment above names. The supervisor reads a fetched package from/system/packages/, checks it with the codegodspeed verifyruns - the publisher's signature over its manifest, the signing key's standing in this machine's trust record, the contract and this machine's binary against the manifest's digests - and hands the kernel the very bytes it hashed, throughSpawnImageas for any other image (services/supervisor/src/installed.rs). It does so at install, at every boot and at every restart, with nothing cached between.What an installed package is given, and why it is safe to give: no privilege at all - none is asked for and none can be granted - and send peers only where its signed contract requests them AND the operator approved them, never
supervisor. It runs under its package name,publisher/name, which no built-in service can hold, so it can never stand in for one when a client reacquires a name (14.3). Restarts are bounded: five a boot, then it is left down, loudly.What is NOT closed, recorded rather than hidden (26.7). The signature is checked against the trust record and the grant read from the package's folder, and both are on
/system, which everyfsholder can write: something that can write there can replace the trust record or widen a grant, up to what the signed contract requests. The narrowing to the contract is what keeps a forged grant from reaching further.IMAGE_SPAWNstays the supervisor's alone and undelegated;godspeed-pmasks over IPC (supcmd::INSTALL). No kernel change, no new syscall, and no responsibility added: the supervisor already starts images and already decides with what.Amendment 2026-10-17, later (apps): one thing beyond peers, the console, for an
appand only with the operator's answer. An installed package of kindappis a utility that owns the screen and the keyboard while it runs (gs::app,docs/developer-services-design.md13.2, approved by the operator the same day). The supervisor starts it withSPAWN_FLAG_REQ_CONSOLE- the console read capabilitychaosand the shell already hold - when its grant namesconsole, whichgodspeed installasks about by name, and refuses to start an app whose grant does not. Still no privilege bit: the console is a spawn flag, and a service or a utility is never given it. The residual is SEC-2's (6.4): a holder of the keyboard can read what is typed while it runs, which is exactly what the operator was asked to approve. The kernel gives the console back when the app dies, so a crash cannot keep it.Amendment 2026-10-23 (drivers): an installed
driveris given ONE DEVICE, by what the bus says it is, and the authority that device carries - which on a machine with no IOMMU puts it inside the TCB (6.4). Not recorded when the first part shipped: v0.29.0 gave a driver package its device's register window and nothing else, v0.30.0 the same, and this section said nothing of it. What a driver package is given now (docs/developer-services-design.md13.1,services/supervisor/src/installed.rs), each named in its signed contract and approved by the operator:
- A PCI device, by class (
hw_pci_class): the kernel resolves which device from its own bus scan, exactly as for an in-tree driver named by class (12.3), and grants its register window - plus its interrupt when the contract asks (hw_pci_irq; the kernel allocates the vector, the caller names none) and a DMA arena of the size it asks (hw_dma, at most 2 MiB, never an address). Confinement is requested; whether it happens is the kernel's, per device (6.4).- A device an in-tree driver drives is TAKEN OVER, not shared: the supervisor stops that driver and keeps it stopped while the package is installed, and starts it again when the package is uninstalled, ends, or is left down. One holder per device, which the kernel does not enforce for a PCI device and the supervisor does.
- A USB device, by vendor and product (
hw_usb): no hardware authority of its own at all. Its host (xhci,dwc2, andehcisince the same day) binds it and serves its transfers to the one driver given that host as a send peer (gs::driver::bus), so the package is the host's client, aswifi-usbalways was.The TCB consequence, stated as 6.4 requires. A driver package granted a DMA arena on a machine whose IOMMU does not confine its device - every Pi, the VisionFive, and any x86 device the kernel leaves in passthrough - can point the device at any address: kernel-equivalent reach, so it is trust-critical by necessity, exactly as an unconfined in-tree driver is. That is why the arena is approved by a SECOND question at install, and why the question is asked on every machine: nothing a service can ask says whether the kernel will confine this device, so the warning is given rather than guessed (a confined machine asks needlessly; recorded, 26.7). A driver package with registers only, or a USB driver, carries no such reach.
What does not change: no privilege bit (the device is a hardware class in the spawn request, and the supervisor already spawns by class), no kernel change and no new syscall, and
IMAGE_SPAWNstays the supervisor's alone. MISCIS is unchanged.
14.2 Restart and Cap Rebinding (Possibly Cross-Core)
Steady state: Service A (Core 0) holds cap to Service B gen=4 (Core 1)
Step 1 - Supervisor kills B:
Kernel closes B's endpoints, drains queues
Kernel bumps B's generation: 4 → 5
Kernel reclaims B's memory (TLB shootdown on all cores)
Step 2 - A tries to send via stale cap:
A ── send(gen=4 cap) ──▶ Kernel ── EndpointDead ──▶ A
(gen mismatch: held=4, current=5)
Step 3 - Supervisor spawns B on Core 2:
Kernel starts B with fresh cap table (gen=5)
B re-registers its endpoint in the kernel name directory
Step 4 - A reacquires:
A ── AcquireSendCap("B") ──▶ fresh cap (gen=5, Core 2) [kernel name directory]
A ── send(gen=5 cap) ──▶ Ok (routes to Core 2)
Key principle: the new instance may run on a different core than the old one. Clients never know - they see only EndpointDead, reacquire by name through the kernel directory, and resume.
14.3 Cascading Failure
Cascading failure is the client's responsibility. There is no implicit recovery. If A depends on B and B restarts, A's next syscall returns CapRevoked or EndpointDead, and A must retry, degrade, or fail.
Reacquiring the endpoint is necessary but not sufficient. A fresh cap to B's new instance does not refresh anything A obtained from B's previous incarnation. Every secondary thing A still holds that was derived from the dead instance - a socket or connection id, a resource or open-file cap, a generation number, or a cached copy of B's state - is stale: the new B never issued it and does not know it. A must discard or re-establish each of these against the new instance. In particular, A must not keep serving a cached view of B's state as authoritative once B has restarted: that view is a derived copy of B's truth (§26.4, Commandment III), and that truth was just replaced. Reacquire the endpoint, and re-derive everything that hung off the old one.
14.4 Supervisor API
#![allow(unused)] fn main() { supervisor.kill(service_name) -> Result<()> supervisor.restart(service_name, placement_override?: CoreId) -> Result<()> }
Required capability: service_control (held only by supervisor).
kill- immediate. The killed service does not get a chance to clean up. Clean shutdown is a separate codepath.restart- kill followed by spawn. Placement is determined as follows:- If
placement_overrideis provided, the supervisor requires that core (subject to the strict rules of §9.2; rejected if the core is unavailable). - If
placement_overrideis omitted, the placement decision is re-evaluated from scratch per §9.2 - contract-specified placement re-applies (and may fail withPlacementInvalidif unavailable); unspecified placement gets a fresh round-robin choice. - The previous core is not remembered. A service that ran on core 1 before the restart has no implicit affinity for core 1 after.
- If
14.5 Kill Semantics
Kill is for misbehaving services and for restart. It is not a graceful shutdown mechanism.
Amendment 2026-10-17 (
Exit, syscall 57): a program may END ITSELF, with a status, and the death notice says so. Until now nothing ended a task but thekillsyscall or a fault, so every program was a service that never returns, and a program that does one job - autility- could not exist outside the shell (docs/stdlib-design.md1, option B, chosen by the operator).Exit(status)ends the caller by the path a task that kills itself already takes (handle_kill's tail), with a third cause: the notice carriesEand the status, besideK(killed by) andF(a fault) (6.2 amendment 2026-10-11).It takes no capability, and that is deliberate, not an oversight against 21. The rule there - a syscall that does not validate a capability is rejected - exists so that no syscall reaches authority without one.
Exitreaches nothing: the one task it can end is the caller, asYieldandParkact on the caller and take none. A program could already end itself by faulting; this makes the same end deliberate and says how.What the kernel learns, and what it does not. A number, said in the notice. What an exit MEANS is the supervisor's (26.10): an installed package that ends itself is not restarted, because it finished; a service in
MANAGEDthat exits is restarted as any death is, because it is meant to run. The kernel keeps no record. No responsibility is added: ending a task is the scheduler's already (4.3). Pinned inCOMMANDMENTS.baseline.toml; one more SDK call site (18.5,exit).
15. State and Persistence
State belongs to services, not the kernel. Services that need to survive restart must persist externally and reconstruct on startup.
The filesystem service is the externalization mechanism for everyone else and cannot persist to itself. Resolution: the block driver holds a direct hardware capability and stores fs metadata. fs gives itself transactional metadata recovery - every mutation commits through a crash-consistent redo-journal and fs recovers to a consistent state on mount (docs/persistence.md §6.8). With that, block-driver and fs are restartable and no longer in the TCB (§6.1 Phase D amendment, 2026-06-17); their death is a supervisor restart, not a reboot. The recovery guarantee is backend-conditional - see the 2026-07-25 amendment in §6.1.
Stateless services (events in v1) restart trivially. Example application services (ping, pong) are also stateless and restart trivially - but they are demonstration services in examples/, not permanent architectural components.
16. Update Model
Update package
│
├── Signature valid? No ──▶ Reject
│ Yes ↓
├── Contract valid? No ──▶ Reject
│ Yes ↓
└── Policy allows? No ──▶ Reject
Yes ↓
Supervisor restarts service with new binary
Push vs pull is irrelevant - verification is the security property. Live code update is permanently rejected (§2.5); the only update mechanism is restart-with-new-binary.
17. Developer Workflow
osdev build # build kernel + services
osdev run --smp <N> # boot in QEMU with N cores
osdev image # build bare-metal image → build/os-usb.img (UEFI GPT)
osdev restart <service> [--core N] # restart in running OS; --core is dev-mode only
osdev logs <service> # tail logs
osdev test identity # run §22 test suite
osdev validate # validate every service contract
osdev mkfs / script-disk # build a filesystem image / a script disk
# NOT IMPLEMENTED - these are `todo!()` stubs that panic if invoked:
# osdev new <service-name> # scaffold (copy examples/00-hello instead)
# osdev publish # package + serve
# osdev status <service> # state + core (use the shell's `status`)
# osdev caps <service> # held caps (use the shell's `caps`)
osdev restart --core N is the CLI surface for the supervisor's placement_override (§14.4). It is rejected outside dev mode and subject to the same strict placement rules as a contract-specified core.
Iteration loop: edit → build → restart → logs. Only the changed service restarts. (publish
is in the not-implemented list above, so the loop does not pass through it; §26.2's "not implemented;
will be implemented when a test requires it" is the honest state of all four.)
18. Unsafe Policy
18.1 Permitted
kernel/src/arch/, kernel/src/memory/, kernel/src/capability/, kernel/src/smp/.
Plus the SDK's audited hardware/ABI layer: the syscall ABI (raw_syscall,
inline asm!) and the MMIO/DMA accessor modules (sdk/rust/src/mmio.rs and
sdk/rust/src/dma.rs). Userspace drivers (§12) cannot touch device registers or
DMA memory without unsafe; isolating it to these designated SDK modules - each
block carrying a // SAFETY: comment - keeps the driver services themselves
unsafe-free behind safe wrappers (Mmio::read32, Dma::write32, etc.), exactly
as the kernel isolates its unsafe to the four layers above. This is a recognition
of what the syscall ABI already required, extended to the hardware access §12 needs.
Amendment 2026-10-17 (install): the SDK's
memory.rsis a fourth permitted module, for a task's OWN memory.AllocMem(syscall 6) returns an address, and an address becomes something a service can read and write only throughunsafe. Until now nothing outside the tests needed that - every working set fit a stack (26.6.1) - and the one case that did, P7's stamped pages, lives inadversarial.rs. The install loader is the first production case: the supervisor reads a package's image fromfs, checks its digest and signature, and hands the kernel those same bytes, and an image is larger than any stack.Regionis two blocks (bytes,bytes_mut) over exactly the pages a successfulAllocMemmapped, and the supervisor staysunsafe-free behind it, as a driver does behindMmio.What it is not: an allocator. There is no free - the kernel reclaims a task's memory at its death (10.5) - so a region is asked for once, its size is the bound, and it is reused. No syscall and no kernel change; the rule that new
unsafelives in a permitted layer (18.5) is met by naming this one.
Plus the SDK's audited adversarial test module (sdk/rust/src/adversarial.rs). The §22 red-team /
fuzz / chaos suite must reach the raw ABI with fuzzed syscall numbers and arguments, and must execute
deliberate ring-3 faults (a null read, a non-canonical read, a divide-by-zero) to prove the kernel
kills the faulting task rather than wedging the machine (invariant 12; A14 / A15 / C2) - things no safe
wrapper can otherwise express. Isolating that unsafe to this one designated, SAFETY-commented module
(fuzz_syscall, fault_null_read, fault_noncanonical_read, fault_divide_by_zero) keeps the test
services themselves (probe) unsafe-free, exactly as the hardware/ABI layer keeps the driver
services unsafe-free. This is a recognition of what adversarial testing already required: probe used
to hold this unsafe directly - an untracked §18.2 violation the userspace audit (M8) closed. The
module is test-only; no production service calls it (a fault primitive just kills the caller, which the
kernel handles). scripts/unsafe_check.py now scans services/ and fails on any service unsafe,
mechanically enforcing the isolation.
18.2 Forbidden
All userspace services, osdev/, and all of sdk/ except the audited
hardware/ABI layer named in §18.1 - and all kernel code outside the four
permitted layers. A driver service that writes unsafe directly (rather than
going through the SDK's safe Mmio/Dma wrappers) is rejected.
Amendment 2026-09-13: this is enforced by the COMPILER now, not only by a grep. Every crate under
services/,examples/andosdev/carries#![deny(unsafe_code)], so rustc refuses the crate rather than a script noticing afterwards. That closes what a text scan cannot see -unsafeproduced by a macro expansion, or spelled across lines - and it fails at the author's keyboard instead of at the next CI run.
denyrather thanforbid, for exactly one reason, stated so nobody "tightens" it and breaks the build: a#[no_mangle]declaration is itself covered by theunsafe_codelint (an exported symbol can collide, which is a soundness hole), and every service needs#[no_mangle] service_mainbecausebuild.rslinks with--entry=service_main.forbidcannot be relaxed even for that. So the crates carrydenyplus ONE#[allow(unsafe_code)]on the entry symbol, andscripts/unsafe_check.pyasserts both halves: that the attribute is present, and that the only#[allow]sits on#[no_mangle]. An#[allow]anywhere else fails the check - the exception cannot become a door.No policy changes here. §18.2 already forbade this; what changed is who enforces it.
18.3 Documentation
Every unsafe block carries a SAFETY comment:
#![allow(unused)] fn main() { // SAFETY: <argument for why this is sound> unsafe { ... } }
A PR with an unsafe block lacking a SAFETY comment is rejected without review.
18.4 Audit Trail
audits/unsafe-audit.md lists every unsafe block. CI checks the file matches source.
18.5 Grandfathered Floors
unsafe outside the four permitted layers (§18.1) is tolerated only as
grandfathered lines in task/, syscall/, interrupt/, loader.rs and
main.rs, and in the two SDK files named below, frozen at the counts in
audits/unsafe-audit.md. Those counts may decrease freely but may
increase only by an amendment recorded here and in the audit, with a written
safety + necessity rationale.
Amendment 2026-09-12: the SDK's
service_context.rs(82) andipc.rs(8) are recorded as grandfathered floors, and this list gainsloader.rsandmain.rs, which it had always omitted. Neither is newunsafe- both are the state of the tree being written down for the first time.scripts/unsafe_check.pyscanned onlykernel/src/andservices/, so the SDK's ~125unsafelines were audited by nothing at all while §18.4 claimed CI checks the audit against source (backlog/fixed/18). The scan now coverssdk/, which is what makes these floors enforceable rather than merely stated.They are one design consequence, not 90 violations. 86 of the 90 are
unsafe { raw_syscall(..) }call sites:raw_syscallis anunsafe fnbecause it issues the trap instruction, so every caller opens a block - and these two files ARE the wrapper layer §18.1 describes, the one that exists so that driver and application services need nounsafeof their own. That worked:services/is at ZERO, mechanically enforced. The isolation stopped one layer short of itself.The fix that would actually close this is a SAFE
raw_syscallwrapper - the kernel validates every user pointer, so passing integers to a validating callee is sound - which collapses ~86 of them and leaves the SDK at roughly the 35 lines §18.1 sanctions. That is an SDK redesign on every service's call path, so per §26.7 it is recorded here as the known route rather than half-done. Until then the floors may only fall.
New unsafe that a feature or hardening needs must first try to live in a permitted
layer (arch/, memory/, capability/, smp/) rather than grow a grandfathered
file. A precondition that is merely boot-ordering (violating it wedges boot - a
liveness bug, not UB) does not justify an unsafe fn; make it a safe fn with a
documented contract, like memory::init / smp::init. Worked example: the H4
kstack-guard / W^X hardening (2026-06-08) was structured so its page-table unsafe
lives in arch/ and the boot call sites are safe fns - main.rs and task/mod.rs
stayed at their floors with no amendment needed. Four amendments to the grandfathered floors stand; the service_context.rs floor fell to 83 after the first two (2026-10-04, a dead call site removed) and the boot record took it back to 84; it fell to 80 on 2026-10-10, when the four spawn-by-name syscalls (7, 19, 38, 39) were retired with their SDK wrappers (backlog/fixed/80 K14), and to 77 on 2026-10-11, when the three uncalled NET_DEVICE wrappers went (backlog/21); it rose to 79 on 2026-10-14 and to 80 on 2026-10-17 by the amendments below. A fall needs no amendment, so this line only keeps the figure current (audits/unsafe-audit.md):
Amendment 2026-10-17 (
Exit):sdk/rust/src/service_context.rs79 -> 80. One call site,exit: oneunsafe { raw_syscall(57, ..) }behind the safeServiceContext::exitandgs::program::exit, for the 14.5 amendment of the same date. Necessity: a program cannot reach a syscall any other way. Safety: one integer and no pointer, and the syscall does not return.
Amendment 2026-10-14 (
PowerOff):sdk/rust/src/service_context.rs77 -> 79. Two call sites behind the §12.3 amendment of the same date:power_off_call, oneunsafe { raw_syscall(56, ..) }behind the three safe wrapperspower_off,power_off_inandpower_off_cancel; andpower_off_pending, oneunsafe { raw_syscall(13, 28, ..) }. The same single design consequence as theCpuClockamendment below. Necessity: a service cannot reach a syscall any other way. Safety: integers only, and the kernel checks the capability before acting; query 28 takes no pointer.Amendment 2026-10-08 (the boot record):
sdk/rust/src/service_context.rs83 -> 84. One moreunsafe { raw_syscall(13, 27, ..) }call site,boot_record_query, behind the safeboot_record_sizeandboot_record_readof the 11.4 amendment of the same date - one block for both, the same single design consequence as the two below. Necessity: a service cannot reach a syscall any other way. Safety: the read's buffer is typed at the kernel's chunk size, and the kernel validates the range before writing into it.Amendment 2026-10-01 (
CpuClock):sdk/rust/src/service_context.rs83 -> 84. One moreunsafe { raw_syscall(55, ..) }call site, the wrappercpu_clockbehind the §12.3 amendment of the same date - the same single design consequence as theDevicePoweramendment below. Necessity: a service cannot reach a syscall any other way. Safety: one integer to a kernel that checks the capability before asking the firmware anything.Amendment 2026-10-01 (
DevicePower):sdk/rust/src/service_context.rs82 -> 83. One moreunsafe { raw_syscall(54, ..) }call site, the wrapperdevice_powerbehind the §12.3 amendment of the same date. It is the same single design consequence the 2026-09-12 amendment describes - the SDK IS the wrapper layer, so a new syscall is one more block here and zero in any service - and the saferaw_syscallthat would collapse all of them remains the recorded route. Necessity: a service cannot reach a syscall any other way. Safety: the kernel validates the capability before touching any pin, and the call passes two integers.
19. Debugging Model
Bugs are classified as one of: kernel, arch, memory, ipc, capability, smp, service, cli.
Bug reports include: logs (kernel ring buffer + service), contract(s), QEMU repro steps including -smp N value, expected behavior, actual behavior, suspected classification.
Kernel panics print the reason (KERNEL PANIC: {info}) to the serial console and the kernel log ring buffer. Panics on any core halt the system: the panic path broadcasts an NMI so every core halts, not only the panicking one (§6.2). A reserved-page mechanism to persist the panic reason across reboot was once described here but was never implemented (and init, which would have re-read it, is removed - Phase 5); the panic reason lives on the serial console only.
20. Performance Philosophy
Ranked: correctness, observability, performance.
The IPC fast path is the exception. In a microkernel, every meaningful operation crosses an IPC boundary. v1 IPC uses simple predictable structures: one memcpy, constant-time cap + generation check, one IPI on cross-core wake.
No vibes-based optimization. Perf claims require benchmarks in tests/qemu/perf/.
21. Contribution Rules
A PR is rejected without further review if it:
- Introduces global mutable state outside a single owning service.
- Introduces ambient authority.
- Bypasses the capability system or generation check.
- Adds service migration or work stealing.
- Adds zero-copy IPC.
- Adds live code update.
- Introduces silent fallbacks at the kernel boundary.
- Breaks restartability of a non-TCB service.
- Adds unsafe code without a SAFETY comment, or outside permitted layers.
- Adds a syscall that does not validate a capability.
- Changes the IPC fast path without a benchmark.
- Edits CLAUDE.md without a rationale in the commit message.
- Introduces an em-dash (U+2014) or en-dash (U+2013) anywhere - in prose, code, comments, string literals, commit messages, or docs. Only the plain ASCII hyphen (-) is permitted as a dash; box-drawing characters are fine. This is a house writing convention, enforced repo-wide for consistency.
- Weakens a gate rather than the rule it enforces. Deleting a checker or removing one from
EXTRA_CHECKS, widening a path exemption, adding a baseline entry instead of fixing what it found, using aconform-okmarker to go quiet rather than to record an exception, or making a diagnostic vaguer (22.7). The enforcement layer is open to contribution like everything else and a rule may be repealed - by amending this document with a written rationale, so that the law and the gate change together. What is rejected is the version where the law still says one thing and the gate has stopped noticing.CONTRIBUTING.mdcarries the long form.
Reviewers ask: does this respect the constitution, leave the kernel small, present a convincing unsafe argument, include a test, make the system more or less understandable?
A grounded catalog of these violations - each paired with the correct pattern and the section it breaks - is docs/anti-patterns.md, the field guide to constitutional violations. Scan the categories your change touches before opening a PR.
22. Identity Test Suite
22.1 Purpose
The identity tests are the minimum set of tests that, if any one fails, the system is no longer the system this document describes.
They are the executable form of the constitution. If you change the spec in a way that invalidates one of these tests, you have changed system identity. That requires a CLAUDE.md amendment.
22.2 Categorization
The test suite is layered. Each layer answers a different question about kernel correctness. A pass on one layer is necessary but not sufficient. Battle-hardening requires passing all layers.
| Category | Purpose | Bar (what failure means) | Status |
|---|---|---|---|
| Identity | Pin constitutional decisions; existence proof | Constitutional invariant violated | §22 (Test 11 added, H11) |
| Property | Universal invariants under random inputs | A claim the spec makes does not hold | §22 (P1-P10, 10/10) |
| Fuzz | Crash resistance under adversarial inputs | Kernel panics on user-controllable input | Active |
| Stress | Survival under sustained load | Drift, leaks, or corruption appear over time | Active |
| Performance | Latency / throughput benchmarks | A measured number regressed | §22 (10/10) |
| Adversarial | Capability isolation under attack | An attack succeeds where the spec says it fails | Active |
| Chaos | Graceful degradation under partial failures | A defined failure mode is not handled cleanly | Active |
┌─────────────────────────────────────────────────────────────────────┐
│ Foundation - must pass before anything else │
│ Identity (§22) - Tests 1-15 ✅ - Constitutional invariants │
└──────────────────────┬──────────────────────────────────────────────┘
┌──────────────┴─────────────────┐
▼ ▼
┌───────────────────┐ ┌───────────────────┐
│ Property │ │ Fuzz │
│ Universal invs. │ │ Crash resistance │
│ under random │ │ on adversarial │
│ inputs │ │ inputs │
└───────┬───────────┘ └──────────┬────────┘
▼ ▼
┌───────────────────┐ ┌───────────────────┐
│ Stress │ │ Adversarial │
│ No drift, leak, │ │ Cap isolation │
│ or corruption │ │ under attack │
└───────┬───────────┘ └──────────┬────────┘
└─────────────┬────────────────────┘
┌───────┴────────┐
▼ ▼
┌──────────────────┐ ┌──────────────────┐
│ Performance │ │ Chaos │
│ Latency / │ │ Graceful │
│ throughput │ │ degradation │
│ baselines │ │ under failures │
└──────────────────┘ └──────────────────┘
Tests live under tests/qemu/, organized by category:
tests/qemu/
identity/ # §22.5-§22.6 (complete)
property/ # see Property Tests below
fuzz/ # see Fuzz Tests below
stress/ # see Stress Tests below
perf/ # see Performance Benchmarks below
adversarial/ # see Adversarial / Red-Team Tests below
chaos/ # see Chaos Tests below
harness/ # shared infrastructure
The base harness (§22.3) boots the OS with a configurable -smp N value; multi-core tests assert on N ≥ 2. The battle-hardening categories extend it with longer timeouts (stress, perf), metric collection (perf), and fault injection (chaos).
The bar across every category is the same as identity: no FAIL, no BLOCKED with a vague reason. A failure means a real bug - fix it, add a regression test to the appropriate suite, then move on.
Identity (§22) - Complete
All passing (Tests 1-15; harness reports 24 cases incl. A/B + IR + Test 11 + Test 15). No regressions allowed. Any failure here is a constitutional violation that requires either a kernel fix or a CLAUDE.md amendment. Test 11 (added by H11) is now name-resolves-after-restart-via-the-kernel-directory - the registry service was retired in naming Phase 4 / Path C (docs/naming-design.md §3.7), so Test 11 pins the directory's restart property instead of a registry service. Test 1B now corrupts the supervisor (the registry it used to corrupt is gone). Test 15 (Path C / Phase 6) pins that the supervisor itself survives its own restart - the kernel respawns it, so the unkillable set is {kernel} alone.
Property Tests
Property tests assert universal claims over randomized inputs. Identity tests prove the system can satisfy each invariant; property tests prove it always does. Each test runs thousands of iterations with QuickCheck-style generators.
| ID | Property | Pins |
|---|---|---|
| P1 | Random bytes → CapNotHeld or CapInvalid; never accepted as a cap | §7.3 (unforgeable) |
| P2 | Generation per service is strictly monotonic across its lifetime | §7.5 |
| P3 | Cap rights never widen during transfer | §7.3 (non-escalating) |
| P4 | ∑ current_task_alloc_bytes ≡ pages mapped, after any sequence of alloc/free | §10.3 |
| P5 | Every live endpoint has exactly one owning task | §8.3 |
| P6 | Queue head ≤ tail ≤ head + 16; count consistent with both | §8.5 |
| P7 | After unmap + TLB shootdown, the page is unreadable from every core | §10.5 |
| P8 | After restart, name resolves to a task with the same name and higher generation | §14.2 |
| P9 | Generation bump invalidates ALL holders, not just some | §7.5 |
| P10 | Every send returns exactly one of {Ok, defined error} - never both, never neither | §8.6 |
Bar: any property failure is a logic bug. Kernel must be fixed before any other work proceeds.
Fuzz Tests
Fuzz tests find the inputs that crash the kernel that no one would write by hand. The bar is binary and absolute: the kernel must never panic on user-controllable input.
| ID | Surface | Generator |
|---|---|---|
| F1 | Syscall args (each × 1M iters) | Random u64 in a0/a1/a2; including kernel addresses, unmapped pointers, misaligned values |
| F2 | Syscall numbers | Random u64 as nr; must return UnknownSyscall, never crash |
| F3 | ELF binaries | Bit-flip mutations of known-good ELFs handed to the spawner |
| F4 | Service contracts | Malformed TOML; JSON Schema-invalid structures |
| F5 | IPC message bodies | Random bytes, random sizes up to 4 KiB |
| F6 | Embedded caps in messages | Messages claiming to carry caps with random structure |
| F7 | Cap generation field | Random u64 as generation in cap usage; must return CapRevoked or EndpointDead |
| F8 | Memory request values | Random sizes including > total RAM, 0, and u64::MAX |
Any panic discovered by F1-F8 is a kernel bug. The fix is mandatory and includes a regression test added to the relevant identity or property suite.
Stress Tests
Stress tests find the bugs that only appear under sustained load. Identity tests prove correctness for individual operations; stress tests prove the system does not drift, leak, or corrupt over hours of operation.
| ID | Scenario | Duration |
|---|---|---|
| S1 | IPC saturation: sustained try_send on a full queue | 1 hour |
| S2 | Restart storm: 100k kill/respawn cycles of one service | until complete |
| S3 | Cross-core thrash: 4 cores × all-to-all IPC | 10 min |
| S4 | Cap table churn: 100k random create/destroy | until complete |
| S5 | Generation overflow: force counter to wrap, observe wraparound semantics | until wrap + 1k operations |
| S6 | Long-running stability: ping/pong + introspection | 24 hours |
| S7 | Memory pressure: alloc-to-limit + free, 10k cycles | until complete |
| S8 | Idle stability: boot, no workload, observe | 24 hours |
| S9 | Interrupt storm: high-frequency timer + IPI cross-fire | 1 hour |
| S10 | Cascading revocation: kill a service held by many; observe propagation | until propagated |
Bar: at the end of each test, the kernel has not panicked, memory accounting is consistent, all services are in a defined state, and no resource is leaked.
Performance Benchmarks
Performance benchmarks lock in numbers so regressions are detected commit-to-commit. Absolute values matter less than the deltas.
| ID | Metric |
|---|---|
| B1 | IPC same-core round-trip latency: p50, p99, p99.9 |
| B2 | IPC cross-core round-trip latency: p50, p99, p99.9 |
| B3 | Syscall floor: yield round trip |
| B4 | Cap validation cost: one cap + generation check |
| B5 | Spawn cost: supervisor.spawn → service "ready" |
| B6 | Restart cost: kill + spawn |
| B7 | Cap table contention: throughput at 1, 2, 4 cores |
| B8 | Allocator throughput: pages/sec under contention |
| B9 | Message copy cost: 4 KiB upper-bound copy |
| B10 | Scheduler decision cost: time to pick next task |
Results are committed to tests/qemu/perf/baseline.json. Comparison is MANUAL. collect_perf_baseline only WRITES the baseline; the regression_threshold_pct: 10 it emits is an inert field nothing reads, and no workflow runs the perf suite at all (every test workflow is workflow_dispatch-only; the release workflow builds images, it does not benchmark). This said "CI compares each run against baseline and flags regressions >= 10%", which described a gate that has never existed. The §7.8 single global lock will surface most visibly in B7 - record the number now so the v2 sharded/RCU migration has a target.
Adversarial / Red-Team Tests
Adversarial tests verify capability isolation holds under direct attack. The system claims a capability model with no ambient authority; these tests run services that try to break that claim.
| ID | Attack |
|---|---|
| A1 | Service crafts random u64 values and tries to use them as caps |
| A2 | Service brute-forces endpoint IDs across the u32 space |
| A3 | Service attempts to allocate beyond its contract memory limit through every syscall path |
| A4 | Service receives a cap with limited rights and attempts to use rights it lacks |
| A5 | TOCTOU: service races a syscall with revocation of the cap it is about to use |
| A6 | Service tries to fill the cap table to denial-of-service the kernel |
| A7 | Service tries to detect IPC partner identity via timing |
| A8 | Service tries to monopolize a core via a tight loop without yielding |
| A9 | Service tries to spawn another service directly, bypassing the supervisor |
| A10 | Service passes kernel addresses as syscall arguments |
| A11 | Service invokes InspectKernel system queries without an INTROSPECT cap |
| A12 | Service invokes Reboot or PowerOff without the capability |
| A13 | Service invokes AcquireSendCap without the capability |
| A14 | Ring-3 CPU exception (null read, non-canonical read, divide-by-zero) kills the task, not the kernel |
| A15 | A bad user pointer kills the caller, not the kernel |
Bar: every attack returns a defined error. Any attack that succeeds is a security hole; any attack that panics the kernel is a kernel bug. Both are mandatory fixes.
Chaos Tests
Chaos tests verify graceful degradation when something the kernel depends on fails partially. Total failures (kernel panic, TCB death) are covered by §6.2 and Test 1B. Chaos tests cover the between cases.
| ID | Failure injected |
|---|---|
| C1 | One or more APs fail to come up during boot |
| C2 | A service in the boot manifest has a corrupted ELF (non-TCB) |
| C3 | Allocator forced to return AllocFailed at random syscall entry points |
| C4 | Bootloader provides degraded environment (minimal RAM, no framebuffer) |
| C5 | Kernel stack approaches exhaustion under deeply nested syscall |
| C6 | One core's timer interrupt is dropped for an extended period |
| C7 | TLB shootdown IPI delivery is delayed across cores |
Bar: the system either continues correctly with degraded capacity, or panics loudly with a defined reason. Silent corruption is never acceptable. Per invariant 12 (§3): failures are loud, never silent.
22.3 Test Harness
osdev test identity
│
├── build: identity-only supervisor + kernel
├── create disk image, install bootloader
│
└── for each test:
│
├── boot QEMU (-smp N; + -enable-kvm when /dev/kvm available)
├── test service runs scenario
├── harness reads serial console line by line
│
├── expected output matched? ──▶ PASS
├── fail_on string seen? ──▶ FAIL
├── timeout fires? ──▶ FAIL
│
└── 500 ms isolation pause (OS reclaims QEMU pages)
Where these tests actually live (spec -> implementation). The pseudocode in this section pins each
test; the executable form lives in osdev/, not as .rs files under tests/qemu/. The identity cases
(Tests 1-11 and 15, each A/B, plus the interrupt-routing IR1A/IR1B) are data-driven TestSpec entries
in osdev/src/validator.rs, run together by osdev test identity - 24 cases. Tests 12, 13, and 14
are heavier bare-metal scenarios with their own subcommands - osdev test iommu (Test 12),
osdev test fs-restart (Test 13), osdev test file-cap (Test 14) - in osdev/src/main.rs and
osdev/src/shell_test.rs. The per-directory guide tests/qemu/identity/CLAUDE.md maps every spec Test
to its entry, and the other categories (Property, Fuzz, Stress, Perf, Adversarial, Chaos, and their
brutal variants) are TestSpec tables in the same validator.rs.
22.4 Sequencing Note
"Tests before code" is aspirational. You cannot run any test until the kernel boots and IPC works. Honest sequence: write test specs (this section); build minimum kernel + harness; see tests fail for the right reasons; implement until they pass.
A test failing for the wrong reason (compile error, harness bug, missing cap not declared in test contract) is a failure of the test, not the kernel.
22.5 Conventions
- Each test has a positive case (the system permits what it should) and a negative case (the system refuses what it shouldn't).
- Pseudocode is illustrative, not literal Rust.
- Each test names the spec section it pins.
- Multi-core tests run with
-smp 4minimum unless otherwise stated.
Test 1: Bootstrap to Steady State
Pins: §11 (Bootstrap), §6 (TCB).
1.A - Positive: Healthy Multi-Core Boot
test bootstrap_steady_state_positive:
# Phase 5: no init - the kernel spawns the supervisor directly; the supervisor spawns events.
image = build_kernel(boot_manifest=[supervisor, events])
qemu = boot(image, smp=4)
assert serial_contains("supervisor: ready", within=5s)
assert serial_contains("events: ready", within=5s)
assert serial_contains("smp: 4 cores ready", within=5s)
assert kernel_did_not_panic()
1.B - Negative: TCB Failure Panics
test bootstrap_tcb_failure_panics:
# Path C / Phase 5: init is removed, so the KERNEL spawns the supervisor directly. A corrupt
# supervisor ELF fails that spawn → the kernel panics (no init abort, so no "reason:" prefix).
image = build_kernel(boot_manifest=[corrupt_binary("supervisor"), events])
qemu = boot(image, smp=4)
assert serial_contains("KERNEL PANIC", within=5s)
assert serial_contains("supervisor spawn failed")
assert qemu_state == "halted"
assert no_app_services_started()
Test 2: Capability Enforcement
Pins: §3.1 (no ambient authority), §7 (use validation).
2.A - Positive
test cap_enforcement_positive:
s = spawn_test_service(contract="[capabilities] log_write = true")
assert s.invoke(Log("hello")) == Ok
assert log_received("hello")
2.B - Negative
test cap_enforcement_negative:
s = spawn_test_service(contract="[capabilities] # no log_write")
assert s.invoke(Log("hello")) == Err(CapNotHeld)
assert log_did_not_receive("hello")
assert s.is_alive()
Test 3: IPC Send / Receive (Same Core)
Pins: §8 (IPC), §7.4 (SEND right).
3.A - Positive
test ipc_send_recv_positive:
a = spawn(contract="ipc_send=['b'], placement.core=0")
b = spawn(contract="ipc_receive=['b'], placement.core=0")
a.send(target="b", payload="ping")
msg = b.recv()
assert msg.payload == "ping"
3.B - Negative
test ipc_send_without_send_right:
cap_no_send = mint_endpoint_cap(target=b, rights=[])
a.install_cap("b_endpoint", cap_no_send)
assert a.try_send(target="b", payload="ping") == Err(CapInsufficientRights)
assert b.queue_depth() == 0
Test 4: Endpoint Death Semantics
Pins: §8.6 (failure semantics), §14.2 (restart drops endpoints), §8.5 (queue depth = 16).
4.A - Positive: Send-After-Death Returns EndpointDead
test endpoint_death_send_returns_dead:
b = spawn_simple_recv_service()
a = spawn_with_cap_to(b.endpoint)
supervisor.kill(b)
wait_for_revocation()
assert a.try_send(b.endpoint, "after death") == Err(EndpointDead)
4.B - Negative: Blocked Sender Wakes With EndpointDead
The queue depth is 16 (§8.5), so this test fills it deterministically.
test blocked_sender_wakes_on_endpoint_death:
b = spawn(non_consuming_receiver) # never calls recv
a = spawn_with_cap_to(b.endpoint)
for i in 0..16:
a.send("fill", index=i) # fills the 16-deep queue
handle = a.send_async("blocked") # 17th: must block
assert handle.is_pending()
supervisor.kill(b)
wait_for_revocation()
assert handle.poll(timeout=1s) == Err(EndpointDead)
assert a.is_alive()
Test 5: Capability Transfer Requires GRANT
Pins: §7.6 (transfer rule), §7.4 (GRANT right).
5.A - Positive
test grant_positive:
cap = mint_cap(target=resource_X, rights=[READ, GRANT])
sender.install_cap("X", cap)
msg = Message::with_cap(cap)
assert sender.send(receiver.endpoint, msg) == Ok
received = receiver.recv()
assert received.embedded_cap.use(READ) == Ok
assert sender.has_cap("X") == false
5.B - Negative
test grant_negative:
cap = mint_cap(target=resource_X, rights=[READ]) # no GRANT
sender.install_cap("X", cap)
msg = Message::with_cap(cap)
assert sender.send(receiver.endpoint, msg) == Err(CapNotGrantable)
assert sender.has_cap("X") == true
assert receiver.queue_depth() == 0
Test 6: Supervisor Restart and Cap Rebinding
Pins: §14.2 (restart flow), §14.3 (cascading failure).
6.A - Positive
test supervisor_restart_positive:
pong = spawn("pong")
original_pid = pong.pid
supervisor.restart("pong")
wait_for_serial("pong: ready", within=5s)
assert pong.pid != original_pid
assert kernel_did_not_panic()
assert all_other_services_alive()
6.B - Negative
test stale_cap_revoked_after_restart:
ping = spawn("ping")
pong = spawn("pong")
supervisor.restart("pong")
wait_for_serial("pong: ready")
assert ping.send_via_stale_cap("hello") in [Err(CapRevoked), Err(EndpointDead)]
fresh = ping.reacquire_by_name("pong")
assert ping.send_via(fresh, "hello") == Ok
Test 7: Memory Limit Enforcement
Pins: §10.3 (enforcement), §10.4 (two failure modes).
7.A - Positive
test memory_alloc_within_limit:
s = spawn(contract="memory.limit = 64MiB")
assert s.alloc(32 * MiB) == Ok
assert s.alloc(20 * MiB) == Ok
assert s.is_alive()
7.B - Negative (Two Modes)
test memory_alloc_beyond_limit_recoverable:
s = spawn(contract="memory.limit = 64MiB")
s.alloc(60 * MiB)
assert s.alloc(20 * MiB) == Err(AllocDenied)
assert s.is_alive()
assert s.alloc(2 * MiB) == Ok
test memory_protection_violation_kills_service:
s = spawn(contract="memory.limit = 64MiB")
s.alloc(32 * MiB)
s.write_to_unmapped_address(0xdead_0000)
wait_for_kill(within=1s)
assert s.is_dead()
assert kernel_did_not_panic()
Test 8: Preemption of Non-Yielding Service
Pins: §3.6 (no service can monopolize), §9.1 (10 ms quantum), §9.3 (yield is advisory).
8.A - Positive
test yield_advisory_works:
yielder = spawn_yielding_service(core=0)
other = spawn_logging_service(core=0)
run_for(1s)
assert other.log_count >= 90
assert yielder.tick_count >= 50
8.B - Negative
test non_yielding_service_is_preempted:
hog = spawn_tight_loop_service(core=0)
other = spawn_logging_service(core=0)
run_for(1s)
assert other.log_count >= 1 # minimum bar
assert other.log_count >= 40 # near fair share
assert hog.is_alive()
assert kernel_did_not_panic()
Test 9: Cross-Core IPC
Pins: §8.3 (routing), §8.4 (send flow), §9 (per-core scheduler).
9.A - Positive
test cross_core_ipc_positive:
a = spawn(contract="ipc_send=['b'], placement.core=0")
b = spawn(contract="ipc_receive=['b'], placement.core=1")
assert a.assigned_core == 0
assert b.assigned_core == 1
a.send(target="b", payload="hello from core 0")
msg = b.recv()
assert msg.payload == "hello from core 0"
9.B - Negative
test cross_core_no_authority_leak:
a = spawn(contract="placement.core=0") # no caps to b
b = spawn(contract="ipc_receive=['b'], placement.core=1")
fake_cap = a.try_construct_cap(target=b.endpoint, rights=[SEND])
assert fake_cap == Err(CapForgeryAttempted)
assert b.queue_depth() == 0
Test 10: Restart With Core Reassignment
Pins: §9.2 (placement, strict), §14.2 (restart can change core), §14.4 (placement override), §11 (identity stable; location not).
10.A - Positive
test restart_changes_core_transparently:
pong = spawn(contract="placement.core=1")
assert pong.assigned_core == 1
pong_gen_old = pong.generation
supervisor.restart("pong", placement_override=2)
wait_for_serial("pong: ready on core 2", within=5s)
assert pong.assigned_core == 2
assert pong.generation > pong_gen_old
10.B - Negative
test client_reacquires_after_core_change:
ping = spawn(contract="placement.core=0")
pong = spawn(contract="placement.core=1")
supervisor.restart("pong", placement_override=2)
wait_for_serial("pong: ready on core 2")
assert ping.send_via_stale_cap("hello") == Err(EndpointDead)
fresh = ping.reacquire_by_name("pong")
assert fresh.target_core == 2
assert ping.send_via(fresh, "hello") == Ok
assert pong.received("hello")
Test 11: Name Resolves After Restart, via the Kernel Directory (Path C / Phase 4)
Pins: §6.1/§6.2 (a restartable service's death is a supervisor restart, not a panic), §14 (supervisor restart authority), §3.11 (identity over location), §4.4/§26.10 (naming = the kernel's minimal recovery directory, not a service).
Amendment 2026-06-21 (naming Phase 4): the registry service is retired (
docs/naming-design.md§3.7, "Path C"). Name→endpoint resolution is a minimal directory inside the kernel (ipc::names
- the gated
AcquireSendCap); the supervisor wires services from aname → capmap and clients reacquire names via the directory. There is no registry service to kill. This test was "registry survives its own restart" (H11); it now pins the directory's restart property - a restartable service killed and respawned must re-establish without a kernel panic, and its name must resolve to the new instance (the directory re-records it on respawn).block-driveris the disk-free restartable target (it idles with no disk in the identity build).
test name_resolves_after_restart_via_directory:
wait_for_serial("supervisor: ready")
control.kill("block-driver") # a restartable service (Phase D)
assert serial_contains("supervisor: block-driver died, restarting")
assert serial_contains("supervisor: block-driver restarted")
assert serial_contains("name-map + block-driver") # re-recorded → directory resolves the new instance
assert kernel_did_not_panic()
# Clients reacquire "block-driver" by name via the kernel directory (§14.3) - pinned end-to-end
# for fs←block-driver and shell←fs by the files-test double-storm regression.
Test 12: Confined Driver Cannot DMA Outside Its Arena (H1)
Pins: §3.1 / invariant 1 (no ambient authority - the DMA gap), §6.4 (DMA-capable drivers are least-privilege when IOMMU-confined), §12 (drivers).
The point of H1: a confined DMA-capable driver's device can reach only its granted
arena. A DMA outside it must be blocked at the IOMMU (a logged IO_PAGE_FAULT on
real hardware), never silently read/write other memory. This is the executable form of
the §6.4 trust claim - without it, "confined" is a word, not a guarantee.
Runs only where an IOMMU is present (osdev test iommu launches QEMU with
-device amd-iommu); on a machine with no IVRS the driver is trusted (§6.4) and the
test is not applicable.
Verification is structural, not a live fault, and the reason is a QEMU limitation.
QEMU's emulated amd-iommu installs the device tables and page tables but does not
enforce translation faults on unmapped I/O addresses - a device DMA to an unmapped page
is silently allowed through. So a live IO_PAGE_FAULT cannot be observed under QEMU.
The harness therefore asserts the property QEMU can be made to prove: the kernel's
confinement selftest - a CPU-side walk of the device's I/O page table - confirms the
arena translates identity and the page one past it is unmapped (so a DMA there has no
translation and would fault on conforming silicon). That selftest is exactly the
structure an IO_PAGE_FAULT is raised from; pinning it pins the guarantee. (The live
fault itself is hardware-verified on the T630 and reproducible anywhere via the
iommu-fault-test build feature, which confines the driver to an empty domain so its
normal init DMA lands out-of-arena.)
test confined_driver_dma_faults: # osdev test iommu
boot(smp=2, iommu=on) # q35 + amd-iommu + qemu-xhci + usb-kbd
assert serial_contains("iommu: ... confined BDF") # driver is confined to its arena
# The kernel's confinement selftest walks the device's I/O page table: the arena
# maps identity, and the page one past arena_end has NO mapping - the structural
# form of "out-of-arena DMA would fault" (QEMU can't raise the fault itself).
assert serial_contains("iommu: selftest PASS")
assert serial_contains("(outside) unmapped")
assert serial_contains("keyboard found") # driver still operates THROUGH the domain
assert kernel_did_not_panic() # confinement is not fatal to a well-behaved driver
# Live-fault form (hardware / `--features iommu-fault-test`, not QEMU's lenient model):
# confine the driver to an EMPTY domain → its first init DMA is out-of-arena →
# IOMMU raises IO_PAGE_FAULT, kernel logs it, memory outside the arena is unchanged.
Test 13: Filesystem Survives Its Own Restart (Phase D)
Pins: §6.1/§6.2 (fs + block-driver are restartable, not trusted root), §6.3 (TCB-shrink
goal reached), §15 (transactional recovery), §14 (supervisor restart authority), §3.11.
fs and block-driver are restartable userspace services (Phase D amendment 2026-06-17), made
safe by fs's crash-consistent recovery (Phase C). Killing fs must NOT panic the kernel; the
supervisor must observe its death and respawn it; fs must re-mount to a consistent state
(persisted data intact) and re-register; and a client must reacquire it by name and
keep working.
test fs_survives_own_restart: # osdev test fs-restart
boot(bare-metal + AHCI disk; shell on COM1, control on COM2)
shell("drives flash data" → y) # format
shell("write /t.txt survives-restart")
assert shell("read /t.txt") contains "survives-restart"
control.kill("fs") # was a panic+reboot pre-Phase-D
assert serial_contains("supervisor: fs died, restarting")
assert serial_contains("supervisor: fs restarted")
assert serial_contains("fs: serving file API") # re-mounted + re-registered
# The shell reacquires a fresh fs cap by name via the kernel directory (§14.3); the file persisted.
assert shell("read /t.txt") contains "survives-restart"
assert kernel_did_not_panic()
Test 14: File Is a Capability (P2)
Pins: §7.3 (cap properties), §7.10 (delegated resource capabilities), §3.1 (no ambient authority), §3.3 (authority by capability, not identity).
The P2 amendment (2026-06-18) makes a file a real, kernel-minted capability via delegated resource caps. This test pins that the file cap is a genuine capability - not a service-level token - by exercising the three properties that distinguish one: unforgeable, revocable, non-escalating.
test file_is_a_capability:
# fs hands out a real cap on open (delegated resource cap, §7.10)
rw = fs.open("/doc.txt", rights=[READ, WRITE]) # returns a file capability
assert rw.write("hello") == Ok
assert rw.read() == "hello"
# Unforgeable (§7.3): a fabricated handle is not a cap
assert use_random_handle_as_file_cap() in [Err(CapNotHeld), Err(CapInvalid)]
# Non-escalating (§7.3): a READ-only file cap cannot write
ro = fs.open("/doc.txt", rights=[READ])
assert ro.read() == "hello"
assert ro.write("nope") == Err(CapInsufficientRights)
# Revocable (§7.5/§7.10): deleting the file revokes every cap to it
fs.delete("/doc.txt") # fs revokes the resource (gen bump)
assert rw.read() == Err(CapRevoked)
assert ro.read() == Err(CapRevoked)
assert kernel_did_not_panic()
Implemented (2026-06-18) as osdev test file-cap (9/9 ✅). The shell fcap <file> command opens a
file as a real kernel capability and exercises every property above end-to-end: read/write through
the cap; non-escalation at both layers (the kernel rejects a READ-only cap's WRITE invocation with
CapInsufficientRights, and fs refuses a write op carried under a read-validated badge - op ≤ right);
a fabricated handle is rejected (unforgeable); and the cap is CapRevoked after close/delete (revocable).
The badge that carries the validated (resource_id, right) to fs is an unforgeable kernel-set Message
field (LastRecvBadge syscall) - a client cannot fake a file-cap invocation over its ordinary fs send cap.
Test 15: Supervisor Survives Its Own Restart (Path C / Phase 6)
Pins: §6.2 (the supervisor is restartable - its death is a kernel respawn, not a reboot), §6.3
(TCB-shrink reached its floor: unkillable = {kernel}), §3.7/§4.4 (the kernel is the recovery
anchor), §14 (restart authority), §3.11 (identity over location).
Amendment 2026-06-21 (Path C / Phase 6): the supervisor is restartable. Killing it (a fault, or a deliberate
chaos kill-storm supervisor/ the operator control channel) must not panic the kernel. The kernel respawns it - unconditionally, forever (no bound: a bound would re-introduce the reboot and be a DoS, §6.2) - and the respawned supervisor reconciles: it adopts the still-running services (reacquiring each by name from the kernel directory) instead of duplicating them. The running services (pong/ping cross-core IPC, the shell) keep going throughout - the shell survives killing its own spawner. This is the executable proof that the unkillable set is{kernel}alone.
test supervisor_survives_own_restart: # osdev test identity (also: chaos kill-storm supervisor)
wait_for_serial("supervisor: ready")
control.kill("supervisor") # was a kernel panic pre-Phase-6 (it was trusted root)
assert serial_contains("kernel: supervisor died - respawning") # the kernel is the recovery anchor
assert serial_contains("supervisor: adopted running block-driver") # reconciled, not duplicated
assert kernel_did_not_panic()
# The shell-test storms it 4× (chaos kill-storm supervisor 4 → recovered 4/4, kernel alive, no
# bound) and the prompt still answers afterward - the system stayed up across every respawn.
22.6 Test Coverage Matrix
| Test | Spec sections pinned | Constitutional invariant |
|---|---|---|
| 1. Bootstrap | §11, §6 | TCB integrity |
| 2. Capability enforcement | §3.1, §7 | No ambient authority |
| 3. IPC send/receive (same core) | §8, §7.4 | Authority is explicit |
| 4. Endpoint death | §8.5, §8.6, §14.2 | Restartability |
| 5. Capability transfer | §7.6, §7.4 | Authority is explicit |
| 6. Supervisor restart | §14.2, §14.3 | Restartability |
| 7. Memory limits | §10.3, §10.4 | Isolation |
| 8. Preemption | §3.6, §9.1, §9.3 | No service monopoly |
| 9. Cross-core IPC | §8.3, §8.4, §9 | Identity over location |
| 10. Restart with core change | §9.2, §14.2, §14.4, §11 | Identity over location |
| 11. Name resolves after restart (directory) | §6.1, §6.2, §14, §3.11, §4.4 | Restartability / naming-out-of-kernel |
| 12. Confined driver DMA faults | §3.1, §6.4, §12 | No ambient authority (DMA) |
| 13. fs survives own restart | §6.1, §6.2, §6.3, §15, §14 | Restartability / TCB shrink |
| 14. File is a capability | §7.3, §7.10, §3.1, §3.3 | Authority is explicit (files) |
| 15. Supervisor survives own restart | §6.2, §6.3, §3.7, §14, §3.11 | Restartability / unkillable = {kernel} |
If any cell becomes obsolete, the corresponding spec section is being changed and the change requires a CLAUDE.md amendment.
22.7 The Stranger Test - is the PUBLIC interface doing the teaching?
Every test above this line asks whether the kernel is correct. This one asks whether the system can be USED, and it is the only test here whose subject is the developer rather than the machine.
The bar: give the least capable model available a fresh context, the PUBLIC developer documentation only, and one ordinary application requirement. No architectural coaching. If it produces a correct Godspeed program under those conditions, the public interface is doing a substantial amount of the teaching. If it can only succeed after someone explains MISCIS, the interface is not finished, whatever the kernel does.
Why the weakest model rather than the best. A sophisticated model can infer the architecture from the source and would pass by being clever, which measures the model. A weak one cannot, so what it produces measures the DOCUMENTATION AND THE API. The point is not to find out whether Godspeed can be understood; it is to find out whether it has to be understood before it can be used.
Let the repository teach, and do not grade on a curve. The temptation is to explain the rules and
then be pleased when they are followed. The rules are already mechanised, so the test is whether the
gates catch a stranger's mistakes and whether the resulting error says enough to recover from:
#![deny(unsafe_code)] refuses unsafe at the compiler, arch_boundary_check refuses an
ISA-conditional workaround, commandments.py refuses ambient authority and an unrecoverable peer,
and Error::retry_is_safe answers the one question a stranger is most likely to get wrong. A gate
that fires with an unhelpful message is a finding, not a pass.
It is the inversion of the grokability probe in audits/documentation-audit.md, which asks
whether a weak model can REGENERATE a document. That one tests whether Godspeed can be understood;
this one tests whether it can be used without being understood. Both use the same instrument and
neither substitutes for the other.
This is not an identity test and does not pretend to be. It has no pass/fail assertion, cannot
be run in CI, and failing it does not mean the system stopped being the system §22.1 describes. It
means v1's stated intent - "Godspeed is simple to program for because its own architecture has a
small, coherent and honest developer interface" - is not yet met. It is recorded here rather than in
docs/ alone because that intent is a commitment, and a commitment nobody measures is a preference.
The correct path must be easier than cheating. That is the whole design rule this test exists to check, and the honest form of the success condition: a stranger should fall into the supported model because it is the path of least resistance, not because they were told to.
docs/stranger-test.md has the protocol, what to measure, and the difficulty ladder.
23. First Milestone ✅ Complete
23.1 Goal
Boot the OS multi-core.
Start two services (ping on core 0, pong on core 1).
Send a message between them via cross-core IPC.
Kill pong.
The supervisor restarts it (possibly on a different core).
The system continues running.
23.2 Acceptance Criteria ✅
osdev run --smp 4boots the OS with 4 cores; supervisor, events, ping, and pong reach steady state. ✅ (As recorded in 2026-05 this read "init, supervisor, registry, logger";initwas removed in Phase 5, theregistryservice retired in Phase 4, andloggerrenamedeventsin 2026-09.)- ping placed on core 0; pong placed on core 1. ✅
osdev logs pingshows ping sending a message every second. ✅osdev logs pongshows pong receiving each message (cross-core IPC). ✅osdev restart pong --core 2kills pong on core 1 and respawns it on core 2. ✅- ping observes
EndpointDeadand reacquires by name; the new cap routes to core 2. ✅ - After reacquisition, ping and pong continue communicating across the new core boundary. ✅
- The kernel does not panic on any core. ✅
- All identity tests in §22 pass. ✅ (ten at the time; fifteen tests / 24 cases today.)
23.3 Bare-Metal Achievement ✅
GodspeedOS has booted on real x86_64 hardware (4-core CPU, 4 GB RAM) via UEFI USB boot (2026-05-21).
osdev imageproduces a UEFI GPT disk image atbuild/os-usb.img. (This saidbuild/os.img, which is the QEMU/BIOS image -osdev/src/disk_image.rsnotes the two are named apart on purpose, and §17 has it right.)- Image written to USB with Cygwin
dd; boots viaBOOTX64.EFI(Limine 12.x). - All 4 cores come up; cross-core IPC (ping core 0 → pong core 1) runs continuously on hardware.
- Null modem serial (115200 8N1, PuTTY) confirms boot output; log appended to
build/putty_serial_output.log. bare-metalsupervisor feature excludes harness-driven probe services that require QEMU's control port.
Persistence + file-as-capability hardware-proven on the HP T630 (2026-06-18). Booted the bare-metal
os.img on the T630 (AMD GX-420GI, real AHCI SSD) and ran the shell selfcheck suite: ran 163, failed 0. That run includes the full persistence stack (GSFS0008 format, journal, fsck/drives check,
read-only drives scrub) and the file-as-capability self-check (fcap, §22 Test 14): a file opened
as a real kernel capability, read/written through the cap, non-escalation enforced at both the kernel
and fs layers, a forged handle rejected, and the cap revoked on close and on rename - all green on real
hardware, no panic. The §7 "north star" (a file is a capability, true not approximate) is hardware-
validated, not just QEMU. Serial in build/putty_serial_output.log.
Hardware performance data (perf-brutal-only build, ~3 GHz CPU, 2026-05-21):
| Benchmark | Result |
|---|---|
| BP1 IPC same-core p50 | 55,320 cycles (~18.4 µs) |
| BP3 yield floor | 39,903 cycles (~13.3 µs) |
| BP4 cap validation | 495 cycles (~165 ns) |
| BP5 spawn cost | 8,121,378 cycles (~2.7 ms) |
| BP6 restart cost | 14,462,309 cycles (~4.8 ms) |
| BP7 cap table | 1,168 cycles (~389 ns) |
| BP8 allocator | 616 cycles/4KiB page (~205 ns) |
| BP9 message copy 4KiB | 20,073 cycles (~6.7 µs) |
| BP10 scheduler decision | 2,323 cycles (~774 ns) |
| BP2 IPC cross-core | Not measured on J5005 (Goldmont+ stalled cross-core under load) - measured on the T630, see table below |
HP T630 (AMD GX-420GI, Jaguar/Puma+, ~2 GHz) - per-probe isolated measurements
(one benchmark alone: no ping/pong, no competing probes; 2026-05-31, build ed8a151).
µs/ms at ~2 GHz:
| Benchmark | T630 isolated | J5005 (above, perf-brutal) |
|---|---|---|
| BP1 IPC same-core p50 | ~102,600 cycles (~51 µs) † | 55,320 |
| BP2 IPC cross-core p50 | 1,433,087 cycles (~0.72 ms); p99/p999 16,409,799 | not measured |
| BP3 yield floor | 19,281 cycles (~9.6 µs) | 39,903 |
| BP4 cap validation | ~1,258 cycles (~0.63 µs) † | 495 |
| BP5 spawn cost | 45,406,292 cycles (~22.7 ms) | 8,121,378 |
| BP6 restart cost | 54,231,139 cycles (~27.1 ms) | 14,462,309 |
| BP7 cap table | 2,932 cycles (~1.5 µs) | 1,168 |
| BP8 allocator | ~1,472 cycles/4KiB (~0.74 µs) † | 616 |
| BP9 message copy 4KiB | 21,796 cycles (~10.9 µs) | 20,073 |
| BP10 scheduler decision | 20,726 cycles (~10.4 µs) | 2,323 |
All cycle counts. † = perf-brutal in-suite p50 (already low-variance); the rest are
single-probe isolation builds (osdev image --mode iso-bp{3,5,7,9,10}; bp5 covers BP5+BP6).
The two columns are not a clean head-to-head: J5005 was perf-brutal (contended), the T630
column is isolated (uncontended), so they compare fairly only where both were clean -
BP1/BP4/BP8 at ~1.9-2.5×, genuine Jaguar-vs-Goldmont IPC. Where the T630 number is lower
(BP3) the J5005 figure was itself contention-inflated. BP5/BP6 (spawn/restart) are
memory-bandwidth-bound - the low-power thin client lags most there. The full investigation
behind BP2 (the COM2 timer-ISR wedge, fixed a306fd3) is in bugs/1_FINDINGS_AP_TO_BSP_IPI.md.
23.4 Out of Scope for v1
Filesystem persistence beyond the trusted block driver, network stack, work-stealing scheduler, service migration, zero-copy IPC, live code updates, restartable block driver / fs, update model in production mode, core hotplug, per-endpoint queue depth in contract.
24. Glossary
- AP - Application Processor. Any core other than the BSP.
- BSP - Bootstrap Processor. The first core to execute kernel code.
- Call - The synchronous request/reply IPC syscall (§8.2, syscall 41): send a request carrying a one-shot reply cap, then block awaiting the reply; wakes with the reply or with
ReplyDeadif the replier dies first, so it never hangs. Mechanism, not policy - the kernel learns a reply cap, not "RPC". The primitive behind the SDKrequest_with_reply. - Capability - Unforgeable token: ResourceId + Rights + Generation.
- Delegated resource capability - A capability for a resource whose meaning is defined by a service (e.g. a file owned by
fs), not the kernel. The owning service mints and revokes it (resource_mint/resource_revoke, gated by aRESOURCE_MINTcap); the kernel validates and routes it as for any cap, badging a send with the opaqueResourceIdso the owner knows which resource. The mechanism behind file-as-capability (§7.10, P2). - Endpoint - IPC destination owned by a service. Bounded queue, depth 16 in v1.
- Generation - Monotonic counter on resources; mismatch on cap use indicates the resource was destroyed or replaced.
- Grant - The right to transfer a capability via IPC.
- Identity test - A test that pins a constitutional decision (§22).
- IPI - Inter-Processor Interrupt. Mechanism for a core to wake another core.
- Limine - The bootloader used in v1. See Appendix A.
- Placement - Strict assignment of a service to a specific core at spawn time. Re-evaluated from scratch on every spawn, including post-restart spawns; the previous core is not remembered.
- PlacementInvalid - Error returned when a contracted core is unavailable; spawn rejected, supervisor logs and skips.
- Quantum - The 10 ms time slice after which the per-core scheduler preempts.
- Reply cap - A one-shot capability to the caller's own endpoint, sent inside a
Callrequest so the replier can reply to it. The kernel tracks, per blocked caller, the target endpoint it awaits; if that endpoint dies, the caller is woken withReplyDead. The reply-side twin of the blocked-sender record (§8.2, §8.6). - ReplyDead - Error returned when the replier's endpoint dies while the caller is blocked in a
Callawaiting its reply (value -12; §7.7, §8.6). The reply-side twin ofEndpointDead, on the same generation/liveness mechanism. - Routing table - Kernel structure mapping
EndpointId → (CoreId, Generation, Liveness). - TCB - Trusted Computing Base. Kernel + arch + smp + supervisor. (Not
init- it was removed in Path C / Phase 5; the kernel spawns the supervisor directly. And the supervisor is trusted but RESTARTABLE, Phase 6, so the only unkillable component is the kernel.)registryleft the TCB via H11 (and the registry service was then retired entirely - naming Phase 4 / Path C,docs/naming-design.md§3.7);block-driver+fsleft via the Phase D amendment (§6.1, oncefsgained crash-consistent recovery). DMA drivers (xhci/ehci, and ARM'sdwc2) are in the TCB only on a machine without an IOMMU to confine them (§6.4); all three are userspace services now. - Trusted root -
supervisor(sole;initwas removed in Path C / Phase 5 - the kernel spawns the supervisor directly). It is trusted but restartable (Path C / Phase 6, §6.2): the kernel respawns it on death - unconditionally, forever - so its failure is recovered, not a reboot. The only unkillable component is the kernel itself. (block-driver+fsare restartable storage services.) - Name directory - the kernel's minimal
name → EndpointIdmap (ipc::names) + a gated "mint a SEND cap by name" (AcquireSendCap). The bounded recovery anchor that replaced the registry service (naming Phase 4 / Path C, §3.7): the supervisor wires services from aname → capmap and clients reacquire names through the directory. (The retiredregistryservice's design note was deleted with the service;docs/naming-design.md§3.7 is the record.) - Service - Userspace component with a contract, capability table, and isolated address space.
- Contract - a service's
contracts/<name>.toml(e.g.examples/ping/contracts/ping.toml) declaring resource, capability, and placement requirements. - Supervisor - User-space service holding restart authority over other services.
osdev- Host-side CLI for building, publishing, and controlling the OS in QEMU.
25. Final Principles
Undefined behavior in spec becomes bugs in system.
If it violates the model, it does not belong.
If an identity test fails, the system is no longer this system.
Identity is stable. Location is not. Movement is invisible. Death is visible.
Failures are loud, never silent.
A failing Godspeed that preserves its invariants is preferable to a working Godspeed that violates them.
The last one ranks the others. Every principle above can be traded against a deadline, a benchmark or a stubborn bug, and this says which way that trade goes: a system that fails while keeping its model intact is still this system, and can be fixed. A system that works by breaking its model is a different system that happens to run today, and what it has really lost is the reason to trust any of the rest of this document.
This is not a preference for failure. It is a statement about what a fix is: making the system work WITHIN the model, and never widening the model to admit what is easier. Where the two genuinely cannot be reconciled, the honest move is to record the gap loudly and leave it open (§26.7) rather than close it with a violation.
Appendix A: Bootloader Choice (Limine)
Status: v1 commitment. This appendix documents and justifies a concrete decision; it is part of the v1 spec, not aspirational.
A.1 Decision
The v1 bootloader is Limine, accessed by the kernel via the Limine Boot Protocol.
A.2 What Limine Provides to the Kernel
At handoff, Limine supplies the kernel with:
- Physical memory map - usable, reserved, ACPI, framebuffer regions all classified.
- Framebuffer descriptor - base address, dimensions, pixel format. Avoids ever needing VGA text mode.
- Kernel relocation info - physical and virtual base addresses of where the kernel was loaded.
- SMP topology - APIC IDs of all available processors, used by
kernel/smpandarch/x86_64/ap_boot.rs. This removes the need to probe ACPI/MADT in v1. - Higher-half direct map - physical memory pre-mapped at a known high-half virtual address, available immediately.
- Boot-time module list - ability to load additional binaries (e.g., the initial service manifest) alongside the kernel.
A.3 Why Limine for v1
| Reason | Detail |
|---|---|
| Tight Rust integration | The limine crate (crates.io) provides type-safe bindings to the boot protocol. Request structures are declared as Rust statics; responses are read back with strong typing. No hand-rolled parsing of bootloader-supplied tables. |
| SMP topology supplied | APIC IDs come pre-discovered. arch/x86_64/ap_boot.rs does not need an ACPI parser to enumerate cores. |
| BIOS + UEFI from one bootloader | Limine supports both firmware modes with the same protocol. The kernel does not need to care which firmware booted it. |
| Good QEMU support | Critical for osdev run (§17). The whole identity test suite runs under QEMU; the bootloader must work there reliably. |
| Active maintenance | Limine is currently maintained and the protocol is stable but evolving. Pin a specific protocol version in Cargo.toml and treat updates as deliberate. |
A.4 Installation Story
GodspeedOS ships with Limine. Users do not install or pre-install Limine separately.
UEFI systems:
- The OS image places
BOOTX64.EFI(the Limine UEFI loader) at/EFI/BOOT/BOOTX64.EFIon the EFI System Partition. - The kernel binary is placed where
limine.confreferences it. - Firmware →
BOOTX64.EFI→ Limine → kernel.
BIOS systems:
- The installer runs
limine bios-installto write Limine's stage-1 to the MBR (or VBR). - Stages 2 and 3 of Limine live on disk alongside the kernel; loaded by the stage-1.
- Firmware → MBR → Limine → kernel.
In both cases the Limine binaries are part of the OS image. The end user installs the OS; Limine arrives with it.
A.5 Dual-Boot Support
Out of scope for v1. If pursued later, Limine supports chainloading other bootloaders, which is the cleanest path. v1 assumes a dedicated machine or VM.
A.6 Alternatives Considered
| Option | Why Not |
|---|---|
| GRUB / Multiboot2 | Older protocol, clunkier Rust integration, no built-in SMP topology surface, much larger surface area to depend on. |
| Custom bootloader | A project unto itself. Distracts from the actual goal (a capability microkernel). |
| Bootboot, stivale (predecessor to Limine) | Stivale is deprecated in favor of Limine Boot Protocol. Bootboot is reasonable but has a smaller community and worse Rust tooling than Limine today. |
A.7 Implementation Notes
- The integration code lives in
kernel/src/arch/x86_64/boot.rs. - The Limine protocol version used is pinned in the workspace
Cargo.toml. Protocol version bumps are PR-reviewed. - The boot handoff (Limine to kernel main) is §11 itself. A separate
docs/bootstrap.mdwas listed here and in §5 but was never written; §11 is the walkthrough, and pointing at it is both truthful and shorter than writing a second file to repeat it.
Appendix B: Userspace Posture
Status: Non-normative. Records the v1 stance on userspace languages and the design intent for early services. Does not amend the constitution.
B.1 Primary Language: Rust
All v1 userspace services are written in Rust against sdk/rust/.
Reasons:
- The kernel is Rust; sharing a toolchain dramatically simplifies the build and CI pipeline.
- Capability handles in
sdk/rust/capability.rsare typed Rust structures. C or other-language equivalents would need parallel SDKs. - Contract validation in
osdevis Rust; reusing the same JSON Schema crate end-to-end avoids drift. - Borrow-check discipline meshes naturally with the no-shared-mutable-state invariant.
B.2 Other Languages
The syscall ABI follows System V AMD64. Any language that can produce a freestanding ELF binary and call via that ABI can run as a service.
Plausible second-fits:
- C - would need a
sdk/c/of thin syscall wrappers. Capability handles become opaque integers; the type-safety of the Rust SDK is lost. - Zig - bare-metal-capable, no runtime, comparable ergonomics to C with better safety. A
sdk/zig/is a future possibility.
Out of scope:
- Languages with substantial runtimes (Go, Python, JavaScript, Java) - would require porting their runtime as a GodspeedOS service. Each is a multi-month project on its own.
B.3 Shell ≠ Unix Shell
The traditional Unix shell relies on fork, exec, file-descriptor inheritance, ambient stdin/stdout/stderr, environment-variable inheritance, and anonymous pipe sharing. None of those primitives exist in GodspeedOS.
A "shell" in this system is a capability-broker service. It:
- Holds a capability to a console service (keyboard input + display output).
- Holds the authority to ask the supervisor to spawn other services (via a cap to invoke
supervisor.spawn). - Reads commands and constructs spawn requests, including the explicit caps each child should receive.
This means there is no stdin, only an IPC endpoint to a console service. There is no fork, only an authenticated request to the supervisor. There is no inherited environment, only the caps the parent explicitly granted.
Note (2026-08-17): a
consoleservice now exists, and it owns OUTPUT only. This appendix anticipated one service holding "keyboard input + display output"; what was built holds the display - the terminal model, the grid, the cursor and the rendering (docs/console-service.md§9). Keyboard INPUT is still brokered by the shell through the kernel's single-reader console ring, for the reason recorded indocs/console-service.md§5a: there is one input ring and one reader slot, so a service that owned the keyboard would block inConsoleReadand could not also field take/release messages. The split is deliberate, not partial. This appendix stays non-normative; it is the intent, and the difference is recorded here rather than left to read as a description of what shipped.
The full mechanics of how Unix-style scripting maps onto this model - pipes as capability-mediated endpoints, redirection as cap minting, etc. - are explored in Appendix D.
B.4 Open Question for Later
When real userspace work begins, the first user-facing design decision is how Unix-flavored the interface should feel - Genode-style superficial familiarity (the Unix word works, even though it is a capability-bearing service) versus a fully fresh vocabulary. Either is defensible. Picking deliberately matters because retrofitting later is painful.
Answered 2026-09-23, and by a third option neither of those two is. The vocabulary is fresh -
dir,read,delete,copy,match,count- and the shell keeps a table of the Unix and DOS words (FOREIGN_HINTS) purely so that typing the reflex tells you the Godspeed word. It is a HINT and never an alias:lsdoes not run, it answerstry \dir``. So familiarity is spent on DISCOVERY rather than on compatibility, and nobody ends up writing scripts against a second set of names that has to be supported forever.Recorded here because this appendix is where the question was posed, and an open question that has been answered is worse than one that never was - the next reader takes it as still open. The mechanism is in
services/shell;scripts/foreign_word_check.pyreads that same table to make sure no document in this repository shows one of those words being used as a command, which is how thels->dirrename was found to have missed ten worked examples.Note 2026-10-13: two Unix words are commands,
cdandpwd, and each has a reason.cdwas kept from the start because it is universal (utilities/17_cd.md).pwdjoined it with the filesystem layout (docs/filesystem-layout.md6): the prompt is a plaingsh>, so something has to say where you are, andpwdiscd's other half - anyone who knows one knows the other. It leftFOREIGN_HINTS, where its hint had beencd ., which asked a reader to know a Unix convention (.) without naming anything. The rule above is unchanged: every other foreign word is still a hint and never an alias, and a new exception needs a reason of its own written beside it, as this one is.Note 2026-10-14: and a third,
shutdown, with its reason. It is the word Linux, Windows and macOS share, and it names the ACT - ending the session - rather than promising a mechanism: on the T630, the Pis and the VisionFive the machine halts without losing power, sopoweroffwould claim what does not happen (docs/shutdown.md). It leftFOREIGN_HINTS, where its hint had beenreboot- wrong advice, sincerebootturns nothing off - andhaltandpoweroffstay hints that answershutdown.
Appendix C: Forward-Looking Vision (Non-Normative)
Status: Non-normative. Records design intent for post-v1 directions. Items may be deferred indefinitely, redesigned, or rejected when their time comes. This appendix does not amend the constitution.
C.1 observe - Native Top/Htop Equivalent
Tentative timeline: v2 candidate.
A native introspection tool, distinct from any third-party utility, that surfaces what the system is doing.
The architecture makes this easier than the equivalent on Unix. Per-service state is already structured: caps held, assigned core, memory request/limit, current allocation, IPC queue depths, generation, liveness. The supervisor already knows about every service. The kernel already tracks per-task state.
observe would be a service holding capabilities to query the supervisor and a kernel-provided introspection endpoint, formatting the result for display. There is no need to parse a /proc-style text interface - the data is already structured.
C.2 Native Metrics Emission
Tentative timeline: v2 / v3 candidate.
The system should emit metrics by default, without requiring third-party agents.
Architectural intent: the kernel emits structured events (IPC volume, cap denials, scheduler statistics, restart events) on a known endpoint. This is a publication, not a feature baked into kernel logic - the kernel does not know what format consumers want. A separate metrics service holds the consuming capability and exports in whatever format is appropriate (Prometheus exposition, OpenTelemetry, statsd, custom).
Constraint: this must not pollute kernel scope. The kernel publishes; the metrics service interprets.
Note (2026-08-31): the "known endpoint" above is the part to re-examine; the constraint under it is exactly right. This appendix predates the
traceutility, which shipped with ZERO kernel growth - the ring lives in theloggerservice and the instrumentation in the SDK. The reasoning that kept it out of ring 0 applies here: a kernel event queue needs a bound, a bound needs a drop policy, and deciding what to discard is a judgement (§26.10). A kernel-held endpoint to a RESTARTABLE consumer is worse still - stale, with nobody above it to recover it (§14.3).(Update 2026-09-04: that service is now called
events- see the §11.4 amendment. The note is left as written, including the old name, because it is dated; only this line is added, so a reader is not sent looking for a service that no longer answers to it.)Kernel STATE is already published by pull (
InspectKernel, 25 queries, andTaskStat, gated by INTROSPECT). Kernel EVENTS can ride the §11.4 shape: a bounded ring the kernel writes and a service DRAINS - no endpoint, no consumer identity, no policy in the kernel.docs/observability.mdhas the full argument and the three-part test any new mechanism must pass first. Non-normative, as is this appendix.
C.3 Cluster Mode (Single-System-Image)
Tentative timeline: multi-year research direction. Not a milestone commitment for any specific version.
The ambition: multiple GodspeedOS instances, possibly identified by a shared token, joining together to act as a single system. Conceptually similar to what k8s does for containers, but at the OS layer: services on any node, IPC across nodes, single namespace.
Why this is unusually feasible architecturally:
- Invariant 11 ("identity is stable; location is not") is the design primitive distributed systems are built on. The routing table generalizes cleanly:
EndpointId → CoreIdbecomesEndpointId → (NodeId, CoreId). SMP already separated identity from execution location; cluster mode extends "location" from a core to a (node, core) pair without changing the philosophy. - The generation-number mechanism for cross-core revocation extends to cross-node revocation.
- The absence of POSIX, fork, shared memory, and ambient authority means none of the impossible-to-distribute primitives are baked in. Linux clustering attempts (OpenSSI, MOSIX) all foundered on
mmap, signals, and inherited file descriptors.
Why it is still a multi-year project, not a v2 weekend:
- Synchronous IPC does not survive network latency. Either remote IPC must be a different primitive (loses transparency), or "blocking send" must mean something different cross-node (semantic fork in the API).
- Cluster membership, leader election, and consensus are real distributed-systems problems (Raft / Paxos territory).
- Cryptographic capability transfer over a network - caps must remain unforgeable when crossing the wire.
- Cross-node TCB definition: does the supervisor on node A have authority over services on node B? If yes, a compromised supervisor compromises the cluster. If no, what coordinates restarts?
- Failure semantics expand: not just node crashes, but network partitions, split-brain, and partial failures.
Reference points:
- Plan 9 from Bell Labs achieved network-transparent files and processes 30+ years ago.
- Barrelfish (Microsoft Research) explored "the OS as a distributed system" via the multikernel model.
- MOSIX, OpenSSI, LOCUS - Linux/Unix attempts at SSI; useful for understanding what didn't work and why.
The architectural primitives in this constitution are unusually well-suited for revisiting these ideas. Whether and when to attempt it is open.
C.4 Cluster Routing: Architecture and API
Full design notes, failure semantics, flow control, ordering, registry scope, transport options, and TCB authority model live in
docs/cluster-design.md. This section records the headline conclusions.
The routing table generalizes from EndpointId → CoreId to EndpointId → (NodeId, CoreId). The invariant "identity is stable; location is not" already encodes this - cluster mode extends the definition of location without changing the philosophy. The generation mechanism handles cross-node service mobility identically to how it handles cross-core restarts today.
The remote IPC API uses a distinct call surface (send_remote with explicit timeout) rather than transparent routing. The existing constitution invariants settle this: a successful local send guarantees queue delivery on this machine; a successful remote send guarantees handoff to a transport. These are different contracts with different durability and failure obligations, and pretending otherwise is the architectural mistake transparent-clustering systems have historically made. The network boundary is visible at three layers: contract (ipc_send_remote), type system (RemoteSendCap vs LocalSendCap), and call site. Applications that never declare ipc_send_remote are entirely unaffected by cluster membership.
Three questions must be resolved before cluster mode can ship: the transport protocol (which shapes failure semantics and ordering guarantees), the registry consistency model (distributed name resolution is the largest single piece of work, comparable in scope to most of v1), and cross-node TCB authority (whether a supervisor on node A governs services on node B - the central security question for clustering).
Appendix D: Shell, Scripting, and Utility Ecosystem (Non-Normative, Far Future)
Status: Non-normative, far-future. Records the design intent for what shell scripting could look like on GodspeedOS, and what porting Unix-style utilities would actually require. This appendix does not amend the constitution.
D.1 Why This Is Possible
The capability constraints in the constitution do not forbid shell scripting. They reshape what scripting is under the hood.
The fundamental abstraction of a shell script is "compose a sequence of commands and feed data between them." Nothing in the constitution forbids that. What changes is how composition happens.
D.2 Walking Through Bash Primitives
| Bash primitive | GodspeedOS mapping |
|---|---|
Sequential (cmd1; cmd2) | Shell calls supervisor.spawn(cmd1), waits, then spawns cmd2. Unchanged. |
Variables, if, while | Entirely shell-internal; never touch the OS. Unchanged. |
Pipes (cmd1 | cmd2) | Capability-mediated. See D.3. |
Redirection (cmd > file) | Shell creates the file via FS, mints a WRITE cap, grants to cmd. Same UX, different mechanism. |
Substitution (x=$(cmd)) | Shell sets up cmd with a SEND cap to a shell-owned endpoint, captures the output, binds the variable. |
Background (cmd &) | Spawn without waiting. Trivial. |
D.3 The Pipe Pattern
The interesting case is the pipe, because Unix pipes rely on fork and inherited file descriptors - neither of which exists.
In GodspeedOS, cmd1 | cmd2 becomes:
- Shell creates a fresh IPC endpoint.
- Shell grants
cmd1aSENDcap to that endpoint, via its spawn contract. - Shell grants
cmd2aRECVcap to the same endpoint, via its spawn contract. cmd1's "stdout" is "send to the cap I was granted."cmd2's "stdin" is "recv from the cap I was granted."
Pipes still exist. They are capability-mediated rather than fd-mediated.
The user-facing syntax can look exactly familiar:
ls /data | grep .txt > files.list
The shell does more capability brokerage than bash; the user sees the same thing.
D.4 The Security Upside
Capability-mediated scripting is meaningfully safer than POSIX shell by construction.
rm -rf / cannot exist on GodspeedOS unless the user (via the shell) explicitly grants the rm service a WRITE cap to /. The shell becomes the deliberate place where authority is decided. It can refuse dangerous compositions, ask for confirmation, or apply policy.
There is no equivalent of "ambient authority leaked through fork-exec and now the wrong process deleted everything."
D.5 Language Design - Open Question
The script language syntax does not fall out of the architecture. Three plausible directions:
| Direction | Trade-offs |
|---|---|
| POSIX-flavored | Familiar muscle memory; inherits 50 years of warts (word-splitting, quoting rules, [ vs [[). |
| Modern shell | (fish, nushell, oil-inspired) Structured data, better composition, fewer footguns. |
| Embedded language | Shell hosts a real language (Lua, Rhai, custom DSL); scripts are programs in that language. |
Likely lean: modern-shell-inspired. POSIX-shell quirks exist for historical reasons that don't apply here.
D.6 What "Porting" GNU Utilities Would Actually Mean
A common assumption is that supporting Unix-style utilities means "port GNU coreutils." This is misleading.
It is not a port. It is a rewrite. GNU coreutils is hundreds of thousands of lines of POSIX-specific C. You cannot recompile it against a new libc and expect it to work, because the underlying primitives don't exist:
- No
fork/exec. - No
errno. - No POSIX signals (no
SIGPIPE,SIGINT,SIGTERMhandlers). - No inherited file descriptors.
- No environment-variable inheritance.
- No process groups, sessions, or terminal control as POSIX defines them.
Each utility has to be rewritten in Rust (or whatever) against the GodspeedOS SDK. Contract per utility. Capabilities for everything it touches. IPC for what it produces and consumes.
The rewrite is genuinely simpler per-utility, however, because the OS handles the plumbing that POSIX utilities have to handle themselves:
GNU cat worries about | GodspeedOS equivalent |
|---|---|
errno translation | Typed Result<> from the SDK |
| Signal handlers | None needed |
| Permission checks | Either you have the cap or you don't |
| Symlinks, special files | FS service handles; utility doesn't see them |
| getopt edge cases | Rust argument-parsing crate |
| Cross-platform abstraction layers | Single platform |
| Memory safety | Free with Rust |
A cat-equivalent in GodspeedOS is on the order of 30 lines of Rust. GNU cat is hundreds of lines, mostly handling POSIX corner cases that GodspeedOS doesn't have.
D.7 Realistic Expectations
The GNU community is heavily invested in POSIX. Existing GNU code is unlikely to be ported by its existing maintainers; the architectural mismatch is too large.
A more realistic scenario is a fresh community building a coreutils-equivalent for GodspeedOS from scratch in Rust, motivated by the architecture rather than by carrying forward existing code. The friendliness this appendix describes is friendliness to the rewrite, not friendliness to existing C source.
Bash compatibility is explicitly not on offer. A shell language that resembles bash superficially but is its own thing underneath is fine; pretending bash scripts will run unmodified would be a lie that bites users later.
D.8 Why This Belongs in Far-Future Scope
None of this is v1, v2, or v3 work. It is what becomes possible once:
- The kernel and TCB are stable.
- A real userspace exists (
events, fs, network). - A supervisor API for service-initiated spawn (with cap delegation) exists - currently
supervisor.spawnis supervisor-internal. - The userspace community has formed enough to have opinions on what shell language to design.
This appendix exists so that, when that time comes, the design intent is on record and the architectural reasoning is preserved.
26. Architectural Discipline
The architecture survives only if the discipline survives.
The greatest long-term risk to this system is not memory corruption, race conditions, or hardware failure.
The greatest risk is gradual architectural erosion:
- hidden complexity;
- convenience abstractions;
- implicit behavior;
- speculative extensibility;
- silent fallback paths;
- and features that weaken the model in exchange for short-term ergonomics.
This section exists to preserve the architectural mindset that produced the system.
26.1 The Model Is The Product
GodspeedOS is not merely a collection of kernel features.
The value of the system is the coherence of the model:
- explicit authority;
- bounded behavior;
- visible failure;
- typed capabilities;
- restartability;
- and identity separated from execution location.
A feature that weakens the model weakens the system, even if the feature appears useful.
The architecture itself is the product.
26.2 Features Must Be Pulled Into Existence
Features are added because:
- a constitutional invariant requires them;
- an identity test requires them;
- a real operational problem requires them;
- or a demonstrated implementation limitation requires them.
Features are not added because:
- they may be useful later;
- other systems have them;
- they feel incomplete without them;
- or they might support hypothetical future flexibility.
Speculative abstraction is architectural debt.
The preferred state of an unneeded feature is:
not implemented; will be implemented when a test requires it
Deferral is a design decision, not a weakness.
26.3 Identity Tests Define System Identity
Identity tests are not implementation tests.
They are executable constitutional invariants.
A passing identity test means:
- the implementation still matches the model;
- the guarantees in this document still hold;
- the architectural invariants still compose correctly;
- and the system is still the system this document describes.
A failing identity test is evidence of architectural drift.
If an identity test fails:
- either the implementation is wrong;
- or the constitution has changed.
There is no third category.
26.4 No Silent Complexity
Complexity must remain visible.
Reject:
- hidden retries;
- invisible caching layers;
- implicit authority escalation;
- silent transport substitution;
- transparent distributed semantics;
- automatic fallback behavior;
- convenience APIs that weaken guarantees;
- or abstractions that obscure ownership or failure.
The system should always make it possible to answer:
- where authority came from;
- where state lives;
- who owns the state;
- what failed;
- what guarantees exist;
- what the timeout boundary is;
- and what recovery obligations now exist.
If those questions become difficult to answer, the abstraction is too opaque.
Visible caching is not silent complexity. The rejection above is of invisible caches: ones that can drift and lie with no way to tell. A derived view (a cache, index, or precomputed count) is legitimate when it reduces to a single irreducible source, is reconciled when it drifts (a repair path rebuilds it from that source), and is subordinate (the source wins; the view is never authoritative). The free bitmap and free count of fs are exactly such views of the file tree: stored, but not a second truth. The line this section draws is between a visible, reconcilable derived view (allowed) and a hidden, unreconcilable one (rejected). This is Commandment III (COMMANDMENTS.md); see also §3.8 and §3.9 / Invariant 9.
26.5 Explicitness Over Magic
The system intentionally prefers explicit operations over implicit convenience.
Examples:
- explicit capability passing instead of ambient authority;
- explicit restart instead of live mutation;
- explicit remote IPC instead of transparent clustering;
- explicit reacquisition instead of silent rebinding;
- explicit queue limits instead of elastic growth;
- explicit contracts instead of inferred permissions.
This is not accidental minimalism.
It is how the system preserves mechanical honesty.
26.6 Bounded Behavior Over Optimistic Behavior
Every subsystem should have:
- bounded memory usage;
- bounded queue growth;
- bounded retry behavior;
- bounded authority;
- bounded execution scope;
- and bounded failure semantics.
Unbounded behavior eventually becomes undefined behavior under load.
If a subsystem cannot explain:
- its limits;
- saturation behavior;
- failure mode;
- and recovery strategy;
then the subsystem is incomplete.
26.6.1 Bounded memory means stack and arenas, not heap (settled direction)
The default mechanism for bounded memory is no heap. State lives in fixed stack arrays, in bounded reusable arenas (a fixed region + a bump pointer, reset between operations), or in immutable rodata - never behind a general allocator. The heap reflex is resisted by default.
This is not asceticism; it is how the bound stays visible. A fixed footprint can be read off the source - the maximum a subsystem can use is right there. There is no allocator in the trusted base to fragment, to fail in the middle of an operation, or to turn memory use into a runtime mystery. And overflow fails the GodspeedOS way: loud, into a guard page, killing one service - never a silent slide into thrashing. A heap erases each of those properties, which is why it is the exception (declared, scoped) and not the default.
When a working set feels too big for the stack, the move is not to reach for a heap - it is to change the representation so the working set is small:
- stream in fixed chunks instead of buffering the whole thing (the
editpiece table holds one window of an arbitrarily large file, never the file;read/write/copystream inIO_CHUNKpieces); - refer to data by
(offset, len)spans instead of copying it (piece spans; interned string ids in the recordsTable); - give a subsystem its own named, bounded arena instead of a shared allocator (the records arena), reset between uses;
- iterate with an explicit bounded stack instead of call-stack recursion (
tree's walk).
format_args! is already bounded - it does not allocate. The no-heap rule forbids a growable
buffer, not lazy formatting. Building output with format_args! - and logging it with the SDK's
log_fmt, which renders through a fixed 256-byte stack buffer - IS the bounded discipline, not a
violation of it. Do not hand-roll digit-by-digit number formatting to "avoid the heap" that
format_args! never touches; reach for log_fmt (or write! into a fixed-size array) instead. Over-
applying this section - refusing the sanctioned bounded tool and reinventing it - is itself the mistake.
A hard ceiling reached loudly is therefore a feature, not a missing heap: it says "rethink
the working set." (The selfcheck | write stack overflow was exactly this lesson - the fix was to
forbid the unbounded nesting, not to add a heap.)
This is simplicity as much as fault tolerance (§2.3). The bounded representation is usually also the clearer one, because the constraint forces you to name the working set instead of hand-waving it onto a heap. Per §26.13 the bar is simple-and-bounded, not clever-and-cramped: a stack-only design that is harder to read than a heap one is a regression, not a win. The goal is the right data shape - a piece table, a ring buffer, an arena - over which boring code is small by construction.
26.7 Loud Failure Over Hidden Recovery
The system must prefer visible failure over ambiguous state.
A loud crash is preferable to silent corruption.
A rejected operation is preferable to undefined semantics.
A restart is preferable to hidden mutation.
A visible timeout is preferable to indefinite waiting.
A reported failed recovery is preferable to a hidden one.
The developer must never be forced to guess whether:
- an operation succeeded;
- a message was delivered;
- authority still exists;
- or the system silently degraded behavior.
The kernel boundary must remain semantically honest.
A recovery that itself fails is still a failure. Retrying, reacquiring, or falling back is the right response to a failure - but when the recovery step also fails, that outcome must remain as visible as the original failure. Proceeding as though a failed recovery had succeeded - discarding its result and continuing - converts a loud failure into a silent one and hides exactly the state an operator needs to see. Every failure path, including a retry that ultimately fails, is reported, never swallowed. This holds in any language: an ignored error return is the same silent fallback as a suppressed exception.
A limitation that cannot be closed is RECORDED, never papered over. The rule above governs what the system does at runtime; this governs what the project says about itself, and it is the same refusal to hide. Some gaps cannot be closed today - the hardware has no such unit, the fix is real work and not a constant, the honest guarantee is narrower than the one already claimed. The temptation is to leave the broader claim standing because it is nearly true. Write the gap down instead: state plainly what does NOT hold, where, and why, at the place a reader would otherwise rely on the claim.
A recorded limitation is a thing the next person can fix and can plan around. An unrecorded one is discovered by whoever trusts the document, usually at the worst moment, and it costs them the right to trust the rest of it. This is why a narrowed guarantee is amended into the text rather than quietly left; §6.1's backend-conditional crash-recovery claim and its ARM DMA posture are both here for exactly this reason.
26.8 Identity Over Location
Services are identities, not placements.
Core assignment is an execution detail.
Node assignment is an execution detail.
The location of execution may change across restart boundaries without changing system identity.
The architecture must continue to separate:
- who a service is;
- from where a service currently executes.
Location is mutable. Identity is stable.
26.9 Authority Must Remain Visible
Authority should always be inspectable and traceable.
A reviewer should be able to determine:
- what a service can do;
- where the authority came from;
- which capability granted it;
- and whether the authority can be revoked.
No subsystem may gain authority through:
- process ancestry;
- ambient inheritance;
- hidden globals;
- implicit trust;
- or side effects.
Authority is granted deliberately or not at all.
26.10 The Kernel Is Mechanism, Not Policy
The kernel exists to enforce invariants, not interpret intent.
The kernel provides:
- isolation;
- scheduling;
- capability enforcement;
- IPC routing;
- memory protection;
- interrupt routing;
- and bounded primitives.
The kernel does not:
- guess developer intent;
- silently reinterpret contracts;
- optimize correctness away;
- or make policy decisions on behalf of services.
Policy belongs in services.
Mechanism belongs in the kernel.
26.11 Understandability Is A Hard Requirement
The system must remain understandable by a single engineer.
The "30-minute whiteboard rule" is mandatory:
- a contributor should be able to explain the architecture,
- the capability flow,
- the restart model,
- the IPC semantics,
- and the failure model
on a whiteboard in roughly 30 minutes.
If understanding requires:
- tribal knowledge;
- hidden runtime behavior;
- undocumented interactions;
- or layered abstractions across dozens of components;
then the system has exceeded its acceptable complexity budget.
26.12 Correctness Before Performance
Performance matters.
Correctness matters more.
Predictability matters more than peak throughput.
The system intentionally accepts:
- extra copies;
- extra validation;
- explicit synchronization;
- and visible restart boundaries
when they preserve architectural clarity and bounded correctness.
Optimization is permitted only when:
- invariants remain visible;
- failure semantics remain unchanged;
- observability is preserved;
- and the resulting system is no harder to reason about.
26.13 Discipline Over Cleverness
Clever code is not an achievement if it weakens the model.
The preferred implementation is:
- boring;
- explicit;
- inspectable;
- testable;
- restartable;
- and mechanically honest.
The system should resist:
- abstraction for its own sake;
- framework-style indirection;
- meta-programming layers;
- hidden runtime behavior;
- and architecture driven by novelty.
A smaller coherent system is preferred over a larger impressive one.
26.14 Borrow The Mechanism, Never The Model
Reference implementations are how this project learns hardware. Linux, BSD and u-boot are read as executable datasheets: which register the silicon needs written, in what order, with what value, and what the device does when you get it wrong. That reading is encouraged and has repeatedly been the difference between a working driver and a week of guessing.
What is borrowed is the SILICON'S requirement. What is not borrowed is the other system's model.
Those two are easy to confuse, because they arrive in the same file. A register write sequence is a fact about the hardware and belongs here unchanged. An ambient global, an unbounded buffer, a heap allocation on a hot path, a driver living in the kernel because that is where the reference put it - those are that system's answers to that system's constraints, and they are not facts about anything. Importing them because "Linux does it" is how a model rots while every individual change looks justified.
The test is one question: is this a property of the device, or a property of their design? Ordering, timing, magic values, error semantics, what a bit means - the device. Where the state lives, who owns it, how it is allocated, what happens when it fails - ours to decide, under the constitution.
Divergence from a reference is therefore normal and does not need apologising for; it needs recording. When this system deliberately does something differently, say so at the point of difference and say why, so the next reader knows it was a decision and not an oversight. Silent divergence is how a port acquires bugs nobody can explain; unexplained convergence is how it acquires violations nobody noticed.
26.15 Preserve The Invariants
Every contributor is responsible for preserving:
- identity over location;
- explicit authority;
- bounded behavior;
- typed capabilities;
- failure visibility;
- restartability;
- and no silent fallback.
If a proposal weakens those principles, the burden of proof is on the proposal.
The default answer to architectural uncertainty is:
- simplify;
- reduce scope;
- make the behavior explicit;
- and preserve the invariants.
26.16 Final Reminder
The system is allowed to evolve.
The model is not allowed to rot.
Every feature, abstraction, optimization, and subsystem must justify its existence against the constitution.
If the implementation becomes easier to extend but harder to reason about, the system has regressed.
Correctness is not enough.
The architecture must remain coherent.