[v0.5] #91 H7: the runtime's walks as kernel-checked theorems (H7-0, H7a, H7b, H7c) #306

Child of #91, moved out of v0.4 by the maintainer's ruling (#91, comment 6377638488): H7-0, H7a, H7b and H7c are not v0.4. The DoD line "every runtime item has its refinement statement kernel-checked" is about runtime::Item, and SP-30 closes it; the walks are the machine beneath the boundary stage 1 fixed (machine primitives with a stated meaning, the transcript of RB-20, the model theorems of SP-27/SP-28). A walk theorem is at SP-25 scale (minutes and gigabytes each, about 35 of them), so the work goes to release/v0.5, with List::length measured on the SP-22 protocol as the first comment on this issue.

No H7 code lands in v0.4. The last v0.4 PR of #91 is the H7-audit (#305).

Parts

• H7-0: the heap evaluator over SP-27's world (RuntimeHeap) on a store-free program agrees with RuntimeSemantics (or H7c restates SP-25's two theorems against it).
• H7a: the closed list of std calls with a stated meaning, the abstraction and tick theorems of the list, byte and text walks, and the Lean half of the shared-write plant.
• H7b: the remaining walks stated against the list.
• H7c: Drop for Node against releaseLoop, and SP-25's theorems against the one semantics.

The six decisions (binding; verbatim from the maintainer)

1. The heap evaluator over SP-27's world (RuntimeHeap) is the route, not the RustSyntax re-authoring: the runtime is authored in RuntimeSyntax, so its semantics is what must cover its constructs, and the spike's cost and the stuck blt decide the rest. One condition: one meaning per syntax at the end. H7-0 proves that RuntimeHeap on a store-free program agrees with RuntimeSemantics, or H7c restates SP-25's two theorems against it. Two semantics that may disagree is a blur.
2. Yes, the closed list of std calls with a stated meaning is the boundary, as the machine primitives were in stage 1, with four conditions: the list is data in the Lean module, not a Rust table; a gate holds the validator's call-name table and the list in bijection, as SP-30 holds items and statements; every meaning is one line naming a calculus primitive or an SP-27/SP-28 operation; no meaning says more than the standard library documents (Rc::get_mut is aloneOn, nothing more).
3. Ticks are stated against the counts the transcript checks, as a closed form of the abstract input in each statement (your shape, ticks + length (absHandle w.store h)), and RB-20 checks the same closed form on the values. Not against TargetSemantics' step count: runMachine discards it by design, and binding it is a claim about the calculus's cost model, which neither [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 nor H7 moves.
4. Yes, both levels: the validator half in v0.4 (above), the Lean half (the meaning of Rc::get_mut planted as always unique, and cons without its truncate(len)) in H7a, each with its red line.
5. Drop for Node is a theorem against releaseLoop in H7c. "Iterative release does not overflow" is a statement the issue names; a statement is not downgraded to evidence by its cost. If the budget refuses it, the theorem is split.
6. Yes, as proposed, in the v0.4 audit PR above.

Budget

One bdd part per PR, 30 minutes at most, peak at most 4 GB on the SP-22 protocol; List::length first, and more than five times an SP-27 theorem re-decides the route before the rest.

Context: #91 (stage 4 heap half: #298, #304, #305).