fix(#742,#743): single-source the mmap floor, close MAP_FIXED gap, repair teardown census

[ryanbreen]

Summary

• mmap validator's lower bound (MMAP_REGION_START) is not the allocators' floor, and MAP_FIXED bypasses all region checks #742: the mmap validator's lower bound (MMAP_REGION_START) was never the allocators' own floor. sys_mmap and five graphics.rs producers each hardcoded 0x1000_0000 instead, ~17.6 TB below the validator's real floor — the same "validator anchored to a bound the allocator does not use" shape as x86: sys_spawn's copy_string_from_user validator misses heap addresses (spawn may EFAULT from a shell) #729's B4-a, just not yet live. All six call sites now floor against crate::memory::vma::MMAP_REGION_START directly (the single source of truth is the constant; redefining it down to the old hardcoded floor would violate the existing USERSPACE_CODE_DATA_END <= MMAP_REGION_START layout invariant, so the producers move to match the constant, not the reverse).
• mmap validator's lower bound (MMAP_REGION_START) is not the allocators' floor, and MAP_FIXED bypasses all region checks #742 M-2: sys_mmap's MAP_FIXED arm accepted any page-aligned address with no region check at all. It now requires the mapping to land wholly inside [MMAP_REGION_START, MMAP_REGION_END), the same window the validator polices. (Deliberately more conservative than Linux here — it also refuses addresses is_valid_user_range would otherwise accept as code/data/stack, since there are zero in-tree MAP_FIXED callers today to need that.)
• layout.rs gains two new load-bearing const-asserts (mmap-region tightness + non-emptiness), both mutation-verified to redden, on both arches.
• tests/mmap_floor_structure.rs (new): a structural ratchet census-pinning the six < MMAP_REGION_START producer comparisons mmap validator's lower bound (MMAP_REGION_START) is not the allocators' floor, and MAP_FIXED bypasses all region checks #742 fixed and the five mmap_hint seed sites that read MMAP_REGION_END, by (file, enclosing function, occurrence count) — never a literal line/file list. Closes a false-universal doc comment this branch's first commit left in layout.rs (review round B2: "there is nowhere left for either bound … to drift apart again" replaced with an accurate, scoped description of what the ratchet does and does not prove). Mutation-proven against the real tree (a temporarily re-literalized graphics.rs floor site reddens it with an exact diagnostic, then reverts clean) as well as against six synthetic-source mutations, two of them negative controls.
• teardown_structure ratchet red: driver_h.rs's corroborating_nonprogress_bit placeholder missing from thread-state census (PR #740 census drift, distinct from #734) #743: driver_h.rs's corroborating_nonprogress_bit() (landed by PR proof(core): rung 3 - dispatch admission torture harness (component H) + rung-2 review leftovers #740) seeds a scratch StrandCandidate buffer with a placeholder ThreadState::Running, the same non-progressing fill-value shape two existing rows already cover — just a construction site the thread-state census's allow-list never got updated for. Registered the row; tests/teardown_structure.rs is back to 81/81 (was 79 passed, 2 failed).
• Both arches: concurrent ext2 read-park vs write-spin is a livelock shape (root & home filesystems) #728: the durable GitHub record (issue title/body + the pinned analysis comment) is corrected to the disposition this branch's diff does not itself change: latent-live on both arches and both filesystems (ROOT_EXT2/HOME_EXT2), not the "verified NOT-LIVE on aarch64" this section originally claimed. The original aarch64 scoping rested on three claims a review round falsified against the kernel's own source (a spinning writer occupying more than one CPU once other threads must also spin to acquire ROOT_EXT2/HOME_EXT2; ordinary readers spinning, not parking, once WRITER/UPGRADED is set; and aarch64's own stock boot workload already supplying most of the concurrency the livelock needs). See the corrected issue and its pinned comment for the full mechanism. A live, observed reproduction of the corrected shape — an unattributed docker/qemu/run-boot-parallel.sh 1 stall at sys_mkdir("/var") with several concurrent ext2 readers in flight — is preserved in-repo at docs/planning/green-program/nic-bus/serials/728-live-repro/ and posted to the issue as a repro path for whoever picks up the actual fix. No lock-discipline fix is attempted by this PR; Both arches: concurrent ext2 read-park vs write-spin is a livelock shape (root & home filesystems) #728's own "Suggested directions" section remains the pointer to that arc.

Test plan

• x86_64 release build (--target x86_64-breenix.json -Z build-std=core,alloc, --bin kernel): zero warnings/errors
• aarch64 release build (--target aarch64-breenix-kernel.json -Z build-std=core,alloc, --bin kernel-aarch64): zero warnings/errors
• cargo test --release --test teardown_structure: 81/81 passed
• cargo test --release --test mmap_floor_structure: 9/9 passed (new ratchet — the branch's newest load-bearing verification artifact)
• All other host structure-test suites (*_structure.rs, percpu_stack_custody, stack_bounds_tests, kernel_no_neon_guard, x86_gate_verdict_test, repo_symlink_hygiene): all green, 0 failures
• aarch64 boot-tests-only strict gate (run-aarch64-boot-test-strict.sh, 20 iterations): 20/20 SUCCESS
• Both new layout.rs const-asserts mutation-proved to redden on the regression they exist to catch, per-arch — including the review-round finding (C1) that the mmap non-empty assert's isolating mutation is arch-specific (no single constant pair isolates it on both x86_64 and aarch64); both arch-specific pairs verified by an actual cargo check against each target, not modeled

🤖 Generated with Claude Code