From 5faf6f68d0651f5a964c7058ed7033d66c81b051 Mon Sep 17 00:00:00 2001 From: Matej Gomboc Date: Sat, 1 Aug 2026 10:25:33 +0200 Subject: [PATCH] Amend Constitution 3: scope the compile-time capability claim On the maintainer's authorisation, taking the reword the 2026-07-30 prior-art review recommended, exactly as flagged in docs/CHANGELOG.md. The kernel-doctrine slogan said Rust's ownership and move semantics "model capability transfer at compile time". That is true of the kernel's internal handling - the no-Clone Capability makes duplication and use-after-move compiler-checked properties - and false of the userspace-observable cross-process transfer, which is a runtime table operation the generation scheme secures. The borrow checker sees one compilation unit and cannot span protection domains; RedLeaf's group reached the same conclusion for ownership types generally, and our own generation counters exist precisely because runtime checks hold that boundary. The constitution had become the last place in the repository making the unscoped claim: RFC-0003's amendment, the research note and the capability crate's documentation all already state the scoped version. RFC-0003 SS6 and the research note still quote the old sentence, deliberately unedited, as the historical record of what was reviewed. Logged in docs/CHANGELOG.md, as constitutional amendments always are. Co-Authored-By: Claude Fable 5 --- CONSTITUTION.md | 4 +++- docs/CHANGELOG.md | 13 +++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/CONSTITUTION.md b/CONSTITUTION.md index d88f9d5..88725f4 100644 --- a/CONSTITUTION.md +++ b/CONSTITUTION.md @@ -70,7 +70,9 @@ The kernel is hand-written and minimal. It provides mechanism, never policy. taking the system down. *(Redox, QNX)* - **Capabilities are the only authority.** Unforgeable, kernel-validated, explicitly passed, and reducible in rights. Rust's ownership and move - semantics model capability transfer at compile time. *(seL4; Fuchsia's + semantics model the kernel's own capability handling at compile time — no + accidental duplication or use-after-move; cross-process transfer is a + 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)* diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 322c065..8e6218a 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -110,6 +110,19 @@ recorded is indistinguishable from law that was never agreed. ### Changed +- **Constitution §3 amended, on the maintainer's authorisation (2026-08-01): the compile-time claim + is scoped.** The kernel-doctrine slogan "Rust's ownership and move semantics model capability + transfer at compile time" now reads "…model the kernel's own capability handling at compile time — + no accidental duplication or use-after-move; cross-process transfer is a runtime table operation + the generation scheme secures" — the reword the 2026-07-30 prior-art review recommended and flagged + below, taken exactly as flagged. The borrow checker sees one compilation unit: it genuinely forbids + a kernel-side capability being duplicated or used after a move (the no-`Clone` `Capability` in the + capability crate makes that a compiler-checked property), but what a *process* observes when + authority transfers is a runtime table operation, and the generation checks are what secure it — + which is why they exist at all. With this amendment the constitution agrees with RFC-0003's + amendment, the research note and the capability crate's own documentation; it had become the last + place in the repository making the unscoped claim. RFC-0003 §6 and the research note still quote + the old sentence, deliberately unedited — they are the historical record of what was reviewed. - **RFC-0004 revised** (prior-art review, 2026-07-30): its spine held, but four corrections were folded in. **§5 no longer maps pages during IPC** — that is L4's abandoned "long IPC", removed by every modern L4 and hostile to verification; bulk data now goes through a shared `Region` capability