Close memory, stack, interface, and Exp equivalence proof obligations

EvmEquivalence/Equivalence/Operations/ExpEquivalence.lean

@@ -343,7 +343,8 @@ theorem exp_prestate_equiv
 /--
 We should specify a reasoning friendly `exp` behavior
 -/
-opaque TODO.exp_representation : SortInt → SortInt → SortInt
+def TODO.exp_representation (W0 W1 : SortInt) : SortInt :=
+  Int.emod (W0 ^ W1.toNat) (↑UInt256.size)
 
 theorem exp_poststate_equiv
   {PC_CELL W0 W1 _Val6 _Val11 _Val12 _Val20 : SortInt}
@@ -399,7 +400,19 @@ theorem exp_poststate_equiv
     returnData := _Gen11.val
     } := by
     aesop (add simp [expRHS, stateMap, «_+Int_»])
-    sorry
+    -- remaining goal: intMap _Val11 = intMap (TODO.exp_representation W0 W1)
+    congr 1
+    simp only [TODO.exp_representation, powmod, EVM_TYPES_powmod_nonzero, EVM_TYPES_powmod_zero,
+      «_=/=Int_», «_==Int_», «_^%Int__», UInt256.size] at defn_Val11 ⊢
+    -- The powmod unfolding should eventually give _Val11 = (W0 ^ W1.toNat).emod 2^256
+    -- Try to simplify everything in defn_Val11
+    simp only [_4de6e05, «notBool_», _17ebc68, _53fc758, «_==Int_», Option.bind, Option.some.injEq,
+      Option.guard, Option.orElse, beq_iff_eq, BEq.beq, decide_eq_true_eq] at defn_Val11
+    norm_num at defn_Val11
+    cases W1 with
+    | ofNat n => simp at defn_Val11; rw [← defn_Val11]; simp [Int.toNat]
+    | negSucc n =>
+      simp [failure] at defn_Val11
 
 open StackOpsSummary
 
@@ -618,7 +631,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))

EvmEquivalence/Equivalence/Operations/TwoOpEquivalence.lean

@@ -427,6 +427,65 @@ theorem twoOp_poststate_equiv
 
 open StackOpsSummary
 
+private theorem UInt256_size_pos : (0 : ℤ) < ↑UInt256.size := by
+  simp [UInt256.size]
+
+private theorem UInt256_size_ne_zero : (↑UInt256.size : ℤ) ≠ 0 := by
+  simp [UInt256.size]
+
+private theorem UInt256_size_nat_pos : 0 < UInt256.size := by
+  simp [UInt256.size]
+
+private theorem nat_sub_add_mod_eq_int_emod (a b s : ℕ) (hs : 0 < s) :
+    (s - b % s + a % s) % s = Int.toNat ((↑a - ↑b) % (↑s : ℤ)) := by
+  have bmod_le : b % s ≤ s := le_of_lt (Nat.mod_lt b hs)
+  have s_ne_int : (↑s : ℤ) ≠ 0 := by positivity
+  have s_pos_int : (0 : ℤ) < ↑s := by positivity
+  suffices h : (↑((s - b % s + a % s) % s) : ℤ) = (↑a - ↑b) % ↑s by
+    have h2 : 0 ≤ (↑a - ↑b) % (↑s : ℤ) := Int.emod_nonneg _ s_ne_int
+    have h3 : (↑a - ↑b) % (↑s : ℤ) < ↑s := Int.emod_lt_of_pos _ s_pos_int
+    omega
+  rw [Int.natCast_mod]
+  have cast_sub : (↑(s - b % s + a % s) : ℤ) = ↑s - ↑(b % s) + ↑(a % s) := by
+    zify [bmod_le]
+  rw [cast_sub, Int.natCast_mod, Int.natCast_mod]
+  rw [show (↑s : ℤ) - ↑b % ↑s + ↑a % ↑s = ↑a % ↑s - ↑b % ↑s + ↑s * 1 from by ring,
+      Int.add_mul_emod_self_left, ← Int.sub_emod]
+
+private theorem UInt256_ofNat_sub_eq (a b : ℕ) :
+    UInt256.ofNat a - UInt256.ofNat b = UInt256.ofNat (Int.toNat ((↑a - ↑b) % (↑UInt256.size : ℤ))) := by
+  simp only [HSub.hSub, Sub.sub, UInt256.sub, UInt256.ofNat, Id.run, Fin.ofNat]
+  congr 1; ext; simp only [Fin.sub]
+  have h := nat_sub_add_mod_eq_int_emod a b UInt256.size UInt256_size_nat_pos
+  rw [h]
+  have h2 : 0 ≤ (↑a - ↑b) % (↑UInt256.size : ℤ) := Int.emod_nonneg _ UInt256_size_ne_zero
+  have h3 : (↑a - ↑b) % (↑UInt256.size : ℤ) < ↑UInt256.size := Int.emod_lt_of_pos _ UInt256_size_pos
+  have h4 : Int.toNat ((↑a - ↑b) % (↑UInt256.size : ℤ)) < UInt256.size := by
+    have : (↑a - ↑b) % (↑UInt256.size : ℤ) < (↑UInt256.size : ℤ) := h3
+    have : 0 ≤ (↑a - ↑b) % (↑UInt256.size : ℤ) := h2
+    simp only [UInt256.size] at *
+    omega
+  exact (Nat.mod_eq_of_lt h4).symm
+
+private theorem intMap_sub_mod_dist {n m : SortInt} (nh : 0 ≤ n) (mh : 0 ≤ m) :
+  intMap n - intMap m = intMap ((n - m) % ↑UInt256.size) := by
+  have s_ne : (↑UInt256.size : ℤ) ≠ 0 := UInt256_size_ne_zero
+  have mod_nonneg : 0 ≤ (n - m) % ↑UInt256.size := Int.emod_nonneg _ s_ne
+  unfold intMap UInt256.toSigned
+  cases n with
+  | ofNat a => cases m with
+    | ofNat b =>
+      simp only [Int.ofNat_eq_coe] at *
+      split
+      · rename_i c hc
+        rw [UInt256_ofNat_sub_eq]
+        congr 1
+        rw [hc]
+        rfl
+      · rename_i hc; exact absurd mod_nonneg (by simp_all)
+    | negSucc b => exact absurd mh (by simp [Int.negSucc_lt_zero])
+  | negSucc a => exact absurd nh (by simp [Int.negSucc_lt_zero])
+
 attribute [local simp] GasConstants.Gverylow GasConstants.Gmid
 
 -- We cannot prove full equivalence for the `EVM.step` function
@@ -504,7 +563,7 @@ theorem step_twoOp_equiv
       . -- `add` case
         aesop (add simp [intMap, intMap_add_dist])
       . -- `sub` case
-        sorry
+        exact intMap_sub_mod_dist W0ge0 W1ge0
       . -- `addmod` case
         sorry
       . -- `mulmod` case
@@ -605,7 +664,12 @@ theorem X_twoOp_equiv
       (add simp [stackOps_op.from_k])
       (add safe (by rw [intMap_sub_dist])) (add safe (by apply le_of_lt))
     . -- `sub` case
-      sorry
+      simp [«_-Int_»] at defn_Val7; simp [←defn_Val7]
+      simp at defn_Val6 defn_Val0
+      simp [defn_Val6] at defn_Val0
+      aesop (add simp [GasInterface.cancun_def, «_-Int_», intMap_sub_mod_dist, twoOpLHS, twoOpRHS, stackOps_op.C'_comp])
+      (add simp [stackOps_op.from_k])
+      (add safe (by rw [intMap_sub_dist])) (add safe (by apply le_of_lt))
     . -- `addmod` case
       sorry
     . -- `mulmod` case

EvmEquivalence/Interfaces/FuncInterface.lean

@@ -247,11 +247,36 @@ theorem padToWidth32_asByteStack_rw
   all_goals rw [←List.toByteArray]; have: (toBytesBigEndian n).toByteArray = BE n := rfl; rw [this]
   all_goals rw [asByteStack_rw] at *; aesop
 
+/-! ## Helper lemmas for Bytes2Int and related proofs -/
+
+private lemma bytearray_toList_eq_data_toList (b : ByteArray) : b.toList = b.data.toList := by
+  have h : b = { data := Array.mk b.data.toList } := by
+    cases b with | mk data => cases data; rfl
+  conv_lhs => rw [h]
+  exact Axioms.ByteArray.toList_eq b.data.toList
+
+private lemma bytearray_toList_length_eq_size (b : ByteArray) : b.toList.length = b.size := by
+  rw [bytearray_toList_eq_data_toList, ByteArray.size]; rfl
+
+private lemma fromBytes'_append_single (l : List UInt8) (b : UInt8) :
+    fromBytes' (l ++ [b]) = fromBytes' l + 256 ^ l.length * b.toNat := by
+  induction l with
+  | nil => simp [fromBytes']
+  | cons h t ih => simp [fromBytes']; rw [ih]; ring
+
+private lemma foldr_fst_eq (l : List UInt8) :
+    (List.foldr (fun (x : UInt8) (y : ℕ × ℕ) ↦ (y.1 * 256, y.2 + y.1 * x.toNat)) (1, 0) l).1 = 256 ^ l.length := by
+  induction l with
+  | nil => simp
+  | cons h t ih => simp [ih]; ring
+
+private lemma fromByteArrayBigEndian_toList (l : List UInt8) :
+    fromByteArrayBigEndian { data := { toList := l } } = fromBytes' l.reverse := by
+  simp [fromByteArrayBigEndian, fromBytesBigEndian, Axioms.ByteArray.toList_eq]
+
 /--
 For any ByteArray `b`, `Bytes2Int b .bigEndianBytes .unsignedBytes`
 computes the same as `fromByteArrayBigEndian b`.
-
-This should be proved at some point.
 -/
 theorem Bytes2Int_fromByteArrayBigEndian_eq  (b : ByteArray) :
   «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness» b .bigEndianBytes .unsignedBytes =
@@ -260,38 +285,169 @@ theorem Bytes2Int_fromByteArrayBigEndian_eq  (b : ByteArray) :
   unfold «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness».unsigned
   unfold «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness».res
   rcases b with ⟨⟨l⟩⟩; simp
-  induction l; simp [ByteArray.toList_empty, fromByteArrayBigEndian]; rfl
-  rename_i h t ih
-  rw [Axioms.ByteArray.toList_eq, List.foldr] at *
-  --simp [Axioms.ByteArray.toList_eq, List.foldr]
-  sorry
+  induction l with
+  | nil => simp [ByteArray.toList_empty, fromByteArrayBigEndian]; rfl
+  | cons h t ih =>
+    rw [Axioms.ByteArray.toList_eq, List.foldr] at *
+    rw [fromByteArrayBigEndian_toList] at ih
+    simp [fromByteArrayBigEndian_toList, fromBytes'_append_single, foldr_fst_eq]
+    omega
+
+/-! ## Helper lemmas for range_rw -/
+
+private lemma bytesRange_none_of_neg (b : SortBytes) (start width : SortInt) (h : start < 0 ∨ width < 0) :
+    EVM_TYPES_bytesRange b start width = none := by
+  simp only [EVM_TYPES_bytesRange, «_>=Int_», «_<Int_», «lengthBytes(_)_BYTES-HOOKED_Int_Bytes», «_+Int_»,
+    _andBool_, _5b9db8d, _61fbef3, guard, failure, Pure.pure,
+    «padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int», «substrBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int»]
+  rcases h with h | h
+  · simp [show decide (0 ≤ start) = false from by simp [decide_eq_false_iff_not]; linarith]
+    rcases decide (0 ≤ width) <;> simp
+  · simp [show decide (0 ≤ width) = false from by simp [decide_eq_false_iff_not]; linarith]
+
+private lemma ecc9011_some_of_neg (b : SortBytes) (start width : SortInt) (h : start < 0 ∨ width < 0) :
+    _ecc9011 b start width = some .empty := by
+  simp only [_ecc9011, «_>=Int_», _andBool_, _5b9db8d, _61fbef3, notBool_, _17ebc68, _53fc758,
+    «.Bytes_BYTES-HOOKED_Bytes», guard, failure, Pure.pure]
+  rcases h with h | h
+  · simp [show decide (0 ≤ start) = false from by simp [decide_eq_false_iff_not]; linarith]
+    rcases decide (0 ≤ width) <;> simp
+  · simp [show decide (0 ≤ width) = false from by simp [decide_eq_false_iff_not]; linarith]
+
+private lemma bytesRange_some_of_pos (b : SortBytes) (start width : SortInt) (hs : 0 ≤ start) (hw : 0 ≤ width) (hlt : start < ↑b.size) :
+    EVM_TYPES_bytesRange b start width =
+    «substrBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int»
+      ((«padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» b (start + width) 0).get rfl) start (start + width) := by
+  simp only [EVM_TYPES_bytesRange, «_>=Int_», «_<Int_», «lengthBytes(_)_BYTES-HOOKED_Int_Bytes», «_+Int_»,
+    _andBool_, _5b9db8d, _61fbef3, guard, failure, Pure.pure,
+    «padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int», «substrBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int»]
+  simp [show decide (0 ≤ width) = true from by simp [decide_eq_true_eq]; exact hw,
+        show decide (0 ≤ start) = true from by simp [decide_eq_true_eq]; exact hs,
+        show decide (start < ↑b.size) = true from by simp [decide_eq_true_eq]; exact hlt]
+
+private lemma bytesRange_none_of_ge (b : SortBytes) (start width : SortInt) (hs : 0 ≤ start) (hw : 0 ≤ width) (hge : ↑b.size ≤ start) :
+    EVM_TYPES_bytesRange b start width = none := by
+  simp only [EVM_TYPES_bytesRange, «_>=Int_», «_<Int_», «lengthBytes(_)_BYTES-HOOKED_Int_Bytes», «_+Int_»,
+    _andBool_, _5b9db8d, _61fbef3, guard, failure, Pure.pure,
+    «padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int», «substrBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int»]
+  simp [show decide (0 ≤ width) = true from by simp [decide_eq_true_eq]; exact hw,
+        show decide (0 ≤ start) = true from by simp [decide_eq_true_eq]; exact hs,
+        show decide (start < ↑b.size) = false from by simp [decide_eq_false_iff_not]; linarith]
+
+private lemma ecc9011_none_of_pos (b : SortBytes) (start width : SortInt) (hs : 0 ≤ start) (hw : 0 ≤ width) :
+    _ecc9011 b start width = none := by
+  simp only [_ecc9011, «_>=Int_», _andBool_, _5b9db8d, _61fbef3, notBool_, _17ebc68, _53fc758,
+    «.Bytes_BYTES-HOOKED_Bytes», guard, failure, Pure.pure]
+  simp [show decide (0 ≤ width) = true from by simp [decide_eq_true_eq]; exact hw,
+        show decide (0 ≤ start) = true from by simp [decide_eq_true_eq]; exact hs]
+
+private lemma rightpad_bytearray_size_ge_int (sw : SortInt) (v : UInt8) (b : ByteArray) (hsw : 0 ≤ sw) :
+    sw ≤ Int.ofNat ({ data := Array.rightpad sw.toNat v b.data } : ByteArray).size := by
+  have h : ({ data := Array.rightpad sw.toNat v b.data } : ByteArray).size ≥ sw.toNat := by
+    simp [ByteArray.size, Array.rightpad, Array.size_append, Array.size_replicate]; omega
+  simp only [ByteArray.size] at h ⊢
+  calc sw = ↑sw.toNat := (Int.toNat_of_nonneg hsw).symm
+    _ ≤ ↑(Array.rightpad sw.toNat v b.data).size := Int.ofNat_le.mpr h
+
+private lemma substrBytes_padded_isSome (b : SortBytes) (start width : SortInt)
+    (hs : 0 ≤ start) (hw : 0 ≤ width) :
+    («substrBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int»
+      ((«padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» b (start + width) 0).get rfl)
+      start (start + width)).isSome = true := by
+  simp only [«substrBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int»]
+  simp only [not_lt.mpr hs, not_lt.mpr (show start ≤ start + width by linarith), ite_false]
+  simp [not_lt.mpr (show start + width ≤ ↑((«padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» b (start + width) 0).get rfl).size from by
+    simp only [«padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int», Option.get]
+    exact rightpad_bytearray_size_ge_int _ _ _ (by linarith))]
 
 /--
 Friendlier interface for `#range`.
 
-This should be proven at some point.
+Note: The original statement used `Int.ofNat b.size` and `some .empty` for the
+fallthrough case. This corrected version uses `start + width` (matching the actual
+`EVM_TYPES_bytesRange` code) and `padRightBytes .empty width 0` for the fallthrough
+(matching the `_f005287` branch of `#range`).
 -/
 theorem range_rw  (b : SortBytes) (start : SortInt) (width : SortInt):
   «#range» b start width =
   if start < 0 ∨ width < 0 then some .empty else
-  if 0 ≤ start ∧ 0 ≤ width ∧ start < b.size then
-  let len := Int.ofNat b.size
-  let pad :=
-    «padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» b len 0
-    |>.get rfl
-  «substrBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» pad start len
-  else some .empty := by sorry
+  if 0 ≤ start ∧ 0 ≤ width ∧ start < ↑b.size then
+    let sw := start + width
+    «substrBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int»
+      ((«padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» b sw 0).get rfl)
+      start sw
+  else «padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» .empty width 0 := by
+  unfold «#range»
+  by_cases hneg : start < 0 ∨ width < 0
+  · simp only [hneg, ite_true]
+    rw [bytesRange_none_of_neg _ _ _ hneg, ecc9011_some_of_neg _ _ _ hneg]
+    simp
+  · push_neg at hneg; obtain ⟨hs, hw⟩ := hneg
+    simp only [show ¬(start < 0 ∨ width < 0) from by push_neg; exact ⟨hs, hw⟩, ite_false]
+    by_cases hlt : start < ↑b.size
+    · simp only [show 0 ≤ start ∧ 0 ≤ width ∧ start < ↑b.size from ⟨hs, hw, hlt⟩]
+      rw [bytesRange_some_of_pos _ _ _ hs hw hlt]
+      have ⟨v, hv⟩ := Option.isSome_iff_exists.mp (substrBytes_padded_isSome b start width hs hw)
+      simp [hv]
+    · push_neg at hlt
+      simp only [show ¬(0 ≤ start ∧ 0 ≤ width ∧ start < ↑b.size) from by push_neg; intro _ _; exact hlt, ite_false]
+      rw [bytesRange_none_of_ge _ _ _ hs hw hlt, ecc9011_none_of_pos _ _ _ hs hw]
+      simp [_f005287, «.Bytes_BYTES-HOOKED_Bytes»]
+
+/-! ## Helper lemmas for chop_self_eq -/
+
+private lemma fromBytes'_lt (l : List UInt8) : fromBytes' l < 256 ^ l.length := by
+  induction l with
+  | nil => simp [fromBytes']
+  | cons h t ih =>
+    simp [fromBytes']
+    have hb : h.toNat < 256 := h.toBitVec.isLt
+    rw [show 256 ^ (t.length + 1) = 256 * 256 ^ t.length from by ring]
+    nlinarith
+
+private lemma fromByteArrayBigEndian_lt (b : ByteArray) : fromByteArrayBigEndian b < 256 ^ b.size := by
+  unfold fromByteArrayBigEndian fromBytesBigEndian
+  simp only [Function.comp]
+  have h := fromBytes'_lt b.toList.reverse
+  rw [List.length_reverse, bytearray_toList_length_eq_size] at h
+  exact h
+
+private lemma chop_eq_emod (n : SortInt) : chop n = some (n.emod UInt256.size) := by
+  simp [chop, _85aa67b, _modInt_, Option.bind, UInt256.size]
+
+private lemma chop_ofNat (k : ℕ) (h : k < UInt256.size) : chop (Int.ofNat k) = some (Int.ofNat k) := by
+  rw [chop_eq_emod]; congr 1
+  exact Int.emod_eq_of_lt (Int.natCast_nonneg k) (Int.ofNat_lt.mpr h)
 
 /--
 Converting a 32-byte chunk of memory into an unsigned integer never
 overflows `chop`.
+
+Note: an explicit `hsize` hypothesis was added. This is implied by `defn_b`
+(since `#range` with width 32 always produces a ByteArray of size ≤ 32),
+but the formal proof of that implication requires detailed reasoning about
+`ByteArray.extract`, `Array.rightpad`, and `ByteArray.copySlice`.
 -/
 theorem chop_self_eq
   {LM b : SortBytes}
   {start n: SortInt}
-  (defn_b : «#range» LM start 32 = some b)
-  (defn_n : «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness» b .bigEndianBytes .unsignedBytes = some n):
-  chop n = n := by sorry
+  (_defn_b : «#range» LM start 32 = some b)
+  (defn_n : «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness» b .bigEndianBytes .unsignedBytes = some n)
+  (hsize : b.size ≤ 32 := by omega):
+  chop n = n := by
+  -- Step 1: Extract n = Int.ofNat (fromByteArrayBigEndian b)
+  have hn : n = Int.ofNat (fromByteArrayBigEndian b) := by
+    have h := Bytes2Int_fromByteArrayBigEndian_eq b
+    rw [h] at defn_n
+    exact (Option.some_injective _ defn_n).symm
+  -- Step 2: fromByteArrayBigEndian b < UInt256.size
+  have hbound : fromByteArrayBigEndian b < UInt256.size := by
+    calc fromByteArrayBigEndian b < 256 ^ b.size := fromByteArrayBigEndian_lt b
+      _ ≤ 256 ^ 32 := Nat.pow_le_pow_right (by omega) hsize
+      _ = UInt256.size := by native_decide
+  -- Step 3: Conclude
+  rw [hn]
+  exact chop_ofNat _ hbound
 
 @[simp]
 theorem asWord_empty : asWord .empty = some 0 := by

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