Preserved EVM state relation

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,59 @@ 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)
+
+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
+  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.1
+
+def preserves_collision {evm evm' : EVMState} (h : preserved evm evm') :
+  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.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
+  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
+
 -- functions for querying balance
 
 namespace EVMState
@@ -339,6 +393,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

Clear/Utilities.lean

@@ -82,4 +82,48 @@ 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
+
+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
+  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) :
+  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
+  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

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