diff --git a/CLAUDE.md b/CLAUDE.md
index e58c265..bda7cbf 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -134,3 +134,11 @@ every rebuild.
 ## Licence
 
 GPLv3 — see [LICENCE](LICENCE). New files carry an SPDX header.
+
+The design documents cite Linux, the seL4 kernel and QEMU down to the file. Read and
+cite them freely; copy from them never. Linux and seL4's kernel code are
+GPL-2.0-only, which cannot be combined with this GPLv3 tree; QEMU is GPL version 2
+as a whole and licensed file by file, so even its GPL-2.0-or-later parts would need
+a per-file provenance check that `vendor/`, which takes MIT code, does not provide
+for. An increment re-derives the mechanism from the architecture manuals and the
+cited design, in its own words and code.
diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md
index 8989bba..57f03f2 100644
--- a/docs/CHANGELOG.md
+++ b/docs/CHANGELOG.md
@@ -15,34 +15,34 @@ recorded is indistinguishable from law that was never agreed.
 - `docs/rfcs/0005-address-spaces-and-physical-memory.md` — **proposed**, the memory half of Phase 1 and
   the first of three interlocking kernel RFCs drafted together with RFC-0006 and RFC-0007. Physical
   memory comes from firmware tables into one bounded `MemoryMap` (the image moves to 0x4020_0000 because
-  QEMU places no DTB for an ELF at the base of RAM), and a colour-capable bitmap hands out frames. O-7's
+  QEMU puts no DTB in RAM for an ELF loaded at its base), and a colour-capable bitmap hands out frames. O-7's
   "who pays" is answered with typed fixed-capacity slot arrays reused by generation and a
   capability-named `Pool` charged for every post-boot frame and slot, `map`'s tables included. The Pool
-  is declared the single accounting domain for counted units, with CPU time left to RFC-0006's `Core`: a
+  is declared the single accounting domain for counted units, with CPU time left to RFC-0006's `SchedControl`: a
   stated split from research/0002. `Region` and `AddressSpace` join RFC-0003's objects, and `EXECUTE`
   joins its rights as bit 5 by a proposed dated amendment. W^X (O-13) holds in four layers, including per
   Region across every address space, backed by `SCTLR_EL1.WXN`, whose full value the RFC states. O-5
   becomes a structural rule: the kernel never dereferences a user virtual address. The SMP shootdown and
   ASID-rollover protocol is designed now rather than bolted on later. Donation (`reissue`) is
   deliberately not proposed but handed to RFC-0003a as input, because gating it on `REVOKE` would
-  pre-empt that RFC's (a)/(b) choice. Twenty increments, fourteen marked for the Phase-1 demo, each with
-  the interims it carries named and costed.
-- `docs/rfcs/0006-threads-and-scheduling.md` — **proposed**, revised the same day against a three-lens
-  review (constitution, technical correctness and implementability). Threads, scheduling contexts and
-  interrupts for Phase 1. The spine is unchanged. The kernel is event-driven, with one stack per core and
-  preemption points, and time is a capability: a `SchedContext` configured only through a per-core
-  `SchedControl` (seL4 MCS). Priorities are 256 fixed levels behind a priority ceiling that any
-  capability to a thread confers. The timer is tickless on both Tier-1 targets. FP/SIMD is enabled per
-  thread and saved lazily. A device line reaches its driver as a notification and stays masked until
-  `ack`. The review turned several quiet choices into verdicts. Endpoint queues are now priority-ordered,
-  because the FIFO citation was wrong. Budgets are declared caps, not minima, departing from
-  research/0002 on purpose. Userspace timers are named: deadline objects on the release queue. A caller's
-  death can no longer take time away from a server mid-request. The departures from accepted papers are
-  now listed as amendments A1–A4: donation only to passive receivers, a short caller waits instead of
-  being refused, seL4's timeout faults corrected, and the big lock rejecting RFC-0003 §14.2's premise.
-  The review also fixed the state machine (a tenth state, `Unfunded`), the FP ownership races, the SCTLR
-  bits RFC-0005 had inverted, and the parked-core start-up (checked against QEMU). The increments now
-  interlock with RFC-0005 and RFC-0007. The demo's interims are named with their numbers.
+  pre-empt that RFC's (a)/(b) choice. Twenty increments, thirteen marked for the Phase-1 demo, with
+  the interims the demo carries named and costed.
+- `docs/rfcs/0006-threads-and-scheduling.md` — **proposed**, threads, scheduling contexts and interrupts
+  for Phase 1, drafted alongside RFC-0005 and RFC-0007 and revised against a three-lens review
+  (constitution, technical correctness and implementability). The kernel is event-driven, with one stack
+  per core and preemption points, and time is a capability: a `SchedContext` configured only through a
+  per-core `SchedControl` (seL4 MCS). Priorities are 256 fixed levels behind a priority ceiling that any
+  capability to a thread confers, and endpoint queues are priority-ordered. Budgets are caps, not minima,
+  departing from research/0002 on purpose. The timer is tickless on both Tier-1 targets, and userspace
+  timers are named as deadline objects on the release queue. FP/SIMD is enabled per thread and saved
+  lazily. A device line reaches its driver as a notification and stays masked until `ack`. A caller's
+  death never takes time away from a server mid-request. Its departures from accepted papers and from
+  research/0002 are listed as amendments A1–A6: donation only to passive receivers, a short caller waits
+  instead of being refused, the claim that seL4's timeout faults remain future work corrected, the big
+  lock rejecting RFC-0003 §14.2's premise, budgets as caps, and capabilities held in a thread's fault
+  slots. Because A1 narrows the constitution's priority inheritance, the RFC also names that as a
+  question for the maintainer (C1) rather than amending the constitution itself. The demo's interims are
+  named with their numbers.
 - `docs/rfcs/0007-system-calls-and-process-bootstrap.md` — **proposed**, the third of the Phase-1 kernel
   RFCs drafted alongside RFC-0005 and RFC-0006, and the one that makes RFC-0003 §9 live. Every
   kernel-object operation is a `call` on its capability (seL4's uniform invocation), with twelve syscalls
@@ -54,7 +54,7 @@ recorded is indistinguishable from law that was never agreed.
   states honestly what that window does not close: a spawner that keeps the child's AddressSpace keeps
   control. There is one root task with every boot capability listed in BootInfo, and no kernel branch on
   "is root". The kernel never parses ELF. The console is a capability that never waits. The `user/abi`
-  binding gets a third designated `unsafe` tree, limited to trap instructions and entry stubs. It
+  binding gets a third designated `unsafe` tree, limited to trap instructions, a register read and entry stubs. It
   proposes dated amendments to RFC-0003 (the handle word) and RFC-0004 (reusable reply objects), and
   names every demo interim with its cost.
 - `docs/research/0002-virtualisation-and-containment-prior-art.md` — the second prior-art review, on
@@ -172,6 +172,39 @@ recorded is indistinguishable from law that was never agreed.
 
 ### Changed
 
+- **A third designated `unsafe` tree approved in principle (2026-09-27), binding nothing yet.** Asked in
+  a Claude Code session how the demo's userspace should issue `svc #0`, the maintainer approved in
+  principle a small write-ourselves crate, `user/abi`, whose `src/arch/**` would become a third tree
+  where `unsafe` is permitted, beside `kernel/src/arch/**` and `kernel/src/mm/**` — to be proposed in the
+  syscall RFC and accepted or rejected there. RFC-0007 (proposed) §12 has since narrowed the tree to trap
+  instructions, the discovery-register read and process entry stubs. Nothing changes until RFC-0007 is
+  accepted: `CLAUDE.md`'s `unsafe` policy, threat-model O-6 and the workspace lint comments move only
+  with its increment 7, and the Borrow Ledger reading it seeks is a separate verdict. Recorded so the
+  decision has a trace in the repository, not only in a chat.
+- **RFC-0005, RFC-0006 and RFC-0007 reconciled and fact-checked (2026-10-02), still proposed.** The three
+  were revised in parallel and had drifted at their seams; a cross-RFC pass aligned them, and an
+  independent check of every claim they had flagged as unverified settled each against primary sources:
+  QEMU 11.0.3's source and experiments on it, seL4's kernel and RFC-14, Arm's register descriptions, the
+  Intel SDM, Linux and TF-A. Seams closed: RFC-0005 names RFC-0006's `SchedControl`, not `Core`, and
+  adopts RFC-0007's `region_copy` into its operations table and W^X counts; RFC-0006 follows RFC-0007's
+  reusable reply objects, requires `TRANSFER` to move an endpoint into a thread, drops a 44 ms console
+  interim that RFC-0007's never-waiting console had made obsolete, and designs the kernel stack-overflow
+  path RFC-0005 relied on; the three implementation orders become one, in RFC-0007 §18. Facts settled:
+  DTB placement and `-initrd` on QEMU 11.0.3; the TLB no-caching rule cited to the Arm ARM (D8.12) and
+  the SDM (§4.10.2.3), with the permission-fault caveat that makes `protect` invalidate; `SCTLR_EL1`'s
+  RES1 bits named and sourced; RFC-14's threshold rule, deferral and performance figures quoted, and its
+  one-layer return attributed to its budget-limit mechanism. A line-by-line proofread then fixed
+  seventy-two smaller defects — argument orders matched to RFC-0007's encoding, verdicts and state tables
+  made to agree with their bodies, the `wfi` and FP/SIMD traps RFC-0007 had counted as faults, a
+  constitution pointer to a non-existent §11.1, and wrapping. An independent audit against the
+  constitution found the three on its vision in substance, and its editorial findings are applied: the
+  kernel's store is renamed the object store, so it no longer collides with the content-addressed store;
+  RFC-0006's amendment table gains A5 (budgets as caps) and A6 (capabilities resting in a thread), and
+  raises its narrowing of priority inheritance as a constitutional question for the maintainer (C1);
+  RFC-0007 names the missing receive-side badge register and the rule that the root must not become the
+  broker; and `CLAUDE.md` § Licence says that GPL-2.0 sources are cited, never copied. No verdict changed
+  in substance: RFC-0005's verdict 7 now names `region_copy`, and RFC-0006's verdict 12 lists the
+  amendments its body already implied.
 - **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
diff --git a/docs/rfcs/0005-address-spaces-and-physical-memory.md b/docs/rfcs/0005-address-spaces-and-physical-memory.md
index 2a9c1e0..12030fe 100644
--- a/docs/rfcs/0005-address-spaces-and-physical-memory.md
+++ b/docs/rfcs/0005-address-spaces-and-physical-memory.md
@@ -7,7 +7,7 @@
 | Status | **Proposed** — 2026-09-27, awaiting the maintainer's verdict |
 | Author | Drafted by Claude Code as sparring partner; verdict the maintainer's |
 | Date | 2026-09-27 |
-| Affects | Constitution §3 (kernel doctrine) and §11.1's "minimal assembly" (§17.7); RFC-0003 (a dated amendment adding one right; three new objects; `capability/src/rights.rs` and `object.rs`'s doc comment); RFC-0004 §9.1; the boot stub, `aarch64.ld` and the exception reporter; `kernel/src/mm/**`; a new host-tested `memory/` crate; threat model §10 and O-7's text (proposals via `docs/CHANGELOG.md`) |
+| Affects | Constitution §3 (kernel doctrine) and the Language clause's "minimal assembly" (§17.7); RFC-0003 (a dated amendment adding one right; three new objects; `capability/src/rights.rs` and `object.rs`'s doc comment); RFC-0004 §9.1; the boot stub, `aarch64.ld` and the exception reporter; `kernel/src/mm/**`; a new host-tested `memory/` crate; threat model §10 and O-7's text (proposals via `docs/CHANGELOG.md`) |
 | Depends on | RFC-0003 (capability table), RFC-0004 (IPC); interlocks with RFC-0006 (threads and scheduling) and RFC-0007 (system calls and process bootstrap), proposed the same day |
 | Discharges | O-7 for kernel allocation (reclaim across a transfer stays open), O-8, O-13 (the mapping half); O-5 for every path by which the kernel touches user memory; O-3's destruction case extended to memory; answers RFC-0003 §14.3 and RFC-0004 §9.1 (share) |
 
@@ -16,15 +16,15 @@
 > 1. **[demo] Discovery:** firmware tables into one bounded `MemoryMap`; the image moves to 0x4020_0000, where QEMU leaves room for the DTB (§4).
 > 2. **[demo] Frames:** a colour-capable bitmap; fresh frames and table frames zeroed, boot data handed over read-only (§4, §7).
 > 3. **[demo] Who pays (O-7):** typed slot arrays reused by generation; every post-boot unit charged to a Pool named by capability, `map`'s too (§5).
-> 4. **[demo] One accounting domain:** the Pool, for every counted unit; time stays with RFC-0006's `Core`, a stated split from research/0002 (§5).
+> 4. **[demo] One accounting domain:** the Pool, for every counted unit; time stays with RFC-0006's `SchedControl`, a stated split from research/0002 (§5).
 > 5. **[demo] Layout:** the same higher-half layout on both; the image read-only in the physmap; per-core stacks guarded, kept by the kernel (§6).
 > 6. **[demo] Objects:** `Region` (eager and zeroed, or boot-minted read-only) and `AddressSpace` join RFC-0003's objects beside `Pool` (§7).
-> 7. **[demo] Operations:** `map` / `unmap` / `protect` are capability-checked, bounded and atomic; the kernel never picks an address (§8).
+> 7. **[demo] Operations:** `map` / `unmap` / `protect` and `region_copy` are capability-checked, bounded and atomic; the kernel never picks an address (§8).
 > 8. **[demo] Rights:** `EXECUTE` joins RFC-0003's set as bit 5 — on Regions and Pools only, refused at mint elsewhere — by dated amendment (§8).
 > 9. **[demo] W^X (O-13):** unrepresentable, enforced per Region across all address spaces, backed by `SCTLR_EL1.WXN` (§9).
 > 10. **Sharing (RFC-0004 §9.1):** *share* is derive-and-transfer; destruction walks mappings; *donation* goes to RFC-0003a as input (§10).
 > 11. **[demo] User memory (O-5):** the kernel never dereferences a user virtual address; a carried one is a number, validated as one (§11).
-> 12. **TLB:** kernel-private, recycled tags; this RFC owns SMP shootdown and rollover, RFC-0006 provides the IPI; single-core half [demo] (§12).
+> 12. **TLB:** kernel-private, recycled tags; this RFC owns SMP shootdown and rollover; RFC-0006 provides the IPI; single-core half [demo] (§12).
 > 13. **[demo] Early boot:** the stub enables the MMU with a stated `SCTLR_EL1`; Rust runs only high and installs the final W^X map (§13).
 
 ## 1. The question
@@ -56,9 +56,9 @@ and 47-bit user and kernel halves whose top level uses 256 entries each** — AA
 | Accessed | `AF` (bit 10), set by software on this CPU | bit 5 (A), set by hardware |
 | Address-space tag | 16-bit ASID in `TTBR0_EL1[63:48]` | 12-bit PCID in `CR3[11:0]` |
 
-*(Checked against Linux's `arch/arm64/include/asm/pgtable-hwdef.h` — Arm's site was unreachable — and SDM
-Vol. 3A §4.5. QEMU's `cortex-a72` has 44-bit physical addresses, 16-bit ASIDs, no hardware access flag and
-no PAN: `target/arm/tcg/cpu64.c`, `ID_AA64MMFR0_EL1 = 0x1124`, `MMFR1` 0.)* Hence **one table engine**,
+*(Checked against Linux's `arch/arm64/include/asm/pgtable-hwdef.h` and SDM Vol. 3A
+§4.5. QEMU's `cortex-a72` has 44-bit physical addresses, 16-bit ASIDs, no hardware access flag and
+no PAN: `target/arm/tcg/cpu64.c`, `ID_AA64MMFR0_EL1 = 0x1124`, `ID_AA64MMFR1_EL1` 0.)* Hence **one table engine**,
 generic over a `Descriptor` encoder and a frame-access trait, host-tested in `memory/`; only turning a frame
 number into `&mut [u64; 512]` through a kernel window (§6, §13) is `unsafe`, in `kernel/src/mm/`.
 
@@ -66,9 +66,11 @@ number into `&mut [u64; 512]` through a kernel window (§6, §13) is `unsafe`, i
 
 **Discovery.** QEMU fixes RAM at 0x4000_0000 on `virt`; every other address "may vary" and comes from the
 DTB, "at the start of RAM" with no register naming it (`docs/system/arm/virt.rst`) — and `hw/arm/boot.c`
-puts it only *below* the image (`dtb_limit`). Checked on QEMU 8.2.2 on 2026-09-27: an ELF at 0x4000_0000
-finds **no DTB in RAM**; at 0x4020_0000 it finds one at 0x4000_0000. **So the image loads at 0x4020_0000**,
-capping the DTB at 2 MiB; increment 1 re-checks QEMU 11.0.3. A minimal FDT reader (Borrow Ledger boot-path
+puts it only *below* the image (`dtb_limit`). Checked on QEMU 8.2.2 and the pinned 11.0.3
+(`arm_setup_direct_kernel_boot`): an ELF at 0x4000_0000 gets the DTB written at physical 0x0 — the flash window,
+not RAM — and nothing in `x0`; at 0x4020_0000 it lands at 0x4000_0000 (`dtb_start = loader_start`, `dtb_limit =
+image_low_addr`), and `arm_load_dtb` silently drops a DTB that does not fit below the image. **So the image loads
+at 0x4020_0000**, capping the DTB at 2 MiB (`virt`'s is 1 MiB). A minimal FDT reader (Borrow Ledger boot-path
 row; Devicetree Specification v0.4) reads the cell sizes, `/memory`, `/memreserve/` and `/reserved-memory`,
 bounds-checks every offset and fails closed; threat model §10 gains a proposed assumption, *firmware tables
 describe memory truthfully*. x86_64's UEFI stub (no RFC yet) hands over `GetMemoryMap` after
@@ -94,7 +96,7 @@ amendment), and makes object layouts ABI: **rejected**. **B — a heap with crea
 (research/0002 Part 6): **rejected alone**. **D — C with counted attribution: verdict sought** *(the requester
 pays, as in seL4; counted quotas, as in Fiasco.OC's factory limits and Genode's quota trading)*.
 
-**The store is typed slot arrays**, one fixed-capacity array per type in `.bss`; a slot holds the object, a
+**The object store is typed slot arrays**, one fixed-capacity array per type in `.bss`; a slot holds the object, a
 generation and a count. The kernel's implementation of `ObjectRef` (`capability/src/object.rs`, a trait) is
 `(type, index, generation)`; `current_generation()` is a slot read. **Only live references count** —
 capabilities at the slot's current generation, Mappings, IPC-buffer bindings; one at any other generation
@@ -104,7 +106,7 @@ pins another's charge. A slot whose generation cannot advance retires, debited o
 keep 64-bit generations, RFC-0007 (proposed) §6). `object.rs`'s "takes a reference count" is qualified to
 match in increment 7. **Where it lives:** generic array and Pool in `memory/`; the concrete store, one
 `Kernel` value with every type's array (RFC-0004/0006/0007 objects too), behind **one** `static` in
-`kernel/src/mm/` whose SAFETY argument is one core entered with interrupts masked (RFC-0006 (proposed) V1),
+`kernel/src/mm/` whose SAFETY argument is one core entered with interrupts masked (RFC-0006 (proposed) verdict 1),
 then the big lock. No other kernel global accretes.
 
 **A Pool is the accounting layer**: an RFC-0003 object holding balances of frames and of each type's slots.
@@ -115,7 +117,7 @@ At boot every free unit becomes the balance of one root Pool (RFC-0007 (proposed
 every unit of r in use       ==  kept by the kernel (at boot, or retired), or charged to exactly one Pool
 ```
 
-- **Charged:** Region frames; every object slot; table frames and the `Mapping` slot, to the Pool `map`
+- **Charged:** Region frames; every object slot; table frames and the Mapping slot, to the Pool `map`
   names (§8). **Kept, never charged:** image, bitmap, arrays, kernel tables, per-core stacks, boot-minted
   Regions (§7). Every charge presents a Pool with `WRITE`.
 - **Charge first, then take**, so the only later failure, `Fragmented`, refunds before returning.
@@ -130,9 +132,11 @@ every unit of r in use       ==  kept by the kernel (at boot, or retired), or ch
 **One accounting domain — decided here, as the programme gives this RFC O-7's model.** research/0002 Part 6
 wants one for memory, object quotas and scheduling contexts. **The Pool is it for every counted unit**,
 SchedContext slots included. **Time is not a unit**: RFC-0006 (proposed) sells per-core bandwidth through
-`Core`, which moving balance cannot conserve, and folding it in would make every Pool holder a CPU seller — a
-deliberate split, congruent by attribution. O-7 would add *"kernel memory is charged to a capability-named
-Pool; CPU time to a SchedContext funded through a `Core`"*, via `docs/CHANGELOG.md`.
+`SchedControl`, which moving balance cannot conserve, and folding it in would make every Pool holder a CPU
+seller — a deliberate split, congruent by attribution; RFC-0006 (proposed) §5 states the same split from its
+side, and leaves any later domain holding both to the broker RFC. O-7 would add *"kernel memory is charged to
+a capability-named Pool; CPU time to a SchedContext configured through a `SchedControl`"*, via
+`docs/CHANGELOG.md`.
 
 ## 6. The kernel's virtual layout
 
@@ -147,10 +151,11 @@ top 2 GiB, as `x86_64-unknown-none`'s default kernel code model expects (overrid
 | `0xFFFF_FFFF_0000_0000` – `0xFFFF_FFFF_7FFF_FFFF` | per-core kernel and emergency stacks, an unmapped guard page below each | Normal; RW; execute-never; kept by the kernel at boot |
 | `0xFFFF_FFFF_8000_0000` – top | image at `+0x20_0000` | `.text` RX, `.rodata` R, `.data`/`.bss` RW execute-never |
 
-- **Stacks.** RFC-0006 (proposed) V1 chose one kernel stack per core, allocated here at boot; core 0's boot
-  stack leaves `aarch64.ld`'s unguarded slot in increment 10. A fault's entry pushes onto the overflowed
-  stack, so **RFC-0006 (proposed) provides the overflow stack** (x86_64 IST; AArch64's EL1-origin vector
-  moving to the emergency stack, a kernel fault being fatal). Until then an overflow is a recursive abort.
+- **Stacks.** RFC-0006 (proposed) verdict 1 chose one kernel stack per core, allocated here at boot; core 0's
+  boot stack leaves `aarch64.ld`'s unguarded slot in increment 10. A fault's entry pushes onto the overflowed
+  stack, so **RFC-0006 (proposed) §9 provides the overflow path** (x86_64 `#DF` on an IST; AArch64's
+  current-EL vector testing `SP` and moving to the emergency stack, a kernel fault being fatal). Until then an
+  overflow is a recursive abort.
 - **The user floor is 64 KiB** *(Linux `mmap_min_addr`)*; **the ceiling leaves the last page below the hole
   unmapped**, closing Intel's `SYSRET` hazard (CVE-2012-0217) for RFC-0007 by layout. The physmap is RAM only.
 - **The kernel's top-level entries never change after boot.** AArch64 shares `TTBR1_EL1`; x86_64 copies PML4
@@ -167,7 +172,7 @@ frames, with rights `READ`, `WRITE`, `EXECUTE` and RFC-0003's `DUPLICATE`, `TRAN
 and IPC-buffer bindings hold counted references, so closing the last capability does not pull memory from
 under a live mapping *(Zircon: a mapping keeps its VMO alive)*. One object, three kinds:
 
-- **Ordinary** (`region_create`): eager, zeroed, charged; unmet in eight extents it fails `Fragmented`; DMA
+- **Ordinary** (`region_create`): eager, zeroed, charged; unmet within `max_extents` it fails `Fragmented`; DMA
   memory is one extent at an alignment. Zeroing runs 512 pages per step between RFC-0006 (proposed)'s
   preemption points, the half-built Region held on the caller's thread; no capability exists until done.
 - **Boot-minted, read-only**, over the DTB and each boot module RFC-0007 (proposed) embeds (every segment
@@ -181,11 +186,12 @@ What the kernel fills for the root before handover (writable segments, stack, Bo
 Regions, charged to the root Pool, bytes copied in through the physmap, and only then a capability minted.
 **An AddressSpace** is a user root table, a tag (§12), the Pool paying for its tables — the only Pool `map`
 may charge — and its mappings; `WRITE` permits `map`/`unmap`/`protect`, `READ` a query; binding it to a
-process is RFC-0007's. **A Mapping** is a charged kernel record, not a capability: `{as, region, first_page,
-vaddr, pages, perms}`, linked into its AddressSpace's list and its Region's, because RFC-0003's 2026-07-30
-amendment makes load-bearing that *a resolved capability is never cached outside the kernel table* — and **a
-page-table entry is exactly such a cache**. *Rejected:* **Zircon VMOs and VMARs** (lazy commit, copy-on-write,
-pagers, nesting: policy, and faults in kernel paths); **seL4's capability per frame**; **user-built tables** (Xen PV).
+process is RFC-0007's. **A Mapping** is a charged kernel record, not a capability:
+`{as, region, first_page, vaddr, pages, perms}`, linked into its AddressSpace's list and its Region's, because
+RFC-0003's 2026-07-30 amendment makes load-bearing that *a resolved capability is never cached outside the
+kernel table* — and **a page-table entry is exactly such a cache**. *Rejected:* **Zircon VMOs and VMARs**
+(lazy commit, copy-on-write, pagers, nesting: policy, and faults in kernel paths); **seL4's capability per
+frame**; **user-built tables** (Xen PV).
 
 ## 8. Map, unmap, protect — and the rights they check
 
@@ -195,11 +201,12 @@ transferred — RFC-0003 §6's move would take the Region from its mapper.
 
 | Operation | Needs | Refused when |
 |-----------|-------|--------------|
-| `region_create(pool, pages, max_extents, align, rights)` | pool `WRITE`; pool `EXECUTE` if `rights` has it | `PoolExhausted`; `Fragmented`; zero pages; `align` not a power-of-two page count; `rights` not Region rights |
+| `region_create(pool, pages, align, max_extents, rights)` | pool `WRITE`; pool `EXECUTE` if `rights` has it | `PoolExhausted`; `Fragmented`; zero pages; `align` not a power-of-two page count; `rights` not Region rights |
 | `as_create(pool, rights)` | pool `WRITE` | `PoolExhausted` |
-| `map(as, region, pool, first_page, vaddr, pages, perms)` | as `WRITE`; region rights ⊇ `perms`; `pool` the AddressSpace's own, `WRITE` | `vaddr` unaligned, below the floor or outside the user half; overlap; beyond the Region; `pages > 512`; `perms ∉ {R, RW, RX}`; W^X (§9); `PoolExhausted` |
+| `map(as, region, pool, vaddr, first_page, pages, perms)` | as `WRITE`; region rights ⊇ `perms`; `pool` the AddressSpace's own, `WRITE` | `vaddr` unaligned, below the floor or outside the user half; overlap; beyond the Region; `pages > 512`; `perms ∉ {R, RW, RX}`; W^X (§9); `PoolExhausted` |
 | `unmap(as, vaddr)` | as `WRITE` | no mapping based at `vaddr` — the unit is the whole mapping |
 | `protect(as, vaddr, perms)` | as `WRITE` | `perms` not a subset of the mapping's current `perms` |
+| `region_copy(dst, src, src_page, dst_page, pages)` | dst `WRITE`; src presented, `READ` | `pages` 0 or above 16; either range beyond its Region; both ranges in one Region and overlapping; `dst` has an `RX` mapping (§9) |
 
 User numbers are validated *as numbers*; **the kernel never chooses a virtual address** *(seL4's VSpace
 discipline)*. **`map` names a Pool because spending is authority** (O-4); requiring the space's *own* Pool
@@ -208,6 +215,10 @@ keeps one payer per space, so refunds need no per-table record *(seL4's caller-s
 (spending never granted). **`map` is atomic**: it charges missing tables and the Mapping slot first, then
 zeroes and links tables, writes leaves and ends with `DSB ISHST` before `eret`; at most 512 leaves and six
 new tables. `protect` only narrows; widening is `map` again *(seL4)*. 4 KiB pages; blocks later.
+**`region_copy`** copies whole pages frame to frame through the physmap, at most 16 per call so one entry's
+copy stays bounded: it is how a loader fills a child's data pages without mapping them into itself (RFC-0007
+(proposed) §10), and the kernel's own fill for the root (§7) is the same copy. It writes, so W^X counts it
+(§9). Its RFC-0007 encoding presents `src`, as `map` presents its Region.
 
 **Verdict sought: `EXECUTE` joins RFC-0003's rights as bit 5**, as §5 there allows "when a subsystem needs
 one". Folded into `READ`, every readable Region is potential code; a Region *kind* fails the loader, which
@@ -232,9 +243,10 @@ execute-only exists on AArch64 but not on x86_64 without protection keys, so nei
 1. **Unrepresentable.** `MapPerms` is `Read`, `ReadWrite` or `ReadExecute`; both encoders are total functions
    from it, so no writable-executable entry can be built. Host-tested exhaustively.
 2. **Per Region, across every address space.** A Region counts writable uses (`RW` mappings, IPC-buffer
-   bindings) and `RX` mappings: `map RX` is refused while any writable use exists, `map RW` and binding while
-   any `RX` mapping does. `unmap`, `protect` and unbinding decrement **only once their invalidation has
-   completed on every core** (§12) — until then a stale writable entry may be live somewhere.
+   bindings) and `RX` mappings: `map RX` is refused while any writable use exists, `map RW`, binding and
+   `region_copy` into it while any `RX` mapping does. `unmap`, `protect` and unbinding decrement **only once
+   their invalidation has completed on every core** (§12) — until then a stale writable entry may be live
+   somewhere.
 3. **Over time.** `EXECUTE` is minted only from a Pool carrying it — the loader holds one, a JIT gets one by
    explicit grant *(Fuchsia's `VmexResource`)*. O-13's Phase-3 load-path clause is policy on this.
 4. **Hardware backstop.** AArch64 sets `SCTLR_EL1.WXN` (bit 19) once the final tables are in (§13); user
@@ -242,8 +254,8 @@ execute-only exists on AArch64 but not on x86_64 without protection keys, so nei
    `mark_linear_text_alias_ro`)*. x86_64 has no `WXN`: `CR0.WP` and `SMEP` where present.
 
 `map RX` makes AArch64's instruction side coherent: `DC CVAU` via the physmap, `DSB ISH`, `IC IVAU` if PIPT
-(`IC IALLUIS` otherwise; Linux's `sync_icache_aliases`), `DSB ISH`, `ISB`; cortex-a72 reports PIPT (`CTR_EL0 =
-0x8444c004`); x86_64 is coherent in hardware. **QEMU models no cache, so errors here pass every test.** These
+(`IC IALLUIS` otherwise; Linux's `sync_icache_aliases`), `DSB ISH`, `ISB`; the Cortex-A72 reports PIPT (`CTR_EL0 =
+0x8444C004`); x86_64 is coherent in hardware. **QEMU models no cache, so errors here pass every test.** These
 and §12's `TLBI`s and `TTBR` writes are single-instruction `asm!` intrinsics in `kernel/src/arch/**`, as `wfe`
 is today — a reading of "minimal assembly" for the maintainer to confirm (§17.7). The physmap still aliases
 *user* code writable at EL1; writing through it only to zero, fill and reach IPC buffers is a convention (§16).
@@ -263,18 +275,18 @@ is today — a reading of "minimal assembly" for the maintainer to confirm (§17
   option **(a)** a peer-transferred Region carrying `REVOKE` could cut the broker off. It is **input to
   RFC-0003a's (a)/(b) choice**; the demo needs none of it.
 
-**Concurrency.** Under RFC-0006 (proposed) V1 — non-preemptible, one big lock once SMP lands — no kernel
-access to a Region's frames (zeroing, table fill, IPC copy) interleaves with its destruction: each runs whole
-in one entry and re-resolves the Region; the dying mark covers destruction's gaps. Finer locking takes
-**Region before AddressSpace**. A former sharer faults: RFC-0006 (proposed) binds delivery, RFC-0007 (proposed)
-defines the message; under its interim the thread stops.
+**Concurrency.** Under RFC-0006 (proposed) verdicts 1 and 11 — non-preemptible, one big lock once SMP lands —
+no kernel access to a Region's frames (zeroing, table fill, IPC copy) interleaves with its destruction: each
+runs whole in one entry and re-resolves the Region; the dying mark covers destruction's gaps. Finer locking
+takes **Region before AddressSpace**. A former sharer faults: RFC-0006 (proposed) binds delivery, RFC-0007
+(proposed) defines the message; under its interim the thread stops.
 
 ## 11. How the kernel touches user memory (O-5)
 
 **The kernel never dereferences a user virtual address** — not through a checked copy or a fixup table, not
 at all *(seL4: the IPC buffer is a frame reached through the kernel window)*. **Where a syscall carries one
 — a `map` destination, an IPC-buffer location — it is a number, validated as a number and used only to
-program tables or registers.** RFC-0007 inherits that sentence exactly. Everything the kernel reads or
+program tables or registers.** RFC-0007 (proposed) §3 inherits that rule. Everything the kernel reads or
 writes for a process is named by capability and reached through the physmap:
 
 - **The IPC buffer** is a 1 KiB-aligned slice of one page of a Region (RFC-0007 (proposed) §5 sets size and
@@ -285,7 +297,7 @@ writes for a process is named by capability and reached through the physmap:
 - **Peer-writable memory is never referenced**: one `kernel/src/mm/` module copies with volatile accesses;
   anything interpreted is copied once and validated as that snapshot *(virtio's double fetch, research/0002
   Part 5)*. *Rejected:* `copy_from_user` with fixups (Linux). `SMAP` and `PAN` back the rule where present;
-  **cortex-a72 has no PAN**, so there it stands on structure.
+  **the Cortex-A72 has no PAN**, so there it stands on structure.
 
 ## 12. TLBs, ASIDs and PCIDs
 
@@ -294,9 +306,12 @@ writes for a process is named by capability and reached through the physmap:
   `TLBI ASIDE1IS` (x86_64: `INVPCID` single-context), so churn does not force rollover. *Rejected:* seL4's
   ASID pools — a tag is not authority.
 - **Kernel entries are global, user entries never.** `map` needs no invalidation: neither architecture caches
-  a faulting entry (the Arm ARM, section uncited as it was unreachable; SDM Vol. 3A §4.10), and a fault whose
-  entry is valid on re-walk is retried. `unmap`, `protect` and teardown store, `DSB ISHST`, `TLBI VALE1IS`,
-  `DSB ISH`, `ISB`; x86_64 `INVLPG`. Freeing an intermediate table needs `TLBI VAE1IS` or `ASIDE1IS`, as
+  an entry that faults for being invalid (Arm ARM DDI 0487 D8.12: entries generating "a Translation fault, an
+  Address size fault, or an Access flag fault are never cached in a TLB"; SDM Vol. 3A §4.10.2.3: a TLB entry
+  exists "only if the P flag is 1 and the reserved bits are 0"), and a fault whose entry is valid on re-walk is
+  retried. A *permission*-faulting entry may be cached on AArch64, which is why `protect` invalidates.
+  `unmap`, `protect` and teardown store, `DSB ISHST`, `TLBI VALE1IS`, `DSB ISH`, `ISB`; x86_64 `INVLPG`.
+  Freeing an intermediate table needs `TLBI VAE1IS` or `ASIDE1IS`, as
   `VALE1IS` spares walk caches; `INVLPG`/`INVPCID` flush them (SDM Vol. 3A §4.10.4.1). **O-8's ordering:
   invalidate, then free** — no frame returns to a Pool while any core can translate to it.
 
@@ -318,8 +333,9 @@ that have run it since its last full flush *(Linux `mm_cpumask`)*.
 ## 13. Early boot: turning the MMU on
 
 The image is linked at `0xFFFF_FFFF_8020_0000`, loaded at 0x4020_0000 (`AT()`). QEMU translates the entry to its
-physical alias **only if** it lies in an executable segment with `p_vaddr != p_paddr` (`include/hw/elf_ops.h`,
-`load_elf`, v8.2.2), which `AT()` gives while `.text.boot` leads that segment. With the MMU off, the stub:
+physical alias **only if** it lies in an executable segment with `p_vaddr != p_paddr`, within `p_filesz`
+(`include/hw/elf_ops.h.inc`, `load_elf`, re-read at 11.0.3), which `AT()` gives while `.text.boot` leads that
+segment. With the MMU off, the stub:
 
 1. Parks secondaries, installs the stack and zeroes `.bss` at physical addresses, as today.
 2. `MAIR_EL1`: index 0 = `0xFF` (Normal write-back, read/write-allocate), index 1 = `0x04` (Device-nGnRE).
@@ -336,21 +352,23 @@ physical alias **only if** it lies in an executable segment with `p_vaddr != p_p
 | `SCTLR_EL1` field (bit) | Value | Why |
 |-------------------------|-------|-----|
 | `M` (0), `C` (2), `SA` (3), `SA0` (4), `I` (12) | 1 | MMU and caches on; stack-alignment checks at EL1 and EL0 |
-| `A` (1), `CP15BEN` (5), `ITD` (7), `SED` (8), `E0E` (24), `EE` (25) | 0 | alignment is the compiler's (`+strict-align`); AArch32 controls, and no thread runs AArch32; little-endian |
-| `UMA` (9), `UCT` (15), `UCI` (26) | 0 | EL0 may neither mask interrupts (defeating preemption) nor maintain caches — the kernel does that at `map RX` (§9) |
+| `A` (1), `CP15BEN` (5), `ITD` (7), `SED` (8), `E0E` (24), `EE` (25) | 0 | alignment is the compiler's (`+strict-align`); AArch32 controls, and no thread runs AArch32 (`ITD` and `SED` are RES1 on a part without AArch32 at EL0, where the 0 is ignored); little-endian |
+| `UMA` (9), `UCT` (15), `UCI` (26) | 0 | EL0 may neither mask interrupts (defeating preemption), read `CTR_EL0` nor maintain caches — the kernel does that at `map RX` (§9) |
 | `DZE` (14) | 1 | EL0 `DC ZVA` is a store its mapping already permits |
 | `nTWI` (16), `nTWE` (18) | 0, 1 | `wfi` traps and `wfe` does not — RFC-0006 (proposed) §8 |
 | `WXN` (19) | 0, then 1 | set by Rust step (5), giving `0x30DC581D` |
-| 11, 20, 22, 23, 28, 29 | 1 | RES1 on Armv8.0: Linux v4.19's `SCTLR_EL1_RES1`, plus bit 23 (`SPAN`, RES1 before Armv8.1), which Linux always sets; not re-checked against the Arm ARM |
-
-Every other bit is 0 (RES0 on Armv8.0, or a later extension left off). Rust then, never leaving the reporter
-without a console: (1) builds the `MemoryMap`, bitmap and arrays through the **boot window** — the
-frame-access trait's offset is `pa − 0x4000_0000 + 0xFFFF_FFFF_8000_0000`, so all it touches lies in the boot
-GiB; (2) builds §6's final tables; (3) swaps `TTBR1_EL1` from the identity map in assembly — empty table,
-`TLBI VMALLE1`, final table, as break-before-make requires *(Linux `idmap_cpu_replace_ttbr1`)* — and moves
-the trait and bitmap to the physmap offset; (4) **repoints every kernel MMIO user** (UART; GIC if up);
-(5) sets `TCR_EL1.EPD0 = 1` (the first AddressSpace install clears it) and `WXN`, then `TLBI VMALLE1`, `DSB
-ISH`, `ISB`. **The boot tables are never freed**: freeing `.bss` would give image frames a second owner.
+| 11, 20, 22, 23, 28, 29 | 1 | RES1 on Armv8.0 — `EOS`, `TSCXT`, `EIS`, `SPAN`, `nTLSMD`, `LSMAOE` in later extensions, each "Reserved, RES1" when its feature is absent (Arm SysReg descriptions; TF-A `SCTLR_EL1_RES1`; Linux `INIT_SCTLR_EL1_MMU_OFF`) |
+
+Every other bit is 0 (RES0 on Armv8.0, or a later extension left off). The whole register is written, never
+read-modified: QEMU's `cortex-a72` resets it to `0x00C50838`, with RES1 bits 20, 28 and 29 clear. Rust then,
+never leaving the reporter without a console: (1) builds the `MemoryMap`, bitmap and arrays through the **boot
+window** — the frame-access trait's offset is `pa − 0x4000_0000 + 0xFFFF_FFFF_8000_0000`, so all it touches
+lies in the boot GiB; (2) builds §6's final tables; (3) swaps `TTBR1_EL1` in assembly running on the identity
+map — empty table, `TLBI VMALLE1`, final table, as break-before-make requires *(Linux
+`idmap_cpu_replace_ttbr1`)* — and moves the trait and bitmap to the physmap offset; (4) **repoints every
+kernel MMIO user** (UART; GIC if up); (5) sets `TCR_EL1.EPD0 = 1` (the first AddressSpace install clears it)
+and `WXN`, then `TLBI VMALLE1`, `DSB ISH`, `ISB`. **The boot tables are never freed**: freeing `.bss` would
+give image frames a second owner.
 
 The reporter gains a DFSC and fault-level decode (it prints `FAR` already); x86_64's `#PF` prints `CR2` and
 its error code. **x86_64**, once the UEFI stub exists, is already paging: Rust builds §6's PML4 with a
@@ -365,7 +383,7 @@ jumps high and drops the identity entry — the same "Rust runs only high" rule.
 |-----------|----------|-----------------------------|
 | O-3 revocability | destruction walks the Region's mappings, invalidates, then bumps; a page-table entry is a cached resolution (§7, §10) | **destruction case extended to memory**; selective revocation and donation are RFC-0003a's |
 | O-5 argument validation | no user virtual address dereferenced; carried ones are numbers; memory by capability through the physmap; snapshots (§11) | **discharged for the memory surface**; RFC-0007 inherits §11's sentence |
-| O-6 kernel memory safety | new `unsafe` only in `mm/**` (window access, volatile copy, the store's static) and `arch/**` (tables, TLB, boot) | **stays Built** — every new block listed per PR |
+| O-6 kernel memory safety | new `unsafe` only in `mm/**` (window access, volatile copy, the object store's static) and `arch/**` (tables, TLB, boot) | **stays Built** — every new block listed per PR |
 | O-7 no unprivileged exhaustion | arrays reused by generation; every post-boot unit charged to a Pool named by capability, `map`'s too; charge-first; `map` ≤ 512 leaves; zeroing in 512-page steps; run search bounded by RAM (§4, §5, §8) | **discharged for kernel allocation**; a transferred object stays charged to its payer until destroyed — **open** with RFC-0003a (§17.2); CPU time is RFC-0006's |
 | O-8 address-space disjointness | per-process tables; Regions only by capability; frames and tables zeroed before use; invalidate before free (§4, §7, §12) | **discharged** |
 | O-9 no ambient side channel | no shared mapping a capability did not establish (§10) | **contributes** |
@@ -378,7 +396,8 @@ jumps high and drops the identity entry — the same "Rust runs only high" rule.
 - **Policy in the kernel.** No address choice, demand paging, copy-on-write, overcommit or OOM response.
 - **Baroque capability hierarchies.** No Untyped tree; Pools are flat, with one funder index for closure.
 - **Multi-copy IPC.** The slow path copies once, frame to frame; bulk data is shared, never copied (§10).
-- **Bolted-on multicore.** Broadcast `TLBI` from the first line; shootdown, rollover, per-core tags designed now (§12).
+- **Bolted-on multicore.** Broadcast `TLBI` from the first line; shootdown, rollover, per-core tags designed
+  now (§12).
 - **The catch-all right.** `EXECUTE` is narrow and refused off-type; no "map any physical address" right.
 - **Compiled-in unused device paths (VENOM).** The kernel maps only the devices it drives itself.
 
@@ -398,11 +417,13 @@ jumps high and drops the identity entry — the same "Rust runs only high" rule.
 1. **Page-table frames on unmap.** Freed only with the AddressSpace; eager freeing needs §12's walk-cache rule.
 2. **Donation and reclaim across a transfer** — `reissue` with a charge move, offered to RFC-0003a (§10).
 3. **Which right authorises explicit destruction** — `REVOKE` would widen as `reissue` would; RFC-0003a.
-4. **Hardware backing for software rules:** software PAN on Armv8.0; unmapping executable user frames from the physmap.
+4. **Hardware backing for software rules:** software PAN on Armv8.0; unmapping executable user frames from the
+   physmap.
 5. **Preemptible teardown**: the O(mappings) walk made restartable at RFC-0006 (proposed)'s preemption points.
 6. **The firmware assumption** (§4) and O-7's new text (§5), via `docs/CHANGELOG.md`.
-7. **"Minimal assembly"** (Constitution §11.1): are runtime one-instruction `TLBI`/`DC`/`IC`/`TTBR` intrinsics within it (§9)?
-8. **One programme order** across RFC-0005/0006/0007 — §18 proposes one for the maintainer to fix.
+7. **"Minimal assembly"** (the Constitution's Language clause): are runtime one-instruction
+   `TLBI`/`DC`/`IC`/`TTBR` intrinsics within it (§9)?
+8. **One programme order** across RFC-0005/0006/0007 — RFC-0007 (proposed) §18 holds it, for the maintainer to fix.
 
 ## 18. Implementation increments
 
@@ -412,34 +433,43 @@ function gets a documented x86_64 stub — an empty `MemoryMap`, on which memory
 memory map (UEFI stub pending)` and halts — so the second Tier-1 build compiles the whole path.
 
 1. **[demo] Relink at 0x4020_0000; prove the DTB.** MMU off. `--expect "DTB 0xd00dfeed at 0x40000000"`.
-2. **[demo] Addresses, `MemoryMap`, FDT reader.** Host tests on a `dumpdtb` fixture, hostile blobs and later an
-   OVMF dump; workspace `members`, `.github/workflows`, `CLAUDE.md` § Layout. `--expect "mm: 512 MiB RAM at 0x40000000"`.
+2. **[demo] Addresses, `MemoryMap`, FDT reader.** Host tests on a `dumpdtb` fixture, hostile blobs and later
+   an OVMF dump; workspace `members`, `.github/workflows`, `CLAUDE.md` § Layout.
+   `--expect "mm: 512 MiB RAM at 0x40000000"`.
 3. **[demo] Frame bitmap.** Churn tests against a shadow model: no frame twice, none reserved, no image frame free.
 4. **[demo] `EXECUTE` in `capability/`** with RFC-0003's amendment: bit 5, `ALL`, `Debug`, tests to `0..64`.
 5. **[demo] `MapPerms` and both encoders.** Exhaustive: never W+X; every user entry `PXN`, `AF`, not-global.
-6. **[demo] Table engine**, both formats: overlap, bounds, unpaid maps nothing, tables zeroed, root untouched by kernel maps.
-7. **[demo] Slot store and one Pool.** Conservation; reuse at generation + 1; stale references count nothing; mint refuses off-type `EXECUTE`.
+6. **[demo] Table engine**, both formats: overlap, bounds, unpaid maps nothing, tables zeroed, root untouched
+   by kernel maps.
+7. **[demo] Object store and one Pool.** Conservation; reuse at generation + 1; stale references count nothing;
+   mint refuses off-type `EXECUTE`.
 8. **`pool_split`/`move`/`merge` and closure forwarding**, under random churn. Host-only; not demo.
-9. **[demo] MMU on (§13, stub)**, `SCTLR_EL1`, `VBAR_EL1` high, DFSC decode: `--expect "mm: running at 0xffffffff80"`.
-10. **[demo] Final kernel map (§13, Rust)**, the store behind its static: physmap with the image read-only,
-    MMIO window with every kernel MMIO user repointed, core 0's stack behind a guard; `EPD0`, `WXN`. One
-    `--expect` per self-test: `provoke-ro-text` and `provoke-ro-alias` write `.text` through the image and
-    the physmap (`data abort, same EL`); `provoke-wxn` branches into `.data` (`instruction abort, same EL`).
+9. **[demo] MMU on (§13, stub)**, `SCTLR_EL1`, `VBAR_EL1` high, DFSC decode:
+   `--expect "mm: running at 0xffffffff80"`.
+10. **[demo] Final kernel map (§13, Rust)**, the object store behind its static: physmap with the image read-only,
+    MMIO window with every kernel MMIO user repointed, core 0's stack moved behind a guard (`aarch64.ld`'s
+    comment with it); `EPD0`, `WXN`. One `--expect` per self-test: `provoke-ro-text` and `provoke-ro-alias`
+    write `.text` through the image and the physmap (`data abort, same EL`); `provoke-wxn` branches into
+    `.data` (`instruction abort, same EL`).
 11. **[demo] Region and Mapping records** with the W^X counts. Host-only.
 12. **[demo] The tag allocator**: rollover, per-core reservation, return on destruction. Host-only.
 13. **[demo] AddressSpace and boot-minted Regions**; `TTBR0_EL1` with ASID; `EPD0` cleared. `AT S1E0R` under
     two ASIDs finds a shared Region at one frame, private ones apart: `mm: shared region agrees`.
-14. **[demo] Pool, Region, AddressSpace methods via RFC-0007's `call`** (its increment 6): `[el0] map ok`.
+14. **[demo] Pool, Region, AddressSpace methods via RFC-0007's `call`** (its increment 6), `region_copy`
+    included: `[el0] map ok`.
 15. **`unmap` and `protect`** with invalidation and count decrements (§9, §12). Not demo.
 16. **User-memory module (§11)**: a message beyond the register budget. Not demo.
-17. **Destruction (§10)**, after RFC-0007 increment 11's fault message: a destroyed sharer's fault reaches its handler.
-18. **Stack overflow**, with RFC-0006's overflow stack: `provoke-stack-overflow` reaches the reporter.
+17. **Destruction (§10)**, after RFC-0007 increment 11's fault message: a destroyed sharer's fault reaches its
+    handler.
+18. **Stack overflow**, with RFC-0006's overflow path (its §9): `provoke-stack-overflow` reaches the reporter.
 19. **PAN, SMAP, SMEP** where reported, with a `provoke-user-deref` self-test under `-cpu max`.
 20. **x86_64** tables, `CR3` and PCID, after the UEFI stub; **Device Regions** in Phase 2.
 
-**Programme order proposed** (§17.8): 1–8 beside RFC-0006 1–2 and RFC-0007 1–5; RFC-0007's MMU-off EL0
-self-test (its 3) before 9, which retires it; 9–10 before RFC-0006 3 (or 10 repoints the GIC too) and 4,
-which needs the stack window; 11–13 before RFC-0006 5 and RFC-0007 6–7; 14 with RFC-0007 6.
+**Programme order:** one merged order for all three RFCs lives in RFC-0007 (proposed) §18, for the maintainer to
+fix (§17.8). This RFC's constraints on it: 1–8, 11 and 12 need nothing else and leave the MMU off; the
+MMU-off EL0 self-tests (RFC-0007 3, RFC-0006 4) land before 9, which retires them; 10 repoints every kernel
+MMIO user, the GIC included when RFC-0006 3 came first; 13 precedes RFC-0006 5 and RFC-0007 6; 14 lands with
+RFC-0007 6.
 
 **Interims the demo carries, with their cost:**
 
@@ -458,4 +488,5 @@ which needs the stack window; 11–13 before RFC-0006 5 and RFC-0007 6–7; 14 w
 Increments 1–14 give RFC-0006 (proposed) address spaces, a guarded per-core stack and a Pool to charge threads
 to; RFC-0007 (proposed) the objects its Process, root task and boot info are made of, and §11's sentence on
 user addresses as a constraint inherited, not discovered. The root receives all memory as one boot-minted
-Pool — RFC-0003 §14.4's bootstrap without an ambient grantor. Increments 1–8 leave the MMU off: all can land now.
+Pool — RFC-0003 §14.4's bootstrap without an ambient grantor. Increments 1–8, 11 and 12 leave the MMU off
+and need no sibling's code, so they can land once this RFC is accepted.
diff --git a/docs/rfcs/0006-threads-and-scheduling.md b/docs/rfcs/0006-threads-and-scheduling.md
index 117b05e..fbf337f 100644
--- a/docs/rfcs/0006-threads-and-scheduling.md
+++ b/docs/rfcs/0006-threads-and-scheduling.md
@@ -7,9 +7,9 @@
 | Status | **Proposed** — 2026-09-27, awaiting the maintainer's verdict |
 | Author | Drafted by Claude Code as sparring partner; verdict the maintainer's |
 | Date | 2026-09-27 |
-| Affects | Constitution §3 ("IPC is the product", priority inheritance, bolted-on multicore); the HAL (`kernel/src/arch/**`), `boot.s`'s park loop and `aarch64.ld`'s stack plan; RFC-0003 §14.2 (a dated note); RFC-0004 §4, §8, §9.2, §9.3 and its 2026-08-01 amendment (§13's amendments); research/0002 Part 6 (one correction); RFC-0005 §13 step 5 and §18.2; `CLAUDE.md` § Architectures (FP enabled per thread) and § Layout (gains `scheduler/`); every userspace driver |
+| Affects | Constitution §3 ("IPC is the product", priority inheritance, bolted-on multicore); the HAL (`kernel/src/arch/**`), `boot.s`'s park loop and `aarch64.ld`'s stack plan; RFC-0003 §6 and §14.2 (dated notes); RFC-0004 §4, §8, §9.2, §9.3 and its 2026-08-01 amendment (§13's amendments); research/0002 Part 6 (a correction and a departure); RFC-0005 §13 (the `SCTLR_EL1` bits it writes) and §6 (the stack window); `CLAUDE.md` § Architectures (FP enabled per thread) and § Layout (gains `scheduler/`); every userspace driver |
 | Depends on | RFC-0003 (capability table); RFC-0004 (IPC) and its 2026-08-01 amendment; RFC-0005 (proposed) for object memory, kernel stacks, discovery and address-space switching; RFC-0007 (proposed) for the trap path, the syscall encoding, the Process object and the root task |
-| Discharges | O-7 for CPU time and the scheduler's own structures; O-4 for time; both commitments of RFC-0004's 2026-08-01 amendment **as amended by verdict 12**; answers RFC-0004 §9.2 in shape; contributes to O-5, O-9, O-17 |
+| Discharges | O-7 for CPU time and the scheduler's own structures; O-4 for time; both commitments of RFC-0004's 2026-08-01 amendment **as amended by verdict 12**; answers RFC-0004 §9.2 in shape; O-5 for the register surface (`write_regs`); contributes to O-9, O-17 |
 
 > **Proposed verdicts.**
 >
@@ -18,13 +18,13 @@
 > 3. **Time is a capability:** a `SchedContext`, configured only through its core's `SchedControl` (§5).
 > 4. **Budgets are caps, not minima:** a guaranteed minimum is admission policy, unlike research/0002 (§5).
 > 5. **Priorities:** 256 fixed levels; any capability to a thread lends its priority ceiling; no new right (§6).
-> 6. **Endpoint queues are priority-ordered,** first come first served within a level, as in seL4 MCS (§6).
+> 6. **Endpoint queues are priority-ordered,** first come, first served within a level, as in seL4 MCS (§6).
 > 7. **Donation:** `call` lends time to a *passive* server; a caller's death never takes it back mid-request (§7).
 > 8. **Budget guard:** endpoints carry a `min_budget` checked at `call`; expiry fails one hop back (§7).
 > 9. **Timer:** tickless per-core deadlines; userspace timers become deadline objects on the same queue (§8).
-> 10. **FP/SIMD:** off by default, enabled per thread, saved lazily; the kernel touches it only to save it (§10).
+> 10. **FP/SIMD:** off by default, enabled per thread, saved lazily; the kernel touches it only to save and restore it (§10).
 > 11. **Interrupts and cores:** a line signals a notification; one big lock; a core starts when funded (§11–§12).
-> 12. **Amendments:** three to RFC-0004, a note on RFC-0003 §14.2, a correction to research/0002 (§13).
+> 12. **Amendments:** A1–A6 to RFC-0004, RFC-0003 and research/0002; C1, a constitutional question for the maintainer (§13).
 
 ## 1. The question
 
@@ -32,8 +32,9 @@
 not granted, a server never runs on time nobody paid for, and the kernel never waits on anything a process
 controls?**
 
-That is O-7's scheduler half plus RFC-0004's three hazards: direct switch, donation, and budget expiry inside a
-server. This RFC designs the mechanism; priorities, admission and load are for whoever holds its capabilities.
+That is O-7's scheduler half plus what RFC-0004 §4, §9.2 and its amendment hand this RFC: direct switch, donation,
+and budget expiry inside a server. This RFC designs the mechanism; priorities, admission and load are for whoever
+holds its capabilities.
 
 ## 2. Which pillar
 
@@ -54,8 +55,8 @@ it becomes one. **Borrow Ledger:** scheduler, timer and interrupt-controller cod
   written into the frame, or it restarts by rewinding the PC (4 bytes for `svc #0`, 2 for `syscall`). *(Heiser &
   Elphinstone, TOCS 2016; Ford et al., "Interface and Execution Models in the Fluke Kernel", OSDI 1999.)*
 
-**The cost:** every path must be bounded. Long ones — destruction, RFC-0005's `reissue` and teardown, RFC-0007's
-console write (both proposed) — take **preemption points**: on a pending interrupt (`ISR_EL1.I`; the LAPIC IRR)
+**The cost:** every path must be bounded. Long ones — destruction, and RFC-0005 (proposed)'s Region zeroing and
+teardown — take **preemption points**: on a pending interrupt (`ISR_EL1.I`; the LAPIC IRR)
 they leave the operation restartable and exit. **A restart re-resolves every handle and re-checks every right**;
 an object mid-teardown is marked *dying* so no entry invokes it meanwhile. The worst path between points is
 measured and published as the interrupt latency. The boot stack becomes core 0's kernel stack in RFC-0005's
@@ -71,14 +72,14 @@ big lock (§12) first.
 ## 4. The Thread object (verdict 2)
 
 A **Thread** is an RFC-0003 object belonging to one Process, which RFC-0007 (proposed) provides; its TCB is a
-slot in RFC-0005 (proposed)'s typed array for threads, charged to the Pool presented at creation.
+slot in RFC-0005 (proposed)'s typed array for threads, charged to the Pool invoked at creation (RFC-0007 §4).
 
 | Field | Meaning |
 |-------|---------|
 | `frame` | the full user register file, written at every kernel entry (§9) |
 | `state`, `blocked_on`, links | a state below; the endpoint, reply object or notification waited on; intrusive queue links |
 | `priority`, `mcp` | base priority and maximum controlled priority (§6); both **0 at creation** |
-| `home_sc`, `sc`, `effective` | the bound context, if any; the context held now, own or donated; the priority run at now (§7) |
+| `home_sc`, `sc`, `effective` | the bound context, if any; the context held now, own or donated; the priority it runs at now (§7) |
 | `bound_notification`, `ipc_buffer` | the notification a `recv` may also wake on (RFC-0004 §10); the IPC-buffer binding (RFC-0007, proposed) |
 | `fault_ep`, `timeout_ep` | **two kernel-held capability slots** *(seL4 MCS)*: moved in by the binder, generation-checked when a fault is raised, failing closed if the endpoint died; the thread cannot close them |
 | `fp_enabled`, `fp_state` | the FP/SIMD flag and save area (§10) |
@@ -89,17 +90,17 @@ slot in RFC-0005 (proposed)'s typed array for threads, charged to the Pool prese
 | `Ready` | runnable with released budget; in its core's run queue | dispatch, `suspend`, context removed |
 | `Running` | the current thread on its core; in no queue | preemption, timeslice end, exhaustion (→ `Throttled`), block, `yield`, fault, `suspend`, `thread_exit`, context removed (→ `Unfunded`) |
 | `Throttled` | holds a context whose released budget is spent, or below what its pending `call` needs; in the release queue | refill release, `suspend`, context removed |
-| `Unfunded` | runnable, no context: a passive thread woken by `send` or `notify`, `resume`d with none, or stranded (§7); in no queue | `bind_sc`, a donation, `suspend` |
+| `Unfunded` | runnable, no context: a passive thread woken by a `send` to an endpoint or a notification, `resume`d with none, or stranded (§7); in no queue | `bind_sc`, a donation, `suspend` |
 | `BlockedOnSend` | queued on an endpoint to `send` or `call` | rendezvous, endpoint destruction, `suspend` |
-| `BlockedOnRecv` | waiting on an endpoint (and any bound notification) | rendezvous, signal, `suspend` |
-| `BlockedOnReply` | waiting on a reply object after `call` or a fault message | reply, error completion (§7) |
-| `BlockedOnNotification` | waiting on a notification alone | signal, `suspend` |
+| `BlockedOnRecv` | waiting on an endpoint (and any bound notification) | rendezvous, signal, endpoint destruction, `suspend` |
+| `BlockedOnReply` | waiting on a reply object after `call` or a fault message | reply, error completion (§7), `suspend` |
+| `BlockedOnNotification` | waiting on a notification alone | signal, notification destruction, `suspend` |
 | `Exited` | finished; in no queue; the object lingers until destroyed | never |
 
 Faults reuse IPC: the kernel `call`s `fault_ep` for the thread, which waits `BlockedOnReply` (RFC-0007 defines
 the message); a fault donates as `call` does, a timeout fault never, and both bypass `min_budget`. Destroying
-a thread bumps its generation (RFC-0003 §7), unlinks it in O(1) and destroys any reply object it waits on
-(RFC-0004 §8); §7 governs a context it lent.
+a thread bumps its generation (RFC-0003 §7), unlinks it in O(1) and unbinds any reply object it waits on
+(RFC-0004 §8, reusable under RFC-0007 (proposed)'s amendment); §7 governs a context it lent.
 **Every internal link survives slot reuse:** queue links, `sc`, `home_sc`, a reply object's record of a lent
 context, an `IrqHandler`'s notification and a core's FP owner are each a counted reference holding the slot
 (RFC-0005 §5) or an `(index, generation)` pair checked on use — never a bare index.
@@ -108,22 +109,22 @@ Every operation is a method `call` on the **invoked** capability (RFC-0007 verdi
 **presented** one — resolved and checked in the caller's table, never moved, needing no `TRANSFER` — an encoding
 RFC-0007 (proposed) provides *(seL4's `extraCaps`)*. The list is closed:
 
-| Operation | Invoked: right | Presented: right | Effect |
-|-----------|----------------|------------------|--------|
+| Operation | Invoked: right | Presented or moved: right | Effect |
+|-----------|----------------|---------------------------|--------|
 | `set_priority(t, auth, p)` / `set_mcp(t, auth, m)` | `t`: `WRITE` | `auth`: any capability to a Thread, no right checked | value `≤ mcp(auth)` (§6) |
 | `bind_sc(t, sc)` / `unbind_sc(t)` | `t`: `WRITE` | `sc`: `WRITE` / — | active ↔ passive |
 | `bind_notification(t, n)` / `unbind_notification(t)` | `t`: `WRITE` | `n`: `READ` / — | a `recv` also wakes on `n` |
-| `set_fault_ep(t, ep)` / `set_timeout_ep(t, ep)` | `t`: `WRITE` | `ep`: `WRITE`, **moved** into the TCB | the binder derives first to keep a copy |
+| `set_fault_ep(t, ep)` / `set_timeout_ep(t, ep)` | `t`: `WRITE` | `ep`: `WRITE` and `TRANSFER` (RFC-0003 §6), **moved** into the TCB | the binder derives first to keep a copy |
 | `resume(t)` / `suspend(t)` | `t`: `WRITE` | — | `Inactive` ↔ runnable; a first `resume` closes the grant window (RFC-0007) |
 | `read_regs(t)` / `write_regs(t, …)` | `t`: `READ` / `WRITE` | — | the frame, `TPIDR_EL0` and `FS_BASE` only, sanitised (§9) |
 | `set_fp(t, on)` | `t`: `WRITE` | — | §10 |
-| `sc_configure(ctl, sc, B, T, refills, 0)` | `ctl`: `WRITE` | `sc`: `WRITE` | §5; the last word, the placement class, is reserved zero (§12) |
+| `sc_configure(ctl, sc, B, T, refills, class)` | `ctl`: `WRITE` | `sc`: `WRITE` | §5; `class`, packed beside `refills` (RFC-0007 §4), is reserved zero (§12) |
 | `sc_stats(sc)` / `ctl_info(ctl)` | `sc` / `ctl`: `READ` | — | §5's counters; the exclusivity check (§12) |
 | `yield()` / `thread_exit()` | none: two of RFC-0003 §9's three authority-free exceptions | — | tail of own level / `Exited` |
 
 No right joins RFC-0003's set. **The supervision cost:** a process with `WRITE` on its own thread can rebind
 its `fault_ep`, so a supervisor grants no `WRITE` on threads it creates for a child; threads the child creates
-are supervised through the Process (RFC-0007 open question 1). A TLS runtime sets `FS_BASE` by `write_regs`,
+are supervised through the Process (RFC-0007 Open question 1). A TLS runtime sets `FS_BASE` by `write_regs`,
 needing `WRITE` on its thread, or its spawner sets it before `resume`.
 
 ## 5. Scheduling contexts and `SchedControl` — time as a capability (verdicts 3, 4)
@@ -146,12 +147,12 @@ with released budget*: a spent partial context leaves its core idle by design, a
 | Aspect | Rule |
 |--------|------|
 | **`SchedControl`** | one per core, minted to the root task and listed in BootInfo (RFC-0007, proposed). Two methods: `sc_configure` (`WRITE`) binds a context to that core with its parameters — moving a context is `sc_configure` through another core's `SchedControl`, and the first one onto a parked core starts it (§12); `ctl_info` (`READ`) returns the count of contexts on the core and the object's reference count. Topology is BootInfo *data* from RFC-0005 (proposed)'s discovery; routing is `IrqControl`'s (§11). No syscall names a core by number. *(seL4 `SchedControl`; research/0002's "core-set capability".)* |
-| **`MIN_BUDGET`** | `B` below twice the published worst kernel path is refused — seL4 MCS's rule, `2u * getKernelWcetTicks() * CONFIG_KERNEL_WCET_SCALE` (`include/kernel/sporadic.h`), without the scale. The path is measured *between preemption points*, which is why RFC-0007's console write must take them (§11): its 44 ms hold would make `MIN_BUDGET` 88 ms. |
+| **`MIN_BUDGET`** | `B` below twice the published worst kernel path is refused — seL4 MCS's rule, `2u * getKernelWcetTicks() * CONFIG_KERNEL_WCET_SCALE` (`include/kernel/sporadic.h`), without the scale. The path is measured *between preemption points*; RFC-0007 (proposed)'s console write never waits and stores at most 24 bytes, so it sets no floor here (§11). |
 | **Full and partial** | full contexts (`B = T`) are never throttled and round-robin with timeslice `T`. Partial ones (`B < T`) are sporadic servers: no window of length `T` sees more than `B` consumed; refills fall due a period after use; when all eight are in use they merge, forfeiting bandwidth rather than exceeding it. *(Sprunt, Sha & Lehoczky 1989.)* |
-| **Billing** | the QNX caveat stated as design (ECRTS '21): each context's window is its own sliding period; billing is exact, from `CNTVCT_EL0` or the TSC read at every entry and exit — 16 ns on QEMU's `cortex-a72`, which keeps the pre-Armv8.6 62.5 MHz default (`target/arm/tcg/cpu64.c`, `target/arm/cpu.c`). Kernel time, **interrupts included, is billed to the context running on entry** *(as seL4)* — a leak costed in §17. |
+| **Billing** | the QNX caveat stated as design (ECRTS 2021): each context's window is its own sliding period; billing is exact, from `CNTVCT_EL0` or the TSC read at every entry and exit — 16 ns on QEMU's `cortex-a72`, which keeps the pre-Armv8.6 62.5 MHz default (`target/arm/tcg/cpu64.c`, `target/arm/cpu.c`). Kernel time, **interrupts included, is billed to the context running on entry** *(as seL4)* — a leak costed in §17. |
 | **Stall counters** | from the first version (research/0002 Part 6, after PSI and oomd): per context, time consumed, time and count throttled, time ready but waiting, expiries; read through `sc_stats` — the O-17 supervisor's wedged-server signal. |
 | **Lifecycle** | destroying or reconfiguring a context preempts the thread running on it (an IPI on SMP), clears every link to it — `sc`, `home_sc`, a reply object's record, its release-queue entry — before its slot count can reach zero, and leaves those threads `Unfunded`. A reply whose recorded context has gone moves nothing. |
-| **Accounting domain** | **decided: separate in Phase 1.** A context's memory is a slot charged to a Pool (RFC-0005); its time comes only from a `SchedControl`. One domain holding both is the broker RFC's; the cost is a broker reasoning over two ledgers. This answers RFC-0005 (proposed) open question 2. |
+| **Accounting domain** | **decided: separate in Phase 1.** A context's memory is a slot charged to a Pool (RFC-0005); its time comes only from a `SchedControl`. One domain holding both is the broker RFC's; the cost is a broker reasoning over two ledgers. RFC-0005 (proposed) §5 states the same split from the memory side. |
 
 ## 6. Priorities and dispatch (verdicts 5, 6)
 
@@ -170,11 +171,12 @@ priority authority, to be handed out sparingly.
   count-leading-zeros over four `u64` words — O(1). A preempted thread re-enters at the head of its level; one
   whose timeslice ended, at the tail; the running thread and one switched to directly are never queued.
   *(Elphinstone & Heiser, "From L3 to seL4", SOSP 2013.)* The per-core **release queue** is sorted by next
-  refill, O(n) in contexts only the `SchedControl` holder adds.
+  refill, O(n) in contexts only the `SchedControl` holder adds, plus §8's deadline objects, bounded by their array.
 - **Priority-aware direct switch** (RFC-0004 §4). When *C* wakes *W* by IPC on the same core and *W* has released
   budget: if *C* blocks (`call`, `recv`, `reply_recv`), switch to *W* when its effective priority is at least the
-  highest ready; if *C* stays runnable (`send`, `reply`, `notify`), only when *W* is also strictly more urgent.
-  Otherwise *W* is queued — on the release queue without budget, on its own core with an IPI (§12).
+  highest ready; if *C* stays runnable (`send` to an endpoint or a notification, `reply`), only when *W* is also
+  strictly more urgent. Otherwise *W* is queued — on the release queue without budget, on its own core with an IPI
+  (§12).
 - **Endpoint queues are priority-ordered, first-come within a level** — seL4 MCS's `tcbAppend`
   (`include/object/tcb.h`, "priority ordered endpoint or notification queue"), walking back from the tail; the
   FIFO `tcbEPAppend` is compiled only without MCS. The walk is O(n) with interrupts masked, *n* bounded by the
@@ -185,16 +187,16 @@ priority authority, to be handed out sparingly.
 ## 7. Donation, inheritance and budget expiry (verdicts 7, 8)
 
 **Donation.** When *C* `call`s a **passive** receiver *S*, the kernel moves *C*'s current context to *S*, recorded
-in the single-use reply object *R* (RFC-0004 §8); `reply` or `reply_recv` moves it back. *S* runs at
-`max(prio(S), eff(C))`, **fixed at donation**, not propagated if *C*'s priority later changes — O(1), one hop at
-a time. Lending priority is safe because time is lent with it. *(Ford & Lepreau, migrating threads, 1994; QNX
+in the reply object *R* that *S*'s `recv` bound to *C* (RFC-0004 §8); `reply` or `reply_recv` moves it back. *S*
+runs at `max(prio(S), eff(C))`, **fixed at donation**, not propagated if *C*'s priority later changes — O(1), one
+hop at a time. Lending priority is safe because time is lent with it. *(Ford & Lepreau, migrating threads, 1994; QNX
 priority inheritance; seL4 MCS passive servers.)*
 
 **An active receiver gets no donation (amendment A1).** It runs on its own context and priority, as in seL4 MCS
 (`reply_push`, `src/object/reply.c`, donates only to a receiver with none): a thread holds one context, and an
 active server chose to pay for itself. RFC-0004 §4 and §8 lend unconditionally, so this amends them. **The
 cost:** an active server inherits nothing, and a low-priority one blocks urgent clients; Constitution §3's
-inheritance holds for passive servers only.
+inheritance would hold for passive servers only, which is the question C1 (§13) puts to the maintainer.
 
 **Inversion, bounded.** Priority-ordered queues serve the most urgent waiter next, but the request in service
 runs on its client's context and a middle-priority thread can preempt it. `prio(S)` is therefore a **ceiling
@@ -203,34 +205,42 @@ seL4 MCS relies on)* — **required, not optional, for a server shared across tr
 **Rejected:** boosting a busy server to a waiting sender's priority (QNX): the kernel would guess which thread
 serves an endpoint and walk unbounded chains.
 
-**Caller death never unfunds a server.** If *C* exits or is killed mid-request, *R* is destroyed but the context
+**Caller death never unfunds a server.** If *C* exits or is killed mid-request, *R* is unbound but the context
 stays with *S* until *S* next blocks in `recv` or `reply_recv` (its `reply` fails `PeerGone`); it then detaches,
 and only its capability holder may rebind or destroy it. A client's `thread_exit` never pulls time from a server
 *(seL4 `reply_remove_tcb` likewise leaves the context with the server)*.
 
-**The 2026-08-01 amendment, discharged as amended,** after seL4 RFC-14 (Mitchell Johnston, "Budget limit
-thresholds on endpoints for SC Donation", seL4/rfcs pull request 24, open):
+**The 2026-08-01 amendment, discharged as amended,** after seL4 RFC-14 (Mitchell Johnston, "MCS: Budget limit
+thresholds on endpoints for SC Donation", proposed 2023-08-15; seL4/rfcs pull request 24, opened 2024-06-17 and
+still open):
 
 - **Prevention — `min_budget`,** fixed at endpoint creation (0 for none; RFC-0007 encodes it). A `call` needs
-  released budget of at least `min_budget + MIN_BUDGET`, the margin paying for the `call` and `reply` — **this
-  RFC's rule**; RFC-14's exact comparison is to be quoted before acceptance. A context whose `B` can never meet
-  it fails `BudgetRefused`; a non-donating `send` to such an endpoint is invalid.
+  released budget of at least `min_budget + MIN_BUDGET`, the margin paying for the `call` and `reply` — RFC-14's
+  comparison, which sets "the budget to pass the threshold" to "the 'threshold' value plus twice the kernel WCET,
+  to account for the call and reply system calls". RFC-14 also deducts "time consumed by the client, but not yet
+  charged to its SC", which is moot here because §5 bills at every entry. A context whose `B` can never meet it
+  fails `BudgetRefused`; a non-donating `send` to such an endpoint is invalid, as in RFC-14.
 - **A caller short *now* waits (amendment A2),** where the amendment says "refused up front": a partial context
   has its refills merged and deferred, waits `Throttled`, and the call restarts when the head refill suffices —
-  free in an event kernel, O(refills) ≤ 8, the deferral the RFC-14 discussion describes; a **full** context ends
-  its timeslice and retries on the next. Nothing is donated below the bar either way; refusal makes clients spin.
+  free in an event kernel, O(refills) ≤ 8, the deferral RFC-14 specifies ("refills will be deferred and merged
+  until its head refill has sufficient budget"); a **full** context ends its timeslice and retries on the next,
+  a branch of this RFC's own, since RFC-14 does not treat round-robin contexts. Nothing is donated below the bar
+  either way; refusal makes clients spin.
 - **Recovery — one layer down.** If a donated context is exhausted with no refill due while passive *S* runs, the
-  kernel returns it to *S*'s immediate caller, whose wait on *R* completes with `BudgetExpired`; *R* is consumed,
-  so a late `reply` fails closed. *S* is left `Unfunded`, registers intact. If `timeout_ep` is live, a **timeout
-  fault** carries consumed time and donates nothing (seL4 MCS likewise); the handler, on its own time, abandons
-  the request (`write_regs`) or lends *S* a context. It carries **no identity** — badges are reserved zero until
-  RFC-0003a — so a handler binds one endpoint per server. Unwinding further (A → B → C) would walk the reply
-  stack, O(n) with interrupts masked; B gets `BudgetExpired` and can fail A itself.
+  kernel returns it to *S*'s immediate caller — RFC-14's budget-limit return, applied here to plain expiry, where
+  seL4 today raises a timeout fault or postpones the context (`endTimeslice`) — whose wait on *R* completes with
+  `BudgetExpired`; *R* is unbound, so a late `reply` fails `PeerGone`. *S* is left `Unfunded`, registers intact. If
+  `timeout_ep` is live, a **timeout fault** carries consumed time and donates nothing (seL4 MCS likewise); the
+  handler, on its own time, abandons the request (`write_regs`) or lends *S* a context. It carries **no identity**
+  — badges are reserved zero until RFC-0003a — so a handler binds one endpoint per server. Unwinding further (A → B
+  → C) would walk the reply stack, O(n) with interrupts masked; B gets `BudgetExpired` and can fail A itself.
 - **`min_budget` 0 prevents nothing:** one client can strand a shared server for all until a handler funds it
   (O-26, A5). Zero suits a server with one client, or one under a supervisor.
 
 **Rejected:** the unwind without timeout faults — a woken supervisor beats a polling one. **Deferred:** RFC-14's
-budget limits, at a reported 22% extra fastpath cost, per-operation figures to be re-checked (Open question 3).
+budget limits: 22% on the IPC `Call` fastpath and 21% on `ReplyRecv` (327 and 352 cycles against 269 and 290),
+13–24% on the slow paths; thresholds alone cost 13% on the `Call` fastpath, and compiled in but unused, 3%
+(RFC-14, "Performance summary"; Open question 3).
 
 ## 8. The timer and preemption (verdict 9)
 
@@ -254,15 +264,15 @@ arms nothing; a lone partial one still arms its exhaustion.
   insert bounded by the deadline array's capacity *(Zircon's timer object)*. **Rejected:** minting a second
   hardware timer — AArch64 has the EL1 physical timer (PPI 30), x86_64 nothing per core short of the HPET.
 
-**Kernel-reserved bits, owned here.** RFC-0005 (proposed) writes `SCTLR_EL1` whole and must carry them; its §13
-step 5 says `nTWE = 0` today and needs correcting.
+**Kernel-reserved bits, owned here.** RFC-0005 (proposed) writes `SCTLR_EL1` whole, and its §13 table carries
+these values (`0x30D4581D` has `nTWI` clear and `nTWE` set).
 
 | Register | Value | Why |
 |----------|-------|-----|
 | `SCTLR_EL1.nTWI` (bit 16) | 0 | EL0 `wfi` traps (EC `0x01`) and completes as `yield`; `ELR_EL1` holds the `wfi` itself, so the saved PC advances by 4 |
 | `SCTLR_EL1.nTWE` (bit 18) | 1 | EL0 `wfe` does not trap, so spin-lock backoff costs no kernel entry; the `sev` residual is in §15's O-9 row |
 | `SCTLR_EL1.UMA` (bit 9), `SA` (bit 3) | 0, 1 | no EL0 DAIF access; `SP` alignment checked at EL1 (§9) |
-| `CNTKCTL_EL1`, `PMUSERENR_EL0` | 0 | no EL0 counter, timer or PMU; written at boot because their reset values are not architecturally fixed |
+| `CNTKCTL_EL1`, `PMUSERENR_EL0` | 0 | no EL0 counter, timer or PMU; written at boot because the Arm ARM resets every field of both to an architecturally UNKNOWN value on a Warm reset (QEMU happens to reset both to 0) |
 
 ## 9. The context switch — what is saved, where
 
@@ -271,7 +281,7 @@ A context switch is *which frame the exit path restores*; assembly stays in the
 frame, so the entry stub's stores land there before it loads the per-core stack from the `TPIDR_EL1` block; with
 `SA` on and the frame 16-byte aligned, the current-EL `SP_ELx` synchronous vector reports a frame overwrite if
 `SP` lies inside a TCB. On x86_64 an interrupt from ring 3 loads `RSP` from `TSS.RSP0`, the TCB frame; **`syscall`
-does not switch `RSP`**, so its stub runs `swapgs`, parks the user `rsp` in per-CPU scratch, loads the frame
+does not switch `RSP`**, so its stub runs `swapgs`, parks the user `rsp` in per-core scratch, loads the frame
 pointer, saves, then loads the kernel stack. RFC-0007 (proposed) owns both entry sequences; this RFC owns the
 layout and §3's IRQ stub. The address-space switch (`TTBR0_EL1` with ASID; `CR3` with PCID) is RFC-0005's, made
 on exit when the process differs — where a time-protection flush would go (Ge et al., EuroSys 2019).
@@ -291,6 +301,13 @@ DAIF clear, only NZCV from the caller); on x86_64 `CS`/`SS` are constants, `RFLA
 and the user GS base are the kernel's IPC-buffer discovery registers (RFC-0007 §5). NMI, `#DB`, `#DF` and `#MC`
 use IST stacks, as they can arrive before `syscall`'s stack switch.
 
+**A kernel stack overflow is reported, never survived.** RFC-0005 (proposed) §6 puts an unmapped guard page below
+each per-core stack and reserves an emergency stack beside it. On AArch64 the current-EL `SP_ELx` vectors test
+`SP` against the stack's bounds before their first store, and switch to the emergency stack when it has left them
+*(Linux `kernel_ventry`'s overflow check)*; on x86_64 a push into the guard page cannot deliver its `#PF` and
+escalates to `#DF`, which runs on its IST stack *(Linux, likewise)*. Either way the reporter prints and the core
+halts; RFC-0005's increment 18 proves it.
+
 ## 10. FP/SIMD — owned by userspace, enabled per thread, saved lazily (verdict 10)
 
 - **Enabled per thread** by `set_fp`, off by default. `CLAUDE.md` says "per process"; per thread is finer, so an
@@ -314,28 +331,28 @@ use IST stacks, as they can arrive before `syscall`'s stack switch.
 
 The kernel owns the controller and nothing behind it *(seL4 `IRQControl`/`IRQHandler`)*.
 
-- **Objects.** One `IrqControl` (the root's) mints at most one `IrqHandler` per device line; the timer PPI, IPI
-  SGIs or vector and spurious INTID 1023 are never minted. `bind(irq, notification, bits)` invokes the
+- **Objects.** One `IrqControl` (the root's) mints at most one `IrqHandler` per device line; the timer PPI, the IPI
+  SGIs or vector, and the spurious INTID 1023 are never minted. `bind(irq, notification, bits)` invokes the
   `IrqHandler` (`WRITE`) and presents the notification (`WRITE`); `ack(irq)` needs `WRITE`. **Phase 1 routes
   every line to the boot core**; SMP routing is `IrqControl`'s, never `SchedControl`'s (Open question 6). Shared
   PCI INTx lines on `q35` are **unsupported** until MSI.
 - **Delivery.** The kernel acknowledges, **masks the line**, signals end of interrupt, ORs `bits` into the
   notification and wakes a waiter; the driver's `ack` unmasks. A level-triggered line cannot storm, though it
   fires once per `ack` (§17). A destroyed notification leaves the line masked; the `IrqHandler` outlives a
-  crashed driver, and a restarted one re-binds (O-17).
-- **AArch64: GICv3 first.** `GICD_CTLR.ARE` and `EnableGrp1` (`virt` without `secure=on` has one security state,
-  `DS = 1`); SPIs through `GICD_ISENABLER<n>`, `GICD_IPRIORITYR<n>`, `GICD_IROUTER<n>`; the redistributor woken
-  by `GICR_WAKER`, SGIs and PPIs through `GICR_ISENABLER0` and `GICR_IPRIORITYR<n>`; every line in Group 1 (Group
-  0 arrives as FIQ) at a priority numerically below `ICC_PMR_EL1`'s mask; `ICC_SRE_EL1.SRE`, `ICC_IGRPEN1_EL1`,
-  `ICC_IAR1_EL1`, `ICC_EOIR1_EL1`. On `virt`: distributor `0x0800_0000`, redistributors from `0x080A_0000` (QEMU
-  `hw/arm/virt.c`), via RFC-0005's MMIO window. *(Arm IHI 0069.)* **Cost:** `virt` picks GICv2 at eight CPUs or
-  fewer, so xtask adds `gic-version=3`; the Raspberry Pi 4's GIC-400 (GICv2) is a **known** second driver.
+  crashed driver, and a restarted one rebinds (O-17).
+- **AArch64: GICv3 first.** `GICD_CTLR.EnableGrp1` (bit 1): `virt` without `secure=on` has one security state,
+  `DS = 1`, so `ARE` is RAO/WI (`hw/intc/arm_gicv3_dist.c`); SPIs through `GICD_ISENABLER<n>`,
+  `GICD_IPRIORITYR<n>`, `GICD_IROUTER<n>`; the redistributor woken by `GICR_WAKER`, SGIs and PPIs through
+  `GICR_ISENABLER0` and `GICR_IPRIORITYR<n>`; every line in Group 1 (Group 0 arrives as FIQ) at a priority
+  numerically below `ICC_PMR_EL1`'s mask; `ICC_SRE_EL1.SRE`, `ICC_IGRPEN1_EL1`, `ICC_IAR1_EL1`, `ICC_EOIR1_EL1`. On
+  `virt`: distributor `0x0800_0000`, redistributors from `0x080A_0000` (QEMU `hw/arm/virt.c`), via RFC-0005's MMIO
+  window. *(Arm IHI 0069.)* **Cost:** `virt` picks GICv2 at eight CPUs or fewer, so xtask adds `gic-version=3`; the
+  Raspberry Pi 4's GIC-400 (GICv2) is a **known** second driver.
 - **x86_64: LAPIC and I/O APIC.** The 8259s are masked; I/O APIC entries carry the mask bit; end of interrupt
   goes to the LAPIC (x2APIC EOI MSR `0x80B`). **MSI waits for the driver RFC:** without interrupt remapping a
   device can aim any vector at any core — O-18's precondition.
-- **Latency** is §3's worst path between preemption points. RFC-0007's console write must take one per
-  FIFO-full poll, restartable by byte count; until then it holds the kernel about 44 ms per 504 bytes on
-  hardware (nothing on QEMU, which has no baud delay).
+- **Latency** is §3's worst path between preemption points. RFC-0007 (proposed)'s console write never waits —
+  at most 24 flag reads and 24 stores per entry — so it needs no preemption point.
 
 ## 12. Multi-core shape, placement and exclusive cores (verdict 11)
 
@@ -353,9 +370,10 @@ Phase 1 runs `-smp 1`; the shape is fixed now so multicore is not bolted on.
   live elsewhere**: a thread whose registers core X owns lazily, run next on core Y, has Y ask X by IPI to save
   them. Cost: a cross-core FP handoff is an IPI round trip.
 - **Cores are parked until funded (default-deny).** On QEMU `virt` with `-kernel` the DTB advertises PSCI and
-  secondaries start powered off (checked on QEMU 8.2.2: CPU 1 never leaves the entry address), so `boot.s`'s
-  `wfe` loop matters only on spin-table firmware. The first `sc_configure` onto a core starts it — PSCI
-  `CPU_ON`, conduit from `/psci`; INIT-SIPI-SIPI on x86_64 — in increment 14, `boot.s`'s comment with it.
+  secondaries start powered off (checked on QEMU 8.2.2 and the pinned 11.0.3: CPU 1 never leaves the entry
+  address; the conduit is `hvc` unless `virtualization=on`), so `boot.s`'s `wfe` loop matters only on spin-table
+  firmware. The first `sc_configure` onto a core starts it — PSCI `CPU_ON`, conduit from `/psci`; INIT-SIPI-SIPI
+  on x86_64 — in increment 14, `boot.s`'s comment with it.
 - **SMT placement, one sentence now** (research/0002 Part 6, after L1TF and MDS): a context will carry a class
   set only by the `SchedControl` holder; SMT siblings never run different classes, donation never crosses one.
   The field is reserved zero until increment 14, so no thread labels itself; SMT-off is "never fund the sibling".
@@ -366,7 +384,9 @@ Phase 1 runs `-smp 1`; the shape is fixed now so multicore is not bolted on.
 
 ## 13. Amendments proposed to accepted documents (verdict 12)
 
-Each, if accepted, is appended to its target as a dated amendment and logged in `docs/CHANGELOG.md` (Changed).
+Each of A1–A6, if accepted, is appended to its target as a dated amendment and logged in `docs/CHANGELOG.md`
+(Changed). C1 is not an amendment this RFC can propose: constitution text is the maintainer's alone (§4, §11.1),
+so C1 only names the question A1 raises, and A1 cannot be accepted without an answer to it.
 
 | # | Target | Change | Why |
 |---|--------|--------|-----|
@@ -374,13 +394,16 @@ Each, if accepted, is appended to its target as a dated amendment and logged in
 | A2 | RFC-0004 amendment 2026-08-01 | a caller short *now* waits `Throttled`; only a context that can *never* pass is refused | refusal makes clients spin; nothing is donated below the bar either way |
 | A3 | the same, and research/0002 Part 6 | seL4's timeout faults ship in MCS (`seL4_Fault_Timeout`); what is unmerged is RFC-14's threshold | a factual correction to "have remained future work" |
 | A4 | RFC-0003 §14.2 | the big lock covers the fast path by design; the question is closed by rejecting its premise | §12; Peters et al. 2015 |
+| A5 | research/0002 Part 6 | budgets are caps, not minima: the kernel enforces a sporadic cap, and a guaranteed minimum is the `SchedControl` holder's admission policy | verdict 4; a cap is what makes fixed-priority admission sound, and a kernel-guaranteed minimum would be policy (§5) |
+| A6 | RFC-0003 §6 | a capability may also rest in a kernel-held slot of a thread (`fault_ep`, `timeout_ep`), moved in and out with `TRANSFER` and generation-checked when used | RFC-0003's invariant names only "one table, or in flight in exactly one message"; the thread slots are a third place (§4) |
+| C1 | Constitution §3, "with priority inheritance" | for the maintainer: under A1, inheritance holds through donation to passive servers, and an active server runs on its own priority, a ceiling bounding the inversion (§7) | A1 narrows a constitutional clause, which no RFC can do on its own authority |
 
 ## 14. Lineage
 
 | Source | What is taken | What is left |
 |--------|---------------|--------------|
 | **seL4 MCS** (Lyons et al. 2018) | contexts as objects; passive servers; `SchedControl`; any-capability MCP; sporadic refills; `MIN_BUDGET`; timeout faults and TCB-held handlers; priority-ordered endpoint queues; no donation to active receivers | the WCET scale factor |
-| **seL4 RFC-14** (Johnston) | the endpoint threshold, deferral, one-layer return | budget limits, for now |
+| **seL4 RFC-14** (Johnston) | the endpoint threshold, deferral, and the one-layer return (its budget-limit mechanism, applied here to expiry) | budget limits, for now |
 | **Heiser & Elphinstone 2016; Fluke 1999; Elphinstone & Heiser 2013** | the event kernel; the running thread unqueued; priority-aware direct switch | per-thread kernel stacks; lazy scheduling; L4's unconditional switch |
 | **QNX Neutrino; Ford & Lepreau 1994** | inheritance across the message; partitions on budgets; the migrating-thread `call` | inheritance to busy servers; Mach |
 | **Sprunt, Sha & Lehoczky 1989; Zircon** | the sporadic server; the timer object | an unbounded replenishment list; per-thread timeslices |
@@ -402,7 +425,7 @@ Each, if accepted, is appended to its target as a dated amendment and logged in
 
 | Grave | How this RFC stays out of it |
 |-------|------------------------------|
-| **Policy in the kernel** | no admission, balancing or budget choice; the constants it does choose are 256 levels, eight refills, `MIN_BUDGET`'s factor 2, the XCR0 extent, the thread and deadline array capacities (RFC-0005), and §19's interim constants until measured |
+| **Policy in the kernel** | no admission, balancing or budget choice; the constants it does choose are 256 levels, eight refills, `MIN_BUDGET`'s factor 2, the `XCR0` extent, the thread and deadline array capacities (RFC-0005), and §19's interim constants until measured |
 | **The catch-all right** | priority authority is a relation (MCP); `SchedControl` has one mutating method, selling time on one core, and a read of its own state; topology is data, routing is `IrqControl`'s; §4's list is closed |
 | **Bolted-on multicore** | per-core state, IPIs, the lock and its IPI-servicing spin, FP handoff, shootdowns and core start-up are stated before any SMP code |
 | **Drivers in the kernel; unused device paths** | the kernel masks and signals, never services a device; one controller and one timer per target; unclaimed lines never enabled |
@@ -433,21 +456,27 @@ Each, if accepted, is appended to its target as a dated amendment and logged in
 5. **Numbers from measurement:** `MIN_BUDGET`, stack size, the worst path; x86_64's clock without invariant TSC.
 6. **Interrupt routing on SMP:** per-(line, core) handlers minted by `IrqControl`, or a per-core interrupt-target
    capability — decided with increment 14.
+7. **Priority authority from a rightless capability.** §6 lets any capability to a thread, a rightless one
+   included, lend its MCP, as seL4 does; but the crate documents `Rights::NONE` as a capability that "permits
+   nothing, though it still names its object" (`capability/src/rights.rs`). Keep seL4's rule, with RFC-0003
+   noting that naming alone confers MCP, or require a right on `auth`?
 
 ## 19. Implementation increments
 
 Pure logic lands in a new host-tested `no_std` workspace crate, `scheduler/`, generic over a thread index as
 `capability/` is over `ObjectRef` (`CLAUDE.md` § Layout gains it in increment 1); hardware behaviour is proved by
 counted boot-test strings. New `unsafe` stays in `kernel/src/arch/**`. The x86_64 HAL gains stubs that compile —
-`-> !` ones halt — so its entry still calls into the kernel proper. **D** marks what the demo needs.
+`-> !` ones halt — so its entry still calls into the kernel proper. **D** marks what the demo needs. The merged
+order across RFC-0005, RFC-0006 and RFC-0007 is RFC-0007 (proposed) §18's; the "Lands after" column states this
+RFC's constraints on it.
 
 | # | PR | Proves; how tested | Lands after | D |
 |---|----|--------------------|-------------|---|
 | 1 | `scheduler` I: run queues, the ten states, MCP, the priority-ordered endpoint queue | exhaustive host transition table against §4's "Left by" column; "a new thread cannot serve as `auth` above 0"; built for both targets | — | D |
 | 2 | `scheduler` II: full contexts, nanosecond conversion and rounding, billing, stall counters, interim constants | host tests against a shadow model | 1 | D |
-| 3 | GICv3 and the virtual timer, kernel-only; `CNTKCTL_EL1`, `PMUSERENR_EL0` zeroed; idle and its abandon-idle stub | xtask gains `gic-version=3`; `timer: tick 3` | — (physical addresses; 0005#9 must repoint the GIC with the console) | D |
-| 4 | Event-kernel dispatch at EL0, no address spaces yet: TCB frames and dispatch under RFC-0007#3's trap stub; §8's `SCTLR_EL1` bits | two EL0 self-test threads alternate under the timer: `sched: A B A B`; an EL0 `wfi` returns: `sched: wfi yields` | 3, 0007#3 | D |
-| 5 | Threads in address spaces; the boot stack moved into the guarded window, `aarch64.ld`'s comment with it | a spinning EL0 thread is preempted and resumes intact: `user: still here` | 4, 0005#10 | D |
+| 3 | GICv3 and the virtual timer, kernel-only; `CNTKCTL_EL1`, `PMUSERENR_EL0` zeroed; idle and its abandon-idle stub | xtask gains `gic-version=3`; `timer: tick 3` | — (physical addresses; 0005#10 repoints the GIC with the console) | D |
+| 4 | Event-kernel dispatch at EL0, no address spaces yet: TCB frames and dispatch under RFC-0007#3's trap stub; §8's `SCTLR_EL1` bits | two EL0 self-test threads alternate under the timer: `sched: A B A B`; an EL0 `wfi` returns: `sched: wfi yields`; retired with the MMU-off self-tests by 0005#9, and 5 re-proves preemption | 3, 0007#3 | D |
+| 5 | Threads in address spaces, on the guarded per-core stack 0005#10 installs | a spinning EL0 thread is preempted and resumes intact: `user: still here` | 4, 0005#13 | D |
 | 6a | Thread, SchedContext, `SchedControl` as RFC-0005 object-store slots; state machine wired; `(index, generation)` links | host: destroy a lent context, reuse the slot, `reply` — nothing moves | 2, 0005#7 | D |
 | 6b | Methods behind RFC-0007's dispatcher: `sc_configure`, `bind_sc`, `resume`, `set_priority`, `write_regs`, `thread_exit` | the root runs two EL0 threads at one level: `[a] 1 [b] 1 [a] 2` | 5, 6a, 0007#6 | D |
 | 7a | The direct-switch decision as a pure function | host tests over every §6 case | 1 | D |
@@ -459,7 +488,7 @@ counted boot-test strings. New `unsafe` stays in `kernel/src/arch/**`. The x86_6
 | 11 | Lazy FP/SIMD | two FP threads load markers into `v0`, each finds its own: `fp: isolated`; host: owner destroyed, slot reused, zeros loaded | 6b | |
 | 12 | `IrqControl` and `IrqHandler`; xtask gains serial input injection | PL011 receive (SPI 1, INTID 33) reaches an EL0 driver: `irq: notified` | 7c | |
 | 13 | x86_64 scheduling HAL (IDT, TSS, IST, LAPIC, `#NM`, `XSAVE`) | 3–5 and 11 again | its boot RFC, 0007#12 | |
-| 14 | SMP: PSCI `CPU_ON`, INIT-SIPI, the lock and its IPI-servicing spin, FP handoff, shootdowns, classes, routing | `-smp 2` boot-tests | 13 | |
+| 14 | SMP: PSCI `CPU_ON`, INIT-SIPI-SIPI, the lock and its IPI-servicing spin, FP handoff, shootdowns, classes, routing | `-smp 2` boot-tests | 13 | |
 | 15 | Deadline objects (RFC-0004 §9.3) | host tests on the shared release queue; `deadline: fired` | 9 | |
 
 **What the demo takes as interim, honestly.** It needs 1–7c and runs full contexts only.
@@ -470,8 +499,8 @@ counted boot-test strings. New `unsafe` stays in `kernel/src/arch/**`. The x86_6
 - **Provisional constants** in `scheduler/src/config.rs` until measured: `MIN_BUDGET_INTERIM` = 100 µs;
   `ROOT_TIMESLICE` = 5 ms, a full context; root priority and MCP 255, the root putting itself and the client at
   100 to share a level; `KERNEL_STACK_SIZE` = 16 KiB. Cost: the budget floor is a guess.
-- **No fault handler** (a faulting thread goes `Inactive`, RFC-0007 §7); **a non-preemptible console write**
-  (free on QEMU, 44 ms on hardware); **no userspace timer** for RFC-0004's watchdog; **x86_64 stubs** that halt.
+- **No fault handler** (a faulting thread goes `Inactive`, RFC-0007 §7); **no userspace timer** for RFC-0004's
+  watchdog; **x86_64 stubs** that halt.
 
 ## 20. What this unblocks
 
diff --git a/docs/rfcs/0007-system-calls-and-process-bootstrap.md b/docs/rfcs/0007-system-calls-and-process-bootstrap.md
index c86f70a..a0f4686 100644
--- a/docs/rfcs/0007-system-calls-and-process-bootstrap.md
+++ b/docs/rfcs/0007-system-calls-and-process-bootstrap.md
@@ -7,9 +7,9 @@
 | Status | **Proposed** — 2026-09-27, awaiting the maintainer's verdict |
 | Author | Drafted by Claude Code as sparring partner; verdict the maintainer's |
 | Date | 2026-09-27 |
-| Affects | Constitution §3 (capabilities are the only authority; the Language clause) and §4 (a Borrow Ledger reading, §12); `CLAUDE.md` § `unsafe` policy and § Layout; threat model O-6's text; RFC-0003 (a dated amendment: the handle word, a slot-generation bound, `free_slots`, one error variant split); RFC-0004 §8 (a dated amendment: reply objects are unbound, not destroyed); `docs/CHANGELOG.md`; the workspace (`user/`), the comments in `Cargo.toml` and `xtask/Cargo.toml`, `kernel/src/main.rs`'s grep scope; `xtask`, `kernel/build.rs` and `aarch64.ld`; the kernel's trap path |
+| Affects | Constitution §3 (capabilities are the only authority; the Language clause) and §4 (a Borrow Ledger reading, §12); `CLAUDE.md` § `unsafe` policy and § Layout; threat-model O-6's text; RFC-0003 (a dated amendment: the handle word, a slot-generation bound, `free_slots`, one error variant split); RFC-0004 §8 (a dated amendment: reply objects are unbound, not destroyed); `docs/CHANGELOG.md`; the workspace (`user/`), the comments in `Cargo.toml` and `xtask/Cargo.toml`, `kernel/src/main.rs`'s grep scope; `xtask`, `kernel/build.rs` and `aarch64.ld`; the kernel's trap path |
 | Depends on | RFC-0003 (accepted; §9 binds every syscall); RFC-0004 (accepted; §5, §6, §8, §9.4, §10 and the 2026-08-01 amendment); RFC-0005 and RFC-0006 (proposed, drafted alongside); a future x86_64 boot RFC for the UEFI stub |
-| Discharges | O-5 (argument validation) for the syscall surface; O-27 (explicit authority at spawn); binds O-1, O-2 and O-4 at B1; keeps O-6 Built with a third designated tree; contributes to O-7, O-9 and O-13; designs O-17's fault path |
+| Discharges | O-5 (argument validation) for the syscall surface; O-27 (explicit authority at spawn); binds O-1 and O-2 at B1; discharges O-4 at the ABI, bar the fault-report interim; keeps O-6 Built with a third designated tree; contributes to O-7, O-9 and O-13; designs O-17's fault path |
 
 > **Proposed verdicts.**
 >
@@ -25,7 +25,7 @@
 > 10. **One root task,** built once from a load descriptor, every boot capability listed in BootInfo, no "is root" branch anywhere (§9).
 > 11. **Boot images:** `arch::boot_modules()` yields descriptors a host-side ELF reader made; the kernel parses no ELF; AArch64 embeds, as an interim (§10).
 > 12. **Console as a capability:** one `WRITE` of at most 24 bytes that never waits; deleted when the Phase-2 UART driver lands (§11).
-> 13. **`user/abi`** is the microkernel-core row; its `src/arch/**` — trap instructions and entry stubs only — is the third `unsafe` tree (§12).
+> 13. **`user/abi`** is the microkernel-core row; its `src/arch/**` — trap instructions, a register read and entry stubs — is the third `unsafe` tree (§12).
 
 ## 1. The question
 
@@ -49,7 +49,8 @@ traversal), and O-27 exists because of it. Boot images reach userspace read-only
 **AArch64 — `svc #0`** traps from EL0 to `VBAR_EL1 + 0x400` with `ESR_EL1.EC = 0x15`, the immediate in
 `ISS[15:0]`, `ELR_EL1` past the `svc`, DAIF masked and `SP_EL1` selected *(Arm ARM DDI 0487)*. The stub
 saves `x0`–`x30`, `SP_EL0`, `ELR_EL1` and `SPSR_EL1` into the thread's frame (RFC-0006 (proposed) §9 owns
-the layout) and dispatches on EC: `0x15` is a syscall, anything else a *fault* (§7). A non-zero immediate
+the layout) and dispatches on EC: `0x15` is a syscall, `0x01` (an EL0 `wfi`, completed as `yield`) and `0x07`
+(first FP/SIMD use) are RFC-0006 §8's and §10's, anything else a *fault* (§7). A non-zero immediate
 answers `InvalidArgument`, so a later ABI revision is detectable. `eret` uses an `SPSR_EL1` the kernel
 builds: EL0t, DAIF clear, NZCV from the frame, `DIT` and `SSBS` where implemented (the Cortex-A72 has
 neither), every other bit zero.
@@ -121,8 +122,8 @@ payload-free doorbell; an `IrqHandler` ORs its bound bits (RFC-0006 §11). **Rej
 **Reply objects** are created once from a Pool and reused *(seL4 MCS)*: `recv` binds one to a caller, and
 `reply`, budget expiry or the caller's death **unbinds** it; `reply` on an unbound one fails `PeerGone`.
 RFC-0004 §8 says it "is destroyed if the caller dies", which would let a client that calls and exits in a
-loop cost the server a Pool allocation per request — an O-7 drain — so RFC-0004 needs a dated amendment and
-RFC-0006 §4 and §7 read "unbinds".
+loop cost the server a Pool allocation per request — an O-7 drain — so RFC-0004 needs a dated amendment, which
+RFC-0006 (proposed) §4 and §7 already follow.
 
 **Kernel-object methods.** A method is a `call` whose label names it and whose MR0–MR3 carry every
 argument; one needing more is split. A handle word there is **presented**: resolved in the caller's table,
@@ -138,13 +139,13 @@ from MR0; labels count from 1 per kind; the `abi` data half (increment 2) is the
 | Pool (`WRITE`) | 2 `as_create` · 3 `process_create` | rights · AddressSpace, presented `WRITE`, bound for life | — | — | — | AddressSpace · Process |
 | Pool (`WRITE`) | 4 `thread_create` | Process, presented `WRITE` | its AddressSpace, presented `WRITE` | IPC-buffer address, or 0 for none | — | Thread |
 | Pool (`WRITE`) | 5 `sc_create` · 6 `endpoint_create` · 7 `notification_create` · 8 `reply_create` | — · `min_budget` in ns (RFC-0006) · — · — | — | — | — | the new object |
-| AddressSpace (`WRITE`) | 1 `map` · 2 `unmap` · 3 `protect` (RFC-0005 §8) | Region, presented · vaddr · vaddr | the space's Pool, presented `WRITE` · — · perms | vaddr | first page (bits 0–31), pages (32–41), perms (48–49) | — |
-| Region (`WRITE`) | 1 `region_copy` (RFC-0005, proposed here) | source Region, presented `READ` | source page | destination page | pages, at most 16 | — |
+| AddressSpace (`WRITE`) | 1 `map` · 2 `unmap` · 3 `protect` (RFC-0005 §8) | Region, presented · vaddr · vaddr | the space's Pool, presented `WRITE` · — · perms | vaddr · — · — | first page (bits 0–31), pages (32–41), perms (48–49) · — · — | — |
+| Region (`WRITE`) | 1 `region_copy` (RFC-0005 §8) | source Region, presented `READ` | source page | destination page | pages, at most 16 | — |
 | Process (`WRITE` / `READ`) | 1 `GRANT` · 2 `KILL` · 3 `INFO` (§8) | handle words, **moved**, count in `tag.length` | | | | `GRANT`: words in the child; `INFO`: counts |
-| Thread (`WRITE` / `READ`; RFC-0006 §4) | 1 `write_regs` · 2 `read_regs`, a four-word group of RFC-0006's frame in label bits 8–15, group 0 being PC, SP, `a0`, `a1` | `write_regs`: the group's four words in MR0–MR3 | | | | `read_regs`: the group |
-| Thread (`WRITE`; RFC-0006 §4) | 3 `resume` · 4 `suspend` · 5 `bind_sc` · 6 `unbind_sc` · 7 `set_priority` · 8 `set_mcp` · 9 `bind_notification` · 10 `unbind_notification` · 11 `set_fault_ep` · 12 `set_timeout_ep` · 13 `set_fp` | 5: SchedContext, presented `WRITE` · 7, 8: `auth`, presented, no right checked · 9: Notification, presented `READ` · 11, 12: endpoint, **moved** · 13: on or off | 7, 8: the value | — | — | — |
+| Thread (`WRITE` / `READ`; RFC-0006 §4) | 1 `write_regs` · 2 `read_regs`, a four-word group of RFC-0006's frame in bits 8–15 of the label, group 0 being PC, SP, `a0`, `a1` | `write_regs`: the group's four words in MR0–MR3 | | | | `read_regs`: the group |
+| Thread (`WRITE`; RFC-0006 §4) | 3 `resume` · 4 `suspend` · 5 `bind_sc` · 6 `unbind_sc` · 7 `set_priority` · 8 `set_mcp` · 9 `bind_notification` · 10 `unbind_notification` · 11 `set_fault_ep` · 12 `set_timeout_ep` · 13 `set_fp` | 5: SchedContext, presented `WRITE` · 7, 8: `auth`, presented, no right checked · 9: Notification, presented `READ` · 11, 12: endpoint, `WRITE`, **moved** · 13: on or off | 7, 8: the value | — | — | — |
 | SchedControl (RFC-0006 §5) | 1 `sc_configure` (`WRITE`) · 2 `ctl_info` (`READ`) | SchedContext, presented `WRITE` | budget, ns | period, ns | refills (bits 0–7), class (8–15, zero) | `ctl_info`: counts |
-| SchedContext (`READ`) · Console (`WRITE`) | 1 `sc_stats` · 1 `WRITE` (§11) | — · byte count, at most 24 | · bytes | · bytes | · bytes | counters · bytes accepted |
+| SchedContext (`READ`) · Console (`WRITE`) | 1 `sc_stats` · 1 `WRITE` (§11) | — · byte count, at most 24 | — · bytes | — · bytes | — · bytes | counters · bytes accepted |
 
 `IrqControl` and `IrqHandler` (RFC-0006 §11) follow the same rule, labelled when built. Endpoints and
 notifications have no methods: they are what `send`, `call` and `recv` act on.
@@ -209,7 +210,7 @@ in RFC-0003: `Handle::to_word`/`from_word`, `MAX_SLOT_GENERATION`, a `const` bou
 
 **Transport status** (`x0`/`rax`) is what the syscall layer found, identical for a kernel object or a
 server. Every failure is atomic. The detail register names the culprit: 0 the invoked handle, 1–4 a handle
-word in MR0–MR3, 5–7 `caps[0..2]`, 8 the tag, 9 the reply handle, 10 the IPC buffer.
+word in MR0–MR3, 5–7 `caps[0]`–`caps[2]`, 8 the tag, 9 the reply handle, 10 the IPC buffer.
 
 | # | Status | Meaning |
 |---|--------|---------|
@@ -233,13 +234,13 @@ label) share one vocabulary for kernel and server, so a stand-in reports errors
 label)*: the numbers above, then 13 `InvalidMethod`, 14 `PoolExhausted`, 15 `Fragmented` (RFC-0005) and 16
 `WindowClosed` (§8).
 
-**Faults** — EL0 exceptions that are not syscalls — are not return values: the thread is suspended and a
-fault message goes to its `fault_ep` (RFC-0006 §4), so a supervisor can restart a driver (O-17).
-**Interim, until increment 11:** the kernel prints one line (thread, `ESR`, `ELR`, `FAR`) and leaves the
-thread `Inactive`. **Its cost:** an **ambient output channel** — a thread holding no Console can put two
-chosen words on the operator's line by faulting, once per thread it can create, each line about 100 bytes
-of kernel UART time. It builds only under a `report-user-faults` feature `xtask` enables for Phase-1
-boot-tests and `run-qemu`, and it qualifies the O-4 and O-9 rows (§14).
+**Faults** — EL0 exceptions that are neither syscalls nor RFC-0006's `wfi` and FP/SIMD traps — are not return
+values: the thread waits `BlockedOnReply` while a fault message goes to its `fault_ep` (RFC-0006 §4), so a
+supervisor can restart a driver (O-17). **Interim, until increment 11:** the kernel prints one line (thread,
+`ESR`, `ELR`, `FAR`) and leaves the thread `Inactive`. **Its cost:** an **ambient output channel** — a thread
+holding no Console can put two chosen words on the operator's line by faulting, once per thread it can create,
+each line about 100 bytes of kernel UART time. It builds only under a `report-user-faults` feature `xtask`
+enables for Phase-1 boot-tests and `run-qemu`, and it qualifies the O-4 and O-9 rows (§14).
 
 ## 8. The Process object and spawning (O-27)
 
@@ -263,8 +264,8 @@ process consents to by receiving. It is **single-use** in research/0002's sense
 response-wrapping) but lacks **prior-use detection**, which is the broker RFC's.
 
 **What the window closes, exactly: capability injection.** Once started, no holder of the Process
-capability adds to its table, and `WRITE` on it means `KILL` alone, so a supervisor can hold kill-and-
-inspect authority without the child's power (O-17). It does **not** close **control**: `WRITE` on the
+capability adds to its table, and `WRITE` on it means `KILL` alone, so a supervisor can hold
+kill-and-inspect authority without the child's power (O-17). It does **not** close **control**: `WRITE` on the
 child's AddressSpace maps into it and, beside `WRITE` on the Process, creates threads in it; `WRITE` on a
 Thread rewrites its registers (RFC-0006 §4). That is authority over the child's code and data, which its
 loader always had — and why thread creation presents the AddressSpace: a Process capability alone cannot
@@ -277,7 +278,7 @@ keeps only the Process capability. A spawner that derived copies first keeps con
 tell, and the child cannot yet check (Open question 3).
 
 **Lifetime.** A Process ends by `KILL`, or when no capability names it and none of its threads can run
-again. One whose threads have all `Exited` is dead but intact, inspectable through `INFO` until then
+again. One whose threads have all `Exited` is dead but intact, inspectable through `INFO` until it ends
 *(seL4: objects live until destroyed)*. **Rejected:** ending with the last thread *(Zircon)* — undefined for
 a newborn, and it destroys what a supervisor would inspect. The spawner passes handle words in `a0` and
 `a1` (the demo's Console and endpoint), or a start Region in `a0` — a runtime convention, not kernel ABI.
@@ -285,8 +286,8 @@ a newborn, and it destroys what a supervisor would inspect. The spawner passes h
 ## 9. The root task and boot info
 
 The one act the kernel performs unasked: at boot it builds **exactly one** process from the first boot
-module and gives it every boot capability *(seL4's root task; research/0002 Part 3, "the bootstrap seam is
-a one-time kernel act")* — an AddressSpace, the segments mapped as in §10, a stack, a read-only
+module and gives it every boot capability *(seL4's root task; research/0002 Part 3 and its synthesis, "the
+bootstrap seam is a one-time kernel act")* — an AddressSpace, the segments mapped as in §10, a stack, a read-only
 **BootInfo** page, a Process and a Thread in §3's entry state with `a0` = BootInfo's address and `a1` = 0.
 Its priority, ceiling and full context are RFC-0006 (proposed) §6's one bootstrap act.
 
@@ -306,7 +307,7 @@ the kernel); a `spawn_from_module` syscall (a loader as a kernel service); a `sy
 
 **Verdict sought — the mechanism:** the kernel reaches modules through `arch::boot_modules()`, which yields
 fixed-shape **load descriptors** made on the host, and **never parses ELF**. A dependency-free, host-tested
-ELF64 reader in `xtask` emits an entry point; text (`R+X`), optional read-only (`R`) and data (`R+W`,
+ELF64 reader in `xtask` emits an entry point; text (`RX`), optional read-only (`R`) and data (`RW`,
 zero-padded to a page, with a `bss` size) segments, page-aligned in the user half; and stack and BootInfo
 addresses. It **refuses** a writable-and-executable, overlapping or unaligned `PT_LOAD`, `PT_DYNAMIC`,
 `PT_INTERP`, `PT_TLS`, `PT_GNU_RELRO` and an executable `PT_GNU_STACK`, ignoring `PT_NOTE` and a
@@ -315,24 +316,24 @@ before the image exists (O-13), and the kernel validates one fixed structure —
 code validating structures built elsewhere is the bug farm (research/0002 Part 7). **Rejected:** an
 in-kernel `elf/` crate, a parser in the TCB for no gain.
 
-**The source — an AArch64 interim: embedded in the kernel image.** QEMU's `-initrd` and `-device loader`
-add a second, QEMU-only artefact (`hw/arm/boot.c`, read at QEMU 8.2.2 and to be re-read at the pinned
-11.0.3, loads `-initrd` only for Linux images); children linked into the root's ELF *(seL4's CPIO
-archive)* would tie the root to each image. So `xtask` writes `payload.bin` — a versioned header, then per
-module a name, descriptor and segment bytes — named by `SETONIX_PAYLOAD`; `kernel/build.rs` re-runs on that
-variable and substitutes an empty bundle when it is unset, so a bare `cargo build` prints `boot modules:
-0`. A `global_asm!` `.incbin` under `kernel/src/arch/aarch64/` embeds it; `aarch64.ld` places it in a
-page-aligned, read-only, `KEEP`ed `.payload` section *(Hubris's `xtask dist`)*. **Cost:** a user change
-relinks the kernel. **On x86_64**, a future x86_64 boot RFC provides the UEFI stub that loads the same
+**The source — an AArch64 interim: embedded in the kernel image.** QEMU's `-initrd` and `-device loader` add a
+second, QEMU-only artefact (`hw/arm/boot.c`, re-read at the pinned 11.0.3, loads `-initrd` only for Linux
+images and silently ignores it for a bare ELF); children linked into the root's ELF *(seL4's CPIO archive)*
+would tie the root to each image. So `xtask` writes `payload.bin` — a versioned header, then per module a
+name, descriptor and segment bytes — named by `SETONIX_PAYLOAD`; `kernel/build.rs` re-runs on that variable
+and substitutes an empty bundle when it is unset, so a kernel from a bare `cargo build` prints
+`boot modules: 0`. A `global_asm!` `.incbin` under `kernel/src/arch/aarch64/` embeds it; `aarch64.ld` places
+it in a page-aligned, read-only, `KEEP`ed `.payload` section *(Hubris's `xtask dist`)*. **Cost:** a user
+change relinks the kernel. **On x86_64**, the future boot RFC provides the UEFI stub that loads the same
 bundle as a file; increment 12 depends on it.
 
 **Loading.** The kernel loads **module 0 only**; the others reach the root as **read-only Regions**
 (RFC-0005 §7) with descriptors in BootInfo *(Genode's core hands init boot modules read-only)*. Every
 loader, kernel or root, maps text `RX` and read-only data `R` **in place**, copies data pages into a fresh
-Region with `region_copy` — which RFC-0005 (proposed) provides as a page-granular, frame-to-frame copy, the
-one it already makes for the root (§7 there), so the demo needs that half of its copy module — and takes
-`bss` as fresh zeroed pages, so no loader maps a child's writable memory into itself. The programs are soft-float `no_std` crates on `abi` alone with no `unsafe`;
-on `x86_64-unknown-none` `xtask` passes `-C relocation-model=static -C code-model=small`.
+Region with `region_copy` — RFC-0005 (proposed) §8's page-granular, frame-to-frame copy, the one the kernel
+already makes for the root — and takes `bss` as fresh zeroed pages, so no loader maps a child's writable
+memory into itself. The programs are soft-float `no_std` crates on `abi` alone with no `unsafe`; on
+`x86_64-unknown-none` `xtask` passes `-C relocation-model=static -C code-model=small`.
 
 ## 11. The console as a capability
 
@@ -341,8 +342,8 @@ count in MR0, at most 24 bytes in MR1–MR3, sent verbatim (`abi`'s writer suppl
 waits:** the kernel stores bytes while the PL011's transmit-full flag is clear and returns the count
 accepted, and `abi` yields and retries the rest, so any waiting happens at EL0, preemptibly. The hold is at
 most 24 flag reads and 24 stores, inside RFC-0006 (proposed)'s measured worst path, so the console sets no
-floor under `MIN_BUDGET` and needs no preemption point. The root receives it with `DUPLICATE | TRANSFER |
-WRITE` (no input path, so no `READ`) and derives `WRITE`-only copies for chosen children; a program not
+floor under `MIN_BUDGET` and needs no preemption point. The root receives it with `DUPLICATE | TRANSFER | WRITE`
+(no input path, so no `READ`) and derives `WRITE`-only copies for chosen children; a program not
 handed one cannot print, but for §7's interim. **Rejected:** seL4's `DebugPutChar`, any thread's in a
 `CONFIG_PRINTING` build; a console at a well-known handle. **Adopted in spirit:** Zircon's write-only
 debuglog. Once a userspace UART driver exists the root hands out an endpoint speaking `WRITE`, no client
@@ -350,7 +351,7 @@ changes, and the Console object is **deleted** (increment 13).
 
 ## 12. `user/abi` — the kernel's own binding
 
-**Which ledger row.** The libc/runtime row ("port code — relibc pieces") gives a program an environment
+**Which ledger row.** The libc/runtime row ("Port code", relibc pieces) gives a program an environment
 and issues no syscalls: relibc sits on `redox_syscall`, versioned with the Redox kernel, and seL4 keeps
 libsel4 in its kernel's repository. The binding is the user half of §3's table, with nothing to port.
 **Verdict sought: the microkernel-core row, write ourselves**; anything that would read the same on
@@ -370,9 +371,9 @@ accessors in `user/abi/src/buffer/**`, whose invariant — the buffer stays mapp
 the thread runs — the process itself upholds; broken, it faults that thread and touches no other process.
 
 **The edits, all in increment 7:** `CLAUDE.md` § `unsafe` policy gains "`user/abi/src/arch/**` — trap
-instructions and process entry stubs" and § Layout gains `user/`; threat-model O-6 names three trees; the
-`Cargo.toml` comment ("the two trees") and `kernel/src/main.rs`'s grep widen to the repository; and
-`xtask/Cargo.toml`'s "No dependencies" becomes "no external dependencies".
+instructions, the discovery-register read and process entry stubs" and § Layout gains `user/`;
+threat-model O-6 names three trees; the `Cargo.toml` comment ("the two trees") and `kernel/src/main.rs`'s
+grep widen to the repository; and `xtask/Cargo.toml`'s "No dependencies" becomes "no external dependencies".
 
 ## 13. Lineage
 
@@ -388,7 +389,7 @@ not a syscall per operation), with **Linux**, **Hubris**, **Genode** and **Redox
 | O-2 non-widenability | `cap_derive` is the only duplication and is subset-only; presented handles move nothing; moves never widen (§4, §8) | **binds at B1** |
 | O-4 no ambient authority | twelve syscalls, each handle-indexed or authority-free; methods take handles; console by capability (§4, §11) | **discharged at the ABI, except the fault-report interim** (§7) until increment 11; each new method checked at review |
 | O-5 argument validation | no pointer arguments; reserved tag bits zero; single fetch at rendezvous; transfers all-or-nothing; kernel-built `SPSR_EL1`; `sysretq` guards (§3, §5, §7) | **discharged for the syscall surface**, with RFC-0005 §11 for user memory |
-| O-6 kernel memory safety | a third designated tree, trap instructions and entry stubs only; threat-model O-6 names it (§12) | **stays Built**, with a repository-wide grep |
+| O-6 kernel memory safety | a third designated tree, trap instructions, the discovery-register read and entry stubs only; threat-model O-6 names it (§12) | **stays Built**, with a repository-wide grep |
 | O-7 no unprivileged exhaustion | 512-byte copy bound; creation paid by a named Pool; reusable reply objects; fixed tables fail closed; a console that never waits (§4, §5, §11) | **contributes** — RFC-0005 owns the accounting |
 | O-9 no ambient side channel | result registers carry results or zero; no grant after start; no ambient console (§3, §8, §11) | **contributes**, except the fault-report interim (§7) |
 | O-13 W^X | the build refuses writable-and-executable segments; loaders map per descriptor (§10) | **contributes** — RFC-0005 owns enforcement |
@@ -428,11 +429,16 @@ not a syscall per operation), with **Linux**, **Hubris**, **Genode** and **Redox
 1. **Fault messages and death** — their layout (this RFC's), how a supervisor learns a process died, and
    how it supervises threads a child creates itself (RFC-0006 §4); likely a notification bound at creation.
 2. **Badges** — `cap_derive`'s badge word is reserved zero until RFC-0003a; notification signals then carry it.
+   §3's table also has no register yet for the badge of the capability a message arrived through, which a
+   server multiplexing clients needs (O-21, O-26); RFC-0003a is to assign one before this ABI is frozen.
 3. **A sovereignty check** — should RFC-0005's AddressSpace query report its live-capability count, as
    RFC-0006's `ctl_info` does for `SchedControl`, so a child can confirm it holds the only one?
 4. **The Language clause** — do single-instruction `svc`/`syscall` wrappers and entry stubs in userspace
    fall within "minimal assembly … for boot and context switching", as RFC-0005 §17.7 asks for `TLBI`?
 5. **The 64-word budget** — a verdict now, to be revisited with the first measurements.
+6. **The root is not the broker** — the root holds every boot capability (§9). The broker RFC must say how the
+   broker is spawned from it holding only what mediation needs, and what the root then drops, so that a
+   compromised broker's reach stays bounded (O-22).
 
 ## 18. Implementation increments
 
@@ -454,8 +460,9 @@ prefixed strings, since bare `Kaya!` matches the kernel's greeting; every demo l
    through a Console handle, `--features syscall-selftest --expect "[el0] Kaya!"`.
 7. **[demo] The root reaches EL0** — `user/abi/src/arch/**` and every §12 edit in one PR, once the tree is
    approved; module 0 becomes the root: `--expect "boot modules: 2" --expect "[root] up"`.
-8. **[demo] `GRANT`, the window, `INFO`, `KILL`** in a host-tested `process/` crate, then wired: born empty;
-   `GRANT` all-or-nothing; `WindowClosed` after the first resume; an AddressSpace bound once.
+8. **[demo] `GRANT`, the window, `INFO`, `KILL`** in a host-tested `process/` crate (`CLAUDE.md` § Layout gains
+   it), then wired: born empty; `GRANT` all-or-nothing; `WindowClosed` after the first resume; an AddressSpace
+   bound once.
 9. **[demo] The root spawns the client,** in three PRs:
     - **a.** A host-tested `no_std` `user/loader` crate: descriptor in, method calls out, W^X and overlaps
       refused; a host test that the spawner ends holding only the Process capability.
@@ -464,22 +471,26 @@ prefixed strings, since bare `Kaya!` matches the kernel's greeting; every demo l
     - **c.** O-27 evidence: the client probes indices 0–63 at generation 1 with `cap_rights` (exhaustive
       while no slot has been vacated), printing `[client] 2 handles`, and the root prints `INFO`'s count,
       `[root] client: 2 caps`. Evidence, not proof: the proof is increment 8's host test.
-10. **[demo] IPC syscalls** over RFC-0004 endpoints, reusable Reply objects and RFC-0006's blocking states:
+10. **[demo] IPC syscalls** over RFC-0004 endpoints, reusable reply objects and RFC-0006's blocking states:
     `[client] -> Kaya!`, `[server] <- Kaya!`, `[client] <- Kaya!` in order. Host test: clients that exit
     mid-call leave the server's Pool balance unchanged.
 11. **Fault messages and death notification** (§17.1): the root prints `[root] child faulted`, and
     `report-user-faults` leaves the boot-tests.
-12. **x86_64 trap path and `abi` stubs** (`EFER.SCE`, `LSTAR`/`STAR`/`FMASK`, `swapgs`, the `sysretq`
-    guards), after the x86_64 boot RFC's UEFI stub: the demo boot-tests on `q35`.
+12. **x86_64 trap path and `abi` stubs** (`IA32_EFER.SCE`, `IA32_LSTAR`/`IA32_STAR`/`IA32_FMASK`, `swapgs`,
+    the `sysretq` guards), after the x86_64 boot RFC's UEFI stub: the demo boot-tests on `q35`.
 13. **Delete the Console object** when the Phase-2 UART driver lands.
 14. **`Revoked`**: the crate's `ObjectDestroyed` split, with RFC-0005's destruction (its 17).
 15. **The root spawns the server** and stops serving, removing that interim.
 
-**Demo order across the three RFCs,** for the maintainer to fix: RFC-0005 1–8, RFC-0006 1–2 and this
-RFC's 1, 2 and 4 in any order → 3 → RFC-0006 3–4 → RFC-0005 9–10, retiring the MMU-off self-tests →
-RFC-0005 11–14 → RFC-0006 5 → 5–6 → 7 → 8 → RFC-0006 6a–6b → 9 → RFC-0006 7a–7b → 10 with RFC-0006 7c.
-RFC-0006 puts its 3–4 before RFC-0005's MMU and RFC-0005 after; this takes RFC-0006's, with RFC-0005's 10
-repointing the GIC, as RFC-0005 allows.
+**Demo order across the three RFCs** — the one merged order, to which RFC-0005 §18 and RFC-0006 §19 defer,
+for the maintainer to fix:
+
+1. **Before any EL0 code, MMU off,** as dependencies allow: RFC-0005 1–8, 11 and 12; RFC-0006 1–3, 6a and
+   7a; this RFC's 1, 2 and 4, with 5 after 2.
+2. **EL0 with the MMU off:** this RFC's 3, then RFC-0006 4.
+3. **MMU on:** RFC-0005 9–10, retiring the MMU-off EL0 self-tests and repointing the UART and the GIC.
+4. **Address spaces and the first userspace:** RFC-0005 13 → RFC-0006 5 → this RFC's 6 with RFC-0005 14 → 7 →
+   8 → RFC-0006 6b → 9 → RFC-0006 7b → 10 with RFC-0006 7c.
 
 **The demo's interims, with their costs:**