Set up Kani and add proof harnesses for memory/paging

[chbaker0]

Filed by an AI coding agent (Claude Code).

Sets up Kani over shared, adds 76
proof harnesses concentrated on memory / memory::paging / memory::alloc,
and fixes the four defects they turned up.

Why Kani here

cargo stest samples inputs and cargo smiri watches one concrete execution
for UB. Neither says anything about the rest of the input domain, which is
exactly where the paging and bitmap-allocator code is interesting: a page-table
walk that is right for the addresses a test happens to pick and wrong for one
index quadruple is invisible to both. Kani proves a property over every input in
a symbolic domain, or hands back a concrete counterexample.

Kani and Miri turn out to be complements on paging.rs specifically: Miri drives
PhysTableStore's real read_volatile/write_volatile walks and checks them for
UB; Kani drives the same Mapper::map traversal through a pointer-free
array-backed store and proves it computes the right answer for every page.
Neither subsumes the other.

Defects found and fixed

Full write-ups, counterexamples and reachability analysis in
docs/kani-findings.md. In short:

1. align_u64_up overflowed near the top of the address space, reached via
   Extent::shrink_to_alignment. Panics with overflow checks on; wraps with
   them off, which would have iter_map_frames hand the allocator frames near
   address 0 that have nothing to do with its input. Added
   align_u64_up_checked / Address::align_up_checked; shrink_to_alignment
   propagates None, which is the correct answer.
2. next_level could clear PRESENT and detach a live subtree while map
   carried on writing into it and returned Ok(()) — a mapping that silently
   does not exist, plus a leaked table on the next map through that slot. The
   allocate branch already forced PRESENT; only the reuse branch didn't. Fixed
   and documented on both next_level and Mapper::map.
3. fill_bitmap_from_map mis-marked small regions, two ways: a subtraction
   underflow for any region ending below frame 8, and — the dangerous one — a
   region confined to a single bitmap byte marked the whole byte free. The
   leading and trailing partial-byte phases each widened to a byte boundary and
   ORed together. BitmapFrameAllocator::new's unsafe contract is "all frames
   marked free must be available and not used by other code", so those extra bits
   are firmware memory, kernel image, or MMIO handed out as ordinary RAM. Both
   are reachable at boot — we just haven't seen a UEFI map that produces such a
   region. Replaced the three-phase split with a uniform per-byte loop that clips
   the range to each byte it touches; the uniform form cannot express either bug.
4. Map::iter_type filtered self.entries, the whole 128-slot backing array,
   instead of self.entries(), the num_entries prefix — returning up to 128
   phantom Reserved extents at address 0.

Nice detail on (4): that bug was also the tractability blocker. The end-to-end
fill_bitmap harness had to unwind two 128-iteration loops and wouldn't settle
in ten minutes; with the fix it verifies in 5 seconds. A representation bug and a
verification-performance problem turned out to be the same bug.

Known-failing harnesses

Five harnesses fail on purpose and are marked KNOWN FAILURE in their doc
comments, catalogued under "Open" in the findings doc. They pin two real,
unfixed defects in alloc::phys — left out of this PR to keep it to the
verification work plus the fixes that were needed to make the harnesses pass:

• find_bit_group's mask is (len << 1) - 1 — that's 2·len − 1, not
  2^len − 1. Coincides for len 1 and 2, diverges at 4. The existing unit
  tests pass by accident: every len == 4 byte they try happens to have its
  fourth bit agree with the other three. The consequence is a physical frame
  handed out twice:

  allocate_range(2) on 0b0111_0111 -> frames 0..=3, bitmap now 0b0111_0000
          frame 3 was *** ALREADY ALLOCATED ***
  

  That breaks FrameAllocator's documented unsafe invariant, which every
  SAFETY comment in mm.rs about "frames not in use anywhere else" rests on.
  Not hit today only because allocate() uses order 0; HeapProvider derives
  its order from a chunk count, so a 4-chunk heap request reaches it.

• allocate_range panics instead of reporting exhaustion. The size >= 8
  path returns None only from inside the loop; when the bitmap length divides
  evenly by the chunk length that early return never fires and control reaches
  unreachable!(). So the ordinary "no run of 8 free frames available" outcome
  the Option exists to express panics the kernel.

Both fixes are one-liners ((1usize << len) - 1; None after the loop) and the
harnesses that prove them are already written and fast — happy to fold them in
here or do them separately, whichever you prefer for review.

A third open item, Extent::from_range_exclusive bypassing new_checked's
non-empty invariant, is left alone deliberately: it's an API-semantics decision
(returning Option would change const call sites in mm::VirtualMap), not a
mechanical fix.

How the harnesses are written

Documented in docs/verification.md; three conventions:

• Prove against a specification, not the implementation. Single-extent ops
  use a universally-quantified probe address — contains_addr(result, p) == spec(p) is extensional set equality. Two-extent ops name their answer's
  endpoints directly (overlap = [max(starts), min(lasts)]), which is
  equivalent for intervals but far cheaper than a third symbolic u64.
  Mapper::map gets an independent translate oracle that walks tables the way
  hardware does and shares no code with Mapper.
• An assume is a precondition, written down. Where a harness narrows its
  domain, that narrowing is the contract; if it isn't in the doc comment, the
  harness says so. This is how (1) surfaced.
• #[kani::should_panic] pins the other side of a contract — num_pages at
  zero, set_addr at 2^52, deallocate on a double free.

Harnesses sit in a #[cfg(kani)] mod verify block at the bottom of each module,
same placement and style as mod tests. Being a child of the module under proof
is what lets them reach private items — TableStore, align_u64_down,
find_bit_group, PageTableEntry::raw, BlockAdapter — where most of the
interesting invariants actually live.

Not done here

• No CI job. The full suite has never completed in one run; several paging
  harnesses take 2-3 minutes each, and five currently fail by design. Wiring up
  model-checking/kani-github-action wants a decision about which subset to gate
  on and probably wants the two alloc::phys fixes landed first.
• One harness, two_mappings_do_not_interfere, is held out of the suite —
  its #[kani::proof] attribute is deliberately absent. It has never produced
  an explained verdict: FAILURE in ~30s with a placeholder message once, then no
  verdict at all after ~50 minutes on a later run of the same code. Suspicion is
  an unwinding-assertion artifact on ArrayStore<6>'s array initializer rather
  than a real counterexample, but that is untested, and the nearly identical
  map_leaves_every_other_page_unmapped (ArrayStore<3>, same unwind bound)
  passes. The body still compiles so it doesn't rot. Worth knowing: Kani does
  not honour #[ignore], and 0.67 has no --exclude-harness, so dropping the
  proof attribute is the only mechanism available.

Test plan

• cargo stest — 56 passed (3 new unit tests in alloc::phys covering the
  region shapes that defect 3 got wrong).
• cargo kcheck / lcheck / icheck — clean, no warnings.
• cargo kani -p shared --only-codegen — all harnesses compile; cargo kani list
  reports 76.
• Individual harnesses run and pass, including
  map_then_translate_round_trips_for_any_page_and_frame (127s, all pages ×
  all frames), remap_replaces_the_leaf_entirely (181s),
  map_2m/map_1g_translates_across_the_whole_huge_page,
  mark_frames_free_marks_exactly_its_frames (3s),
  fill_bitmap_marks_exactly_the_available_frames (5s).
• No QEMU boot yet — the fixes are in shared, and CI's smoke job covers it.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: d2ab6bda89

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".