From fde3c73bbe68061d0f95f091f98b591a0ed77e2e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= Date: Thu, 3 Oct 2024 14:01:41 +0200 Subject: [PATCH 1/7] Inter instance for binary relation To be honest I was kind of surprised I didn't found it in mathlib. Perhaps that is not _idiomatic_ Lean solution? --- Clear/Wheels.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Clear/Wheels.lean b/Clear/Wheels.lean index de70965..c07c533 100644 --- a/Clear/Wheels.lean +++ b/Clear/Wheels.lean @@ -1,7 +1,17 @@ import Aesop +import Mathlib.Data.Rel import Mathlib.Tactic.ApplyAt +instance instRelInter {α β} : Inter (Rel α β) where + inter r s := λ a b ↦ r a b ∧ s a b + +def Rel.inter {α β} (r : α → β → Prop) (s : α → β → Prop) : α → β → Prop := + λ a b ↦ r a b ∧ s a b + +instance instFunInter {α β : Type} : Inter (α → β → Prop) where + inter r s := λ a b ↦ r a b ∧ s a b + declare_aesop_rule_sets [Clear.aesop_ok, Clear.aesop_spec, Clear.aesop_varstore] set_option hygiene false in From 5b717c3bdeffbb454ffe2f4afd0e158e6d32a019 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= Date: Thu, 3 Oct 2024 17:09:12 +0200 Subject: [PATCH 2/7] Preserved, relation for EVM state that mostly stays the same --- Clear/EVMState.lean | 44 ++++++++++++++++++++++++++++++++++++++++++++ Clear/Utilities.lean | 27 +++++++++++++++++++++++++++ 2 files changed, 71 insertions(+) diff --git a/Clear/EVMState.lean b/Clear/EVMState.lean index 96f1092..036a48c 100644 --- a/Clear/EVMState.lean +++ b/Clear/EVMState.lean @@ -3,6 +3,7 @@ import Mathlib.Data.Fin.Basic import Clear.Ast import Clear.Instr import Clear.UInt256 +import Clear.Wheels open Clear Instr UInt256 @@ -163,6 +164,44 @@ instance : Inhabited EVMState := abbrev EVM := EVMState +def preserved : EVMState → EVMState → Prop := + (Eq on EVMState.account_map) ∩ + (Eq on EVMState.hash_collision) ∩ + (Eq on EVMState.execution_env) + +lemma preserved_def {e₀ e₁ : EVM} : preserved e₀ e₁ = + (e₀.account_map = e₁.account_map ∧ + e₀.hash_collision = e₁.hash_collision ∧ + e₀.execution_env = e₁.execution_env) := by + unfold preserved + dsimp [(· ∩ ·)] + simp [Function.onFun, and_assoc] + +def preserves_account_map {evm evm' : EVMState} (h : preserved evm evm') : + evm.account_map = evm'.account_map := h.1.1 + +def preserves_collision {evm evm' : EVMState} (h : preserved evm evm') : + evm.hash_collision = evm'.hash_collision := h.1.2 + +def preserves_execution_env {evm evm' : EVMState} (h : preserved evm evm') : + evm.execution_env = evm'.execution_env := h.2 + +@[simp] +lemma preserved_rfl {e : EVM} : preserved e e := by + rw [preserved_def] + simp + +@[simp] +lemma preserved_trans {e₀ e₁ e₂ : EVM} : + preserved e₀ e₁ → preserved e₁ e₂ → preserved e₀ e₂ := by + rw (config := {occs := .pos [3]}) [preserved_def] + intro h₀ h₁ + have acc := Eq.trans (preserves_account_map h₀) (preserves_account_map h₁) + have col := Eq.trans (preserves_collision h₀) (preserves_collision h₁) + have env := Eq.trans (preserves_execution_env h₀) (preserves_execution_env h₁) + constructor; swap; constructor + all_goals assumption + -- functions for querying balance namespace EVMState @@ -339,6 +378,11 @@ def evm_return (σ : EVMState) (mstart s : UInt256) : EVMState := def evm_revert (σ : EVMState) (mstart s : UInt256) : EVMState := σ.evm_return mstart s +lemma mstore_preserves {evm} {pos val} : preserved evm (evm.mstore pos val) := by + unfold mstore updateMemory + rw [preserved_def] + simp + end end Clear.EVMState diff --git a/Clear/Utilities.lean b/Clear/Utilities.lean index 434a984..4b32e87 100644 --- a/Clear/Utilities.lean +++ b/Clear/Utilities.lean @@ -82,4 +82,31 @@ lemma evm_eq_symm_of_isPure_ok_ok {evm evm'} {vs vs'} (h : isPure (Ok evm vs) (O symm aesop_spec +def preservesEvm (s₀ : State) (s₁ : State) : Prop := + match s₀, s₁ with + | .Ok e₀ _, .Ok e₁ _ => preserved e₀ e₁ + | _, _ => True + +@[simp] +lemma preservesEvm_rfl {s : State} : preservesEvm s s := by + unfold preservesEvm + cases s <;> simp + +@[simp] +lemma preservesEvm_trans {s₀ s₁ s₂} (h : s₁.isOk) : + preservesEvm s₀ s₁ → preservesEvm s₁ s₂ → preservesEvm s₀ s₂ := by + unfold preservesEvm + cases s₀ <;> cases s₁ <;> cases s₂ <;> simp_all + exact preserved_trans + +lemma sload_eq_of_preservesEvm + {s s' : State} {a : UInt256} (h : s.isOk) (h' : s'.isOk) (hss : preservesEvm s s') : + s.evm.sload a = s'.evm.sload a := by + cases s <;> cases s' <;> simp_all + simp only [evm] + unfold EVMState.sload EVMState.lookupAccount + rw [ preserves_account_map hss + , preserves_execution_env hss + ] + end Clear.Utilities From 0b98838e5f7442961c29f925d9ac9c98ec0e3941 Mon Sep 17 00:00:00 2001 From: Daniel Britten Date: Thu, 3 Oct 2024 19:30:00 +1300 Subject: [PATCH 3/7] Add `keccak_map` to `preserved` relation --- Clear/EVMState.lean | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/Clear/EVMState.lean b/Clear/EVMState.lean index 036a48c..5150ef4 100644 --- a/Clear/EVMState.lean +++ b/Clear/EVMState.lean @@ -167,24 +167,29 @@ abbrev EVM := EVMState def preserved : EVMState → EVMState → Prop := (Eq on EVMState.account_map) ∩ (Eq on EVMState.hash_collision) ∩ - (Eq on EVMState.execution_env) + (Eq on EVMState.execution_env) ∩ + (Eq on EVMState.keccak_map) lemma preserved_def {e₀ e₁ : EVM} : preserved e₀ e₁ = (e₀.account_map = e₁.account_map ∧ e₀.hash_collision = e₁.hash_collision ∧ - e₀.execution_env = e₁.execution_env) := by + e₀.execution_env = e₁.execution_env ∧ + e₀.keccak_map = e₁.keccak_map) := by unfold preserved dsimp [(· ∩ ·)] simp [Function.onFun, and_assoc] def preserves_account_map {evm evm' : EVMState} (h : preserved evm evm') : - evm.account_map = evm'.account_map := h.1.1 + evm.account_map = evm'.account_map := h.1.1.1 def preserves_collision {evm evm' : EVMState} (h : preserved evm evm') : - evm.hash_collision = evm'.hash_collision := h.1.2 + evm.hash_collision = evm'.hash_collision := h.1.1.2 def preserves_execution_env {evm evm' : EVMState} (h : preserved evm evm') : - evm.execution_env = evm'.execution_env := h.2 + evm.execution_env = evm'.execution_env := h.1.2 + +def preserves_keccak_map {evm evm' : EVMState} (h : preserved evm evm') : + evm.keccak_map = evm'.keccak_map := h.2 @[simp] lemma preserved_rfl {e : EVM} : preserved e e := by @@ -199,7 +204,8 @@ lemma preserved_trans {e₀ e₁ e₂ : EVM} : have acc := Eq.trans (preserves_account_map h₀) (preserves_account_map h₁) have col := Eq.trans (preserves_collision h₀) (preserves_collision h₁) have env := Eq.trans (preserves_execution_env h₀) (preserves_execution_env h₁) - constructor; swap; constructor + have kec := Eq.trans (preserves_keccak_map h₀) (preserves_keccak_map h₁) + constructor; swap; constructor; swap; constructor all_goals assumption -- functions for querying balance From ffb62e4b4a1ab40f8b378554b7c5c2904dd98ecf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= Date: Fri, 4 Oct 2024 12:33:44 +0200 Subject: [PATCH 4/7] Some more lemmas about preserving EVM --- Clear/EVMState.lean | 9 +++++++++ Clear/Utilities.lean | 17 +++++++++++++++++ 2 files changed, 26 insertions(+) diff --git a/Clear/EVMState.lean b/Clear/EVMState.lean index 5150ef4..21cf16a 100644 --- a/Clear/EVMState.lean +++ b/Clear/EVMState.lean @@ -196,6 +196,15 @@ lemma preserved_rfl {e : EVM} : preserved e e := by rw [preserved_def] simp +lemma preserved_symm {e₀ e₁ : EVM} : preserved e₀ e₁ = preserved e₁ e₀ := by + rw [preserved_def, preserved_def] + ext + apply Iff.intro <;> { + intro ⟨acc, col, env, kec⟩ + symm at acc col env kec + exact ⟨acc, col, env, kec⟩ + } + @[simp] lemma preserved_trans {e₀ e₁ e₂ : EVM} : preserved e₀ e₁ → preserved e₁ e₂ → preserved e₀ e₂ := by diff --git a/Clear/Utilities.lean b/Clear/Utilities.lean index 4b32e87..12c66d6 100644 --- a/Clear/Utilities.lean +++ b/Clear/Utilities.lean @@ -87,6 +87,17 @@ def preservesEvm (s₀ : State) (s₁ : State) : Prop := | .Ok e₀ _, .Ok e₁ _ => preserved e₀ e₁ | _, _ => True +lemma preservesEvm_of_isOk {s₀ s₁ : State} (s₀_ok : s₀.isOk) (s₁_ok : s₁.isOk) : + preservesEvm s₀ s₁ → + (s₀.evm.account_map = s₁.evm.account_map ∧ + s₀.evm.hash_collision = s₁.evm.hash_collision ∧ + s₀.evm.execution_env = s₁.evm.execution_env ∧ + s₀.evm.keccak_map = s₁.evm.keccak_map) := by + unfold preservesEvm + cases s₀ <;> cases s₁ <;> simp at * + rw [preserved_def] + intro _; assumption + @[simp] lemma preservesEvm_rfl {s : State} : preservesEvm s s := by unfold preservesEvm @@ -99,6 +110,12 @@ lemma preservesEvm_trans {s₀ s₁ s₂} (h : s₁.isOk) : cases s₀ <;> cases s₁ <;> cases s₂ <;> simp_all exact preserved_trans +lemma preservesEvm_eq (s₀ : State) (s₁ : State) : + preserved s₀.evm s₁.evm → preservesEvm s₀ s₁ := by + unfold preservesEvm + cases s₀ <;> cases s₁ <;> simp + simp [evm] + lemma sload_eq_of_preservesEvm {s s' : State} {a : UInt256} (h : s.isOk) (h' : s'.isOk) (hss : preservesEvm s s') : s.evm.sload a = s'.evm.sload a := by From dd00c5585b8a2706b93641f039af069399cb0ab7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= Date: Mon, 7 Oct 2024 22:31:03 +0200 Subject: [PATCH 5/7] Remove Inter instance --- Clear/EVMState.lean | 27 +++++++++++++++++---------- Clear/Wheels.lean | 10 ---------- 2 files changed, 17 insertions(+), 20 deletions(-) diff --git a/Clear/EVMState.lean b/Clear/EVMState.lean index 21cf16a..c61a9d5 100644 --- a/Clear/EVMState.lean +++ b/Clear/EVMState.lean @@ -165,10 +165,10 @@ instance : Inhabited EVMState := abbrev EVM := EVMState def preserved : EVMState → EVMState → Prop := - (Eq on EVMState.account_map) ∩ - (Eq on EVMState.hash_collision) ∩ - (Eq on EVMState.execution_env) ∩ - (Eq on EVMState.keccak_map) + λ a b ↦ (Eq on EVMState.account_map) a b ∧ + (Eq on EVMState.hash_collision) a b ∧ + (Eq on EVMState.execution_env) a b ∧ + (Eq on EVMState.keccak_map) a b lemma preserved_def {e₀ e₁ : EVM} : preserved e₀ e₁ = (e₀.account_map = e₁.account_map ∧ @@ -176,20 +176,27 @@ lemma preserved_def {e₀ e₁ : EVM} : preserved e₀ e₁ = e₀.execution_env = e₁.execution_env ∧ e₀.keccak_map = e₁.keccak_map) := by unfold preserved - dsimp [(· ∩ ·)] - simp [Function.onFun, and_assoc] + dsimp def preserves_account_map {evm evm' : EVMState} (h : preserved evm evm') : - evm.account_map = evm'.account_map := h.1.1.1 + evm.account_map = evm'.account_map := by + rw [preserved_def] at h + exact h.1 def preserves_collision {evm evm' : EVMState} (h : preserved evm evm') : - evm.hash_collision = evm'.hash_collision := h.1.1.2 + evm.hash_collision = evm'.hash_collision := by + rw [preserved_def] at h + exact h.2.1 def preserves_execution_env {evm evm' : EVMState} (h : preserved evm evm') : - evm.execution_env = evm'.execution_env := h.1.2 + evm.execution_env = evm'.execution_env := by + rw [preserved_def] at h + exact h.2.2.1 def preserves_keccak_map {evm evm' : EVMState} (h : preserved evm evm') : - evm.keccak_map = evm'.keccak_map := h.2 + evm.keccak_map = evm'.keccak_map := by + rw [preserved_def] at h + exact h.2.2.2 @[simp] lemma preserved_rfl {e : EVM} : preserved e e := by diff --git a/Clear/Wheels.lean b/Clear/Wheels.lean index c07c533..de70965 100644 --- a/Clear/Wheels.lean +++ b/Clear/Wheels.lean @@ -1,17 +1,7 @@ import Aesop -import Mathlib.Data.Rel import Mathlib.Tactic.ApplyAt -instance instRelInter {α β} : Inter (Rel α β) where - inter r s := λ a b ↦ r a b ∧ s a b - -def Rel.inter {α β} (r : α → β → Prop) (s : α → β → Prop) : α → β → Prop := - λ a b ↦ r a b ∧ s a b - -instance instFunInter {α β : Type} : Inter (α → β → Prop) where - inter r s := λ a b ↦ r a b ∧ s a b - declare_aesop_rule_sets [Clear.aesop_ok, Clear.aesop_spec, Clear.aesop_varstore] set_option hygiene false in From e57b13920780221c7792ea99a52c722f58218201 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= Date: Tue, 8 Oct 2024 12:50:01 +0200 Subject: [PATCH 6/7] Use order for the keccek map preserve relation some more lemmas --- Clear/EVMState.lean | 57 ++++++++++++++++++++++---------------------- Clear/Utilities.lean | 32 ++++++++++++++++++------- 2 files changed, 52 insertions(+), 37 deletions(-) diff --git a/Clear/EVMState.lean b/Clear/EVMState.lean index c61a9d5..3d01ff2 100644 --- a/Clear/EVMState.lean +++ b/Clear/EVMState.lean @@ -164,37 +164,42 @@ instance : Inhabited EVMState := abbrev EVM := EVMState +instance instFinmapPreorder : Preorder (Finmap (λ _ : List UInt256 ↦ UInt256)) where + le a b := a.keys ⊆ b.keys ∧ ∀ {key}, key ∈ a → a.lookup key = b.lookup key + le_refl := by aesop + le_trans := by aesop (add safe forward subset_trans) + def preserved : EVMState → EVMState → Prop := λ a b ↦ (Eq on EVMState.account_map) a b ∧ (Eq on EVMState.hash_collision) a b ∧ (Eq on EVMState.execution_env) a b ∧ - (Eq on EVMState.keccak_map) a b + (a.keccak_map ≤ b.keccak_map) -lemma preserved_def {e₀ e₁ : EVM} : preserved e₀ e₁ = - (e₀.account_map = e₁.account_map ∧ - e₀.hash_collision = e₁.hash_collision ∧ - e₀.execution_env = e₁.execution_env ∧ - e₀.keccak_map = e₁.keccak_map) := by +lemma preserved_def {σ₀ σ₁ : EVM} : preserved σ₀ σ₁ = + (σ₀.account_map = σ₁.account_map ∧ + σ₀.hash_collision = σ₁.hash_collision ∧ + σ₀.execution_env = σ₁.execution_env ∧ + σ₀.keccak_map ≤ σ₁.keccak_map) := by unfold preserved dsimp -def preserves_account_map {evm evm' : EVMState} (h : preserved evm evm') : +def preserved_account_map {evm evm' : EVMState} (h : preserved evm evm') : evm.account_map = evm'.account_map := by rw [preserved_def] at h exact h.1 -def preserves_collision {evm evm' : EVMState} (h : preserved evm evm') : +def preserved_collision {evm evm' : EVMState} (h : preserved evm evm') : evm.hash_collision = evm'.hash_collision := by rw [preserved_def] at h exact h.2.1 -def preserves_execution_env {evm evm' : EVMState} (h : preserved evm evm') : +def preserved_execution_env {evm evm' : EVMState} (h : preserved evm evm') : evm.execution_env = evm'.execution_env := by rw [preserved_def] at h exact h.2.2.1 -def preserves_keccak_map {evm evm' : EVMState} (h : preserved evm evm') : - evm.keccak_map = evm'.keccak_map := by +def mono_keccak_map {evm evm' : EVMState} (h : preserved evm evm') : + evm.keccak_map ≤ evm'.keccak_map := by rw [preserved_def] at h exact h.2.2.2 @@ -203,26 +208,15 @@ lemma preserved_rfl {e : EVM} : preserved e e := by rw [preserved_def] simp -lemma preserved_symm {e₀ e₁ : EVM} : preserved e₀ e₁ = preserved e₁ e₀ := by - rw [preserved_def, preserved_def] - ext - apply Iff.intro <;> { - intro ⟨acc, col, env, kec⟩ - symm at acc col env kec - exact ⟨acc, col, env, kec⟩ - } - -@[simp] lemma preserved_trans {e₀ e₁ e₂ : EVM} : preserved e₀ e₁ → preserved e₁ e₂ → preserved e₀ e₂ := by rw (config := {occs := .pos [3]}) [preserved_def] intro h₀ h₁ - have acc := Eq.trans (preserves_account_map h₀) (preserves_account_map h₁) - have col := Eq.trans (preserves_collision h₀) (preserves_collision h₁) - have env := Eq.trans (preserves_execution_env h₀) (preserves_execution_env h₁) - have kec := Eq.trans (preserves_keccak_map h₀) (preserves_keccak_map h₁) - constructor; swap; constructor; swap; constructor - all_goals assumption + have acc := Eq.trans (preserved_account_map h₀) (preserved_account_map h₁) + have col := Eq.trans (preserved_collision h₀) (preserved_collision h₁) + have env := Eq.trans (preserved_execution_env h₀) (preserved_execution_env h₁) + have kec := le_trans (mono_keccak_map h₀) (mono_keccak_map h₁) + aesop -- functions for querying balance @@ -400,11 +394,18 @@ def evm_return (σ : EVMState) (mstart s : UInt256) : EVMState := def evm_revert (σ : EVMState) (mstart s : UInt256) : EVMState := σ.evm_return mstart s -lemma mstore_preserves {evm} {pos val} : preserved evm (evm.mstore pos val) := by +lemma mstore_preserved {σ} {pos val} : preserved σ (σ.mstore pos val) := by unfold mstore updateMemory rw [preserved_def] simp +lemma sload_eq_of_preserved {σ₀ σ₁} {pos} (h : preserved σ₀ σ₁) : + sload σ₀ pos = sload σ₁ pos := by + unfold sload lookupAccount + rw [ preserved_account_map h + , preserved_execution_env h + ] + end end Clear.EVMState diff --git a/Clear/Utilities.lean b/Clear/Utilities.lean index 12c66d6..a25d26b 100644 --- a/Clear/Utilities.lean +++ b/Clear/Utilities.lean @@ -92,7 +92,7 @@ lemma preservesEvm_of_isOk {s₀ s₁ : State} (s₀_ok : s₀.isOk) (s₁_ok : (s₀.evm.account_map = s₁.evm.account_map ∧ s₀.evm.hash_collision = s₁.evm.hash_collision ∧ s₀.evm.execution_env = s₁.evm.execution_env ∧ - s₀.evm.keccak_map = s₁.evm.keccak_map) := by + s₀.evm.keccak_map ≤ s₁.evm.keccak_map) := by unfold preservesEvm cases s₀ <;> cases s₁ <;> simp at * rw [preserved_def] @@ -103,14 +103,13 @@ lemma preservesEvm_rfl {s : State} : preservesEvm s s := by unfold preservesEvm cases s <;> simp -@[simp] lemma preservesEvm_trans {s₀ s₁ s₂} (h : s₁.isOk) : preservesEvm s₀ s₁ → preservesEvm s₁ s₂ → preservesEvm s₀ s₂ := by unfold preservesEvm cases s₀ <;> cases s₁ <;> cases s₂ <;> simp_all exact preserved_trans -lemma preservesEvm_eq (s₀ : State) (s₁ : State) : +lemma preservesEvm_of_preserved (s₀ : State) (s₁ : State) : preserved s₀.evm s₁.evm → preservesEvm s₀ s₁ := by unfold preservesEvm cases s₀ <;> cases s₁ <;> simp @@ -119,11 +118,26 @@ lemma preservesEvm_eq (s₀ : State) (s₁ : State) : lemma sload_eq_of_preservesEvm {s s' : State} {a : UInt256} (h : s.isOk) (h' : s'.isOk) (hss : preservesEvm s s') : s.evm.sload a = s'.evm.sload a := by - cases s <;> cases s' <;> simp_all - simp only [evm] - unfold EVMState.sload EVMState.lookupAccount - rw [ preserves_account_map hss - , preserves_execution_env hss - ] + unfold preservesEvm at hss + unfold isOk at h h' + cases s <;> cases s' <;> simp [evm] at * + exact EVMState.sload_eq_of_preserved hss + +@[aesop safe norm (rule_sets := [Clear.aesop_spec])] +lemma preservesEvm_of_insert {s₀ s₁} {var val} : + preservesEvm (s₀⟦var ↦ val⟧) s₁ ↔ preservesEvm s₀ s₁ := by + unfold preservesEvm + cases s₀ <;> cases s₁ <;> simp + unfold State.insert; simp + unfold State.insert; simp + +@[aesop safe norm (rule_sets := [Clear.aesop_spec])] +lemma preservesEvm_of_insert' {s₀ s₁} {var val} : + preservesEvm s₀ (s₁⟦var ↦ val⟧) ↔ preservesEvm s₀ s₁ := by + unfold preservesEvm + cases s₀ <;> cases s₁ <;> simp + swap + unfold State.insert; simp + unfold State.insert; simp end Clear.Utilities From 585e97d75d62e5dcb0a73ed713575f058416d432 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= Date: Tue, 8 Oct 2024 14:18:24 +0200 Subject: [PATCH 7/7] Use a structure for Preserved relation --- Clear/EVMState.lean | 79 ++++++++++++++++++++------------------------ Clear/Utilities.lean | 8 ++--- 2 files changed, 39 insertions(+), 48 deletions(-) diff --git a/Clear/EVMState.lean b/Clear/EVMState.lean index 3d01ff2..90f5ba9 100644 --- a/Clear/EVMState.lean +++ b/Clear/EVMState.lean @@ -164,59 +164,50 @@ instance : Inhabited EVMState := abbrev EVM := EVMState -instance instFinmapPreorder : Preorder (Finmap (λ _ : List UInt256 ↦ UInt256)) where +instance instPreorderFinmap : Preorder (Finmap (λ _ : List UInt256 ↦ UInt256)) where le a b := a.keys ⊆ b.keys ∧ ∀ {key}, key ∈ a → a.lookup key = b.lookup key le_refl := by aesop le_trans := by aesop (add safe forward subset_trans) -def preserved : EVMState → EVMState → Prop := - λ a b ↦ (Eq on EVMState.account_map) a b ∧ - (Eq on EVMState.hash_collision) a b ∧ - (Eq on EVMState.execution_env) a b ∧ - (a.keccak_map ≤ b.keccak_map) +structure Preserved (a : EVMState) (b : EVMState) : Prop where + account_map : (Eq on EVMState.account_map) a b + hash_collision : (Eq on EVMState.hash_collision) a b + execution_env : (Eq on EVMState.execution_env) a b + keccak_map : a.keccak_map ≤ b.keccak_map -lemma preserved_def {σ₀ σ₁ : EVM} : preserved σ₀ σ₁ = +lemma Preserved_def {σ₀ σ₁ : EVM} : Preserved σ₀ σ₁ = (σ₀.account_map = σ₁.account_map ∧ σ₀.hash_collision = σ₁.hash_collision ∧ σ₀.execution_env = σ₁.execution_env ∧ σ₀.keccak_map ≤ σ₁.keccak_map) := by - unfold preserved - dsimp + ext + apply Iff.intro + intro h + obtain ⟨_,_,_,_⟩ := h + all_goals tauto -def preserved_account_map {evm evm' : EVMState} (h : preserved evm evm') : - evm.account_map = evm'.account_map := by - rw [preserved_def] at h - exact h.1 - -def preserved_collision {evm evm' : EVMState} (h : preserved evm evm') : - evm.hash_collision = evm'.hash_collision := by - rw [preserved_def] at h - exact h.2.1 - -def preserved_execution_env {evm evm' : EVMState} (h : preserved evm evm') : - evm.execution_env = evm'.execution_env := by - rw [preserved_def] at h - exact h.2.2.1 - -def mono_keccak_map {evm evm' : EVMState} (h : preserved evm evm') : - evm.keccak_map ≤ evm'.keccak_map := by - rw [preserved_def] at h - exact h.2.2.2 +namespace Preserved @[simp] -lemma preserved_rfl {e : EVM} : preserved e e := by - rw [preserved_def] - simp +lemma refl {e : EVM} : Preserved e e := by + constructor + all_goals simp -lemma preserved_trans {e₀ e₁ e₂ : EVM} : - preserved e₀ e₁ → preserved e₁ e₂ → preserved e₀ e₂ := by - rw (config := {occs := .pos [3]}) [preserved_def] +lemma trans {e₀ e₁ e₂ : EVM} : + Preserved e₀ e₁ → Preserved e₁ e₂ → Preserved e₀ e₂ := by intro h₀ h₁ - have acc := Eq.trans (preserved_account_map h₀) (preserved_account_map h₁) - have col := Eq.trans (preserved_collision h₀) (preserved_collision h₁) - have env := Eq.trans (preserved_execution_env h₀) (preserved_execution_env h₁) - have kec := le_trans (mono_keccak_map h₀) (mono_keccak_map h₁) - aesop + have acc := Eq.trans h₀.account_map h₁.account_map + have col := Eq.trans h₀.hash_collision h₁.hash_collision + have env := Eq.trans h₀.execution_env h₁.execution_env + have kec := le_trans h₀.keccak_map h₁.keccak_map + constructor <;> assumption + +end Preserved + +instance instPreorderEVMState : Preorder EVMState where + le := Preserved + le_refl := @Preserved.refl + le_trans := @Preserved.trans -- functions for querying balance @@ -394,16 +385,16 @@ def evm_return (σ : EVMState) (mstart s : UInt256) : EVMState := def evm_revert (σ : EVMState) (mstart s : UInt256) : EVMState := σ.evm_return mstart s -lemma mstore_preserved {σ} {pos val} : preserved σ (σ.mstore pos val) := by +lemma mstore_preserved {σ} {pos val} : Preserved σ (σ.mstore pos val) := by unfold mstore updateMemory - rw [preserved_def] + rw [Preserved_def] simp -lemma sload_eq_of_preserved {σ₀ σ₁} {pos} (h : preserved σ₀ σ₁) : +lemma sload_eq_of_preserved {σ₀ σ₁} {pos} (h : Preserved σ₀ σ₁) : sload σ₀ pos = sload σ₁ pos := by unfold sload lookupAccount - rw [ preserved_account_map h - , preserved_execution_env h + rw [ h.account_map + , h.execution_env ] end diff --git a/Clear/Utilities.lean b/Clear/Utilities.lean index a25d26b..ea4aaf5 100644 --- a/Clear/Utilities.lean +++ b/Clear/Utilities.lean @@ -84,7 +84,7 @@ lemma evm_eq_symm_of_isPure_ok_ok {evm evm'} {vs vs'} (h : isPure (Ok evm vs) (O def preservesEvm (s₀ : State) (s₁ : State) : Prop := match s₀, s₁ with - | .Ok e₀ _, .Ok e₁ _ => preserved e₀ e₁ + | .Ok e₀ _, .Ok e₁ _ => Preserved e₀ e₁ | _, _ => True lemma preservesEvm_of_isOk {s₀ s₁ : State} (s₀_ok : s₀.isOk) (s₁_ok : s₁.isOk) : @@ -95,7 +95,7 @@ lemma preservesEvm_of_isOk {s₀ s₁ : State} (s₀_ok : s₀.isOk) (s₁_ok : s₀.evm.keccak_map ≤ s₁.evm.keccak_map) := by unfold preservesEvm cases s₀ <;> cases s₁ <;> simp at * - rw [preserved_def] + rw [Preserved_def] intro _; assumption @[simp] @@ -107,10 +107,10 @@ lemma preservesEvm_trans {s₀ s₁ s₂} (h : s₁.isOk) : preservesEvm s₀ s₁ → preservesEvm s₁ s₂ → preservesEvm s₀ s₂ := by unfold preservesEvm cases s₀ <;> cases s₁ <;> cases s₂ <;> simp_all - exact preserved_trans + exact Preserved.trans lemma preservesEvm_of_preserved (s₀ : State) (s₁ : State) : - preserved s₀.evm s₁.evm → preservesEvm s₀ s₁ := by + Preserved s₀.evm s₁.evm → preservesEvm s₀ s₁ := by unfold preservesEvm cases s₀ <;> cases s₁ <;> simp simp [evm]