From 2a0ee0f89f7eefe51c5f234ccda9dfc50cc33c80 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Tue, 16 Dec 2025 12:28:18 +0200 Subject: [PATCH 1/3] implement p256verify precompile --- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 17 +++++++++++++++-- .../kevm_pyk/kproj/evm-semantics/schedule.md | 8 ++++++-- 2 files changed, 21 insertions(+), 4 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index ba3bd845ba..42349b124b 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1695,7 +1695,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d syntax Bool ::= #isPrecompiledAccount ( Int , Schedule ) [symbol(isPrecompiledAccount), function, total, smtlib(isPrecompiledAccount)] // -------------------------------------------------------------------------------------------------------------------------------------- - rule [isPrecompiledAccount]: #isPrecompiledAccount(ACCTCODE, SCHED) => 0 true + rule [isPrecompiledAccount]: #isPrecompiledAccount(ACCTCODE, SCHED) => 0 BLS12_PAIRING_CHECK rule #precompiled(16) => BLS12_MAP_FP_TO_G1 rule #precompiled(17) => BLS12_MAP_FP2_TO_G2 + rule #precompiled(256) => P256VERIFY syntax Int ::= #precompiledAccountsUB ( Schedule ) [symbol(#precompiledAccountsUB), function, total] @@ -2199,7 +2201,8 @@ Precompiled Contracts syntax Set ::= #precompiledAccountsSet ( Schedule ) [symbol(#precompiledAccountsSet), function, total] syntax Set ::= #precompiledAccountsSetAux ( Int ) [symbol(#precompiledAccountsSetAux), function, total] // ------------------------------------------------------------------------------------------------------------ - rule #precompiledAccountsSet(SCHED) => #precompiledAccountsSetAux(#precompiledAccountsUB(SCHED)) + rule #precompiledAccountsSet(OSAKA) => #precompiledAccountsSetAux(#precompiledAccountsUB(OSAKA)) SetItem(256) + rule #precompiledAccountsSet(SCHED) => #precompiledAccountsSetAux(#precompiledAccountsUB(SCHED)) [owise] rule #precompiledAccountsSetAux(N) => .Set requires N <=Int 0 rule #precompiledAccountsSetAux(N) => SetItem(N) #precompiledAccountsSetAux(N -Int 1) [owise, preserves-definedness] @@ -2682,6 +2685,14 @@ Precompiled Contracts orBool notBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned)) ``` +```k + syntax PrecompiledOp ::= "P256VERIFY" + // ------------------------------------- + rule P256VERIFY => #end EVMC_SUCCESS ... + DATA + _ => P256Verify(DATA) +``` + Ethereum Gas Calculation ======================== @@ -3044,6 +3055,8 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). rule #gasExec(SCHED, BLS12_MAP_FP_TO_G1) => Gbls12mapfptog1 < SCHED > ... rule #gasExec(SCHED, BLS12_MAP_FP2_TO_G2) => Gbls12mapfp2tog2 < SCHED > ... + rule #gasExec(SCHED, P256VERIFY) => Gp256verify < SCHED > ... + syntax InternalOp ::= "#allocateCallGas" // ---------------------------------------- rule GCALL:Gas ~> #allocateCallGas => .K ... diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md index dba74d67fc..6737843c12 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -53,7 +53,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. | "Gaccessliststoragekey" | "Rmaxquotient" | "Ginitcodewordcost" | "maxInitCodeSize" | "Gwarmstoragedirtystore" | "Gpointeval" | "Gmaxblobgas" | "Gminbasefee" | "Gtargetblobgas" | "Gperblob" | "Blobbasefeeupdatefraction" | "Gbls12g1add" | "Gbls12g1mul" | "Gbls12g2add" | "Gbls12g2mul" | "Gbls12mapfptog1" | "Gbls12PairingCheckMul" - | "Gbls12PairingCheckAdd" | "Gauthbase" | "Gbls12mapfp2tog2" | "Gtxdatafloor" + | "Gbls12PairingCheckAdd" | "Gauthbase" | "Gbls12mapfp2tog2" | "Gtxdatafloor" | "Gp256verify" // ------------------------------------------------------------------------------------------------------------------------------------------------------- ``` @@ -149,6 +149,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [Gbls12mapfptog1Default]: Gbls12mapfptog1 < DEFAULT > => 0 rule [Gbls12mapfp2tog2Default]: Gbls12mapfp2tog2 < DEFAULT > => 0 + rule [Gp256verifyDefault]: Gp256verify < DEFAULT > => 0 + rule [GselfdestructnewaccountDefault]: Gselfdestructnewaccount << DEFAULT >> => false rule [GstaticcalldepthDefault]: Gstaticcalldepth << DEFAULT >> => true rule [GemptyisnonexistentDefault]: Gemptyisnonexistent << DEFAULT >> => false @@ -504,7 +506,9 @@ A `ScheduleConst` is a constant determined by the fee schedule. ```k syntax Schedule ::= "OSAKA" [symbol(OSAKA_EVM), smtlib(schedule_OSAKA)] // ----------------------------------------------------------------------- - rule [SCHEDCONSTOsaka]: SCHEDCONST < OSAKA > => SCHEDCONST < PRAGUE > + rule [Gp256verifyOsaka]: Gp256verify < OSAKA > => 3450 + rule [SCHEDCONSTOsaka]: SCHEDCONST < OSAKA > => SCHEDCONST < PRAGUE > + requires notBool ( SCHEDCONST ==K Gp256verify ) rule [GhasclzOsaka]: Ghasclz << OSAKA >> => true rule [SCHEDFLAGOsaka]: SCHEDFLAG << OSAKA >> => SCHEDFLAG << PRAGUE >> From 00272c4cb3ee7aba30b688572b5e17728fc88543 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Wed, 14 Jan 2026 12:58:48 +0200 Subject: [PATCH 2/3] update gas price of the P256VERIFY precompile --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md index 6737843c12..9d210b5d15 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -506,7 +506,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. ```k syntax Schedule ::= "OSAKA" [symbol(OSAKA_EVM), smtlib(schedule_OSAKA)] // ----------------------------------------------------------------------- - rule [Gp256verifyOsaka]: Gp256verify < OSAKA > => 3450 + rule [Gp256verifyOsaka]: Gp256verify < OSAKA > => 6900 rule [SCHEDCONSTOsaka]: SCHEDCONST < OSAKA > => SCHEDCONST < PRAGUE > requires notBool ( SCHEDCONST ==K Gp256verify ) From 80ce04c8896acabbb2cf29f3523b4488fa847f5c Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Mon, 16 Mar 2026 15:05:00 +0200 Subject: [PATCH 3/3] update failing.llvm --- tests/execution-spec-tests/failing.llvm | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/tests/execution-spec-tests/failing.llvm b/tests/execution-spec-tests/failing.llvm index a440b1dc58..f275928f1f 100644 --- a/tests/execution-spec-tests/failing.llvm +++ b/tests/execution-spec-tests/failing.llvm @@ -609,6 +609,7 @@ blockchain_tests/osaka/eip7951_p256verify_precompiles/test_gas.json,* blockchain_tests/osaka/eip7951_p256verify_precompiles/test_invalid.json,* blockchain_tests/osaka/eip7951_p256verify_precompiles/test_modular_comparison.json,* blockchain_tests/osaka/eip7951_p256verify_precompiles/test_precompile_as_tx_entry_point.json,* +blockchain_tests/osaka/eip7951_p256verify_precompiles/test_precompile_before_fork.json,* blockchain_tests/osaka/eip7951_p256verify_precompiles/test_precompile_will_return_success_with_tx_value.json,* blockchain_tests/osaka/eip7951_p256verify_precompiles/test_valid.json,* blockchain_tests/osaka/eip7951_p256verify_precompiles/test_wycheproof_extra.json,* @@ -666,10 +667,6 @@ blockchain_tests/prague/eip7623_increase_calldata_cost/test_transaction_validity blockchain_tests/prague/eip7702_set_code_tx/test_call_to_precompile_in_pointer_context.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_call_to_precompile_in_pointer_context[fork_Osaka-precompile_0x0000000000000000000000000000000000000005-blockchain_test_from_state_test] blockchain_tests/prague/eip7702_set_code_tx/test_call_to_precompile_in_pointer_context.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_call_to_precompile_in_pointer_context[fork_Osaka-precompile_0x0000000000000000000000000000000000000100-blockchain_test_from_state_test] blockchain_tests/prague/eip7702_set_code_tx/test_pointer_to_precompile.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_pointer_to_precompile[fork_Osaka-precompile_0x0000000000000000000000000000000000000100-blockchain_test_from_state_test] -blockchain_tests/prague/eip7702_set_code_tx/test_set_code_to_precompile.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_set_code_to_precompile[fork_Osaka-precompile_0x0000000000000000000000000000000000000100-call_opcode_CALL-evm_code_type_LEGACY-blockchain_test_from_state_test] -blockchain_tests/prague/eip7702_set_code_tx/test_set_code_to_precompile.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_set_code_to_precompile[fork_Osaka-precompile_0x0000000000000000000000000000000000000100-call_opcode_CALLCODE-evm_code_type_LEGACY-blockchain_test_from_state_test] -blockchain_tests/prague/eip7702_set_code_tx/test_set_code_to_precompile.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_set_code_to_precompile[fork_Osaka-precompile_0x0000000000000000000000000000000000000100-call_opcode_DELEGATECALL-evm_code_type_LEGACY-blockchain_test_from_state_test] -blockchain_tests/prague/eip7702_set_code_tx/test_set_code_to_precompile.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_set_code_to_precompile[fork_Osaka-precompile_0x0000000000000000000000000000000000000100-call_opcode_STATICCALL-evm_code_type_LEGACY-blockchain_test_from_state_test] blockchain_tests/shanghai/eip4895_withdrawals/test_withdrawals_root.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawals_root[fork_Cancun-blockchain_test-n_withdrawals_0-valid_False] blockchain_tests/shanghai/eip4895_withdrawals/test_withdrawals_root.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawals_root[fork_Cancun-blockchain_test-n_withdrawals_1-valid_False] blockchain_tests/shanghai/eip4895_withdrawals/test_withdrawals_root.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawals_root[fork_Cancun-blockchain_test-n_withdrawals_16-valid_False] @@ -727,7 +724,6 @@ blockchain_tests/static/state_tests/stReturnDataTest/modexp_modsize0_returndatas blockchain_tests/static/state_tests/stReturnDataTest/modexp_modsize0_returndatasize.json,tests/static/state_tests/stReturnDataTest/modexp_modsize0_returndatasizeFiller.json::modexp_modsize0_returndatasize[fork_Osaka-blockchain_test_from_state_test-d1] blockchain_tests/static/state_tests/stReturnDataTest/modexp_modsize0_returndatasize.json,tests/static/state_tests/stReturnDataTest/modexp_modsize0_returndatasizeFiller.json::modexp_modsize0_returndatasize[fork_Osaka-blockchain_test_from_state_test-d2] blockchain_tests/static/state_tests/stReturnDataTest/modexp_modsize0_returndatasize.json,tests/static/state_tests/stReturnDataTest/modexp_modsize0_returndatasizeFiller.json::modexp_modsize0_returndatasize[fork_Osaka-blockchain_test_from_state_test-d3] -blockchain_tests/static/state_tests/stSpecialTest/failed_tx_xcf416c53_Paris.json,tests/static/state_tests/stSpecialTest/failed_tx_xcf416c53_ParisFiller.json::failed_tx_xcf416c53_Paris[fork_Osaka-blockchain_test_from_state_test-] blockchain_tests/static/state_tests/stStaticCall/static_CallEcrecover0_0input.json,tests/static/state_tests/stStaticCall/static_CallEcrecover0_0inputFiller.json::static_CallEcrecover0_0input[fork_Osaka-blockchain_test_from_state_test-d5] blockchain_tests/static/state_tests/stStaticCall/StaticcallToPrecompileFromCalledContract.json,tests/static/state_tests/stStaticCall/StaticcallToPrecompileFromCalledContractFiller.yml::StaticcallToPrecompileFromCalledContract[fork_Osaka-blockchain_test_from_state_test-] blockchain_tests/static/state_tests/stStaticCall/StaticcallToPrecompileFromContractInitialization.json,tests/static/state_tests/stStaticCall/StaticcallToPrecompileFromContractInitializationFiller.yml::StaticcallToPrecompileFromContractInitialization[fork_Osaka-blockchain_test_from_state_test-]