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,60 @@ 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 ∧
+          (a.keccak_map ≤ b.keccak_map)
+
+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 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
+
+@[simp]
+lemma preserved_rfl {e : EVM} : preserved e e := by
+  rw [preserved_def]
+  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 (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
 
 namespace EVMState
@@ -339,6 +394,18 @@ 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
+  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

Clear/Utilities.lean

@@ -82,4 +82,62 @@ 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
+
+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_of_preserved (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
+  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