Amend the constitution, three RFCs and the threat model: the bug hunt's flagged items, as ruled

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

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.

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.

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.

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

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