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..dded202 100644 --- a/Clear/EVMState.lean +++ b/Clear/EVMState.lean @@ -1,8 +1,13 @@ 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 open Clear Instr UInt256 @@ -171,21 +176,156 @@ 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_le_32 : ∀ {n}, n < 32 → n ∈ offsets := + mem_offsets.mpr + +lemma le_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' {n} (start : UInt256) (len : Fin (n + 1)) (step : UInt256 := 1) : List UInt256 := + match start, len with + | _, 0 => [] + | s, ⟨n+1, _⟩ => s :: range' (s + step) ⟨n, by linarith⟩ step + +@[simp] +lemma range'_zero {s step : UInt256} : range' (n := 0) s 0 step = [] := by + unfold range' + rfl + +@[simp] +lemma range'_one {s step : UInt256} : range' (n := 1) s 1 step = [s] := by + unfold range' + simp + +lemma range'_succ {n} (start : UInt256) (len : Fin (n + 2)) (step : UInt256) [NeZero len] : + range' start len step = + start :: range' (start + step) (len.pred NeZero.out) step := by + have ne : len ≠ 0 := NeZero.out + obtain ⟨y, y_succ_eq_len⟩ := Fin.exists_succ_eq_of_ne_zero ne + simp_rw [← y_succ_eq_len] + conv => + lhs + unfold range' + simp + dsimp [Fin.succ] + + simp + + +-- lemma range'_eq_cons_iff +-- {s n a : UInt256} {xs : List UInt256} : +-- range' s n = a :: xs ↔ +-- s = a ∧ 0 < n ∧ xs = range' (a + 1) (n - 1) := sorry + +lemma map_add_range' (a) : ∀ s n step, + List.map (λ (x : UInt256) ↦ a + x) (range' s n step) = + range' (a + s) n step + | _, 0, _ => by simp + | s, ⟨n+1, _⟩, step => sorry + +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_le_32 h₂ + fin_cases h_offset + all_goals aesop + def MachineState.updateMemory (m : MachineState) (addr v : UInt256) : MachineState := - {m with memory := let offsets := List.range 32 - let addrs := offsets.map (·+addr) + {m with memory := let addrs := offsets.map (addr + ↑·) let inserts := addrs.zipWith Finmap.insert (UInt256.toBytes! v) inserts.foldl (init := m.memory) (flip id) 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 MachineState.lookupByte (m : MachineState) (addr : UInt256) : UInt8 := + (m.memory.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 MachineState.lookupWord (m : MachineState) (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 +333,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 +393,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 +407,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 @@ -296,8 +445,8 @@ def calldatacopy (σ : EVMState) (mstart datastart s : UInt256) : EVMState := 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 + let m := (List.range' i f 32).map Fin.ofNat + m.map ms.lookupWord def keccak256 (σ : EVMState) (p n : UInt256) : Option (UInt256 × EVMState) := let interval : List UInt256 := mkInterval σ.machine_state p n @@ -381,7 +530,7 @@ def selfbalance (σ : EVMState) : UInt256 := -- memory and storage operations def mload (σ : EVMState) (spos : UInt256) : UInt256 := - σ.machine_state.lookupMemory spos + σ.machine_state.lookupWord spos def mstore (σ : EVMState) (spos sval : UInt256) : EVMState := σ.updateMemory spos sval @@ -432,4 +581,206 @@ def evm_revert (σ : EVMState) (mstart s : UInt256) : EVMState := end +section Memory + +section MachineState + +variable {p n : UInt256} +variable {ms : MachineState} +variable {val : UInt256} + +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.lookupByte ∘ (addr + ↑·)) = [] := by + simp + +lemma lookupBytes_cons : + ∀ {addr} {offset : ℕ} {os : List ℕ}, + (offset :: os).map ((ms.updateMemory addr val).lookupByte ∘ (addr + ↑·)) = + (ms.updateMemory addr val).lookupByte (addr + ↑offset) + :: os.map ((ms.updateMemory addr val).lookupByte ∘ (addr + ↑·)) := by + intro addr offset os + exact List.map_cons + ((ms.updateMemory addr val).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).lookupByte addr = + (UInt256.toBytes! val)[0] := by + intro addr + unfold MachineState.updateMemory MachineState.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_updateMemory_of_ne : + ∀ {addr addr' : UInt256}, + (h : addr' ∉ offsets.map (addr + ↑·)) → + (ms.updateMemory addr val).lookupByte addr' = + ms.lookupByte addr' := by + intro addr addr' h + unfold MachineState.updateMemory MachineState.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 ] + + 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_updateMemory : + ∀ {addr} {n}, (mem: n ∈ offsets) → + (ms.updateMemory addr val).lookupByte (addr + ↑n) = + (UInt256.toBytes! val)[n]'(lt_toBytes_length_of_mem_offset val mem) := by + intro addr n mem + unfold MachineState.updateMemory MachineState.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 + fin_cases mem + · rw [ Nat.cast_zero, Fin.add_zero addr ] + simp + · rw [ Nat.cast_one ] + simp + all_goals simp only [ Nat.cast_ofNat, Fin.isValue, List.getElem_eq_get, add_zero, ne_eq + , add_right_inj, Fin.reduceEq, not_false_eq_true + , Finmap.lookup_insert_of_ne, Finmap.lookup_insert, get!_some + ] + +lemma lookupByte_at_offset_updateMemory_of_ne {addr addr' : UInt256} : + ∀ {n}, (mem: n ∈ offsets) → + (h : addr' + ↑n ∉ offsets.map (addr + ↑·)) → + (ms.updateMemory addr val).lookupByte (addr' + ↑n) = + ms.lookupByte (addr' + ↑n) := by + intro n mem h + apply lookupByte_updateMemory_of_ne (addr' := addr' + ↑n) + assumption + +lemma lookupWord_updateMemory : ∀ {addr}, (ms.updateMemory addr val).lookupWord addr = val := by + intro addr + unfold MachineState.lookupWord offsets + repeat rw [ lookupBytes_cons, lookupByte_at_offset_updateMemory (by simp) ] + rw [ List.map_nil + , ← splice_toBytes! + , fromBytes!_toBytes! + ] + +-- set_option maxHeartbeats 5000000 + +lemma lookupWord_updateMemory_of_ne {addr addr' : UInt256} : + ∀ {n}, (mem: n ∈ offsets) → + (h : addr' + ↑n ∉ offsets.map (addr + ↑·)) → + (ms.updateMemory addr val).lookupWord addr' = ms.lookupWord addr' := by + intro n mem h + + unfold MachineState.lookupWord + + rw [ ← List.map_comp_map + , Function.comp_apply + , ← List.map_comp_map + , Function.comp_apply + -- , Function.comp_def + ] + sorry + +-- lemma updateMemory_updateMemory : +-- ∀ {addr} {val val'}, +-- (ms.updateMemory addr val).updateMemory addr val' = ms.updateMemory addr val' := by +-- sorry + +end MachineState + +section Interval + +variable {p n : UInt256} +variable {evm : EVM} +variable {ms : MachineState} +variable {val : UInt256} + + -- mkInterval (mstore evm x v) x = v :: (mkInterval evm (x + 32)) + +lemma zero_len_eq_nil : + mkInterval ms p 0 = [] := by + unfold mkInterval + simp + +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 ofNat_of_val (k : UInt256) : (Fin.ofNat k.val : UInt256) = k := by + dsimp [Fin.ofNat] + simp_rw [ ← UInt256.size_def, Nat.mod_eq_of_lt k.isLt ] + rfl + +lemma succ_len_eq_cons [NeZero n] : + mkInterval (mstore evm p val).machine_state p n = + val :: mkInterval evm.machine_state (p + 1) (n - 1) := by + -- generalize k_def : n.pred h = k + -- have k : UInt256 := n.pred h + have ne : n.val ≠ 0 := Fin.val_ne_of_ne NeZero.out + have one_le_n : 1 ≤ n.val := Nat.one_le_iff_ne_zero.mpr ne + have u_def : Σ' u : ℕ, u.succ = ↑n := by + use (n.pred NeZero.out).val + simp + rw [Nat.sub_add_cancel one_le_n] + + let ⟨u, succ_u_eq_n⟩ := u_def + + unfold mstore mkInterval updateMemory + simp + rw [ ← succ_u_eq_n, List.range'_succ ↑p ↑u 1, List.map_cons ] + rw [Function.comp_apply] -- dsimp [(· ∘ ·)] + + have u_eq_pred_n : u = n - 1 := by + rw [← Nat.succ_inj] + dsimp + rw [Nat.sub_add_cancel one_le_n] + exact succ_u_eq_n + + rw [ ofNat_of_val p, @lookupWord_updateMemory evm.machine_state val p ] + rw [ u_eq_pred_n ] + simp + sorry + +end Memory.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 diff --git a/Generated/erc20shim/ERC20Shim/panic_error_0x11.lean b/Generated/erc20shim/ERC20Shim/panic_error_0x11.lean index 24cc0d7..0a72141 100644 --- a/Generated/erc20shim/ERC20Shim/panic_error_0x11.lean +++ b/Generated/erc20shim/ERC20Shim/panic_error_0x11.lean @@ -12,7 +12,7 @@ section open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities -lemma panic_error_0x11_abs_of_code {s₀ s₉ : State} } {fuel : Nat} : +lemma panic_error_0x11_abs_of_code {s₀ s₉ : State} {fuel : Nat} : execCall fuel panic_error_0x11 [] (s₀, []) = s₉ → Spec (A_panic_error_0x11 ) s₀ s₉ := λ h ↦ panic_error_0x11_abs_of_concrete (panic_error_0x11_concrete_of_code.2 h) diff --git a/Generated/erc20shim/ERC20Shim/panic_error_0x11_user.lean b/Generated/erc20shim/ERC20Shim/panic_error_0x11_user.lean index ac78615..77716bf 100644 --- a/Generated/erc20shim/ERC20Shim/panic_error_0x11_user.lean +++ b/Generated/erc20shim/ERC20Shim/panic_error_0x11_user.lean @@ -12,7 +12,7 @@ open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemma def A_panic_error_0x11 (s₀ s₉ : State) : Prop := sorry -lemma panic_error_0x11_abs_of_concrete {s₀ s₉ : State} } : +lemma panic_error_0x11_abs_of_concrete {s₀ s₉ : State} : Spec (panic_error_0x11_concrete_of_code.1 ) s₀ s₉ → Spec (A_panic_error_0x11 ) s₀ s₉ := by unfold panic_error_0x11_concrete_of_code A_panic_error_0x11 diff --git a/Generated/erc20shim/ERC20Shim/panic_error_0x22.lean b/Generated/erc20shim/ERC20Shim/panic_error_0x22.lean index e94476c..94f0264 100644 --- a/Generated/erc20shim/ERC20Shim/panic_error_0x22.lean +++ b/Generated/erc20shim/ERC20Shim/panic_error_0x22.lean @@ -12,7 +12,7 @@ section open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities -lemma panic_error_0x22_abs_of_code {s₀ s₉ : State} } {fuel : Nat} : +lemma panic_error_0x22_abs_of_code {s₀ s₉ : State} {fuel : Nat} : execCall fuel panic_error_0x22 [] (s₀, []) = s₉ → Spec (A_panic_error_0x22 ) s₀ s₉ := λ h ↦ panic_error_0x22_abs_of_concrete (panic_error_0x22_concrete_of_code.2 h) diff --git a/Generated/erc20shim/ERC20Shim/panic_error_0x22_user.lean b/Generated/erc20shim/ERC20Shim/panic_error_0x22_user.lean index 6cdddce..5ad3b95 100644 --- a/Generated/erc20shim/ERC20Shim/panic_error_0x22_user.lean +++ b/Generated/erc20shim/ERC20Shim/panic_error_0x22_user.lean @@ -12,7 +12,7 @@ open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemma def A_panic_error_0x22 (s₀ s₉ : State) : Prop := sorry -lemma panic_error_0x22_abs_of_concrete {s₀ s₉ : State} } : +lemma panic_error_0x22_abs_of_concrete {s₀ s₉ : State} : Spec (panic_error_0x22_concrete_of_code.1 ) s₀ s₉ → Spec (A_panic_error_0x22 ) s₀ s₉ := by unfold panic_error_0x22_concrete_of_code A_panic_error_0x22 diff --git a/Generated/erc20shim/ERC20Shim/panic_error_0x41.lean b/Generated/erc20shim/ERC20Shim/panic_error_0x41.lean index 033e1f0..b882fb4 100644 --- a/Generated/erc20shim/ERC20Shim/panic_error_0x41.lean +++ b/Generated/erc20shim/ERC20Shim/panic_error_0x41.lean @@ -12,7 +12,7 @@ section open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities -lemma panic_error_0x41_abs_of_code {s₀ s₉ : State} } {fuel : Nat} : +lemma panic_error_0x41_abs_of_code {s₀ s₉ : State} {fuel : Nat} : execCall fuel panic_error_0x41 [] (s₀, []) = s₉ → Spec (A_panic_error_0x41 ) s₀ s₉ := λ h ↦ panic_error_0x41_abs_of_concrete (panic_error_0x41_concrete_of_code.2 h) diff --git a/Generated/erc20shim/ERC20Shim/panic_error_0x41_user.lean b/Generated/erc20shim/ERC20Shim/panic_error_0x41_user.lean index 4826936..5e30215 100644 --- a/Generated/erc20shim/ERC20Shim/panic_error_0x41_user.lean +++ b/Generated/erc20shim/ERC20Shim/panic_error_0x41_user.lean @@ -12,7 +12,7 @@ open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemma def A_panic_error_0x41 (s₀ s₉ : State) : Prop := sorry -lemma panic_error_0x41_abs_of_concrete {s₀ s₉ : State} } : +lemma panic_error_0x41_abs_of_concrete {s₀ s₉ : State} : Spec (panic_error_0x41_concrete_of_code.1 ) s₀ s₉ → Spec (A_panic_error_0x41 ) s₀ s₉ := by unfold panic_error_0x41_concrete_of_code A_panic_error_0x41 diff --git a/Generated/erc20shim/ERC20Shim/revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74.lean b/Generated/erc20shim/ERC20Shim/revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74.lean index 97c0e34..6d1bc5f 100644 --- a/Generated/erc20shim/ERC20Shim/revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74.lean +++ b/Generated/erc20shim/ERC20Shim/revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74.lean @@ -12,7 +12,7 @@ section open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities -lemma revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74_abs_of_code {s₀ s₉ : State} } {fuel : Nat} : +lemma revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74_abs_of_code {s₀ s₉ : State} {fuel : Nat} : execCall fuel revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74 [] (s₀, []) = s₉ → Spec (A_revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74 ) s₀ s₉ := λ h ↦ revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74_abs_of_concrete (revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74_concrete_of_code.2 h) diff --git a/Generated/erc20shim/ERC20Shim/revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74_user.lean b/Generated/erc20shim/ERC20Shim/revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74_user.lean index 19aae0d..549228a 100644 --- a/Generated/erc20shim/ERC20Shim/revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74_user.lean +++ b/Generated/erc20shim/ERC20Shim/revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74_user.lean @@ -12,7 +12,7 @@ open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemma def A_revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74 (s₀ s₉ : State) : Prop := sorry -lemma revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74_abs_of_concrete {s₀ s₉ : State} } : +lemma revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74_abs_of_concrete {s₀ s₉ : State} : Spec (revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74_concrete_of_code.1 ) s₀ s₉ → Spec (A_revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74 ) s₀ s₉ := by unfold revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74_concrete_of_code A_revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74 diff --git a/Generated/erc20shim/ERC20Shim/revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb.lean b/Generated/erc20shim/ERC20Shim/revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb.lean index 71185ec..4a2bab6 100644 --- a/Generated/erc20shim/ERC20Shim/revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb.lean +++ b/Generated/erc20shim/ERC20Shim/revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb.lean @@ -12,7 +12,7 @@ section open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities -lemma revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb_abs_of_code {s₀ s₉ : State} } {fuel : Nat} : +lemma revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb_abs_of_code {s₀ s₉ : State} {fuel : Nat} : execCall fuel revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb [] (s₀, []) = s₉ → Spec (A_revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb ) s₀ s₉ := λ h ↦ revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb_abs_of_concrete (revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb_concrete_of_code.2 h) diff --git a/Generated/erc20shim/ERC20Shim/revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb_user.lean b/Generated/erc20shim/ERC20Shim/revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb_user.lean index 668329e..573eac3 100644 --- a/Generated/erc20shim/ERC20Shim/revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb_user.lean +++ b/Generated/erc20shim/ERC20Shim/revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb_user.lean @@ -12,7 +12,7 @@ open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemma def A_revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb (s₀ s₉ : State) : Prop := sorry -lemma revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb_abs_of_concrete {s₀ s₉ : State} } : +lemma revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb_abs_of_concrete {s₀ s₉ : State} : Spec (revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb_concrete_of_code.1 ) s₀ s₉ → Spec (A_revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb ) s₀ s₉ := by unfold revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb_concrete_of_code A_revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb diff --git a/Generated/erc20shim/ERC20Shim/revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b.lean b/Generated/erc20shim/ERC20Shim/revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b.lean index 45e55ba..c14848e 100644 --- a/Generated/erc20shim/ERC20Shim/revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b.lean +++ b/Generated/erc20shim/ERC20Shim/revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b.lean @@ -12,7 +12,7 @@ section open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities -lemma revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b_abs_of_code {s₀ s₉ : State} } {fuel : Nat} : +lemma revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b_abs_of_code {s₀ s₉ : State} {fuel : Nat} : execCall fuel revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b [] (s₀, []) = s₉ → Spec (A_revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b ) s₀ s₉ := λ h ↦ revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b_abs_of_concrete (revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b_concrete_of_code.2 h) diff --git a/Generated/erc20shim/ERC20Shim/revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b_user.lean b/Generated/erc20shim/ERC20Shim/revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b_user.lean index 8ef0836..c3df60e 100644 --- a/Generated/erc20shim/ERC20Shim/revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b_user.lean +++ b/Generated/erc20shim/ERC20Shim/revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b_user.lean @@ -12,7 +12,7 @@ open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemma def A_revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b (s₀ s₉ : State) : Prop := sorry -lemma revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b_abs_of_concrete {s₀ s₉ : State} } : +lemma revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b_abs_of_concrete {s₀ s₉ : State} : Spec (revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b_concrete_of_code.1 ) s₀ s₉ → Spec (A_revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b ) s₀ s₉ := by unfold revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b_concrete_of_code A_revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b diff --git a/vc/src/Main.hs b/vc/src/Main.hs index 6c76fef..e33cf2f 100644 --- a/vc/src/Main.hs +++ b/vc/src/Main.hs @@ -259,7 +259,7 @@ fillInFunction topLevelContract file imports (FuncDef _ contract fargs ret body) funcArgs = generateGuarded (null fargs) $ "(" ++ unwords fargs ++ " : Literal)" opens = opensOfImports topLevelContract imports retVals = generateGuarded (null ret) $ "(" ++ unwords ret ++ " : Identifier)" - rValsAndArgs = generateGuarded (null (ret ++ fargs)) "{" ++ unwords ret ++ " " ++ argsSepSpace ++ "}" + rValsAndArgs = generateGuarded (null (ret ++ fargs)) $ "{" ++ unwords ret ++ " " ++ argsSepSpace ++ "}" replaceIn ttype = replaceMany [ ("\\", leanImports ++ internalImports topLevelContract contract file ttype),