Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,5 @@ __pycache__/
sha2/
blake2/
keccak256/
out_*
out_*
**/target
33 changes: 22 additions & 11 deletions Conform/Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,27 @@ def nproc : IO Nat := do
return out.stdout.trim.toNat? |>.getD 1

def main (args : List String) : IO UInt32 := do
let NumThreads : ℕ := args.head? <&> String.toNat! |>.getD (←nproc)
let (NumThreads, cliWhitelist) ← do
match args.head? >>= String.toNat? with
| some n => pure (n, (args.drop 1).toArray)
| none => pure (←nproc, args.toArray)

let printResults (result : ℕ × Array String) : IO (Array String) := do
let (success, failure) := result
IO.println s!"Total tests: {success + failure.size}"
IO.println s!"The post was NOT equal to the resulting state: {failure.size}"
IO.println s!"Succeeded: {success}"
IO.println s!"Success rate of: {(success.toFloat / (failure.size + success).toFloat) * 100.0}"
IO.println s!"Failed tests:\n{failure}"
return failure

if !cliWhitelist.isEmpty then
IO.println s!"Running filtered tests: {cliWhitelist}"
let failed ← testFiles (root := "EthereumTests/BlockchainTests/")
(testWhitelist := cliWhitelist)
(phase := 1)
(threads := NumThreads) >>= printResults
return if failed.isEmpty then 0 else 1

let ExpectedToFail : Std.HashSet String := {
"invalid_block_blob_count.json[src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_blob_txs.py::test_invalid_block_blob_count[fork_Cancun-blockchain_test--blobs_per_tx_(7,)]]",
Expand All @@ -107,22 +127,13 @@ def main (args : List String) : IO UInt32 := do
"CALLBlake2f_MaxRounds_d0g0v0_Cancun",
"SuicideIssue_Cancun"]

let printResults (result : ℕ × Array String) : IO (Array String) := do
let (success, failure) := result
IO.println s!"Total tests: {success + failure.size}"
IO.println s!"The post was NOT equal to the resulting state: {failure.size}"
IO.println s!"Succeeded: {success}"
IO.println s!"Success rate of: {(success.toFloat / (failure.size + success).toFloat) * 100.0}"
IO.println s!"Failed tests:\n{failure}"
return failure

IO.println s!"Phase 1/3 - No performance tests."
let failed₁ ← testFiles (root := "EthereumTests/BlockchainTests/")
(directoryBlacklist := #["EthereumTests/BlockchainTests//GeneralStateTests/VMTests/vmPerformance"])
(testBlacklist := DelayFiles)
(phase := 1)
(threads := NumThreads) >>= printResults

IO.println s!"Phase 2/3 - Performance tests only."
let failed₂ ← testFiles (root := "EthereumTests/BlockchainTests/GeneralStateTests/VMTests/vmPerformance/")
(phase := 2)
Expand Down
2 changes: 0 additions & 2 deletions EvmYul.lean
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,9 @@ 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

Expand Down
16 changes: 0 additions & 16 deletions EvmYul/BLAKE2_F.lean

This file was deleted.

9 changes: 1 addition & 8 deletions EvmYul/EVM/PrecompiledContracts.lean
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,9 @@ 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
import EvmYul.PointEval

import EvmYul.FFI.ffi
Expand Down Expand Up @@ -93,12 +91,7 @@ def Ξ_RIP160
if g.toNat < gᵣ then
(false, ∅, ⟨0⟩, A, .empty)
else
let o :=
match RIP160 I.calldata with
| .ok s => s
| .error e =>
dbg_trace s!"Ξ_RIP160 failed: {e}"
.empty
let o := ffi.RIP160 I.calldata
(true, σ, g - .ofNat gᵣ, A, o)

def Ξ_ID
Expand Down
250 changes: 0 additions & 250 deletions EvmYul/EllipticCurvesPy/blake2.py

This file was deleted.

28 changes: 0 additions & 28 deletions EvmYul/EllipticCurvesPy/blake2_f.py

This file was deleted.

Loading