fix: Discharge hbody hypothesis via fuel adequacy axiom (closes #159)

[Th0rgal]

Summary

• Add ir_function_body_equiv theorem that fully instantiates the proof chain from all_stmts_equiv through fuel adequacy to function-level IR↔Yul equivalence
• Add execIRStmtsFuel_adequate axiom to bridge the partial IR evaluator with the fuel-parametric version used in proofs
• The Layer 3 preservation theorem's hbody hypothesis is now dischargeable for any contract
• Axiom count increases from 4→5 (all 3 new IR axioms are eliminable by a single ~500 LOC refactor)

Details

Issue: #159 — Layer 3 preservation theorem has undischarged hbody hypothesis

Problem: yulCodegen_preserves_semantics required hbody : ∀ fn, fn ∈ contract.functions → resultsMatch (execIRFunction fn ...) (interpretYulBody fn ...) but no theorem supplied this proof. The existing statement-level equivalence proofs (all_stmts_equiv) couldn't bridge to hbody because of two gaps:

1. execIRFunction uses partial execIRStmts, while proofs use fuel-parametric execIRStmtsFuel
2. No adequacy proof connected these two execution modes

Fix: Add execIRStmtsFuel_adequate axiom (standard fuel adequacy pattern) and compose it with the proven statement equivalence chain to produce ir_function_body_equiv.

Proof chain:

all_stmts_equiv (proven, 8 statement types)
    ↓
execIRStmtsFuel_equiv_execYulStmtsFuel_of_stmt_equiv (proven, list composition)
    ↓
ir_yul_function_equiv_fuel_goal_of_stmt_equiv (proven, function-level fuel equiv)
    ↓
execIRStmtsFuel_adequate (NEW AXIOM, bridges partial ↔ fuel)
    ↓
ir_function_body_equiv (NEW THEOREM, fully instantiated)

Files changed:

File	Change
Equivalence.lean	Add execIRStmtsFuel_adequate axiom + execIRFunctionFuel_adequate theorem
Preservation.lean	Add ir_function_body_equiv theorem, import StatementEquivalence
AXIOMS.md	Document new axiom #3, renumber #3→#4, #4→#5
README.md, TRUST_ASSUMPTIONS.md, compiler.mdx, verification.mdx, llms.txt	Update axiom count 4→5

Test plan

• Lean build passes (76/76 modules, no new sorry)
• check_doc_counts.py passes (5 axioms)
• check_axiom_locations.py passes (all 5 axiom locations correct)
• Full CI green

🤖 Generated with Claude Code

---

Note

Medium Risk
Introduces a new axiom bridging partial and fuel-based IR execution; while localized to proofs/docs, it expands the trusted base for core compiler-correctness results.

Overview
Discharges Layer 3 yulCodegen_preserves_semantics’s previously external hbody assumption by introducing a fuel-adequacy bridge from total execIRStmtsFuel to partial execIRStmts, and composing it with existing statement equivalence to produce a self-contained ir_function_body_equiv theorem.

Adds a new axiom execIRStmtsFuel_adequate (plus execIRFunctionFuel_adequate) and updates axiom/trust-model documentation across AXIOMS.md, README.md, TRUST_ASSUMPTIONS.md, and docs to reflect the axiom count increase from 4→5.

^{Written by Cursor Bugbot for commit 9bac89a. This will update automatically on new commits. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
dumbcontracts	Ready	Preview, Comment	Feb 16, 2026 8:00am