Skip to content

Fill W1_zero_eq sorry in X_exp_equiv #40

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 1 commit into from
Closed

Fill W1_zero_eq sorry in X_exp_equiv #40

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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