From 4e5c6e7b745a122f46a20600431c825fc17ec4cb Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 16 Feb 2026 02:19:08 +0000 Subject: [PATCH] =?UTF-8?q?docs:=20Fix=20misleading=20axiom=20justificatio?= =?UTF-8?q?n=20=E2=80=94=20only=20IR=20eval=20is=20partial=20(issue=20#160?= =?UTF-8?q?)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit AXIOMS.md, StatementEquivalence.lean, CONTRIBUTING.md, and YulGeneration/README.md all claimed that "both evalIRExpr and evalYulExpr are partial functions." In fact, only evalIRExpr is partial — evalYulExpr uses structural recursion and is total. This matters because: - The elimination strategy is simpler than documented: only the IR evaluator needs refactoring (~300 LOC, not ~500+) - The Yul side already demonstrates the fuel-based pattern to follow - The trust surface is smaller than previously stated Co-Authored-By: Claude Opus 4.6 --- AXIOMS.md | 22 ++++++++++--------- CONTRIBUTING.md | 2 +- Compiler/Proofs/YulGeneration/README.md | 2 +- .../YulGeneration/StatementEquivalence.lean | 12 +++++----- 4 files changed, 20 insertions(+), 18 deletions(-) diff --git a/AXIOMS.md b/AXIOMS.md index 8d3248026..0318a3e3b 100644 --- a/AXIOMS.md +++ b/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 diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b7a660109..16797e288 100644 --- a/CONTRIBUTING.md +++ b/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 : ... diff --git a/Compiler/Proofs/YulGeneration/README.md b/Compiler/Proofs/YulGeneration/README.md index 268ea9a95..433fcf14a 100644 --- a/Compiler/Proofs/YulGeneration/README.md +++ b/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 diff --git a/Compiler/Proofs/YulGeneration/StatementEquivalence.lean b/Compiler/Proofs/YulGeneration/StatementEquivalence.lean index 474c8cc12..6f9130e04 100644 --- a/Compiler/Proofs/YulGeneration/StatementEquivalence.lean +++ b/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.