Precompiled contracts

Conform/TestRunner.lean

@@ -222,7 +222,7 @@ def executeTransactions (blocks : Blocks) (s₀ : EVM.State) : Except EVM.Except
               SYSTEM_ADDRESS
               SYSTEM_ADDRESS
               BEACON_ROOTS_ADDRESS
-              beaconRootsAddressCode
+              (.Code beaconRootsAddressCode)
               30000000
               0xe8d4a51000
               0

EvmYul.lean

@@ -12,6 +12,13 @@ import EvmYul.Wheels
 import EvmYul.EllipticCurves
 import EvmYul.PerformIO
 
+import EvmYul.SHA256
+import EvmYul.RIP160
+import EvmYul.BN_ADD
+import EvmYul.BN_MUL
+import EvmYul.SNARKV
+import EvmYul.BLAKE2_F
+
 import EvmYul.Data.Stack
 
 import EvmYul.EVM.Exception
@@ -20,6 +27,7 @@ import EvmYul.EVM.PrimOps
 import EvmYul.EVM.Semantics
 import EvmYul.EVM.State
 import EvmYul.EVM.StateOps
+import EvmYul.EVM.PrecompiledContracts
 
 import EvmYul.Maps.AccountMap
 import EvmYul.Maps.ByteMap

EvmYul/BLAKE2_F.lean

@@ -0,0 +1,16 @@
+import EvmYul.Wheels
+import EvmYul.PerformIO
+import Conform.Wheels
+
+def blobBLAKE2_F (data : String) : String :=
+  totallySafePerformIO ∘ IO.Process.run <|
+    pythonCommandOfInput data
+  where pythonCommandOfInput (data : String) : IO.Process.SpawnArgs := {
+    cmd := "python3",
+    args := #["EvmYul/EllipticCurvesPy/blake2_f.py", data]
+  }
+
+def BLAKE2_F (data : ByteArray) : Except String ByteArray :=
+  match blobBLAKE2_F (toHex data) with
+    | "error" => .error "BLAKE2_F failed"
+    | s => ByteArray.ofBlob s

EvmYul/BN_ADD.lean

@@ -0,0 +1,14 @@
+import EvmYul.Wheels
+import EvmYul.PerformIO
+import Conform.Wheels
+
+def blobBN_ADD (x₀ y₀ x₁ y₁ : String) : String :=
+  totallySafePerformIO ∘ IO.Process.run <|
+    pythonCommandOfInput x₀ y₀ x₁ y₁
+  where pythonCommandOfInput (x₀ y₀ x₁ y₁ : String) : IO.Process.SpawnArgs := {
+    cmd := "python3",
+    args := #["EvmYul/EllipticCurvesPy/bn_add.py", x₀, y₀, x₁, y₁]
+  }
+
+def BN_ADD (x₀ y₀ x₁ y₁ : ByteArray) : Except String ByteArray :=
+  ByteArray.ofBlob <| blobBN_ADD (toHex x₀) (toHex y₀) (toHex x₁) (toHex y₁)

EvmYul/BN_MUL.lean

@@ -0,0 +1,14 @@
+import EvmYul.Wheels
+import EvmYul.PerformIO
+import Conform.Wheels
+
+def blobBN_MUL (x₀ y₀ n : String) : String :=
+  totallySafePerformIO ∘ IO.Process.run <|
+    pythonCommandOfInput x₀ y₀ n
+  where pythonCommandOfInput (x₀ y₀ n : String) : IO.Process.SpawnArgs := {
+    cmd := "python3",
+    args := #["EvmYul/EllipticCurvesPy/bn_mul.py", x₀, y₀, n]
+  }
+
+def BN_MUL (x₀ y₀ n : ByteArray) : Except String ByteArray :=
+  ByteArray.ofBlob <| blobBN_MUL (toHex x₀) (toHex y₀) (toHex n)

EvmYul/EVM/Exception.lean

@@ -13,7 +13,6 @@ inductive InvalidTransactionException where
   | BaseFeeTooHigh : InvalidTransactionException
   | InconsistentFees : InvalidTransactionException
   | DataGreaterThan9152 : InvalidTransactionException
-  | SenderRecoverError : String → InvalidTransactionException
 
 instance : Repr InvalidTransactionException where
   reprPrec s _ :=
@@ -26,7 +25,6 @@ instance : Repr InvalidTransactionException where
       | .BaseFeeTooHigh       => "BaseFeeTooHigh"
       | .InconsistentFees     => "InconsistentFees"
       | .DataGreaterThan9152  => "DataGreaterThan9152"
-      | .SenderRecoverError s => "SenderRecoverError: " ++ s
 
 -- TODO - fix / cleanup.
 inductive Exception where
@@ -48,6 +46,7 @@ inductive Exception where
   | InvalidWithdrawal (s : String) : Exception
   | BogusExceptionToBeReplaced (s : String) : Exception
   | ExpectedException (s : String)          : Exception
+  | SenderRecoverError             : String → Exception
 
 instance : Repr Exception where
   reprPrec s _ := match s with
@@ -69,6 +68,7 @@ instance : Repr Exception where
                     | .InvalidWithdrawal s               => s!"InvalidWithdrawal: {s}"
                     | .BogusExceptionToBeReplaced s      => s!"BogusExceptionToBeReplaced: {s}"
                     | .ExpectedException s               => s!"Expected exception: {s}"
+                    | .SenderRecoverError s              => "SenderRecoverError: " ++ s
 
 end EVM
 

EvmYul/EVM/PrecompiledContracts.lean

@@ -0,0 +1,252 @@
+import EvmYul.Maps.AccountMap
+import EvmYul.UInt256
+import EvmYul.State.Substate
+import EvmYul.State.ExecutionEnv
+import EvmYul.EVM.Exception
+import EvmYul.Wheels
+
+import EvmYul.EllipticCurves
+import EvmYul.SHA256
+import EvmYul.RIP160
+import EvmYul.BN_ADD
+import EvmYul.BN_MUL
+import EvmYul.SNARKV
+import EvmYul.BLAKE2_F
+
+open EvmYul
+
+def Ξ_ECREC
+  (σ : AccountMap)
+  (g : UInt256)
+  (A : Substate)
+  (I : ExecutionEnv)
+    :
+  (AccountMap × UInt256 × Substate × ByteArray)
+:=
+  let gᵣ : UInt256 := 3000
+
+  if g < gᵣ then
+    (∅, 0, A, .empty)
+  else
+    let d := I.inputData
+    let h := d.readBytes 0 32
+    let v := d.readBytes 32 32
+    let r := d.readBytes 64 32
+    let s := d.readBytes 96 32
+    let v' : UInt256 := fromBytesBigEndian v.data.data
+    let r' : UInt256 := fromBytesBigEndian r.data.data
+    let s' : UInt256 := fromBytesBigEndian s.data.data
+    let o :=
+      match ECDSARECOVER h v r s with
+        | .ok s =>
+          if v' < 27 || 28 < v' || r' = 0 || r' >= secp256k1n || s' = 0 || s' >= secp256k1n then
+            .empty
+          else
+            ByteArray.zeroes ⟨12⟩ ++ (KEC s).extract 12 32
+        | .error e =>
+          dbg_trace s!"Ξ_ECREC failed: {e}"
+          .empty
+    (σ, g - gᵣ, A, o)
+
+def Ξ_SHA256
+  (σ : AccountMap)
+  (g : UInt256)
+  (A : Substate)
+  (I : ExecutionEnv)
+    :
+  (AccountMap × UInt256 × Substate × ByteArray)
+:=
+  let gᵣ : UInt256 :=
+    let l := I.inputData.size
+    let rem := l % 32
+    let divided := l / 32
+    let ceil := if rem == 0 then divided else divided + 1
+    60 + 12 * ceil
+
+  if g < gᵣ then
+    (∅, 0, A, .empty)
+  else
+    let o :=
+      match SHA256 I.inputData with
+        | .ok s => s
+        | .error e =>
+          dbg_trace s!"Ξ_SHA56 failed: {e}"
+          .empty
+    (σ, g - gᵣ, A, o)
+
+def Ξ_RIP160
+  (σ : AccountMap)
+  (g : UInt256)
+  (A : Substate)
+  (I : ExecutionEnv)
+    :
+  (AccountMap × UInt256 × Substate × ByteArray)
+:=
+  let gᵣ : UInt256 :=
+    let l := I.inputData.size
+    let rem := l % 32
+    let divided := l / 32
+    let ceil := if rem == 0 then divided else divided + 1
+    60 + 12 * ceil
+
+  if g < gᵣ then
+    (∅, 0, A, .empty)
+  else
+    let o :=
+      match RIP160 I.inputData with
+        | .ok s => s
+        | .error e =>
+          dbg_trace s!"Ξ_RIP160 failed: {e}"
+          .empty
+    (σ, g - gᵣ, A, o)
+
+def Ξ_ID
+  (σ : AccountMap)
+  (g : UInt256)
+  (A : Substate)
+  (I : ExecutionEnv)
+    :
+  (AccountMap × UInt256 × Substate × ByteArray)
+:=
+  let gᵣ : UInt256 :=
+    let l := I.inputData.size
+    let rem := l % 32
+    let divided := l / 32
+    let ceil := if rem == 0 then divided else divided + 1
+    15 + 3 * ceil
+
+  if g < gᵣ then
+    (∅, 0, A, .empty)
+  else
+    let o := I.inputData
+    (σ, g - gᵣ, A, o)
+
+def expModAux (m : ℕ) (a : ℕ) (c : ℕ) : ℕ → ℕ
+  | 0 => a % m
+  | n@(k + 1) =>
+    if n % 2 == 1 then
+      expModAux m (a * c % m) (c * c % m) (n / 2)
+    else
+      expModAux m (a % m)     (c * c % m) (n / 2)
+
+def expMod (m : ℕ) (b : UInt256) (n : ℕ) : ℕ := expModAux m 1 b n
+
+def Ξ_EXPMOD
+  (σ : AccountMap)
+  (g : UInt256)
+  (A : Substate)
+  (I : ExecutionEnv)
+    :
+  (AccountMap × UInt256 × Substate × ByteArray)
+:=
+  let d := I.inputData
+  let l_B := d.readBytes 0 32 |>.data.data |> fromBytesBigEndian
+  let l_E := d.readBytes 32 32 |>.data.data |> fromBytesBigEndian
+  let l_M := d.readBytes 64 32 |>.data.data |> fromBytesBigEndian
+  let B := d.readBytes 96 l_B |>.data.data |> fromBytesBigEndian
+  let E := d.readBytes (96 + l_B) l_E |>.data.data |> fromBytesBigEndian
+  let M := d.readBytes (96 + l_B + l_E) l_M |>.data.data |> fromBytesBigEndian
+
+  let l_E' :=
+    let E_firstWord := d.readBytes (96 + l_B) 32 |>.data.data |> fromBytesBigEndian
+    if l_E ≤ 32 && E == 0 then
+      0
+    else
+      if l_E ≤ 32 && E != 0 then
+        Nat.log 2 E
+      else
+        if 32 < l_E && E_firstWord != 0 then
+          8 * (l_E - 32) + (Nat.log 2 E_firstWord)
+        else
+          8 * (l_E - 32)
+
+  let gᵣ :=
+    let G_quaddivisor := 3
+    let f x :=
+      let rem := x % 8
+      let divided := x / 8
+      let ceil := if rem == 0 then divided else divided + 1
+      ceil ^ 2
+
+    max 200 (f (max l_M l_B) * max l_E' 1 / G_quaddivisor)
+
+  let o : ByteArray := BE (expMod M B E)
+  let o : ByteArray := ByteArray.zeroes ⟨l_M - o.size⟩ ++ o
+
+  (σ, g - gᵣ, A, o)
+
+def Ξ_BN_ADD
+  (σ : AccountMap)
+  (g : UInt256)
+  (A : Substate)
+  (I : ExecutionEnv)
+    :
+  (AccountMap × UInt256 × Substate × ByteArray)
+:=
+  let gᵣ : UInt256 := 150
+  let d := I.inputData
+  let x := (d.readBytes 0 32, d.readBytes 32 32)
+  let y := (d.readBytes 64 32, d.readBytes 96 32)
+  let o := BN_ADD x.1 x.2 y.1 y.2
+  match o with
+    | .ok o => (σ, g - gᵣ, A, o)
+    | .error e =>
+      dbg_trace s!"Ξ_BN_ADD failed: {e}"
+      (σ, g - gᵣ, A, .empty)
+
+def Ξ_BN_MUL
+  (σ : AccountMap)
+  (g : UInt256)
+  (A : Substate)
+  (I : ExecutionEnv)
+    :
+  (AccountMap × UInt256 × Substate × ByteArray)
+:=
+  let gᵣ : UInt256 := 6000
+  let d := I.inputData
+  let x := (d.readBytes 0 32, d.readBytes 32 32)
+  let n := d.readBytes 64 32
+  let o := BN_MUL x.1 x.2 n
+  match o with
+    | .ok o => (σ, g - gᵣ, A, o)
+    | .error e =>
+      dbg_trace s!"Ξ_BN_MUL failed: {e}"
+      (σ, g - gᵣ, A, .empty)
+
+def Ξ_SNARKV
+  (σ : AccountMap)
+  (g : UInt256)
+  (A : Substate)
+  (I : ExecutionEnv)
+    :
+  (AccountMap × UInt256 × Substate × ByteArray)
+:=
+  let d := I.inputData
+  let k := d.size / 192
+  let gᵣ : UInt256 := 34000 * k + 45000
+
+  let o := SNARKV d
+  match o with
+    | .ok o => (σ, g - gᵣ, A, o)
+    | .error e =>
+      dbg_trace s!"Ξ_SNARKV failed: {e}"
+      (∅, 0, A, .empty)
+
+def Ξ_BLAKE2_F
+  (σ : AccountMap)
+  (g : UInt256)
+  (A : Substate)
+  (I : ExecutionEnv)
+    :
+  (AccountMap × UInt256 × Substate × ByteArray)
+:=
+  let d := I.inputData
+  let k := d.size / 192
+  let gᵣ : UInt256 := 34000 * k + 45000
+
+  let o := BLAKE2_F d
+  match o with
+    | .ok o => (σ, g - gᵣ, A, o)
+    | .error e =>
+      dbg_trace s!"Ξ_BLAKE2_F failed: {e}"
+      (∅, 0, A, .empty)