[Japabu]

Stage 0 of the native memory design: no kernel page is ever both writable and executable, on x86-64 and AArch64, and every boot checks it.

Problem

The kernel's direct map was one 2 MiB leaf per page, writable and executable (x86-64 kernel_leaf had no NX; AArch64's left PXN clear), and the kernel image runs from that map. So kernel text could be overwritten, and the heap, the stacks and every user frame's direct-map alias could be executed at CPL 0 / EL1 (issues/kernel-text-is-writable-and-every-kernel-page-executable.md).

Resulting behaviour

• Kernel leaves take a Prot. Each page of the kernel image follows its PT_LOAD flags (mm::Image). A 2 MiB page of the direct map stays one leaf wherever the image's protection is the same across it, and is split into 4 KiB leaves only where it holds two:

  • text is read-only and executable;
  • rodata is read-only and execute-never;
  • data and the boot stack are read-write and execute-never.

  Every other kernel leaf is read-write and execute-never. That covers the rest of the direct map, the heap, MMIO and the scanout. The image still runs from the direct map, so its text has exactly one mapping and no writable alias.

• x86-64 control registers. control_regs::init_cr0 is now init_paging. It writes the declared CR0 (WP) and EFER (NXE) before a CPU loads the kernel's tables: on the BSP before mm::init, and on an AP first thing in ap_entry. The NX CPUID check moves ahead of that write. control_regs::init no longer writes EFER, but its self-check still asserts it.

• x86-64 AP trampoline. It used to OR in LME. It now writes the declared EFER minus LMA (EFER_BEFORE_LONG_MODE) from its data block, so an AP enters long mode under the declaration. As a result, an AP left undeclared by no-ap-control-regs can still walk NX entries and reach the self-check that catches it.

• AArch64 WXN. SCTLR_EL1.WXN is now part of the declaration, so hardware forces every writable page execute-never at EL1 and EL0. The entry writes SCTLR before it turns translation on under the loader's boot map. That boot map therefore had to stop mapping the kernel's text writable:

  • toyos_bootmap::Plan takes the text range and splits the 2 MiB pages it shares;
  • each leaf is Access::Text or Access::Data;
  • the AArch64 encoding makes text read-only and everything else PXN.

  AArch64's boot map is now W^X too.

• x86-64 boot map. Its encoding makes the text read-only, but it cannot mark anything XD: the loader switches to the boot map before anyone has set NXE. That map stays writable and executable until each CPU loads the kernel's tables (filed below).

• The boot audit. kernel::wx::audit is a pure, host-tested walk with a decoder for each architecture. The boot runs it once its own mappings are made, after iommu::drivers_settled. It panics on any kernel leaf that is writable and executable, or executable outside the text, and otherwise logs paging: N kernel leaves, none writable and executable, none executable outside the text A..B. It judges each leaf by the leaf's own bits only, never crediting a table's narrowing, so it can be stricter than the hardware but never looser.

• Negative-control actuator. kernel-wx-leaf makes one direct-map leaf writable and executable before the audit runs.

Handoff, trampoline, patched code and early boot

• Loader to kernel. Both architectures' loaders map the text read-only in the boot map. The loader refuses an image with more or fewer than one executable segment, a writable one, or two segments sharing a page. mm::Image refuses the same.
• x86-64 AP trampoline. The BSP writes the page at 0x8000 only through the kernel's direct map, where it is read-write and NX. The AP executes it only through the boot map's identity view, and only after the copy. That boot map view is writable as well: this is the residual filed below.
• AArch64 join, the switch from the loader's map to the kernel's tables. It is a break-before-make. The two maps differ in block size and in permissions, and Arm ARM DDI 0487 M.d D8.17.1 requires break-before-make for a block-size change. So join runs from the image's identity alias under the old TTBR0, swaps TTBR1 to an empty root, runs TLBI VMALLE1, installs the kernel's root, and returns to the link address. Only then does it switch TTBR0, whose new root maps nothing. Interrupts stay masked throughout. QEMU models no TLB conflict, so this rests on the architecture, not on a test.
• AArch64 APs turn their MMU on under bringup_root, which shares the kernel's own W^X tables, with WXN already set, and then go through the same join.
• Patched code. The kernel patches no code of its own: rg finds no text patching. cache::make_executable cleans user frames through the direct map's data alias and is unchanged.

Decisions to look at

• The image keeps running from the direct map rather than from a separate image mapping. With the image's pages split, its text is the single mapping of those frames, so no alias exists to make read-only. This is simpler than the design's "the image runs from its own mapping", and it meets the same W^X property.
• The boot map changes on both architectures. AArch64 needs it because of WXN. On x86-64 it costs nothing and makes the text read-only from the first kernel instruction. The alternative was a two-phase SCTLR (enter without WXN, set it after join), which would have given the one declaration two values.
• The trampoline writes EFER from the declaration's own value. It already wrote EFER (LME), and now it applies the declaration instead of deciding a bit itself.
• SCTLR_EL1.UCI/UCT are not set here. The design's stage-0 row lists them, but they open EL0 cache maintenance for user JIT, which belongs to the user-memory stages the brief excluded.
• PT_GNU_RELRO is not made read-only. toyos-elf doesn't parse it, and teaching it to would change the sysroot's identity. It is filed instead.

Checks and evidence

Review r1 fixes, head aa2295250

The index is at https://github.com/ToyOSOrg/evidence/blob/6afdea6bb08e80ef6409cdee413b7ca729d58f99/r2/README.md.

• cargo run -- --ci host: exit 0, 87 steps green (log).
• Both --build-only builds: exit 0.
• Guest tests (the same 8 as below): 8 of 8 pass (log). They include SMP on virt at EL1 and at EL2 through the new join. The leaf counts fall to 4092 on q35 and 3184 on virt.
• The data-executable mutation, rerun here: 4 of 4 red, as wanted (log).
• no-ap-control-regs, run as a temporary probe that was then reverted (log):
  • the AP the actuator leaves undeclared holds the trampoline's efer=0x0d01;
  • it walks the kernel's NX tables and reaches the self-check;
  • the self-check stops the boot with cpu1 holds cr0=0xe0000011, the declaration is 0x80010033.
• Metal at b7a7b5827 (posted on the PR): the T14 passed with 12529 leaves and the AMD bench with 12390. The x86-64 mappings changed in r2, so both benches are restaged for aa2295250: T14, AMD.

First round, head b7a7b5827

The index is at https://github.com/ToyOSOrg/evidence/blob/b2796eb810f176286974aec225239a0076c1f101/README.md. Results for head b7a7b5827:

• cargo run -- --ci host: exit 0, 87 steps green (log).
• cargo run -- --build-only and --arch aarch64: both exit 0 (x86-64, AArch64).
• Guest tests: cargo test --test toyos-build -- kernel_wx_leaf_is_refused virt_user_mode virt_smp virt_el1_smp console_image_boots virt_early_panic virt_el2_drop, exit 0, 8 of 8 passed (log).
• Shipping boots with a temporary, uncommitted probe that prints the audit and control-register lines (log):
  • q35: 6647 leaves pass, 2 CPUs, cr0=0x80010033, efer=0x0d01;
  • virt: 5749 leaves pass, 8 CPUs at EL1 and at EL2, every CPU holding SCTLR_EL1=0x30d8199d (WXN set).
• New host tests: kernel::wx (10 tests: both decoders, leaf sizes, canonical and TTBR1 addresses, both rules); toyos-bootmap text splitting, encodings and refusals, plus an independent x86-64 walk that reads the text as read-only in both views.
• Negative controls, each applied as a checked patch and then reverted:
  • Data left executable, i.e. the direct map as it was before this change: the audit refuses 6197 to 6275 leaves on x86-64 and 4891 to 4902 on AArch64, and the shipping boots stop there (patch, log).
  • Boot-map text writable: 6 host tests fail (patch, log).
  • The audit reading the execute bit inverted: 10 of 10 host tests fail (patch, log).
• The mutation runs and the probe ran on the pre-commit tree. It differs from the head only by a comment reflow, issue text and a test-only clippy fix, so those results still apply to the head; the guest tests were also repeated on the head itself.

Integration tests and where they run

• kernel_wx_leaf_is_refused (q35, Profile::Metal, whose 16550 carries the panic) and virt_kernel_wx_leaf_is_refused (virt). Each needs a boot of its own because the audit's panic ends it. The judge requires the refusal to name the staged leaf, and no other leaf, under both rules. That also shows every leaf the boot made itself passed the same walk.
• Metal row kernel_wx (the T14 and the AMD bench) reads the shipping kernel's pass line from the shared testcases boot and adds no boot. Firmware, memory maps and machine tables differ on metal, which is why that row matters. It is staged and not yet run: the orchestrator runs it. Requests: T14, AMD (the AMD bench's run needs its --host). No AArch64 bench exists, so AArch64 has QEMU evidence only.

Arm sources

Every AArch64 bit position was checked against Arm's own documents, with hashes and pages recorded in the provenance file:

• SCTLR_EL1.WXN bit 19: Arm's system register XML 2023-12 (DDI 0601's source);
• WXN semantics: DDI 0487 M.d D8.4.1.2.4;
• descriptor bits: D8.3, Tables D8-48 and D8-52;
• the TTBR1 range: D8.2.4.

Issues

• Deleted kernel-text-is-writable-and-every-kernel-page-executable.md: its exit is met, including that the old direct map now reds the walk.
• Filed the-kernels-relro-stays-writable.md (Linux-parity residual; it takes the deleted issue's place in the security track) and x86-64s-boot-map-is-writable-and-executable.md.

Risks

• Metal at aa2295250 waits on the restaged runs. b7a7b5827 passed on both benches.
• The x86-64 boot map stays writable and executable (filed), and so does the trampoline page within it, until each CPU loads the kernel's tables.
• Kernel leaves written after the audit (MMIO for later claims) are covered only by construction: every writer goes through kernel_leaf(cache, Prot), and no Prot is both writable and executable.
• Only 2 MiB pages that hold two of the image's protections are split (a handful around the text, rodata and data boundaries). Nothing measured the cost of their 4 KiB TLB entries.
• AArch64 join's break-before-make cannot be shown by a test: QEMU models no TLB conflict, and there is no AArch64 bench. It rests on D8.17.1 and the code.

🤖 Generated with Claude Code

[Japabu]

Metal, head b7a7b5827, run by the orchestrator, shared testcases boot:

• T14 (ThinkPad T14 Gen 2): boot rc 0, kernel_wx PASS. paging: 12529 kernel leaves, none writable and executable, none executable outside the text
• AMD (Lenovo 82A2): boot rc 0, kernel_wx PASS. paging: 12390 kernel leaves, none writable and executable, none executable outside the text

[Japabu]

Review r1 — PR #984 at b7a7b5827

I read the commit, the whole diff, each changed file and the code around it: x86-64 paging.rs (map_2m, guard_4k, ensure_table, init), smp.rs (trampoline data and asm), control_regs.rs (init_paging, init, check, skipped), AArch64 boot.rs (apply_declaration, ap_start), paging.rs (map_direct, init, join, bringup_root, user_bits), the loader's load_kernel_elf and start_kernel, toyos_elf::Segment::page_range and overlapping_load_pages, and the bootmap plan and its tests. I checked the Arm citations against the PDF extract and the sysreg XML in the implementer's armdocs. I also read memory-design §4 and the §7 stage-0 row. Metal results are as posted: T14 and AMD both pass kernel_wx.

Architecture

The design fits the codebase. Kernel leaves now take a Prot, so a W+X leaf cannot be built through kernel_leaf on either architecture. The kernel builds its tables W^X from the start. The audit is a pure, host-tested decoder with a separate implementation from the encoders, and it runs on the live root, so it checks construction without trusting it. The image still runs from the direct map, with only its own 2 MiB pages split. That is simpler than the design's separate image mapping and gives the same property: the text frames have one mapping, RX, and nothing else in the kernel's tables is executable (executable_outside_text enforces this exactly). No decision in memory-design §8 for Jan depends on it. The orchestrator should still update §4 and stage 0 of the design to match ("image runs from its own mapping", "the whole direct map is NX", and UCI/UCT in the stage-0 row).

Control registers:

• x86-64: EFER and CR0 move into init_paging, which runs before each CPU loads the kernel's tables (BSP in after_console before mm::init, AP first in ap_entry). check still asserts both on every CPU.
• AP trampoline: it now writes the declaration (EFER_BEFORE_LONG_MODE) instead of choosing a bit itself. That is still one declaration with two appliers, both named in the module header.
• AArch64: WXN is in SCTLR and written with M=0 before translation turns on, after tlbi vmalle1, on every entry path (EL1, EL2 drop and AP). This respects "SCTLR_ELx.WXN is permitted to be cached in a TLB" (D8.4.1.2.4). This satisfies "one declaration, applied and asserted on every CPU".

The loader↔kernel contract holds together:

• Both sides derive the text from the same ELF with the same page_range offsets. The loader's extent.min() + offset matches the kernel's memory.start + extent.min() + offset.
• The boot map's text is RO in both views on both architectures. AArch64 data is PXN, the text's partial 2 MiB pages are split, and FINE_TABLES covers both splits.
• AArch64's switch-on happens in the kernel's own entry, from text that is RX in the identity view, so the loader's image going PXN costs nothing. AP identity comes from bringup_root, which reuses the kernel's W^X tables.
• The SMMU encoding is unchanged bit for bit (Data supplies the PXN that DEVICES used to).

Executable paths I checked:

• The x86 trampoline is copied through the NX direct map and fetched only through the boot map's identity view.
• Exception vectors, syscall entry, apply_declaration and ap_start are all in the single executable segment. Image::new and the loader refuse any other layout.
• make_executable cleans through the PXN alias. Arm allows that at EL1: IC IVAU raises no permission fault there (D7, "EL0 accessibility of cache maintenance instructions").
• User leaves stay PXN, and no Prot is RWX, so WXN cannot break a user mapping.
• I found no path that writes a kernel leaf after the audit without a Prot. The audit runs after iommu::drivers_settled, which covers every boot-time MMIO mapping.

Audit (kernel/pure/wx.rs):

• x86: PS is honoured at levels 1–2 only (PS in a PML4E is treated as a table, which is conservative). XD is bit 63, R/W is bit 1, and upper levels can only narrow (KERNEL_TABLE carries no XD and is ignored).
• AArch64: bit 1 is decoded per Table D8-48, so a reserved L3 descriptor is invalid and a level-0 block counts as a leaf, which is conservative. AP[2] and PXN follow Table D8-52.
• APTable, PXNTable and XNTable only narrow (D8.4.1.2.5), and so do WXN and "UnprivWrite removes PrivExecute" (D8.4.1.2.3). Ignoring them therefore makes the audit stricter, never looser.
• TTBR1 addressing matches T1SZ = 16 in TCR.
• Failure is a loud panic, the right response to an internal invariant violation.

Citations: Table D8-48 (p. D8-7735), Table D8-52 (p. D8-7742) and D8.4.1.2.4 (p. D8-7758) all say what the code cites. SCTLR_EL1.WXN is bit 19 in SysReg_xml_A_profile-2023-12/AArch64-sctlr_el1.xml. D8.2.4 is the TTBR0/TTBR1 selection section.

The negative control is test-only: kernel_wx_leaf's call site and both stage_writable_executables are cfg(feature = "boot-actuators"), and the accessor is const false without that feature. build/clippy.rs already lints the boot-actuators arms for both architectures. The judge requires exactly one leaf, at the staged address, under both rules, which also shows that every leaf the boot built passed.

Deleted paths: init_cr0 becomes init_paging and its one issue reference is updated; the second NX CPUID read is gone; the !kernel_elf.is_empty() guard goes because the loader always hands over the ELF. The deleted issue's exit is met, including "the old direct map reds the walk" (the data-executable mutation). No stale references remain outside issues/.

Size: production grows by about 535 lines net. That is wx.rs's decoder (~175), mm::Image (73), the bootmap Access plumbing and the two staging functions. Tests grow by about 330 lines (wx unit tests, bootmap plan and walk tests, one judge). That seems proportionate.

BLOCKER

1. kernel/src/arch/aarch64/paging.rs:740-748 — join's safety premise is now false, and the change it hides is the one Arm requires break-before-make for.

   • What: The doc says the loader's tables map "the code, stack and data this runs on exactly as the kernel's root does", and the SAFETY comment says they "map everything this function touches as they do". Before this PR that was true for the image. Now it is not:
     • The boot map maps the 8 MiB boot stack, the data and any 2 MiB page wholly inside the image as 2 MiB blocks. init (:702, held =>) maps every 2 MiB page the image overlaps as 4 KiB pages.
     • Rodata is RW+PXN in the boot map and RO+PXN in the kernel's tables.
   • Why it matters: join writes TTBR1_EL1 while the CPU fetches text and holds global TLB entries from the boot map for those VAs, and only then runs tlbi vmalle1. Arm ARM M.d D8.17 (p. D8-7859) requires break-before-make for "changing from a larger size to a smaller size". Without it, TLBs may "concurrently hold multiple different copies", with a TLB conflict abort or CONSTRAINED UNPREDICTABLE amalgamation as the permitted outcomes. The BSP runs this exact sequence on every AArch64 boot, on the stack and text whose block size just changed. QEMU does not model TLB conflicts, and no AArch64 bench exists, so nothing in the evidence could catch this.
   • Resolve by any of these:
     • (a) Make the old and new translations agree for what join touches. One way: split only the 2 MiB pages whose protection is not uniform, see S1 (which also keeps the stack in blocks), and have the boot map split the same pages.
     • (b) Perform a real break-before-make for TTBR1: from the identity alias, switch to an empty TTBR1, tlbi vmalle1, dsb, then install the new root.
     • (c) Show from the Arm ARM that a TTBR switch followed by tlbi vmalle1 is exempt.

   Whichever you pick, rewrite the doc and SAFETY text to state the real argument.

2. kernel/src/arch/x86_64/paging.rs:76 — stale doc. "Every bit of a 2 MiB kernel-half leaf but its address and size" no longer holds: kernel_page (:82-86) uses kernel_leaf for 4 KiB leaves too, and that wrapper's doc exists only to excuse the stale one. Fix the kernel_leaf doc to cover both sizes, with the PAT-bit caveat for non-Normal policies, and inline kernel_page at its one caller.

SUGGESTION

1. init on both architectures (aarch64/paging.rs:702, x86_64/paging.rs:1100): split only the 2 MiB pages whose Image::prot differs across the page. The boot stack and any data or rodata page wholly inside one protection could stay a single block. That would cut the unmeasured 4 KiB TLB cost the PR lists as a risk, and it makes B1(a) cheap.
2. Duplicated refusal (loader/src/main.rs:298-310, kernel/src/mm/image.rs:27-35). One toyos_elf::Layout method, such as "the one non-writable executable segment's page range, or why not", would give the loader and the kernel a single definition. If toyos-elf is truly off limits because of the sysroot, leave it as is. That reason is the implementer's claim, and I did not verify it.
3. aarch64/paging.rs:829-833 (test-only): stage_writable_executable treats any entry that is not a block as a table. An invalid L2 entry would then dereference Table::at_mut(0) before the leaf assert, contrary to its SAFETY comment. Assert VALID | TABLE in that branch. The x86 twin (x86_64/paging.rs:1159) refuses a frame under a split 2 MiB page, which guard_4k or the image can produce. That is deterministic in QEMU today, but handling the 4 KiB case as the AArch64 version does would stop the control depending on where the PMM's next frame lands.
4. issues/x86-64s-boot-map-is-writable-and-executable.md: add it to the parity list in the-kernel-is-at-least-as-secure-as-linux-on-every-machine-toyos-supports.md next to the RELRO entry. It is the remaining kernel W^X gap on x86-64.
5. For the orchestrator, not the branch. UCI/UCT are deferred with reason: they serve EL0 JIT, which is a later stage. They are recorded only in the PR body and in the design's §4 JIT bullet, so move them from the stage-0 row to the JIT stage in the design so they are not lost. Also, the PR body's claim that the trampoline's EFER write keeps no-ap-control-regs reaching the self-check is an inference: no registered test exercises that actuator.

Evidence

• The host CI log ends with 87 step(s), all green and exit 0.
• The guest log shows 8 of 8 passing, at the head, including both negative controls.
• The probe and the mutations ran on the pre-commit tree. The stated delta (comment reflow, issue text, clippy test fix) cannot change their outcome, so reusing them is sound.
• Metal (posted on the PR): T14 12529 leaves and AMD 12390 leaves, both passing. That covers x86-64's early-boot changes on real firmware: the RO boot-map text, NXE before mm::init, and the trampoline's EFER.
• AArch64 has QEMU evidence only. That limits B1, which is why it has to be settled by the Arm ARM or by construction, not by a test.

SEND BACK

[Japabu]

Response to review r1. The new head is aa2295250; evidence is at https://github.com/ToyOSOrg/evidence/blob/6afdea6bb08e80ef6409cdee413b7ca729d58f99/r2/README.md

B1 (AArch64 join): fixed by option (b), a real break-before-make.

• join now branches to the image's identity alias under the old TTBR0, swaps TTBR1 to an empty root, runs TLBI VMALLE1, installs the kernel's root, and branches back to the link address. Only then does it switch TTBR0, whose new root maps nothing, so that switch only removes translations. Interrupts stay masked throughout.
• The doc comment and the SAFETY comment now state that argument, citing D8.17.1.
• (a) alone would not have been enough. Even with the mixed-only split, a 2 MiB page holding rodata and data is split in the kernel's tables but stays a block in the loader's, because the loader splits only around the text. The loader also splits scanout pages differently.
• QEMU runs the new sequence on virt at EL1 and at EL2 (BSP and 8-CPU SMP). It cannot show a TLB conflict.

B2 (x86-64 kernel_leaf doc): fixed. The doc now covers both leaf sizes and the PAT-bit caveat. kernel_page is gone, inlined at its one caller.

Suggestions:

• S1, split only mixed pages: taken, on both architectures (mm::Image::block). Leaf counts fall from 6647 to 4092 on q35 and from 5739 to 3184 on virt. The x86-64 mappings changed, so both benches are restaged.
• S2, one shared definition: declined. lib/elf/src is in build/sysroot.rs' SYSROOT_SOURCES (checked), so changing toyos-elf changes the sysroot's identity.
• S3, staging helpers: taken. Both refuse an absent entry, and x86-64 now also handles a leaf under a split 2 MiB page.
• S4, parity list: taken. The x86-64 boot-map issue is now listed.
• no-ap-control-regs: run, not dropped. A temporary probe showed the undeclared AP holding the trampoline's efer=0x0d01, walking the NX tables, and being stopped by the self-check's CR0 assert.

Host CI is green, both builds pass, 8 of 8 guest tests pass, and the data-executable mutation reds 4 of 4 again.

Please review the fixes; the earlier findings stay settled.

[Japabu]

Metal, head aa2295250, run by the orchestrator, shared testcases boot:

• T14: rc 0, kernel_wx PASS. paging: 9974 kernel leaves, none writable and executable, none executable outside the text
• AMD: rc 0, kernel_wx PASS. paging: 9835 kernel leaves, none writable and executable, none executable outside the text

The mixed-only split cut leaves from 12529 to 9974 (T14) and from 12390 to 9835 (AMD).

[Japabu]

Review r2 — PR #984 at aa2295250

Scope: only the fixup commit b7a7b5827..aa2295250 (4 files, +82/−30), checked against my r1 findings. Earlier findings stay settled.

B1 — AArch64 join (kernel/src/arch/aarch64/paging.rs:740-800): resolved

I checked the sequence step by step against D8.17.1 (p. D8-7858/7859):

1. mrs daif / msr daifset, #0xf: IRQ, FIQ, SError and debug are masked, so no exception is taken through VBAR_EL1 at PHYS_OFFSET while TTBR1 is empty. The saved DAIF is restored at the end. daif and at are out operands, so they never share a register with an input.
2. dsb ishst comes first. That covers BBM step 6 for the kernel's tables, which init wrote before join.
3. adr / sub PHYS_OFFSET / br: the image runs at PHYS_OFFSET plus its physical address, so this lands on the identity alias.
   • BSP: the old TTBR0_EL1 is the loader's map. Its identity view gives the text Access::Text, which is executable because access is decided by physical address in both views.
   • AP: the old TTBR0_EL1 is bringup_root, whose low slots copy the kernel's own L0 entries, so the text is RX there as well.
   • TTBR0 does not change during the TTBR1 swap, so the identity translations that are fetched stay consistent.
4. msr ttbr1_el1, empty then isb is BBM step 1 (the break). The ISB ensures that no later walk, speculative or not, uses the old root.
   • empty is the kernel space's TTBR0 root address with the ASID removed. It is a permanently empty table.
   • With TCR.A1 = 0, TTBR1's ASID field plays no part.
5. tlbi vmalle1 / dsb nsh / isb is steps 3–4. Local scope is enough: the change is to this PE's TTBR, not to a table entry another PE walks. Other PEs' TLBs never cached this PE's old root.
6. msr ttbr1_el1, kernel root / isb, then br back to the link address. This is step 5: no old global TTBR1 entry can survive here.
7. msr ttbr0_el1, empty / isb / tlbi vmalle1 / dsb nsh / isb. The new TTBR0 translates nothing, so the old global identity entries are only stale-and-removed, never in conflict with a different valid entry. That is the "invalid entry first" half of BBM again.

The asm block uses no stack (nostack). It also omits nomem, so it remains a compiler barrier. The rewritten doc and SAFETY comments state exactly this argument and cite D8.17.1, and that heading is correct in the PDF extract. Both callers (paging::init on the BSP and smp::ap_entry) reach join with the old TTBR0 described above. check_joined still checks the end state.

The remaining risk is that no test can show a TLB conflict: QEMU does not model one, and there is no AArch64 bench. That is now argued from the specification rather than assumed, which is the right basis.

B2 — x86-64 kernel_leaf doc: resolved

The doc now covers both leaf sizes, and states the PAT-bit caveat where it applies (Normal sets neither bit). kernel_page is inlined at its single caller.

S1 — mixed-only split (mm::Image::block): no assumption broken

• block treats pages outside the image as ReadWrite. So a block is ReadExec only when all 512 of its pages are text, which keeps it inside the page-rounded text range that executable_outside_text checks. A Read or ReadWrite block is never executable. The audit therefore stays exact.
• AArch64: Coverage::Whole with a uniform block uses memory(at), which is the same Prot as block's. Mixed pages and Coverage::Pages still go page by page. The split at :604 copies a block's attributes whole.
• x86-64: map_2m receives the block's Prot.
  • guard_4k copies the flags of whatever 2 MiB leaf it splits, so a guard inside an image block keeps that block's protection.
  • translate_in_current_tables and policy_at handle both leaf sizes.
  • map_mmio's overwrite allowance applies only to Normal RAM leaves, and the image is never MMIO.
• overlaps is now private. Its only remaining user is prot, and nothing else depended on the old "the image's 2 MiB pages are always split" behaviour.
• Leaf counts dropped from 6647 to 4092 on q35 and from 5739 to 3184 on virt, which matches keeping the 8 MiB stack and the uniform data in blocks.

S3 / S4 and no-ap-control-regs

• S3: both staging helpers now assert presence. x86-64 also handles a leaf under a split 2 MiB page, and invalidates the 4 KiB address in that case.
• S4: the parity-list entry has been added.
• no-ap-control-regs: the implementer reports a reverted probe showing an undeclared AP holding the trampoline's efer=0x0d01 and stopped by the CR0 assert. I accept this as evidence; it is not a registered test, and it does not need to be one for this PR.

Evidence at aa2295250

• r2-ci-host.log: 87 step(s), all green, exit 0.
• r2-qemu.log: 8 of 8 PASS. That includes virt_smp, virt_el1_smp and virt_el2_drop, so the new join ran on the BSP and the APs, at both EL1 and EL2. Both negative controls name exactly the staged leaf.
• r2-mutation-data-executable.log: it fails as intended (exit 1).
• Metal at this head is being rerun on both benches, because the x86-64 mappings changed. The orchestrator should attach those results before landing.

No new findings.

LAND