Skip to content

Fill W1_zero_eq and normalize X summary gas preconditions #41

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
eliasjudin wants to merge 3 commits into from
Closed

Fill W1_zero_eq and normalize X summary gas preconditions #41

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
da20bd0
Fill W1_zero_eq in X_exp_equiv
eliasjudin Feb 25, 2026
c54d5f9
Normalize X_mstore_summary gas precondition
eliasjudin Feb 25, 2026
68de99f
Normalize X_mload_summary gas precondition
eliasjudin Feb 25, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 12 additions & 1 deletion EvmEquivalence/Equivalence/Operations/ExpEquivalence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down
5 changes: 2 additions & 3 deletions EvmEquivalence/Summaries/MloadSummary.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions EvmEquivalence/Summaries/MstoreSummary.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down