From 0c459b68eb954e467268f078066d31cca64455ac Mon Sep 17 00:00:00 2001 From: Elias Judin Date: Sun, 22 Feb 2026 19:59:32 +0200 Subject: [PATCH] Fill `W1_zero_eq` sorry in `X_exp_equiv` Replaces the `sorry` in the local helper `W1_zero_eq` inside `X_exp_equiv` with a proof using BEq-to-equality conversion, `intMap_toNat`, and `Int.toNat_eq_zero`. Aristotle solved the decomposed micro-theorem `int_eq_zero_of_nonneg_toNat_zero` (project 00c420ff-9399-41cc-9401-8e44071a3fcd, solved_target: true), which directly guided this recomposition. Co-authored-by: Aristotle (Harmonic) --- .../Equivalence/Operations/ExpEquivalence.lean | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/EvmEquivalence/Equivalence/Operations/ExpEquivalence.lean b/EvmEquivalence/Equivalence/Operations/ExpEquivalence.lean index be2fb21..aac6da0 100644 --- a/EvmEquivalence/Equivalence/Operations/ExpEquivalence.lean +++ b/EvmEquivalence/Equivalence/Operations/ExpEquivalence.lean @@ -618,7 +618,18 @@ theorem X_exp_equiv rw [stack_op, code_op, pc_equiv, X_stackOps_summary] /- This have could be subsumed, but it's useful for the `gt0` case above -/ have W1_zero_eq : (intMap W1 == { val := 0 }) = true → W1 = 0 := by - sorry + intro h + have hEq : intMap W1 = ({ val := 0 } : UInt256) := by + cases hi : intMap W1 with + | mk v => + rw [hi] at h + simp [BEq.beq] at h + have hv : v = 0 := beq_iff_eq.mp h + simp [hv] + have hNat : (intMap W1).toNat = 0 := by + simpa [UInt256.toNat] using congrArg UInt256.toNat hEq + rw [intMap_toNat W1ge0 boundedW1] at hNat + linarith [Int.toNat_eq_zero.mp hNat] have W1_zero_eq' : ec = .eq0 → W1 = 0 := by intro ecc; simp [ecc] at defn_Val0 aesop (add simp [«_<=Int_»]) (add safe (by linarith))