diff --git a/Conform/TestRunner.lean b/Conform/TestRunner.lean index 3666016..3f9bfa1 100644 --- a/Conform/TestRunner.lean +++ b/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 diff --git a/EvmYul.lean b/EvmYul.lean index b2ad8b7..2d22315 100644 --- a/EvmYul.lean +++ b/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 diff --git a/EvmYul/BLAKE2_F.lean b/EvmYul/BLAKE2_F.lean new file mode 100644 index 0000000..b0eb71e --- /dev/null +++ b/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 diff --git a/EvmYul/BN_ADD.lean b/EvmYul/BN_ADD.lean new file mode 100644 index 0000000..4d5bce0 --- /dev/null +++ b/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₁) diff --git a/EvmYul/BN_MUL.lean b/EvmYul/BN_MUL.lean new file mode 100644 index 0000000..a538f9c --- /dev/null +++ b/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) diff --git a/EvmYul/EVM/Exception.lean b/EvmYul/EVM/Exception.lean index 673e4b4..ab129a5 100644 --- a/EvmYul/EVM/Exception.lean +++ b/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 diff --git a/EvmYul/EVM/PrecompiledContracts.lean b/EvmYul/EVM/PrecompiledContracts.lean new file mode 100644 index 0000000..23a5cc2 --- /dev/null +++ b/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) diff --git a/EvmYul/EVM/Semantics.lean b/EvmYul/EVM/Semantics.lean index bf2e451..aec68ae 100644 --- a/EvmYul/EVM/Semantics.lean +++ b/EvmYul/EVM/Semantics.lean @@ -17,6 +17,7 @@ import EvmYul.EVM.State import EvmYul.EVM.StateOps import EvmYul.EVM.Exception import EvmYul.EVM.Instr +import EvmYul.EVM.PrecompiledContracts import EvmYul.Operations import EvmYul.Pretty @@ -354,9 +355,8 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti | _ => .error .InvalidStackSizeException -- TODO: Factor out the semantics for `CALL`, `CALLCODE`, `DELEGATECALL`, `STATICCALL` - | .CALL => + | .CALL => do -- dbg_trace /- op -/ "CALL" - do -- Names are from the YP, these are: -- μ₀ - gas -- μ₁ - to @@ -377,8 +377,6 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti if μ₂ ≤ (evmState.accountMap.find? evmState.executionEnv.codeOwner |>.option 0 Account.balance) ∧ evmState.executionEnv.depth < 1024 then -- dbg_trace s!"DBG REMOVE; Calling address: {t}" let A' := evmState.addAccessedAccount t |>.substate -- A' ≡ A except A'ₐ ≡ Aₐ ∪ {t} - let .some tDirect := evmState.accountMap.find? t | default - let tDirect := tDirect.code -- We use the code directly without an indirection a'la `codeMap[t]`. -- dbg_trace s!"looking up memory range: {evmState.toMachineState.readBytes μ₃ μ₄}" let (i, newMachineState) := evmState.toMachineState.readBytes μ₃ μ₄ -- m[μs[3] . . . (μs[3] + μs[4] − 1)] let resultOfΘ ← @@ -390,7 +388,7 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti (s := evmState.executionEnv.codeOwner) -- Iₐ in Θ(.., Iₐ, ..) (o := evmState.executionEnv.sender) -- Iₒ in Θ(.., Iₒ, ..) (r := t) -- t in Θ(.., t, ..) - (c := tDirect) -- t in Θ(.., t, ..) except 'dereferenced' + (c := toExecute evmState.accountMap t) -- t in Θ(.., t, ..) except 'dereferenced' (g := μ₀) -- TODO gas - CCALLGAS(σ, μ, A) (p := evmState.executionEnv.gasPrice) -- Iₚ in Θ(.., Iₚ, ..) (v := μ₂) -- μₛ[2] in Θ(.., μₛ[2], ..) @@ -461,7 +459,6 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti -- dbg_trace s!"DBG REMOVE; Calling address: {t}" let A' := evmState.addAccessedAccount t |>.substate -- A' ≡ A except A'ₐ ≡ Aₐ ∪ {t} let .some tDirect := evmState.accountMap.find? t | default - let tDirect := tDirect.code -- We use the code directly without an indirection a'la `codeMap[t]`. -- dbg_trace s!"looking up memory range: {evmState.toMachineState.readBytes μ₃ μ₄}" let (i, newMachineState) := evmState.toMachineState.readBytes μ₃ μ₄ -- m[μs[3] . . . (μs[3] + μs[4] − 1)] let resultOfΘ ← @@ -473,8 +470,8 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti (A := A') -- A* in Θ(.., A*, ..) (s := evmState.executionEnv.codeOwner) -- Iₐ in Θ(.., Iₐ, ..) (o := evmState.executionEnv.sender) -- Iₒ in Θ(.., Iₒ, ..) - (r := evmState.executionEnv.codeOwner) -- t in Θ(.., t, ..) - (c := tDirect) -- t in Θ(.., t, ..) except 'dereferenced' + (r := evmState.executionEnv.codeOwner) -- t in Θ(.., t, ..) + (c := toExecute evmState.accountMap t) -- t in Θ(.., t, ..) except 'dereferenced' (g := μ₀) -- TODO gas - CCALLGAS(σ, μ, A) (p := evmState.executionEnv.gasPrice) -- Iₚ in Θ(.., Iₚ, ..) (v := μ₂) -- μₛ[2] in Θ(.., μₛ[2], ..) @@ -559,14 +556,14 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti (createdAccounts := evmState.createdAccounts) (σ := evmState.accountMap) -- σ in Θ(σ, ..) (A := A') -- A* in Θ(.., A*, ..) - (s := evmState.executionEnv.source) -- Iₛ in Θ(.., Iₐ, ..) + (s := evmState.executionEnv.source) -- Iₛ in Θ(.., Iₐ, ..) (o := evmState.executionEnv.sender) -- Iₒ in Θ(.., Iₒ, ..) - (r := evmState.executionEnv.codeOwner) -- t in Θ(.., t, ..) - (c := tDirect) -- t in Θ(.., t, ..) except 'dereferenced' + (r := evmState.executionEnv.codeOwner) -- t in Θ(.., t, ..) + (c := toExecute evmState.accountMap t) -- t in Θ(.., t, ..) except 'dereferenced' (g := μ₀) -- TODO gas - CCALLGAS(σ, μ, A) (p := evmState.executionEnv.gasPrice) -- Iₚ in Θ(.., Iₚ, ..) - (v := 0) -- μₛ[2] in Θ(.., μₛ[2], ..) - (v' := evmState.executionEnv.weiValue) -- μₛ[2] in Θ(.., μₛ[2], ..) + (v := 0) -- μₛ[2] in Θ(.., μₛ[2], ..) + (v' := evmState.executionEnv.weiValue) -- μₛ[2] in Θ(.., μₛ[2], ..) (d := i) -- i in Θ(.., i, ..) (e := evmState.executionEnv.depth + 1) -- Iₑ + 1 in Θ(.., Iₑ + 1, ..) (H := evmState.executionEnv.header) @@ -649,11 +646,11 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti (s := evmState.executionEnv.codeOwner) -- Iₐ in Θ(.., Iₐ, ..) (o := evmState.executionEnv.sender) -- Iₒ in Θ(.., Iₒ, ..) (r := t) -- t in Θ(.., t, ..) - (c := tDirect) -- t in Θ(.., t, ..) except 'dereferenced' + (c := toExecute evmState.accountMap t) -- t in Θ(.., t, ..) except 'dereferenced' (g := μ₀) -- TODO gas - CCALLGAS(σ, μ, A) (p := evmState.executionEnv.gasPrice) -- Iₚ in Θ(.., Iₚ, ..) - (v := 0) -- μₛ[2] in Θ(.., μₛ[2], ..) - (v' := 0) -- μₛ[2] in Θ(.., μₛ[2], ..) + (v := 0) -- μₛ[2] in Θ(.., μₛ[2], ..) + (v' := 0) -- μₛ[2] in Θ(.., μₛ[2], ..) (d := i) -- i in Θ(.., i, ..) (e := evmState.executionEnv.depth + 1) -- Iₑ + 1 in Θ(.., Iₑ + 1, ..) (H := evmState.executionEnv.header) @@ -1037,7 +1034,7 @@ def Θ (debugMode : Bool) (s : AccountAddress) (o : AccountAddress) (r : AccountAddress) - (c : ByteArray) + (c : ToExecute) (g : UInt256) (p : UInt256) (v : UInt256) @@ -1086,14 +1083,49 @@ def Θ (debugMode : Bool) weiValue := v' -- Equation (137) depth := e -- Equation (138) perm := w -- Equation (139) - code := c -- Note that we don't use an address, but the actual code. Equation (141)-ish. + -- Note that we don't use an address, but the actual code. Equation (141)-ish. + code := + match c with + | ToExecute.Precompiled _ => default + | ToExecute.Code code => code header := H } - -- Equation (131) -- Note that the `c` used here is the actual code, not the address. TODO - Handle precompiled contracts. - let (createdAccounts, σ'', g'', A'', out) ← Ξ debugMode fuel createdAccounts σ₁ g A I + let (createdAccounts, σ'', g'', A'', out) ← + match c with + | ToExecute.Precompiled p => + match p with + | 1 => + let (σ', g', A', o) := Ξ_ECREC σ₁ g A I + .ok (∅, σ', g', A', some o) + | 2 => + let (σ', g', A', o) := Ξ_SHA256 σ₁ g A I + .ok (∅, σ', g', A', some o) + | 3 => + let (σ', g', A', o) := Ξ_RIP160 σ₁ g A I + .ok (∅, σ', g', A', some o) + | 4 => + let (σ', g', A', o) := Ξ_ID σ₁ g A I + .ok (∅, σ', g', A', some o) + | 5 => + let (σ', g', A', o) := Ξ_EXPMOD σ₁ g A I + .ok (∅, σ', g', A', some o) + | 6 => + let (σ', g', A', o) := Ξ_BN_ADD σ₁ g A I + .ok (∅, σ', g', A', some o) + | 7 => + let (σ', g', A', o) := Ξ_BN_MUL σ₁ g A I + .ok (∅, σ', g', A', some o) + | 8 => + let (σ', g', A', o) := Ξ_SNARKV σ₁ g A I + .ok (∅, σ', g', A', some o) + | 9 => + let (σ', g', A', o) := Ξ_BLAKE2_F σ₁ g A I + .ok (∅, σ', g', A', some o) + | _ => default + | ToExecute.Code _ => Ξ debugMode fuel createdAccounts σ₁ g A I -- dbg_trace s!"σ'' after Ξ: {repr σ''}" -- Equation (127) let σ' := if σ'' == ∅ then σ else σ'' @@ -1120,7 +1152,6 @@ def checkTransactionGetSender (σ : YPState) (chainId H_f : ℕ) (T : Transactio -- dbg_trace "Transaction: {repr T}" let some T_RLP := RLP (← (L_X T)) | .error <| .InvalidTransaction .IllFormedRLP - let secp256k1n : ℕ := 115792089237316195423570985008687907852837564279074904382605163141518161494337 let r : ℕ := fromBytesBigEndian T.base.r.data.data let s : ℕ := fromBytesBigEndian T.base.s.data.data if 0 ≥ r ∨ r ≥ secp256k1n then .error <| .InvalidTransaction .InvalidSignature @@ -1150,7 +1181,7 @@ def checkTransactionGetSender (σ : YPState) (chainId H_f : ℕ) (T : Transactio | .ok s => pure <| Fin.ofNat <| fromBytesBigEndian <| ((KEC s).extract 12 32 /- 160 bits = 20 bytes -/ ).data.data - | .error s => .error <| .InvalidTransaction (.SenderRecoverError s) + | .error s => .error <| .SenderRecoverError s | .some sender => pure sender -- dbg_trace s!"Looking for S_T: {S_T} in: σ: {repr σ}" @@ -1321,13 +1352,11 @@ def Υ (debugMode : Bool) (fuel : ℕ) (σ : YPState) (chainId H_f : ℕ) (H : B | .some x => x pure (σ_P, g', A, z) | some t => - match σ₀.find? t with - | .none => dbg_trace "σ₀.find failed; this should probably not be happening; test semantics will be off."; default - | .some v => - let (_, σ_P, g', A, z, _) ← - Θ debugMode fuel createdAccounts σ₀ AStar S_T S_T t v.code g p T.base.value T.base.value T.base.data 0 H true + -- Proposition (71) suggests the recipient can be inexistent + let (_, σ_P, g', A, z, _) ← + Θ debugMode fuel createdAccounts σ₀ AStar S_T S_T t (toExecute σ₀ t) g p T.base.value T.base.value T.base.data 0 H true -- dbg_trace "Θ gave back σ_P: {repr σ_P}" - pure (σ_P, g', A, z) + pure (σ_P, g', A, z) -- The amount to be refunded (82) let gStar := g' + min ((T.base.gasLimit - g') / 5) A.refundBalance -- The pre-final state (83) diff --git a/EvmYul/EllipticCurves.lean b/EvmYul/EllipticCurves.lean index c6a19ef..385f23c 100644 --- a/EvmYul/EllipticCurves.lean +++ b/EvmYul/EllipticCurves.lean @@ -4,6 +4,8 @@ import EvmYul.Wheels import EvmYul.PerformIO import Conform.Wheels +def secp256k1n : ℕ := 115792089237316195423570985008687907852837564279074904382605163141518161494337 + def blobECDSARECOVER (e v r s : String) : String := totallySafePerformIO ∘ IO.Process.run <| pythonCommandOfInput e v r s diff --git a/EvmYul/EllipticCurvesPy/alt_bn128.py b/EvmYul/EllipticCurvesPy/alt_bn128.py new file mode 100644 index 0000000..c97241d --- /dev/null +++ b/EvmYul/EllipticCurvesPy/alt_bn128.py @@ -0,0 +1,195 @@ +""" +The alt_bn128 curve +^^^^^^^^^^^^^^^^^^^ +""" + +import elliptic_curve, finite_field + +ALT_BN128_PRIME = 21888242871839275222246405745257275088696311157297823662689037894645226208583 # noqa: E501 +ALT_BN128_CURVE_ORDER = 21888242871839275222246405745257275088548364400416034343698204186575808495617 # noqa: E501 +ATE_PAIRING_COUNT = 29793968203157093289 +ATE_PAIRING_COUNT_BITS = 63 + + +class BNF(finite_field.PrimeField): + """ + The prime field over which the alt_bn128 curve is defined. + """ + + PRIME = ALT_BN128_PRIME + + +class BNP(elliptic_curve.EllipticCurve): + """ + The alt_bn128 curve. + """ + + FIELD = BNF + A = BNF(0) + B = BNF(3) + + +class BNF2(finite_field.GaloisField): + """ + `BNF` extended with a square root of 1 (`i`). + """ + + PRIME = ALT_BN128_PRIME + MODULUS = (1, 0) + + i: "BNF2" + i_plus_9: "BNF2" + + +BNF2.FROBENIUS_COEFFICIENTS = BNF2.calculate_frobenius_coefficients() +"""autoapi_noindex""" + +BNF2.i = BNF2((0, 1)) +"""autoapi_noindex""" + +BNF2.i_plus_9 = BNF2((9, 1)) +"""autoapi_noindex""" + + +class BNP2(elliptic_curve.EllipticCurve): + """ + A twist of `BNP`. This is actually the same curve as `BNP` under a change + of variable, but that change of variable is only possible over the larger + field `BNP12`. + """ + + FIELD = BNF2 + A = BNF2.zero() + B = BNF2.from_int(3) / (BNF2.i + BNF2.from_int(9)) + + +class BNF12(finite_field.GaloisField): + """ + `BNF2` extended by adding a 6th root of `9 + i` called `w` (omega). + """ + + PRIME = ALT_BN128_PRIME + MODULUS = (82, 0, 0, 0, 0, 0, -18, 0, 0, 0, 0, 0) + + w: "BNF12" + i_plus_9: "BNF12" + + def __mul__(self: "BNF12", right: "BNF12") -> "BNF12": # type: ignore[override] # noqa: E501 + """ + Multiplication special cased for BNF12. + """ + mul = [0] * 23 + + for i in range(12): + for j in range(12): + mul[i + j] += self[i] * right[j] + + for i in range(22, 11, -1): + mul[i - 6] -= mul[i] * (-18) + mul[i - 12] -= mul[i] * 82 + + return BNF12.__new__( + BNF12, + mul[:12], + ) + + +BNF12.FROBENIUS_COEFFICIENTS = BNF12.calculate_frobenius_coefficients() +"""autoapi_noindex""" + +BNF12.w = BNF12((0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0)) +"""autoapi_noindex""" + +BNF12.i_plus_9 = BNF12.w**6 +"""autoapi_noindex""" + + +class BNP12(elliptic_curve.EllipticCurve): + """ + The same curve as `BNP`, but defined over the larger field. This curve has + both subgroups of order `ALT_BN128_CURVE_ORDER` and allows pairings to be + computed. + """ + + FIELD = BNF12 + A = BNF12.zero() + B = BNF12.from_int(3) + + +def bnf2_to_bnf12(x: BNF2) -> BNF12: + """ + Lift a field element in `BNF2` to `BNF12`. + """ + return BNF12.from_int(x[0]) + BNF12.from_int(x[1]) * ( + BNF12.i_plus_9 - BNF12.from_int(9) + ) + + +def bnp_to_bnp12(p: BNP) -> BNP12: + """ + Lift a point from `BNP` to `BNP12`. + """ + return BNP12(BNF12.from_int(int(p.x)), BNF12.from_int(int(p.y))) + + +def twist(p: BNP2) -> BNP12: + """ + Apply to twist to change variables from the curve `BNP2` to `BNP12`. + """ + return BNP12( + bnf2_to_bnf12(p.x) * (BNF12.w**2), + bnf2_to_bnf12(p.y) * (BNF12.w**3), + ) + + +def linefunc(p1: BNP12, p2: BNP12, t: BNP12) -> BNF12: + """ + Evaluate the function defining the line between points `p1` and `p2` at the + point `t`. The mathematical significance of this function is that is has + divisor `(p1) + (p2) + (p1 + p2) - 3(O)`. + + Note: Abstract mathematical presentations of Miller's algorithm often + specify the divisor `(p1) + (p2) - (p1 + p2) - (O)`. This turns out not to + matter. + """ + if p1.x != p2.x: + lam = (p2.y - p1.y) / (p2.x - p1.x) + return lam * (t.x - p1.x) - (t.y - p1.y) + elif p1.y == p2.y: + lam = BNF12.from_int(3) * p1.x**2 / (BNF12.from_int(2) * p1.y) + return lam * (t.x - p1.x) - (t.y - p1.y) + else: + return t.x - p1.x + + +def miller_loop(q: BNP12, p: BNP12) -> BNF12: + """ + The core of the pairing algorithm. + """ + if p == BNP12.point_at_infinity() or q == BNP12.point_at_infinity(): + return BNF12.from_int(1) + r = q + f = BNF12.from_int(1) + for i in range(ATE_PAIRING_COUNT_BITS, -1, -1): + f = f * f * linefunc(r, r, p) + r = r.double() + if (ATE_PAIRING_COUNT - 1) & (2**i): + f = f * linefunc(r, q, p) + r = r + q + assert r == q.mul_by(ATE_PAIRING_COUNT - 1) + + q1 = BNP12(q.x.frobenius(), q.y.frobenius()) + nq2 = BNP12(q1.x.frobenius(), -q1.y.frobenius()) + + f = f * linefunc(r, q1, p) + r = r + q1 + f = f * linefunc(r, nq2, p) + + return f ** ((ALT_BN128_PRIME**12 - 1) // ALT_BN128_CURVE_ORDER) + + +def pairing(q: BNP2, p: BNP) -> BNF12: + """ + Compute the pairing of `q` and `p`. + """ + return miller_loop(twist(q), bnp_to_bnp12(p)) diff --git a/EvmYul/EllipticCurvesPy/blake2.py b/EvmYul/EllipticCurvesPy/blake2.py new file mode 100644 index 0000000..e6a1e3c --- /dev/null +++ b/EvmYul/EllipticCurvesPy/blake2.py @@ -0,0 +1,250 @@ +""" +The Blake2 Implementation +^^^^^^^^^^^^^^^^^^^^^^^^^^ +""" +import struct +from dataclasses import dataclass +from typing import List, Tuple + +from base_types import Uint + + +def spit_le_to_uint(data: bytes, start: int, num_words: int) -> List[Uint]: + """ + Extracts 8 byte words from a given data. + + Parameters + ---------- + data : + The data in bytes from which the words need to be extracted + start : + Position to start the extraction + num_words: + The number of words to be extracted + """ + words = [] + for i in range(num_words): + start_position = start + (i * 8) + words.append( + Uint.from_le_bytes(data[start_position : start_position + 8]) + ) + + return words + + +@dataclass +class Blake2: + """ + Implementation of the BLAKE2 cryptographic hashing algorithm. + + Please refer the following document for details: + https://datatracker.ietf.org/doc/html/rfc7693 + """ + + w: int + mask_bits: int + word_format: str + + R1: int + R2: int + R3: int + R4: int + + @property + def max_word(self) -> int: + """ + Largest value for a given Blake2 flavor. + """ + return 2**self.w + + @property + def w_R1(self) -> int: + """ + (w - R1) value for a given Blake2 flavor. + Used in the function G + """ + return self.w - self.R1 + + @property + def w_R2(self) -> int: + """ + (w - R2) value for a given Blake2 flavor. + Used in the function G + """ + return self.w - self.R2 + + @property + def w_R3(self) -> int: + """ + (w - R3) value for a given Blake2 flavor. + Used in the function G + """ + return self.w - self.R3 + + @property + def w_R4(self) -> int: + """ + (w - R4) value for a given Blake2 flavor. + Used in the function G + """ + return self.w - self.R4 + + sigma: Tuple = ( + (0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15), + (14, 10, 4, 8, 9, 15, 13, 6, 1, 12, 0, 2, 11, 7, 5, 3), + (11, 8, 12, 0, 5, 2, 15, 13, 10, 14, 3, 6, 7, 1, 9, 4), + (7, 9, 3, 1, 13, 12, 11, 14, 2, 6, 5, 10, 4, 0, 15, 8), + (9, 0, 5, 7, 2, 4, 10, 15, 14, 1, 11, 12, 6, 8, 3, 13), + (2, 12, 6, 10, 0, 11, 8, 3, 4, 13, 7, 5, 15, 14, 1, 9), + (12, 5, 1, 15, 14, 13, 4, 10, 0, 7, 6, 3, 9, 2, 8, 11), + (13, 11, 7, 14, 12, 1, 3, 9, 5, 0, 15, 4, 8, 6, 2, 10), + (6, 15, 14, 9, 11, 3, 0, 8, 12, 2, 13, 7, 1, 4, 10, 5), + (10, 2, 8, 4, 7, 6, 1, 5, 15, 11, 9, 14, 3, 12, 13, 0), + ) + + IV: Tuple = ( + 0x6A09E667F3BCC908, + 0xBB67AE8584CAA73B, + 0x3C6EF372FE94F82B, + 0xA54FF53A5F1D36F1, + 0x510E527FADE682D1, + 0x9B05688C2B3E6C1F, + 0x1F83D9ABFB41BD6B, + 0x5BE0CD19137E2179, + ) + + @property + def sigma_len(self) -> int: + """ + Length of the sigma parameter. + """ + return len(self.sigma) + + def get_blake2_parameters(self, data: bytes) -> Tuple: + """ + Extract the parameters required in the Blake2 compression function + from the provided bytes data. + + Parameters + ---------- + data : + The bytes data that has been passed in the message. + """ + rounds = Uint.from_be_bytes(data[:4]) + h = spit_le_to_uint(data, 4, 8) + m = spit_le_to_uint(data, 68, 16) + t_0, t_1 = spit_le_to_uint(data, 196, 2) + f = Uint.from_be_bytes(data[212:]) + + return (rounds, h, m, t_0, t_1, f) + + def G( + self, v: List, a: int, b: int, c: int, d: int, x: int, y: int + ) -> List: + """ + The mixing function used in Blake2 + https://datatracker.ietf.org/doc/html/rfc7693#section-3.1 + + Parameters + ---------- + v : + The working vector to be mixed. + a, b, c, d : + Indexes within v of the words to be mixed. + x, y : + The two input words for the mixing. + """ + v[a] = (v[a] + v[b] + x) % self.max_word + v[d] = ((v[d] ^ v[a]) >> self.R1) ^ ( + (v[d] ^ v[a]) << self.w_R1 + ) % self.max_word + + v[c] = (v[c] + v[d]) % self.max_word + v[b] = ((v[b] ^ v[c]) >> self.R2) ^ ( + (v[b] ^ v[c]) << self.w_R2 + ) % self.max_word + + v[a] = (v[a] + v[b] + y) % self.max_word + v[d] = ((v[d] ^ v[a]) >> self.R3) ^ ( + (v[d] ^ v[a]) << self.w_R3 + ) % self.max_word + + v[c] = (v[c] + v[d]) % self.max_word + v[b] = ((v[b] ^ v[c]) >> self.R4) ^ ( + (v[b] ^ v[c]) << self.w_R4 + ) % self.max_word + + return v + + def compress( + self, + num_rounds: Uint, + h: List[Uint], + m: List[Uint], + t_0: Uint, + t_1: Uint, + f: bool, + ) -> bytes: + """ + 'F Compression' from section 3.2 of RFC 7693: + https://tools.ietf.org/html/rfc7693#section-3.2 + + Parameters + ---------- + num_rounds : + The number of rounds. A 32-bit unsigned big-endian word + h : + The state vector. 8 unsigned 64-bit little-endian words + m : + The message block vector. 16 unsigned 64-bit little-endian words + t_0, t_1 : + Offset counters. 2 unsigned 64-bit little-endian words + f: + The final block indicator flag. An 8-bit word + """ + # Initialize local work vector v[0..15] + v = [0] * 16 + v[0:8] = h # First half from state + v[8:15] = self.IV # Second half from IV + + v[12] = t_0 ^ self.IV[4] # Low word of the offset + v[13] = t_1 ^ self.IV[5] # High word of the offset + + if f: + v[14] = v[14] ^ self.mask_bits # Invert all bits for last block + + # Mixing + for r in range(num_rounds): + # for more than sigma_len rounds, the schedule + # wraps around to the beginning + s = self.sigma[r % self.sigma_len] + + v = self.G(v, 0, 4, 8, 12, m[s[0]], m[s[1]]) + v = self.G(v, 1, 5, 9, 13, m[s[2]], m[s[3]]) + v = self.G(v, 2, 6, 10, 14, m[s[4]], m[s[5]]) + v = self.G(v, 3, 7, 11, 15, m[s[6]], m[s[7]]) + v = self.G(v, 0, 5, 10, 15, m[s[8]], m[s[9]]) + v = self.G(v, 1, 6, 11, 12, m[s[10]], m[s[11]]) + v = self.G(v, 2, 7, 8, 13, m[s[12]], m[s[13]]) + v = self.G(v, 3, 4, 9, 14, m[s[14]], m[s[15]]) + + result_message_words = (h[i] ^ v[i] ^ v[i + 8] for i in range(8)) + return struct.pack("<8%s" % self.word_format, *result_message_words) + + +# Parameters specific to the Blake2b implementation +@dataclass +class Blake2b(Blake2): + """ + The Blake2b flavor (64-bits) of Blake2. + This version is used in the pre-compiled contract. + """ + + w: int = 64 + mask_bits: int = 0xFFFFFFFFFFFFFFFF + word_format: str = "Q" + + R1: int = 32 + R2: int = 24 + R3: int = 16 + R4: int = 63 diff --git a/EvmYul/EllipticCurvesPy/blake2_f.py b/EvmYul/EllipticCurvesPy/blake2_f.py new file mode 100644 index 0000000..632dd9b --- /dev/null +++ b/EvmYul/EllipticCurvesPy/blake2_f.py @@ -0,0 +1,28 @@ +import sys +from base_types import U256, Uint +from alt_bn128 import ( + ALT_BN128_CURVE_ORDER, + ALT_BN128_PRIME, + BNF, + BNF2, + BNF12, + BNP, + BNP2, + pairing, +) +from blake2 import Blake2b + +data = bytes.fromhex(sys.argv[1]) +if len(data) != 213: + print('error', end = '') + sys.exit() + +blake2b = Blake2b() +rounds, h, m, t_0, t_1, f = blake2b.get_blake2_parameters(data) + +if f not in [0, 1]: + print('error', end = '') + sys.exit() + +output = blake2b.compress(rounds, h, m, t_0, t_1, f) +print(bytes.hex(output)) diff --git a/EvmYul/EllipticCurvesPy/bn_add.py b/EvmYul/EllipticCurvesPy/bn_add.py new file mode 100644 index 0000000..27863d6 --- /dev/null +++ b/EvmYul/EllipticCurvesPy/bn_add.py @@ -0,0 +1,37 @@ +import sys +from base_types import U256, Uint +from alt_bn128 import ( + ALT_BN128_CURVE_ORDER, + ALT_BN128_PRIME, + BNF, + BNF2, + BNF12, + BNP, + BNP2, + pairing, +) + +# OPERATION +x0_bytes = bytes.fromhex(sys.argv[1]) +x0_value = U256.from_be_bytes(x0_bytes) +y0_bytes = bytes.fromhex(sys.argv[2]) +y0_value = U256.from_be_bytes(y0_bytes) +x1_bytes = bytes.fromhex(sys.argv[3]) +x1_value = U256.from_be_bytes(x1_bytes) +y1_bytes = bytes.fromhex(sys.argv[4]) +y1_value = U256.from_be_bytes(y1_bytes) + +for i in (x0_value, y0_value, x1_value, y1_value): + if i >= ALT_BN128_PRIME: + raise OutOfGasError + +try: + p0 = BNP(BNF(x0_value), BNF(y0_value)) + p1 = BNP(BNF(x1_value), BNF(y1_value)) +except ValueError: + raise OutOfGasError + +p = p0 + p1 + +output = p.x.to_be_bytes32() + p.y.to_be_bytes32() +print(bytes.hex(output), end = '') \ No newline at end of file diff --git a/EvmYul/EllipticCurvesPy/bn_mul.py b/EvmYul/EllipticCurvesPy/bn_mul.py new file mode 100644 index 0000000..bee0257 --- /dev/null +++ b/EvmYul/EllipticCurvesPy/bn_mul.py @@ -0,0 +1,33 @@ +import sys +from base_types import U256, Uint +from alt_bn128 import ( + ALT_BN128_CURVE_ORDER, + ALT_BN128_PRIME, + BNF, + BNF2, + BNF12, + BNP, + BNP2, + pairing, +) + +# OPERATION +x0_bytes = bytes.fromhex(sys.argv[1]) +x0_value = U256.from_be_bytes(x0_bytes) +y0_bytes = bytes.fromhex(sys.argv[2]) +y0_value = U256.from_be_bytes(y0_bytes) +n = U256.from_be_bytes(bytes.fromhex(sys.argv[2])) + +for i in (x0_value, y0_value): + if i >= ALT_BN128_PRIME: + raise OutOfGasError + +try: + p0 = BNP(BNF(x0_value), BNF(y0_value)) +except ValueError: + raise OutOfGasError + +p = p0.mul_by(n) + +output = p.x.to_be_bytes32() + p.y.to_be_bytes32() +print(bytes.hex(output)) diff --git a/EvmYul/EllipticCurvesPy/elliptic_curve.py b/EvmYul/EllipticCurvesPy/elliptic_curve.py index 2c70020..0d1b95e 100644 --- a/EvmYul/EllipticCurvesPy/elliptic_curve.py +++ b/EvmYul/EllipticCurvesPy/elliptic_curve.py @@ -8,10 +8,14 @@ import coincurve from base_types import U256, Bytes +from finite_field import Field from hash import Hash32 SECP256K1N = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEBAAEDCE6AF48A03BBFD25E8CD0364141 +F = TypeVar("F", bound=Field) +T = TypeVar("T", bound="EllipticCurve") + def secp256k1_recover(r: U256, s: U256, v: U256, msg_hash: Hash32) -> Bytes: """ Recovers the public key from a given signature. @@ -44,3 +48,108 @@ def secp256k1_recover(r: U256, s: U256, v: U256, msg_hash: Hash32) -> Bytes: ) public_key = public_key.format(compressed=False)[1:] return public_key + +class EllipticCurve(Generic[F]): + """ + Superclass for integers modulo a prime. Not intended to be used + directly, but rather to be subclassed. + """ + + __slots__ = ("x", "y") + + FIELD: Type[F] + A: F + B: F + + x: F + y: F + + def __new__(cls: Type[T], x: F, y: F) -> T: + """ + Make new point on the curve. The point is not checked to see if it is + on the curve. + """ + res = object.__new__(cls) + res.x = x + res.y = y + return res + + def __init__(self, x: F, y: F) -> None: + """ + Checks if the point is on the curve. To skip this check call + `__new__()` directly. + """ + if ( + x != self.FIELD.zero() or y != self.FIELD.zero() + ) and y ** 2 - x**3 - self.A * x - self.B != self.FIELD.zero(): + raise ValueError("Point not on curve") + + def __eq__(self, other: object) -> bool: + """ + Test two points for equality. + """ + if not isinstance(other, type(self)): + return False + return self.x == other.x and self.y == other.y + + def __str__(self) -> str: + """ + Stringify a point as its coordinates. + """ + return str((self.x, self.y)) + + @classmethod + def point_at_infinity(cls: Type[T]) -> T: + """ + Return the point at infinity. This is the identity element of the group + operation. + + The point at infinity doesn't actually have coordinates so we use + `(0, 0)` (which isn't on the curve) to represent it. + """ + return cls.__new__(cls, cls.FIELD.zero(), cls.FIELD.zero()) + + def double(self: T) -> T: + """ + Add a point to itself. + """ + x, y, F = self.x, self.y, self.FIELD + if x == 0 and y == 0: + return self + lam = (F.from_int(3) * x**2 + self.A) / (F.from_int(2) * y) + new_x = lam**2 - x - x + new_y = lam * (x - new_x) - y + return self.__new__(type(self), new_x, new_y) + + def __add__(self: T, other: T) -> T: + """ + Add two points together. + """ + ZERO = self.FIELD.zero() + self_x, self_y, other_x, other_y = self.x, self.y, other.x, other.y + if self_x == ZERO and self_y == ZERO: + return other + if other_x == ZERO and other_y == ZERO: + return self + if self_x == other_x: + if self_y == other_y: + return self.double() + else: + return self.point_at_infinity() + lam = (other_y - self_y) / (other_x - self_x) + x = lam**2 - self_x - other_x + y = lam * (self_x - x) - self_y + return self.__new__(type(self), x, y) + + def mul_by(self: T, n: int) -> T: + """ + Multiply `self` by `n` using the double and add algorithm. + """ + res = self.__new__(type(self), self.FIELD.zero(), self.FIELD.zero()) + s = self + while n != 0: + if n % 2 == 1: + res = res + s + s = s + s + n //= 2 + return res diff --git a/EvmYul/EllipticCurvesPy/finite_field.py b/EvmYul/EllipticCurvesPy/finite_field.py new file mode 100644 index 0000000..96fbc6b --- /dev/null +++ b/EvmYul/EllipticCurvesPy/finite_field.py @@ -0,0 +1,404 @@ +""" +Finite Fields +^^^^^^^^^^^^^ +""" + +# flake8: noqa: D102, D105 + +from typing import Iterable, List, Tuple, Type, TypeVar, cast + +from typing_extensions import Protocol + +from base_types import Bytes, Bytes32 + +F = TypeVar("F", bound="Field") + + +class Field(Protocol): + """ + A type protocol for defining fields. + """ + + __slots__ = () + + @classmethod + def zero(cls: Type[F]) -> F: + ... + + @classmethod + def from_int(cls: Type[F], n: int) -> F: + ... + + def __radd__(self: F, left: F) -> F: + ... + + def __add__(self: F, right: F) -> F: + ... + + def __iadd__(self: F, right: F) -> F: + ... + + def __sub__(self: F, right: F) -> F: + ... + + def __rsub__(self: F, left: F) -> F: + ... + + def __mul__(self: F, right: F) -> F: + ... + + def __rmul__(self: F, left: F) -> F: + ... + + def __imul__(self: F, right: F) -> F: + ... + + def __pow__(self: F, exponent: int) -> F: + ... + + def __ipow__(self: F, right: int) -> F: + ... + + def __neg__(self: F) -> F: + ... + + def __truediv__(self: F, right: F) -> F: + ... + + +T = TypeVar("T", bound="PrimeField") + + +class PrimeField(int, Field): + """ + Superclass for integers modulo a prime. Not intended to be used + directly, but rather to be subclassed. + """ + + __slots__ = () + PRIME: int + + @classmethod + def from_be_bytes(cls: Type[T], buffer: "Bytes") -> T: + """ + Converts a sequence of bytes into a element of the field. + Parameters + ---------- + buffer : + Bytes to decode. + Returns + ------- + self : `T` + Unsigned integer decoded from `buffer`. + """ + return cls(int.from_bytes(buffer, "big")) + + @classmethod + def zero(cls: Type[T]) -> T: + return cls.__new__(cls, 0) + + @classmethod + def from_int(cls: Type[T], n: int) -> T: + return cls(n) + + def __new__(cls: Type[T], value: int) -> T: + return int.__new__(cls, value % cls.PRIME) + + def __radd__(self: T, left: T) -> T: # type: ignore[override] + return self.__add__(left) + + def __add__(self: T, right: T) -> T: # type: ignore[override] + if not isinstance(right, int): + return NotImplemented + + return self.__new__(type(self), int.__add__(self, right)) + + def __iadd__(self: T, right: T) -> T: # type: ignore[override] + return self.__add__(right) + + def __sub__(self: T, right: T) -> T: # type: ignore[override] + if not isinstance(right, int): + return NotImplemented + + return self.__new__(type(self), int.__sub__(self, right)) + + def __rsub__(self: T, left: T) -> T: # type: ignore[override] + if not isinstance(left, int): + return NotImplemented + + return self.__new__(type(self), int.__rsub__(self, left)) + + def __mul__(self: T, right: T) -> T: # type: ignore[override] + if not isinstance(right, int): + return NotImplemented + + return self.__new__(type(self), int.__mul__(self, right)) + + def __rmul__(self: T, left: T) -> T: # type: ignore[override] + return self.__mul__(left) + + def __imul__(self: T, right: T) -> T: # type: ignore[override] + return self.__mul__(right) + + __floordiv__ = None # type: ignore + __rfloordiv__ = None # type: ignore + __ifloordiv__ = None + __divmod__ = None # type: ignore + __rdivmod__ = None # type: ignore + + def __pow__(self: T, exponent: int) -> T: # type: ignore[override] + # For reasons that are unclear, self must be cast to int here under + # PyPy. + return self.__new__( + type(self), int.__pow__(int(self), exponent, self.PRIME) + ) + + __rpow__ = None # type: ignore + + def __ipow__(self: T, right: int) -> T: # type: ignore[override] + return self.__pow__(right) + + __and__ = None # type: ignore + __or__ = None # type: ignore + __xor__ = None # type: ignore + __rxor__ = None # type: ignore + __ixor__ = None + __rshift__ = None # type: ignore + __lshift__ = None # type: ignore + __irshift__ = None + __ilshift__ = None + + def __neg__(self: T) -> T: + return self.__new__(type(self), int.__neg__(self)) + + def __truediv__(self: T, right: T) -> T: # type: ignore[override] + return self * right.multiplicative_inverse() + + def multiplicative_inverse(self: T) -> T: + return self ** (-1) + + def to_be_bytes32(self) -> "Bytes32": + """ + Converts this arbitrarily sized unsigned integer into its big endian + representation with exactly 32 bytes. + Returns + ------- + big_endian : `Bytes32` + Big endian (most significant bits first) representation. + """ + return Bytes32(self.to_bytes(32, "big")) + + +U = TypeVar("U", bound="GaloisField") + + +class GaloisField(tuple, Field): + """ + Superclass for defining finite fields. Not intended to be used + directly, but rather to be subclassed. + + Fields are represented as `F_p[x]/(x^n + ...)` where the `MODULUS` is a + tuple of the non-leading coefficients of the defining polynomial. For + example `x^3 + 2x^2 + 3x + 4` is `(2, 3, 4)`. + + In practice the polynomial is likely to be sparse and you should overload + the `__mul__()` function to take advantage of this fact. + """ + + __slots__ = () + + PRIME: int + MODULUS: Tuple[int, ...] + FROBENIUS_COEFFICIENTS: Tuple["GaloisField", ...] + + @classmethod + def zero(cls: Type[U]) -> U: + return cls.__new__(cls, [0] * len(cls.MODULUS)) + + @classmethod + def from_int(cls: Type[U], n: int) -> U: + return cls.__new__(cls, [n] + [0] * (len(cls.MODULUS) - 1)) + + def __new__(cls: Type[U], iterable: Iterable[int]) -> U: + self = tuple.__new__(cls, (x % cls.PRIME for x in iterable)) + assert len(self) == len(cls.MODULUS) + return self + + def __add__(self: U, right: U) -> U: # type: ignore[override] + if not isinstance(right, type(self)): + return NotImplemented + + return self.__new__( + type(self), + ( + x + y + for (x, y) in cast(Iterable[Tuple[int, int]], zip(self, right)) + ), + ) + + def __radd__(self: U, left: U) -> U: + return self.__add__(left) + + def __iadd__(self: U, right: U) -> U: # type: ignore[override] + return self.__add__(right) + + def __sub__(self: U, right: U) -> U: + if not isinstance(right, type(self)): + return NotImplemented + + x: int + y: int + return self.__new__( + type(self), + ( + x - y + for (x, y) in cast(Iterable[Tuple[int, int]], zip(self, right)) + ), + ) + + def __rsub__(self: U, left: U) -> U: + if not isinstance(left, type(self)): + return NotImplemented + + return self.__new__( + type(self), + ( + x - y + for (x, y) in cast(Iterable[Tuple[int, int]], zip(left, self)) + ), + ) + + def __mul__(self: U, right: U) -> U: # type: ignore[override] + modulus = self.MODULUS + degree = len(modulus) + prime = self.PRIME + mul = [0] * (degree * 2) + + for i in range(degree): + for j in range(degree): + mul[i + j] += self[i] * right[j] + + for i in range(degree * 2 - 1, degree - 1, -1): + for j in range(i - degree, i): + mul[j] -= (mul[i] * modulus[degree - (i - j)]) % prime + + return self.__new__( + type(self), + mul[:degree], + ) + + def __rmul__(self: U, left: U) -> U: # type: ignore[override] + return self.__mul__(left) + + def __imul__(self: U, right: U) -> U: # type: ignore[override] + return self.__mul__(right) + + def __truediv__(self: U, right: U) -> U: + return self * right.multiplicative_inverse() + + def __neg__(self: U) -> U: + return self.__new__(type(self), (-a for a in self)) + + def scalar_mul(self: U, x: int) -> U: + """ + Multiply a field element by a integer. This is faster than using + `from_int()` and field multiplication. + """ + return self.__new__(type(self), (x * n for n in self)) + + def deg(self: U) -> int: + """ + This is a support function for `multiplicative_inverse()`. + """ + for i in range(len(self.MODULUS) - 1, -1, -1): + if self[i] != 0: + return i + raise ValueError("deg() does not support zero") + + def multiplicative_inverse(self: U) -> U: + """ + Calculate the multiplicative inverse. Uses the Euclidean algorithm. + """ + x2: List[int] + p = self.PRIME + x1, f1 = list(self.MODULUS), [0] * len(self) + x2, f2, d2 = list(self), [1] + [0] * (len(self) - 1), self.deg() + q_0 = pow(x2[d2], -1, p) + for i in range(d2): + x1[i + len(x1) - d2] = (x1[i + len(x1) - d2] - q_0 * x2[i]) % p + f1[i + len(x1) - d2] = (f1[i + len(x1) - d2] - q_0 * f2[i]) % p + for i in range(len(self.MODULUS) - 1, -1, -1): + if x1[i] != 0: + d1 = i + break + while True: + if d1 == 0: + ans = f1 + q = pow(x1[0], -1, self.PRIME) + for i in range(len(ans)): + ans[i] *= q + break + elif d2 == 0: + ans = f2 + q = pow(x2[0], -1, self.PRIME) + for i in range(len(ans)): + ans *= q + break + if d1 < d2: + q = x2[d2] * pow(x1[d1], -1, self.PRIME) + for i in range(len(self.MODULUS) - (d2 - d1)): + x2[i + (d2 - d1)] = (x2[i + (d2 - d1)] - q * x1[i]) % p + f2[i + (d2 - d1)] = (f2[i + (d2 - d1)] - q * f1[i]) % p + while x2[d2] == 0: + d2 -= 1 + else: + q = x1[d1] * pow(x2[d2], -1, self.PRIME) + for i in range(len(self.MODULUS) - (d1 - d2)): + x1[i + (d1 - d2)] = (x1[i + (d1 - d2)] - q * x2[i]) % p + f1[i + (d1 - d2)] = (f1[i + (d1 - d2)] - q * f2[i]) % p + while x1[d1] == 0: + d1 -= 1 + return self.__new__(type(self), ans) + + def __pow__(self: U, exponent: int) -> U: + degree = len(self.MODULUS) + if exponent < 0: + self = self.multiplicative_inverse() + exponent = -exponent + + res = self.__new__(type(self), [1] + [0] * (degree - 1)) + s = self + while exponent != 0: + if exponent % 2 == 1: + res *= s + s *= s + exponent //= 2 + return res + + def __ipow__(self: U, right: int) -> U: + return self.__pow__(right) + + @classmethod + def calculate_frobenius_coefficients(cls: Type[U]) -> Tuple[U, ...]: + """ + Calculate the coefficients needed by `frobenius()`. + """ + coefficients = [] + for i in range(len(cls.MODULUS)): + x = [0] * len(cls.MODULUS) + x[i] = 1 + coefficients.append(cls.__new__(cls, x) ** cls.PRIME) + return tuple(coefficients) + + def frobenius(self: U) -> U: + """ + Returns `self ** p`. This function is known as the Frobenius + endomorphism and has many special mathematical properties. In + particular it is extremely cheap to compute compared to other + exponentiations. + """ + ans = self.from_int(0) + a: int + for i, a in enumerate(self): + ans += cast(U, self.FROBENIUS_COEFFICIENTS[i]).scalar_mul(a) + return ans diff --git a/EvmYul/EllipticCurvesPy/rip160.py b/EvmYul/EllipticCurvesPy/rip160.py new file mode 100644 index 0000000..b2c644e --- /dev/null +++ b/EvmYul/EllipticCurvesPy/rip160.py @@ -0,0 +1,27 @@ +import sys +import hashlib +from base_types import Bytes + +def left_pad_zero_bytes(value: Bytes, size: int) -> Bytes: + """ + Left pad zeroes to `value` if it's length is less than the given `size`. + + Parameters + ---------- + value : + The byte string that needs to be padded. + size : + The number of bytes that need that need to be padded. + + Returns + ------- + left_padded_value: `ethereum.base_types.Bytes` + left padded byte string of given `size`. + """ + return value.rjust(size, b"\x00") + +data = bytes.fromhex(sys.argv[1]) +hash_bytes = hashlib.new("ripemd160", data).digest() +padded_hash = left_pad_zero_bytes(hash_bytes, 32) +output = padded_hash +print(bytes.hex(output), end = '') diff --git a/EvmYul/EllipticCurvesPy/sha256.py b/EvmYul/EllipticCurvesPy/sha256.py new file mode 100644 index 0000000..ce252f4 --- /dev/null +++ b/EvmYul/EllipticCurvesPy/sha256.py @@ -0,0 +1,6 @@ +import sys +import hashlib + +data = bytes.fromhex(sys.argv[1]) +output = hashlib.sha256(data).digest() +print(bytes.hex(output), end = '') diff --git a/EvmYul/EllipticCurvesPy/snarkv.py b/EvmYul/EllipticCurvesPy/snarkv.py new file mode 100644 index 0000000..5c6a51d --- /dev/null +++ b/EvmYul/EllipticCurvesPy/snarkv.py @@ -0,0 +1,55 @@ +import sys +from base_types import U256, Uint +from alt_bn128 import ( + ALT_BN128_CURVE_ORDER, + ALT_BN128_PRIME, + BNF, + BNF2, + BNF12, + BNP, + BNP2, + pairing, +) + +data = bytes.fromhex(sys.argv[1]) + +# OPERATION +if len(data) % 192 != 0: + print('error', end = '') + sys.exit() +result = BNF12.from_int(1) +for i in range(len(data) // 192): + values = [] + for j in range(6): + value = U256.from_be_bytes( + data[i * 192 + 32 * j : i * 192 + 32 * (j + 1)] + ) + if value >= ALT_BN128_PRIME: + print('error', end = '') + sys.exit() + values.append(int(value)) + + try: + p = BNP(BNF(values[0]), BNF(values[1])) + q = BNP2( + BNF2((values[3], values[2])), BNF2((values[5], values[4])) + ) + except ValueError: + print('error', end = '') + sys.exit() + + if p.mul_by(ALT_BN128_CURVE_ORDER) != BNP.point_at_infinity(): + print('error', end = '') + sys.exit() + if q.mul_by(ALT_BN128_CURVE_ORDER) != BNP2.point_at_infinity(): + print('error', end = '') + sys.exit() + if p != BNP.point_at_infinity() and q != BNP2.point_at_infinity(): + result = result * pairing(q, p) + +if result == BNF12.from_int(1): + output = U256(1).to_be_bytes32() +else: + output = U256(0).to_be_bytes32() + +print(bytes.hex(output)) diff --git a/EvmYul/Maps/AccountMap.lean b/EvmYul/Maps/AccountMap.lean index 3820878..b5fb09d 100644 --- a/EvmYul/Maps/AccountMap.lean +++ b/EvmYul/Maps/AccountMap.lean @@ -32,6 +32,14 @@ section RemoveLater abbrev AccountMap := Batteries.RBMap AccountAddress Account compare +def toExecute (σ : AccountMap) (t : AccountAddress) : ToExecute := + if /- t is a precompiled account -/ 1 ≤ t && t ≤ 9 then + ToExecute.Precompiled t + else Id.run do + -- We use the code directly without an indirection a'la `codeMap[t]`. + let .some tDirect := σ.find? t | ToExecute.Code default + ToExecute.Code tDirect.code + -- instance : LE ((_ : Address) × Account) where -- le lhs rhs := if lhs.1 = rhs.1 then lhs.2 ≤ rhs.2 else lhs.1 ≤ rhs.1 diff --git a/EvmYul/RIP160.lean b/EvmYul/RIP160.lean new file mode 100644 index 0000000..35b1f41 --- /dev/null +++ b/EvmYul/RIP160.lean @@ -0,0 +1,14 @@ +import EvmYul.PerformIO +import EvmYul.Wheels +import Conform.Wheels + +def blobRIP160 (d : String) : String := + totallySafePerformIO ∘ IO.Process.run <| + pythonCommandOfInput d + where pythonCommandOfInput (d : String) : IO.Process.SpawnArgs := { + cmd := "python3", + args := #["EvmYul/EllipticCurvesPy/rip160.py", d] + } + +def RIP160 (d : ByteArray) : Except String ByteArray := + ByteArray.ofBlob <| blobRIP160 (toHex d) diff --git a/EvmYul/SHA256.lean b/EvmYul/SHA256.lean new file mode 100644 index 0000000..dadf200 --- /dev/null +++ b/EvmYul/SHA256.lean @@ -0,0 +1,14 @@ +import EvmYul.PerformIO +import EvmYul.Wheels +import Conform.Wheels + +def blobSHA256 (d : String) : String := + totallySafePerformIO ∘ IO.Process.run <| + pythonCommandOfInput d + where pythonCommandOfInput (d : String) : IO.Process.SpawnArgs := { + cmd := "python3", + args := #["EvmYul/EllipticCurvesPy/sha256.py", d] + } + +def SHA256 (d : ByteArray) : Except String ByteArray := + ByteArray.ofBlob <| blobSHA256 (toHex d) diff --git a/EvmYul/SNARKV.lean b/EvmYul/SNARKV.lean new file mode 100644 index 0000000..9b5ac82 --- /dev/null +++ b/EvmYul/SNARKV.lean @@ -0,0 +1,16 @@ +import EvmYul.Wheels +import EvmYul.PerformIO +import Conform.Wheels + +def blobSNARKV (data : String) : String := + totallySafePerformIO ∘ IO.Process.run <| + pythonCommandOfInput data + where pythonCommandOfInput (data : String) : IO.Process.SpawnArgs := { + cmd := "python3", + args := #["EvmYul/EllipticCurvesPy/snarkv.py", data] + } + +def SNARKV (data : ByteArray) : Except String ByteArray := + match blobSNARKV (toHex data) with + | "error" => .error "SNARKV failed" + | s => ByteArray.ofBlob s diff --git a/EvmYul/State/Account.lean b/EvmYul/State/Account.lean index f4a0391..6c205ea 100644 --- a/EvmYul/State/Account.lean +++ b/EvmYul/State/Account.lean @@ -6,6 +6,13 @@ import EvmYul.Wheels namespace EvmYul +/-- + (142) `π ≡ {1, 2, 3, 4, 5, 6, 7, 8, 9}` +-/ +def π : Batteries.RBSet AccountAddress compare := Batteries.RBSet.ofList ((List.range 10).tail.map Fin.ofNat) compare + +inductive ToExecute := | Code (code : ByteArray) | Precompiled (precompiled : AccountAddress) + /-- The `Account` data. Section 4.1. diff --git a/EvmYul/State/Substate.lean b/EvmYul/State/Substate.lean index 11f287c..2d99768 100644 --- a/EvmYul/State/Substate.lean +++ b/EvmYul/State/Substate.lean @@ -53,11 +53,6 @@ structure Substate := logSeries : Array (AccountAddress × List UInt256 × ByteArray) deriving BEq, Inhabited, Repr -/-- - (142) `π ≡ {1, 2, 3, 4, 5, 6, 7, 8, 9}` --/ -def π : Batteries.RBSet AccountAddress compare := Batteries.RBSet.ofList ((List.range 10).tail.map Fin.ofNat) compare - /-- (63) `A0 ≡ (∅, (), ∅, 0, π, ∅)` -/