diff --git a/Clear/Abstraction.lean b/Clear/Abstraction.lean index d7111c7..5ed24cb 100644 --- a/Clear/Abstraction.lean +++ b/Clear/Abstraction.lean @@ -3,6 +3,7 @@ import Clear.ExecLemmas import Clear.OutOfFuelLemmas import Clear.JumpLemmas import Clear.YulNotation +import Clear.Wheels namespace Clear.Abstraction @@ -18,7 +19,7 @@ variable {s s₀ s₁ sEnd : State} -- | General form for relational specs (concrete and abstract). @[aesop safe 0 unfold (rule_sets := [Clear.aesop_spec])] -def Spec (R : State → State → Prop) (s₀ s₁ : State) : Prop := +def Spec (R : State → State → Prop) (s₀ s₁ : State) := match s₀ with | OutOfFuel => ❓ s₁ | Checkpoint c => s₁.isJump c @@ -31,6 +32,30 @@ lemma Spec_ok_unfold {P : State → State → Prop} : unfold Spec aesop +-- | Specs that are somewhat pure +@[aesop safe 0 unfold (rule_sets := [Clear.aesop_spec])] +def PureSpec (R : State → State → Prop) : State → State → Prop := + Spec (R ∩ (preserved on evm)) + +lemma PureSpec_ok_unfold {P : State → State → Prop} : + ∀ {s s' : State}, s.isOk → ¬ ❓ s' → PureSpec P s s' → (P ∩ (preserved on evm)) s s' := by + intros s s' h h' + unfold PureSpec Spec + aesop + +-- | Specs for code that might result in hash collision +@[aesop safe 0 unfold (rule_sets := [Clear.aesop_spec])] +def CollidingSpec (R : State → State → Prop) (s₀ s₁ : State) : Prop := + if s₀.evm.hash_collision + then ❓ s₁ + else ¬ s₁.evm.hash_collision → Spec R s₀ s₁ + +lemma CollidingSpec_ok_unfold {P : State → State → Prop} : + ∀ {s s' : State}, s.isOk → ¬ ❓ s' → ¬ s'.evm.hash_collision → CollidingSpec P s s' → P s s' := by + intros s s' h h' h'' + unfold CollidingSpec Spec + aesop + open Lean Elab Tactic in elab "clr_spec" "at" h:ident : tactic => do evalTactic <| ← `(tactic| ( @@ -46,6 +71,12 @@ lemma not_isOutOfFuel_Spec (spec : Spec R s₀ s₁) (h : ¬ isOutOfFuel s₁) : intros hs₀ aesop_spec +-- | No hash collision propagates backwards through specs. +-- lemma not_hashCollision_Spec +-- (spec : CollidingSpec R s₀ s₁) (h : ¬ s₁.evm.hasHashCollision) : ¬ s₀.evm.hasHashCollision := by +-- intros hs₀ +-- aesop_spec + -- ============================================================================ -- TACTICS -- ============================================================================ @@ -151,7 +182,7 @@ elab "clr_funargs" "at" h:ident : tactic => do simp only [multifill_cons, multifill_nil', isOk_insert, isOk_Ok, isOutOfFuel_Ok, not_false_eq_true, imp_false, Ok.injEq, and_imp, forall_apply_eq_imp_iff₂, forall_apply_eq_imp_iff] at $h:ident - repeat (rw [←State.insert] at $h:ident) + repeat (rw [←State.insert] at $h:ident) )) end Clear diff --git a/Clear/EVMState.lean b/Clear/EVMState.lean index 9fa9075..8204873 100644 --- a/Clear/EVMState.lean +++ b/Clear/EVMState.lean @@ -1,8 +1,16 @@ import Mathlib.Data.Finmap import Mathlib.Data.Fin.Basic +import Mathlib.Data.List.Intervals import Clear.Ast import Clear.Instr import Clear.UInt256 +import Clear.Wheels + +set_option linter.setOption false +set_option pp.coercions false + +set_option maxHeartbeats 700000 +set_option maxRecDepth 800 open Clear Instr UInt256 @@ -160,8 +168,10 @@ def Account.updateStorage (act : Account) (k v : UInt256) : Account := -- definition of the machine state +abbrev Memory := Finmap (λ _ : UInt256 ↦ UInt8) + structure MachineState : Type where - memory : Finmap (λ _ : UInt256 => UInt8) + memory : Memory max_address : UInt256 gas_available : UInt256 return_data : List UInt256 @@ -171,21 +181,172 @@ instance : Inhabited MachineState := ⟨ MachineState.mk ∅ 0 0 [] ⟩ -- @langfield: Nit, but definitions should be camelCase. -def UInt256.offsets : List UInt256 := +def UInt256.offsets : List ℕ := [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16, 17,18,19,20,21,22,23,24,25,26,27,28,29,30,31] +lemma UInt256.offsets_def : offsets = List.range 32 := by + repeat rw [ List.range_succ_eq_map ] + unfold offsets + simp + +lemma max_of_offsets_lt_32 : offsets.maximum < 32 := by decide +lemma min_of_offsets_eq_0 : offsets.minimum = 0 := by decide + +lemma mem_offsets : ∀ {n}, n ∈ offsets ↔ n < 32 := by + intro n + rw [offsets_def] + simp + +@[simp] +lemma mem_offsets_of_lt_32 : ∀ {n}, n < 32 → n ∈ offsets := + mem_offsets.mpr + +lemma lt_32_of_mem_offsets : ∀ {n}, n ∈ offsets → n < 32 := + mem_offsets.mp + +-- List.Ico not yet in mathlib +lemma UInt256.offsets_eq_Ico : offsets = List.Ico 0 32 := by + unfold List.Ico + rw [ List.range'_eq_map_range, offsets_def ] + simp + +-- lemma UInt256.offsets_at_addr : +-- ∀ (addr : UInt256), +-- offsets.map (addr + ↑·) = List.Ico addr.val (addr.val + 32) := by +-- intro addr +-- rw [offsets_eq_Ico, List.Ico.map_add 0 32 addr, zero_add, add_comm] + +lemma UInt256.mem_offsets_iff_mem_Ico : ∀ {n}, n ∈ offsets ↔ n ∈ Set.Ico 0 32 := by + intro n + apply Iff.intro + · intro mem + simp + exact mem_offsets.mp mem + · intro mem + simp at mem + exact mem_offsets.mpr mem + +lemma UInt256.offsetted_addresses (addr : UInt256) : ∀ {n}, + (h : n ∈ offsets) → addr + ↑n ∈ offsets.map (addr + ↑·) := by + intro n h + exact List.mem_map_of_mem (addr + ↑·) h + +-- lemma UInt256.word_addresses (addr : UInt256) : +-- Set.MapsTo (addr + ↑·) (Set.Ico 0 32) (Set.Ico addr (addr + 32)) := by +-- have : (addr + ↑·) '' (Set.Ico 0 32) = Set.Ico addr (addr + 32) := by +-- dsimp [Set.image] +-- conv => rhs; rw [← Set.Ico_def] + +-- sorry + +-- rw [← this] +-- exact Set.mapsTo_image (addr + ↑·) (Set.Ico 0 32) + + +-- lemma UInt256.same_address_of_offsetted_addresses (addr addr': UInt256) {n} : +-- (h : n ∈ offsets) → +-- addr' + ↑n ∈ offsets.map (addr + ↑·) → +-- addr' = addr := by +-- intro h mem +-- simp at mem +-- sorry + +-- lemma UInt256.addresses_of (addr : UInt256) {a} : +-- a ∈ offsets.map (addr + ↑·) ↔ a ∈ Set.Ico addr (addr + 32) := by +-- sorry + +namespace UInt256 + +def range' (start : UInt256) (len : ℕ) (step : UInt256 := 1) : List UInt256 := + match start, len with + | _, 0 => [] + | s, n + 1 => s :: range' (s + step) n step + +@[simp] +lemma range'_zero {s step : UInt256} : range' s 0 step = [] := by + unfold range' + rfl + +@[simp] +lemma range'_one {s step : UInt256} : range' s 1 step = [s] := by + unfold range' + simp + +lemma range'_succ (start : UInt256) (len : ℕ) (step : UInt256) : + range' start (len + 1) step = + start :: range' (start + step) len step := by + conv => + lhs + unfold range' + simp + +-- lemma range'_succ' (start : UInt256) (len : ℕ) (step : UInt256) (k : ℕ) [NeZero k] : +-- range' start (len + k) step = +-- start :: range' (start + step) (len + k - 1) step := by +-- admit + +lemma map_add_range' (a) : ∀ s n step, + List.map (a + ·) (range' s n step) = + range' (a + s) n step + | _, 0, _ => by simp + | s, n+1, step => by + unfold range' + simp [map_add_range', add_assoc] + +def offsets_at (addr : UInt256) : List UInt256 := + range' addr 32 1 + +def words_at (addr : UInt256) (n : ℕ) : List UInt256 := + range' addr n 32 + +end UInt256 + +lemma splice_toBytes! (v : UInt256) : toBytes! v = + [ (toBytes! v)[0], (toBytes! v)[1], (toBytes! v)[2], (toBytes! v)[3] + , (toBytes! v)[4], (toBytes! v)[5], (toBytes! v)[6], (toBytes! v)[7] + , (toBytes! v)[8], (toBytes! v)[9], (toBytes! v)[10], (toBytes! v)[11] + , (toBytes! v)[12], (toBytes! v)[13], (toBytes! v)[14], (toBytes! v)[15] + , (toBytes! v)[16], (toBytes! v)[17], (toBytes! v)[18], (toBytes! v)[19] + , (toBytes! v)[20], (toBytes! v)[21], (toBytes! v)[22], (toBytes! v)[23] + , (toBytes! v)[24], (toBytes! v)[25], (toBytes! v)[26], (toBytes! v)[27] + , (toBytes! v)[28], (toBytes! v)[29], (toBytes! v)[30], (toBytes! v)[31] + ] := by + apply List.ext_get + · simp + · intro n h₁ h₂ + simp at h₂ + have h_offset := mem_offsets_of_lt_32 h₂ + fin_cases h_offset + all_goals aesop + +abbrev Entry := UInt256 × UInt8 + +@[simp] +def memInsert (entry : Entry) (mem : Memory) : Memory := + Function.uncurry mem.insert entry + +@[simp] +def mkEntries (addr data : UInt256) : List Entry := + let addrs := offsets.map (addr + ↑·) + addrs.zip (UInt256.toBytes! data) + +def Memory.maxWords := 3618502788666131106986593281521497120414687020801267626233049500247285301247 + +def Memory.maxWords_def : Memory.maxWords = (⊤ : UInt256) / 32 := by + rw [maxWords, Fin.top_eq_last] + simp + def MachineState.updateMemory (m : MachineState) (addr v : UInt256) : MachineState := - {m with memory := let offsets := List.range 32 - let addrs := offsets.map (·+addr) - let inserts := addrs.zipWith Finmap.insert (UInt256.toBytes! v) - inserts.foldl (init := m.memory) (flip id) + {m with memory := List.foldr (init := m.memory) memInsert <| mkEntries addr v max_address := max addr m.max_address } -lemma cheeky_proof {a b : Int} : (if a > b then a else b) = max a b := by rw [max_comm, max_def_lt] +def Memory.lookupByte (m : Memory) (addr : UInt256) : UInt8 := + (m.lookup addr).get! -def MachineState.lookupMemory (m : MachineState) (addr : UInt256) : UInt256 := - UInt256.fromBytes! (List.map (fun i => (m.memory.lookup (addr + i)).get!) UInt256.offsets) +def Memory.lookupWord (m : Memory) (addr : UInt256) : UInt256 := +-- UInt256.fromBytes! (offsets.map λ i ↦ (m.memory.lookup (addr + i)).get!) + UInt256.fromBytes! $ offsets.map $ m.lookupByte ∘ (addr + ↑·) def MachineState.setReturnData (m : MachineState) (r : List UInt256) : MachineState := {m with return_data := r} @@ -193,7 +354,6 @@ def MachineState.setReturnData (m : MachineState) (r : List UInt256) : MachineSt def MachineState.msize (m : MachineState) : UInt256 := m.max_address - -- definition of the blocks structure BlockHeader : Type where @@ -254,6 +414,11 @@ 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) + -- functions for querying balance namespace EVMState @@ -263,7 +428,12 @@ section open Array ByteArray -- | Add an error to the EVMState indicating that we hit a hash collision in `keccak256`. -def addHashCollision (σ : EVMState) : EVMState := { σ with hash_collision := True } +def addHashCollision (σ : EVMState) : EVMState := { σ with hash_collision := true } + +-- def hasHashCollision (σ : EVMState) : Prop := σ.hash_collision = true + +-- instance : DecidablePred hasHashCollision := λ σ ↦ +-- decidable_of_bool σ.hash_collision (by unfold hasHashCollision; simp) def lookupAccount (σ : EVMState) (addr : Address) : Option Account := σ.account_map.lookup addr @@ -293,14 +463,11 @@ def calldatacopy (σ : EVMState) (mstart datastart s : UInt256) : EVMState := let r := arr.foldl (λ (sa , j) i => (EVMState.updateMemory sa j i.val, j + 1)) (σ , mstart) r.1 -def mkInterval (ms : MachineState) (p n : UInt256) : List UInt256 := - let i : ℕ := p.val - let f : ℕ := n.val - let m := (List.range' i f).map Fin.ofNat - m.map ms.lookupMemory +def mkInterval (ms : Memory) (p : UInt256) (n : ℕ) : List UInt256 := + (words_at p n).map ms.lookupWord def keccak256 (σ : EVMState) (p n : UInt256) : Option (UInt256 × EVMState) := - let interval : List UInt256 := mkInterval σ.machine_state p n + let interval : List UInt256 := mkInterval σ.machine_state.memory p n.val match Finmap.lookup interval σ.keccak_map with | .some val => .some (val, σ) | .none => @@ -381,7 +548,7 @@ def selfbalance (σ : EVMState) : UInt256 := -- memory and storage operations def mload (σ : EVMState) (spos : UInt256) : UInt256 := - σ.machine_state.lookupMemory spos + σ.machine_state.memory.lookupWord spos def mstore (σ : EVMState) (spos sval : UInt256) : EVMState := σ.updateMemory spos sval @@ -432,4 +599,1328 @@ def evm_revert (σ : EVMState) (mstart s : UInt256) : EVMState := end +section Memory + +variable {addr addr' : UInt256} +variable {ms : MachineState} +variable {val val' : UInt256} +variable {entry : Entry} +variable {es es' : List Entry} + +@[simp] +lemma frontflip : (λ b a ↦ memInsert a b) = flip memInsert := by + unfold flip + ext + simp + +@[simp] +lemma backflip : (λ b a ↦ flip memInsert a b) = memInsert := by + unfold flip + ext + simp + +lemma foldr_mem_nil {init : Memory} : + List.foldr memInsert (List.foldr memInsert init []) [] = init := by + simp + +lemma memInsert_memInsert {m : Memory} {a b : UInt8} : + memInsert ⟨addr, a⟩ (memInsert ⟨addr, b⟩ m) = + memInsert ⟨addr, a⟩ m := by + simp + +lemma memInsert_memInsert_of_ne {m : Memory} {a b : UInt8} : + (h : addr' ≠ addr) → + memInsert ⟨addr, a⟩ (memInsert ⟨addr', b⟩ m) = + memInsert ⟨addr', b⟩ (memInsert ⟨addr, a⟩ m) := by + intro h + simp + exact Finmap.insert_insert_of_ne m h + +lemma foldr_memInsert_reverse {init : Memory} : + List.foldr memInsert init (mkEntries addr val) = + List.foldr memInsert init (mkEntries addr val).reverse := by + simp only [mkEntries] + rw [ splice_toBytes! val ] + unfold offsets + + simp only [List.map, List.zip, List.zipWith, List.reverse, List.reverseAux] + simp only [Nat.cast_ofNat, Nat.cast_one, Nat.cast_zero] + rw [List.foldr_cons] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[1]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[2]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[2]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[3]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[3]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[3]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[4]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[4]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[4]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[4]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[5]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[5]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[5]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[5]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[5]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[6]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[6]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[6]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[6]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[6]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[6]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[7]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[7]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[7]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[7]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[7]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[7]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[7]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[8]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[8]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[8]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[8]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[8]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[8]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[8]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[8]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[9]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[9]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[9]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[9]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[9]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[9]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[9]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[9]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[9]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[10]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[10]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[10]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[10]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[10]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[10]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[10]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[10]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[10]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[10]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[11]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[11]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[11]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[11]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[11]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[11]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[11]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[11]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[11]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[11]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[11]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[12]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[12]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[12]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[12]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[12]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[12]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[12]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[12]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[12]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[12]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[12]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[12]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[13]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[13]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[13]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[13]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[13]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[13]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[13]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[13]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[13]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[13]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[13]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[13]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[13]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[14]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[15]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[16]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[17]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[18]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[19]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[20]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[21]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[22]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[23]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[24]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[25]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[26]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[27]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[28]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[29]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[30]) (by simp) + ] + rw [ List.foldr_cons + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + , memInsert_memInsert_of_ne (b := (toBytes! val)[31]) (by simp) + ] + rw [ ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + , ← List.foldr_cons (f := memInsert), ← List.foldr_cons (f := memInsert) + ] + +lemma foldl_memInsert_reverse {init : Memory} : + List.foldl (flip memInsert) init (mkEntries addr val) = + List.foldl (flip memInsert) init (mkEntries addr val).reverse := by + rw [ List.foldl_reverse, backflip, foldr_memInsert_reverse, List.foldr_reverse, frontflip] + +lemma foldr_memInsert_eq_foldl_memInsert {init : Memory} : + List.foldr memInsert init (mkEntries addr val) = + List.foldl (flip memInsert) init (mkEntries addr val) := by + rw [ foldr_memInsert_reverse, List.foldr_reverse, frontflip] + +end Memory + +section MachineState + +variable {addr addr' : UInt256} +variable {ms : MachineState} +variable {val val' : UInt256} +variable {entry : Entry} +variable {es es' : List Entry} + +lemma update_update : + (ms.updateMemory addr val).updateMemory addr val' = ms.updateMemory addr val' := by + unfold MachineState.updateMemory + simp + + rw [ ← mkEntries, ← mkEntries ] + rw [ foldr_memInsert_eq_foldl_memInsert ] + + conv => rhs; rw [ foldr_memInsert_eq_foldl_memInsert, foldl_memInsert_reverse ] + rw [ mkEntries, mkEntries ] + + rw [ splice_toBytes! val, splice_toBytes! val' ] + unfold offsets + + unfold flip + simp only [List.map, List.zip, List.zipWith] + simp only [Nat.cast_ofNat, Nat.cast_one, Nat.cast_zero] + + rw [ List.foldr_cons, List.foldl_cons, memInsert_memInsert] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 2) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 3) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 3) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 4) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 4) (by simp), memInsert_memInsert_of_ne (addr := addr + 4) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 5) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 5) (by simp), memInsert_memInsert_of_ne (addr := addr + 5) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 5) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 6) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 6) (by simp), memInsert_memInsert_of_ne (addr := addr + 6) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 6) (by simp), memInsert_memInsert_of_ne (addr := addr + 6) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 7) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 7) (by simp), memInsert_memInsert_of_ne (addr := addr + 7) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 7) (by simp), memInsert_memInsert_of_ne (addr := addr + 7) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 7) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 8) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 8) (by simp), memInsert_memInsert_of_ne (addr := addr + 8) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 8) (by simp), memInsert_memInsert_of_ne (addr := addr + 8) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 8) (by simp), memInsert_memInsert_of_ne (addr := addr + 8) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 9) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 9) (by simp), memInsert_memInsert_of_ne (addr := addr + 9) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 9) (by simp), memInsert_memInsert_of_ne (addr := addr + 9) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 9) (by simp), memInsert_memInsert_of_ne (addr := addr + 9) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 9) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 10) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 10) (by simp), memInsert_memInsert_of_ne (addr := addr + 10) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 10) (by simp), memInsert_memInsert_of_ne (addr := addr + 10) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 10) (by simp), memInsert_memInsert_of_ne (addr := addr + 10) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 10) (by simp), memInsert_memInsert_of_ne (addr := addr + 10) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 11) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 11) (by simp), memInsert_memInsert_of_ne (addr := addr + 11) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 11) (by simp), memInsert_memInsert_of_ne (addr := addr + 11) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 11) (by simp), memInsert_memInsert_of_ne (addr := addr + 11) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 11) (by simp), memInsert_memInsert_of_ne (addr := addr + 11) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 11) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 12) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 12) (by simp), memInsert_memInsert_of_ne (addr := addr + 12) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 12) (by simp), memInsert_memInsert_of_ne (addr := addr + 12) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 12) (by simp), memInsert_memInsert_of_ne (addr := addr + 12) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 12) (by simp), memInsert_memInsert_of_ne (addr := addr + 12) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 12) (by simp), memInsert_memInsert_of_ne (addr := addr + 12) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 13) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 13) (by simp), memInsert_memInsert_of_ne (addr := addr + 13) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 13) (by simp), memInsert_memInsert_of_ne (addr := addr + 13) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 13) (by simp), memInsert_memInsert_of_ne (addr := addr + 13) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 13) (by simp), memInsert_memInsert_of_ne (addr := addr + 13) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 13) (by simp), memInsert_memInsert_of_ne (addr := addr + 13) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 13) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 14) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 14) (by simp), memInsert_memInsert_of_ne (addr := addr + 14) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 14) (by simp), memInsert_memInsert_of_ne (addr := addr + 14) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 14) (by simp), memInsert_memInsert_of_ne (addr := addr + 14) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 14) (by simp), memInsert_memInsert_of_ne (addr := addr + 14) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 14) (by simp), memInsert_memInsert_of_ne (addr := addr + 14) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 14) (by simp), memInsert_memInsert_of_ne (addr := addr + 14) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 15) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 15) (by simp), memInsert_memInsert_of_ne (addr := addr + 15) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 15) (by simp), memInsert_memInsert_of_ne (addr := addr + 15) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 15) (by simp), memInsert_memInsert_of_ne (addr := addr + 15) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 15) (by simp), memInsert_memInsert_of_ne (addr := addr + 15) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 15) (by simp), memInsert_memInsert_of_ne (addr := addr + 15) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 15) (by simp), memInsert_memInsert_of_ne (addr := addr + 15) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 15) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 16) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 16) (by simp), memInsert_memInsert_of_ne (addr := addr + 16) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 16) (by simp), memInsert_memInsert_of_ne (addr := addr + 16) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 16) (by simp), memInsert_memInsert_of_ne (addr := addr + 16) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 16) (by simp), memInsert_memInsert_of_ne (addr := addr + 16) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 16) (by simp), memInsert_memInsert_of_ne (addr := addr + 16) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 16) (by simp), memInsert_memInsert_of_ne (addr := addr + 16) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 16) (by simp), memInsert_memInsert_of_ne (addr := addr + 16) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 17) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 17) (by simp), memInsert_memInsert_of_ne (addr := addr + 17) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 17) (by simp), memInsert_memInsert_of_ne (addr := addr + 17) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 17) (by simp), memInsert_memInsert_of_ne (addr := addr + 17) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 17) (by simp), memInsert_memInsert_of_ne (addr := addr + 17) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 17) (by simp), memInsert_memInsert_of_ne (addr := addr + 17) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 17) (by simp), memInsert_memInsert_of_ne (addr := addr + 17) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 17) (by simp), memInsert_memInsert_of_ne (addr := addr + 17) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 17) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 18) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 18) (by simp), memInsert_memInsert_of_ne (addr := addr + 18) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 18) (by simp), memInsert_memInsert_of_ne (addr := addr + 18) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 18) (by simp), memInsert_memInsert_of_ne (addr := addr + 18) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 18) (by simp), memInsert_memInsert_of_ne (addr := addr + 18) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 18) (by simp), memInsert_memInsert_of_ne (addr := addr + 18) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 18) (by simp), memInsert_memInsert_of_ne (addr := addr + 18) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 18) (by simp), memInsert_memInsert_of_ne (addr := addr + 18) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 18) (by simp), memInsert_memInsert_of_ne (addr := addr + 18) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 19) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 19) (by simp), memInsert_memInsert_of_ne (addr := addr + 19) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 19) (by simp), memInsert_memInsert_of_ne (addr := addr + 19) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 19) (by simp), memInsert_memInsert_of_ne (addr := addr + 19) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 19) (by simp), memInsert_memInsert_of_ne (addr := addr + 19) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 19) (by simp), memInsert_memInsert_of_ne (addr := addr + 19) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 19) (by simp), memInsert_memInsert_of_ne (addr := addr + 19) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 19) (by simp), memInsert_memInsert_of_ne (addr := addr + 19) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 19) (by simp), memInsert_memInsert_of_ne (addr := addr + 19) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 19) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 20) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 20) (by simp), memInsert_memInsert_of_ne (addr := addr + 20) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 20) (by simp), memInsert_memInsert_of_ne (addr := addr + 20) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 20) (by simp), memInsert_memInsert_of_ne (addr := addr + 20) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 20) (by simp), memInsert_memInsert_of_ne (addr := addr + 20) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 20) (by simp), memInsert_memInsert_of_ne (addr := addr + 20) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 20) (by simp), memInsert_memInsert_of_ne (addr := addr + 20) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 20) (by simp), memInsert_memInsert_of_ne (addr := addr + 20) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 20) (by simp), memInsert_memInsert_of_ne (addr := addr + 20) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 20) (by simp), memInsert_memInsert_of_ne (addr := addr + 20) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 21) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 21) (by simp), memInsert_memInsert_of_ne (addr := addr + 21) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 21) (by simp), memInsert_memInsert_of_ne (addr := addr + 21) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 21) (by simp), memInsert_memInsert_of_ne (addr := addr + 21) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 21) (by simp), memInsert_memInsert_of_ne (addr := addr + 21) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 21) (by simp), memInsert_memInsert_of_ne (addr := addr + 21) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 21) (by simp), memInsert_memInsert_of_ne (addr := addr + 21) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 21) (by simp), memInsert_memInsert_of_ne (addr := addr + 21) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 21) (by simp), memInsert_memInsert_of_ne (addr := addr + 21) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 21) (by simp), memInsert_memInsert_of_ne (addr := addr + 21) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 21) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 22) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 22) (by simp), memInsert_memInsert_of_ne (addr := addr + 22) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 22) (by simp), memInsert_memInsert_of_ne (addr := addr + 22) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 22) (by simp), memInsert_memInsert_of_ne (addr := addr + 22) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 22) (by simp), memInsert_memInsert_of_ne (addr := addr + 22) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 22) (by simp), memInsert_memInsert_of_ne (addr := addr + 22) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 22) (by simp), memInsert_memInsert_of_ne (addr := addr + 22) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 22) (by simp), memInsert_memInsert_of_ne (addr := addr + 22) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 22) (by simp), memInsert_memInsert_of_ne (addr := addr + 22) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 22) (by simp), memInsert_memInsert_of_ne (addr := addr + 22) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 22) (by simp), memInsert_memInsert_of_ne (addr := addr + 22) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 23) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 23) (by simp), memInsert_memInsert_of_ne (addr := addr + 23) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 23) (by simp), memInsert_memInsert_of_ne (addr := addr + 23) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 23) (by simp), memInsert_memInsert_of_ne (addr := addr + 23) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 23) (by simp), memInsert_memInsert_of_ne (addr := addr + 23) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 23) (by simp), memInsert_memInsert_of_ne (addr := addr + 23) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 23) (by simp), memInsert_memInsert_of_ne (addr := addr + 23) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 23) (by simp), memInsert_memInsert_of_ne (addr := addr + 23) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 23) (by simp), memInsert_memInsert_of_ne (addr := addr + 23) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 23) (by simp), memInsert_memInsert_of_ne (addr := addr + 23) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 23) (by simp), memInsert_memInsert_of_ne (addr := addr + 23) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 23) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 24) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 24) (by simp), memInsert_memInsert_of_ne (addr := addr + 24) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 24) (by simp), memInsert_memInsert_of_ne (addr := addr + 24) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 24) (by simp), memInsert_memInsert_of_ne (addr := addr + 24) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 24) (by simp), memInsert_memInsert_of_ne (addr := addr + 24) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 24) (by simp), memInsert_memInsert_of_ne (addr := addr + 24) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 24) (by simp), memInsert_memInsert_of_ne (addr := addr + 24) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 24) (by simp), memInsert_memInsert_of_ne (addr := addr + 24) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 24) (by simp), memInsert_memInsert_of_ne (addr := addr + 24) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 24) (by simp), memInsert_memInsert_of_ne (addr := addr + 24) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 24) (by simp), memInsert_memInsert_of_ne (addr := addr + 24) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 24) (by simp), memInsert_memInsert_of_ne (addr := addr + 24) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 25) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 25) (by simp), memInsert_memInsert_of_ne (addr := addr + 25) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 25) (by simp), memInsert_memInsert_of_ne (addr := addr + 25) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 25) (by simp), memInsert_memInsert_of_ne (addr := addr + 25) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 25) (by simp), memInsert_memInsert_of_ne (addr := addr + 25) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 25) (by simp), memInsert_memInsert_of_ne (addr := addr + 25) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 25) (by simp), memInsert_memInsert_of_ne (addr := addr + 25) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 25) (by simp), memInsert_memInsert_of_ne (addr := addr + 25) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 25) (by simp), memInsert_memInsert_of_ne (addr := addr + 25) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 25) (by simp), memInsert_memInsert_of_ne (addr := addr + 25) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 25) (by simp), memInsert_memInsert_of_ne (addr := addr + 25) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 25) (by simp), memInsert_memInsert_of_ne (addr := addr + 25) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 25) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 26) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 26) (by simp), memInsert_memInsert_of_ne (addr := addr + 26) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 26) (by simp), memInsert_memInsert_of_ne (addr := addr + 26) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 26) (by simp), memInsert_memInsert_of_ne (addr := addr + 26) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 26) (by simp), memInsert_memInsert_of_ne (addr := addr + 26) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 26) (by simp), memInsert_memInsert_of_ne (addr := addr + 26) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 26) (by simp), memInsert_memInsert_of_ne (addr := addr + 26) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 26) (by simp), memInsert_memInsert_of_ne (addr := addr + 26) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 26) (by simp), memInsert_memInsert_of_ne (addr := addr + 26) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 26) (by simp), memInsert_memInsert_of_ne (addr := addr + 26) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 26) (by simp), memInsert_memInsert_of_ne (addr := addr + 26) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 26) (by simp), memInsert_memInsert_of_ne (addr := addr + 26) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 26) (by simp), memInsert_memInsert_of_ne (addr := addr + 26) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 27) (by simp), memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 27) (by simp), memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 27) (by simp), memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 27) (by simp), memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 27) (by simp), memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 27) (by simp), memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 27) (by simp), memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 27) (by simp), memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 27) (by simp), memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 27) (by simp), memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 27) (by simp), memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 27) (by simp), memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 27) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 28) (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 28) (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 28) (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 28) (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 28) (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 28) (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 28) (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 28) (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 28) (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 28) (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 28) (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 28) (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 28) (by simp), memInsert_memInsert_of_ne (addr := addr + 28) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp), memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 29) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 30) (by simp), memInsert_memInsert_of_ne (addr := addr + 30) (by simp) + , memInsert_memInsert ] + rw [ List.foldr_cons, List.foldl_cons + , memInsert_memInsert_of_ne (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp), memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert_of_ne (addr := addr + 31) (by simp) + , memInsert_memInsert ] + + rw [List.foldr_nil] + repeat rw [← List.foldl_cons] + simp only [List.reverse, List.reverseAux] + +lemma update_update_of_ne : + (h : ∀ {a}, a ∈ offsets_at addr' → a ∉ offsets_at addr) → + (ms.updateMemory addr val).updateMemory addr' val' = + (ms.updateMemory addr' val').updateMemory addr val := by + intro h + unfold MachineState.updateMemory + simp + apply And.intro + + swap + rw [← max_assoc, max_comm addr' addr, max_assoc] + + rw [ ← mkEntries, ← mkEntries ] + sorry + +lemma lt_toBytes_length_of_mem_offset : + ∀ {offset}, (v : UInt256) → (offset ∈ offsets) → offset < (toBytes! v).length := by + unfold offsets + simp + +lemma lookupBytes_nil : + ∀ {addr}, + [].map (ms.memory.lookupByte ∘ (addr + ↑·)) = [] := by + simp + +lemma lookupBytes_cons : + ∀ {addr} {offset : ℕ} {os : List ℕ}, + (offset :: os).map ((ms.updateMemory addr val).memory.lookupByte ∘ (addr + ↑·)) = + (ms.updateMemory addr val).memory.lookupByte (addr + ↑offset) + :: os.map ((ms.updateMemory addr val).memory.lookupByte ∘ (addr + ↑·)) := by + intro addr offset os + exact List.map_cons + ((ms.updateMemory addr val).memory.lookupByte ∘ (addr + ↑·)) + offset + os + +-- TODO: in newer mathlib +@[simp] theorem get!_some {α} [Inhabited α] {a : α} : (some a).get! = a := rfl + +-- lemma lookupByte_updateMemory : +-- ∀ {addr}, +-- (ms.updateMemory addr val).memory.lookupByte addr = +-- (UInt256.toBytes! val)[0] := by +-- intro addr +-- unfold MachineState.updateMemory Memory.lookupByte +-- simp +-- rw [ List.zipWith_foldl_eq_zip_foldl ] +-- conv => lhs; rw [splice_toBytes! val] +-- unfold offsets +-- simp only [List.map, List.zip, List.zipWith, List.foldl, flip, id] +-- norm_cast +-- rw [ Fin.add_zero addr ] +-- simp + +lemma lookupByte_update_of_ne : + ∀ {addr addr' : UInt256}, + (h : addr' ∉ offsets.map (addr + ↑·)) → + (ms.updateMemory addr val).memory.lookupByte addr' = + ms.memory.lookupByte addr' := by + intro addr addr' h + unfold MachineState.updateMemory Memory.lookupByte + simp + rw [splice_toBytes! val] + unfold offsets + simp [memInsert, List.foldr] + + unfold offsets at h + simp at h + repeat rw [← ne_eq] at h + let ⟨_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_⟩ := h + + rw [ Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne + , Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne + , Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne + , Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne + , Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne + , Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne + , Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne + , Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne + , Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne + , Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne + , Finmap.lookup_insert_of_ne, Finmap.lookup_insert_of_ne + ] + + all_goals assumption + +lemma lookupByte_at_offset_update : + ∀ {addr} {n}, (mem: n ∈ offsets) → + (ms.updateMemory addr val).memory.lookupByte (addr + ↑n) = + (UInt256.toBytes! val)[n]'(lt_toBytes_length_of_mem_offset val mem) := by + intro addr n mem + unfold MachineState.updateMemory Memory.lookupByte + simp + conv => lhs; rw [splice_toBytes! val] + unfold offsets + simp only [List.foldr] + norm_cast + fin_cases mem + · rw [ Nat.cast_zero, Fin.add_zero addr ] + simp + · rw [ Nat.cast_one ] + simp + all_goals simp only [ Nat.cast_ofNat, memInsert, Fin.isValue, List.getElem_eq_get + , Function.uncurry_apply_pair, add_zero, ne_eq, add_right_eq_self + , Fin.reduceEq, not_false_eq_true, Finmap.lookup_insert_of_ne + , add_right_inj, Finmap.lookup_insert, get!_some + ] + +lemma lookupByte_at_offset_update_of_ne {addr addr' : UInt256} : + ∀ {n}, (mem: n ∈ offsets) → + (h : addr' + ↑n ∉ offsets.map (addr + ↑·)) → + (ms.updateMemory addr val).memory.lookupByte (addr' + ↑n) = + ms.memory.lookupByte (addr' + ↑n) := by + intro n _ _ + apply lookupByte_update_of_ne (addr' := addr' + ↑n) + assumption + +lemma lookupWord_update : ∀ {addr}, + (ms.updateMemory addr val).memory.lookupWord addr = val := by + intro addr + unfold Memory.lookupWord offsets + repeat rw [ lookupBytes_cons, lookupByte_at_offset_update (by simp) ] + rw [ List.map_nil + , ← splice_toBytes! + , fromBytes!_toBytes! + ] + +lemma lookupWord_update_of_ne {addr addr' : UInt256} : + (h : ∀ {n}, (mem: n ∈ offsets) → addr' + ↑n ∉ offsets.map (addr + ↑·)) → + (ms.updateMemory addr val).memory.lookupWord addr' = ms.memory.lookupWord addr' := by + intro h + + unfold Memory.lookupWord + + rw [ ← List.map_comp_map + , Function.comp_apply + , ← List.map_comp_map + , Function.comp_apply + ] + simp only [List.map] + + rw [ lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + , lookupByte_at_offset_update_of_ne (by simp) (h (by simp)) + ] + +lemma lookupWord_update_of_next {addr : UInt256} : + (ms.updateMemory addr val).memory.lookupWord (addr + 32) = ms.memory.lookupWord (addr + 32) := by + refine lookupWord_update_of_ne (addr := addr) (addr' := addr + 32) ?h + intro n mem + fin_cases mem <;> (norm_cast; simp; intro x x_mem) + · fin_cases x_mem <;> norm_cast + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + · fin_cases x_mem <;> (norm_cast; try rw [add_assoc]; simp) + +lemma addr_no_overlap : ∀ {k : ℕ}, + (h : k < Memory.maxWords) → + addr + (k + 1) * 32 ∉ offsets.map (addr + ↑·) := by + intro k h + simp + intro x x_mem + apply ne_of_lt + norm_cast + + apply lt_of_le_of_lt (b := Nat.cast 31) + · rw [Fin.natCast_le_natCast (by linarith [lt_32_of_mem_offsets x_mem]) (by simp)] + apply Nat.le_of_lt_succ + exact lt_32_of_mem_offsets x_mem + · have succ_k_words_lt_size : + (k + 1) * 32 ≤ 115792089237316195423570985008687907853269984665640564039457584007913129639935 := by + trans Memory.maxWords * 32 + · simp + rw [Nat.succ_le] + exact h + · rw [Memory.maxWords] + simp + rw [Fin.natCast_lt_natCast (by simp) succ_k_words_lt_size] + apply Nat.lt_of_lt_of_le + · show (31 < 32); simp + · linarith + +end MachineState + +variable {addr addr' p : UInt256} +variable {evm : EVM} +variable {val val' : UInt256} + +lemma mstore_mstore : + mstore (mstore evm p val) p val' = mstore evm p val' := by + unfold mstore updateMemory + simp + exact update_update + +lemma mstore_mstore_of_ne : + mstore (mstore evm addr val) addr' val' = + mstore (mstore evm addr' val') addr val := by + unfold mstore updateMemory + simp + refine update_update_of_ne ?_ + sorry + +lemma lookup_mstore : + (mstore evm p val).machine_state.memory.lookupWord p = val := by + unfold mstore updateMemory + simp + rw [lookupWord_update] + +lemma lookup_mstore_of_ne {addr addr' : UInt256} : + (h : ∀ {n}, (mem: n ∈ offsets) → addr' + ↑n ∉ offsets.map (addr + ↑·)) → + (mstore evm addr val).machine_state.memory.lookupWord addr' = + evm.machine_state.memory.lookupWord addr' := by + intro h + unfold mstore updateMemory + rw [lookupWord_update_of_ne h] + +lemma lookup_mstore_of_next : + ∀ {k}, (h : k < Memory.maxWords) → + (mstore evm p val).machine_state.memory.lookupWord (p + (k + 1) * 32) = + evm.machine_state.memory.lookupWord (p + (k + 1) * 32) := by + sorry + +section Interval + +variable {p : UInt256} +variable {n : ℕ} +variable {evm : EVM} +variable {ms : MachineState} +variable {val : UInt256} + +lemma interval_of_0_eq_nil : + mkInterval ms.memory p 0 = [] := by + unfold mkInterval words_at + simp + +lemma interval_eq_lookup_cons : ∀ {n}, + mkInterval ms.memory p (n + 1) = + ms.memory.lookupWord p :: mkInterval ms.memory (p + 32) n := by + intro n + unfold mkInterval words_at + rw [range'_succ p n, List.map_cons] + +-- theorem List.range'_succ (s n step) : +-- List.range' s (n + 1) step = s :: List.range' (s + step) n step := by +-- simp [List.range', Nat.add_succ, Nat.mul_succ] + +-- lemma out_of_range : +-- ∀ {n}, (h : n ≤ Memory.maxWords) → +-- mkInterval (mstore evm p val).machine_state.memory (p + 32) n = +-- mkInterval evm.machine_state.memory (p + 32) n := by +-- intro n h +-- induction n generalizing p with +-- | zero => rw [zero_len_eq_nil, zero_len_eq_nil] +-- | succ n' ih => +-- have : (2 : UInt256) * 32 = (1 + 1) * 32 := sorry +-- rw [ succ_len_eq_cons +-- , ← one_mul 32, ← zero_add 1, ← Nat.cast_zero +-- , mstore_lookup_of_next (p := p) (k := 0) (by simp [Memory.maxWords]) +-- , Nat.cast_zero, zero_add 1, one_mul 32 +-- , add_assoc, ← two_mul 32 +-- , this ] +-- rw (config := {occs := .pos [1]}) [ ← Nat.cast_one ] +-- rw [ +-- ] + +lemma interval_of_mstore_eq_val_cons : + mkInterval (mstore evm p val).machine_state.memory p (n + 1) = + val :: mkInterval (mstore evm p val).machine_state.memory (p + 32) n := by + rw [ eq_lookup_cons, lookup_mstore ] + +lemma eq_val_cons' : + ∀ {n}, (h : n < Memory.maxWords) → + mkInterval (mstore evm p val).machine_state.memory p (n + 1) = + val :: mkInterval evm.machine_state.memory (p + 32) n := by + sorry + -- intro n h + -- induction n generalizing p with + -- | zero => admit + -- | succ n' => + -- rw [ succ_len_eq_cons, mstore_lookup, out_of_range (le_of_lt h) ] + +end Interval + end Clear.EVMState diff --git a/Clear/State.lean b/Clear/State.lean index 2d709b9..5d44041 100644 --- a/Clear/State.lean +++ b/Clear/State.lean @@ -389,6 +389,10 @@ lemma overwrite?_insert : (s.overwrite? (s'.insert var x)) = s.overwrite? s' unfold insert overwrite? rcases s' <;> simp +lemma insert_of_ok : (Ok evm store)⟦var ↦ val⟧ = Ok evm (store.insert var val) +:= by + rfl + -- | Looking up a variable you've just inserted gives you the value you inserted. @[simp] lemma lookup_insert : (Ok evm store)⟦var ↦ x⟧[var]!! = x diff --git a/Clear/Utilities.lean b/Clear/Utilities.lean index 434a984..afa4070 100644 --- a/Clear/Utilities.lean +++ b/Clear/Utilities.lean @@ -29,6 +29,25 @@ lemma spec_eq {P P' : State → State → Prop} {s₀ s₉ : State} : simp only exact h +@[aesop safe apply (rule_sets := [Clear.aesop_spec])] +lemma collision_spec_eq {P P' : State → State → Prop} {s₀ s₉ : State} : + (¬ s₉.evm.hash_collision → Spec P s₀ s₉ → Spec P' s₀ s₉) → CollidingSpec P s₀ s₉ → CollidingSpec P' s₀ s₉ := by + unfold CollidingSpec + intro S'_of_S + split + simp + intro Spec_of_c c + exact S'_of_S c (Spec_of_c c) + +@[aesop safe apply (rule_sets := [Clear.aesop_spec])] +lemma collision_spec_eq' {P P' : State → State → Prop} {s₀ s₉ : State} : + (¬ s₉.evm.hash_collision → ¬❓ s₉ → P s₀ s₉ → P' s₀ s₉) → CollidingSpec P s₀ s₉ → CollidingSpec P' s₀ s₉ := by + intro P'_of_P + apply collision_spec_eq + intro c + apply spec_eq + exact P'_of_P c + @[simp] lemma checkpt_insert_elim {var} {val} {j} : (.Checkpoint j)⟦var ↦ val⟧ = .Checkpoint j := by simp only [State.insert] 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 diff --git a/Generated/erc20shim/ERC20Shim/Predicate.lean b/Generated/erc20shim/ERC20Shim/Predicate.lean new file mode 100644 index 0000000..c387439 --- /dev/null +++ b/Generated/erc20shim/ERC20Shim/Predicate.lean @@ -0,0 +1,67 @@ +import Mathlib.Data.Finmap + +import Clear.State + +import Generated.erc20shim.ERC20Shim.Variables + +open Clear + +namespace Generated.erc20shim.ERC20Shim + +abbrev BalanceMap := Finmap (λ _ : Address ↦ UInt256) +abbrev AllowanceMap := Finmap (λ _ : Address × Address ↦ UInt256) + +structure ERC20 where + supply : UInt256 + balances : BalanceMap + allowances : AllowanceMap + +-- structure HasBalance (balances : BalanceMap) (account : Address) (s : State) where +-- address : Address +-- keccak : s.evm.keccak_map.lookup [ ↑account , ERC20Private.balances ] = some address +-- balance : some (s.evm.sload address) = balances.lookup account + +abbrev HasBalance (balances : BalanceMap) (account : Address) (s : State) := + ∃ address, + s.evm.keccak_map.lookup [ ↑account , ERC20Private.balances ] = some address ∧ + some (s.evm.sload address) = balances.lookup account + +namespace HasBalance + +variable {balances : BalanceMap} {account : Address} {s : State} + +-- theorem keccak (address(h : HasBalance balances account s) : +-- ∃ address, s.evm.keccak_map.lookup [ ↑account , ERC20Private.balances ] = some address := +-- let ⟨addr, keccak, _⟩ := h +-- ⟨addr, keccak⟩ + +-- theorem balance (h : HasBalance balances account s) : +-- ∃ address, some (s.evm.sload address) = balances.lookup account := +-- let ⟨addr, _, balance⟩ := h +-- ⟨addr, balance⟩ + +end HasBalance + +-- structure HasAllowance (allowances : AllowanceMap) (owner : Address) (spender : Address) (s : State) where +-- address : Address +-- keccak : s.evm.keccak_map.lookup [ ↑owner, ↑spender, ERC20Private.allowances ] = some address +-- allowance : some (s.evm.sload address) = allowances.lookup ⟨owner, spender⟩ + +def HasAllowance (allowances : AllowanceMap) (owner : Address) (spender : Address) (s : State) : Prop := + ∃ address, + s.evm.keccak_map.lookup [ ↑owner, ↑spender, ERC20Private.allowances ] = some address ∧ + some (s.evm.sload address) = allowances.lookup ⟨owner, spender⟩ + +-- def balance_predicate (erc20 : ERC20) (s : State) : Prop := +-- ∀ account, +-- account ∈ erc20.balances → HasBalance erc20.balances account s + +-- def balance_predicate (erc20 : ERC20) (s : State) : ? := +-- ∀ account, +-- account ∈ erc20.balances → HasBalance erc20.balances account s + +def allowance_predicate (erc20 : ERC20) (s : State) : Prop := + ∀ (owner spender : Address), + ⟨owner, spender⟩ ∈ erc20.allowances → HasAllowance erc20.allowances owner spender s + +end Generated.erc20shim.ERC20Shim diff --git a/Generated/erc20shim/ERC20Shim/Variables.lean b/Generated/erc20shim/ERC20Shim/Variables.lean index 75340a1..b7d0a1e 100644 --- a/Generated/erc20shim/ERC20Shim/Variables.lean +++ b/Generated/erc20shim/ERC20Shim/Variables.lean @@ -1,4 +1,10 @@ +import Mathlib.Data.Finmap +import Clear.Ast +import Clear.EVMState import Clear.UInt256 +import Clear.State + +open Clear namespace Generated.erc20shim.ERC20Shim @@ -12,4 +18,10 @@ structure PrivateAddresses where def ERC20Private : PrivateAddresses := { balances := 0, allowances := 1, totalSupply := 2, name := 3, symbol := 4 } + +def ERC20Pred (balances : Finmap (λ (_ : Address) ↦ UInt256)) (s : State) : Prop := + ∀ account, account ∈ balances → + ∃ addr, s.evm.keccak_map.lookup [ ↑account , ERC20Private.balances ] = some addr ∧ + some (s.evm.sload addr) = balances.lookup account + end Generated.erc20shim.ERC20Shim diff --git a/Generated/erc20shim/ERC20Shim/fun_balanceOf_user.lean b/Generated/erc20shim/ERC20Shim/fun_balanceOf_user.lean index daddd88..a97536c 100644 --- a/Generated/erc20shim/ERC20Shim/fun_balanceOf_user.lean +++ b/Generated/erc20shim/ERC20Shim/fun_balanceOf_user.lean @@ -1,9 +1,9 @@ import Clear.ReasoningPrinciple -import Generated.erc20shim.ERC20Shim.mapping_index_access_mapping_address_uint256_of_address - +-- import Generated.erc20shim.ERC20Shim.mapping_index_access_mapping_address_uint256_of_address import Generated.erc20shim.ERC20Shim.fun_balanceOf_gen +import Generated.erc20shim.ERC20Shim.Predicate namespace Generated.erc20shim.ERC20Shim @@ -11,13 +11,42 @@ section open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities Generated.erc20shim ERC20Shim -def A_fun_balanceOf (var : Identifier) (var_account : Literal) (s₀ s₉ : State) : Prop := sorry +def A_fun_balanceOf (var : Identifier) (var_account : Literal) (s₀ s₉ : State) : Prop := + ∀ erc20, balance_predicate erc20 s₀ → balance_predicate erc20 s₉ + + -- ∃ (s : State) (addr : UInt256), (s₉ = s⟦ var ↦ s.evm.sload addr ⟧) lemma fun_balanceOf_abs_of_concrete {s₀ s₉ : State} {var var_account} : Spec (fun_balanceOf_concrete_of_code.1 var var_account) s₀ s₉ → Spec (A_fun_balanceOf var var_account) s₀ s₉ := by - unfold fun_balanceOf_concrete_of_code A_fun_balanceOf - sorry + unfold fun_balanceOf_concrete_of_code A_fun_balanceOf + rcases s₀ with ⟨evm, varstore⟩ | _ | _ <;> [simp only; aesop_spec; aesop_spec] + apply spec_eq + clr_funargs + + intro hasFuel index_access erc20 pred_s₀ + + rcases index_access with ⟨sₖ, mapping, h'⟩ + -- clr_spec at mapping + + -- have sₖ_isOk : isOk sₖ := mapping_of_ok mapping (by simp) + -- rcases sₖ with ⟨evmₖ, _⟩ | _ | _ <;> try contradiction + -- use (Ok evmₖ varstore) + + -- simp at * + -- rw [ ← State.insert_of_ok, ← State.insert_of_ok + -- , State.lookup_insert + -- ] at h' + -- symm at h' + + -- by_cases h : evmₖ.hash_collision = true + -- · use 0 + -- rw [ lookup_addr_fail mapping h] at h' + -- assumption + -- · rcases lookup_addr_ok mapping (by aesop) with ⟨addr, lookup_eq_addr⟩ + -- use addr + -- rw [ lookup_eq_addr ] at h' + -- assumption end diff --git a/Generated/erc20shim/ERC20Shim/fun_totalSupply_user.lean b/Generated/erc20shim/ERC20Shim/fun_totalSupply_user.lean index a649948..637e33a 100644 --- a/Generated/erc20shim/ERC20Shim/fun_totalSupply_user.lean +++ b/Generated/erc20shim/ERC20Shim/fun_totalSupply_user.lean @@ -17,7 +17,20 @@ lemma fun_totalSupply_abs_of_concrete {s₀ s₉ : State} {var_ } : Spec (fun_totalSupply_concrete_of_code.1 var_ ) s₀ s₉ → Spec (A_fun_totalSupply var_ ) s₀ s₉ := by unfold fun_totalSupply_concrete_of_code A_fun_totalSupply - aesop_spec + rcases s₀ with ⟨evm, varstore⟩ | _ | _ <;> [simp only; aesop_spec; aesop_spec] + apply spec_eq + clr_funargs + intro hasFuel + + unfold reviveJump + simp + + rw [ ← State.insert_of_ok, ← State.insert_of_ok, ← State.insert_of_ok ] + clr_varstore + intro h + unfold ERC20Private; dsimp only + symm + assumption end diff --git a/Generated/erc20shim/ERC20Shim/mapping_index_access_mapping_address_uint256_of_address_user.lean b/Generated/erc20shim/ERC20Shim/mapping_index_access_mapping_address_uint256_of_address_user.lean index 9527d18..780f94f 100644 --- a/Generated/erc20shim/ERC20Shim/mapping_index_access_mapping_address_uint256_of_address_user.lean +++ b/Generated/erc20shim/ERC20Shim/mapping_index_access_mapping_address_uint256_of_address_user.lean @@ -3,6 +3,8 @@ import Clear.ReasoningPrinciple import Generated.erc20shim.ERC20Shim.mapping_index_access_mapping_address_uint256_of_address_gen +import Generated.erc20shim.ERC20Shim.Predicate +import Generated.erc20shim.ERC20Shim.Variables namespace Generated.erc20shim.ERC20Shim @@ -10,13 +12,92 @@ section open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities -def A_mapping_index_access_mapping_address_uint256_of_address (dataSlot : Identifier) (slot key : Literal) (s₀ s₉ : State) : Prop := - let s₁ := s₀ 🇪⟦ s₀.evm.mstore 0x00 (Address.ofUInt256 key) ⟧ - let s₂ := s₁ 🇪⟦ s₁.evm.mstore 0x20 slot ⟧ - match s₂.evm.keccak256 0x00 0x40 with - | some ⟨addr, evm⟩ => s₉ = s₂ 🇪⟦ evm ⟧⟦ dataSlot ↦ addr ⟧ - | none => s₉.evm.hash_collision = True +abbrev AddressMap := Finmap (λ _ : Address ↦ UInt256) +def A_mapping_index_access_mapping_address_uint256_of_address (dataSlot : Identifier) (slot key : Literal) (s₀ s₉ : State) : Prop := + let account := Address.ofUInt256 key + ∀ {map : AddressMap}, account ∈ map → + ∃ address, + s₀.evm.keccak_map.lookup [ ↑account , slot ] = some address ∧ + some (s₀.evm.sload address) = map.lookup account → + s₉ = s₀ ⟦ dataSlot ↦ address ⟧ + + -- account ∈ erc20.balances → + -- ∃ address, s₀.evm.keccak_map.lookup [ ↑account, ERC20Private.balances ] = some address → + -- s₉ = s₀ ⟦ dataSlot ↦ address ⟧ + + -- let s₁ := s₀ 🇪⟦ s₀.evm.mstore 0x00 (Address.ofUInt256 key) ⟧ + -- let s₂ := s₁ 🇪⟦ s₁.evm.mstore 0x20 slot ⟧ + -- match s₂.evm.keccak256 0x00 0x40 with + -- | some ⟨addr, evm⟩ => s₉ = s₂ 🇪⟦ evm ⟧⟦ dataSlot ↦ addr ⟧ + -- | none => s₉ = s₂ 🇪⟦ s₂.evm.addHashCollision ⟧ + +-- lemma mapping_of_ok {dataSlot : Identifier} {slot key : Literal} {s₀ s₉ : State} +-- : A_mapping_index_access_mapping_address_uint256_of_address dataSlot slot key s₀ s₉ → +-- isOk s₀ → isOk s₉ := by +-- intro mapping s₀_ok +-- unfold A_mapping_index_access_mapping_address_uint256_of_address at mapping + +-- have : s₀🇪⟦mstore s₀.evm 0 ↑↑(Address.ofUInt256 key)⟧.isOk := by +-- rw [isOk_setEvm] +-- assumption + +-- simp at mapping +-- rw [ evm_get_set_of_isOk s₀_ok +-- , evm_get_set_of_isOk this +-- ] at mapping + +-- -- split at mapping +-- -- <;> apply_fun isOk at mapping +-- -- <;> try rw [ isOk_insert ] at mapping +-- -- <;> [simp only [ isOk_setEvm ] at mapping; simp only [ isOk_setEvm ] at mapping] +-- -- <;> exact mapping.to_iff.mpr s₀_ok + +-- split at mapping <;> apply_fun isOk at mapping +-- · rw [ isOk_insert ] at mapping +-- rw [ isOk_setEvm, isOk_setEvm, isOk_setEvm] at mapping +-- exact mapping.to_iff.mpr s₀_ok +-- · rw [ isOk_setEvm, isOk_setEvm, isOk_setEvm] at mapping +-- exact mapping.to_iff.mpr s₀_ok + +-- lemma lookup_addr_fail {dataSlot : Identifier} {slot key : Literal} {s₀ s₉ : State} +-- : A_mapping_index_access_mapping_address_uint256_of_address dataSlot slot key s₀ s₉ → +-- s₉.evm.hash_collision = true → +-- s₉[dataSlot]!! = 0 := by +-- intro r_addr h +-- rcases s₀ with ⟨evm, varstore⟩ | _ | _ <;> [simp only; aesop_spec; aesop_spec] + +-- clr_funargs + +-- unfold A_mapping_index_access_mapping_address_uint256_of_address at r_addr +-- simp at r_addr + +-- sorry + +-- lemma lookup_addr_ok {dataSlot : Identifier} {slot key : Literal} {s₀ s₉ : State} +-- : A_mapping_index_access_mapping_address_uint256_of_address dataSlot slot key s₀ s₉ → +-- s₉.evm.hash_collision = false → +-- ∃ addr, s₉[dataSlot]!! = addr := by +-- intro r_addr +-- sorry + + -- unfold A_mapping_index_access_mapping_address_uint256_of_address at r_addr + -- simp at r_addr + + + -- unfold setEvm at r_addr + -- simp at r_addr + -- generalize prep_def + -- : (mstore s₀.evm 0 ↑↑(Address.ofUInt256 key)).mstore 32 slot = state_prep + -- at r_addr + + -- cases (b.evm.keccak256 0x00 0x40) with + -- | none => + + -- use 0 + -- sorry + -- | some a => sorry + -- Helper reifications lemma shift_eq_size : Fin.shiftLeft (n := UInt256.size) 1 160 = Address.size := by constructor @@ -26,27 +107,49 @@ lemma EVMAddrSize' {s : State} : (s, [Fin.shiftLeft 1 160]) = (s, [Address.size. exact shift_eq_size lemma mapping_index_access_mapping_address_uint256_of_address_abs_of_concrete {s₀ s₉ : State} {dataSlot slot key} : - Spec (mapping_index_access_mapping_address_uint256_of_address_concrete_of_code.1 dataSlot slot key) s₀ s₉ → - Spec (A_mapping_index_access_mapping_address_uint256_of_address dataSlot slot key) s₀ s₉ := by - unfold mapping_index_access_mapping_address_uint256_of_address_concrete_of_code A_mapping_index_access_mapping_address_uint256_of_address + CollidingSpec (mapping_index_access_mapping_address_uint256_of_address_concrete_of_code.1 dataSlot slot key) s₀ s₉ → + CollidingSpec (A_mapping_index_access_mapping_address_uint256_of_address dataSlot slot key) s₀ s₉ := by + unfold mapping_index_access_mapping_address_uint256_of_address_concrete_of_code A_mapping_index_access_mapping_address_uint256_of_address rcases s₀ with ⟨evm, varstore⟩ | _ | _ <;> [simp only; aesop_spec; aesop_spec] - apply spec_eq + apply collision_spec_eq' + + intro noCollision hasFuel + clr_funargs rw [ EVMSub', EVMShl', EVMAddrSize' ]; simp rw [ Address.and_size_eq_ofUInt256 ] rw [ multifill_cons, multifill_nil ] simp - + clr_varstore - generalize prep_def : (mstore evm 0 ↑↑(Address.ofUInt256 key)).mstore 32 slot = state_prep - - cases state_prep.keccak256 0 64 - · aesop_spec - · simp - unfold setEvm State.insert - aesop_spec + generalize acconut_def : Address.ofUInt256 key = account + + intro prog erc20 account_mem_balances + + rcases (Finmap.mem_iff.mp account_mem_balances) with ⟨bal, h_bal⟩ + sorry + -- use address + -- intro h_lookup + -- generalize prep_def : (mstore evm 0 ↑↑account).mstore 32 slot = state_prep + + -- have : Option.isSome $ state_prep.keccak256 0 64 := by + -- unfold keccak256 + -- unfold mkInterval + -- unfold MachineState.lookupMemory + -- unfold_let + + -- rw [ ← prep_def ] + -- unfold mstore updateMemory + -- sorry + + -- cases this + -- · simp + -- sorry + -- · simp + -- unfold setEvm State.insert + -- aesop_spec end