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 9f53281648..e37b4ff803 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -2045,6 +2045,14 @@ Precompiled Contracts rule #precompiled(8) => ECPAIRING rule #precompiled(9) => BLAKE2F rule #precompiled(10) => KZGPOINTEVAL + rule #precompiled(11) => BLS12_G1ADD + rule #precompiled(12) => BLS12_G1MSM + rule #precompiled(13) => BLS12_G2ADD + rule #precompiled(14) => BLS12_G2MSM + rule #precompiled(15) => BLS12_PAIRING_CHECK + rule #precompiled(16) => BLS12_MAP_FP_TO_G1 + rule #precompiled(17) => BLS12_MAP_FP2_TO_G2 + syntax Int ::= #precompiledAccountsUB ( Schedule ) [symbol(#precompiledAccountsUB), function, total] // ---------------------------------------------------------------------------------------------------- @@ -2062,7 +2070,7 @@ Precompiled Contracts rule #precompiledAccountsUB(MERGE) => #precompiledAccountsUB(LONDON) rule #precompiledAccountsUB(SHANGHAI) => #precompiledAccountsUB(MERGE) rule #precompiledAccountsUB(CANCUN) => 10 - rule #precompiledAccountsUB(PRAGUE) => #precompiledAccountsUB(CANCUN) + rule #precompiledAccountsUB(PRAGUE) => 17 syntax Set ::= #precompiledAccountsSet ( Schedule ) [symbol(#precompiledAccountsSet), function, total] @@ -2229,6 +2237,327 @@ Precompiled Contracts rule #kzg2vh ( C ) => Sha256rawWrapper(C)[0 <- 1] ``` +- `BLS12_G1ADD` performs point addition in G1 (curve over base prime field) +- `BLS12_G1MSM` performs multi-scalar-multiplication (MSM) in G1 (curve over base prime field) +- `BLS12_G2ADD` performs point addition in G2 (curve over quadratic extension of the base prime field) +- `BLS12_G2MSM` to perform multi-scalar-multiplication (MSM) in G2 (curve over quadratic extension of the base prime field) +- `BLS12_PAIRING_CHECK` performs a pairing operations between a set of pairs of (G1, G2) points +- `BLS12_MAP_FP_TO_G1` maps base field element into the G1 point +- `BLS12_MAP_FP2_TO_G2` maps extension field element into the G2 point + +```k + syntax Bytes ::= #bls12point ( G1Point ) [symbol(#bls12point1), function] + // ------------------------------------------------------------------------- + rule #bls12point((X, Y)) => #padToWidth(64, #asByteStack(X)) +Bytes #padToWidth(64, #asByteStack(Y)) + + syntax Bytes ::= #bls12point ( G2Point ) [symbol(#bls12point2), function] + // ------------------------------------------------------------------------- + rule #bls12point((X0 x X1, Y0 x Y1)) + => #padToWidth(64, #asByteStack(X0)) +Bytes #padToWidth(64, #asByteStack(X1)) + +Bytes #padToWidth(64, #asByteStack(Y0)) +Bytes #padToWidth(64, #asByteStack(Y1)) + + syntax Bool ::= isValidBLS12Coordinate ( Int ) [symbol(isValidBLS12Coordinate), function, total] + // ----------------------------------------------------------------------------------------------- + rule isValidBLS12Coordinate(X) => isValidBLS12Fp(X) + + syntax Bool ::= isValidBLS12Fp ( Int ) [symbol(isValidBLS12Fp), function, total] + // ------------------------------------------------------------------------------- + rule isValidBLS12Fp(X) => X >=Int 0 andBool X X >=Int 0 andBool X BLS12_G1ADD => #end EVMC_SUCCESS ... + DATA + + _ => #bls12point(BLS12G1Add + ( ( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned) + ) + , ( Bytes2Int(substrBytes(DATA, 128, 192), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 192, 256), BE, Unsigned) + ) + )) + + requires lengthBytes( DATA ) ==Int 256 + andBool bls12ValidForAdd + ( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 128, 192), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 192, 256), BE, Unsigned) + ) + + rule BLS12_G1ADD => #end EVMC_PRECOMPILE_FAILURE ... + DATA + requires lengthBytes( DATA ) =/=Int 256 + orBool notBool bls12ValidForAdd + ( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 128, 192), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 192, 256), BE, Unsigned) + ) + + syntax Bool ::= bls12ValidForAdd(Int, Int, Int, Int) [function, total] + // ----------------------------------------------------------------------- + rule bls12ValidForAdd(X0, Y0, X1, Y1) + => true + andBool isValidBLS12Coordinate(X0) + andBool isValidBLS12Coordinate(Y0) + andBool isValidBLS12Coordinate(X1) + andBool isValidBLS12Coordinate(Y1) + andBool BLS12G1OnCurve((X0, Y0)) + andBool BLS12G1OnCurve((X1, Y1)) + + syntax PrecompiledOp ::= "BLS12_G1MSM" + // -------------------------------------- + // Note that the implementation of `g1_lincomb_fast` has the following comment: + // + // * @remark While this function is significantly faster than g1_lincomb_naive(), we refrain from + // * using it in security-critical places (like verification) because the blst Pippenger code has not + // * been audited. In those critical places, we prefer using g1_lincomb_naive() which is much simpler. + // + // https://github.com/ethereum/c-kzg-4844/blob/cc33b779cd3a227f51b35ce519a83cf91d81ccea/src/common/lincomb.c#L54-L56 + + rule BLS12_G1MSM => bls12G1Msm(DATA) ... DATA + + rule g1MsmResult(P:G1Point) => #end EVMC_SUCCESS ... _ => #bls12point(P) + + rule g1MsmError => #end EVMC_PRECOMPILE_FAILURE ... + + syntax G1MsmResult ::= "g1MsmError" | g1MsmResult(G1Point) + | bls12G1Msm(Bytes) [symbol(bls12G1Msm), function, total] + | #bls12G1Msm(Bytes, List, List) [function, total] + | #bls12G1MsmCheck(Bytes, List, List, Int, Int, Int) [function, total] + // ------------------------------------------------------------------------------------------- + rule bls12G1Msm(B:Bytes) => g1MsmError requires lengthBytes(B) ==Int 0 + rule bls12G1Msm(B:Bytes) => #bls12G1Msm(B, .List, .List) requires lengthBytes(B) >Int 0 + + rule #bls12G1Msm(B:Bytes, Ps:List, Ss:List) => g1MsmResult(BLS12G1Msm(... scalars: Ss, points: Ps)) + requires lengthBytes(B) ==Int 0 + rule #bls12G1Msm(B:Bytes, _:List, _:List) => g1MsmError + requires 0 #bls12G1MsmCheck + ( substrBytes(B, 160, lengthBytes(B)), Ps, Ss + , Bytes2Int(substrBytes(B, 0, 64), BE, Unsigned) + , Bytes2Int(substrBytes(B, 64, 128), BE, Unsigned) + , Bytes2Int(substrBytes(B, 128, 160), BE, Unsigned) + ) + requires 160 <=Int lengthBytes(B) + + rule #bls12G1MsmCheck(B:Bytes, Ps:List, Ss:List, X:Int, Y:Int, N:Int) + => #bls12G1Msm(B, Ps ListItem( ( X , Y ) ), Ss ListItem( N )) + requires isValidBLS12Coordinate(X) andBool isValidBLS12Coordinate(Y) + andBool isValidBLS12Scalar(N) + andBool BLS12G1InSubgroup((X, Y)) + rule #bls12G1MsmCheck(_, _, _, _, _, _) => g1MsmError [owise] + + syntax PrecompiledOp ::= "BLS12_G2ADD" + // -------------------------------------- + rule BLS12_G2ADD => #end EVMC_SUCCESS ... + DATA + + _ => #bls12point(BLS12G2Add + ( ( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned) + x Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 128, 192), BE, Unsigned) + x Bytes2Int(substrBytes(DATA, 192, 256), BE, Unsigned) + ) + , ( Bytes2Int(substrBytes(DATA, 256, 320), BE, Unsigned) + x Bytes2Int(substrBytes(DATA, 320, 384), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 384, 448), BE, Unsigned) + x Bytes2Int(substrBytes(DATA, 448, 512), BE, Unsigned) + ) + )) + + requires lengthBytes( DATA ) ==Int 512 + andBool bls12ValidForAdd2 + ( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 128, 192), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 192, 256), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 256, 320), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 320, 384), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 384, 448), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 448, 512), BE, Unsigned) + ) + + rule BLS12_G2ADD => #end EVMC_PRECOMPILE_FAILURE ... + DATA + requires lengthBytes( DATA ) =/=Int 512 + orBool notBool bls12ValidForAdd2 + ( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 128, 192), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 192, 256), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 256, 320), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 320, 384), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 384, 448), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 448, 512), BE, Unsigned) + ) + + syntax Bool ::= bls12ValidForAdd2(Int, Int, Int, Int, Int, Int, Int, Int) [function, total] + // -------------------------------------------------------------------------------------------- + rule bls12ValidForAdd2(PX0, PX1, PY0, PY1, QX0, QX1, QY0, QY1) + => true + andBool isValidBLS12Coordinate(PX0) + andBool isValidBLS12Coordinate(PX1) + andBool isValidBLS12Coordinate(PY0) + andBool isValidBLS12Coordinate(PY1) + andBool isValidBLS12Coordinate(QX0) + andBool isValidBLS12Coordinate(QX1) + andBool isValidBLS12Coordinate(QY0) + andBool isValidBLS12Coordinate(QY1) + andBool BLS12G2OnCurve((PX0 x PX1, PY0 x PY1)) + andBool BLS12G2OnCurve((QX0 x QX1, QY0 x QY1)) + + syntax PrecompiledOp ::= "BLS12_G2MSM" + // ------------------------------------- + rule BLS12_G2MSM => bls12G2Msm(DATA) ... DATA + + rule g2MsmResult(P:G2Point) => #end EVMC_SUCCESS ... + _ => #bls12point(P) + + rule g2MsmError => #end EVMC_PRECOMPILE_FAILURE ... + + syntax G2MsmResult ::= "g2MsmError" | g2MsmResult(G2Point) + | bls12G2Msm(Bytes) [symbol(bls12G2Msm), function, total] + | #bls12G2Msm(Bytes, List, List) [function, total] + | #bls12G2MsmCheck(Bytes, List, List, Int, Int, Int, Int, Int) [function, total] + // ----------------------------------------------------------------------------------------------------- + rule bls12G2Msm(B:Bytes) => g2MsmError requires lengthBytes(B) ==Int 0 + rule bls12G2Msm(B:Bytes) => #bls12G2Msm(B, .List, .List) requires lengthBytes(B) >Int 0 + + rule #bls12G2Msm(B:Bytes, Ps:List, Ss:List) => g2MsmResult(BLS12G2Msm(... scalars: Ss, points: Ps)) + requires lengthBytes(B) ==Int 0 + rule #bls12G2Msm(B:Bytes, _:List, _:List) => g2MsmError + requires 0 #bls12G2MsmCheck + ( substrBytes(B, 288, lengthBytes(B)), Ps, Ss + , Bytes2Int(substrBytes(B, 0, 64), BE, Unsigned) + , Bytes2Int(substrBytes(B, 64, 128), BE, Unsigned) + , Bytes2Int(substrBytes(B, 128, 192), BE, Unsigned) + , Bytes2Int(substrBytes(B, 192, 256), BE, Unsigned) + , Bytes2Int(substrBytes(B, 256, 288), BE, Unsigned) + ) + requires 288 <=Int lengthBytes(B) + + rule #bls12G2MsmCheck(B:Bytes, Ps:List, Ss:List, X0:Int, X1:Int, Y0:Int, Y1:Int, N:Int) + => #bls12G2Msm(B, Ps ListItem( ( X0 x X1, Y0 x Y1 ) ), Ss ListItem( N )) + requires isValidBLS12Coordinate(X0) andBool isValidBLS12Coordinate(X1) + andBool isValidBLS12Coordinate(Y0) andBool isValidBLS12Coordinate(Y1) + andBool isValidBLS12Scalar(N) + andBool BLS12G2InSubgroup(( X0 x X1, Y0 x Y1 )) + rule #bls12G2MsmCheck(_, _, _, _, _, _, _, _) => g2MsmError [owise] + + syntax PrecompiledOp ::= "BLS12_PAIRING_CHECK" + // ---------------------------------------------- + rule BLS12_PAIRING_CHECK => bls12PairingCheck(DATA, .List, .List) ... DATA + + rule bls12PairingResult(B:Bool) => #end EVMC_SUCCESS ... + _ => #if B #then Int2Bytes(32, 1, BE:Endianness) #else Int2Bytes(32, 0, BE:Endianness) #fi + + rule bls12PairingError => #end EVMC_PRECOMPILE_FAILURE ... + + syntax Bls12PairingResult ::= "bls12PairingError" | bls12PairingResult(Bool) + | bls12PairingCheck(Bytes, List, List) [symbol(bls12PairingCheck), function, total] + // --------------------------------------------------------------------------------------------------------------- + rule bls12PairingCheck(B:Bytes, L1:List, L2:List) => bls12PairingResult(BLS12PairingCheck(L1, L2)) + requires lengthBytes(B) ==Int 0 + andBool validBls12G1PairingPoints(L1) + andBool validBls12G2PairingPoints(L2) + andBool size(L1) ==Int size(L2) + andBool size(L1) >Int 0 + + rule bls12PairingCheck(B:Bytes, L1:List, L2:List) + => bls12PairingCheck + ( substrBytes(B, 384, lengthBytes(B)) + , L1 ListItem( + ( Bytes2Int(substrBytes(B, 0, 64), BE, Unsigned) + , Bytes2Int(substrBytes(B, 64, 128), BE, Unsigned) + ) + ) + , L2 ListItem( + ( Bytes2Int(substrBytes(B, 128, 192), BE, Unsigned) + x Bytes2Int(substrBytes(B, 192, 256), BE, Unsigned) + , Bytes2Int(substrBytes(B, 256, 320), BE, Unsigned) + x Bytes2Int(substrBytes(B, 320, 384), BE, Unsigned) + ) + ) + ) + requires lengthBytes(B) >=Int 384 + + rule bls12PairingCheck(_:Bytes, _:List, _:List) => bls12PairingError [owise] + + syntax Bool ::= validBls12G1PairingPoints(List) [function, total] + | validBls12G1PairingPoint(G1Point) [function, total] +// -------------------------------------------------------------------- + rule validBls12G1PairingPoints(.List) => true + rule validBls12G1PairingPoints(ListItem(P:G1Point) L:List) => validBls12G1PairingPoints(L) + requires validBls12G1PairingPoint(P) + rule validBls12G1PairingPoints(_) => false [owise] + + rule validBls12G1PairingPoint((X, Y) #as P:G1Point) + => isValidBLS12Coordinate(X) + andBool isValidBLS12Coordinate(Y) + andBool BLS12G1InSubgroup(P) + + syntax Bool ::= validBls12G2PairingPoints(List) [function, total] + | validBls12G2PairingPoint(G2Point) [function, total] +// -------------------------------------------------------------------- + rule validBls12G2PairingPoints(.List) => true + rule validBls12G2PairingPoints(ListItem(P:G2Point) L:List) => validBls12G2PairingPoints(L) + requires validBls12G2PairingPoint(P) + rule validBls12G2PairingPoints(_) => false [owise] + + rule validBls12G2PairingPoint((X0 x X1, Y0 x Y1) #as P:G2Point) + => isValidBLS12Coordinate(X0) + andBool isValidBLS12Coordinate(X1) + andBool isValidBLS12Coordinate(Y0) + andBool isValidBLS12Coordinate(Y1) + andBool BLS12G2InSubgroup(P) + + syntax PrecompiledOp ::= "BLS12_MAP_FP_TO_G1" + // --------------------------------------------- + rule BLS12_MAP_FP_TO_G1 => #end EVMC_SUCCESS ... + DATA + _ => #bls12point(BLS12MapFpToG1(Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned))) + + requires lengthBytes( DATA ) ==Int 64 + andBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned)) + + rule BLS12_MAP_FP_TO_G1 => #end EVMC_PRECOMPILE_FAILURE ... + DATA + requires lengthBytes( DATA ) =/=Int 64 + orBool notBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned)) + + + syntax PrecompiledOp ::= "BLS12_MAP_FP2_TO_G2" + // ---------------------------------------------- + rule BLS12_MAP_FP2_TO_G2 => #end EVMC_SUCCESS ... + DATA + + _ => #bls12point(BLS12MapFp2ToG2 + ( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned) + , Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned) + )) + + requires lengthBytes( DATA ) ==Int 128 + andBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned)) + andBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned)) + + rule BLS12_MAP_FP2_TO_G2 => #end EVMC_PRECOMPILE_FAILURE ... + DATA + requires lengthBytes( DATA ) =/=Int 128 + orBool notBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned)) + orBool notBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned)) +``` Ethereum Gas Calculation ======================== @@ -2582,6 +2911,15 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). rule #gasExec(SCHED, BLAKE2F) => Gfround < SCHED > *Int #asWord(#range(DATA, 0, 4) ) ... DATA rule #gasExec(SCHED, KZGPOINTEVAL) => Gpointeval < SCHED > ... + rule #gasExec(SCHED, BLS12_G1ADD) => Gbls12g1add < SCHED > ... + rule #gasExec(SCHED, BLS12_G1MSM) => #let N = lengthBytes(DATA) /Int 160 #in N *Int Gbls12g1mul < SCHED > *Int Cbls12g1MsmDiscount(SCHED, N) /Int 1000 ... DATA + rule #gasExec(SCHED, BLS12_G2ADD) => Gbls12g2add < SCHED > ... + rule #gasExec(SCHED, BLS12_G2MSM) => #let N = lengthBytes(DATA) /Int 288 #in N *Int Gbls12g2mul < SCHED > *Int Cbls12g2MsmDiscount(SCHED, N) /Int 1000 ... DATA + + rule #gasExec(SCHED, BLS12_PAIRING_CHECK) => #let N = lengthBytes(DATA) /Int 384 #in N *Int Gbls12PairingCheckMul < SCHED > +Int Gbls12PairingCheckAdd < SCHED > ... DATA + rule #gasExec(SCHED, BLS12_MAP_FP_TO_G1) => Gbls12mapfptog1 < SCHED > ... + rule #gasExec(SCHED, BLS12_MAP_FP2_TO_G2) => Gbls12mapfp2tog2 < SCHED > ... + syntax InternalOp ::= "#allocateCallGas" // ---------------------------------------- rule GCALL:Gas ~> #allocateCallGas => .K ... diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md index bd081d6360..c7a0d55c88 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md @@ -270,6 +270,281 @@ module GAS-FEES rule #adjustedExpLength(0) => 0 rule #adjustedExpLength(1) => 0 rule #adjustedExpLength(N) => 1 +Int #adjustedExpLength(N /Int 2) requires N >Int 1 + + syntax Int ::= Cbls12g1MsmDiscount( Schedule , Int ) [symbol(Cbls12g1MsmDiscount), function, total, smtlib(gas_Cbls12g1MsmDiscount)] + | Cbls12g2MsmDiscount( Schedule , Int ) [symbol(Cbls12g2MsmDiscount), function, total, smtlib(gas_Cbls12g2MsmDiscount)] + // ------------------------------------------------------------------------------------------------------------------------------------ + rule [Cbls12g1MsmDiscount.new]: Cbls12g1MsmDiscount(SCHED, N) => #Cbls12g1MsmDiscount( N ) requires Ghasbls12msmdiscount << SCHED >> [concrete] + rule [Cbls12g1MsmDiscount.old]: Cbls12g1MsmDiscount(SCHED, _) => 0 requires notBool Ghasbls12msmdiscount << SCHED >> [concrete] + + rule [Cbls12g2MsmDiscount.new]: Cbls12g2MsmDiscount(SCHED, N) => #Cbls12g2MsmDiscount( N ) requires Ghasbls12msmdiscount << SCHED >> [concrete] + rule [Cbls12g2MsmDiscount.old]: Cbls12g2MsmDiscount(SCHED, _) => 0 requires notBool Ghasbls12msmdiscount << SCHED >> [concrete] + + syntax Int ::= #Cbls12g1MsmDiscount( Int ) [function, total] + // ----------------------------------------------------------- + rule #Cbls12g1MsmDiscount(N) => 1000 requires N 1000 + rule #Cbls12g1MsmDiscount(2) => 949 + rule #Cbls12g1MsmDiscount(3) => 848 + rule #Cbls12g1MsmDiscount(4) => 797 + rule #Cbls12g1MsmDiscount(5) => 764 + rule #Cbls12g1MsmDiscount(6) => 750 + rule #Cbls12g1MsmDiscount(7) => 738 + rule #Cbls12g1MsmDiscount(8) => 728 + rule #Cbls12g1MsmDiscount(9) => 719 + rule #Cbls12g1MsmDiscount(10) => 712 + rule #Cbls12g1MsmDiscount(11) => 705 + rule #Cbls12g1MsmDiscount(12) => 698 + rule #Cbls12g1MsmDiscount(13) => 692 + rule #Cbls12g1MsmDiscount(14) => 687 + rule #Cbls12g1MsmDiscount(15) => 682 + rule #Cbls12g1MsmDiscount(16) => 677 + rule #Cbls12g1MsmDiscount(17) => 673 + rule #Cbls12g1MsmDiscount(18) => 669 + rule #Cbls12g1MsmDiscount(19) => 665 + rule #Cbls12g1MsmDiscount(20) => 661 + rule #Cbls12g1MsmDiscount(21) => 658 + rule #Cbls12g1MsmDiscount(22) => 654 + rule #Cbls12g1MsmDiscount(23) => 651 + rule #Cbls12g1MsmDiscount(24) => 648 + rule #Cbls12g1MsmDiscount(25) => 645 + rule #Cbls12g1MsmDiscount(26) => 642 + rule #Cbls12g1MsmDiscount(27) => 640 + rule #Cbls12g1MsmDiscount(28) => 637 + rule #Cbls12g1MsmDiscount(29) => 635 + rule #Cbls12g1MsmDiscount(30) => 632 + rule #Cbls12g1MsmDiscount(31) => 630 + rule #Cbls12g1MsmDiscount(32) => 627 + rule #Cbls12g1MsmDiscount(33) => 625 + rule #Cbls12g1MsmDiscount(34) => 623 + rule #Cbls12g1MsmDiscount(35) => 621 + rule #Cbls12g1MsmDiscount(36) => 619 + rule #Cbls12g1MsmDiscount(37) => 617 + rule #Cbls12g1MsmDiscount(38) => 615 + rule #Cbls12g1MsmDiscount(39) => 613 + rule #Cbls12g1MsmDiscount(40) => 611 + rule #Cbls12g1MsmDiscount(41) => 609 + rule #Cbls12g1MsmDiscount(42) => 608 + rule #Cbls12g1MsmDiscount(43) => 606 + rule #Cbls12g1MsmDiscount(44) => 604 + rule #Cbls12g1MsmDiscount(45) => 603 + rule #Cbls12g1MsmDiscount(46) => 601 + rule #Cbls12g1MsmDiscount(47) => 599 + rule #Cbls12g1MsmDiscount(48) => 598 + rule #Cbls12g1MsmDiscount(49) => 596 + rule #Cbls12g1MsmDiscount(50) => 595 + rule #Cbls12g1MsmDiscount(51) => 593 + rule #Cbls12g1MsmDiscount(52) => 592 + rule #Cbls12g1MsmDiscount(53) => 591 + rule #Cbls12g1MsmDiscount(54) => 589 + rule #Cbls12g1MsmDiscount(55) => 588 + rule #Cbls12g1MsmDiscount(56) => 586 + rule #Cbls12g1MsmDiscount(57) => 585 + rule #Cbls12g1MsmDiscount(58) => 584 + rule #Cbls12g1MsmDiscount(59) => 582 + rule #Cbls12g1MsmDiscount(60) => 581 + rule #Cbls12g1MsmDiscount(61) => 580 + rule #Cbls12g1MsmDiscount(62) => 579 + rule #Cbls12g1MsmDiscount(63) => 577 + rule #Cbls12g1MsmDiscount(64) => 576 + rule #Cbls12g1MsmDiscount(65) => 575 + rule #Cbls12g1MsmDiscount(66) => 574 + rule #Cbls12g1MsmDiscount(67) => 573 + rule #Cbls12g1MsmDiscount(68) => 572 + rule #Cbls12g1MsmDiscount(69) => 570 + rule #Cbls12g1MsmDiscount(70) => 569 + rule #Cbls12g1MsmDiscount(71) => 568 + rule #Cbls12g1MsmDiscount(72) => 567 + rule #Cbls12g1MsmDiscount(73) => 566 + rule #Cbls12g1MsmDiscount(74) => 565 + rule #Cbls12g1MsmDiscount(75) => 564 + rule #Cbls12g1MsmDiscount(76) => 563 + rule #Cbls12g1MsmDiscount(77) => 562 + rule #Cbls12g1MsmDiscount(78) => 561 + rule #Cbls12g1MsmDiscount(79) => 560 + rule #Cbls12g1MsmDiscount(80) => 559 + rule #Cbls12g1MsmDiscount(81) => 558 + rule #Cbls12g1MsmDiscount(82) => 557 + rule #Cbls12g1MsmDiscount(83) => 556 + rule #Cbls12g1MsmDiscount(84) => 555 + rule #Cbls12g1MsmDiscount(85) => 554 + rule #Cbls12g1MsmDiscount(86) => 553 + rule #Cbls12g1MsmDiscount(87) => 552 + rule #Cbls12g1MsmDiscount(88) => 551 + rule #Cbls12g1MsmDiscount(89) => 550 + rule #Cbls12g1MsmDiscount(90) => 549 + rule #Cbls12g1MsmDiscount(91) => 548 + rule #Cbls12g1MsmDiscount(92) => 547 + rule #Cbls12g1MsmDiscount(93) => 547 + rule #Cbls12g1MsmDiscount(94) => 546 + rule #Cbls12g1MsmDiscount(95) => 545 + rule #Cbls12g1MsmDiscount(96) => 544 + rule #Cbls12g1MsmDiscount(97) => 543 + rule #Cbls12g1MsmDiscount(98) => 542 + rule #Cbls12g1MsmDiscount(99) => 541 + rule #Cbls12g1MsmDiscount(100) => 540 + rule #Cbls12g1MsmDiscount(101) => 540 + rule #Cbls12g1MsmDiscount(102) => 539 + rule #Cbls12g1MsmDiscount(103) => 538 + rule #Cbls12g1MsmDiscount(104) => 537 + rule #Cbls12g1MsmDiscount(105) => 536 + rule #Cbls12g1MsmDiscount(106) => 536 + rule #Cbls12g1MsmDiscount(107) => 535 + rule #Cbls12g1MsmDiscount(108) => 534 + rule #Cbls12g1MsmDiscount(109) => 533 + rule #Cbls12g1MsmDiscount(110) => 532 + rule #Cbls12g1MsmDiscount(111) => 532 + rule #Cbls12g1MsmDiscount(112) => 531 + rule #Cbls12g1MsmDiscount(113) => 530 + rule #Cbls12g1MsmDiscount(114) => 529 + rule #Cbls12g1MsmDiscount(115) => 528 + rule #Cbls12g1MsmDiscount(116) => 528 + rule #Cbls12g1MsmDiscount(117) => 527 + rule #Cbls12g1MsmDiscount(118) => 526 + rule #Cbls12g1MsmDiscount(119) => 525 + rule #Cbls12g1MsmDiscount(120) => 525 + rule #Cbls12g1MsmDiscount(121) => 524 + rule #Cbls12g1MsmDiscount(122) => 523 + rule #Cbls12g1MsmDiscount(123) => 522 + rule #Cbls12g1MsmDiscount(124) => 522 + rule #Cbls12g1MsmDiscount(125) => 521 + rule #Cbls12g1MsmDiscount(126) => 520 + rule #Cbls12g1MsmDiscount(127) => 520 + rule #Cbls12g1MsmDiscount(128) => 519 + rule #Cbls12g1MsmDiscount(N) => 519 requires N >Int 128 + + syntax Int ::= #Cbls12g2MsmDiscount( Int ) [function, total] + // ----------------------------------------------------------- + rule #Cbls12g2MsmDiscount(N) => 1000 requires N 1000 + rule #Cbls12g2MsmDiscount(2) => 1000 + rule #Cbls12g2MsmDiscount(3) => 923 + rule #Cbls12g2MsmDiscount(4) => 884 + rule #Cbls12g2MsmDiscount(5) => 855 + rule #Cbls12g2MsmDiscount(6) => 832 + rule #Cbls12g2MsmDiscount(7) => 812 + rule #Cbls12g2MsmDiscount(8) => 796 + rule #Cbls12g2MsmDiscount(9) => 782 + rule #Cbls12g2MsmDiscount(10) => 770 + rule #Cbls12g2MsmDiscount(11) => 759 + rule #Cbls12g2MsmDiscount(12) => 749 + rule #Cbls12g2MsmDiscount(13) => 740 + rule #Cbls12g2MsmDiscount(14) => 732 + rule #Cbls12g2MsmDiscount(15) => 724 + rule #Cbls12g2MsmDiscount(16) => 717 + rule #Cbls12g2MsmDiscount(17) => 711 + rule #Cbls12g2MsmDiscount(18) => 704 + rule #Cbls12g2MsmDiscount(19) => 699 + rule #Cbls12g2MsmDiscount(20) => 693 + rule #Cbls12g2MsmDiscount(21) => 688 + rule #Cbls12g2MsmDiscount(22) => 683 + rule #Cbls12g2MsmDiscount(23) => 679 + rule #Cbls12g2MsmDiscount(24) => 674 + rule #Cbls12g2MsmDiscount(25) => 670 + rule #Cbls12g2MsmDiscount(26) => 666 + rule #Cbls12g2MsmDiscount(27) => 663 + rule #Cbls12g2MsmDiscount(28) => 659 + rule #Cbls12g2MsmDiscount(29) => 655 + rule #Cbls12g2MsmDiscount(30) => 652 + rule #Cbls12g2MsmDiscount(31) => 649 + rule #Cbls12g2MsmDiscount(32) => 646 + rule #Cbls12g2MsmDiscount(33) => 643 + rule #Cbls12g2MsmDiscount(34) => 640 + rule #Cbls12g2MsmDiscount(35) => 637 + rule #Cbls12g2MsmDiscount(36) => 634 + rule #Cbls12g2MsmDiscount(37) => 632 + rule #Cbls12g2MsmDiscount(38) => 629 + rule #Cbls12g2MsmDiscount(39) => 627 + rule #Cbls12g2MsmDiscount(40) => 624 + rule #Cbls12g2MsmDiscount(41) => 622 + rule #Cbls12g2MsmDiscount(42) => 620 + rule #Cbls12g2MsmDiscount(43) => 618 + rule #Cbls12g2MsmDiscount(44) => 615 + rule #Cbls12g2MsmDiscount(45) => 613 + rule #Cbls12g2MsmDiscount(46) => 611 + rule #Cbls12g2MsmDiscount(47) => 609 + rule #Cbls12g2MsmDiscount(48) => 607 + rule #Cbls12g2MsmDiscount(49) => 606 + rule #Cbls12g2MsmDiscount(50) => 604 + rule #Cbls12g2MsmDiscount(51) => 602 + rule #Cbls12g2MsmDiscount(52) => 600 + rule #Cbls12g2MsmDiscount(53) => 598 + rule #Cbls12g2MsmDiscount(54) => 597 + rule #Cbls12g2MsmDiscount(55) => 595 + rule #Cbls12g2MsmDiscount(56) => 593 + rule #Cbls12g2MsmDiscount(57) => 592 + rule #Cbls12g2MsmDiscount(58) => 590 + rule #Cbls12g2MsmDiscount(59) => 589 + rule #Cbls12g2MsmDiscount(60) => 587 + rule #Cbls12g2MsmDiscount(61) => 586 + rule #Cbls12g2MsmDiscount(62) => 584 + rule #Cbls12g2MsmDiscount(63) => 583 + rule #Cbls12g2MsmDiscount(64) => 582 + rule #Cbls12g2MsmDiscount(65) => 580 + rule #Cbls12g2MsmDiscount(66) => 579 + rule #Cbls12g2MsmDiscount(67) => 578 + rule #Cbls12g2MsmDiscount(68) => 576 + rule #Cbls12g2MsmDiscount(69) => 575 + rule #Cbls12g2MsmDiscount(70) => 574 + rule #Cbls12g2MsmDiscount(71) => 573 + rule #Cbls12g2MsmDiscount(72) => 571 + rule #Cbls12g2MsmDiscount(73) => 570 + rule #Cbls12g2MsmDiscount(74) => 569 + rule #Cbls12g2MsmDiscount(75) => 568 + rule #Cbls12g2MsmDiscount(76) => 567 + rule #Cbls12g2MsmDiscount(77) => 566 + rule #Cbls12g2MsmDiscount(78) => 565 + rule #Cbls12g2MsmDiscount(79) => 563 + rule #Cbls12g2MsmDiscount(80) => 562 + rule #Cbls12g2MsmDiscount(81) => 561 + rule #Cbls12g2MsmDiscount(82) => 560 + rule #Cbls12g2MsmDiscount(83) => 559 + rule #Cbls12g2MsmDiscount(84) => 558 + rule #Cbls12g2MsmDiscount(85) => 557 + rule #Cbls12g2MsmDiscount(86) => 556 + rule #Cbls12g2MsmDiscount(87) => 555 + rule #Cbls12g2MsmDiscount(88) => 554 + rule #Cbls12g2MsmDiscount(89) => 553 + rule #Cbls12g2MsmDiscount(90) => 552 + rule #Cbls12g2MsmDiscount(91) => 552 + rule #Cbls12g2MsmDiscount(92) => 551 + rule #Cbls12g2MsmDiscount(93) => 550 + rule #Cbls12g2MsmDiscount(94) => 549 + rule #Cbls12g2MsmDiscount(95) => 548 + rule #Cbls12g2MsmDiscount(96) => 547 + rule #Cbls12g2MsmDiscount(97) => 546 + rule #Cbls12g2MsmDiscount(98) => 545 + rule #Cbls12g2MsmDiscount(99) => 545 + rule #Cbls12g2MsmDiscount(100) => 544 + rule #Cbls12g2MsmDiscount(101) => 543 + rule #Cbls12g2MsmDiscount(102) => 542 + rule #Cbls12g2MsmDiscount(103) => 541 + rule #Cbls12g2MsmDiscount(104) => 541 + rule #Cbls12g2MsmDiscount(105) => 540 + rule #Cbls12g2MsmDiscount(106) => 539 + rule #Cbls12g2MsmDiscount(107) => 538 + rule #Cbls12g2MsmDiscount(108) => 537 + rule #Cbls12g2MsmDiscount(109) => 537 + rule #Cbls12g2MsmDiscount(110) => 536 + rule #Cbls12g2MsmDiscount(111) => 535 + rule #Cbls12g2MsmDiscount(112) => 535 + rule #Cbls12g2MsmDiscount(113) => 534 + rule #Cbls12g2MsmDiscount(114) => 533 + rule #Cbls12g2MsmDiscount(115) => 532 + rule #Cbls12g2MsmDiscount(116) => 532 + rule #Cbls12g2MsmDiscount(117) => 531 + rule #Cbls12g2MsmDiscount(118) => 530 + rule #Cbls12g2MsmDiscount(119) => 530 + rule #Cbls12g2MsmDiscount(120) => 529 + rule #Cbls12g2MsmDiscount(121) => 528 + rule #Cbls12g2MsmDiscount(122) => 528 + rule #Cbls12g2MsmDiscount(123) => 527 + rule #Cbls12g2MsmDiscount(124) => 526 + rule #Cbls12g2MsmDiscount(125) => 526 + rule #Cbls12g2MsmDiscount(126) => 525 + rule #Cbls12g2MsmDiscount(127) => 524 + rule #Cbls12g2MsmDiscount(128) => 524 + rule #Cbls12g2MsmDiscount(N) => 524 requires N >Int 128 endmodule ``` 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 b0639948d4..dd13372764 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -30,7 +30,7 @@ module SCHEDULE | "Ghasrejectedfirstbyte" | "Ghasprevrandao" | "Ghasmaxinitcodesize" | "Ghaspushzero" | "Ghaswarmcoinbase" | "Ghaswithdrawals" | "Ghastransient" | "Ghasmcopy" | "Ghasbeaconroot" | "Ghaseip6780" | "Ghasblobbasefee" | "Ghasblobhash" - | "Ghasrequests" | "Ghashistory" + | "Ghasbls12msmdiscount" | "Ghashistory" | "Ghasrequests" // ----------------------------------------------------------------- ``` @@ -51,6 +51,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. | "Gecpairconst" | "Gecpaircoeff" | "Gfround" | "Gcoldsload" | "Gcoldaccountaccess" | "Gwarmstorageread" | "Gaccesslistaddress" | "Gaccessliststoragekey" | "Rmaxquotient" | "Ginitcodewordcost" | "maxInitCodeSize" | "Gwarmstoragedirtystore" | "Gpointeval" | "Gmaxblobgas" | "Gminbasefee" | "Gtargetblobgas" | "Gperblob" | "Blobbasefeeupdatefraction" + | "Gbls12g1add" | "Gbls12g1mul" | "Gbls12g2add" | "Gbls12g2mul" | "Gbls12mapfptog1" | "Gbls12PairingCheckMul" + | "Gbls12PairingCheckAdd" | "Gbls12mapfp2tog2" // ------------------------------------------------------------------------------------------------------------------------------------------------------- ``` @@ -135,6 +137,15 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [RmaxquotientDefault]: Rmaxquotient < DEFAULT > => 2 + rule [Gbls12g1addDefault]: Gbls12g1add < DEFAULT > => 0 + rule [Gbls12g1mulDefault]: Gbls12g1mul < DEFAULT > => 0 + rule [Gbls12g2addDefault]: Gbls12g2add < DEFAULT > => 0 + rule [Gbls12g2mulDefault]: Gbls12g2mul < DEFAULT > => 0 + rule [Gbls12PairingCheckMulDefault]: Gbls12PairingCheckMul < DEFAULT > => 0 + rule [Gbls12PairingCheckAddDefault]: Gbls12PairingCheckAdd < DEFAULT > => 0 + rule [Gbls12mapfptog1Default]: Gbls12mapfptog1 < DEFAULT > => 0 + rule [Gbls12mapfp2tog2Default]: Gbls12mapfp2tog2 < DEFAULT > => 0 + rule [GselfdestructnewaccountDefault]: Gselfdestructnewaccount << DEFAULT >> => false rule [GstaticcalldepthDefault]: Gstaticcalldepth << DEFAULT >> => true rule [GemptyisnonexistentDefault]: Gemptyisnonexistent << DEFAULT >> => false @@ -165,6 +176,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [GhasblobhashDefault]: Ghasblobhash << DEFAULT >> => false rule [GhashistoryDefault]: Ghashistory << DEFAULT >> => false rule [GhasrequestsDefault]: Ghasrequests << DEFAULT >> => false + rule [Ghasbls12msmdiscountDefault]: Ghasbls12msmdiscount << DEFAULT >> => false ``` ### Frontier Schedule @@ -443,16 +455,34 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [GmaxblobgasPrague]: Gmaxblobgas < PRAGUE > => 1179648 rule [GtargetblobgasPrague]: Gtargetblobgas < PRAGUE > => 786432 rule [BlobbasefeeupdatefractionPrague]: Blobbasefeeupdatefraction < PRAGUE > => 5007716 + rule [Gbls12g1addPrague]: Gbls12g1add < PRAGUE > => 375 + rule [Gbls12g1mulPrague]: Gbls12g1mul < PRAGUE > => 12000 + rule [Gbls12g2addPrague]: Gbls12g2add < PRAGUE > => 600 + rule [Gbls12g2mulPrague]: Gbls12g2mul < PRAGUE > => 22500 + rule [Gbls12PairingCheckMulPrague]: Gbls12PairingCheckMul < PRAGUE > => 32600 + rule [Gbls12PairingCheckAddPrague]: Gbls12PairingCheckAdd < PRAGUE > => 37700 + rule [Gbls12mapfptog1Prague]: Gbls12mapfptog1 < PRAGUE > => 5500 + rule [Gbls12mapfp2tog2Prague]: Gbls12mapfp2tog2 < PRAGUE > => 23800 rule [SCHEDCONSTPrague]: SCHEDCONST < PRAGUE > => SCHEDCONST < CANCUN > requires notBool ( SCHEDCONST ==K Gmaxblobgas orBool SCHEDCONST ==K Gtargetblobgas - orBool SCHEDCONST ==K Blobbasefeeupdatefraction ) - - rule [GhasrequestsPrague]: Ghasrequests << PRAGUE >> => true - rule [GhashistoryPrague]: Ghashistory << PRAGUE >> => true - rule [SCHEDFLAGPrague]: SCHEDFLAG << PRAGUE >> => SCHEDFLAG << CANCUN >> - requires notBool ( SCHEDFLAG ==K Ghasrequests - orBool SCHEDFLAG ==K Ghashistory ) + orBool SCHEDCONST ==K Blobbasefeeupdatefraction + orBool SCHEDCONST ==K Gbls12g1add + orBool SCHEDCONST ==K Gbls12g1mul + orBool SCHEDCONST ==K Gbls12g2add + orBool SCHEDCONST ==K Gbls12g2mul + orBool SCHEDCONST ==K Gbls12PairingCheckMul + orBool SCHEDCONST ==K Gbls12PairingCheckAdd + orBool SCHEDCONST ==K Gbls12mapfptog1 + orBool SCHEDCONST ==K Gbls12mapfp2tog2 ) + + rule [GhasrequestsPrague]: Ghasrequests << PRAGUE >> => true + rule [GhashistoryPrague]: Ghashistory << PRAGUE >> => true + rule [Ghasbls12msmdiscountPrague]: Ghasbls12msmdiscount << PRAGUE >> => true + rule [SCHEDFLAGPrague]: SCHEDFLAG << PRAGUE >> => SCHEDFLAG << CANCUN >> + requires notBool ( SCHEDFLAG ==K Ghasrequests + orBool SCHEDFLAG ==K Ghashistory + orBool SCHEDFLAG ==K Ghasbls12msmdiscount ) ``` ```k diff --git a/tests/execution-spec-tests/failing.llvm b/tests/execution-spec-tests/failing.llvm index 1ddaffe6bc..dfdcd6d866 100644 --- a/tests/execution-spec-tests/failing.llvm +++ b/tests/execution-spec-tests/failing.llvm @@ -1615,57 +1615,26 @@ blockchain_tests/cancun/eip6780_selfdestruct/dynamic_create2_selfdestruct_collis blockchain_tests/cancun/eip6780_selfdestruct/dynamic_create2_selfdestruct_collision/dynamic_create2_selfdestruct_collision.json,* blockchain_tests/cancun/eip7516_blobgasfee/blobgasfee_opcode/blobbasefee_before_fork.json,* blockchain_tests/cancun/eip7516_blobgasfee/blobgasfee_opcode/blobbasefee_during_fork.json,* -blockchain_tests/frontier/precompiles/precompiles/precompiles.json,tests/frontier/precompiles/test_precompiles.py::test_precompiles[fork_Prague-address_0x10-precompile_exists_True-blockchain_test_from_state_test] -blockchain_tests/frontier/precompiles/precompiles/precompiles.json,tests/frontier/precompiles/test_precompiles.py::test_precompiles[fork_Prague-address_0x11-precompile_exists_True-blockchain_test_from_state_test] -blockchain_tests/frontier/precompiles/precompiles/precompiles.json,tests/frontier/precompiles/test_precompiles.py::test_precompiles[fork_Prague-address_0xb-precompile_exists_True-blockchain_test_from_state_test] -blockchain_tests/frontier/precompiles/precompiles/precompiles.json,tests/frontier/precompiles/test_precompiles.py::test_precompiles[fork_Prague-address_0xc-precompile_exists_True-blockchain_test_from_state_test] -blockchain_tests/frontier/precompiles/precompiles/precompiles.json,tests/frontier/precompiles/test_precompiles.py::test_precompiles[fork_Prague-address_0xd-precompile_exists_True-blockchain_test_from_state_test] -blockchain_tests/frontier/precompiles/precompiles/precompiles.json,tests/frontier/precompiles/test_precompiles.py::test_precompiles[fork_Prague-address_0xe-precompile_exists_True-blockchain_test_from_state_test] -blockchain_tests/frontier/precompiles/precompiles/precompiles.json,tests/frontier/precompiles/test_precompiles.py::test_precompiles[fork_Prague-address_0xf-precompile_exists_True-blockchain_test_from_state_test] -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1add/call_types.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1add/gas.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1add/invalid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1add/valid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1msm/call_types.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1msm/invalid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1msm/valid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1mul/call_types.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1mul/gas.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1mul/invalid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1mul/valid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2add/call_types.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2add/gas.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2add/invalid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2add/valid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2msm/call_types.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2msm/invalid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2msm/valid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2mul/call_types.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2mul/gas.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2mul/invalid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2mul/valid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_map_fp_to_g1/call_types.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_map_fp_to_g1/gas.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_map_fp_to_g1/invalid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_map_fp_to_g1/valid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_map_fp2_to_g2/call_types.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_map_fp2_to_g2/gas.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_map_fp2_to_g2/invalid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_map_fp2_to_g2/valid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_pairing/call_types.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_pairing/invalid.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_pairing/multi_pair_invalid_inf.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_pairing/valid.json,* +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g1add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g1add_large_input-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g1add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g1add_point_not_on_curve-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g1add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g1add_short_input-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g1add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g1add_violate_top_bytes-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g1add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g2add_invalid_field_element-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g1add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--g2_points-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g1add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--invalid_point_a_5-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g1add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g1add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--invalid_point_b_5-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g2add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g2add_invalid_field_element-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g2add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g2add_long_input-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g2add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g2add_point_not_on_curve-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g2add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g2add_short_input-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g2add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g2add_violate_top_bytes-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g2add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--invalid_point_a_5-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2add/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g2add.py::test_invalid[fork_Prague-blockchain_test_from_state_test--invalid_point_b_5-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2msm/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g2msm.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g2_truncated_input-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2mul/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g2mul.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g1_add_input_invalid_length-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2mul/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g2mul.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g2_truncated_input-] +blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_g2mul/invalid.json,tests/prague/eip2537_bls_12_381_precompiles/test_bls12_g2mul.py::test_invalid[fork_Prague-blockchain_test_from_state_test--bls_g2mul_short_input-] blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_precompiles_before_fork/precompile_before_fork.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_variable_length_input_contracts/invalid_gas_g1msm.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_variable_length_input_contracts/invalid_gas_g2msm.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_variable_length_input_contracts/invalid_gas_pairing.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_variable_length_input_contracts/invalid_length_g1msm.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_variable_length_input_contracts/invalid_length_g2msm.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_variable_length_input_contracts/invalid_length_pairing.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_variable_length_input_contracts/valid_gas_g1msm.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_variable_length_input_contracts/valid_gas_g2msm.json,* -blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_variable_length_input_contracts/valid_gas_pairing.json,* blockchain_tests/prague/eip2935_historical_block_hashes_from_state/block_hashes/block_hashes_history_at_transition.json,* blockchain_tests/prague/eip2935_historical_block_hashes_from_state/block_hashes/block_hashes_history.json,* blockchain_tests/prague/eip2935_historical_block_hashes_from_state/contract_deployment/system_contract_deployment.json,* @@ -1941,20 +1910,6 @@ blockchain_tests/shanghai/eip3860_initcode/initcode/create_opcode_initcode.json, blockchain_tests/shanghai/eip3860_initcode/initcode/create_opcode_initcode.json,tests/shanghai/eip3860_initcode/test_initcode.py::TestCreateInitcode::test_create_opcode_initcode[fork_Prague-blockchain_test_from_state_test-create2-max_size_zeros] blockchain_tests/shanghai/eip3860_initcode/with_eof/legacy_create_edge_code_size.json,tests/shanghai/eip3860_initcode/test_with_eof.py::test_legacy_create_edge_code_size[fork_Prague-blockchain_test_from_state_test-max_initcode-opcode_CREATE] blockchain_tests/shanghai/eip3860_initcode/with_eof/legacy_create_edge_code_size.json,tests/shanghai/eip3860_initcode/test_with_eof.py::test_legacy_create_edge_code_size[fork_Prague-blockchain_test_from_state_test-max_initcode-opcode_CREATE2] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x000000000000000000000000000000000000000b-blockchain_test-amount_0] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x000000000000000000000000000000000000000b-blockchain_test-amount_1] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x000000000000000000000000000000000000000c-blockchain_test-amount_0] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x000000000000000000000000000000000000000c-blockchain_test-amount_1] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x000000000000000000000000000000000000000d-blockchain_test-amount_0] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x000000000000000000000000000000000000000d-blockchain_test-amount_1] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x000000000000000000000000000000000000000e-blockchain_test-amount_0] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x000000000000000000000000000000000000000e-blockchain_test-amount_1] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x000000000000000000000000000000000000000f-blockchain_test-amount_0] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x000000000000000000000000000000000000000f-blockchain_test-amount_1] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x0000000000000000000000000000000000000010-blockchain_test-amount_0] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x0000000000000000000000000000000000000010-blockchain_test-amount_1] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x0000000000000000000000000000000000000011-blockchain_test-amount_0] -blockchain_tests/shanghai/eip4895_withdrawals/withdrawals/withdrawing_to_precompiles.json,tests/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Prague-precompile_0x0000000000000000000000000000000000000011-blockchain_test-amount_1] state_tests/berlin/eip2930_access_list/acl/access_list.json,* state_tests/byzantium/eip198_modexp_precompile/modexp/modexp.json,* state_tests/cancun/eip1153_tstore/basic_tload/basic_tload_after_store.json,*