docs: Fix misleading axiom justification — only IR eval is partial

AXIOMS.md

@@ -37,21 +37,23 @@ axiom evalIRExpr_eq_evalYulExpr (selector : Nat) (irState : IRState) (expr : Yul
 **Purpose**: Proves that expression evaluation produces identical results in IR and Yul contexts when states are aligned.
 
 **Why Axiom?**:
-- Both `evalIRExpr` and `evalYulExpr` are defined as `partial` functions (not provably terminating in Lean)
-- Lean cannot prove equality between partial functions
+- `evalIRExpr` is defined as `partial` (not provably terminating in Lean), making it opaque to the kernel
+- `evalYulExpr` is **total** (no `partial` annotation) — it uses structural recursion
+- Lean cannot unfold a `partial` definition inside a proof, so equality between the IR and Yul evaluators cannot be proven even though their source code is structurally identical
 - Functions have identical source code structure but different state type parameters
 
 **Soundness Argument**:
 1. **Source code inspection**: Both functions have structurally identical implementations
-2. **State translation**: `yulStateOfIR` simply copies all fields from IRState to YulState
-3. **Selector field**: Only difference is the `selector` field, which doesn't affect expression evaluation
-4. **Differential testing**: 70,000+ property tests validate this equivalence holds in practice
+2. **Asymmetry**: Only the IR side is `partial`; the Yul side is already total
+3. **State translation**: `yulStateOfIR` simply copies all fields from IRState to YulState
+4. **Selector field**: Only difference is the `selector` field, which doesn't affect expression evaluation
+5. **Differential testing**: 70,000+ property tests validate this equivalence holds in practice
 
 **Alternative Approach**:
-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
+To eliminate this axiom, only the IR evaluator needs refactoring:
+- Refactor `evalIRExpr` (and `evalIRExprs`, `evalIRCall`) to use fuel parameters or well-founded recursion on expression depth, matching the total pattern already used by `evalYulExpr`
+- The Yul side is already total and requires no changes
+- **Effort**: ~300 lines of refactoring (simpler than previously estimated since only one side needs work)
 
 **Trade-off**: Given that the functions are structurally identical by inspection and validated by extensive testing, the axiom is a pragmatic choice.
 
@@ -76,7 +78,7 @@ axiom evalIRExprs_eq_evalYulExprs (selector : Nat) (irState : IRState) (exprs :
 
 **Purpose**: List version of `evalIRExpr_eq_evalYulExpr` for multiple expressions.
 
-**Why Axiom?**: Same reasoning as axiom #1 (partial functions).
+**Why Axiom?**: Same reasoning as axiom #1 — `evalIRExprs` is `partial` while `evalYulExprs` is total.
 
 **Soundness Argument**:
 - Follows directly from axiom #1 via structural induction on lists

CONTRIBUTING.md

@@ -167,7 +167,7 @@ All axioms **must** be documented inline **and** in AXIOMS.md:
 ```lean
 /-- AXIOM: Expression evaluation equivalence
 
-This is an axiom because both evalIRExpr and evalYulExpr are partial functions.
+This is an axiom because evalIRExpr is partial (evalYulExpr is total).
 See AXIOMS.md for full soundness justification.
 -/
 axiom evalIRExpr_eq_evalYulExpr : ...

Compiler/Proofs/YulGeneration/README.md

@@ -39,7 +39,7 @@ Two expression evaluation axioms in `StatementEquivalence.lean`:
 1. `evalIRExpr_eq_evalYulExpr` - IR and Yul expression evaluation are identical when states are aligned
 2. `evalIRExprs_eq_evalYulExprs` - List version of the above
 
-These are sound because both eval functions have identical source code and `yulStateOfIR` copies all fields. Making them theorems would require refactoring both `partial` functions to use fuel parameters (~500+ lines).
+These are sound because both eval functions have identical source code and `yulStateOfIR` copies all fields. The axiom exists because `evalIRExpr` is `partial` (opaque to Lean's kernel) while `evalYulExpr` is total. Eliminating the axiom requires only refactoring the IR evaluator to use fuel parameters (~300 lines).
 
 ## References
 

Compiler/Proofs/YulGeneration/StatementEquivalence.lean

@@ -24,18 +24,18 @@ Individual statement proofs compose via `execIRStmtsFuel_equiv_execYulStmtsFuel_
 
 /-- IR and Yul expression evaluation are identical when states are aligned.
 
-This is an axiom because both `evalIRExpr` and `evalYulExpr` are defined as `partial`
-functions, making them unprovable in Lean's logic. However, this axiom is sound because:
+This is an axiom because `evalIRExpr` is defined as `partial` (not provably terminating),
+making it opaque to Lean's kernel. `evalYulExpr` is total (structural recursion), but
+Lean cannot unfold the `partial` IR side to prove equality. This axiom is sound because:
 
 1. Both functions have **identical** source code (see IRInterpreter.lean and Semantics.lean)
 2. `yulStateOfIR` just copies all IRState fields to YulState
 3. The only difference is the `selector` field, which doesn't affect expression evaluation
 4. This is a structural equality, not a semantic one
 
-**Alternative**: To avoid this axiom, we would need to refactor both eval functions
-to use fuel parameters (similar to what we did for execIRStmtFuel). This would be
-a significant undertaking (~500+ lines of code) for relatively little benefit, since
-the functions are already known to be identical by inspection.
+**Alternative**: To avoid this axiom, only the IR evaluator needs refactoring to use
+fuel parameters (matching the pattern already used by `evalYulExpr`). The Yul side is
+already total and requires no changes. Estimated effort: ~300 lines.
 
 **Usage**: This axiom is used by all statement equivalence proofs to show that
 evaluating expressions gives the same results in both IR and Yul contexts.