[Submitted on 11 Aug 2026 (this version), latest revision 11 Aug 2026 (v2)]
Title:Goal-Shape Tactic Retrieval for Exact WebAssembly Artifact Proofs
Abstract: A coding agent constructing a direct Lean proof about WebAssembly needs to find proof support from the semantic shape of a residual goal. LeanExe extends its structured catalog of lemmas, tactics, and guidance with checked tactic records that name a command, its defining module, applicable goal shape, required premises, compiler-annotation kinds, and a fallback theorem. The reported catalog contains 24 entries, 79 unique declaration names, and five indexed tactics drawn from 27 commands in the supplied proof kit. A controlled proof task held the specification, source, WebAssembly binary, decoded program, and artifact digest fixed. The agent selected and used tactics for bounded array-length dispatch and block-wrapped loop induction, rejected three tactics whose recorded shapes did not match later goals, and used neither fallback theorem. An independent outer Lean check rejected the candidate at a later continuation-frame proof, while Lean accepted a focused manual repair of the complete exact-artifact proof. The result establishes selective tactic retrieval and shows how the retained journal and outer check expose missing general guidance. The experiment supplies no accepted autonomous proof or proof-generation-time improvement.
| Subjects: | Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI) |
| Cite as: | marXiv:2608.00036 [cs.LO] (or marXiv:2608.00036v1 [cs.LO] for this version) |
Submission history
[v1] Tue, 11 Aug 2026 17:38:09 UTC (153 KB)
[v2] Tue, 11 Aug 2026 17:52:55 UTC (149 KB)
Related work
- marXiv:2608.00034
- evaluates tactic retrieval alongside the compiler-generated fold interfaces reported there