Upgrade to Lean 4.27.0 and update dependencies

Clear/EVMState.lean

@@ -22,9 +22,9 @@ def ByteArray.byteArrayToUInt256 (μ₀ : UInt256) (size : ℕ) (Id : ByteArray)
   open Array in
   let v₀ := μ₀.val
   let arr : ByteArray := extractBytes v₀ size Id
-  let arr1 : Array UInt8 := arr.data
+  let arr1 : Array UInt8 := arr.toArray
   -- converting to big endian
-  let step p v := (p.1 - 8, Fin.lor p.2 (Nat.shiftLeft v.val p.1))
+  let step p v := (p.1 - 8, Fin.lor p.2 (Nat.shiftLeft v.toNat p.1))
   let r : (ℕ × UInt256) := Array.foldl step ((size - 1) * 8, 0) arr1
   r.2
 
@@ -34,13 +34,15 @@ namespace Clear
 -- 2^160 https://www.wolframalpha.com/input?i=2%5E160
 def Address.size : Nat := 1461501637330902918203684832716283019655932542976
 
+instance : NeZero Address.size := ⟨by norm_num [Address.size]⟩
+
 abbrev Address : Type := Fin Address.size
 
-instance : Inhabited Address := ⟨Fin.ofNat 0⟩
+instance : Inhabited Address := ⟨Fin.ofNat Address.size 0⟩
 
-def Address.ofNat {n : ℕ} : Address := Fin.ofNat n
-def Address.ofUInt256 (v : UInt256) : Address := Fin.ofNat (v.val  % Address.size)
-instance {n : Nat} : OfNat Address n := ⟨Fin.ofNat n⟩
+def Address.ofNat {n : ℕ} : Address := Fin.ofNat Address.size n
+def Address.ofUInt256 (v : UInt256) : Address := Fin.ofNat Address.size (v.val  % Address.size)
+instance {n : Nat} : OfNat Address n := ⟨Fin.ofNat Address.size n⟩
 
 instance byteArrayDecEq : DecidableEq ByteArray := λ xs ys => by {
   rcases xs with ⟨ xs1 ⟩ ; rcases ys with ⟨ ys1 ⟩
@@ -187,7 +189,7 @@ def balanceOf (σ : EVMState) (k : UInt256) : UInt256 :=
   let addr : Address := Address.ofUInt256 k
   match Finmap.lookup addr σ.account_map with
   | .some act => act.balance
-  | .none => Fin.ofNat 0
+  | .none => 0
 
 -- functions for accessing memory
 
@@ -202,13 +204,13 @@ def calldataload (σ : EVMState) (v : UInt256) : UInt256 :=
 def calldatacopy (σ : EVMState) (mstart datastart s : UInt256) : EVMState :=
   let size := s.val
   let arr := extractBytes datastart.val size σ.execution_env.input_data
-  let r := arr.foldl (λ (sa , j) i => (EVMState.updateMemory sa j i.val, j + 1)) (σ , mstart)
+  let r := arr.foldl (λ (sa , j) i => (EVMState.updateMemory sa j i.toNat, 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
+  let m     := (List.range' i f).map (Fin.ofNat UInt256.size)
   m.map ms.lookupMemory
 
 def keccak256 (σ : EVMState) (p n : UInt256) : Option (UInt256 × EVMState) :=
@@ -247,7 +249,7 @@ def extCodeCopy (σ : EVMState) (act mstart cstart s : UInt256) : EVMState :=
     r.1
   | _ =>
     let size := s.val
-    let r := size.fold (λ _ (sa , j) => (EVMState.updateMemory sa j 0, j + 1)) (σ, mstart)
+    let r := (List.range size).foldl (λ (sa , j) _ => (EVMState.updateMemory sa j 0, j + 1)) (σ, mstart)
     r.1
 
 def extCodeHash (σ : EVMState) (v : UInt256) : UInt256 :=
@@ -288,7 +290,7 @@ def selfbalance (σ : EVMState) : UInt256 :=
   let addr := σ.execution_env.code_owner
   match Finmap.lookup addr σ.account_map with
   | .some act => act.balance
-  | .none => Fin.ofNat 0
+  | .none => 0
 
 -- memory and storage operations
 
@@ -299,7 +301,7 @@ def mstore (σ : EVMState) (spos sval : UInt256) : EVMState :=
   σ.updateMemory spos sval
 
 def mstore8 (σ : EVMState) (spos sval : UInt256) : EVMState :=
-  σ.updateMemory spos (Fin.ofNat (sval.val % 256))
+  σ.updateMemory spos (Fin.ofNat UInt256.size (sval.val % 256))
 
 def sload (σ : EVMState) (spos : UInt256) : UInt256 :=
   match σ.lookupAccount σ.execution_env.code_owner with
@@ -331,13 +333,13 @@ def returndatacopy (σ : EVMState) (mstart rstart s : UInt256) : Option EVMState
   else
     let arr := σ.machine_state.return_data.toArray
     let rdata := arr.extract rstart.val (rstart.val + s.val - 1)
-    let s := rdata.data.foldr (λ v (ac,p) => (ac.updateMemory p v, p +1)) (σ , mstart)
+    let s := rdata.toList.foldr (λ v (ac,p) => (ac.updateMemory p v, p +1)) (σ , mstart)
     .some s.1
 
 def evm_return (σ : EVMState) (mstart s : UInt256) : EVMState :=
   let arr := σ.machine_state.return_data.toArray
   let vals := extractFill mstart.val s.val arr
-  {σ with machine_state := σ.machine_state.setReturnData vals.data}
+  {σ with machine_state := σ.machine_state.setReturnData vals.toList}
 
 def evm_revert (σ : EVMState) (mstart s : UInt256) : EVMState :=
   σ.evm_return mstart s

Clear/Instr.lean

@@ -1,4 +1,4 @@
-import Mathlib.Data.Nat.Defs
+import Mathlib.Data.Nat.Basic
 import Clear.UInt256
 
 inductive AInstr : Type where

Clear/Interpreter.lean

@@ -1,5 +1,4 @@
 import Mathlib.Data.Finmap
-import Mathlib.Init.Data.List.Lemmas
 
 import Clear.Ast
 import Clear.State

Clear/SizeLemmas.lean

@@ -25,27 +25,27 @@ lemma Zero.zero_le {n : ℕ} : Zero.zero ≤ n := by ring_nf; exact Nat.zero_le
 @[simp]
 lemma List.zero_lt_sizeOf : 0 < sizeOf xs
 := by
-  rcases xs <;> simp_arith
+  rcases xs <;> simp +arith
 
 @[simp]
 lemma List.reverseAux_size : sizeOf (List.reverseAux args args') = sizeOf args + sizeOf args' - 1 := by
   induction args generalizing args' with
-    | nil => simp_arith
+    | nil => simp +arith
     | cons z zs ih =>
       aesop (config := {warnOnNonterminal := false}); omega
 
 @[simp]
 lemma List.reverse_size : sizeOf (args.reverse) = sizeOf args := by
   unfold List.reverse
   rw [List.reverseAux_size]
-  simp_arith
+  simp +arith
 
 /--
   Expressions have positive size.
 -/ 
 @[simp]
 lemma Expr.zero_lt_sizeOf : 0 < sizeOf expr := by
-  rcases expr <;> simp_arith
+  rcases expr <;> simp +arith
 
 @[simp]
 lemma Stmt.sizeOf_stmt_ne_0 : sizeOf stmt ≠ 0 := by cases stmt <;> aesop
@@ -68,11 +68,11 @@ lemma Expr.zero_lt_sizeOf_List : 0 < sizeOf exprs := by
 
 @[simp]
 lemma Expr.sizeOf_head_lt_sizeOf_List : sizeOf expr < sizeOf (expr :: exprs) := by
-  simp_arith
+  simp +arith
 
 @[simp]
 lemma Expr.sizeOf_tail_lt_sizeOf_List : sizeOf exprs < sizeOf (expr :: exprs) := by
-  simp_arith
+  simp +arith
 
 /--
   Lists of statements have positive size.
@@ -88,11 +88,11 @@ lemma FunctionDefinition.zero_lt_sizeOf : 0 < sizeOf f := by cases f; aesop
 
 @[simp]
 lemma Expr.sizeOf_args_lt_sizeOf_Call : sizeOf args < sizeOf (Call f args) := by
-  simp_arith
+  simp +arith
 
 @[simp]
 lemma Expr.sizeOf_args_lt_sizeOf_PrimCall : sizeOf args < sizeOf (PrimCall prim args) := by
-  simp_arith
+  simp +arith
 
 /--
   The size of the body of a function is less than the size of the function itself.
@@ -103,7 +103,7 @@ lemma FunctionDefinition.sizeOf_body_lt_sizeOf : sizeOf (body f) < sizeOf f := b
 lemma FunctionDefinition.sizeOf_body_succ_lt_sizeOf : sizeOf (FunctionDefinition.body f) + 1 < sizeOf f := by
   cases f
   unfold body
-  simp_arith
+  simp +arith
   exact le_add_right List.zero_lt_sizeOf
 
 /--

Clear/UInt256.lean

@@ -1,11 +1,11 @@
 import Init.Data.Nat.Div
-import Mathlib.Data.Nat.Defs
+import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Fin.Basic
 import Mathlib.Data.Vector.Basic
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Algebra.Ring.Basic
-import Mathlib.Algebra.Order.Floor
+import Mathlib.Algebra.Order.Floor.Defs
 import Mathlib.Data.ZMod.Defs
 import Mathlib.Tactic
 
@@ -20,11 +20,11 @@ abbrev UInt256 := Fin UInt256.size
 instance : SizeOf UInt256 where
   sizeOf := 1
 
-instance (n : ℕ) : OfNat UInt256 n := ⟨Fin.ofNat n⟩
+instance (n : ℕ) : OfNat UInt256 n := ⟨Fin.ofNat UInt256.size n⟩
 instance : Inhabited UInt256 := ⟨0⟩
-instance : NatCast UInt256 := ⟨Fin.ofNat⟩
+instance : NatCast UInt256 := ⟨Fin.ofNat UInt256.size⟩
 
-abbrev Nat.toUInt256 : ℕ → UInt256 := Fin.ofNat
+abbrev Nat.toUInt256 : ℕ → UInt256 := Fin.ofNat UInt256.size
 abbrev UInt8.toUInt256 (a : UInt8) : UInt256 := a.toNat.toUInt256
 
 def Bool.toUInt256 (b : Bool) : UInt256 := if b then 1 else 0
@@ -120,7 +120,7 @@ def signextend (a b : UInt256) : UInt256 :=
 -- | Convert from a list of little-endian bytes to a natural number.
 def fromBytes' : List UInt8 → ℕ
 | [] => 0
-| b :: bs => b.val.val + 2^8 * fromBytes' bs
+| b :: bs => b.toNat + 2^8 * fromBytes' bs
 
 variable {bs : List UInt8}
          {n : ℕ}
@@ -131,7 +131,7 @@ private lemma fromBytes'_le : fromBytes' bs < 2^(8 * bs.length) := by
   | nil => unfold fromBytes'; simp
   | cons b bs ih =>
     unfold fromBytes'
-    have h := b.val.isLt
+    have h := b.toNat_lt
     simp only [List.length_cons, Nat.mul_succ, Nat.add_comm, Nat.pow_add]
     have :=
       Nat.add_le_of_le_sub
@@ -148,13 +148,12 @@ private lemma fromBytes'_UInt256_le (h : bs.length = 32) : fromBytes' bs < 2^256
 -- | Convert a natural number into a list of bytes.
 private def toBytes' : ℕ → List UInt8
   | 0 => []
-  | n@(.succ n') =>
-    let byte : UInt8 := ⟨Nat.mod n UInt8.size, Nat.mod_lt _ (by linarith)⟩
-    have : n / UInt8.size < n' + 1 := by
-      rename_i h
-      rw [h]
-      apply Nat.div_lt_self <;> simp
+  | n@(.succ _) =>
+    let byte : UInt8 := UInt8.ofNat n
     byte :: toBytes' (n / UInt8.size)
+termination_by n => n
+decreasing_by
+  exact Nat.div_lt_self (Nat.succ_pos _) (by decide)
 
 -- | If n < 2⁸ᵏ, then (toBytes' n).length ≤ k.
 private lemma toBytes'_le {k : ℕ} (h : n < 2 ^ (8 * k)) : (toBytes' n).length ≤ k := by
@@ -207,11 +206,14 @@ private lemma fromBytes'_toBytes' {x : ℕ} : fromBytes' (toBytes' x) = x := by
   | .zero => simp [toBytes', fromBytes']
   | .succ n =>
     unfold toBytes' fromBytes'
-    simp only
-    have := Nat.div_lt_self (Nat.zero_lt_succ n) (by decide : 1 < UInt8.size)
     rw [fromBytes'_toBytes']
-    simp [UInt8.size, add_comm]
-    apply Nat.div_add_mod
+    have hbyte : (UInt8.ofNat n.succ).toNat = n.succ % UInt8.size := by
+      simp [UInt8.toNat_ofNat, UInt8.size]
+    rw [hbyte, show UInt8.size = 256 from rfl, show (2:ℕ)^8 = 256 from by decide]
+    omega
+termination_by x
+decreasing_by
+  exact Nat.div_lt_self (Nat.succ_pos _) (by decide)
 
 def fromBytes! (bs : List UInt8) : ℕ := fromBytes' (bs.take 32)
 
@@ -220,7 +222,7 @@ private lemma fromBytes_was_good_all_year_long
   have h' := @fromBytes'_le bs
   rw [pow_mul] at h'
   refine lt_of_lt_of_le (b := (2 ^ 8) ^ List.length bs) h' ?lenBs
-  case lenBs => rw [←pow_mul]; exact pow_le_pow_right (by decide) (by linarith)
+  case lenBs => rw [←pow_mul]; exact Nat.pow_le_pow_right (by decide) (by linarith)
 
 @[simp]
 lemma fromBytes_wasnt_naughty : fromBytes! bs < 2^256 := fromBytes_was_good_all_year_long (by simp)
@@ -239,15 +241,19 @@ lemma UInt256_pow_def {a b : UInt256} : a ^ b = a ^ b.val := by
   rfl
 
 lemma UInt256_pow_succ {a b : UInt256} (h : b.val + 1 < UInt256.size) : a * a ^ b = a ^ (b + 1) := by
-  rw [UInt256_pow_def, UInt256_pow_def]
-  have : (↑(b + 1) : ℕ) = (b + 1 : ℕ) := by rw [Fin.val_add, Nat.mod_eq_of_lt (by norm_cast)]; rfl
-  rw [this]
-  ring
-
-lemma UInt256_zero_pow {a : UInt256} (h : a.val ≠ 0) : (0 : UInt256) ^ a = 0 := zero_pow h
+  simp only [UInt256_pow_def]
+  have hval : (b + 1 : UInt256).val = b.val + 1 := by
+    simp only [Fin.val_add, Fin.val_one]
+    exact Nat.mod_eq_of_lt h
+  rw [hval, pow_succ]
+  exact mul_comm _ _
+
+lemma UInt256_zero_pow {a : UInt256} (h : a.val ≠ 0) : (0 : UInt256) ^ a = 0 := by
+  simp only [UInt256_pow_def]
+  rcases Nat.exists_eq_succ_of_ne_zero h with ⟨n, hn⟩
+  rw [hn, pow_succ, mul_zero]
 
 lemma UInt256_pow_zero {a : UInt256} : a ^ (0 : UInt256) = 1 := by
-  unfold HPow.hPow instHPowUInt256
-  simp
+  simp [UInt256_pow_def]
 
 end Clear.UInt256