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

[MatejGomboc]

Summary

The thirteen flag-only findings from the bug-hunt PR (#19), resolved as the maintainer ruled today and applied on that authorisation. Stacked on #19 — the base is fix/comprehensive-sweep, and GitHub will retarget this PR to main automatically when #19 merges and its branch is deleted. Review only the one commit here.

Explanation for the maintainer

You made four rulings; this PR is those rulings and nothing else:

1. Constitution §3 and §7 amended (your authorisation, this session). §3's "zero-copy page transfer for large ones (L4)" was 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. (L4, as corrected by RFC-0004)", which also re-agrees with the README fixed in Repository-wide bug sweep: fail-closed xtask, honest comments, dead configuration removed #19. §7 now names aarch64-unknown-none-softfloat — it had named the plain triple the project's own changelog records as fatal.
2. RFC-0004 corrected in two places, plus this changelog's transcription. The acceptance note said the copy-vs-map verdict joins the MMU RFC; the revised body it accepted had already settled that by pruning map, so the note (and docs/CHANGELOG.md's faithful transcription of it) now names shared-memory establishment as what joins the MMU RFC. §5's "~100 cycle" figure is re-attributed to the earlier C++ blueprint — constitution §3 never contained a cycle figure, as git log -S confirms.
3. RFC-0003 and RFC-0001 gain dated amendments. RFC-0003's scopes §6's "records the parent" to what the built flat table actually promises (a test pins the absence of a parent link; the record-or-not decision is RFC-0003a's), and the header's Discharges field now says of O-3 what §13 already did: destruction case only. RFC-0001's re-runs its graves check against §3's grown list of seven — none of the three additions applies to a userspace store, and the section's own recorded risk is precisely the first new grave.
4. Threat model §6's Built definition tightened rather than promoting O-1/O-2: Built now requires enforcement at the boundary the obligation guards. O-1 and O-2 gain notes that the mechanism is host-proven in the capability crate and binds at B1 when the syscall surface lands. The ratio stays three of twenty-seven, now unambiguous.

Which pillar does this serve?

Documents before code (§5.5), directly: every one of these is the paper record being brought back into agreement with the decisions it exists to record.

If this changes a document or the constitution

• Cross-references still resolve; no clause is left contradicting another — repo-wide grep confirms the only surviving "zero-copy page transfer" occurrences are the two changelog records describing this correction
• The constitution amendments are the maintainer's (authorised this session, rulings recorded in the conversation), and docs/CHANGELOG.md records every change here, dated
• No section other documents cite has been renumbered

Borrow Ledger

• I checked the Borrow Ledger (CONSTITUTION.md §4) for this subsystem
• The verdict for this subsystem is: n/a (documents only)
• Vendored code retains its original licence notices; new files carry an SPDX header (no files added)

unsafe register

• New unsafe blocks: None
• Every new unsafe block carries a // SAFETY: comment (n/a)
• Every unsafe block is inside a module CLAUDE.md designates for it (n/a)
• I have listed them in the session summary / PR description above

Checklist

• Builds for both Tier-1 targets — no code touched; CI re-proves it
• Clippy passes — no code touched; CI re-proves it
• Formatted — no Rust touched
• Toolchain pins agree (bash .github/scripts/check-toolchain-pin.sh)
• British spelling (bash .github/scripts/check-british-spelling.sh — clean, 65 files)
• Markdown is lint-clean (markdownlint-cli2 "**/*.md" — 0 issues in 21 files)
• Boots in QEMU where applicable (n/a — documents only)
• docs/CHANGELOG.md updated — five entries, one per ruling plus the transcription note
• Commit messages follow Conventional Commits (see CONTRIBUTING.md)
• Commit GPG-signed

Related

Resolves the "Flagged for you, not taken" section of #19.

🤖 Generated with Claude Code