[Improvement] partial def functions in IR interpreter block formal verification of Layer 2-3

[Th0rgal]

Summary

The IR and Yul interpreters use 16 partial def declarations which prevent Lean from proving termination. This is the root cause of axioms #1 and #2 (evalIRExpr_eq_evalYulExpr and evalIRExprs_eq_evalYulExprs).

Affected Functions

All in Compiler/Proofs/IRGeneration/IRInterpreter.lean:

• partial def evalIRExprs (line 79)
• partial def evalIRCall (line 85)
• partial def evalIRExpr (line 141)
• partial def execIRStmt (line 163)
• partial def execIRStmts (line 238)

And in Compiler/Yul/PrettyPrint.lean:

• partial def toHex (line 13)
• partial def ppExpr (line 28)
• partial def ppStmt (line 37)
• partial def render (line 100)

And in Compiler/ContractSpec.lean:

• partial def compileExprList (line 146)
• partial def compileExpr (line 149)

And in Compiler/Linker.lean:

• partial def extractFunction (line 50)
• partial def extractAllFunctions (line 72)
• partial def collectExternalCalls (line 149)

And in Compiler/RandomGen.lean:

• partial def genTransactions (line 169)

Impact

The two expression evaluation axioms (AXIOMS.md #1 and #2) exist only because evalIRExpr and evalYulExpr are partial. If these were refactored to use fuel-based evaluation (e.g., Nat parameter as recursion bound), the axioms could be eliminated entirely.

AXIOMS.md already acknowledges this:

To eliminate this axiom, we would need to:

• Refactor both eval functions to use fuel parameters (like execIRStmtFuel)
• Prove termination for all expression types
• Effort: ~500+ lines of refactoring

Priority

The interpreter functions (evalIRExpr, evalIRExprs, evalIRCall, execIRStmt, execIRStmts) are the critical ones since they carry axiom debt. The pretty-printer, linker, and random-gen partial functions are non-critical since they don't affect verification.

Recommendation

Refactor the 5 IR interpreter functions to use fuel-based recursion. This would:

1. Eliminate 2 of 5 axioms (reducing to 3)
2. Make Layer 3 verification fully axiom-free for expression evaluation
3. Improve the trust model significantly

This is the single highest-impact trust reduction possible with moderate effort.