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,51 @@ instance : Inhabited EVMState :=
 
 abbrev EVM := EVMState
 
+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)
+
+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 σ₀ σ₁ =
+  (σ₀.account_map    = σ₁.account_map ∧
+   σ₀.hash_collision = σ₁.hash_collision ∧
+   σ₀.execution_env  = σ₁.execution_env ∧
+   σ₀.keccak_map     ≤ σ₁.keccak_map) := by
+  ext
+  apply Iff.intro
+  intro h
+  obtain ⟨_,_,_,_⟩ := h
+  all_goals tauto
+
+namespace Preserved
+
+@[simp]
+lemma refl {e : EVM} : Preserved e e := by
+  constructor
+  all_goals simp
+
+lemma trans {e₀ e₁ e₂ : EVM} :
+  Preserved e₀ e₁ → Preserved e₁ e₂ → Preserved e₀ e₂ := by
+  intro h₀ h₁
+  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
 
 namespace EVMState
@@ -339,6 +385,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 [ h.account_map
+     , h.execution_env
+     ]
+
 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