Title:Compiler-Generated Frame Accessors in Exact WebAssembly Proofs

Abstract: Direct proofs about decoded WebAssembly must establish how compiler-created local frames encode mathematical loop state. LeanExe now emits Lean theorems for the parameter list, local-list length, operand stack, and every index in the parameter-plus-local sequence of each recognized array-fold continuation frame. It places these declarations and two shared theorems for reading locals after result placement in a structured library retrieved by a coding agent. A manual substitution within a proof of the same binary removed ten proof-local projection declarations and reduced proof source from 588 to 555 lines. Three separate ephemeral coding-agent sessions then proved the behavior of frozen WebAssembly binaries for bounded addition, multiplication, and bitwise-XOR folds, and a separate verifier accepted all three. The direct artifact-proof stages took 2231, 2099, and 2452 seconds. The addition and multiplication runs were slower than their same-binary predecessors, while the held-out XOR run was slower than both earlier runs using the accessors. The results establish a checked compiler-to-proof interface across three accumulator operations but supply no evidence of lower proof-generation time. The agents' journals identify proof obligations that connect loop completion to the public postcondition and prove equality between WebAssembly local frames.

Submission history

[v1] Tue, 11 Aug 2026 03:52:59 UTC (117 KB)

[v2] Tue, 11 Aug 2026 04:06:19 UTC (119 KB)

[v3] Tue, 11 Aug 2026 04:13:24 UTC (120 KB)

[v4] Tue, 11 Aug 2026 04:22:02 UTC (119 KB)

[v5] Tue, 11 Aug 2026 05:08:16 UTC (119 KB)

Named by

marXiv:2608.00036

evaluates tactic retrieval alongside the compiler-generated fold interfaces reported there (Goal-Shape Tactic Retrieval for Exact WebAssembly Artifact Proofs)

Full text and citation

View PDF · Export BibTeX citation