From fc091b13f421bd6978fc392589271e5fa47c4505 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Thu, 16 Jul 2026 12:26:12 +0300 Subject: [PATCH 1/2] kproj/{evm,schedule}.md: implement eip-7843 slotnum opcode Add the SLOTNUM opcode (0x4b, EIP-7843): a NullStackOp pushing the block's slot number (already parsed into ) at a fixed Gbase (2) cost, disassembled from byte 75 and gated on the new Ghasslotnum schedule flag (true at AMSTERDAM). Unmask the four for_amsterdam SLOTNUM conformance fixtures; two sub-cases (value/slot_zero, gas_cost/out_of_gas) remain masked pending the separate Amsterdam Csstore cold-no-op repricing (EIP-8037/8038). Co-Authored-By: Claude Opus 4.8 --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 7 +++++-- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md | 9 ++++++--- 2 files changed, 11 insertions(+), 5 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 fe6317d3e4..1f39c2368f 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1269,13 +1269,14 @@ These operators make queries about the current execution state. rule BASEFEE => BFEE ~> #push ... BFEE rule BLOBBASEFEE => Cbasefeeperblob(SCHED, EXCESS_BLOB_GAS) ~> #push ... EXCESS_BLOB_GAS SCHED requires notBool #rangeNegUInt64(EXCESS_BLOB_GAS) - syntax NullStackOp ::= "COINBASE" | "TIMESTAMP" | "NUMBER" | "DIFFICULTY" | "PREVRANDAO" - // ---------------------------------------------------------------------------------------- + syntax NullStackOp ::= "COINBASE" | "TIMESTAMP" | "NUMBER" | "DIFFICULTY" | "PREVRANDAO" | "SLOTNUM" + // --------------------------------------------------------------------------------------------------- rule COINBASE => CB ~> #push ... CB rule TIMESTAMP => TS ~> #push ... TS rule NUMBER => NUMB ~> #push ... NUMB rule DIFFICULTY => DIFF ~> #push ... DIFF rule PREVRANDAO => RDAO ~> #push ... RDAO + rule SLOTNUM => SN ~> #push ... SN syntax NullStackOp ::= "ADDRESS" | "ORIGIN" | "CALLER" | "CALLVALUE" | "CHAINID" | "SELFBALANCE" // ------------------------------------------------------------------------------------------------ @@ -2957,6 +2958,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). rule #gasExec(SCHED, COINBASE) => Gbase < SCHED > ... rule #gasExec(SCHED, TIMESTAMP) => Gbase < SCHED > ... rule #gasExec(SCHED, NUMBER) => Gbase < SCHED > ... + rule #gasExec(SCHED, SLOTNUM) => Gbase < SCHED > ... rule #gasExec(SCHED, DIFFICULTY) => Gbase < SCHED > ... rule #gasExec(SCHED, PREVRANDAO) => Gbase < SCHED > ... rule #gasExec(SCHED, GASLIMIT) => Gbase < SCHED > ... @@ -3251,6 +3253,7 @@ After interpreting the strings representing programs as a `WordStack`, it should rule #dasmOpCode( 72, SCHED ) => BASEFEE requires Ghasbasefee << SCHED >> rule #dasmOpCode( 73, SCHED ) => BLOBHASH requires Ghasblobhash << SCHED >> rule #dasmOpCode( 74, SCHED ) => BLOBBASEFEE requires Ghasblobbasefee << SCHED >> + rule #dasmOpCode( 75, SCHED ) => SLOTNUM requires Ghasslotnum << SCHED >> rule #dasmOpCode( 80, _ ) => POP rule #dasmOpCode( 81, _ ) => MLOAD rule #dasmOpCode( 82, _ ) => MSTORE 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 b5f4f3f157..3c5522ed6e 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -31,8 +31,8 @@ module SCHEDULE | "Ghaswarmcoinbase" | "Ghaswithdrawals" | "Ghastransient" | "Ghasmcopy" | "Ghasbeaconroot" | "Ghaseip6780" | "Ghasblobbasefee" | "Ghasblobhash" | "Ghasbls12msmdiscount" | "Ghashistory" | "Ghasrequests" | "Ghasauthority" - | "Ghasfloorcost" | "Ghasclz" - // ------------------------------------------------------------- + | "Ghasfloorcost" | "Ghasclz" | "Ghasslotnum" + // --------------------------------------------------------------------------------------- ``` ### Schedule Constants @@ -183,6 +183,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [GhasauthorityDefault]: Ghasauthority << DEFAULT >> => false rule [GhasfloorcostDefault]: Ghasfloorcost << DEFAULT >> => false rule [GhasclzDefault]: Ghasclz << DEFAULT >> => false + rule [GhasslotnumDefault]: Ghasslotnum << DEFAULT >> => false ``` ### Frontier Schedule @@ -526,7 +527,9 @@ A `ScheduleConst` is a constant determined by the fee schedule. orBool SCHEDCONST ==K Blobbasefeeupdatefraction ) - rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >> + rule [GhasslotnumAmsterdam]: Ghasslotnum << AMSTERDAM >> => true + rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >> + requires notBool ( SCHEDFLAG ==K Ghasslotnum ) ``` ```k From 1b0eb004de15391878cef9c79214288429043f96 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:12:30 +0300 Subject: [PATCH 2/2] schedule.md: remove spacing --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 3c5522ed6e..f2bff4e3b6 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -527,8 +527,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. orBool SCHEDCONST ==K Blobbasefeeupdatefraction ) - rule [GhasslotnumAmsterdam]: Ghasslotnum << AMSTERDAM >> => true - rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >> + rule [GhasslotnumAmsterdam]: Ghasslotnum << AMSTERDAM >> => true + rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >> requires notBool ( SCHEDFLAG ==K Ghasslotnum ) ```