diff --git a/EvmEquivalence/Equivalence/MloadEquivalence.lean b/EvmEquivalence/Equivalence/MloadEquivalence.lean
index 2b266e2..c7693f1 100644
--- a/EvmEquivalence/Equivalence/MloadEquivalence.lean
+++ b/EvmEquivalence/Equivalence/MloadEquivalence.lean
@@ -399,6 +399,201 @@ theorem range_lookupMemory_eq
   sorry
   . aesop
 
+/-! ## Private helpers for KEVM `Cmem` ↔ EVM `Cₘ` gas correspondence (MLOAD, width = 32) -/
+
+/-- Connects the KEVM `Cmem` function on the CANCUN schedule to the EVM `Cₘ` function. -/
+private theorem Cmem_cancun_eq_Cm (N : SortInt) (hN : 0 ≤ N) (hNs : N < ↑UInt256.size) :
+    Cmem .CANCUN_EVM N = some ↑(EVM.Cₘ (intMap N)) := by
+  simp [Cmem, GAS_FEES_Cmem, «_*Int_», «_/Int_», «_+Int_», GasInterface.cancun_def]
+  simp [EVM.Cₘ, EVM.Cₘ.QuadraticCeofficient, GasConstants.Gmemory]
+  rw [intMap_toNat hN hNs]
+  cases N with
+  | ofNat n =>
+    simp [Int.toNat]
+    conv_lhs => rw [show (↑n * ↑n : Int) = ↑(n * n) from by push_cast; ring]
+    rw [show Int.tdiv ↑(n * n) (512 : Int) = ↑(n * n / 512) from Int.ofNat_tdiv _ _]
+    push_cast; ring
+  | negSucc n =>
+    exfalso; exact absurd hN (by simp)
+
+private theorem memUsageUpdate_nonneg
+  {MEMORYUSED_CELL W0 _Val : SortInt}
+  (defn_Val : «#memoryUsageUpdate» MEMORYUSED_CELL W0 32 = some _Val)
+  (mucge0 : 0 ≤ MEMORYUSED_CELL) :
+  0 ≤ _Val := by
+  rw [memoryUsageUpdate_rw _ _ _ (by omega : (0 : Int) < 32), Option.some.injEq] at defn_Val
+  subst defn_Val
+  exact le_sup_of_le_left mucge0
+
+private theorem memUsageUpdate_small
+  {MEMORYUSED_CELL W0 _Val : SortInt}
+  (defn_Val : «#memoryUsageUpdate» MEMORYUSED_CELL W0 32 = some _Val)
+  (W0ge0 : 0 ≤ W0)
+  (mucsmall : MEMORYUSED_CELL < ↑UInt256.size)
+  (W0small_realpolitik : W0 < ↑UInt32.size) :
+  _Val < ↑UInt256.size := by
+  rw [memoryUsageUpdate_rw _ _ _ (by omega : (0 : Int) < 32), Option.some.injEq] at defn_Val
+  subst defn_Val
+  have hsum_nonneg : 0 ≤ W0 + 32 + 31 := by linarith
+  have hceil_le : Int.tdiv (W0 + 32 + 31) 32 ≤ W0 + 32 + 31 :=
+    Int.tdiv_le_self 32 hsum_nonneg
+  have hsum_bound : W0 + 32 + 31 < ↑UInt256.size := by
+    have : (UInt256.size : ℤ) = 115792089237316195423570985008687907853269984665640564039457584007913129639936 := by
+      simp [UInt256.size]
+    have : (UInt32.size : ℤ) = 4294967296 := by simp [UInt32.size]
+    linarith
+  exact max_lt mucsmall (lt_of_le_of_lt hceil_le hsum_bound)
+
+private theorem Cm_mono (a b : UInt256) (h : a.toNat ≤ b.toNat) :
+    EVM.Cₘ a ≤ EVM.Cₘ b := by
+  simp [EVM.Cₘ, EVM.Cₘ.QuadraticCeofficient]
+  have h1 : GasConstants.Gmemory * a.toNat ≤ GasConstants.Gmemory * b.toNat :=
+    Nat.mul_le_mul_left _ h
+  have h2 : a.toNat * a.toNat / 512 ≤ b.toNat * b.toNat / 512 :=
+    Nat.div_le_div_right (Nat.mul_le_mul h h)
+  omega
+
+/-- For MLOAD, `MachineState.M` (computing active words) equals `intMap _Val` where
+    `_Val` comes from `#memoryUsageUpdate`. -/
+private theorem vawg_eq_intMap_mload
+  {MEMORYUSED_CELL W0 _Val : SortInt}
+  (defn_Val : «#memoryUsageUpdate» MEMORYUSED_CELL W0 32 = some _Val)
+  (W0ge0 : 0 ≤ W0) (W0small : W0 < ↑UInt256.size)
+  (mucge0 : 0 ≤ MEMORYUSED_CELL) (mucsmall : MEMORYUSED_CELL < ↑UInt256.size) :
+  UInt256.ofNat (MachineState.M (intMap MEMORYUSED_CELL).toNat (intMap W0).toNat 32) = intMap _Val := by
+  have aw := MstoreOpcodeEquivalence.activeWords_eq .mstore defn_Val W0ge0 W0small mucge0 mucsmall
+  simp only [MstoreSummary.activeWords_comp] at aw
+  exact aw
+
+/-- Proves the gas correctness goal in `X_mload_equiv`: the KEVM gas chain
+    (Cmem subtractions via `_-Int_`) equals the EVM `memoryExpansionCost` (via `Cₘ`). -/
+private theorem gas_cost_X_mload_equiv
+  {GAS_CELL MEMORYUSED_CELL W0 _Val17 _Val18 _Val19 _Val20 _Val21 _Val22 _Val23 : SortInt}
+  {SCHEDULE_CELL : SortSchedule}
+  (defn_Val17 : «#memoryUsageUpdate» MEMORYUSED_CELL W0 32 = some _Val17)
+  (defn_Val18 : Cmem SCHEDULE_CELL _Val17 = some _Val18)
+  (defn_Val19 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val19)
+  (defn_Val20 : «_-Int_» _Val18 _Val19 = some _Val20)
+  (defn_Val21 : «_-Int_» GAS_CELL _Val20 = some _Val21)
+  (defn_Val22 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val22)
+  (defn_Val23 : «_-Int_» _Val21 _Val22 = some _Val23)
+  (cancun : SCHEDULE_CELL = .CANCUN_EVM)
+  (gavailSmall : GAS_CELL < ↑UInt256.size)
+  (W0ge0 : 0 ≤ W0) (W0small : W0 < ↑UInt256.size)
+  (mucge0 : 0 ≤ MEMORYUSED_CELL) (mucsmall : MEMORYUSED_CELL < ↑UInt256.size)
+  (W0small_realpolitik : W0 < ↑UInt32.size)
+  (hmec_le_gas : _Val20 ≤ GAS_CELL)
+  (hgvl_le : _Val22 ≤ GAS_CELL - _Val20) :
+  intMap GAS_CELL -
+    UInt256.ofNat (EVM.Cₘ (UInt256.ofNat (MachineState.M (intMap MEMORYUSED_CELL).toNat (intMap W0).toNat 32)) -
+                   EVM.Cₘ (intMap MEMORYUSED_CELL)) -
+    UInt256.ofNat GasConstants.Gverylow = intMap _Val23 := by
+  have eq20 : _Val18 - _Val19 = _Val20 := by simp [«_-Int_»] at defn_Val20; exact defn_Val20
+  have eq21 : GAS_CELL - _Val20 = _Val21 := by simp [«_-Int_»] at defn_Val21; exact defn_Val21
+  have eq23 : _Val21 - _Val22 = _Val23 := by simp [«_-Int_»] at defn_Val23; exact defn_Val23
+  have eq22 : _Val22 = 3 := by
+    rw [cancun] at defn_Val22; simp [GasInterface.cancun_def] at defn_Val22; exact defn_Val22.symm
+  have h17_nn := memUsageUpdate_nonneg defn_Val17 mucge0
+  have h17_sm := memUsageUpdate_small defn_Val17 W0ge0 mucsmall W0small_realpolitik
+  have eq18 : _Val18 = ↑(EVM.Cₘ (intMap _Val17)) := by
+    have := Cmem_cancun_eq_Cm _Val17 h17_nn h17_sm
+    rw [cancun] at defn_Val18; rw [this] at defn_Val18
+    exact (Option.some.inj defn_Val18).symm
+  have eq19 : _Val19 = ↑(EVM.Cₘ (intMap MEMORYUSED_CELL)) := by
+    have := Cmem_cancun_eq_Cm MEMORYUSED_CELL mucge0 mucsmall
+    rw [cancun] at defn_Val19; rw [this] at defn_Val19
+    exact (Option.some.inj defn_Val19).symm
+  rw [vawg_eq_intMap_mload defn_Val17 W0ge0 W0small mucge0 mucsmall]
+  have hCm_le : EVM.Cₘ (intMap MEMORYUSED_CELL) ≤ EVM.Cₘ (intMap _Val17) := by
+    apply Cm_mono
+    rw [intMap_toNat mucge0 mucsmall, intMap_toNat h17_nn h17_sm]
+    have defn17' := defn_Val17
+    rw [memoryUsageUpdate_rw _ _ _ (by omega : (0 : Int) < 32)] at defn17'
+    have eq17 : _Val17 = MEMORYUSED_CELL ⊔ Int.tdiv (W0 + 32 + 31) 32 :=
+      (Option.some.inj defn17').symm
+    rw [eq17]
+    exact Int.toNat_le_toNat (le_max_left _ _)
+  have hv23 : _Val23 = GAS_CELL - (↑(EVM.Cₘ (intMap _Val17)) - ↑(EVM.Cₘ (intMap MEMORYUSED_CELL))) - 3 := by
+    rw [← eq23, ← eq21, ← eq20, eq18, eq19, eq22]
+  rw [hv23]
+  set cm17 := EVM.Cₘ (intMap _Val17) with hcm17_def
+  set cmmu := EVM.Cₘ (intMap MEMORYUSED_CELL) with hcmmu_def
+  have hcast : (↑cm17 : SortInt) - ↑cmmu = ↑(cm17 - cmmu) := (Nat.cast_sub hCm_le).symm
+  rw [hcast]
+  simp only [GasConstants.Gverylow]
+  have hmec_le : (↑(cm17 - cmmu) : SortInt) ≤ GAS_CELL := by
+    rw [← hcast, ← eq18, ← eq19, eq20]; exact hmec_le_gas
+  have h3_le : (3 : SortInt) ≤ GAS_CELL - ↑(cm17 - cmmu) := by
+    rw [← hcast, ← eq18, ← eq19, eq20, ← eq22]; exact hgvl_le
+  rw [intMap_sub_dist h3_le (by norm_num) (by linarith)]
+  rw [intMap_sub_dist hmec_le (Int.natCast_nonneg _) gavailSmall]
+  simp [intMap, UInt256.toSigned]
+
+/-- Derives the memory expansion cost inequality `_Val20 ≤ GAS_CELL` and
+    the Gverylow inequality `_Val22 ≤ GAS_CELL - _Val20` from the KEVM `req` flag. -/
+private theorem gas_bounds_from_req
+  {GAS_CELL MEMORYUSED_CELL W0 _Val0 _Val1 _Val10 _Val17 _Val18 _Val19 _Val2 _Val20 _Val21 _Val22 _Val3 _Val5 _Val6 _Val7 _Val8 _Val9 : SortInt}
+  {SCHEDULE_CELL : SortSchedule}
+  {USEGAS_CELL _Val11 _Val12 _Val13 _Val4 : SortBool}
+  (defn_Val0 : «#memoryUsageUpdate» MEMORYUSED_CELL W0 32 = some _Val0)
+  (defn_Val1 : Cmem SCHEDULE_CELL _Val0 = some _Val1)
+  (defn_Val2 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val2)
+  (defn_Val3 : «_-Int_» _Val1 _Val2 = some _Val3)
+  (defn_Val4 : «_<=Int_» _Val3 GAS_CELL = some _Val4)
+  (defn_Val5 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val5)
+  (defn_Val6 : «#memoryUsageUpdate» MEMORYUSED_CELL W0 32 = some _Val6)
+  (defn_Val7 : Cmem SCHEDULE_CELL _Val6 = some _Val7)
+  (defn_Val8 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val8)
+  (defn_Val9 : «_-Int_» _Val7 _Val8 = some _Val9)
+  (defn_Val10 : «_-Int_» GAS_CELL _Val9 = some _Val10)
+  (defn_Val11 : «_<=Int_» _Val5 _Val10 = some _Val11)
+  (defn_Val12 : _andBool_ _Val4 _Val11 = some _Val12)
+  (defn_Val13 : _andBool_ USEGAS_CELL _Val12 = some _Val13)
+  (defn_Val17 : «#memoryUsageUpdate» MEMORYUSED_CELL W0 32 = some _Val17)
+  (defn_Val18 : Cmem SCHEDULE_CELL _Val17 = some _Val18)
+  (defn_Val19 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val19)
+  (defn_Val20 : «_-Int_» _Val18 _Val19 = some _Val20)
+  (defn_Val21 : «_-Int_» GAS_CELL _Val20 = some _Val21)
+  (defn_Val22 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val22)
+  (req : _Val13 = true)
+  (_cancun : SCHEDULE_CELL = .CANCUN_EVM) :
+  _Val20 ≤ GAS_CELL ∧ _Val22 ≤ GAS_CELL - _Val20 := by
+  have hbool13 : USEGAS_CELL = true ∧ _Val12 = true := by
+    have h := defn_Val13; simp [andBool_def] at h; rw [← h] at req; exact Bool.and_eq_true_iff.mp req
+  have hbool12 : _Val4 = true ∧ _Val11 = true := by
+    have h := defn_Val12; simp [andBool_def] at h; rw [← h] at hbool13; exact Bool.and_eq_true_iff.mp hbool13.2
+  have eq_0_17 : _Val0 = _Val17 := Option.some.inj (defn_Val0.symm.trans defn_Val17)
+  have eq_1_18 : _Val1 = _Val18 := by
+    have h := defn_Val1; rw [eq_0_17] at h; exact Option.some.inj (h.symm.trans defn_Val18)
+  have eq_2_19 : _Val2 = _Val19 := Option.some.inj (defn_Val2.symm.trans defn_Val19)
+  have eq_3_20 : _Val3 = _Val20 := by
+    have h3 := defn_Val3; have h20 := defn_Val20
+    simp [«_-Int_»] at h3 h20; rw [← h3, ← h20, eq_1_18, eq_2_19]
+  have eq_6_17 : _Val6 = _Val17 := Option.some.inj (defn_Val6.symm.trans defn_Val17)
+  have eq_7_18 : _Val7 = _Val18 := by
+    have h := defn_Val7; rw [eq_6_17] at h; exact Option.some.inj (h.symm.trans defn_Val18)
+  have eq_8_19 : _Val8 = _Val19 := Option.some.inj (defn_Val8.symm.trans defn_Val19)
+  have eq_9_20 : _Val9 = _Val20 := by
+    have h9 := defn_Val9; have h20 := defn_Val20
+    simp [«_-Int_»] at h9 h20; rw [← h9, ← h20, eq_7_18, eq_8_19]
+  have eq_5_22 : _Val5 = _Val22 := Option.some.inj (defn_Val5.symm.trans defn_Val22)
+  have eq_10_21 : _Val10 = _Val21 := by
+    have h10 := defn_Val10; have h21 := defn_Val21
+    simp [«_-Int_»] at h10 h21; rw [← h10, ← h21, eq_9_20]
+  have hmec_le_gas : _Val3 ≤ GAS_CELL := by
+    simp [«_<=Int_»] at defn_Val4; rw [← defn_Val4] at hbool12
+    exact of_decide_eq_true hbool12.1
+  have hgvl_le : _Val5 ≤ _Val10 := by
+    simp [«_<=Int_»] at defn_Val11; rw [← defn_Val11] at hbool12
+    exact of_decide_eq_true hbool12.2
+  constructor
+  · rw [eq_3_20] at hmec_le_gas; exact hmec_le_gas
+  · rw [← eq_5_22]
+    rw [eq_10_21] at hgvl_le
+    have h21 : _Val21 = GAS_CELL - _Val20 := by
+      simp [«_-Int_»] at defn_Val21; exact defn_Val21.symm
+    linarith
+
 theorem EVM.step_mload_equiv
   {GAS_CELL MEMORYUSED_CELL PC_CELL W0 _Val0 _Val1 _Val10 _Val15 _Val16 _Val17 _Val18 _Val19 _Val2 _Val20 _Val21 _Val22 _Val23 _Val24 _Val3 _Val5 _Val6 _Val7 _Val8 _Val9 : SortInt}
   {LOCALMEM_CELL _Val14 : SortBytes}
@@ -611,16 +806,151 @@ theorem X_mload_equiv
   simp [mloadLHS, mloadRHS]; rw [pc_equiv, X_mload_summary] <;> try assumption
   . simp; constructor <;> try constructor <;> try constructor
     . -- The deducted amount of gas coincides
-      sorry
+      -- Use the gas_cost_X_mload_equiv helper with bounds extracted from `req`.
+      have ⟨hmec, hgvl⟩ := gas_bounds_from_req defn_Val0 defn_Val1 defn_Val2 defn_Val3 defn_Val4
+        defn_Val5 defn_Val6 defn_Val7 defn_Val8 defn_Val9 defn_Val10 defn_Val11 defn_Val12 defn_Val13
+        defn_Val17 defn_Val18 defn_Val19 defn_Val20 defn_Val21 defn_Val22 req cancun
+      exact gas_cost_X_mload_equiv defn_Val17 defn_Val18 defn_Val19 defn_Val20 defn_Val21 defn_Val22
+        defn_Val23 cancun gavailSmall W0ge0 W0small mucge0 mucsmall W0small_realpolitik hmec hgvl
     . have := MstoreOpcodeEquivalence.activeWords_eq .mstore defn_Val24
       rw [MloadSummary.activeWords_comp]; aesop
     . rw [←UInt256.add_succ_mod_size, intMap_add_dist] <;> aesop
     . simp [MachineState.lookupMemory]
       apply range_lookupMemory_eq defn_Val14 defn_Val15 <;> aesop
   . -- There is enough gas
-    sorry
+    -- X_mload_summary now requires `3 ≤` (non-strict), matching the KEVM hypothesis.
+    -- Extract the KEVM gas sufficiency inequality from `req`
+    have h13 : _Val13 = (USEGAS_CELL && _Val12) := by
+      simp [andBool_def] at defn_Val13; exact defn_Val13.symm
+    rw [h13] at req
+    have huse : USEGAS_CELL = true := by cases USEGAS_CELL <;> simp_all
+    have h12t : _Val12 = true := by cases USEGAS_CELL <;> cases _Val12 <;> simp_all
+    have h12 : _Val12 = (_Val4 && _Val11) := by
+      simp [andBool_def] at defn_Val12; exact defn_Val12.symm
+    rw [h12] at h12t
+    have h4t : _Val4 = true := by cases _Val4 <;> simp_all
+    have h11t : _Val11 = true := by cases _Val4 <;> cases _Val11 <;> simp_all
+    have hv5 : _Val5 = 3 := by
+      rw [cancun] at defn_Val5; simp [GasInterface.cancun_def] at defn_Val5; exact defn_Val5.symm
+    have hv10 : _Val10 = GAS_CELL - _Val9 := by
+      simp [«_-Int_»] at defn_Val10; exact defn_Val10.symm
+    have hleq : _Val5 ≤ _Val10 := by
+      simp [«_<=Int_»] at defn_Val11
+      rw [← defn_Val11] at h11t
+      exact decide_eq_true_eq.mp h11t
+    rw [hv5, hv10] at hleq
+    have hv9 : _Val9 = _Val7 - _Val8 := by
+      simp [«_-Int_»] at defn_Val9; exact defn_Val9.symm
+    rw [hv9] at hleq
+    have hv3_le_gas : _Val3 ≤ GAS_CELL := by
+      simp [«_<=Int_»] at defn_Val4
+      rw [← defn_Val4] at h4t
+      exact decide_eq_true_eq.mp h4t
+    have hv3_eq : _Val3 = _Val1 - _Val2 := by
+      simp [«_-Int_»] at defn_Val3; exact defn_Val3.symm
+    -- _Val1 = _Val7, _Val2 = _Val8 because they compute the same Cmem on the same args
+    have hv0 : _Val0 = MEMORYUSED_CELL ⊔ Int.tdiv (W0 + 32 + 31) 32 := by
+      have := memoryUsageUpdate_rw MEMORYUSED_CELL W0 32 (by omega : (0 : Int) < 32)
+      rw [this] at defn_Val0; simp at defn_Val0; exact defn_Val0.symm
+    have hv6 : _Val6 = MEMORYUSED_CELL ⊔ Int.tdiv (W0 + 32 + 31) 32 := by
+      have := memoryUsageUpdate_rw MEMORYUSED_CELL W0 32 (by omega : (0 : Int) < 32)
+      rw [this] at defn_Val6; simp at defn_Val6; exact defn_Val6.symm
+    have hv0_eq_v6 : _Val0 = _Val6 := by rw [hv0, hv6]
+    have hv1_eq_v7 : _Val1 = _Val7 := by
+      have h1 : Cmem SCHEDULE_CELL _Val0 = some _Val1 := defn_Val1
+      have h7 : Cmem SCHEDULE_CELL _Val6 = some _Val7 := defn_Val7
+      rw [hv0_eq_v6] at h1; rw [h1] at h7; simp at h7; exact h7
+    have hv2_eq_v8 : _Val2 = _Val8 := by
+      have h2 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val2 := defn_Val2
+      have h8 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val8 := defn_Val8
+      rw [h2] at h8; simp at h8; exact h8
+    have hv3_eq_v9 : _Val3 = _Val7 - _Val8 := by
+      rw [hv3_eq, hv1_eq_v7, hv2_eq_v8]
+    rw [hv3_eq_v9] at hv3_le_gas
+    rw [GasConstants.Gverylow]
+    have hgas_nat : (intMap GAS_CELL).toNat = Int.toNat GAS_CELL :=
+      intMap_toNat (le_of_lt gavailEnough) gavailSmall
+    rw [hgas_nat]
+    simp only [EVM.memoryExpansionCost, EVM.memoryExpansionCost.μᵢ', EVM.Cₘ,
+               EVM.Cₘ.QuadraticCeofficient, GasConstants.Gmemory, MachineState.M]
+    have hstack0 : (intMap W0 :: wordStackMap _WS)[0]!.toNat = (intMap W0).toNat := rfl
+    simp only [hstack0]
+    set aw := (intMap MEMORYUSED_CELL).toNat with haw_def
+    set w0 := (intMap W0).toNat with hw0_def
+    set m := max aw ((w0 + 32 + 31) / 32) with hm_def
+    have hm_bound : m < UInt256.size := by
+      simp only [hm_def, Nat.max_def]; split
+      · have hw0_small : w0 < UInt32.size := by
+          rw [hw0_def, intMap_toNat W0ge0 W0small]
+          exact (Int.toNat_lt W0ge0).mpr W0small_realpolitik
+        simp [UInt32.size, UInt256.size] at hw0_small ⊢; omega
+      · exact (intMap MEMORYUSED_CELL).val.isLt
+    rw [UInt256.ofNat_toNat hm_bound]
+    have cmem_cancun : ∀ n : SortInt, Cmem .CANCUN_EVM n = some (n * 3 + Int.tdiv (n * n) 512) := by
+      intro n; simp only [Cmem, GAS_FEES_Cmem]
+      simp only [GasInterface.cancun_def, «_*Int_», «_/Int_», «_+Int_»]; simp
+    rw [cancun] at defn_Val7 defn_Val8
+    rw [cmem_cancun] at defn_Val7 defn_Val8
+    simp only [Option.some.injEq] at defn_Val7 defn_Val8
+    have haw_int : aw = Int.toNat MEMORYUSED_CELL := by
+      rw [haw_def, intMap_toNat mucge0 mucsmall]
+    have hw0_int : w0 = Int.toNat W0 := by
+      rw [hw0_def, intMap_toNat W0ge0 W0small]
+    have hv6_ge_muc : MEMORYUSED_CELL ≤ _Val6 := by rw [hv6]; exact le_max_left _ _
+    have hv6_nonneg : 0 ≤ _Val6 := le_trans mucge0 hv6_ge_muc
+    have hm_ge_aw : aw ≤ m := le_max_left _ _
+    have evm_cost_sub_ok : 3 * aw + aw * aw / 512 ≤ 3 * m + m * m / 512 := by
+      have : aw * aw / 512 ≤ m * m / 512 := Nat.div_le_div_right (Nat.mul_le_mul hm_ge_aw hm_ge_aw)
+      omega
+    have hm_eq_v6 : (m : ℤ) = _Val6 := by
+      rw [hm_def, hv6, haw_int, hw0_int]
+      simp only [Nat.cast_max, Int.natCast_div, Int.toNat_of_nonneg mucge0]
+      congr 1
+      rw [show ((Int.toNat W0 + 32 + 31 : ℕ) : ℤ) = W0 + 32 + 31 from by push_cast; rw [Int.toNat_of_nonneg W0ge0]]
+      rw [Int.tdiv_eq_ediv_of_nonneg (by linarith : 0 ≤ W0 + 32 + 31)]; norm_cast
+    have haw_eq : (aw : ℤ) = MEMORYUSED_CELL := by
+      rw [haw_int]; exact Int.toNat_of_nonneg mucge0
+    have hcm_m : (↑(3 * m + m * m / 512) : ℤ) = _Val7 := by
+      push_cast [Int.natCast_div]
+      rw [hm_eq_v6, ← defn_Val7]
+      rw [Int.tdiv_eq_ediv_of_nonneg (mul_self_nonneg _Val6)]
+      ring
+    have hcm_aw : (↑(3 * aw + aw * aw / 512) : ℤ) = _Val8 := by
+      push_cast [Int.natCast_div]
+      rw [haw_eq, ← defn_Val8]
+      rw [Int.tdiv_eq_ediv_of_nonneg (mul_self_nonneg MEMORYUSED_CELL)]
+      ring
+    have evm_cost_int : ↑(3 * m + m * m / 512 - (3 * aw + aw * aw / 512)) = _Val7 - _Val8 := by
+      rw [Nat.cast_sub evm_cost_sub_ok, hcm_m, hcm_aw]
+    have : (3 : ℤ) ≤ GAS_CELL - ↑(3 * m + m * m / 512 - (3 * aw + aw * aw / 512)) := by
+      linarith [evm_cost_int]
+    omega
   . -- Gas doesn't overflow
-    sorry
+    simp only [EVM.memoryExpansionCost, EVM.Cₘ, EVM.memoryExpansionCost.μᵢ', MachineState.M]
+    simp only [GasConstants.Gmemory, EVM.Cₘ.QuadraticCeofficient, UInt256.size]
+    have hw0 : (intMap W0).toNat < UInt32.size := by
+      rw [intMap_toNat W0ge0 W0small]; exact (Int.toNat_lt W0ge0).mpr W0small_realpolitik
+    have haw : (intMap MEMORYUSED_CELL).toNat < UInt256.size := (intMap MEMORYUSED_CELL).val.isLt
+    set aw := (intMap MEMORYUSED_CELL).toNat
+    set w0 := (intMap W0).toNat
+    set m := max aw ((w0 + 32 + 31) / 32)
+    have hm_bound : m < UInt256.size := by
+      simp only [m, Nat.max_def]; split
+      · simp [UInt32.size, UInt256.size] at hw0 ⊢; omega
+      · exact haw
+    have hstack : (intMap W0 :: wordStackMap _WS)[0]!.toNat = w0 := by rfl
+    rw [hstack]
+    have : m = max aw ((w0 + 32 + 31) / 32) := rfl
+    have hmu : (UInt256.ofNat m).toNat = m := UInt256.ofNat_toNat hm_bound
+    rw [hmu]
+    simp only [m, Nat.max_def] at hmu ⊢
+    split
+    · -- aw ≤ (w0+63)/32, so m = (w0+63)/32 which is small
+      have hb : (w0 + 32 + 31) / 32 < 134217730 := by simp [UInt32.size] at hw0; omega
+      apply Nat.lt_of_le_of_lt (Nat.sub_le _ _)
+      nlinarith [Nat.div_le_self ((w0 + 32 + 31) / 32 * ((w0 + 32 + 31) / 32)) 512]
+    · -- aw > (w0+63)/32, so m = aw and Cm(m) - Cm(aw) = 0
+      omega
 
 
 
diff --git a/EvmEquivalence/Equivalence/MstoreEquivalence.lean b/EvmEquivalence/Equivalence/MstoreEquivalence.lean
index 428f8a9..e193aad 100644
--- a/EvmEquivalence/Equivalence/MstoreEquivalence.lean
+++ b/EvmEquivalence/Equivalence/MstoreEquivalence.lean
@@ -542,6 +542,167 @@ theorem step_mstore_equiv
       -- `rw [mstore8_memory_write_eq defn_Val14 defn_Val15 defn_Val16] <;> assumption`
   . rw [←UInt256.add_succ_mod_size, intMap_add_dist] <;> aesop
 
+private theorem mec_ceil_bound (f l : ℕ) (hf : f < UInt32.size) (hl : l ≤ 32) :
+    (f + l + 31) / 32 ≤ 134217730 := by
+  have : UInt32.size = 4294967296 := rfl
+  have : f + l + 31 ≤ 4294967358 := by omega
+  exact Nat.le_trans (Nat.div_le_div_right this) (by norm_num)
+
+private theorem mec_M_bound (s f l : ℕ) (hf : f < UInt32.size) (hl : l ≤ 32) :
+    MachineState.M s f l ≤ Nat.max s 134217730 := by
+  unfold MachineState.M
+  cases l with
+  | zero => simp
+  | succ n =>
+    have hceil : (f + (n + 1) + 31) / 32 ≤ 134217730 :=
+      mec_ceil_bound f (n + 1) hf (by omega)
+    exact max_le_max_left s hceil
+
+private theorem mec_Cm_bound_const : EVM.Cₘ (UInt256.ofNat 134217730) < UInt256.size := by
+  native_decide
+
+private theorem mec_Cm_mono (a b : UInt256) (h : a.toNat ≤ b.toNat) :
+    EVM.Cₘ a ≤ EVM.Cₘ b := by
+  simp [EVM.Cₘ, EVM.Cₘ.QuadraticCeofficient]
+  have h1 : GasConstants.Gmemory * a.toNat ≤ GasConstants.Gmemory * b.toNat :=
+    Nat.mul_le_mul_left _ h
+  have h2 : a.toNat * a.toNat / 512 ≤ b.toNat * b.toNat / 512 :=
+    Nat.div_le_div_right (Nat.mul_le_mul h h)
+  omega
+
+/-- Connects the KEVM `Cmem` function on the CANCUN schedule to the EVM `Cₘ` function. -/
+private theorem Cmem_cancun_eq_Cm (N : SortInt) (hN : 0 ≤ N) (hNs : N < ↑UInt256.size) :
+    Cmem .CANCUN_EVM N = some ↑(EVM.Cₘ (intMap N)) := by
+  simp [Cmem, GAS_FEES_Cmem, «_*Int_», «_/Int_», «_+Int_», GasInterface.cancun_def]
+  simp [EVM.Cₘ, EVM.Cₘ.QuadraticCeofficient, GasConstants.Gmemory]
+  rw [intMap_toNat hN hNs]
+  cases N with
+  | ofNat n =>
+    simp [Int.toNat]
+    conv_lhs => rw [show (↑n * ↑n : Int) = ↑(n * n) from by push_cast; ring]
+    rw [show Int.tdiv ↑(n * n) (512 : Int) = ↑(n * n / 512) from Int.ofNat_tdiv _ _]
+    push_cast; ring
+  | negSucc n =>
+    exfalso; exact absurd hN (by simp)
+
+private theorem vawg_eq_intMap
+  {MEMORYUSED_CELL W0 _Val18 : SortInt}
+  (defn_Val18 : «#memoryUsageUpdate» MEMORYUSED_CELL W0 op.to_width = some _Val18)
+  (W0ge0 : 0 ≤ W0) (W0small : W0 < ↑UInt256.size)
+  (mucge0 : 0 ≤ MEMORYUSED_CELL) (mucsmall : MEMORYUSED_CELL < ↑UInt256.size) :
+  value_and_activeWords_gas op.from_k (intMap W0) (intMap MEMORYUSED_CELL) = intMap _Val18 := by
+  have aw := activeWords_eq op defn_Val18 W0ge0 W0small mucge0 mucsmall
+  simp [value_and_activeWords_gas, activeWords_comp, MachineState.M] at aw ⊢
+  cases op <;> simp [MstoreOpcodeEquivalence.mstore_op.from_k, mstore_op.to_l,
+    MstoreOpcodeEquivalence.mstore_op.to_width] at aw ⊢ <;> exact aw
+
+private theorem memUsageUpdate_nonneg
+  {MEMORYUSED_CELL W0 _Val18 : SortInt}
+  (defn_Val18 : «#memoryUsageUpdate» MEMORYUSED_CELL W0 op.to_width = some _Val18)
+  (mucge0 : 0 ≤ MEMORYUSED_CELL) :
+  0 ≤ _Val18 := by
+  have hw : (0 : SortInt) < op.to_width := by cases op <;> simp [MstoreOpcodeEquivalence.mstore_op.to_width] <;> omega
+  rw [memoryUsageUpdate_rw _ _ _ hw, Option.some.injEq] at defn_Val18
+  subst defn_Val18
+  exact le_sup_of_le_left mucge0
+
+private theorem memUsageUpdate_small
+  {MEMORYUSED_CELL W0 _Val18 : SortInt}
+  (defn_Val18 : «#memoryUsageUpdate» MEMORYUSED_CELL W0 op.to_width = some _Val18)
+  (W0ge0 : 0 ≤ W0)
+  (mucsmall : MEMORYUSED_CELL < ↑UInt256.size)
+  (W0small_realpolitik : W0 < ↑UInt32.size) :
+  _Val18 < ↑UInt256.size := by
+  have hw_pos : (0 : SortInt) < op.to_width := by
+    cases op <;> simp [MstoreOpcodeEquivalence.mstore_op.to_width]
+  have hw_le : (op.to_width : SortInt) ≤ 32 := by
+    cases op <;> simp [MstoreOpcodeEquivalence.mstore_op.to_width]
+  rw [memoryUsageUpdate_rw _ _ _ hw_pos, Option.some.injEq] at defn_Val18
+  subst defn_Val18
+  have hsum_nonneg : 0 ≤ W0 + ↑op.to_width + 31 := by linarith
+  have hceil_le : Int.tdiv (W0 + ↑op.to_width + 31) 32 ≤ W0 + ↑op.to_width + 31 :=
+    Int.tdiv_le_self 32 hsum_nonneg
+  have hsum_bound : W0 + ↑op.to_width + 31 < ↑UInt256.size := by
+    have : (UInt256.size : ℤ) = 115792089237316195423570985008687907853269984665640564039457584007913129639936 := by
+      simp [UInt256.size]
+    have : (UInt32.size : ℤ) = 4294967296 := by simp [UInt32.size]
+    linarith
+  exact max_lt mucsmall (lt_of_le_of_lt hceil_le hsum_bound)
+
+/-- Proves the gas correctness goal in `X_mstore_equiv`: the KEVM gas chain
+    (Cmem subtractions via `_-Int_`) equals the EVM `memoryExpansionCost` (via `Cₘ`). -/
+private theorem gas_cost_X_equiv
+  {GAS_CELL MEMORYUSED_CELL W0 _Val18 _Val19 _Val20 _Val21 _Val22 _Val23 _Val24 : SortInt}
+  {SCHEDULE_CELL : SortSchedule}
+  (defn_Val18 : «#memoryUsageUpdate» MEMORYUSED_CELL W0 op.to_width = some _Val18)
+  (defn_Val19 : Cmem SCHEDULE_CELL _Val18 = some _Val19)
+  (defn_Val20 : Cmem SCHEDULE_CELL MEMORYUSED_CELL = some _Val20)
+  (defn_Val21 : «_-Int_» _Val19 _Val20 = some _Val21)
+  (defn_Val22 : «_-Int_» GAS_CELL _Val21 = some _Val22)
+  (defn_Val23 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst SCHEDULE_CELL = some _Val23)
+  (defn_Val24 : «_-Int_» _Val22 _Val23 = some _Val24)
+  (cancun : SCHEDULE_CELL = .CANCUN_EVM)
+  (gavailSmall : GAS_CELL < ↑UInt256.size)
+  (W0ge0 : 0 ≤ W0) (W0small : W0 < ↑UInt256.size)
+  (mucge0 : 0 ≤ MEMORYUSED_CELL) (mucsmall : MEMORYUSED_CELL < ↑UInt256.size)
+  (W0small_realpolitik : W0 < ↑UInt32.size)
+  (hmec_le_gas : _Val21 ≤ GAS_CELL)
+  (hgvl_le : _Val23 ≤ GAS_CELL - _Val21) :
+  intMap GAS_CELL -
+    UInt256.ofNat (EVM.Cₘ (value_and_activeWords_gas op.from_k (intMap W0) (intMap MEMORYUSED_CELL)) -
+                   EVM.Cₘ (intMap MEMORYUSED_CELL)) -
+    UInt256.ofNat GasConstants.Gverylow = intMap _Val24 := by
+  -- Extract concrete values from the KEVM chain
+  have eq21 : _Val19 - _Val20 = _Val21 := by simp [«_-Int_»] at defn_Val21; exact defn_Val21
+  have eq22 : GAS_CELL - _Val21 = _Val22 := by simp [«_-Int_»] at defn_Val22; exact defn_Val22
+  have eq24 : _Val22 - _Val23 = _Val24 := by simp [«_-Int_»] at defn_Val24; exact defn_Val24
+  have eq23 : _Val23 = 3 := by
+    rw [cancun] at defn_Val23; simp [GasInterface.cancun_def] at defn_Val23; exact defn_Val23.symm
+  -- Compute _Val19, _Val20 via Cmem_cancun_eq_Cm
+  have h18_nn := memUsageUpdate_nonneg op defn_Val18 mucge0
+  have h18_sm := memUsageUpdate_small op defn_Val18 W0ge0 mucsmall W0small_realpolitik
+  have eq19 : _Val19 = ↑(EVM.Cₘ (intMap _Val18)) := by
+    have := Cmem_cancun_eq_Cm _Val18 h18_nn h18_sm
+    rw [cancun] at defn_Val19; rw [this] at defn_Val19
+    exact (Option.some.inj defn_Val19).symm
+  have eq20 : _Val20 = ↑(EVM.Cₘ (intMap MEMORYUSED_CELL)) := by
+    have := Cmem_cancun_eq_Cm MEMORYUSED_CELL mucge0 mucsmall
+    rw [cancun] at defn_Val20; rw [this] at defn_Val20
+    exact (Option.some.inj defn_Val20).symm
+  -- Rewrite value_and_activeWords_gas to intMap _Val18
+  rw [vawg_eq_intMap op defn_Val18 W0ge0 W0small mucge0 mucsmall]
+  -- Cₘ monotonicity: cmmu ≤ cm18
+  have hCm_le : EVM.Cₘ (intMap MEMORYUSED_CELL) ≤ EVM.Cₘ (intMap _Val18) := by
+    apply mec_Cm_mono
+    rw [intMap_toNat mucge0 mucsmall, intMap_toNat h18_nn h18_sm]
+    have hw : (0 : SortInt) < op.to_width := by
+      cases op <;> simp [MstoreOpcodeEquivalence.mstore_op.to_width]
+    have defn18' := defn_Val18
+    rw [memoryUsageUpdate_rw _ _ _ hw] at defn18'
+    have eq18 : _Val18 = MEMORYUSED_CELL ⊔ Int.tdiv (W0 + ↑op.to_width + 31) 32 :=
+      (Option.some.inj defn18').symm
+    rw [eq18]
+    exact Int.toNat_le_toNat (le_max_left _ _)
+  -- Derive _Val24 = GAS_CELL - (↑cm18 - ↑cmmu) - 3
+  have hv24 : _Val24 = GAS_CELL - (↑(EVM.Cₘ (intMap _Val18)) - ↑(EVM.Cₘ (intMap MEMORYUSED_CELL))) - 3 := by
+    rw [← eq24, ← eq22, ← eq21, eq19, eq20, eq23]
+  rw [hv24]
+  -- Introduce names for Cₘ values to help with opaque terms
+  set cm18 := EVM.Cₘ (intMap _Val18) with hcm18_def
+  set cmmu := EVM.Cₘ (intMap MEMORYUSED_CELL) with hcmmu_def
+  -- Simplify ↑cm18 - ↑cmmu = ↑(cm18 - cmmu) using Nat.cast_sub
+  have hcast : (↑cm18 : SortInt) - ↑cmmu = ↑(cm18 - cmmu) := (Nat.cast_sub hCm_le).symm
+  rw [hcast]
+  simp only [GasConstants.Gverylow]
+  -- Bounds for intMap_sub_dist (derived from hmec_le_gas and hgvl_le)
+  have hmec_le : (↑(cm18 - cmmu) : SortInt) ≤ GAS_CELL := by
+    rw [← hcast, ← eq19, ← eq20, eq21]; exact hmec_le_gas
+  have h3_le : (3 : SortInt) ≤ GAS_CELL - ↑(cm18 - cmmu) := by
+    rw [← hcast, ← eq19, ← eq20, eq21, ← eq23]; exact hgvl_le
+  rw [intMap_sub_dist h3_le (by norm_num) (by linarith)]
+  rw [intMap_sub_dist hmec_le (Int.natCast_nonneg _) gavailSmall]
+  simp [intMap, UInt256.toSigned]
+
 theorem X_mstore_equiv
   {GAS_CELL MEMORYUSED_CELL PC_CELL W0 W1 _Val0 _Val1 _Val10 _Val14mstore8 _Val17 _Val18 _Val19 _Val2 _Val20 _Val21 _Val22 _Val23 _Val24 _Val25 _Val3 _Val5 _Val6 _Val7 _Val8 _Val9 : SortInt}
   {LOCALMEM_CELL _Val14mstore _Val15 _Val16 : SortBytes}
@@ -641,9 +802,42 @@ theorem X_mstore_equiv
   simp [mstoreLHS, mstoreRHS]; rw [pc_equiv, X_mstore_summary] <;> try assumption
   . simp; constructor <;> try constructor <;> try constructor
     . -- Gas correctness goal
-      /- rw [memoryExpansionCost_mstore op (wordStackMap WS) (intMap W0) (intMap MEMORYUSED_CELL)]
-      simp [EVM.Cₘ] -/
-      sorry
+      rw [memoryExpansionCost_mstore op.from_k (wordStackMap WS) (intMap W0) (intMap W1) (intMap MEMORYUSED_CELL) _ rfl rfl]
+      -- Derive variable equalities across duplicated KEVM computation chains
+      have eq_0_18 : _Val0 = _Val18 := Option.some.inj (defn_Val0.symm.trans defn_Val18)
+      have eq_1_19 : _Val1 = _Val19 := by
+        have h := defn_Val1; rw [eq_0_18] at h; exact Option.some.inj (h.symm.trans defn_Val19)
+      have eq_2_20 : _Val2 = _Val20 := Option.some.inj (defn_Val2.symm.trans defn_Val20)
+      have eq_3_21 : _Val3 = _Val21 := by
+        have h3 := defn_Val3; have h21 := defn_Val21
+        simp [«_-Int_»] at h3 h21; rw [← h3, ← h21, eq_1_19, eq_2_20]
+      have eq_5_23 : _Val5 = _Val23 := Option.some.inj (defn_Val5.symm.trans defn_Val23)
+      have eq_6_18 : _Val6 = _Val18 := Option.some.inj (defn_Val6.symm.trans defn_Val18)
+      have eq_7_19 : _Val7 = _Val19 := by
+        have h := defn_Val7; rw [eq_6_18] at h; exact Option.some.inj (h.symm.trans defn_Val19)
+      have eq_8_20 : _Val8 = _Val20 := Option.some.inj (defn_Val8.symm.trans defn_Val20)
+      have eq_9_21 : _Val9 = _Val21 := by
+        have h9 := defn_Val9; have h21 := defn_Val21
+        simp [«_-Int_»] at h9 h21; rw [← h9, ← h21, eq_7_19, eq_8_20]
+      have eq_10_22 : _Val10 = _Val22 := by
+        have h10 := defn_Val10; have h22 := defn_Val22
+        simp [«_-Int_»] at h10 h22; rw [← h10, ← h22, eq_9_21]
+      -- Extract gas bounds from `req`
+      have hbool13 : USEGAS_CELL = true ∧ _Val12 = true := by
+        have h := defn_Val13; simp [andBool_def] at h; rw [← h] at req; exact Bool.and_eq_true_iff.mp req
+      have hbool12 : _Val4 = true ∧ _Val11 = true := by
+        have h := defn_Val12; simp [andBool_def] at h; rw [← h] at hbool13; exact Bool.and_eq_true_iff.mp hbool13.2
+      have hmec_le_gas : _Val21 ≤ GAS_CELL := by
+        have h := defn_Val4; simp [«_<=Int_»] at h; rw [← h] at hbool12
+        rw [← eq_3_21]; exact of_decide_eq_true hbool12.1
+      have hgvl_le : _Val23 ≤ GAS_CELL - _Val21 := by
+        have h := defn_Val11; simp [«_<=Int_»] at h; rw [← h] at hbool12
+        have hle : _Val5 ≤ _Val10 := of_decide_eq_true hbool12.2
+        rw [eq_5_23] at hle; rw [eq_10_22] at hle
+        have h22 := defn_Val22; simp [«_-Int_»] at h22
+        linarith
+      exact gas_cost_X_equiv op defn_Val18 defn_Val19 defn_Val20 defn_Val21 defn_Val22 defn_Val23 defn_Val24
+            cancun gavailSmall W0ge0 W0small mucge0 mucsmall W0small_realpolitik hmec_le_gas hgvl_le
     . have aw_rw := activeWords_eq op defn_Val25
       cases op <;> simp [mstore_op.from_k] <;> aesop
     . cases op <;> simp [mstore_op.from_k]
@@ -656,11 +850,124 @@ theorem X_mstore_equiv
       -- `rw [mstore8_memory_write_eq defn_Val14 defn_Val15 defn_Val16] <;> assumption`
     . aesop
   . -- Enough Gas
-    sorry
+    cases op <;> simp [mstore_op.from_k] <;> omega
   . -- Gas is not greater than `UInt256.size`
-    simp [EVM.memoryExpansionCost, EVM.Cₘ, EVM.memoryExpansionCost.μᵢ', MachineState.M]
-    sorry
+    rw [memoryExpansionCost_mstore op.from_k (wordStackMap WS) (intMap W0) (intMap W1) (intMap MEMORYUSED_CELL) _ rfl rfl,
+        vawg_eq_intMap op defn_Val18 W0ge0 W0small mucge0 mucsmall]
+    -- Re-derive variable equalities across duplicated KEVM computation chains
+    have eq_0_18 : _Val0 = _Val18 := Option.some.inj (defn_Val0.symm.trans defn_Val18)
+    have eq_1_19 : _Val1 = _Val19 := by
+      have h := defn_Val1; rw [eq_0_18] at h; exact Option.some.inj (h.symm.trans defn_Val19)
+    have eq_2_20 : _Val2 = _Val20 := Option.some.inj (defn_Val2.symm.trans defn_Val20)
+    have eq_3_21 : _Val3 = _Val21 := by
+      have h3 := defn_Val3; have h21 := defn_Val21
+      simp [«_-Int_»] at h3 h21; rw [← h3, ← h21, eq_1_19, eq_2_20]
+    have eq_5_23 : _Val5 = _Val23 := Option.some.inj (defn_Val5.symm.trans defn_Val23)
+    have eq_6_18 : _Val6 = _Val18 := Option.some.inj (defn_Val6.symm.trans defn_Val18)
+    have eq_7_19 : _Val7 = _Val19 := by
+      have h := defn_Val7; rw [eq_6_18] at h; exact Option.some.inj (h.symm.trans defn_Val19)
+    have eq_8_20 : _Val8 = _Val20 := Option.some.inj (defn_Val8.symm.trans defn_Val20)
+    have eq_9_21 : _Val9 = _Val21 := by
+      have h9 := defn_Val9; have h21 := defn_Val21
+      simp [«_-Int_»] at h9 h21; rw [← h9, ← h21, eq_7_19, eq_8_20]
+    have eq_10_22 : _Val10 = _Val22 := by
+      have h10 := defn_Val10; have h22 := defn_Val22
+      simp [«_-Int_»] at h10 h22; rw [← h10, ← h22, eq_9_21]
+    -- Extract gas bounds from req
+    have hbool13 : USEGAS_CELL = true ∧ _Val12 = true := by
+      have h := defn_Val13; simp [andBool_def] at h; rw [← h] at req; exact Bool.and_eq_true_iff.mp req
+    have hbool12 : _Val4 = true ∧ _Val11 = true := by
+      have h := defn_Val12; simp [andBool_def] at h; rw [← h] at hbool13; exact Bool.and_eq_true_iff.mp hbool13.2
+    have hmec_le_gas : _Val21 ≤ GAS_CELL := by
+      have h := defn_Val4; simp [«_<=Int_»] at h; rw [← h] at hbool12
+      rw [← eq_3_21]; exact of_decide_eq_true hbool12.1
+    have hgvl_le : _Val23 ≤ GAS_CELL - _Val21 := by
+      have h := defn_Val11; simp [«_<=Int_»] at h; rw [← h] at hbool12
+      have hle : _Val5 ≤ _Val10 := of_decide_eq_true hbool12.2
+      rw [eq_5_23] at hle; rw [eq_10_22] at hle
+      have h22 := defn_Val22; simp [«_-Int_»] at h22
+      linarith
+    -- Get _Val23 = 3 (Gverylow for Cancun)
+    have eq23 : _Val23 = 3 := by
+      rw [cancun] at defn_Val23; simp [GasInterface.cancun_def] at defn_Val23; exact defn_Val23.symm
+    -- Connect Cmem to Cₘ
+    have h18_nn := memUsageUpdate_nonneg op defn_Val18 mucge0
+    have h18_sm := memUsageUpdate_small op defn_Val18 W0ge0 mucsmall W0small_realpolitik
+    have eq19 : _Val19 = ↑(EVM.Cₘ (intMap _Val18)) := by
+      have := Cmem_cancun_eq_Cm _Val18 h18_nn h18_sm
+      rw [cancun] at defn_Val19; rw [this] at defn_Val19
+      exact (Option.some.inj defn_Val19).symm
+    have eq20 : _Val20 = ↑(EVM.Cₘ (intMap MEMORYUSED_CELL)) := by
+      have := Cmem_cancun_eq_Cm MEMORYUSED_CELL mucge0 mucsmall
+      rw [cancun] at defn_Val20; rw [this] at defn_Val20
+      exact (Option.some.inj defn_Val20).symm
+    -- Cₘ monotonicity: Cₘ(intMap MEMORYUSED_CELL) ≤ Cₘ(intMap _Val18)
+    have hCm_le : EVM.Cₘ (intMap MEMORYUSED_CELL) ≤ EVM.Cₘ (intMap _Val18) := by
+      apply mec_Cm_mono
+      rw [intMap_toNat mucge0 mucsmall, intMap_toNat h18_nn h18_sm]
+      have hw : (0 : SortInt) < op.to_width := by
+        cases op <;> simp [MstoreOpcodeEquivalence.mstore_op.to_width]
+      have defn18' := defn_Val18
+      rw [memoryUsageUpdate_rw _ _ _ hw] at defn18'
+      have eq18 : _Val18 = MEMORYUSED_CELL ⊔ Int.tdiv (W0 + ↑op.to_width + 31) 32 :=
+        (Option.some.inj defn18').symm
+      rw [eq18]
+      exact Int.toNat_le_toNat (le_max_left _ _)
+    -- _Val21 = ↑(Cₘ(intMap _Val18) - Cₘ(intMap MEMORYUSED_CELL))
+    have eq21_z : _Val21 = ↑(EVM.Cₘ (intMap _Val18)) - ↑(EVM.Cₘ (intMap MEMORYUSED_CELL)) := by
+      have h := defn_Val21; simp [«_-Int_»] at h; rw [← h, eq19, eq20]
+    have h21_nn : 0 ≤ _Val21 := by
+      rw [eq21_z]; exact sub_nonneg.mpr (Nat.cast_le.mpr hCm_le)
+    have hCm_diff : _Val21.toNat = EVM.Cₘ (intMap _Val18) - EVM.Cₘ (intMap MEMORYUSED_CELL) := by
+      rw [eq21_z, show (↑(EVM.Cₘ (intMap _Val18)) - ↑(EVM.Cₘ (intMap MEMORYUSED_CELL)) : ℤ) =
+        ↑(EVM.Cₘ (intMap _Val18) - EVM.Cₘ (intMap MEMORYUSED_CELL)) from (Nat.cast_sub hCm_le).symm]
+      exact Int.toNat_natCast _
+    -- Final: GasConstants.Gverylow ≤ (intMap GAS_CELL).toNat - (Cₘ ... - Cₘ ...)
+    simp only [GasConstants.Gverylow]
+    rw [intMap_toNat (le_of_lt gavailEnough) gavailSmall, ← hCm_diff]
+    -- Goal: 3 ≤ GAS_CELL.toNat - _Val21.toNat
+    have h3_le : 3 ≤ GAS_CELL - _Val21 := by rw [← eq23]; exact hgvl_le
+    have hGAS_nn : 0 ≤ GAS_CELL := le_of_lt gavailEnough
+    have h_sub_nn : 0 ≤ GAS_CELL - _Val21 := by linarith
+    have h_sub_eq : ↑(GAS_CELL - _Val21).toNat = GAS_CELL - _Val21 :=
+      Int.toNat_of_nonneg h_sub_nn
+    have h_gas_eq : ↑GAS_CELL.toNat = GAS_CELL := Int.toNat_of_nonneg hGAS_nn
+    have h_val_eq : ↑_Val21.toNat = _Val21 := Int.toNat_of_nonneg h21_nn
+    have h_sub_nat : (GAS_CELL - _Val21).toNat = GAS_CELL.toNat - _Val21.toNat := by
+      zify [Int.toNat_le_toNat hmec_le_gas]
+      rw [h_sub_eq, h_gas_eq, h_val_eq]
+    have h1 : (3 : ℤ).toNat ≤ (GAS_CELL - _Val21).toNat := Int.toNat_le_toNat h3_le
+    simp at h1
+    linarith
   . -- `memoryExpansionCost < UInt256.size`
-    sorry
+    rw [memoryExpansionCost_mstore op.from_k (wordStackMap WS) (intMap W0) (intMap W1) (intMap MEMORYUSED_CELL) _ rfl rfl]
+    have hoff : (intMap W0).toNat < UInt32.size := by
+      rw [intMap_toNat W0ge0 W0small]
+      exact (Int.toNat_lt_toNat (by linarith : (0 : ℤ) < (↑UInt32.size : ℤ))).mpr W0small_realpolitik
+    have hl : op.from_k.to_l ≤ 32 := by cases op <;> simp [mstore_op.from_k, MstoreSummary.mstore_op.to_l]
+    simp only [value_and_activeWords_gas]
+    have hb := mec_M_bound (intMap MEMORYUSED_CELL).toNat (intMap W0).toNat op.from_k.to_l hoff hl
+    by_cases haw : (intMap MEMORYUSED_CELL).toNat ≤ 134217730
+    · -- aw ≤ bound: M ≤ bound
+      have hM_le : MachineState.M (intMap MEMORYUSED_CELL).toNat (intMap W0).toNat op.from_k.to_l ≤ 134217730 :=
+        le_trans hb (Nat.max_le_of_le_of_le haw (le_refl _))
+      have hM_small : MachineState.M (intMap MEMORYUSED_CELL).toNat (intMap W0).toNat op.from_k.to_l < UInt256.size := by
+        have : UInt256.size = 115792089237316195423570985008687907853269984665640564039457584007913129639936 := rfl; omega
+      have hCm := mec_Cm_mono
+        (UInt256.ofNat (MachineState.M (intMap MEMORYUSED_CELL).toNat (intMap W0).toNat op.from_k.to_l))
+        (UInt256.ofNat 134217730)
+        (by rw [UInt256.ofNat_toNat hM_small, UInt256.ofNat_toNat (by native_decide)]; exact hM_le)
+      have := mec_Cm_bound_const
+      omega
+    · -- aw > bound: M = aw, cost = 0
+      push_neg at haw
+      have hM_eq : MachineState.M (intMap MEMORYUSED_CELL).toNat (intMap W0).toNat op.from_k.to_l = (intMap MEMORYUSED_CELL).toNat := by
+        unfold MachineState.M
+        have hceil := mec_ceil_bound (intMap W0).toNat op.from_k.to_l hoff hl
+        cases op <;> simp [mstore_op.from_k, MstoreSummary.mstore_op.to_l] at hceil ⊢ <;> omega
+      rw [hM_eq]
+      have hrt : (UInt256.ofNat (intMap MEMORYUSED_CELL).toNat) = (intMap MEMORYUSED_CELL) := by
+        simp [UInt256.ofNat, UInt256.toNat]; rfl
+      rw [hrt]; simp [UInt256.size]
 
 end MstoreOpcodeEquivalence
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))
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
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