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

  1. Purpose of This Document
  2. Project Identity
  3. Constitution: Non-Negotiable Invariants
  4. Architecture Overview
  5. Repository Structure
  6. Trusted Computing Base
  7. Capability System
  8. IPC
  9. Scheduler and SMP
  10. Memory Model
  11. Bootstrap Sequence
  12. Drivers and Interrupts
  13. Service Contracts
  14. Service Lifecycle
  15. State and Persistence
  16. Update Model
  17. Developer Workflow
  18. Unsafe Policy
  19. Debugging Model
  20. Performance Philosophy
  21. Contribution Rules
  22. Identity Test Suite
  23. First Milestone
  24. Glossary
  25. Final Principles
  26. Architectural Discipline

Appendices (forward-looking, mostly non-normative):


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

  1. Clarity over novelty. Every part of the system should be explainable in a paragraph.
  2. Correctness over cleverness. A boring, verifiable design beats a clever, fragile one.
  3. 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

CapabilityStatusRationale
SMPSupported (static)Cross-core parallelism; no migration
Zero-copy IPCRejected, permanentViolates "no shared mutable memory"
Live code updatesRejected, permanentRestart-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.md 14). 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's gs::call reports OutcomeUnknown, 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

SystemWhat we borrow
seL4Capability model, synchronous IPC discipline
HubrisDeclarative task contracts, supervisor-driven restart
FuchsiaUserspace drivers, capability handles in IPC messages
GenodeComposition through capability delegation
RedoxRust 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.

  1. 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.

  2. No shared mutable memory by default. Services have isolated address spaces.
  3. All authority is explicit. Capabilities, not identity.
  4. Kernel remains tiny. Memory, scheduling, IPC, capabilities, interrupts, cross-core routing. Nothing else.
  5. Unsafe is isolated and audited. Permitted only in arch/, memory/, capability/, smp/.
  6. Services must be restartable (with stated TCB exceptions).
  7. Contracts are enforced, not interpreted.
  8. State must be explicit and owned. No anonymous singletons.
  9. No unowned global mutable state. Immutable globals are fine.
  10. System must remain understandable. 30-minute whiteboard rule.
  11. Identity is stable; location is not. Services have stable names; their core assignment may change across restarts.
  12. 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_64 in 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 the arch::imp seam and must never name an ISA - enforced mechanically by scripts/arch_boundary_check.py (neutral layers reach hardware only through the seam) and scripts/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 in memory/allocator.rs and task/scheduler.rs cite 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 names arm in 8 places, aarch64 in 4 and x86_64 in 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's hwclass list - 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 figure milestones/ 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-repeated any(x86_64, aarch64, riscv64) was one question - is configuration space reachable - and is now one build.rs fact. 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 hwclass list 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 arm in 8 places, aarch64 in 4 and x86_64 in 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.py forbids inline assembly and named arch modules outside arch/, and a #[cfg(target_arch = "arm")] in kernel/src/task/mod.rs is 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 in services/supervisor/build.rs and services/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.md has 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 are target_pointer_width on 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-driver picks its MAC by ISA on three of four boards and needs a kernel query to stop (backlog/21), hw-enumerator packs a host-bridge config selector that belongs in arch/ (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.py parses 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 ResourceId and its owning endpoint and nothing more; the owning service (fs) alone maps ResourceId → 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/ehci on x86, dwc2 on 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

ComponentTrusted because
KernelEnforces 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/smpConcurrent-correctness primitives
supervisorHolds 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-driver and fs are no longer TCB members. They were a v1 simplification (§6.3): fs owned persistent state it could not recover after a crash, so its death - and that of the block-driver it depends on - was a panic+reboot. The filesystem robustness program closes that gap: fs now 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; fs re-mounts (recovering via the journal) and re-registers, block-driver re-initialises the controller, and clients reacquire via the registry and retry (§14.3, §6.2). block-driver holds 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 (fs survives its own restart). The remaining non-restartable set is now just init + 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-driver and fs from 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 of fs alone: 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. ahci issues FLUSH CACHE EXT when fs asks 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 barriers fs already 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, fs recovers 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 CACHE outright, 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-kernel arch/arm/dwc2.rs; that file was DELETED by the 2026-08-17 amendment below and the driver is services/dwc2 now - 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, and fs says 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: fs is restartable everywhere; it is crash-recoverable on a backend that can be ordered. Where it cannot be, fs remains 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 CACHE outright", 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 - dwc2 on the Pi 2, xhci on the Pi 4, xhci on the VisionFive 2, one physical stick - and fs has 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 answered SYNCHRONIZE 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 in build/pi2a.log immediately after block-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 repaired

A 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-lyingflush models exactly that case in QEMU and it stays. The honest form of the Phase D claim - fs is 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-window cuts 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/42 carries 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): registry is 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 registry SERVICE 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 minimal name → endpoint recovery directory inside the kernel (ipc::names + the gated AcquireSendCap). The supervisor wires every service from a name → cap map 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 and docs/naming-design.md are 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 supervisor is 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. (init removed, Phase 5; registry retired, Phase 4; block-driver + fs restartable, 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, and shell are 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 temporary EndpointDead / lookup miss, reacquire by name via the kernel directory, and retry (§14.3). fs re-mounts to a consistent state via its crash-consistency journal (Phase C; docs/persistence.md §6.8). The shell is the user's interface - a crash or a deliberate kill shell respawns 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). registry left the TCB via H11 (then the service was retired, Phase 4); block-driver + fs via 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: the kill syscall, 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 did fs restart?" could be answered nowhere in the system: a deliberate kill and a crash looked the same.

The notice now carries it: the name, a NUL, then K and the name of the task that called kill, or F, 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's death). 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 answers supcmd::DEATH; its "died, restarting" line now ends - killed by shell or - 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's el0-fault-test); osdev test identity 24/0 and adv 15/0. docs/ask-design.md 6 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, ehci and dwc2 as 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) and nic-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:

  • xhci is the only confined driver in the system. ehci and block-driver keep a stale firmware DMA pointer that confinement would fault, so both run in deliberate passthrough (kernel/src/task/mod.rs, the confine flag on HwClass::Pci - this cited a DeviceSpec type that has never existed, and it was introduced to replace a rotting line number on the grounds that a field name cannot drift); nic-driver is spawned confine=false.
  • AMD-Vi is x86-only. Every iommu:: entry point on arm, aarch64 and riscv64 is a stub and confine_device returns false. 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.md and docs/ahci.md each 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 xhci is 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 with amd-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 xhci and ehci, 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-driver and nic-driver are still in passthrough, and on the T630 the audio driver does not yet use DMA at all (docs/audio.md, A6), so on real hardware xhci is 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 xhci and 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 an xhci that stopped completing commands in a chaos run, docs/wifi-usb.md 51.)

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_PUSH holders 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 removed REBOOT from the USB drivers, so a compromised driver can no longer hard-reset the machine directly from any context - reboot lives only with the shell (its reboot command). The residual (a keyboard can type) is inherent to being a keyboard, and is recorded here rather than papered over. audits/security-audit.md SEC-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 holds REBOOT - 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 a CONSOLE_PUSH holder could already type reboot - 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. The xhci SERVICE drives the controller through an MMIO capability and a DMA arena granted at spawn, reaches the console through CONSOLE_PUSH, and serves storage over the block IPC protocol that block-driver already 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 and confine_device returns false - 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.rs is 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/dwc2 registers for USB_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 of arch/arm/dwc2.rs is 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 call hardware_reset and 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 for services/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.rs is deleted and services/dwc2 drives the controller from userspace on USB_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_device returns false on 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/smsc95xx networking, 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 of arch/arm/dwc2.rs is TCB-critical (audited: audits/unsafe-audit.md, audits/security-audit.md Audit 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 call hardware_reset directly), 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.md Audit 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 GRANT right).
  • Generationed. Stale caps fail their generation check on use.

7.4 Rights Model

RightMeaning
READRead from a resource
WRITEWrite to a resource
SENDSend messages to an IPC endpoint
RECVReceive messages from an IPC endpoint
GRANTTransfer this capability via IPC
REVOKERevoke 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:

ErrorMeaning
CapNotHeldCap not in calling task's table
CapInsufficientRightsCap held but lacks required right
CapNotGrantableSend embedded a cap without GRANT
CapWrongScopeCap targets a different resource than the action
CapRevokedAuthority explicitly invalidated
EndpointDeadEndpoint/service lifecycle terminated
ReplyDeadReplier 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 an RwLock, and this section claimed a property the code never had. GLOBAL_RESOURCES is a SpinLock<GlobalResourceTable> (kernel/src/capability/table.rs); there is no RwLock type 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 the RwLock this 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 fresh ResourceId in its band, register it (generation 0, Alive), record the service's endpoint as its owner, and mint a cap with chosen Rights (READ/WRITE/GRANT). The service hands a (narrowed) copy to a client by the existing embedded-cap transfer (§8.5). fs does this on Open, recording ResourceId → 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 the ResourceId - 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 returns CapRevoked. fs revokes on delete/close.
  • Minting is gated (§3.1). resource_mint requires a RESOURCE_MINT capability, 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): call gains a BOUND, because the unbounded one was being worked around in a way that lost messages. call is 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 of send + a plain endpoint recv. 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 as fs clients 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 machinery RecvTimeout already 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 call with 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:

  1. Validates the cap (rights + generation).
  2. Looks up the target endpoint in the routing table.
  3. Enqueues into the target endpoint's queue (which lives on the target's core).
  4. 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:

  1. Grantable? The cap being sent must hold the GRANT right, or the transfer is rejected with CapNotGrantable (§7.7). A copy made by derive_cap carries 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).
  2. 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.
  3. Narrowed to need. Grant the least rights the receiver needs (§7.3). In particular, do not pass GRANT onward unless the receiver is meant to re-delegate - a cap handed out with GRANT lets 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

EventEffect
Service diesEndpoint generation bumped; queue drained
send to closed endpointReturns EndpointDead
recv on closed endpointReturns EndpointDead
Sender already blocked when endpoint closesWakes with EndpointDead (cross-core IPI)
Send-during-restart raceGeneration check catches it; returns EndpointDead
Replier dies while the caller is blocked awaiting its replyCaller 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 SDK request_with_reply, on which fs's block_rpc rides) 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 blocked recv hung 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 new ReplyDead code, 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 by osdev test reply-dead (the reply-side twin of §22 Test 4).

No delivery guarantee. A successful send means 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_LEAVING in task/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 TLBIALL when TTBR0 changes, RISC-V issues sfence.vma after writing satp, 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_root issues 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, until free_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 in backlog/fixed/80 K20.


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 supervisor directly; init is 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 minimal name → endpoint recovery directory - ipc::names + the gated AcquireSendCap - is the namer now; the supervisor wires every service from its name → cap map and clients reacquire by name through the directory). Phase 5 removes init: the kernel's one direct spawn is the supervisor (task::spawn_supervisor, using the gated SUPERVISOR_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 just supervisor + kernel.

Amendment 2026-09-12 (multi-architecture): the sequence above is the x86-64 one, and THERE IS MORE THAN ONE ENTRY PATH. kernel_main is 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 componentEffect
BootloaderHardware reset
Kernel BSP initKernel panic, halt
AP startupKernel 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 svcSupervisor logs, may retry per policy
Service contracted to unavailable coreSpawn 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 the logger service 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 the log_write capability, 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 only ipc_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 returns EndpointDead from it. So logs must NOT be re-pointed at events as 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 trace shipped, and has never held a log. events rather than observability: observe already 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 through log_write_slot and the trace path through a single SINK_NAME constant, so no service names its own sink.

What is NOT renamed, deliberately: log_write, log_write_slot, ctx.log(), syscall 5 and kernel/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 renamed log_received / log_did_not_receive for 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.rs and build.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 console service, 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 which fbcon was 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.rs now 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 as events 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 in COMMANDMENTS.baseline.toml because 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 hand wifi-driver the 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.md 45). 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_POWER at 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_ON on the firmware's GPIO expander, through the mailbox SET_GPIO_STATE tag - the pin Linux's mmc-pwrseq-simple toggles 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 with false, 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 kind WIFI_SDIO, result by read-back, arch/riscv64. Every port but those two answers false.)

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.md 46); 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.md 47). 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.md 55) 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.md 56). 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.md 55), 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 own GET_MIN_CLOCK_RATE or GET_MAX_CLOCK_RATE and returns what it reads back. The caller cannot name a rate. It is gated by CPU_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 are power'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.md 15, 26.10). Every port but the Pi 4 answers the seam with None and 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 DevicePower above - and the power service is where the policy, and any future power policy, lives.

Amendment 2026-10-01 (later): the result follows the pin's READ-BACK. DevicePower used to report success whenever the firmware accepted the SET_GPIO_STATE request, 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 when WL_ON reads back at the level asked for. The spawn also logs BT_ON, the same chip's Bluetooth enable: it reads 0 on this board, so WL_ON really is the whole of the radio's power and nothing else needs cutting (docs/wifi.md 53). 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 DevicePower amendment 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-audio as "the existing practice". The operator asked whether that was normal, and it was not: it was debt, and docs/service-ownership.md had 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.
  • DevicePower reaches 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 its MANAGED roster. The kernel's two lists of nineteen names are gone, and with them the drift that once left time and control uncounted; V-managed-watched checks the chain that replaced them.
  • The display is reclaimed from, and console output delivered to, the task granted the FRAMEBUFFER kind, not whatever is called console.
  • 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-matched console_push mint 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. reboot resets 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 \_S5 package 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 through halt_all_cores and 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. PowerOff turns 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.md 4.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, beside REBOOT: ending the session is the operator's, and no service has a reason to end it - a failing service is restarted, never the machine. power holds 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 type shutdown.

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 \_PTS method 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 sets POWER_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.md 5).

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 the DevicePower and CpuClock amendments above make. MISCIS is unchanged.

Amendment 2026-10-15 (reboot on the deadline, S6): the one deadline also holds a REBOOT. The operator asked that reboot take shutdown's forms - reboot counting 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. PowerOff gains two ops, 3 (reboot in secs) and 4 (cancel it), gated by REBOOT rather than POWER_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 through hardware_reset, the path Reboot (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 now and Ctrl+Alt+Del stay the immediate Reboot (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 in arch/, 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 = 2 and 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 own service_config table 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_std and cannot parse TOML at spawn. That is not a new fact and not an implementation shortcut - scripts/contract_check.py has opened with it since it was written, and that script exists PRECISELY because the .toml is 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 by contract_check.py (memory limit, placement, send peers) and by IV-contract-authority in scripts/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 recorder restart a service it sees stop responding", with no mention of any checker. It added service_control = true to recorder'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 validate passed it, and all twelve checkers stayed silent. It does not work: recorder's privilege word is 0, every call is denied, and the denial is discarded twice (the SDK's restart swallows its own kill error and the caller wrote let _ = ...) 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.md flagged 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

  1. 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).
  2. Determines core placement (round-robin or contract override per §9.2; rejected if contracted core unavailable).
  3. 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.
  4. Kernel refuses any privilege the supervisor does not itself hold (SUPERVISOR_DELEGATABLE), so a spawner passes on what it has and never mints.
  5. Kernel mints capabilities per the spawn request (each tagged with current resource generation).
  6. Kernel maps service binary into new address space.
  7. Service registers any owned endpoints in the kernel name directory (ipc::names).
  8. 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 is supervisor alone. So a spawner can no longer ask for "the image you already have" - it must SUPPLY one, and SpawnImage (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. SPAWN and image-spawn were the same right until step C, which meant every SPAWN holder - 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. SpawnImage therefore requires IMAGE_SPAWN on top of SPAWN, and the kernel refuses the call when a caller holds only the latter.

IMAGE_SPAWN is deliberately NOT delegatable. It is absent from SUPERVISOR_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 own spawn_by_image and spawn_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_pages over 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, and docs/service-ownership.md has 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 dozen SPAWN holders, 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.md 4b) 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 code godspeed verify runs - 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, through SpawnImage as 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 every fs holder 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_SPAWN stays the supervisor's alone and undelegated; godspeed-pm asks 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 app and only with the operator's answer. An installed package of kind app is a utility that owns the screen and the keyboard while it runs (gs::app, docs/developer-services-design.md 13.2, approved by the operator the same day). The supervisor starts it with SPAWN_FLAG_REQ_CONSOLE - the console read capability chaos and the shell already hold - when its grant names console, which godspeed install asks 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 driver is 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.md 13.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, and ehci since 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, as wifi-usb always 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_SPAWN stays 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_override is provided, the supervisor requires that core (subject to the strict rules of §9.2; rejected if the core is unavailable).
    • If placement_override is omitted, the placement decision is re-evaluated from scratch per §9.2 - contract-specified placement re-applies (and may fail with PlacementInvalid if 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.

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 the kill syscall or a fault, so every program was a service that never returns, and a program that does one job - a utility - could not exist outside the shell (docs/stdlib-design.md 1, 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 carries E and the status, beside K (killed by) and F (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. Exit reaches nothing: the one task it can end is the caller, as Yield and Park act 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 MANAGED that 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 in COMMANDMENTS.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.rs is 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 through unsafe. 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 in adversarial.rs. The install loader is the first production case: the supervisor reads a package's image from fs, checks its digest and signature, and hands the kernel those same bytes, and an image is larger than any stack. Region is two blocks (bytes, bytes_mut) over exactly the pages a successful AllocMem mapped, and the supervisor stays unsafe-free behind it, as a driver does behind Mmio.

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 unsafe lives 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/ and osdev/ carries #![deny(unsafe_code)], so rustc refuses the crate rather than a script noticing afterwards. That closes what a text scan cannot see - unsafe produced by a macro expansion, or spelled across lines - and it fails at the author's keyboard instead of at the next CI run.

deny rather than forbid, for exactly one reason, stated so nobody "tightens" it and breaks the build: a #[no_mangle] declaration is itself covered by the unsafe_code lint (an exported symbol can collide, which is a soundness hole), and every service needs #[no_mangle] service_main because build.rs links with --entry=service_main. forbid cannot be relaxed even for that. So the crates carry deny plus ONE #[allow(unsafe_code)] on the entry symbol, and scripts/unsafe_check.py asserts 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) and ipc.rs (8) are recorded as grandfathered floors, and this list gains loader.rs and main.rs, which it had always omitted. Neither is new unsafe - both are the state of the tree being written down for the first time. scripts/unsafe_check.py scanned only kernel/src/ and services/, so the SDK's ~125 unsafe lines were audited by nothing at all while §18.4 claimed CI checks the audit against source (backlog/fixed/18). The scan now covers sdk/, 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_syscall is an unsafe fn because 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 no unsafe of 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_syscall wrapper - 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.rs 79 -> 80. One call site, exit: one unsafe { raw_syscall(57, ..) } behind the safe ServiceContext::exit and gs::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.rs 77 -> 79. Two call sites behind the §12.3 amendment of the same date: power_off_call, one unsafe { raw_syscall(56, ..) } behind the three safe wrappers power_off, power_off_in and power_off_cancel; and power_off_pending, one unsafe { raw_syscall(13, 28, ..) }. The same single design consequence as the CpuClock amendment 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.rs 83 -> 84. One more unsafe { raw_syscall(13, 27, ..) } call site, boot_record_query, behind the safe boot_record_size and boot_record_read of 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.rs 83 -> 84. One more unsafe { raw_syscall(55, ..) } call site, the wrapper cpu_clock behind the §12.3 amendment of the same date - the same single design consequence as the DevicePower amendment 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.rs 82 -> 83. One more unsafe { raw_syscall(54, ..) } call site, the wrapper device_power behind 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 safe raw_syscall that 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 a conform-ok marker 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.md carries 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.

CategoryPurposeBar (what failure means)Status
IdentityPin constitutional decisions; existence proofConstitutional invariant violated§22 (Test 11 added, H11)
PropertyUniversal invariants under random inputsA claim the spec makes does not hold§22 (P1-P10, 10/10)
FuzzCrash resistance under adversarial inputsKernel panics on user-controllable inputActive
StressSurvival under sustained loadDrift, leaks, or corruption appear over timeActive
PerformanceLatency / throughput benchmarksA measured number regressed§22 (10/10)
AdversarialCapability isolation under attackAn attack succeeds where the spec says it failsActive
ChaosGraceful degradation under partial failuresA defined failure mode is not handled cleanlyActive
  ┌─────────────────────────────────────────────────────────────────────┐
  │  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.

IDPropertyPins
P1Random bytes → CapNotHeld or CapInvalid; never accepted as a cap§7.3 (unforgeable)
P2Generation per service is strictly monotonic across its lifetime§7.5
P3Cap rights never widen during transfer§7.3 (non-escalating)
P4∑ current_task_alloc_bytes ≡ pages mapped, after any sequence of alloc/free§10.3
P5Every live endpoint has exactly one owning task§8.3
P6Queue head ≤ tail ≤ head + 16; count consistent with both§8.5
P7After unmap + TLB shootdown, the page is unreadable from every core§10.5
P8After restart, name resolves to a task with the same name and higher generation§14.2
P9Generation bump invalidates ALL holders, not just some§7.5
P10Every 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.

IDSurfaceGenerator
F1Syscall args (each × 1M iters)Random u64 in a0/a1/a2; including kernel addresses, unmapped pointers, misaligned values
F2Syscall numbersRandom u64 as nr; must return UnknownSyscall, never crash
F3ELF binariesBit-flip mutations of known-good ELFs handed to the spawner
F4Service contractsMalformed TOML; JSON Schema-invalid structures
F5IPC message bodiesRandom bytes, random sizes up to 4 KiB
F6Embedded caps in messagesMessages claiming to carry caps with random structure
F7Cap generation fieldRandom u64 as generation in cap usage; must return CapRevoked or EndpointDead
F8Memory request valuesRandom 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.

IDScenarioDuration
S1IPC saturation: sustained try_send on a full queue1 hour
S2Restart storm: 100k kill/respawn cycles of one serviceuntil complete
S3Cross-core thrash: 4 cores × all-to-all IPC10 min
S4Cap table churn: 100k random create/destroyuntil complete
S5Generation overflow: force counter to wrap, observe wraparound semanticsuntil wrap + 1k operations
S6Long-running stability: ping/pong + introspection24 hours
S7Memory pressure: alloc-to-limit + free, 10k cyclesuntil complete
S8Idle stability: boot, no workload, observe24 hours
S9Interrupt storm: high-frequency timer + IPI cross-fire1 hour
S10Cascading revocation: kill a service held by many; observe propagationuntil 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.

IDMetric
B1IPC same-core round-trip latency: p50, p99, p99.9
B2IPC cross-core round-trip latency: p50, p99, p99.9
B3Syscall floor: yield round trip
B4Cap validation cost: one cap + generation check
B5Spawn cost: supervisor.spawn → service "ready"
B6Restart cost: kill + spawn
B7Cap table contention: throughput at 1, 2, 4 cores
B8Allocator throughput: pages/sec under contention
B9Message copy cost: 4 KiB upper-bound copy
B10Scheduler 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.

IDAttack
A1Service crafts random u64 values and tries to use them as caps
A2Service brute-forces endpoint IDs across the u32 space
A3Service attempts to allocate beyond its contract memory limit through every syscall path
A4Service receives a cap with limited rights and attempts to use rights it lacks
A5TOCTOU: service races a syscall with revocation of the cap it is about to use
A6Service tries to fill the cap table to denial-of-service the kernel
A7Service tries to detect IPC partner identity via timing
A8Service tries to monopolize a core via a tight loop without yielding
A9Service tries to spawn another service directly, bypassing the supervisor
A10Service passes kernel addresses as syscall arguments
A11Service invokes InspectKernel system queries without an INTROSPECT cap
A12Service invokes Reboot or PowerOff without the capability
A13Service invokes AcquireSendCap without the capability
A14Ring-3 CPU exception (null read, non-canonical read, divide-by-zero) kills the task, not the kernel
A15A 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.

IDFailure injected
C1One or more APs fail to come up during boot
C2A service in the boot manifest has a corrupted ELF (non-TCB)
C3Allocator forced to return AllocFailed at random syscall entry points
C4Bootloader provides degraded environment (minimal RAM, no framebuffer)
C5Kernel stack approaches exhaustion under deeply nested syscall
C6One core's timer interrupt is dropped for an extended period
C7TLB 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 4 minimum 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 a name → cap map 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-driver is 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

TestSpec sections pinnedConstitutional invariant
1. Bootstrap§11, §6TCB integrity
2. Capability enforcement§3.1, §7No ambient authority
3. IPC send/receive (same core)§8, §7.4Authority is explicit
4. Endpoint death§8.5, §8.6, §14.2Restartability
5. Capability transfer§7.6, §7.4Authority is explicit
6. Supervisor restart§14.2, §14.3Restartability
7. Memory limits§10.3, §10.4Isolation
8. Preemption§3.6, §9.1, §9.3No service monopoly
9. Cross-core IPC§8.3, §8.4, §9Identity over location
10. Restart with core change§9.2, §14.2, §14.4, §11Identity over location
11. Name resolves after restart (directory)§6.1, §6.2, §14, §3.11, §4.4Restartability / naming-out-of-kernel
12. Confined driver DMA faults§3.1, §6.4, §12No ambient authority (DMA)
13. fs survives own restart§6.1, §6.2, §6.3, §15, §14Restartability / TCB shrink
14. File is a capability§7.3, §7.10, §3.1, §3.3Authority is explicit (files)
15. Supervisor survives own restart§6.2, §6.3, §3.7, §14, §3.11Restartability / 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 ✅

  1. osdev run --smp 4 boots the OS with 4 cores; supervisor, events, ping, and pong reach steady state. ✅ (As recorded in 2026-05 this read "init, supervisor, registry, logger"; init was removed in Phase 5, the registry service retired in Phase 4, and logger renamed events in 2026-09.)
  2. ping placed on core 0; pong placed on core 1. ✅
  3. osdev logs ping shows ping sending a message every second. ✅
  4. osdev logs pong shows pong receiving each message (cross-core IPC). ✅
  5. osdev restart pong --core 2 kills pong on core 1 and respawns it on core 2. ✅
  6. ping observes EndpointDead and reacquires by name; the new cap routes to core 2. ✅
  7. After reacquisition, ping and pong continue communicating across the new core boundary. ✅
  8. The kernel does not panic on any core. ✅
  9. 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 image produces a UEFI GPT disk image at build/os-usb.img. (This said build/os.img, which is the QEMU/BIOS image - osdev/src/disk_image.rs notes the two are named apart on purpose, and §17 has it right.)
  • Image written to USB with Cygwin dd; boots via BOOTX64.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-metal supervisor 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):

BenchmarkResult
BP1 IPC same-core p5055,320 cycles (~18.4 µs)
BP3 yield floor39,903 cycles (~13.3 µs)
BP4 cap validation495 cycles (~165 ns)
BP5 spawn cost8,121,378 cycles (~2.7 ms)
BP6 restart cost14,462,309 cycles (~4.8 ms)
BP7 cap table1,168 cycles (~389 ns)
BP8 allocator616 cycles/4KiB page (~205 ns)
BP9 message copy 4KiB20,073 cycles (~6.7 µs)
BP10 scheduler decision2,323 cycles (~774 ns)
BP2 IPC cross-coreNot 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:

BenchmarkT630 isolatedJ5005 (above, perf-brutal)
BP1 IPC same-core p50~102,600 cycles (~51 µs) †55,320
BP2 IPC cross-core p501,433,087 cycles (~0.72 ms); p99/p999 16,409,799not measured
BP3 yield floor19,281 cycles (~9.6 µs)39,903
BP4 cap validation~1,258 cycles (~0.63 µs) †495
BP5 spawn cost45,406,292 cycles (~22.7 ms)8,121,378
BP6 restart cost54,231,139 cycles (~27.1 ms)14,462,309
BP7 cap table2,932 cycles (~1.5 µs)1,168
BP8 allocator~1,472 cycles/4KiB (~0.74 µs) †616
BP9 message copy 4KiB21,796 cycles (~10.9 µs)20,073
BP10 scheduler decision20,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 ReplyDead if the replier dies first, so it never hangs. Mechanism, not policy - the kernel learns a reply cap, not "RPC". The primitive behind the SDK request_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 a RESOURCE_MINT cap); the kernel validates and routes it as for any cap, badging a send with the opaque ResourceId so 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 Call request 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 with ReplyDead. 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 Call awaiting its reply (value -12; §7.7, §8.6). The reply-side twin of EndpointDead, 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.) registry left 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 + fs left via the Phase D amendment (§6.1, once fs gained crash-consistent recovery). DMA drivers (xhci/ehci, and ARM's dwc2) 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; init was 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 + fs are restartable storage services.)
  • Name directory - the kernel's minimal name → EndpointId map (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 a name → cap map and clients reacquire names through the directory. (The retired registry service'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/smp and arch/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

ReasonDetail
Tight Rust integrationThe 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 suppliedAPIC IDs come pre-discovered. arch/x86_64/ap_boot.rs does not need an ACPI parser to enumerate cores.
BIOS + UEFI from one bootloaderLimine supports both firmware modes with the same protocol. The kernel does not need to care which firmware booted it.
Good QEMU supportCritical for osdev run (§17). The whole identity test suite runs under QEMU; the bootloader must work there reliably.
Active maintenanceLimine 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.EFI on the EFI System Partition.
  • The kernel binary is placed where limine.conf references it.
  • Firmware → BOOTX64.EFI → Limine → kernel.

BIOS systems:

  • The installer runs limine bios-install to 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

OptionWhy Not
GRUB / Multiboot2Older protocol, clunkier Rust integration, no built-in SMP topology surface, much larger surface area to depend on.
Custom bootloaderA 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.md was 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.rs are typed Rust structures. C or other-language equivalents would need parallel SDKs.
  • Contract validation in osdev is 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 console service 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 in docs/console-service.md §5a: there is one input ring and one reader slot, so a service that owned the keyboard would block in ConsoleRead and 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: ls does not run, it answers try \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.py reads that same table to make sure no document in this repository shows one of those words being used as a command, which is how the ls -> dir rename was found to have missed ten worked examples.

Note 2026-10-13: two Unix words are commands, cd and pwd, and each has a reason. cd was kept from the start because it is universal (utilities/17_cd.md). pwd joined it with the filesystem layout (docs/filesystem-layout.md 6): the prompt is a plain gsh> , so something has to say where you are, and pwd is cd's other half - anyone who knows one knows the other. It left FOREIGN_HINTS, where its hint had been cd ., 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, so poweroff would claim what does not happen (docs/shutdown.md). It left FOREIGN_HINTS, where its hint had been reboot - wrong advice, since reboot turns nothing off - and halt and poweroff stay hints that answer shutdown.


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 trace utility, which shipped with ZERO kernel growth - the ring lives in the logger service 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, and TaskStat, 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.md has 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 → CoreId becomes EndpointId → (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 primitiveGodspeedOS mapping
Sequential (cmd1; cmd2)Shell calls supervisor.spawn(cmd1), waits, then spawns cmd2. Unchanged.
Variables, if, whileEntirely 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:

  1. Shell creates a fresh IPC endpoint.
  2. Shell grants cmd1 a SEND cap to that endpoint, via its spawn contract.
  3. Shell grants cmd2 a RECV cap to the same endpoint, via its spawn contract.
  4. cmd1's "stdout" is "send to the cap I was granted."
  5. 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:

DirectionTrade-offs
POSIX-flavoredFamiliar 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 languageShell 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, SIGTERM handlers).
  • 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 aboutGodspeedOS equivalent
errno translationTyped Result<> from the SDK
Signal handlersNone needed
Permission checksEither you have the cap or you don't
Symlinks, special filesFS service handles; utility doesn't see them
getopt edge casesRust argument-parsing crate
Cross-platform abstraction layersSingle platform
Memory safetyFree 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.spawn is 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 edit piece table holds one window of an arbitrarily large file, never the file; read/write/copy stream in IO_CHUNK pieces);
  • refer to data by (offset, len) spans instead of copying it (piece spans; interned string ids in the records Table);
  • 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.