[Bug] Axiom justification in StatementEquivalence.lean is misleading — only IR eval is partial, not Yul

[Th0rgal]

Summary

The axiom documentation for evalIRExpr_eq_evalYulExpr (AXIOMS.md and inline comments) claims that both evalIRExpr and evalYulExpr are partial functions, which is why an axiom is needed. However, only the IR side appears to use partial def.

AXIOMS.md Claim

Why Axiom?:

• Both evalIRExpr and evalYulExpr are defined as partial functions (not provably terminating in Lean)
• Lean cannot prove equality between partial functions
• Functions have identical source code structure but different state type parameters

Actual Code

IR side (Compiler/Proofs/IRGeneration/IRInterpreter.lean):

partial def evalIRExpr (state : IRState) : YulExpr → Option Nat  -- ✅ partial

Yul side — the Yul evaluator in Compiler/Proofs/YulGeneration/Semantics.lean uses fuel-based evaluation (the execYulStmtFuel pattern mentioned elsewhere), which may NOT be partial.

Why This Matters

If only evalIRExpr is partial and the Yul side is total (fuel-based), then:

1. The axiom justification ("both are partial") is wrong
2. The elimination strategy should be simpler — only the IR side needs refactoring
3. The documentation overstates why the axiom is needed

Recommendation

1. Verify whether evalYulExpr in Semantics.lean is actually partial or fuel-based
2. Correct AXIOMS.md to accurately describe the asymmetry
3. Update the elimination strategy accordingly — refactoring only the IR evaluator to match the Yul evaluator's fuel pattern may be sufficient

[Th0rgal]

Fixed in PR #198 — the misleading axiom justification in StatementEquivalence.lean was rewritten to accurately describe the partial/total asymmetry between evalIRExpr and evalYulExpr.