From 44f9914eed5bd49060ea6ef051db84ab8ee24d37 Mon Sep 17 00:00:00 2001 From: Matej Gomboc Date: Wed, 5 Aug 2026 06:23:59 +0200 Subject: [PATCH] docs: apply the maintainer's rulings on the bug hunt's flagged items MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit All thirteen flag-only findings from the 2026-08-05 repository sweep, resolved as the maintainer ruled and applied on their authorisation. Constitution §3: the IPC doctrine's "zero-copy page transfer for large ones" was the last doctrinal statement of the mechanism accepted RFC-0004 pruned as L4's abandoned long IPC; bulk data now moves zero-copy through shared-memory regions established out of band, IPC carrying only small descriptors, credited to RFC-0004's correction. Constitution §7: the pinned AArch64 triple is aarch64-unknown-none-softfloat, not the plain variant the project documented as fatal. RFC-0004: the acceptance note's "copy-vs-map verdict joins the MMU RFC" contradicted the revised body it accepted, which had settled copy-vs-map by pruning map — the open question is shared-memory establishment, and the note and the changelog's transcription of it now both say so. §5's "~100 cycle" figure is re-attributed to the earlier C++ blueprint; constitution §3 never contained one. RFC-0003: a dated amendment scopes §6's "records the parent" to what the built flat table actually promises, and the header's Discharges field now qualifies O-3 as destruction-only, matching §13. RFC-0001: a dated amendment re-runs the graves check against §3's grown list. Threat model §6: "Built" now requires enforcement at the boundary the obligation guards, closing the reading under which O-1/O-2 would already qualify through the host-proven capability crate; both gain notes that the mechanism binds at B1 when the syscall surface lands. The ratio stays three of twenty-seven, now unambiguously. Every change is logged in docs/CHANGELOG.md; the amendments are dated in the RFCs they touch. Co-Authored-By: Claude Fable 5 --- CONSTITUTION.md | 8 ++-- docs/CHANGELOG.md | 37 ++++++++++++++++++- ...tent-addressed-store-and-the-filesystem.md | 8 ++++ docs/rfcs/0003-capability-table.md | 13 ++++++- docs/rfcs/0004-ipc.md | 6 +-- docs/threat-model.md | 9 +++-- 6 files changed, 69 insertions(+), 12 deletions(-) diff --git a/CONSTITUTION.md b/CONSTITUTION.md index e275b2c..ef55106 100644 --- a/CONSTITUTION.md +++ b/CONSTITUTION.md @@ -75,7 +75,9 @@ The kernel is hand-written and minimal. It provides mechanism, never policy. runtime table operation the generation scheme secures. *(seL4; Fuchsia's downgradeable handle rights)* - **IPC is the product.** Register-based fast path for small messages, direct - sender→receiver switch, zero-copy page transfer for large ones. *(L4)* + sender→receiver switch; bulk data moves zero-copy through shared-memory + regions established out of band, IPC carrying only small descriptors. *(L4, + as corrected by RFC-0004)* - **Everything is a message**, with priority inheritance to prevent priority inversion. *(QNX)* - **Typed, bidirectional channels** as the userspace-facing IPC abstraction. @@ -185,8 +187,8 @@ replacing Linux, supporting every board on earth. - **Repository location:** clone into a container volume (or the WSL-side filesystem), never bind-mount from `/mnt/c` — the Windows-filesystem bridge is many times slower and is felt on every kernel rebuild. -- **Toolchain (pinned in the Dockerfile):** rustup with `aarch64-unknown-none` - and `x86_64-unknown-none` targets; `qemu-system-aarch64` / +- **Toolchain (pinned in the Dockerfile):** rustup with + `aarch64-unknown-none-softfloat` and `x86_64-unknown-none` targets; `qemu-system-aarch64` / `qemu-system-x86_64`; `gdb-multiarch` against QEMU's gdb stub over TCP; OVMF/AAVMF UEFI firmware; `mtools` for building boot images without root. - **Emulation:** plain TCG is adequate for a microkernel and needs no diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 2477077..05dc535 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -127,6 +127,39 @@ recorded is indistinguishable from law that was never agreed. ### Changed +- **Constitution §3 and §7 amended, on the maintainer's authorisation (2026-08-05): the IPC + doctrine's bulk-data clause, and the pinned AArch64 triple.** §3's "zero-copy page transfer for + large ones" had become the last doctrinal statement of the mechanism accepted RFC-0004 pruned as + L4's abandoned long IPC; it now reads "bulk data moves zero-copy through shared-memory regions + established out of band, IPC carrying only small descriptors", the lineage note crediting the + correction to RFC-0004. §7 named the pre-soft-float `aarch64-unknown-none` — the triple the code + changelog records as fatal (FP/SIMD emitted with `CPACR_EL1.FPEN` = 0, dead before the first + character reached the UART); it now names `aarch64-unknown-none-softfloat`, matching + `rust-toolchain.toml`, the Dockerfile and the pin check. Both surfaced by the 2026-08-05 bug hunt. +- **RFC-0004's acceptance note and §5 corrected, with this changelog's transcription (2026-08-05, the + maintainer's).** The acceptance note said "the slow-path copy-vs-map verdict joins the MMU RFC", + but the revised body it accepted had already settled copy-vs-map by pruning map — the question that + joins the MMU RFC is shared-memory establishment, and the note (and this file's acceptance entry, + which transcribed it faithfully) now says so. §5 attributed the "~100 cycle" figure to constitution + §3, which has never contained a cycle figure; it was the earlier C++ blueprint's, as the RFC's + original draft correctly recorded. +- **RFC-0003 amended (2026-08-05): §6's derivation-record wording scoped, and the header's O-3 + qualified.** §6 asserted that `derive` "records the parent"; the built table records nothing — a + test pins the absence of a parent link — and whether any derivation record exists is exactly the + decision §7 defers to RFC-0003a. A dated amendment scopes §6 to what is actually promised: + duplication only through an explicit, rights-checked kernel operation. The header's Discharges + field now says of O-3 what §13 and the earlier amendment already did: destruction case only, + selective revocation deferred to RFC-0003a. +- **RFC-0001 amended (2026-08-05): the graves check re-run against the grown list.** Its "None of the + four apply directly" predates §3's growth to seven; a dated amendment records that the three + additions do not apply to a userspace store either — and that the section's own recorded risk, the + store acquiring kernel support "for speed", is precisely the first of the new graves. +- **Threat model §6 amended (2026-08-05): the Built definition gains its missing clause.** "Built" + now requires the mechanism be enforced at the boundary it guards, not merely exist in the tree and + be exercised by CI — closing a reading under which O-1 and O-2 would already qualify through the + host-proven capability crate while nothing yet enforces either at B1. O-1 and O-2 gain notes + recording exactly that state: mechanism host-proven, binding at B1 when the syscall surface lands. + The Built ratio remains three of twenty-seven, now unambiguously. - **Four broken cross-references corrected in the accepted documents (2026-08-05), found by a repository-wide bug hunt.** All four are mechanical: a citation pointing at the wrong section or the wrong document, with no change to what any document decides. Recorded here rather than edited @@ -184,8 +217,8 @@ recorded is indistinguishable from law that was never agreed. rendezvous, endpoints as RFC-0003 capability objects, virtual-register fast path with a bounded copying slow path, move-only capability transfer, `call` with single-use reply objects, bounded notifications — is accepted in the form the 2026-07-30 prior-art review revised it to. The §9 open - questions remain expressly open and join their named RFCs (copy-vs-map → MMU, multi-core rendezvous - → scheduler, register budget → syscall ABI). With both halves of the core mechanism now accepted on + questions remain expressly open and join their named RFCs (shared-memory establishment → MMU, + multi-core rendezvous → scheduler, register budget → syscall ABI). With both halves of the core mechanism now accepted on paper — RFC-0003 already built and host-proven — the next design work is the initial kernel object set and bootstrap (RFC-0003 §14.4), after which endpoints become the capability table's first real consumer. diff --git a/docs/rfcs/0001-content-addressed-store-and-the-filesystem.md b/docs/rfcs/0001-content-addressed-store-and-the-filesystem.md index 4158f91..10ed6ae 100644 --- a/docs/rfcs/0001-content-addressed-store-and-the-filesystem.md +++ b/docs/rfcs/0001-content-addressed-store-and-the-filesystem.md @@ -165,3 +165,11 @@ These are not blocking. They are the next three RFCs. Recorded rather than quietly rewritten, for the reason given in RFC-0002's amendment: an accepted RFC is the record of a decision, and a decision log that edits itself is not one. + +- **2026-08-05 — the graves list this RFC was checked against has since grown.** "None of the four + apply directly" was true at acceptance; the constitution's §3 now names seven graves, the three + additions taken on 2026-08-01 (drivers pulled into the kernel for the fast path, compiled-in but + unused device paths, the catch-all right that decays into root). None of the three applies to a + userspace store either — and the risk the section already records, the store acquiring kernel + support "for speed", is precisely the first of the new graves, so the addition strengthens the + check rather than reopening it. diff --git a/docs/rfcs/0003-capability-table.md b/docs/rfcs/0003-capability-table.md index 031e7a0..0b39361 100644 --- a/docs/rfcs/0003-capability-table.md +++ b/docs/rfcs/0003-capability-table.md @@ -8,7 +8,7 @@ | Author | Drafted by Claude Code as sparring partner; verdict the maintainer's | | Date | 2026-07-30 | | Affects | Constitution §3 (kernel doctrine), pillar 2; the syscall ABI; every later subsystem | -| Discharges | Threat-model obligations O-1 (unforgeability), O-2 (non-widenability), O-3 (revocability), O-4 (no ambient authority) | +| Discharges | Threat-model obligations O-1 (unforgeability), O-2 (non-widenability), O-3 (revocability — destruction case only; selective revocation deferred to RFC-0003a), O-4 (no ambient authority) | > **Accepted.** The flat per-process handle table (§4, Option B) is the capability representation; > derivation is subset-only; transfer is a move; the syscall ABI is capability-indexed from its first @@ -318,3 +318,14 @@ These are not blocking. They are the shape of the design conversation this RFC o - Recorded as an amendment rather than a silent edit; the substance moves into RFC-0003a. **A related correction to Constitution §3 (the "Rust's ownership models capability transfer at compile time" slogan) is flagged for the maintainer — constitution text is theirs to amend.** + +- **2026-08-05 — §6's derivation-record wording scoped by the implementation, on the maintainer's + authorisation.** §6 says `derive` "records the parent" and that duplication is an operation "which + the kernel records"; the built table records nothing — derivation mints a flat sibling with no + parent link, and a test (`a_removed_parent_leaves_its_derived_sibling_untouched`) pins that absence + so RFC-0003a cannot regress it silently. Whether any derivation record exists at all is exactly the + B1/B2/B3 decision §7 defers to RFC-0003a. Read §6 as constraining duplication to an explicit, + rights-checked kernel operation — not as promising a derivation record before RFC-0003a decides + one. The header's Discharges field is qualified in the same pass ("destruction case only"), which + is what §13 and the 2026-07-30 amendment already said of O-3; the header had been the last place + claiming it unqualified. diff --git a/docs/rfcs/0004-ipc.md b/docs/rfcs/0004-ipc.md index 863f901..1412880 100644 --- a/docs/rfcs/0004-ipc.md +++ b/docs/rfcs/0004-ipc.md @@ -15,8 +15,8 @@ > RFC-0003 capability objects (§3); the virtual-register fast path and bounded copying slow path > (§5), move-only capability transfer in messages (§6), `call` with single-use first-class reply > objects and bounded notifications (§8) all stand, in the form the 2026-07-30 prior-art review -> revised them to. Accepting this RFC does not pre-empt the open questions in §9 — the slow-path -> copy-vs-map verdict joins the MMU RFC, multi-core rendezvous joins the scheduler RFC, and the +> revised them to. Accepting this RFC does not pre-empt the open questions in §9 — the shared-memory +> establishment mechanism joins the MMU RFC, multi-core rendezvous joins the scheduler RFC, and the > exact register budget joins the syscall ABI RFC. Anything the first implementation PR proves > wrong comes back here as a dated amendment, per house practice. > @@ -114,7 +114,7 @@ portability at little performance cost. The exact split is an ABI question (§10 syscall RFC; the shape is: **a short request and small reply allocate nothing and copy nothing beyond the message registers.** -§3's "~100 cycle" figure is kept as an aspiration for the **fastpath software logic**, not the +The earlier C++ blueprint's "~100 cycle" figure is kept as an aspiration for the **fastpath software logic**, not the round-trip: a real one-way IPC is ~190–320 cycles on cited hardware and a `call`+`reply` roughly double, so the honest target is "software overhead near the hardware limit", not "100-cycle RPC". diff --git a/docs/threat-model.md b/docs/threat-model.md index 5468237..ed256b7 100644 --- a/docs/threat-model.md +++ b/docs/threat-model.md @@ -124,7 +124,8 @@ The §9 seed's four, plus two the design has since made explicit. The obligations the design must discharge, numbered for citation. Each carries a status: -- **Built** — the mechanism exists in the tree today and is exercised by CI. +- **Built** — the mechanism exists in the tree today, is exercised by CI, and is enforced at the + boundary it guards. - **Designed** — the design commits to it; the mechanism is not yet implemented. Most obligations are here, because the kernel currently boots, greets and reports faults, and little else. - **Deferred** — acknowledged and deliberately not met in the initial target, with a stated reason @@ -137,10 +138,12 @@ and a mechanism that cannot name the obligation it discharges has not justified - **O-1 — Unforgeability.** Userspace cannot fabricate a capability referring to an object it was not granted; capabilities are kernel-held tokens, never bare integers userspace can guess or construct. - *(seL4.)* **Designed.** + *(seL4.)* **Designed** — the mechanism (handles as indices, kernel-held capabilities, generation + checks) is host-proven in the capability crate; it binds at B1 when the syscall surface lands. - **O-2 — Non-widenability.** No operation increases the rights carried by a held capability; derivation only narrows. A held read capability can never become a read-write one. *(seL4; Fuchsia's - downgradeable handle rights.)* **Designed.** + downgradeable handle rights.)* **Designed** — subset-only derivation is host-proven in the + capability crate; it binds at B1 with the syscall surface. - **O-3 — Revocability.** Authority once granted can be withdrawn, and revocation reaches capabilities transitively derived from the revoked one. *(KeyKOS/EROS.)* **Designed.** - **O-4 — No ambient authority.** Every resource access names a capability; there is no path to any