Repository navigation
WordRAM: symbolic execution of straight-line structured code (proof automation) #2182
Description
Opened by coordinator-claude-015dlg8k (Claude Code, Opus), working on tech debt for Samuel.
Problem
WordRAM correctness proofs are hand-stepped. On main at 73d32b3c0, scripts/proof_lengths.py counts 81,731 proof-body lines under WordRAM paths, 19% of the library's 431,039. 554 of those proofs are 40 lines or longer, totalling 52,173 lines. The ten longest proofs in the library are all of this kind: FibonacciHeap/Cut.lean decreaseKeyCode_exec (849 lines), Consolidate.lean scatterBody_exec (791) and extractMinCode_exec (722), Cut.lean cutNodeCode_raw (698), plus Karger contractLoop_spec (379), van Emde Boas successor_some_spec (356) and others.
A typical proof does three things per instruction:
- It states the next intermediate
Databy hand, e.g.let x2 := (x1.set s0 …).set s1 …. - It proves one
ExecWithinstep withsimpa only [reg facts] using ExecWithin.store …. - It re-derives register and memory reads through
simp only [Data.set_regs, Function.update_of_ne (by decide : r ≠ s0), …].
Invariants such as FibonacciHeap.BaseRegs, a 13-conjunct Prop, are read positionally (hbr.2.2.2.2.2.2.2.2.2.2.2.1). Structured.lean already offers forward rules and an interpreter (Code.eval, Exec.of_eval), but only three files in Algorithms/DataStructure use of_eval.
Definition of done
- Automation. A tactic or simp set that symbolically executes loop-free structured code with symbolic register contents, producing the final
Dataand the instruction count.Fitsand address side goals are discharged by a configurable discharger, or left as named goals. Register and memory reads afterset/writereduce automatically when register names are literals. - Tests. The automation has tests on concrete programs, including a failure case with a readable error.
- Pilot. One heavy module (FibonacciHeap) is migrated, with every public statement unchanged.
BaseRegs-style conjunctions become structures with named fields. The PR reports the measured line reduction. - Guide. A short note in the WordRAM docs tells authors to use it.
Loops stay on the existing loop_invariant/loop_potential rules. This issue covers only the straight-line glue between them.
Activity
SamuelSchlesinger commentedon Nov 1, 2026
Claimed by
worker-claude-015dlg8k-wrexec(Claude Code, Opus), worker ofcoordinator-claude-015dlg8k. Branchclaude/wordram-exec-2182. Plan: investigate why the long proofs avoidCode.eval, then an infrastructure+tests PR, then a stacked FibonacciHeap pilot PR (Cut.leanfirst).SamuelSchlesinger commentedon Nov 1, 2026
worker-claude-015dlg8k-wrexec(Claude Code, Opus): two PRs are up.Code.eval/ram_evalwas not enough here. The interpreter is monolithic, so it cannot use specifications of subprograms or loops. Reads after writes to symbolic addresses stay as unresolvedifs, everyFits/branch fact must be stated beforehand in simp-normal form, and branches on symbolic data cannot be split. feat(WordRAM): symbolic execution of straight-line structured code #2193 therefore addsWP, the weakest-precondition form ofExecWithin, with one backward rule per construct, and the tacticwram_exec, which walks the program with these rules and stops at loops and named subprograms. The helpers arewram_simp,wram_bounded,WP.cut,WP.nameandWP.bounded.BaseRegsbecomes a structure with named fields, andCut.lean's four execution proofs are migrated, going from 1,792 to 923 body lines (Cut.leantotal 2,115 → 1,246;decreaseKeyCode_exec849 → 565,cutNodeCode_raw698 → 317). The costs are slower elaboration (about 10 s → 19 s forCut.lean) and onemaxRecDepth 1024ondecreaseKeyCode_exec.Still open:
Consolidate.leanandBasicOps.lean, andMinPQ's positionalAllocRepreads.SamuelSchlesinger commentedon Nov 1, 2026
coordinator-claude-015dlg8k(Claude Code): direction update. Samuel has chosen the oracle-refinement design in #2205 for WordRAM.wram_exec(#2193) stays as its bottom layer, for verifying primitive memory operations and the realization kernel, andworker-claude-015dlg8k-wrexec2is finishing its performance pass. #2195 (Cut.leanpilot) can land as an interim improvement. Further code-level migrations of large proofs (Consolidate,BasicOps, Karger, cuckoo) are paused: they will be redone through #2205's hops instead.feat(WordRAM): symbolic execution of straight-line structured code (w…
refactor(FibonacciHeap): name BaseRegs fields and migrate Cut.lean to…