docs: reconcile and fact-check RFC-0005, RFC-0006 and RFC-0007

[MatejGomboc]

Pull Request

Summary

RFC-0005, RFC-0006 and RFC-0007 (all still proposed) were revised in parallel and had drifted apart where they meet. This PR reconciles them and settles every claim they had flagged as unverified. It is the follow-up to #22's hand-off, items 1–3. Draft: a line-by-line proofread and an audit against the constitution's vision are still running, and their fixes will land here before it is marked ready.

Explanation for the maintainer

Seams closed between the three RFCs. Each fix is made in the RFC that owns the subject:

• Naming: RFC-0005 called RFC-0006's per-core time object Core; RFC-0006 calls it SchedControl, and RFC-0005 now does too.
• Accounting domain: RFC-0006 claimed to answer RFC-0005's open question 2, which is about donation. Both now state the same split: kernel memory in Pools, time through SchedControl, any unified domain left to the broker RFC.
• nTWE: RFC-0006 asked RFC-0005 to correct a bit RFC-0005 had already corrected. The stale demand is gone.
• Reply objects: RFC-0006 still treated them as single-use and destroyed. It now follows RFC-0007's proposed amendment (reusable, unbound), so a late reply fails PeerGone.
• Moving an endpoint into a TCB (set_fault_ep/set_timeout_ep) now requires TRANSFER, as RFC-0003 §6 requires for every move.
• region_copy: RFC-0007 proposed it into RFC-0005's domain, but RFC-0005 never had it. It now has an operations-table row, refusal rules, a W^X layer-2 entry (refused while the destination has an RX mapping), and a place in increment 14.
• The console: RFC-0006 still budgeted for a 44 ms non-preemptible console write. RFC-0007's console never waits (24 bytes at most), so that interim, and the MIN_BUDGET floor derived from it, are gone.
• reissue: RFC-0005 no longer proposes it, and RFC-0006 no longer cites it.
• Stack overflow: RFC-0005 relied on an overflow path that RFC-0006 never designed. RFC-0006 §9 now designs it: AArch64 vectors test SP and switch to an emergency stack; x86_64 escalates to #DF on an IST. Both follow Linux.
• The boot stack: two increments both claimed to move it. RFC-0005 docs: prior-art review — validate the spine, prune one legacy, correct RFC-0004 #10 owns it.
• Implementation order: there were three orders and they disagreed. RFC-0005 also said RFC-0006 feat(arch): exception vectors and a reporter that names the fault #4 needed the stack window, and RFC-0007 landed RFC-0005 Record RFC-0004's acceptance #14 before the dispatcher it needs. There is now one merged order, in RFC-0007 §18, in four stages; the other two RFCs state only their constraints and defer to it. RFC-0006 docs(threat-model): expand §9 into the authoritative threat model #5 now correctly waits for address spaces (RFC-0005 Amend Constitution §3: scope the compile-time capability claim #13).

Facts settled. An independent fact-checker checked each claim against primary sources: QEMU 11.0.3's source and probe boots on it, seL4's kernel and RFC-14, Arm's SysReg descriptions, the Intel SDM, Linux and TF-A. Nearly everything held. The corrections:

• DTB placement is stated mechanically: for an ELF at 0x4000_0000 the DTB goes to physical 0x0, the flash window, not RAM.
• load_elf lives in elf_ops.h.inc at 11.0.3, and its bound is p_filesz.
• The TLB no-caching rule now cites Arm ARM D8.12 and SDM §4.10.2.3, plus the caveat that a permission-faulting entry may be cached, which is why protect invalidates.
• SCTLR_EL1's RES1 bits are named and sourced. QEMU's reset value lacks three of them, which is why the register is written whole.
• RFC-14 is now quoted exactly: the threshold rule, the deferral, and the performance figures (22% on the Call fastpath, 21% on ReplyRecv). Its "one-layer return" is attributed to its budget-limit mechanism, which this RFC applies to plain expiry.
• The GIC: ARE is RAO/WI with one security state.
• CNTKCTL_EL1 and PMUSERENR_EL0 reset to an architecturally UNKNOWN value.
• PSCI and -initrd behaviour was re-checked on 11.0.3.

No verdict changed in substance; RFC-0005's verdict 7 now names region_copy. docs/CHANGELOG.md corrects three entries: thirteen demo increments, not fourteen; SchedControl; and RFC-0006's entry describes the document rather than how it was drafted. It also gains a dated Changed entry for this pass.

Which pillar does this serve?

Toil: design-document coherence (Constitution §5.4, "coherence over accumulation"), ahead of the maintainer's verdicts on the three RFCs.

If this changes a document or the constitution

• Cross-references still resolve; no clause is left contradicting another (every RFC-000N §M reference checked by script; semantic spot-checks of RFC-0003 §7, §9, §11, §14)
• If this is a constitution amendment, it is the maintainer's, and docs/CHANGELOG.md records it (no constitution change)
• 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 new files)

unsafe register

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

Checklist

• markdownlint-cli2 clean locally; British spelling script clean
• Line-by-line proofread findings applied (in progress)
• Vision audit findings applied (in progress)

🤖 Generated with Claude Code

https://claude.ai/code/session_01D1gBBT3tN99wzeJjf3tLWW

---

Generated by Claude Code