From da20bd0cf8537446d5000509a0e478af67e2805e Mon Sep 17 00:00:00 2001 From: Elias Judin Date: Wed, 25 Feb 2026 14:06:59 +0200 Subject: [PATCH 1/3] Fill W1_zero_eq in X_exp_equiv 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)) From c54d5f93efe3735f46a3c5aeea2fb1b5114ba512 Mon Sep 17 00:00:00 2001 From: Elias Judin Date: Wed, 25 Feb 2026 14:06:59 +0200 Subject: [PATCH 2/3] Normalize X_mstore_summary gas precondition Co-authored-by: Aristotle (Harmonic) --- EvmEquivalence/Summaries/MstoreSummary.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/EvmEquivalence/Summaries/MstoreSummary.lean b/EvmEquivalence/Summaries/MstoreSummary.lean index 2e64be0..28d753f 100644 --- a/EvmEquivalence/Summaries/MstoreSummary.lean +++ b/EvmEquivalence/Summaries/MstoreSummary.lean @@ -276,7 +276,7 @@ theorem X_mstore_summary (symState : EVM.State) returnData := symReturnData, execLength := symExecLength} -- Assume we have enough gas - GasConstants.Gverylow < symGasAvailable.toNat - (memoryExpansionCost ss op.t) → + GasConstants.Gverylow ≤ symGasAvailable.toNat - (memoryExpansionCost ss op.t) → memoryExpansionCost ss op.t < UInt256.size → X symGasAvailable.toNat symValidJumps ss = .ok (.success {ss with @@ -297,8 +297,8 @@ theorem X_mstore_summary (symState : EVM.State) simp; apply Nat.ge_of_not_lt; simp; omega simp [α] have fls1 : (symGasAvailable.toNat < memoryExpansionCost ss op.t) = False := by - rw [Nat.lt_sub_iff_add_lt] at enoughGas - aesop (add safe (by linarith)) + apply eq_false_intro; rw [Nat.not_lt] + rw [GasConstants.Gverylow] at enoughGas; omega have decode_rw : ((decode ss.executionEnv.code ss.pc).getD ⟨@Operation.STOP .EVM, none⟩).1 = op.t := by aesop have gavail_rw1 : ss.gasAvailable.toNat = symGasAvailable.toNat := rfl have gavail_rw2 : ss.gasAvailable = symGasAvailable := rfl From 68de99f2be2b933994dfa89bb6b87bb07792a996 Mon Sep 17 00:00:00 2001 From: Elias Judin Date: Wed, 25 Feb 2026 14:06:59 +0200 Subject: [PATCH 3/3] Normalize X_mload_summary gas precondition Co-authored-by: Aristotle (Harmonic) --- EvmEquivalence/Summaries/MloadSummary.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/EvmEquivalence/Summaries/MloadSummary.lean b/EvmEquivalence/Summaries/MloadSummary.lean index 3fec4f1..0aafcf2 100644 --- a/EvmEquivalence/Summaries/MloadSummary.lean +++ b/EvmEquivalence/Summaries/MloadSummary.lean @@ -159,7 +159,7 @@ theorem X_mload_summary (symState : EVM.State) returnData := symReturnData, execLength := symExecLength} -- Assume we have enough gas - GasConstants.Gverylow < symGasAvailable.toNat - (memoryExpansionCost ss Operation.MLOAD) → + GasConstants.Gverylow ≤ symGasAvailable.toNat - (memoryExpansionCost ss Operation.MLOAD) → memoryExpansionCost ss Operation.MLOAD < UInt256.size → X symGasAvailable.toNat symValidJumps ss = .ok (.success {ss with @@ -195,8 +195,7 @@ theorem X_mload_summary (symState : EVM.State) have fls2 : ((symGasAvailable - UInt256.ofNat (memoryExpansionCost ss Operation.MLOAD)).toNat < GasConstants.Gverylow) = False := by apply eq_false_intro; rw [Nat.not_lt] have fls1 : (symGasAvailable.toNat < memoryExpansionCost ss (@Operation.MLOAD .EVM)) = False := by - rw [Nat.lt_sub_iff_add_lt] at enoughGas - aesop (add safe (by omega)) (add safe (by linarith)) (add simp [Cₘ, MachineState.M]) + apply eq_false_intro; rw [Nat.not_lt]; rw [GasConstants.Gverylow] at enoughGas; omega rw [UInt256.toNat_sub_dist, UInt256.ofNat_toNat] <;> aesop (add simp [UInt256.ofNat_le, UInt256.ofNat_toNat]) --have ss_lt2_f (n : ℕ) : (n + 1 + 1 < 2) = False := by simp