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..9d210b5d15 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 > => 6900 + rule [SCHEDCONSTOsaka]: SCHEDCONST < OSAKA > => SCHEDCONST < PRAGUE > + requires notBool ( SCHEDCONST ==K Gp256verify ) rule [GhasclzOsaka]: Ghasclz << OSAKA >> => true rule [SCHEDFLAGOsaka]: SCHEDFLAG << OSAKA >> => SCHEDFLAG << PRAGUE >> 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-]