From bdd65b77569569b57a89f453762c1933a91e77ce Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Tue, 14 Jul 2026 13:44:38 +0300 Subject: [PATCH 01/11] kproj/{schedule,driver}.md: eip-8037 state-creation gas cost increase (const part) AMSTERDAM overrides Gsstoreset/Gnewaccount/Gcreate/Gtxcreate/Gcallvalue per the state-creation-cost repricing. Gnewaccount's new value (183600) would otherwise leak into the existing EIP-7702 "new account" refund rule ( += Gnewaccount - Gauthbase), so that rule is now gated by a new Ghasauthbaserefund flag (true through Osaka, false at AMSTERDAM) until Wave 1b's state-gas AUTH_BASE charge replaces it outright. Docs record two scoping findings from implementing this and EIP-7954: Amsterdam's full state-gas reservoir mechanism (which most devnet-7 fixtures exercise via tx gas limits above today's Gmaxtxgaslimit) is not const-only and is re-scoped into its own "Wave 1b" plan item, with the mapping doc gaining a fully-cited mechanics section for it. --- .../kevm_pyk/kproj/evm-semantics/driver.md | 15 ++++++++++++- .../kevm_pyk/kproj/evm-semantics/schedule.md | 22 +++++++++++++++---- 2 files changed, 32 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md index 0e4cb25254..26f8ac358d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -337,7 +337,20 @@ Processing SetCode Transaction Authority Entries ACCTNONCE => ACCTNONCE +Int 1 ... - requires (ACCTCODE ==K .Bytes orBool #isValidDelegation(ACCTCODE)) + requires Ghasauthbaserefund << SCHED >> + andBool (ACCTCODE ==K .Bytes orBool #isValidDelegation(ACCTCODE)) + andBool #asWord(NONCE) ==K ACCTNONCE + + rule #addAuthority(AUTHORITY, _CID, NONCE, ADDR) => .K ... + SCHED + + AUTHORITY + ACCTCODE => #if #asWord(ADDR) ==Int 0 #then .Bytes #else EOA_DELEGATION_MARKER +Bytes ADDR #fi + ACCTNONCE => ACCTNONCE +Int 1 + ... + + requires notBool Ghasauthbaserefund << SCHED >> + andBool (ACCTCODE ==K .Bytes orBool #isValidDelegation(ACCTCODE)) andBool #asWord(NONCE) ==K ACCTNONCE rule #addAuthority(AUTHORITY, _CID, NONCE, ADDR) => .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 b5f4f3f157..bcb2ed6857 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" | "Ghasauthbaserefund" + // --------------------------------------------------------------------------------------- ``` ### Schedule Constants @@ -491,12 +491,14 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [Ghasbls12msmdiscountPrague]: Ghasbls12msmdiscount << PRAGUE >> => true rule [GhasauthorityPrague]: Ghasauthority << PRAGUE >> => true rule [GhasfloorcostPrague]: Ghasfloorcost << PRAGUE >> => true + rule [GhasauthbaserefundPrague]: Ghasauthbaserefund << PRAGUE >> => true rule [SCHEDFLAGPrague]: SCHEDFLAG << PRAGUE >> => SCHEDFLAG << CANCUN >> requires notBool ( SCHEDFLAG ==K Ghasrequests orBool SCHEDFLAG ==K Ghashistory orBool SCHEDFLAG ==K Ghasbls12msmdiscount orBool SCHEDFLAG ==K Ghasauthority - orBool SCHEDFLAG ==K Ghasfloorcost ) + orBool SCHEDFLAG ==K Ghasfloorcost + orBool SCHEDFLAG ==K Ghasauthbaserefund ) ``` ### Osaka Schedule @@ -520,13 +522,25 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [GmaxblobgasAmsterdam]: Gmaxblobgas < AMSTERDAM > => 2752512 rule [GtargetblobgasAmsterdam]: Gtargetblobgas < AMSTERDAM > => 1835008 rule [BlobbasefeeupdatefractionAmsterdam]: Blobbasefeeupdatefraction < AMSTERDAM > => 11684671 + rule [GsstoresetAmsterdam]: Gsstoreset < AMSTERDAM > => 10000 + rule [GnewaccountAmsterdam]: Gnewaccount < AMSTERDAM > => 183600 + rule [GcreateAmsterdam]: Gcreate < AMSTERDAM > => 11000 + rule [GtxcreateAmsterdam]: Gtxcreate < AMSTERDAM > => 23000 + rule [GcallvalueAmsterdam]: Gcallvalue < AMSTERDAM > => 10300 rule [SCHEDCONSTAmsterdam]: SCHEDCONST < AMSTERDAM > => SCHEDCONST < OSAKA > requires notBool ( SCHEDCONST ==K Gmaxblobgas orBool SCHEDCONST ==K Gtargetblobgas orBool SCHEDCONST ==K Blobbasefeeupdatefraction + orBool SCHEDCONST ==K Gsstoreset + orBool SCHEDCONST ==K Gnewaccount + orBool SCHEDCONST ==K Gcreate + orBool SCHEDCONST ==K Gtxcreate + orBool SCHEDCONST ==K Gcallvalue ) - rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >> + rule [GhasauthbaserefundAmsterdam]: Ghasauthbaserefund << AMSTERDAM >> => false + rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >> + requires notBool ( SCHEDFLAG ==K Ghasauthbaserefund ) ``` ```k From df53c0a53d78cb01775328677fe2f99861e12653 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Wed, 15 Jul 2026 10:25:59 +0300 Subject: [PATCH 02/11] kproj/schedule.md: add missing Ghasauthbaserefund << DEFAULT >> rule Ghasauthbaserefund was added without a DEFAULT-schedule case, triggering a non-exhaustive-match warning from kompile on every build. Co-Authored-By: Claude Sonnet 5 --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md | 1 + 1 file changed, 1 insertion(+) 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 bcb2ed6857..0b9b8579a3 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -181,6 +181,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [GhasrequestsDefault]: Ghasrequests << DEFAULT >> => false rule [Ghasbls12msmdiscountDefault]: Ghasbls12msmdiscount << DEFAULT >> => false rule [GhasauthorityDefault]: Ghasauthority << DEFAULT >> => false + rule [GhasauthbaserefundDefault]: Ghasauthbaserefund << DEFAULT >> => false rule [GhasfloorcostDefault]: Ghasfloorcost << DEFAULT >> => false rule [GhasclzDefault]: Ghasclz << DEFAULT >> => false ``` From 4a8e7cb92eb5a49168174b82ed054067d94c22ae Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Wed, 15 Jul 2026 11:50:31 +0300 Subject: [PATCH 03/11] kproj/{evm,gas,driver,schedule,state-utils}.md: implement eip-8037 state gas reservoir mechanism (Wave 1b) Amsterdam splits gas into a regular and a state dimension. A per-tx reservoir (nonzero only when tx.gas exceeds Gmaxtxgaslimit) is drawn down first by state-gas-priced operations -- SSTORE zero-to-nonzero, new-account creation on CALL/CREATE/SELFDESTRUCT, EIP-7702 authority processing, and code-deposit -- spilling into regular gas once exhausted. Two new per-frame cells (, ) carry this through the call stack for free via the existing #pushCallStack/#popCallStack snapshot-restore, avoiding a fuller EELS-style running-total mirror. Two new block-level cells (, ) track the split separately; remains the single source of truth, updated to max(regular, state) at #finalizeTx so the existing header-check rule needs no changes. Tx admission replaces the old flat Gmaxtxgaslimit cap with dual per-block budget checks, one per dimension. Also folds in the adjacent Amsterdam code-deposit repricing (flat Gcodedeposit/byte cost becomes a keccak-per-word regular cost, plus a new per-byte state-gas charge), since CREATE needed touching for the state-gas charge anyway and every CREATE fixture needs both pieces correct together. Verified against the full 5051-fixture Osaka+Prague regression suite (0 failures) and spot-checked against real Amsterdam EIP-8037 conformance fixtures (SSTORE, CREATE, and CALL-family cases). A wider for_amsterdam sweep surfaced 8 remaining edge-case fixtures (extreme-boundary gas accounting on authority overspend, and a system-contract calling-convention issue) documented as follow-up in the plan doc rather than blocking this commit. Co-Authored-By: Claude Sonnet 5 --- .../kevm_pyk/kproj/evm-semantics/driver.md | 39 +++- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 211 +++++++++++++++++- .../src/kevm_pyk/kproj/evm-semantics/gas.md | 32 +++ .../kevm_pyk/kproj/evm-semantics/schedule.md | 24 +- .../kproj/evm-semantics/state-utils.md | 12 + 5 files changed, 300 insertions(+), 18 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md index 26f8ac358d..60257ae34a 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -128,7 +128,9 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a SCHED _ => #effectiveGasPrice(TXID) - _ => GLIMIT -Int G0(SCHED, CODE, true) + _ => GLIMIT -Int G0(SCHED, CODE, true) -Int #txStateGasReservoir(SCHED, GLIMIT) + _ => #txStateGasReservoir(SCHED, GLIMIT) + _ => 0 _ => ACCTFROM _ => -1 ListItem(TXID:Int) ... @@ -167,7 +169,9 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a SCHED _ => #effectiveGasPrice(TXID) - _ => GLIMIT -Int G0(SCHED, DATA, false) + _ => GLIMIT -Int G0(SCHED, DATA, false) -Int #txStateGasReservoir(SCHED, GLIMIT) + _ => #txStateGasReservoir(SCHED, GLIMIT) + _ => 0 _ => ACCTFROM _ => -1 ListItem(TXID:Int) ... @@ -202,8 +206,10 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax EthereumCommand ::= "#finishTx" // -------------------------------------- - rule _:ExceptionalStatusCode #halt ~> #finishTx => #popCallStack ~> #popWorldState ... - rule EVMC_REVERT #halt ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... GAVAIL + rule _:ExceptionalStatusCode #halt ~> #finishTx => #popCallStack ~> #popWorldState ... + rule EVMC_REVERT #halt ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund (GAVAIL +Gas SGS) ... + GAVAIL + SGS rule EVMC_SUCCESS #halt ~> #finishTx => #mkCodeDeposit ACCT ... @@ -216,8 +222,10 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a rule EVMC_SUCCESS - #halt ~> #finishTx => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ... + #halt ~> #finishTx => #popCallStack ~> #dropWorldState ~> #restoreStateGas SGR SGS ~> #refund GAVAIL ... GAVAIL + SGR + SGS ListItem(TXID:Int) ... TXID @@ -301,7 +309,25 @@ Processing SetCode Transaction Authority Entries SetCode ... - GLIMIT => GLIMIT -Int 25000 [owise] + SCHED + GLIMIT => GLIMIT -Int 25000 + requires notBool Ghasstategas << SCHED >> + [owise] + + rule #loadAuthorities (ListItem(ListItem(CID) ListItem(ADDR) ListItem(NONCE) ListItem(YPAR) ListItem(SIGR) ListItem(SIGS)) REST ) + => Gauthbase < SCHED > ~> #chargeStateGasIntoCallGas + ~> #setDelegation (#recoverAuthority(CID, ADDR, NONCE, YPAR, SIGR, SIGS), CID, NONCE, ADDR) + ~> #loadAuthorities (REST) + ... + ListItem(TXID:Int) ... + + TXID + SetCode + ... + + SCHED + requires Ghasstategas << SCHED >> + [owise] syntax InternalOp ::= #setDelegation ( Account , Bytes , Bytes , Bytes ) [symbol(#setDelegation)] // ------------------------------------------------------------------------------------------------- @@ -354,6 +380,7 @@ Processing SetCode Transaction Authority Entries andBool #asWord(NONCE) ==K ACCTNONCE rule #addAuthority(AUTHORITY, _CID, NONCE, ADDR) => .K ... + SCHED ( .Bag => 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..9b5c52bbd8 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -76,6 +76,9 @@ In the comments next to each cell, we've marked which component of the YellowPap false 0 + 0:Gas + 0:Gas + .Account @@ -126,6 +129,8 @@ In the comments next to each cell, we've marked which component of the YellowPap 0 0 + 0:Gas + 0:Gas [ .JSONs ] @@ -642,6 +647,7 @@ After executing a transaction, it's necessary to have the effect of the substate ... requires REFUND =/=Int 0 + andBool notBool Ghasstategas << SCHED >> rule #finalizeTx(false => true, GFLOOR) ... true @@ -673,6 +679,7 @@ After executing a transaction, it's necessary to have the effect of the substate ... requires ORG =/=Int MINER + andBool notBool Ghasstategas << SCHED >> rule #finalizeTx(false => true, GFLOOR) ... true @@ -698,6 +705,73 @@ After executing a transaction, it's necessary to have the effect of the substate TXTYPE ... + requires notBool Ghasstategas << SCHED >> + + rule #finalizeTx(false => true, GFLOOR) ... + true + SCHED + BFEE + ORG + MINER + GAVAIL + RES => 0 + SPL => 0 + UREG => UREG +Gas maxInt((GLIMIT -Int (GAVAIL +Int RES)) -Int #txStateGasUsed(SCHED, GLIMIT, RES, SPL), GFLOOR) + USTATE => USTATE +Gas #txStateGasUsed(SCHED, GLIMIT, RES, SPL) + _ => maxInt(gas2Int(UREG +Gas maxInt((GLIMIT -Int (GAVAIL +Int RES)) -Int #txStateGasUsed(SCHED, GLIMIT, RES, SPL), GFLOOR)), gas2Int(USTATE +Gas #txStateGasUsed(SCHED, GLIMIT, RES, SPL))) + BLOB_GAS_USED => #if TXTYPE ==K Blob #then BLOB_GAS_USED +Int Ctotalblob(SCHED, size(TVH)) #else BLOB_GAS_USED #fi + GPRICE + REFUND => 0 + + ORG + ORGBAL => ORGBAL +Int minInt(gas2Int(G*(GAVAIL +Int RES, GLIMIT, REFUND, SCHED)), GLIMIT -Int GFLOOR) *Int GPRICE + ... + + + MINER + MINBAL => MINBAL +Int maxInt(GLIMIT -Int gas2Int(G*(GAVAIL +Int RES, GLIMIT, REFUND, SCHED)), GFLOOR) *Int (GPRICE -Int BFEE) + ... + + ListItem(MSGID:Int) REST => REST + + MSGID + GLIMIT + TVH + TXTYPE + ... + + requires ORG =/=Int MINER + andBool Ghasstategas << SCHED >> + + rule #finalizeTx(false => true, GFLOOR) ... + true + SCHED + BFEE + ACCT + ACCT + GAVAIL + RES => 0 + SPL => 0 + UREG => UREG +Gas maxInt((GLIMIT -Int (GAVAIL +Int RES)) -Int #txStateGasUsed(SCHED, GLIMIT, RES, SPL), GFLOOR) + USTATE => USTATE +Gas #txStateGasUsed(SCHED, GLIMIT, RES, SPL) + _ => maxInt(gas2Int(UREG +Gas maxInt((GLIMIT -Int (GAVAIL +Int RES)) -Int #txStateGasUsed(SCHED, GLIMIT, RES, SPL), GFLOOR)), gas2Int(USTATE +Gas #txStateGasUsed(SCHED, GLIMIT, RES, SPL))) + BLOB_GAS_USED => #if TXTYPE ==K Blob #then BLOB_GAS_USED +Int Ctotalblob(SCHED, size(TVH)) #else BLOB_GAS_USED #fi + GPRICE + REFUND => 0 + + ACCT + BAL => BAL +Int GLIMIT *Int GPRICE -Int maxInt(GLIMIT -Int gas2Int(G*(GAVAIL +Int RES, GLIMIT, REFUND, SCHED)), GFLOOR) *Int BFEE + ... + + ListItem(MSGID:Int) REST => REST + + MSGID + GLIMIT + TVH + TXTYPE + ... + + requires Ghasstategas << SCHED >> rule #finalizeTx(false => true, _) ... false @@ -882,6 +956,8 @@ Terminates validation successfully when all conditions are met or when blob vali rule #startBlock => #validateBlockBlobs 0 TXS ~> #executeBeaconRoots ~> #executeBlockHashHistory ... _ => 0 _ => 0 + _ => 0 + _ => 0 _ => .List _ => #padToWidth(256, .Bytes) TXS @@ -1530,11 +1606,17 @@ These rules reach into the network state and load/store from account storage: syntax BinStackOp ::= "SSTORE" // ------------------------------ rule [sstore]: - SSTORE INDEX NEW => .K ... + SSTORE INDEX NEW + => SstoreStateCredit(SCHED, NEW, #lookup(STORAGE, INDEX), #lookup(ORIGSTORAGE, INDEX)) ~> #creditStateGas + ~> SstoreStateGas(SCHED, NEW, #lookup(STORAGE, INDEX), #lookup(ORIGSTORAGE, INDEX)) ~> #chargeStateGas + ... + + SCHED ACCT ACCT STORAGE => STORAGE [ INDEX <- NEW ] + ORIGSTORAGE ... [preserves-definedness] @@ -1669,11 +1751,13 @@ The various `CALL*` (and other inter-contract control flow) operations will be d [owise] rule #callWithCode ACCTFROM ACCTTO ACCTCODE BYTES VALUE APPVALUE ARGS STATIC - => #pushCallStack ~> #pushWorldState + => #accountNonexistent(ACCTTO) ~> #chargeNewAccountStateGas(VALUE, CD) + ~> #pushCallStack ~> #pushWorldState ~> #transferFunds ACCTFROM ACCTTO VALUE ~> #mkCall ACCTFROM ACCTTO ACCTCODE BYTES APPVALUE ARGS STATIC ... + CD rule #mkCall ACCTFROM ACCTTO ACCTCODE BYTES APPVALUE ARGS STATIC:Bool => #touchAccounts ACCTFROM ACCTTO ~> #accessAccounts ACCTFROM ACCTTO ~> #loadProgram BYTES ~> #initVM ~> #precompiled?(ACCTCODE, SCHED) ~> #execute @@ -1834,21 +1918,25 @@ System Transaction Configuration EVMC_REVERT #halt ~> #return RETSTART RETWIDTH => #popCallStack ~> #popWorldState - ~> 0 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT + ~> 0 ~> #push ~> #refund (GAVAIL +Gas SGS) ~> #setLocalMem RETSTART RETWIDTH OUT ... OUT GAVAIL + SGS rule [return.success]: EVMC_SUCCESS #halt ~> #return RETSTART RETWIDTH => #popCallStack ~> #dropWorldState + ~> #restoreStateGas SGR SGS ~> 1 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT ... OUT GAVAIL + SGR + SGS syntax InternalOp ::= "#refund" Gas | "#setLocalMem" Int Int Bytes @@ -1856,6 +1944,14 @@ System Transaction Configuration rule [refund]: #refund G:Gas => .K ... GAVAIL => GAVAIL +Gas G true rule [refund.noGas]: #refund _ => .K ... false + syntax InternalOp ::= "#restoreStateGas" Gas Gas + // -------------------------------------------------- + rule #restoreStateGas R S => .K ... + _ => R + _ => S + true + rule #restoreStateGas _ _ => .K ... false + rule #setLocalMem START WIDTH WS => .K ... LM => LM [ START := #range(WS, 0, minInt(WIDTH, lengthBytes(WS))) ] @@ -1938,13 +2034,15 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- | "#checkCreate" Int Int // -------------------------------------------- rule #create ACCTFROM ACCTTO VALUE INITCODE - => #incrementNonce ACCTFROM + => #accountNonexistent(ACCTTO) ~> #chargeCreateNewAccountStateGas(CD) + ~> #incrementNonce ACCTFROM ~> #pushCallStack ~> #pushWorldState ~> #newAccount ACCTTO ~> #transferFunds ACCTFROM ACCTTO VALUE ~> #mkCreate ACCTFROM ACCTTO VALUE INITCODE ... + CD rule #mkCreate ACCTFROM ACCTTO VALUE INITCODE => #touchAccounts ACCTFROM ACCTTO ~> #accessAccounts ACCTFROM ACCTTO ~> #loadProgram INITCODE ~> #initVM ~> #execute @@ -1991,14 +2089,16 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- #halt ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... _ => .Bytes rule EVMC_REVERT - #halt ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... + #halt ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund (GAVAIL +Gas SGS) ~> 0 ~> #push ... GAVAIL + SGS rule EVMC_SUCCESS #halt ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... rule #mkCodeDeposit ACCT - => Gcodedeposit < SCHED > *Int lengthBytes(OUT) ~> #deductGas + => #if Ghasstategas << SCHED >> #then Gsha3word < SCHED > *Int (lengthBytes(OUT) up/Int 32) #else Gcodedeposit < SCHED > *Int lengthBytes(OUT) #fi ~> #deductGas + ~> (lengthBytes(OUT) *Int Gcostperstatebyte < SCHED >) ~> #chargeStateGas ~> #finishCodeDeposit ACCT OUT ... @@ -2013,10 +2113,13 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- rule #finishCodeDeposit ACCT OUT => #popCallStack ~> #dropWorldState + ~> #restoreStateGas SGR SGS ~> #refund GAVAIL ~> ACCT ~> #push ... GAVAIL + SGR + SGS ACCT _ => OUT @@ -2096,7 +2199,7 @@ Self destructing to yourself, unlike a regular transfer, destroys the balance in ```k syntax UnStackOp ::= "SELFDESTRUCT" // ----------------------------------- - rule SELFDESTRUCT ACCTTO => #touchAccounts ACCT ACCTTO ~> #accessAccounts ACCTTO ~> #transferFunds ACCT ACCTTO BALFROM ~> #end EVMC_SUCCESS ... + rule SELFDESTRUCT ACCTTO => #touchAccounts ACCT ACCTTO ~> #accessAccounts ACCTTO ~> #accountNonexistent(ACCTTO) ~> #chargeSelfdestructNewAccountStateGas BALFROM ~> #transferFunds ACCT ACCTTO BALFROM ~> #end EVMC_SUCCESS ... SCHED ACCT SDS => SDS |Set SetItem(ACCT) @@ -2123,7 +2226,7 @@ Self destructing to yourself, unlike a regular transfer, destroys the balance in CA requires ((notBool Ghaseip6780 << SCHED >>) orBool ACCT in CA) - rule SELFDESTRUCT ACCTTO => #touchAccounts ACCT ACCTTO ~> #accessAccounts ACCTTO ~> #transferFunds ACCT ACCTTO BALFROM ~> #end EVMC_SUCCESS ... + rule SELFDESTRUCT ACCTTO => #touchAccounts ACCT ACCTTO ~> #accessAccounts ACCTTO ~> #accountNonexistent(ACCTTO) ~> #chargeSelfdestructNewAccountStateGas BALFROM ~> #transferFunds ACCT ACCTTO BALFROM ~> #end EVMC_SUCCESS ... SCHED ACCT @@ -2724,6 +2827,91 @@ Overall Gas rule G:Gas ~> #deductGas => .K ... GAVAIL:Gas => GAVAIL -Gas G true requires G <=Gas GAVAIL rule _:Gas ~> #deductGas => .K ... false + syntax InternalOp ::= "#chargeStateGas" | "#creditStateGas" + // ------------------------------------------------------------ + rule A:Gas ~> #chargeStateGas => .K ... + true + R => R -Gas A + requires A <=Gas R + + rule A:Gas ~> #chargeStateGas => .K ... + true + R => 0:Gas + S => S +Gas (A -Gas R) + G => G -Gas (A -Gas R) + requires R A:Gas ~> #chargeStateGas => #end EVMC_OUT_OF_GAS ... + true + R + G + requires R _:Gas ~> #chargeStateGas => .K ... false + + rule A:Gas ~> #creditStateGas => .K ... + true + S => S -Gas minGas(A, S) + G => G +Gas minGas(A, S) + R => R +Gas (A -Gas minGas(A, S)) + + rule _:Gas ~> #creditStateGas => .K ... false + + syntax InternalOp ::= "#chargeStateGasIntoCallGas" + // ---------------------------------------------------- + rule A:Gas ~> #chargeStateGasIntoCallGas => .K ... + true + R => R -Gas A + requires A <=Gas R + + rule A:Gas ~> #chargeStateGasIntoCallGas => .K ... + true + R => 0:Gas + S => S +Gas (A -Gas R) + G => G -Gas (A -Gas R) + requires R _:Gas ~> #chargeStateGasIntoCallGas => .K ... false + + syntax InternalOp ::= "#chargeNewAccountStateGas" "(" Int "," Int ")" + // ------------------------------------------------------------- + rule true ~> #chargeNewAccountStateGas(VALUE, -1) + => #if Ghasstategas << SCHED >> andBool VALUE =/=Int 0 #then Gnewaccount < SCHED > #else 0 #fi ~> #chargeStateGasIntoCallGas + ... + + SCHED + rule true ~> #chargeNewAccountStateGas(VALUE, CD) + => #if Ghasstategas << SCHED >> andBool VALUE =/=Int 0 #then Gnewaccount < SCHED > #else 0 #fi ~> #chargeStateGas + ... + + SCHED + requires CD =/=Int -1 + rule false ~> #chargeNewAccountStateGas(_, _) => .K ... + + syntax InternalOp ::= "#chargeSelfdestructNewAccountStateGas" Int + // -------------------------------------------------------------------- + rule true ~> #chargeSelfdestructNewAccountStateGas(BAL) + => #if Ghasstategas << SCHED >> andBool BAL =/=Int 0 #then Gnewaccount < SCHED > #else 0 #fi ~> #chargeStateGas + ... + + SCHED + rule false ~> #chargeSelfdestructNewAccountStateGas(_) => .K ... + + syntax InternalOp ::= "#chargeCreateNewAccountStateGas" Int + // -------------------------------------------------------------- + rule true ~> #chargeCreateNewAccountStateGas(-1) + => #if Ghasstategas << SCHED >> #then Gnewaccount < SCHED > #else 0 #fi ~> #chargeStateGasIntoCallGas + ... + + SCHED + rule true ~> #chargeCreateNewAccountStateGas(CD) + => #if Ghasstategas << SCHED >> #then Gnewaccount < SCHED > #else 0 #fi ~> #chargeStateGas + ... + + SCHED + requires CD =/=Int -1 + rule false ~> #chargeCreateNewAccountStateGas(_) => .K ... + syntax Bool ::= #inStorage ( Map , Account , Int ) [symbol(#inStorage), function, total] | #inStorageAux1 ( KItem , Int ) [symbol(#inStorageAux1), function, total] | #inStorageAux2 ( Set , Int ) [symbol(#inStorageAux2), function, total] @@ -3072,8 +3260,15 @@ There are several helpers for calculating gas (most of them also specified in th rule Ccallgas(SCHED, ISEMPTY:Bool, GCAP, GAVAIL, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION) => Cgascap(SCHED, GCAP, GAVAIL, Cextra(SCHED, ISEMPTY, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION)) +Gas #if VALUE ==Int 0 #then 0 #else Gcallstipend < SCHED > #fi ... + rule Cselfdestruct(SCHED, ISEMPTY:Bool, BAL) + => Gselfdestruct < SCHED > +Int #if ISEMPTY andBool Gselfdestructnewaccount << SCHED >> andBool (BAL =/=Int 0 orBool Gzerovaluenewaccountgas << SCHED >>) #then Gaccountwrite < SCHED > #else 0 #fi + ... + + requires Ghasstategas << SCHED >> + rule Cselfdestruct(SCHED, ISEMPTY:Bool, BAL) => Gselfdestruct < SCHED > +Int Cnew(SCHED, ISEMPTY andBool Gselfdestructnewaccount << SCHED >>, BAL) ... + requires notBool Ghasstategas << SCHED >> syntax BExp ::= Bool syntax KResult ::= Bool 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 caa924c003..41a70644ee 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md @@ -127,6 +127,8 @@ module GAS-FEES | Cexcessblob ( Schedule , Int , Int ) [symbol(Cexcessblob), function, total, smtlib(gas_Cexcessblob) ] | Cdelegationaccess( Schedule, Bool, Bool ) [symbol(Cdelegationaccess), function, total, smtlib(gas_Cdelegationaccess)] | Ctxfloor ( Schedule , Bytes ) [symbol(Ctxfloor), function, total, smtlib(gas_Ctxfloor) ] + | SstoreStateGas ( Schedule , Int , Int , Int ) [symbol(SstoreStateGas), function, total, smtlib(gas_SstoreStateGas) ] + | SstoreStateCredit( Schedule , Int , Int , Int ) [symbol(SstoreStateCredit), function, total, smtlib(gas_SstoreStateCredit)] // --------------------------------------------------------------------------------------------------------------------------------------------------------- rule [Cgascap]: Cgascap(SCHED, GCAP:Int, GAVAIL:Int, GEXTRA) @@ -173,13 +175,26 @@ module GAS-FEES requires notBool Ghasdirtysstore << SCHED >> [concrete] + rule [SstoreStateGas]: + SstoreStateGas(SCHED, NEW, CURR, ORIG) + => #if ORIG ==Int CURR andBool CURR =/=Int NEW andBool ORIG ==Int 0 #then Gstorageset < SCHED > #else 0 #fi + [concrete] + + rule [SstoreStateCredit]: + SstoreStateCredit(SCHED, NEW, CURR, ORIG) + => #if CURR =/=Int NEW andBool ORIG ==Int NEW andBool ORIG ==Int 0 #then Gstorageset < SCHED > #else 0 #fi + [concrete] + rule [Cextra.delegation]: Cextra(SCHED, ISEMPTY, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION) => Cdelegationaccess(SCHED, ISDELEGATION, ISWARMDELEGATION) +Int Caddraccess(SCHED, ISWARM) +Int Cnew(SCHED, ISEMPTY, VALUE) +Int Cxfer(SCHED, VALUE) requires Ghasaccesslist << SCHED >> andBool Ghasauthority << SCHED >> rule [Cextra.new]: Cextra(SCHED, ISEMPTY, VALUE, ISWARM, _ISDELEGATION, _ISWARMDELEGATION) => Caddraccess(SCHED, ISWARM) +Int Cnew(SCHED, ISEMPTY, VALUE) +Int Cxfer(SCHED, VALUE) requires Ghasaccesslist << SCHED >> andBool notBool Ghasauthority << SCHED >> rule [Cextra.old]: Cextra(SCHED, ISEMPTY, VALUE, _ISWARM, _ISDELEGATION, _ISWARMDELEGATION) => Gcall < SCHED > +Int Cnew(SCHED, ISEMPTY, VALUE) +Int Cxfer(SCHED, VALUE) requires notBool Ghasaccesslist << SCHED >> + rule [Cnew.stategas]: Cnew(SCHED, _, _) => 0 requires Ghasstategas << SCHED >> + rule [Cnew]: Cnew(SCHED, ISEMPTY:Bool, VALUE) => #if ISEMPTY andBool (VALUE =/=Int 0 orBool Gzerovaluenewaccountgas << SCHED >>) #then Gnewaccount < SCHED > #else 0 #fi + requires notBool Ghasstategas << SCHED >> rule [Cxfer.none]: Cxfer(_SCHED, 0) => 0 rule [Cxfer.some]: Cxfer( SCHED, N) => Gcallvalue < SCHED > requires N =/=Int 0 @@ -255,6 +270,23 @@ module GAS-FEES rule G0( _, _, I, I, R) => R rule G0(SCHED, WS, I, J, R) => G0(SCHED, WS, I +Int 1, J, R +Int #if WS[I] ==Int 0 #then Gtxdatazero < SCHED > #else Gtxdatanonzero < SCHED > #fi) [owise] + syntax Int ::= #txStateGasReservoir ( Schedule , Int ) [symbol(#txStateGasReservoir), function, total] + // ------------------------------------------------------------------------------------------------------- + rule #txStateGasReservoir(SCHED, GLIMIT) => #if Ghasstategas << SCHED >> #then maxInt(0, GLIMIT -Int Gmaxtxgaslimit < SCHED >) #else 0 #fi + + syntax Int ::= #txStateGasUsed ( Schedule , Int , Int , Int ) [symbol(#txStateGasUsed), function, total] + // SCHED, GLIMIT, RES (final reservoir), SPL (final spilled) + rule #txStateGasUsed(SCHED, GLIMIT, RES, SPL) => maxInt(0, #txStateGasReservoir(SCHED, GLIMIT) -Int RES +Int SPL) + + syntax Bool ::= #isValidTxGasLimit ( Schedule , Int , Int , Int , Int ) [symbol(#isValidTxGasLimit), function, total] + // SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSEDREG, GASUSEDSTATE + rule #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSEDREG, GASUSEDSTATE) + => #if Ghasstategas << SCHED >> + #then minInt(Gmaxtxgaslimit < SCHED >, TX_GAS_LIMIT) <=Int (BLOCK_GAS_LIMIT -Int GASUSEDREG) + andBool TX_GAS_LIMIT <=Int (BLOCK_GAS_LIMIT -Int GASUSEDSTATE) + #else notBool Ghastxgaslimit << SCHED >> orBool TX_GAS_LIMIT <=Int Gmaxtxgaslimit < SCHED > + #fi + syntax Gas ::= "G*" "(" Gas "," Int "," Int "," Schedule ")" [function] // ----------------------------------------------------------------------- rule G*(GAVAIL, GLIMIT, REFUND, SCHED) => GAVAIL +Gas minGas((GLIMIT -Gas GAVAIL) /Gas Rmaxquotient < SCHED >, REFUND) 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 0b9b8579a3..8d6df46f14 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" | "Ghasauthbaserefund" - // --------------------------------------------------------------------------------------- + | "Ghasfloorcost" | "Ghasclz" | "Ghasstategas" | "Ghasauthbaserefund" + // --------------------------------------------------------------------------------------------------------------- ``` ### Schedule Constants @@ -53,7 +53,8 @@ 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" | "Gstorageset" | "Gaccountwrite" + | "Gcostperstatebyte" // ------------------------------------------------------------------------------------------------------------------------------------------------------- ``` @@ -148,6 +149,9 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [Gbls12PairingCheckAddDefault]: Gbls12PairingCheckAdd < DEFAULT > => 0 rule [Gbls12mapfptog1Default]: Gbls12mapfptog1 < DEFAULT > => 0 rule [Gbls12mapfp2tog2Default]: Gbls12mapfp2tog2 < DEFAULT > => 0 + rule [GstoragesetDefault]: Gstorageset < DEFAULT > => 0 + rule [GaccountwriteDefault]: Gaccountwrite < DEFAULT > => 0 + rule [GcostperstatebyteDefault]: Gcostperstatebyte < DEFAULT > => 0 rule [GselfdestructnewaccountDefault]: Gselfdestructnewaccount << DEFAULT >> => false rule [GstaticcalldepthDefault]: Gstaticcalldepth << DEFAULT >> => true @@ -184,6 +188,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [GhasauthbaserefundDefault]: Ghasauthbaserefund << DEFAULT >> => false rule [GhasfloorcostDefault]: Ghasfloorcost << DEFAULT >> => false rule [GhasclzDefault]: Ghasclz << DEFAULT >> => false + rule [GhasstategasDefault]: Ghasstategas << DEFAULT >> => false ``` ### Frontier Schedule @@ -528,6 +533,10 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [GcreateAmsterdam]: Gcreate < AMSTERDAM > => 11000 rule [GtxcreateAmsterdam]: Gtxcreate < AMSTERDAM > => 23000 rule [GcallvalueAmsterdam]: Gcallvalue < AMSTERDAM > => 10300 + rule [GstoragesetAmsterdam]: Gstorageset < AMSTERDAM > => 97920 + rule [GaccountwriteAmsterdam]: Gaccountwrite < AMSTERDAM > => 8000 + rule [GcostperstatebyteAmsterdam]: Gcostperstatebyte < AMSTERDAM > => 1530 + rule [GauthbaseAmsterdam]: Gauthbase < AMSTERDAM > => 35190 rule [SCHEDCONSTAmsterdam]: SCHEDCONST < AMSTERDAM > => SCHEDCONST < OSAKA > requires notBool ( SCHEDCONST ==K Gmaxblobgas orBool SCHEDCONST ==K Gtargetblobgas @@ -537,11 +546,18 @@ A `ScheduleConst` is a constant determined by the fee schedule. orBool SCHEDCONST ==K Gcreate orBool SCHEDCONST ==K Gtxcreate orBool SCHEDCONST ==K Gcallvalue + orBool SCHEDCONST ==K Gstorageset + orBool SCHEDCONST ==K Gaccountwrite + orBool SCHEDCONST ==K Gcostperstatebyte + orBool SCHEDCONST ==K Gauthbase ) rule [GhasauthbaserefundAmsterdam]: Ghasauthbaserefund << AMSTERDAM >> => false + rule [GhasstategasAmsterdam]: Ghasstategas << AMSTERDAM >> => true rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >> - requires notBool ( SCHEDFLAG ==K Ghasauthbaserefund ) + requires notBool ( SCHEDFLAG ==K Ghasauthbaserefund + orBool SCHEDFLAG ==K Ghasstategas + ) ``` ```k diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md index f2d8fb5ca1..3e769989b0 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md @@ -600,6 +600,8 @@ The `"rlp"` key loads the block information. SCHED BASE_FEE BLOCK_GAS_LIMIT + GASUSEDREG + GASUSEDSTATE ACCTFROM BAL @@ -626,6 +628,7 @@ The `"rlp"` key loads the block information. andBool TX_MAX_PRIORITY_FEE <=Int TX_MAX_FEE andBool BAL >=Int TX_GAS_LIMIT *Int TX_MAX_FEE +Int VALUE andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT + andBool #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSEDREG, GASUSEDSTATE) andBool size(TX_AUTH_LIST) >Int 0 andBool #checkAuthorityList(TX_AUTH_LIST) rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]] @@ -633,6 +636,8 @@ The `"rlp"` key loads the block information. BASE_FEE EXCESS_BLOB_GAS BLOCK_GAS_LIMIT + GASUSEDREG + GASUSEDSTATE ACCTFROM BAL @@ -662,12 +667,15 @@ The `"rlp"` key loads the block information. andBool TX_MAX_BLOB_FEE >=Int Cbasefeeperblob(SCHED, EXCESS_BLOB_GAS) andBool BAL >=Int TX_GAS_LIMIT *Int TX_MAX_FEE +Int (Ctotalblob(SCHED, size(TVH)) *Int TX_MAX_BLOB_FEE) +Int VALUE andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT + andBool #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSEDREG, GASUSEDSTATE) andBool Ctotalblob(SCHED, size(TVH)) <=Int Gmaxblobgas < SCHED> rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]] SCHED BASE_FEE BLOCK_GAS_LIMIT + GASUSEDREG + GASUSEDSTATE ACCTFROM BAL @@ -691,11 +699,14 @@ The `"rlp"` key loads the block information. andBool TX_MAX_PRIORITY_FEE <=Int TX_MAX_FEE andBool BAL >=Int TX_GAS_LIMIT *Int TX_MAX_FEE +Int VALUE andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT + andBool #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSEDREG, GASUSEDSTATE) rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]] SCHED BASE_FEE BLOCK_GAS_LIMIT + GASUSEDREG + GASUSEDSTATE ACCTFROM BAL @@ -718,6 +729,7 @@ The `"rlp"` key loads the block information. andBool BASE_FEE <=Int TX_GAS_PRICE andBool BAL >=Int TX_GAS_LIMIT *Int TX_GAS_PRICE +Int VALUE andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT + andBool #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSEDREG, GASUSEDSTATE) rule #isValidTransaction (_, _) => false [owise] ``` From b338726b3904b9ae4c1bb2f0a4ec5520f5e240f5 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Thu, 16 Jul 2026 13:57:10 +0300 Subject: [PATCH 04/11] kproj/{evm,gas}.md: restructure amsterdam sstore regular gas (eip-8037/8038) The EIP-8037 work (commit 3ff7af55a) added the SSTORE state-gas half (STORAGE_SET -> reservoir) but left the regular half in its Prague shape, which charges the storage-access surcharge (Gcoldsload) AND a separate Gsload operation cost. Amsterdam charges the access as cold XOR warm (Gcoldsload=3000 if cold, else Gwarmstorageread=100, mutually exclusive) plus STORAGE_WRITE (Gsstoreset=10000) only on the first real change, with a simplified refund (a restore always refunds STORAGE_WRITE). Net effect of the old shape: a cold no-op/dirty SSTORE was over-charged by 100 and a warm first-change was under-charged by 100; both were masked wherever the state-gas dimension dominated gasUsed=max(regular,state). Restructure Csstore/Rsstore and the SSTORE #gasAccess surcharge with Amsterdam-gated (Ghasstategas) variants matching the EELS reference; the state-gas halves (SstoreStateGas/SstoreStateCredit) were already correct. Unmask the two SLOTNUM sub-cases (value/slot_zero, gas_cost/out_of_gas) that this fixes. Verified: osaka/prague sweep unchanged (5 fail / 5122 pass); Amsterdam SSTORE suites show the identical 9 pre-existing failures before and after (no regression). Co-Authored-By: Claude Opus 4.8 --- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 2 +- .../src/kevm_pyk/kproj/evm-semantics/gas.md | 18 ++++++++++++++++-- 2 files changed, 17 insertions(+), 3 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 9b5c52bbd8..0cf580eb17 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -3016,7 +3016,7 @@ Access List Gas rule #gasAccess(SCHED, BALANCE ACCT) => Caddraccess(SCHED, ACCT in ACCTS) ... ACCTS rule #gasAccess(SCHED, SELFDESTRUCT ACCT) => #if ACCT in ACCTS #then 0 #else Gcoldaccountaccess < SCHED > #fi ... ACCTS rule #gasAccess(_ , SLOAD INDEX ) => #accessStorage ACCT INDEX ~> 0 ... ACCT - rule #gasAccess(SCHED, SSTORE INDEX _) => #accessStorage ACCT INDEX ~> #if #inStorage(TS, ACCT, INDEX) #then 0 #else Gcoldsload < SCHED > #fi ... ACCT TS + rule #gasAccess(SCHED, SSTORE INDEX _) => #accessStorage ACCT INDEX ~> #if #inStorage(TS, ACCT, INDEX) #then #if Ghasstategas << SCHED >> #then Gwarmstorageread < SCHED > #else 0 #fi #else Gcoldsload < SCHED > #fi ... ACCT TS rule #gasAccess(_ , _ ) => 0 ... [owise] ``` 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 41a70644ee..97a563da35 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md @@ -138,10 +138,16 @@ module GAS-FEES rule Cgascap(_, GCAP, _, _) => 0 requires GCAP #if ORIG ==Int CURR andBool CURR =/=Int NEW #then Gsstoreset < SCHED > #else 0 #fi + requires Ghasstategas << SCHED >> + [concrete] + rule [Csstore.new]: Csstore(SCHED, NEW, CURR, ORIG) => #if CURR ==Int NEW orBool ORIG =/=Int CURR #then Gsload < SCHED > #else #if ORIG ==Int 0 #then Gsstoreset < SCHED > #else Gsstorereset < SCHED > #fi #fi - requires Ghasdirtysstore << SCHED >> + requires Ghasdirtysstore << SCHED >> andBool notBool Ghasstategas << SCHED >> [concrete] rule [Csstore.old]: @@ -150,6 +156,14 @@ module GAS-FEES requires notBool Ghasdirtysstore << SCHED >> [concrete] + rule [Rsstore.amsterdam]: + Rsstore(SCHED, NEW, CURR, ORIG) + => #if CURR =/=Int NEW andBool ORIG =/=Int 0 andBool CURR =/=Int 0 andBool NEW ==Int 0 #then Rsstoreclear < SCHED > #else 0 #fi + +Int #if CURR =/=Int NEW andBool ORIG =/=Int 0 andBool CURR ==Int 0 #then 0 -Int Rsstoreclear < SCHED > #else 0 #fi + +Int #if CURR =/=Int NEW andBool ORIG ==Int NEW #then Gsstoreset < SCHED > #else 0 #fi + requires Ghasstategas << SCHED >> + [concrete] + rule [Rsstore.new]: Rsstore(SCHED, NEW, CURR, ORIG) => #if CURR =/=Int NEW andBool ORIG ==Int CURR andBool NEW ==Int 0 #then @@ -166,7 +180,7 @@ module GAS-FEES 0 #fi #fi - requires Ghasdirtysstore << SCHED >> + requires Ghasdirtysstore << SCHED >> andBool notBool Ghasstategas << SCHED >> [concrete] rule [Rsstore.old]: From 80a19b04467e7686031820331fd9359f1f6ead34 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Mon, 20 Jul 2026 13:29:33 +0300 Subject: [PATCH 05/11] kproj/{evm,driver}.md: eip-8037 CREATE new-account OOG halts caller and top-frame state-gas refill on create-tx failure On the CREATE/CREATE2 opcode path the new-account state-gas charge is lifted out of #create into #chargeCreateNewAccount, run before #create, so an OOG there halts the calling frame cleanly instead of leaving a dangling #codeDeposit that popped a never-pushed call frame. The charge uses #chargeStateGasForCreate, whose out-of-gas rule drops the trailing handler. On create-transaction failure (init-code halt, code-deposit halt, and oversized/invalid deployed code) #refillTopFrameStateGas discards the top frame's refillable state gas (reservoir reset to the tx reservoir, spilled folded into the burned regular gas), matching EELS refill_frame_state_gas. It is gated to the top create-tx frame (callDepth -1, empty 'to') and is inert on non-state-gas forks. Unmasks the now-passing state_gas_create fixtures in failing.llvm. Co-Authored-By: Claude Fable 5 --- .../kevm_pyk/kproj/evm-semantics/driver.md | 3 +- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 59 +++++++++++++++++-- 2 files changed, 55 insertions(+), 7 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md index 60257ae34a..ef20a4c259 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -122,6 +122,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a ~> #loadAccessList(TA) ~> #loadAuthorities(AUTH) ~> #checkCreate ACCTFROM VALUE + ~> #chargeCreateNewAccount #newAddr(ACCTFROM, NONCE) -1 ~> #create ACCTFROM #newAddr(ACCTFROM, NONCE) VALUE CODE ~> #finishTx ~> #finalizeTx(false, Ctxfloor(SCHED, CODE)) ~> startTx ... @@ -206,7 +207,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax EthereumCommand ::= "#finishTx" // -------------------------------------- - rule _:ExceptionalStatusCode #halt ~> #finishTx => #popCallStack ~> #popWorldState ... + rule _:ExceptionalStatusCode #halt ~> #finishTx => #popCallStack ~> #popWorldState ~> #refillTopFrameStateGas ... rule EVMC_REVERT #halt ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund (GAVAIL +Gas SGS) ... GAVAIL SGS 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 0cf580eb17..3b441850da 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1952,6 +1952,23 @@ System Transaction Configuration true rule #restoreStateGas _ _ => .K ... false + syntax InternalOp ::= "#refillTopFrameStateGas" + // ----------------------------------------------- + rule #refillTopFrameStateGas => .K ... + true + -1 + SCHED + _ => #txStateGasReservoir(SCHED, GLIMIT) + _ => 0 + ListItem(TXID:Int) ... + + TXID + GLIMIT + .Account + ... + + rule #refillTopFrameStateGas => .K ... [owise] + rule #setLocalMem START WIDTH WS => .K ... LM => LM [ START := #range(WS, 0, minInt(WIDTH, lengthBytes(WS))) ] @@ -2029,20 +2046,24 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- ```k syntax InternalOp ::= "#create" Int Int Int Bytes + | "#chargeCreateNewAccount" Int Int | "#mkCreate" Int Int Int Bytes | "#incrementNonce" Int | "#checkCreate" Int Int // -------------------------------------------- rule #create ACCTFROM ACCTTO VALUE INITCODE - => #accountNonexistent(ACCTTO) ~> #chargeCreateNewAccountStateGas(CD) - ~> #incrementNonce ACCTFROM + => #incrementNonce ACCTFROM ~> #pushCallStack ~> #pushWorldState ~> #newAccount ACCTTO ~> #transferFunds ACCTFROM ACCTTO VALUE ~> #mkCreate ACCTFROM ACCTTO VALUE INITCODE ... - CD + + rule #chargeCreateNewAccount ACCTTO CD + => #accountNonexistent(ACCTTO) ~> #chargeCreateNewAccountStateGas(CD) + ... + rule #mkCreate ACCTFROM ACCTTO VALUE INITCODE => #touchAccounts ACCTFROM ACCTTO ~> #accessAccounts ACCTFROM ACCTTO ~> #loadProgram INITCODE ~> #initVM ~> #execute @@ -2106,7 +2127,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- OUT => .Bytes requires lengthBytes(OUT) <=Int maxCodeSize < SCHED > andBool #isValidCode(OUT, SCHED) - rule #mkCodeDeposit _ACCT => #popCallStack ~> #popWorldState ~> 0 ~> #push ... + rule #mkCodeDeposit _ACCT => #popCallStack ~> #popWorldState ~> #refillTopFrameStateGas ~> 0 ~> #push ... SCHED OUT => .Bytes requires notBool ( lengthBytes(OUT) <=Int maxCodeSize < SCHED > andBool #isValidCode(OUT, SCHED) ) @@ -2136,7 +2157,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- FRONTIER rule _:ExceptionalStatusCode - #halt ~> #finishCodeDeposit _ _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... + #halt ~> #finishCodeDeposit _ _ => #popCallStack ~> #popWorldState ~> #refillTopFrameStateGas ~> 0 ~> #push ... SCHED requires SCHED =/=K FRONTIER @@ -2152,6 +2173,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- CREATE VALUE MEMSTART MEMWIDTH => #accessAccounts #newAddr(ACCT, NONCE) ~> #checkCreate ACCT VALUE + ~> #chargeCreateNewAccount #newAddr(ACCT, NONCE) CD ~> #create ACCT #newAddr(ACCT, NONCE) VALUE #range(LM, MEMSTART, MEMWIDTH) ~> #codeDeposit #newAddr(ACCT, NONCE) ... @@ -2164,6 +2186,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- ... SCHED + CD requires #hasValidInitCode(MEMWIDTH, SCHED) [preserves-definedness] @@ -2180,6 +2203,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- CREATE2 VALUE MEMSTART MEMWIDTH SALT => #accessAccounts #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) ~> #checkCreate ACCT VALUE + ~> #chargeCreateNewAccount #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) CD ~> #create ACCT #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) VALUE #range(LM, MEMSTART, MEMWIDTH) ~> #codeDeposit #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) ... @@ -2187,6 +2211,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- ACCT LM SCHED + CD requires #hasValidInitCode(MEMWIDTH, SCHED) rule [create2-invalid]: @@ -2849,6 +2874,28 @@ Overall Gas rule _:Gas ~> #chargeStateGas => .K ... false + syntax InternalOp ::= "#chargeStateGasForCreate" + // ------------------------------------------------ + rule A:Gas ~> #chargeStateGasForCreate => .K ... + true + R => R -Gas A + requires A <=Gas R + + rule A:Gas ~> #chargeStateGasForCreate => .K ... + true + R => 0:Gas + S => S +Gas (A -Gas R) + G => G -Gas (A -Gas R) + requires R A:Gas ~> #chargeStateGasForCreate ~> #create _ _ _ _ ~> #codeDeposit _ => #end EVMC_OUT_OF_GAS ... + true + R + G + requires R _:Gas ~> #chargeStateGasForCreate => .K ... false + rule A:Gas ~> #creditStateGas => .K ... true S => S -Gas minGas(A, S) @@ -2905,7 +2952,7 @@ Overall Gas SCHED rule true ~> #chargeCreateNewAccountStateGas(CD) - => #if Ghasstategas << SCHED >> #then Gnewaccount < SCHED > #else 0 #fi ~> #chargeStateGas + => #if Ghasstategas << SCHED >> #then Gnewaccount < SCHED > #else 0 #fi ~> #chargeStateGasForCreate ... SCHED From 4c9d6781aebc04b71485f2ba66fdff078a053660 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Mon, 20 Jul 2026 17:18:41 +0300 Subject: [PATCH 06/11] kproj/{evm,driver}.md: charge eip-8037 create new-account state gas before the 63/64 split EELS generic_create charges NEW_ACCOUNT state gas before computing create_message_gas = max_message_call_gas(gas_left), so the charge draws from the caller's full remaining gas. KEVM ran #allocateCreateGas first (from NEW_ACCOUNT into regular gas hit a spurious OOG and burned the whole transaction. Wrap the charge in #unallocateCreateGas / #allocateCreateGas so the 63/64 split is taken after it, matching the reference. The round trip is exact (#allBut64th(G) +Int G /Int 64 ==Int G) and the charge is 0 without Ghasstategas, so pre-Amsterdam behavior is unchanged; the early allocation is kept because the #checkCreate failure paths refund . Also refill the top-frame state gas when a create transaction reverts: the EVMC_REVERT #finishTx rule returned the spilled gas but left set, so a reverted create kept its NEW_ACCOUNT charge in the state dimension. The reference treats the prepare_dispatch charges as refillable -- they pay for state that rolls back with the dispatched frame. Unmask the four inner_create_succeeds_code_deposit_state_gas sub-cases, which now report exactly 2 * 183600 + 1 * 1530 = 368730 state gas. The remaining failed_create_tx_refills_top_frame_new_account[revert] sub-case stays masked: its state gas is correctly 0 and the residual 256 gas is the calldata floor (23320) versus the v7.1.0 fixture's pre-floor 23064 -- the known floor placement drift, not a state-gas defect. Co-Authored-By: Claude Fable 5 --- .../src/kevm_pyk/kproj/evm-semantics/driver.md | 2 +- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 15 ++++++++++++++- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md index ef20a4c259..a19f6bf59d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -208,7 +208,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax EthereumCommand ::= "#finishTx" // -------------------------------------- rule _:ExceptionalStatusCode #halt ~> #finishTx => #popCallStack ~> #popWorldState ~> #refillTopFrameStateGas ... - rule EVMC_REVERT #halt ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund (GAVAIL +Gas SGS) ... + rule EVMC_REVERT #halt ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund (GAVAIL +Gas SGS) ~> #refillTopFrameStateGas ... GAVAIL SGS 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 3b441850da..7e089c9a42 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -2173,7 +2173,9 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- CREATE VALUE MEMSTART MEMWIDTH => #accessAccounts #newAddr(ACCT, NONCE) ~> #checkCreate ACCT VALUE + ~> #unallocateCreateGas ~> #chargeCreateNewAccount #newAddr(ACCT, NONCE) CD + ~> #allocateCreateGas ~> #create ACCT #newAddr(ACCT, NONCE) VALUE #range(LM, MEMSTART, MEMWIDTH) ~> #codeDeposit #newAddr(ACCT, NONCE) ... @@ -2203,7 +2205,9 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- CREATE2 VALUE MEMSTART MEMWIDTH SALT => #accessAccounts #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) ~> #checkCreate ACCT VALUE + ~> #unallocateCreateGas ~> #chargeCreateNewAccount #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) CD + ~> #allocateCreateGas ~> #create ACCT #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) VALUE #range(LM, MEMSTART, MEMWIDTH) ~> #codeDeposit #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) ... @@ -2888,7 +2892,7 @@ Overall Gas G => G -Gas (A -Gas R) requires R A:Gas ~> #chargeStateGasForCreate ~> #create _ _ _ _ ~> #codeDeposit _ => #end EVMC_OUT_OF_GAS ... + rule A:Gas ~> #chargeStateGasForCreate ~> #allocateCreateGas ~> #create _ _ _ _ ~> #codeDeposit _ => #end EVMC_OUT_OF_GAS ... true R G @@ -3283,6 +3287,15 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). rule GCALL:Gas ~> #allocateCallGas => .K ... _ => GCALL + syntax InternalOp ::= "#unallocateCreateGas" + // -------------------------------------------- + rule #unallocateCreateGas => .K ... + GAVAIL => GAVAIL +Gas GCALL + GCALL => 0 + true + + rule #unallocateCreateGas => .K ... false + syntax InternalOp ::= "#allocateCreateGas" // ------------------------------------------ rule SCHED From 8eb365f86a3dfc6285f08ec702cc6ce975a3de9d Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Mon, 20 Jul 2026 19:29:57 +0300 Subject: [PATCH 07/11] kproj/{evm,driver}.md: align eip-8037 frame state-gas lifecycle, eip-7702 auth charges, and CALL/SELFDESTRUCT charge sites with EELS Per-frame spill: now resets at child-frame entry (#startFrameStateGas) and #restoreStateGas accumulates the child's own spill into the parent on success, so revert refunds (GAVAIL + spill) and LIFO state-gas credits stop double-counting ancestor spill in nested chains. Child-failure refunds: parent-side NEW_ACCOUNT charges (CALL value to dead account, CREATE/CREATE2) are recorded in a new callState flag and credited back via #creditChargedNewAccount on every child failure path (return.exception/revert, exceptional), matching EELS incorporate_child_on_error + credit_state_gas_refund. Dispatch charges in-frame: the tx-level (callDepth -1) NEW_ACCOUNT charges for call and create dispatch moved after #pushCallStack, so #finishTx's pop restores the post-auth fold baseline exactly like EELS refill_frame_state_gas; #refillTopFrameStateGas is now redundant and removed. The delegated-recipient dispatch access charge (#chargeDispatchDelegationAccess, Amsterdam-only) implements EELS prepare_dispatch. Auth charges: #loadAuthorities/#setDelegation/#addAuthority now thread EELS set_delegation's written-accounts / no-auth-base / touched sets; nonexistent authorities are charged Gnewaccount (state), first-writes Gaccountwrite (regular, sender and value-bearing recipient exempt), and net-new delegations Gauthbase (state, once per authority, pre-tx delegation exempt). Auth processing is bracketed by now have OOG rules) rolls back applied delegations and burns exactly tx.gas. Charge ordering: CALL charges extra regular gas, then NEW_ACCOUNT state gas, then computes the 63/64 allocation from the remaining gas (#allocateCallGasStateGas), and SELFDESTRUCT charges its state gas in the gas phase, so an OOG in either kills the calling frame instead of being mis-caught by the inner #return pop or sticking on Co-Authored-By: Claude Fable 5 --- .../kevm_pyk/kproj/evm-semantics/driver.md | 111 ++++++++----- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 146 ++++++++++++++---- 2 files changed, 185 insertions(+), 72 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md index a19f6bf59d..adda0b7d59 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -122,7 +122,6 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a ~> #loadAccessList(TA) ~> #loadAuthorities(AUTH) ~> #checkCreate ACCTFROM VALUE - ~> #chargeCreateNewAccount #newAddr(ACCTFROM, NONCE) -1 ~> #create ACCTFROM #newAddr(ACCTFROM, NONCE) VALUE CODE ~> #finishTx ~> #finalizeTx(false, Ctxfloor(SCHED, CODE)) ~> startTx ... @@ -162,7 +161,9 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a => #accessAccounts ACCTFROM ACCTTO #precompiledAccountsSet(SCHED) ~> #deductBlobGas ~> #loadAccessList(TA) + ~> #pushWorldState ~> #pushCallStack ~> #loadAuthorities(AUTH) + ~> #dropWorldState ~> #dropCallStack ~> #checkCall ACCTFROM VALUE ~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE DATA false ~> #finishTx ~> #finalizeTx(false, Ctxfloor(SCHED, DATA)) ~> startTx @@ -207,8 +208,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax EthereumCommand ::= "#finishTx" // -------------------------------------- - rule _:ExceptionalStatusCode #halt ~> #finishTx => #popCallStack ~> #popWorldState ~> #refillTopFrameStateGas ... - rule EVMC_REVERT #halt ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund (GAVAIL +Gas SGS) ~> #refillTopFrameStateGas ... + rule _:ExceptionalStatusCode #halt ~> #finishTx => #popCallStack ~> #popWorldState ... + rule EVMC_REVERT #halt ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund (GAVAIL +Gas SGS) ... GAVAIL SGS @@ -270,19 +271,21 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a Processing SetCode Transaction Authority Entries ================================================ -- The `#loadAuthorities` function processes authorization entries in EIP-7702 SetCode transactions, charging 25000 gas per tuple regardless of validity. +- The `#loadAuthorities` function processes authorization entries in EIP-7702 SetCode transactions, charging 25000 gas per tuple regardless of validity on pre-Amsterdam schedules. - Skips processing if transaction is not SetCode type; processes each authorization tuple by recovering the signer and attempting delegation. +- The Amsterdam (`Ghasstategas`) charge model threads three sets through the tuple loop, mirroring EELS `set_delegation`: accounts already written by the transaction (seeded with the sender, plus the recipient of a value-bearing call), authorities that must never be charged `Gauthbase` again (delegated before the transaction, or already charged), and authorities touched by an earlier tuple. - The `#addAuthority` function implements EIP-7702 verification and delegation: - Validates that the chain ID matches current chain (or is 0) and nonce is within bounds - Checks if authority account code is empty or already delegated - Verifies that the authority nonce equals authorization nonce - Sets delegation code (0xEF0100 + address) and increments nonce on success - - Provides refund (25000 - 12500 = 12500 gas) only for accounts that existed before processing - - A new account will be created for Authorities that are not in the `` state, without increasing the refund amount + - Pre-Amsterdam: provides refund (25000 - 12500 = 12500 gas) only for accounts that existed before processing; a new account will be created for Authorities that are not in the `` state, without increasing the refund amount + - Amsterdam: charges `Gnewaccount` state gas for authorities with no account leaf, `Gaccountwrite` regular gas on the transaction's first write to the authority, and `Gauthbase` state gas at most once per authority for a net-new delegation indicator ```k syntax InternalOp ::= #loadAuthorities ( List ) [symbol(#loadAuthorities)] - // -------------------------------------------------------------------------- + | #loadAuthorities ( List , Set , Set , Set ) [symbol(#loadAuthoritiesAux)] + // ----------------------------------------------------------------------------------------------- rule #loadAuthorities(_) => .K ... ListItem(TXID:Int) ... @@ -292,60 +295,56 @@ Processing SetCode Transaction Authority Entries requires notBool TXTYPE ==K SetCode - rule #loadAuthorities( .List ) => .K ... + rule #loadAuthorities(AUTHS) + => #loadAuthorities(AUTHS, SetItem(ORG) |Set (#if VALUE >Int 0 #then SetItem(TT) #else .Set #fi), .Set, .Set) + ... + ORG ListItem(TXID:Int) ... TXID SetCode + TT + VALUE ... - rule #loadAuthorities (ListItem(ListItem(CID) ListItem(ADDR) ListItem(NONCE) ListItem(YPAR) ListItem(SIGR) ListItem(SIGS)) REST ) - => #setDelegation (#recoverAuthority(CID, ADDR, NONCE, YPAR, SIGR, SIGS), CID, NONCE, ADDR) - ~> #loadAuthorities (REST) + rule #loadAuthorities( .List, _, _, _ ) => .K ... + + rule #loadAuthorities (ListItem(ListItem(CID) ListItem(ADDR) ListItem(NONCE) ListItem(YPAR) ListItem(SIGR) ListItem(SIGS)) REST, W, NB, T) + => #setDelegation (#recoverAuthority(CID, ADDR, NONCE, YPAR, SIGR, SIGS), CID, NONCE, ADDR, REST, W, NB, T) ... - ListItem(TXID:Int) ... - - TXID - SetCode - ... - SCHED GLIMIT => GLIMIT -Int 25000 requires notBool Ghasstategas << SCHED >> - [owise] - rule #loadAuthorities (ListItem(ListItem(CID) ListItem(ADDR) ListItem(NONCE) ListItem(YPAR) ListItem(SIGR) ListItem(SIGS)) REST ) - => Gauthbase < SCHED > ~> #chargeStateGasIntoCallGas - ~> #setDelegation (#recoverAuthority(CID, ADDR, NONCE, YPAR, SIGR, SIGS), CID, NONCE, ADDR) - ~> #loadAuthorities (REST) + rule #loadAuthorities (ListItem(ListItem(CID) ListItem(ADDR) ListItem(NONCE) ListItem(YPAR) ListItem(SIGR) ListItem(SIGS)) REST, W, NB, T) + => #setDelegation (#recoverAuthority(CID, ADDR, NONCE, YPAR, SIGR, SIGS), CID, NONCE, ADDR, REST, W, NB, T) ... - ListItem(TXID:Int) ... - - TXID - SetCode - ... - SCHED requires Ghasstategas << SCHED >> - [owise] - syntax InternalOp ::= #setDelegation ( Account , Bytes , Bytes , Bytes ) [symbol(#setDelegation)] - // ------------------------------------------------------------------------------------------------- - rule #setDelegation(AUTHORITY, CID, NONCE, _ADDR) => .K ... ENV_CID + syntax InternalOp ::= #setDelegation ( Account , Bytes , Bytes , Bytes , List , Set , Set , Set ) [symbol(#setDelegation)] + // -------------------------------------------------------------------------------------------------------------------------- + rule #setDelegation(AUTHORITY, CID, NONCE, _ADDR, REST, W, NB, T) => #loadAuthorities(REST, W, NB, T) ... ENV_CID requires AUTHORITY ==K .Account orBool (notBool #asWord(CID) in (SetItem(ENV_CID) SetItem(0))) orBool (#asWord(NONCE) >=Int maxUInt64) - rule #setDelegation(AUTHORITY, CID, NONCE, ADDR) + rule #setDelegation(AUTHORITY, CID, NONCE, ADDR, REST, W, NB, T) => #touchAccounts AUTHORITY ~> #accessAccounts AUTHORITY - ~> #addAuthority(AUTHORITY, CID, NONCE, ADDR) + ~> #addAuthority(AUTHORITY, CID, NONCE, ADDR, REST, W, NB, T) ... [owise] - syntax InternalOp ::= #addAuthority ( Account , Bytes , Bytes , Bytes ) [symbol(#addAuthority)] - // ----------------------------------------------------------------------------------------------- - rule #addAuthority(AUTHORITY, _CID, NONCE, _ADDR) => .K ... + syntax Set ::= #authNoBase ( Set , Set , Account , Bytes ) [symbol(#authNoBase), function, total] + // ------------------------------------------------------------------------------------------------- + rule #authNoBase(NB, T, AUTHORITY, ACCTCODE) => NB |Set SetItem(AUTHORITY) + requires notBool AUTHORITY in T andBool #isValidDelegation(ACCTCODE) + rule #authNoBase(NB, _, _, _) => NB [owise] + + syntax InternalOp ::= #addAuthority ( Account , Bytes , Bytes , Bytes , List , Set , Set , Set ) [symbol(#addAuthority)] + // ------------------------------------------------------------------------------------------------------------------------ + rule #addAuthority(AUTHORITY, _CID, NONCE, _ADDR, REST, W, NB, T) => #loadAuthorities(REST, W, NB, T) ... AUTHORITY ACCTCODE @@ -355,7 +354,7 @@ Processing SetCode Transaction Authority Entries requires notBool (ACCTCODE ==K .Bytes orBool #isValidDelegation(ACCTCODE)) orBool (notBool #asWord(NONCE) ==K ACCTNONCE) - rule #addAuthority(AUTHORITY, _CID, NONCE, ADDR) => .K ... + rule #addAuthority(AUTHORITY, _CID, NONCE, ADDR, REST, W, NB, T) => #loadAuthorities(REST, W, NB, T) ... SCHED REFUND => REFUND +Int Gnewaccount < SCHED > -Int Gauthbase < SCHED > @@ -368,7 +367,12 @@ Processing SetCode Transaction Authority Entries andBool (ACCTCODE ==K .Bytes orBool #isValidDelegation(ACCTCODE)) andBool #asWord(NONCE) ==K ACCTNONCE - rule #addAuthority(AUTHORITY, _CID, NONCE, ADDR) => .K ... + rule #addAuthority(AUTHORITY, _CID, NONCE, ADDR, REST, W, NB, T) + => #if Ghasstategas << SCHED >> andBool notBool AUTHORITY in W #then Gaccountwrite < SCHED > #else 0 #fi ~> #deductCallGas + ~> #if Ghasstategas << SCHED >> andBool #asWord(ADDR) =/=Int 0 andBool notBool AUTHORITY in #authNoBase(NB, T, AUTHORITY, ACCTCODE) #then Gauthbase < SCHED > #else 0 #fi ~> #chargeStateGasIntoCallGas + ~> #loadAuthorities(REST, W |Set SetItem(AUTHORITY), #authNoBase(NB, T, AUTHORITY, ACCTCODE) |Set (#if #asWord(ADDR) =/=Int 0 #then SetItem(AUTHORITY) #else .Set #fi), T |Set SetItem(AUTHORITY)) + ... + SCHED AUTHORITY @@ -380,7 +384,30 @@ Processing SetCode Transaction Authority Entries andBool (ACCTCODE ==K .Bytes orBool #isValidDelegation(ACCTCODE)) andBool #asWord(NONCE) ==K ACCTNONCE - rule #addAuthority(AUTHORITY, _CID, NONCE, ADDR) => .K ... + rule #addAuthority(AUTHORITY, _CID, NONCE, ADDR, REST, W, NB, T) => #loadAuthorities(REST, W, NB, T) ... + SCHED + + ( .Bag + => + + AUTHORITY + #if #asWord(ADDR) ==Int 0 #then .Bytes #else EOA_DELEGATION_MARKER +Bytes ADDR #fi + 1 + ... + + ) + ... + + requires #asWord(NONCE) ==Int 0 andBool notBool #accountExists(AUTHORITY) + andBool notBool Ghasstategas << SCHED >> + + rule #addAuthority(AUTHORITY, _CID, NONCE, ADDR, REST, W, NB, T) + => Gnewaccount < SCHED > ~> #chargeStateGasIntoCallGas + ~> #if notBool AUTHORITY in W #then Gaccountwrite < SCHED > #else 0 #fi ~> #deductCallGas + ~> #if #asWord(ADDR) =/=Int 0 #then Gauthbase < SCHED > #else 0 #fi ~> #chargeStateGasIntoCallGas + ~> #loadAuthorities(REST, W |Set SetItem(AUTHORITY), NB |Set (#if #asWord(ADDR) =/=Int 0 #then SetItem(AUTHORITY) #else .Set #fi), T |Set SetItem(AUTHORITY)) + ... + SCHED ( .Bag @@ -395,8 +422,10 @@ Processing SetCode Transaction Authority Entries ... requires #asWord(NONCE) ==Int 0 andBool notBool #accountExists(AUTHORITY) + andBool Ghasstategas << SCHED >> - rule #addAuthority(AUTHORITY, _CID, NONCE, _ADDR) => .K ... requires notBool (#accountExists(AUTHORITY) orBool #asWord(NONCE) ==Int 0) + rule #addAuthority(AUTHORITY, _CID, NONCE, _ADDR, REST, W, NB, T) => #loadAuthorities(REST, W, NB, T) ... + requires notBool (#accountExists(AUTHORITY) orBool #asWord(NONCE) ==Int 0) ``` - `exception` only clears from the `` cell if there is an exception preceding it. 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 7e089c9a42..e21d921ef5 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -78,6 +78,7 @@ In the comments next to each cell, we've marked which component of the YellowPap 0:Gas 0:Gas + false .Account @@ -314,6 +315,7 @@ Control Flow rule #halt ~> (_:Int => .K) ... rule #halt ~> (_:OpCode => .K) ... + rule #halt ~> (_:BExp => .K) ... ``` OpCode Execution @@ -1717,7 +1719,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d rule [call.delegatedAuthority]: #call ACCTFROM ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC => #let DELEGATED_ACCOUNT = #asAccount(#range(CODE,3,20)) #in - (#accessAccounts DELEGATED_ACCOUNT + (#chargeDispatchDelegationAccess DELEGATED_ACCOUNT + ~> #accessAccounts DELEGATED_ACCOUNT ~> #callWithCode ACCTFROM ACCTTO ACCTCODE #getAccountCode(DELEGATED_ACCOUNT) VALUE APPVALUE ARGS STATIC ) ... @@ -1730,6 +1733,18 @@ The various `CALL*` (and other inter-contract control flow) operations will be d requires Ghasauthority << SCHED >> andBool #isValidDelegation (CODE) + syntax InternalOp ::= "#chargeDispatchDelegationAccess" Account + // --------------------------------------------------------------- + rule #chargeDispatchDelegationAccess ACCT + => (#if ACCT in ACCTS #then Gwarmstorageread < SCHED > #else Gcoldaccountaccess < SCHED > #fi) ~> #deductCallGas + ... + + -1 + ACCTS + SCHED + requires Ghasstategas << SCHED >> + rule #chargeDispatchDelegationAccess _ => .K ... [owise] + rule [call.true]: #call ACCTFROM ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC => #callWithCode ACCTFROM ACCTTO ACCTCODE CODE VALUE APPVALUE ARGS STATIC @@ -1751,13 +1766,24 @@ The various `CALL*` (and other inter-contract control flow) operations will be d [owise] rule #callWithCode ACCTFROM ACCTTO ACCTCODE BYTES VALUE APPVALUE ARGS STATIC - => #accountNonexistent(ACCTTO) ~> #chargeNewAccountStateGas(VALUE, CD) - ~> #pushCallStack ~> #pushWorldState + => #pushCallStack ~> #pushWorldState + ~> #startFrameStateGas ~> #transferFunds ACCTFROM ACCTTO VALUE ~> #mkCall ACCTFROM ACCTTO ACCTCODE BYTES APPVALUE ARGS STATIC ... CD + requires CD =/=Int -1 + + rule #callWithCode ACCTFROM ACCTTO ACCTCODE BYTES VALUE APPVALUE ARGS STATIC + => #pushCallStack ~> #pushWorldState + ~> #startFrameStateGas + ~> #accountNonexistent(ACCTTO) ~> #chargeNewAccountStateGas(VALUE, -1) + ~> #transferFunds ACCTFROM ACCTTO VALUE + ~> #mkCall ACCTFROM ACCTTO ACCTCODE BYTES APPVALUE ARGS STATIC + ... + + -1 rule #mkCall ACCTFROM ACCTTO ACCTCODE BYTES APPVALUE ARGS STATIC:Bool => #touchAccounts ACCTFROM ACCTTO ~> #accessAccounts ACCTFROM ACCTTO ~> #loadProgram BYTES ~> #initVM ~> #precompiled?(ACCTCODE, SCHED) ~> #execute @@ -1909,7 +1935,7 @@ System Transaction Configuration rule [return.exception]: _:ExceptionalStatusCode #halt ~> #return _ _ - => #popCallStack ~> #popWorldState ~> 0 ~> #push + => #popCallStack ~> #popWorldState ~> #creditChargedNewAccount ~> 0 ~> #push ... _ => .Bytes @@ -1917,7 +1943,7 @@ System Transaction Configuration rule [return.revert]: EVMC_REVERT #halt ~> #return RETSTART RETWIDTH - => #popCallStack ~> #popWorldState + => #popCallStack ~> #popWorldState ~> #creditChargedNewAccount ~> 0 ~> #push ~> #refund (GAVAIL +Gas SGS) ~> #setLocalMem RETSTART RETWIDTH OUT ... @@ -1948,26 +1974,24 @@ System Transaction Configuration // -------------------------------------------------- rule #restoreStateGas R S => .K ... _ => R - _ => S + PS => PS +Gas S + _ => false true rule #restoreStateGas _ _ => .K ... false - syntax InternalOp ::= "#refillTopFrameStateGas" - // ----------------------------------------------- - rule #refillTopFrameStateGas => .K ... - true - -1 + syntax InternalOp ::= "#startFrameStateGas" + // ------------------------------------------- + rule #startFrameStateGas => .K ... + _ => 0 + _ => false + + syntax InternalOp ::= "#creditChargedNewAccount" + // ------------------------------------------------ + rule #creditChargedNewAccount => Gnewaccount < SCHED > ~> #creditStateGas ... SCHED - _ => #txStateGasReservoir(SCHED, GLIMIT) - _ => 0 - ListItem(TXID:Int) ... - - TXID - GLIMIT - .Account - ... - - rule #refillTopFrameStateGas => .K ... [owise] + true => false + rule #creditChargedNewAccount => .K ... + false rule #setLocalMem START WIDTH WS => .K ... @@ -2047,6 +2071,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- ```k syntax InternalOp ::= "#create" Int Int Int Bytes | "#chargeCreateNewAccount" Int Int + | "#chargeCreateTxNewAccount" Int Int | "#mkCreate" Int Int Int Bytes | "#incrementNonce" Int | "#checkCreate" Int Int @@ -2054,17 +2079,26 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- rule #create ACCTFROM ACCTTO VALUE INITCODE => #incrementNonce ACCTFROM ~> #pushCallStack ~> #pushWorldState + ~> #startFrameStateGas + ~> #chargeCreateTxNewAccount ACCTTO CD ~> #newAccount ACCTTO ~> #transferFunds ACCTFROM ACCTTO VALUE ~> #mkCreate ACCTFROM ACCTTO VALUE INITCODE ... + CD rule #chargeCreateNewAccount ACCTTO CD => #accountNonexistent(ACCTTO) ~> #chargeCreateNewAccountStateGas(CD) ... + rule #chargeCreateTxNewAccount ACCTTO -1 + => #accountNonexistent(ACCTTO) ~> #chargeCreateNewAccountStateGas(-1) + ... + + rule #chargeCreateTxNewAccount _ CD => .K ... requires CD =/=Int -1 + rule #mkCreate ACCTFROM ACCTTO VALUE INITCODE => #touchAccounts ACCTFROM ACCTTO ~> #accessAccounts ACCTFROM ACCTTO ~> #loadProgram INITCODE ~> #initVM ~> #execute ... @@ -2107,10 +2141,10 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- | "#finishCodeDeposit" Int Bytes // ----------------------------------------------- rule _:ExceptionalStatusCode - #halt ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... _ => .Bytes + #halt ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #creditChargedNewAccount ~> 0 ~> #push ... _ => .Bytes rule EVMC_REVERT - #halt ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund (GAVAIL +Gas SGS) ~> 0 ~> #push ... + #halt ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #creditChargedNewAccount ~> #refund (GAVAIL +Gas SGS) ~> 0 ~> #push ... GAVAIL SGS @@ -2127,7 +2161,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- OUT => .Bytes requires lengthBytes(OUT) <=Int maxCodeSize < SCHED > andBool #isValidCode(OUT, SCHED) - rule #mkCodeDeposit _ACCT => #popCallStack ~> #popWorldState ~> #refillTopFrameStateGas ~> 0 ~> #push ... + rule #mkCodeDeposit _ACCT => #popCallStack ~> #popWorldState ~> #creditChargedNewAccount ~> 0 ~> #push ... SCHED OUT => .Bytes requires notBool ( lengthBytes(OUT) <=Int maxCodeSize < SCHED > andBool #isValidCode(OUT, SCHED) ) @@ -2157,7 +2191,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- FRONTIER rule _:ExceptionalStatusCode - #halt ~> #finishCodeDeposit _ _ => #popCallStack ~> #popWorldState ~> #refillTopFrameStateGas ~> 0 ~> #push ... + #halt ~> #finishCodeDeposit _ _ => #popCallStack ~> #popWorldState ~> #creditChargedNewAccount ~> 0 ~> #push ... SCHED requires SCHED =/=K FRONTIER @@ -2228,7 +2262,7 @@ Self destructing to yourself, unlike a regular transfer, destroys the balance in ```k syntax UnStackOp ::= "SELFDESTRUCT" // ----------------------------------- - rule SELFDESTRUCT ACCTTO => #touchAccounts ACCT ACCTTO ~> #accessAccounts ACCTTO ~> #accountNonexistent(ACCTTO) ~> #chargeSelfdestructNewAccountStateGas BALFROM ~> #transferFunds ACCT ACCTTO BALFROM ~> #end EVMC_SUCCESS ... + rule SELFDESTRUCT ACCTTO => #touchAccounts ACCT ACCTTO ~> #accessAccounts ACCTTO ~> #transferFunds ACCT ACCTTO BALFROM ~> #end EVMC_SUCCESS ... SCHED ACCT SDS => SDS |Set SetItem(ACCT) @@ -2255,7 +2289,7 @@ Self destructing to yourself, unlike a regular transfer, destroys the balance in CA requires ((notBool Ghaseip6780 << SCHED >>) orBool ACCT in CA) - rule SELFDESTRUCT ACCTTO => #touchAccounts ACCT ACCTTO ~> #accessAccounts ACCTTO ~> #accountNonexistent(ACCTTO) ~> #chargeSelfdestructNewAccountStateGas BALFROM ~> #transferFunds ACCT ACCTTO BALFROM ~> #end EVMC_SUCCESS ... + rule SELFDESTRUCT ACCTTO => #touchAccounts ACCT ACCTTO ~> #accessAccounts ACCTTO ~> #transferFunds ACCT ACCTTO BALFROM ~> #end EVMC_SUCCESS ... SCHED ACCT @@ -2920,10 +2954,22 @@ Overall Gas R => 0:Gas S => S +Gas (A -Gas R) G => G -Gas (A -Gas R) - requires R A:Gas ~> #chargeStateGasIntoCallGas => #end EVMC_OUT_OF_GAS ... + true + R + G + requires R _:Gas ~> #chargeStateGasIntoCallGas => .K ... false + syntax InternalOp ::= "#deductCallGas" + // -------------------------------------- + rule A:Gas ~> #deductCallGas => .K ... true G => G -Gas A requires A <=Gas G + rule A:Gas ~> #deductCallGas => #end EVMC_OUT_OF_GAS ... true G requires G _:Gas ~> #deductCallGas => .K ... false + syntax InternalOp ::= "#chargeNewAccountStateGas" "(" Int "," Int ")" // ------------------------------------------------------------- rule true ~> #chargeNewAccountStateGas(VALUE, -1) @@ -2936,8 +2982,12 @@ Overall Gas ... SCHED + _ => Ghasstategas << SCHED >> andBool VALUE =/=Int 0 requires CD =/=Int -1 - rule false ~> #chargeNewAccountStateGas(_, _) => .K ... + rule false ~> #chargeNewAccountStateGas(_, CD) => .K ... + _ => false + requires CD =/=Int -1 + rule false ~> #chargeNewAccountStateGas(_, -1) => .K ... syntax InternalOp ::= "#chargeSelfdestructNewAccountStateGas" Int // -------------------------------------------------------------------- @@ -2960,8 +3010,12 @@ Overall Gas ... SCHED + _ => Ghasstategas << SCHED >> + requires CD =/=Int -1 + rule false ~> #chargeCreateNewAccountStateGas(CD) => .K ... + _ => false requires CD =/=Int -1 - rule false ~> #chargeCreateNewAccountStateGas(_) => .K ... + rule false ~> #chargeCreateNewAccountStateGas(-1) => .K ... syntax Bool ::= #inStorage ( Map , Account , Int ) [symbol(#inStorage), function, total] | #inStorageAux1 ( KItem , Int ) [symbol(#inStorageAux1), function, total] @@ -3123,6 +3177,17 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). GAVAIL ACCTS + requires notBool Ghasstategas << SCHED >> + + rule #gasExec(SCHED, CALL GCAP ACCTTO VALUE _ _ _ _) + => CcallExtra(SCHED, #accountNonexistent(ACCTTO), VALUE, ACCTTO in ACCTS, #accountHasAuthority(ACCTTO), #accountAuthorityIsWarm(ACCTTO)) ~> #deductGas + ~> #accountNonexistent(ACCTTO) ~> #chargeNewAccountStateGas(VALUE, CD) + ~> #allocateCallGasStateGas GCAP VALUE + ... + + ACCTS + CD + requires Ghasstategas << SCHED >> rule #gasExec(SCHED, CALLCODE GCAP ACCTTO VALUE _ _ _ _) => Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, VALUE, ACCTTO in ACCTS, #accountHasAuthority(ACCTTO), #accountAuthorityIsWarm(ACCTTO)) ~> #allocateCallGas @@ -3150,7 +3215,12 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). GAVAIL ACCTS - rule #gasExec(SCHED, SELFDESTRUCT ACCTTO) => Cselfdestruct(SCHED, #accountNonexistent(ACCTTO), BAL) ... + rule #gasExec(SCHED, SELFDESTRUCT ACCTTO) + => Cselfdestruct(SCHED, #accountNonexistent(ACCTTO), BAL) ~> #deductGas + ~> #accountNonexistent(ACCTTO) ~> #chargeSelfdestructNewAccountStateGas BAL + ~> 0 + ... + ACCTFROM SDS RF => #if ACCTFROM in SDS #then RF #else RF +Word Rselfdestruct < SCHED > #fi @@ -3312,8 +3382,22 @@ There are several helpers for calculating gas (most of them also specified in th syntax KResult ::= Int syntax Exp ::= Ccall ( Schedule , BExp , Gas , Gas , Int , Bool , Bool , Bool ) [symbol(Ccall), strict(2)] | Ccallgas ( Schedule , BExp , Gas , Gas , Int , Bool , Bool , Bool ) [symbol(Ccallgas), strict(2)] + | CcallExtra ( Schedule , BExp , Int , Bool , Bool , Bool ) [symbol(CcallExtra), strict(2)] | Cselfdestruct ( Schedule , BExp , Int ) [symbol(Cselfdestruct), strict(2)] // -------------------------------------------------------------------------------------------------------------------------- + rule CcallExtra(SCHED, ISEMPTY:Bool, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION) + => Cextra(SCHED, ISEMPTY, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION) ... + + syntax InternalOp ::= "#allocateCallGasStateGas" Int Int + // -------------------------------------------------------- + rule #allocateCallGasStateGas GCAP VALUE + => Cgascap(SCHED, GCAP, GAVAIL, 0) +Gas (#if VALUE ==Int 0 #then 0:Gas #else Gcallstipend < SCHED > #fi) ~> #allocateCallGas + ~> Cgascap(SCHED, GCAP, GAVAIL, 0) + ... + + GAVAIL + SCHED + rule Ccall(SCHED, ISEMPTY:Bool, GCAP, GAVAIL, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION) => Cextra(SCHED, ISEMPTY, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION) +Gas Cgascap(SCHED, GCAP, GAVAIL, Cextra(SCHED, ISEMPTY, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION)) ... From 723434648f3a7eb2ff41743eddb1f023db585d52 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Mon, 20 Jul 2026 19:30:09 +0300 Subject: [PATCH 08/11] kproj/{gas,state-utils}.md: enforce per-tx block-gas-remaining admission on pre-state-gas forks remaining (BLOCK_GAS_LIMIT - ) on schedules without Ghasstategas, matching EELS check_transaction's gas_available test on every fork; the Amsterdam two-dimensional admission branch is unchanged. Co-Authored-By: Claude Fable 5 --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md | 9 +++++---- .../src/kevm_pyk/kproj/evm-semantics/state-utils.md | 12 ++++++++---- 2 files changed, 13 insertions(+), 8 deletions(-) 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 97a563da35..580626fca6 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md @@ -292,13 +292,14 @@ module GAS-FEES // SCHED, GLIMIT, RES (final reservoir), SPL (final spilled) rule #txStateGasUsed(SCHED, GLIMIT, RES, SPL) => maxInt(0, #txStateGasReservoir(SCHED, GLIMIT) -Int RES +Int SPL) - syntax Bool ::= #isValidTxGasLimit ( Schedule , Int , Int , Int , Int ) [symbol(#isValidTxGasLimit), function, total] - // SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSEDREG, GASUSEDSTATE - rule #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSEDREG, GASUSEDSTATE) + syntax Bool ::= #isValidTxGasLimit ( Schedule , Int , Int , Int , Int , Int ) [symbol(#isValidTxGasLimit), function, total] + // SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSED, GASUSEDREG, GASUSEDSTATE + rule #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSED, GASUSEDREG, GASUSEDSTATE) => #if Ghasstategas << SCHED >> #then minInt(Gmaxtxgaslimit < SCHED >, TX_GAS_LIMIT) <=Int (BLOCK_GAS_LIMIT -Int GASUSEDREG) andBool TX_GAS_LIMIT <=Int (BLOCK_GAS_LIMIT -Int GASUSEDSTATE) - #else notBool Ghastxgaslimit << SCHED >> orBool TX_GAS_LIMIT <=Int Gmaxtxgaslimit < SCHED > + #else (notBool Ghastxgaslimit << SCHED >> orBool TX_GAS_LIMIT <=Int Gmaxtxgaslimit < SCHED >) + andBool TX_GAS_LIMIT <=Int (BLOCK_GAS_LIMIT -Int GASUSED) #fi syntax Gas ::= "G*" "(" Gas "," Int "," Int "," Schedule ")" [function] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md index 3e769989b0..7ceb02b270 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md @@ -600,6 +600,7 @@ The `"rlp"` key loads the block information. SCHED BASE_FEE BLOCK_GAS_LIMIT + GASUSED GASUSEDREG GASUSEDSTATE @@ -628,7 +629,7 @@ The `"rlp"` key loads the block information. andBool TX_MAX_PRIORITY_FEE <=Int TX_MAX_FEE andBool BAL >=Int TX_GAS_LIMIT *Int TX_MAX_FEE +Int VALUE andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT - andBool #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSEDREG, GASUSEDSTATE) + andBool #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, gas2Int(GASUSED), GASUSEDREG, GASUSEDSTATE) andBool size(TX_AUTH_LIST) >Int 0 andBool #checkAuthorityList(TX_AUTH_LIST) rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]] @@ -636,6 +637,7 @@ The `"rlp"` key loads the block information. BASE_FEE EXCESS_BLOB_GAS BLOCK_GAS_LIMIT + GASUSED GASUSEDREG GASUSEDSTATE @@ -667,13 +669,14 @@ The `"rlp"` key loads the block information. andBool TX_MAX_BLOB_FEE >=Int Cbasefeeperblob(SCHED, EXCESS_BLOB_GAS) andBool BAL >=Int TX_GAS_LIMIT *Int TX_MAX_FEE +Int (Ctotalblob(SCHED, size(TVH)) *Int TX_MAX_BLOB_FEE) +Int VALUE andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT - andBool #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSEDREG, GASUSEDSTATE) + andBool #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, gas2Int(GASUSED), GASUSEDREG, GASUSEDSTATE) andBool Ctotalblob(SCHED, size(TVH)) <=Int Gmaxblobgas < SCHED> rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]] SCHED BASE_FEE BLOCK_GAS_LIMIT + GASUSED GASUSEDREG GASUSEDSTATE @@ -699,12 +702,13 @@ The `"rlp"` key loads the block information. andBool TX_MAX_PRIORITY_FEE <=Int TX_MAX_FEE andBool BAL >=Int TX_GAS_LIMIT *Int TX_MAX_FEE +Int VALUE andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT - andBool #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSEDREG, GASUSEDSTATE) + andBool #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, gas2Int(GASUSED), GASUSEDREG, GASUSEDSTATE) rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]] SCHED BASE_FEE BLOCK_GAS_LIMIT + GASUSED GASUSEDREG GASUSEDSTATE @@ -729,7 +733,7 @@ The `"rlp"` key loads the block information. andBool BASE_FEE <=Int TX_GAS_PRICE andBool BAL >=Int TX_GAS_LIMIT *Int TX_GAS_PRICE +Int VALUE andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT - andBool #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, GASUSEDREG, GASUSEDSTATE) + andBool #isValidTxGasLimit(SCHED, TX_GAS_LIMIT, BLOCK_GAS_LIMIT, gas2Int(GASUSED), GASUSEDREG, GASUSEDSTATE) rule #isValidTransaction (_, _) => false [owise] ``` From 2b699722207f19695e9b1777cc513babebebf138 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Fri, 24 Jul 2026 13:15:24 +0300 Subject: [PATCH 09/11] tests/specs: add eip-8037 callState cells to closed-form spec configs --- tests/specs/benchmarks/address00-spec.k | 3 +++ tests/specs/benchmarks/bytes00-spec.k | 3 +++ tests/specs/benchmarks/dynamicarray00-spec.k | 3 +++ .../benchmarks/ecrecover00-siginvalid-spec.k | 3 +++ .../benchmarks/ecrecover00-sigvalid-spec.k | 3 +++ .../ecrecoverloop00-sig0-invalid-spec.k | 3 +++ .../ecrecoverloop00-sig1-invalid-spec.k | 3 +++ .../ecrecoverloop00-sigs-valid-spec.k | 3 +++ .../ecrecoverloop02-sig0-invalid-spec.k | 3 +++ .../ecrecoverloop02-sig1-invalid-spec.k | 3 +++ .../ecrecoverloop02-sigs-valid-spec.k | 3 +++ tests/specs/benchmarks/encode-keccak00-spec.k | 3 +++ .../benchmarks/encodepacked-keccak01-spec.k | 3 +++ tests/specs/benchmarks/keccak00-spec.k | 3 +++ .../benchmarks/overflow00-nooverflow-spec.k | 3 +++ .../benchmarks/overflow00-overflow-spec.k | 3 +++ tests/specs/benchmarks/requires01-a0gt0-spec.k | 3 +++ tests/specs/benchmarks/requires01-a0le0-spec.k | 3 +++ tests/specs/benchmarks/staticarray00-spec.k | 3 +++ .../benchmarks/staticloop00-a0lt10-spec.k | 3 +++ tests/specs/benchmarks/storagevar00-spec.k | 3 +++ tests/specs/benchmarks/storagevar01-spec.k | 3 +++ .../benchmarks/storagevar02-nooverflow-spec.k | 3 +++ .../benchmarks/storagevar02-overflow-spec.k | 3 +++ tests/specs/benchmarks/storagevar03-spec.k | 3 +++ tests/specs/benchmarks/structarg00-spec.k | 3 +++ tests/specs/benchmarks/structarg01-spec.k | 3 +++ tests/specs/erc20/ds/allowance-spec.k | 3 +++ tests/specs/erc20/ds/approve-failure-spec.k | 3 +++ tests/specs/erc20/ds/approve-success-spec.k | 3 +++ tests/specs/erc20/ds/balanceOf-spec.k | 3 +++ tests/specs/erc20/ds/totalSupply-spec.k | 3 +++ .../specs/erc20/ds/transfer-failure-1-a-spec.k | 3 +++ .../specs/erc20/ds/transfer-failure-1-b-spec.k | 3 +++ .../specs/erc20/ds/transfer-failure-1-c-spec.k | 3 +++ .../specs/erc20/ds/transfer-failure-2-a-spec.k | 3 +++ .../specs/erc20/ds/transfer-failure-2-b-spec.k | 3 +++ tests/specs/erc20/ds/transfer-success-1-spec.k | 3 +++ tests/specs/erc20/ds/transfer-success-2-spec.k | 3 +++ .../erc20/ds/transferFrom-failure-1-a-spec.k | 3 +++ .../erc20/ds/transferFrom-failure-1-b-spec.k | 3 +++ .../erc20/ds/transferFrom-failure-1-c-spec.k | 3 +++ .../erc20/ds/transferFrom-failure-1-d-spec.k | 3 +++ .../erc20/ds/transferFrom-failure-2-a-spec.k | 3 +++ .../erc20/ds/transferFrom-failure-2-b-spec.k | 3 +++ .../erc20/ds/transferFrom-failure-2-c-spec.k | 3 +++ .../erc20/ds/transferFrom-success-1-spec.k | 3 +++ .../erc20/ds/transferFrom-success-2-spec.k | 3 +++ tests/specs/erc20/hkg/allowance-spec.k | 3 +++ tests/specs/erc20/hkg/approve-spec.k | 3 +++ tests/specs/erc20/hkg/balanceOf-spec.k | 3 +++ tests/specs/erc20/hkg/totalSupply-spec.k | 3 +++ .../specs/erc20/hkg/transfer-failure-1-spec.k | 3 +++ .../specs/erc20/hkg/transfer-failure-2-spec.k | 3 +++ .../specs/erc20/hkg/transfer-success-1-spec.k | 3 +++ .../specs/erc20/hkg/transfer-success-2-spec.k | 3 +++ .../erc20/hkg/transferFrom-failure-1-spec.k | 3 +++ .../erc20/hkg/transferFrom-failure-2-spec.k | 3 +++ .../erc20/hkg/transferFrom-success-1-spec.k | 3 +++ .../erc20/hkg/transferFrom-success-2-spec.k | 3 +++ .../test-allowchangestest-testallow-0-spec.k | 3 +++ ...st-allowchangestest-testallow_fail-0-spec.k | 3 +++ ...estest-testfailallowcallstoaddress-0-spec.k | 3 +++ ...test-testfailallowchangestostorage-0-spec.k | 6 ++++++ ...t-test_max1_broken-uint256-uint256-0-spec.k | 3 +++ .../test-countertest-testincrement-0-spec.k | 9 +++++++++ ...st-emitcontracttest-testexpectemit-0-spec.k | 3 +++ ...acttest-testexpectemitcheckemitter-0-spec.k | 3 +++ ...ttest-testexpectemitdonotcheckdata-0-spec.k | 3 +++ ...pectcalltest-testexpectregularcall-0-spec.k | 3 +++ ...xpectcalltest-testexpectstaticcall-0-spec.k | 3 +++ ...everttest-test_expectrevert_bytes4-0-spec.k | 6 ++++++ ...verttest-test_expectrevert_message-0-spec.k | 3 +++ ...test-test_expectrevert_returnvalue-0-spec.k | 3 +++ ...ttest-testfail_expectrevert_bytes4-0-spec.k | 3 +++ ...stfail_expectrevert_failandsuccess-0-spec.k | 3 +++ ...rttest-testfail_expectrevert_false-0-spec.k | 6 ++++++ ...neruponlytest-testincrementasowner-0-spec.k | 6 ++++++ ...t-safetest-testwithdrawfuzz-uint96-0-spec.k | 3 +++ .../test-storetest-testaccesses-0-spec.k | 3 +++ .../test-storetest-teststoreload-0-spec.k | 3 +++ .../mcd-structured/cat-exhaustiveness-spec.k | 3 +++ .../cat-file-addr-pass-rough-spec.k | 3 +++ .../mcd-structured/dai-adduu-fail-rough-spec.k | 3 +++ .../mcd-structured/dai-symbol-pass-spec.k | 3 +++ .../dstoken-approve-fail-rough-spec.k | 3 +++ .../dsvalue-peek-pass-rough-spec.k | 3 +++ .../mcd-structured/dsvalue-read-pass-spec.k | 3 +++ .../dsvalue-read-pass-summarize-spec.k | 3 +++ .../mcd-structured/end-cash-pass-rough-spec.k | 12 ++++++++++++ .../mcd-structured/end-pack-pass-rough-spec.k | 12 ++++++++++++ .../specs/mcd-structured/end-subuu-pass-spec.k | 3 +++ .../flapper-yank-pass-rough-spec.k | 6 ++++++ .../flipper-addu48u48-fail-rough-spec.k | 3 +++ .../flipper-bids-pass-rough-spec.k | 3 +++ .../mcd-structured/flipper-tau-pass-spec.k | 3 +++ .../mcd-structured/flipper-ttl-pass-spec.k | 3 +++ .../mcd-structured/flopper-cage-pass-spec.k | 3 +++ ...r-dent-guy-diff-tic-not-0-pass-rough-spec.k | 12 ++++++++++++ .../flopper-dent-guy-same-pass-rough-spec.k | 9 +++++++++ .../flopper-kick-pass-rough-spec.k | 6 ++++++ .../flopper-tick-pass-rough-spec.k | 6 ++++++ .../mcd-structured/pot-join-pass-rough-spec.k | 12 ++++++++++++ .../mcd-structured/vat-addui-fail-rough-spec.k | 3 +++ .../specs/mcd-structured/vat-arithmetic-spec.k | 18 ++++++++++++++++++ tests/specs/mcd-structured/vat-dai-pass-spec.k | 3 +++ .../vat-deny-diff-fail-rough-spec.k | 3 +++ .../vat-flux-diff-pass-rough-spec.k | 3 +++ .../mcd-structured/vat-flux-diff-pass-spec.k | 3 +++ .../mcd-structured/vat-fold-pass-rough-spec.k | 3 +++ .../vat-fork-diff-pass-rough-spec.k | 3 +++ .../vat-frob-diff-zero-dart-pass-rough-spec.k | 3 +++ .../specs/mcd-structured/vat-heal-pass-spec.k | 3 +++ .../mcd-structured/vat-move-diff-rough-spec.k | 3 +++ tests/specs/mcd-structured/vat-sin-pass-spec.k | 3 +++ .../mcd-structured/vat-slip-pass-rough-spec.k | 3 +++ .../mcd-structured/vat-subui-fail-rough-spec.k | 3 +++ .../mcd-structured/vow-fess-fail-rough-spec.k | 6 ++++++ .../mcd-structured/vow-flog-fail-rough-spec.k | 9 +++++++++ tests/specs/mcd/cat-exhaustiveness-spec.k | 3 +++ .../specs/mcd/cat-file-addr-pass-rough-spec.k | 3 +++ tests/specs/mcd/dai-adduu-fail-rough-spec.k | 3 +++ tests/specs/mcd/dai-symbol-pass-spec.k | 3 +++ .../mcd/dstoken-approve-fail-rough-spec.k | 3 +++ tests/specs/mcd/dsvalue-peek-pass-rough-spec.k | 3 +++ tests/specs/mcd/dsvalue-read-pass-spec.k | 3 +++ .../mcd/dsvalue-read-pass-summarize-spec.k | 3 +++ tests/specs/mcd/end-cash-pass-rough-spec.k | 12 ++++++++++++ tests/specs/mcd/end-pack-pass-rough-spec.k | 12 ++++++++++++ tests/specs/mcd/end-subuu-pass-spec.k | 3 +++ tests/specs/mcd/flapper-yank-pass-rough-spec.k | 6 ++++++ .../mcd/flipper-addu48u48-fail-rough-spec.k | 3 +++ tests/specs/mcd/flipper-bids-pass-rough-spec.k | 3 +++ tests/specs/mcd/flipper-tau-pass-spec.k | 3 +++ tests/specs/mcd/flipper-ttl-pass-spec.k | 3 +++ tests/specs/mcd/flopper-cage-pass-spec.k | 3 +++ ...r-dent-guy-diff-tic-not-0-pass-rough-spec.k | 12 ++++++++++++ .../flopper-dent-guy-same-pass-rough-spec.k | 9 +++++++++ tests/specs/mcd/flopper-kick-pass-rough-spec.k | 6 ++++++ tests/specs/mcd/flopper-tick-pass-rough-spec.k | 6 ++++++ tests/specs/mcd/pot-join-pass-rough-spec.k | 12 ++++++++++++ tests/specs/mcd/vat-addui-fail-rough-spec.k | 3 +++ tests/specs/mcd/vat-arithmetic-spec.k | 18 ++++++++++++++++++ tests/specs/mcd/vat-dai-pass-spec.k | 3 +++ .../specs/mcd/vat-deny-diff-fail-rough-spec.k | 3 +++ .../specs/mcd/vat-flux-diff-pass-rough-spec.k | 3 +++ tests/specs/mcd/vat-flux-diff-pass-spec.k | 3 +++ tests/specs/mcd/vat-fold-pass-rough-spec.k | 3 +++ .../specs/mcd/vat-fork-diff-pass-rough-spec.k | 3 +++ .../vat-frob-diff-zero-dart-pass-rough-spec.k | 3 +++ tests/specs/mcd/vat-heal-pass-spec.k | 3 +++ tests/specs/mcd/vat-move-diff-rough-spec.k | 3 +++ tests/specs/mcd/vat-sin-pass-spec.k | 3 +++ tests/specs/mcd/vat-slip-pass-rough-spec.k | 3 +++ tests/specs/mcd/vat-subui-fail-rough-spec.k | 3 +++ tests/specs/mcd/vow-fess-fail-rough-spec.k | 6 ++++++ tests/specs/mcd/vow-flog-fail-rough-spec.k | 9 +++++++++ 157 files changed, 639 insertions(+) diff --git a/tests/specs/benchmarks/address00-spec.k b/tests/specs/benchmarks/address00-spec.k index cac1b7a569..f6b7aa1633 100644 --- a/tests/specs/benchmarks/address00-spec.k +++ b/tests/specs/benchmarks/address00-spec.k @@ -32,6 +32,9 @@ module ADDRESS00-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/bytes00-spec.k b/tests/specs/benchmarks/bytes00-spec.k index 599f9c2a67..fdbdd9d575 100644 --- a/tests/specs/benchmarks/bytes00-spec.k +++ b/tests/specs/benchmarks/bytes00-spec.k @@ -32,6 +32,9 @@ module BYTES00-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/dynamicarray00-spec.k b/tests/specs/benchmarks/dynamicarray00-spec.k index 1166baee0c..314da32bac 100644 --- a/tests/specs/benchmarks/dynamicarray00-spec.k +++ b/tests/specs/benchmarks/dynamicarray00-spec.k @@ -32,6 +32,9 @@ module DYNAMICARRAY00-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/ecrecover00-siginvalid-spec.k b/tests/specs/benchmarks/ecrecover00-siginvalid-spec.k index 3b14305654..b6e207adfb 100644 --- a/tests/specs/benchmarks/ecrecover00-siginvalid-spec.k +++ b/tests/specs/benchmarks/ecrecover00-siginvalid-spec.k @@ -32,6 +32,9 @@ module ECRECOVER00-SIGINVALID-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/ecrecover00-sigvalid-spec.k b/tests/specs/benchmarks/ecrecover00-sigvalid-spec.k index e1f1a8c2b4..fa5046cefd 100644 --- a/tests/specs/benchmarks/ecrecover00-sigvalid-spec.k +++ b/tests/specs/benchmarks/ecrecover00-sigvalid-spec.k @@ -32,6 +32,9 @@ module ECRECOVER00-SIGVALID-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k b/tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k index 06d397de6e..9a28f36149 100644 --- a/tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k +++ b/tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k @@ -35,6 +35,9 @@ module ECRECOVERLOOP00-SIG0-INVALID-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k b/tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k index d8770ce221..ddccaf31ef 100644 --- a/tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k +++ b/tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k @@ -35,6 +35,9 @@ module ECRECOVERLOOP00-SIG1-INVALID-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k b/tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k index f03e261855..8b39014eaa 100644 --- a/tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k +++ b/tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k @@ -35,6 +35,9 @@ module ECRECOVERLOOP00-SIGS-VALID-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k b/tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k index 4899e00716..90eb8d042d 100644 --- a/tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k +++ b/tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k @@ -36,6 +36,9 @@ module ECRECOVERLOOP02-SIG0-INVALID-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k b/tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k index 165a963385..f5934fb17c 100644 --- a/tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k +++ b/tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k @@ -36,6 +36,9 @@ module ECRECOVERLOOP02-SIG1-INVALID-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k b/tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k index 639e7a542e..35052cd4e7 100644 --- a/tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k +++ b/tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k @@ -36,6 +36,9 @@ module ECRECOVERLOOP02-SIGS-VALID-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/encode-keccak00-spec.k b/tests/specs/benchmarks/encode-keccak00-spec.k index d6a36babdf..f26e1937f5 100644 --- a/tests/specs/benchmarks/encode-keccak00-spec.k +++ b/tests/specs/benchmarks/encode-keccak00-spec.k @@ -32,6 +32,9 @@ module ENCODE-KECCAK00-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/encodepacked-keccak01-spec.k b/tests/specs/benchmarks/encodepacked-keccak01-spec.k index d9610a085a..c616c69c21 100644 --- a/tests/specs/benchmarks/encodepacked-keccak01-spec.k +++ b/tests/specs/benchmarks/encodepacked-keccak01-spec.k @@ -32,6 +32,9 @@ module ENCODEPACKED-KECCAK01-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/keccak00-spec.k b/tests/specs/benchmarks/keccak00-spec.k index b195c5632d..2b50ded07d 100644 --- a/tests/specs/benchmarks/keccak00-spec.k +++ b/tests/specs/benchmarks/keccak00-spec.k @@ -32,6 +32,9 @@ module KECCAK00-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/overflow00-nooverflow-spec.k b/tests/specs/benchmarks/overflow00-nooverflow-spec.k index 2cdeabf2c7..c9463ef208 100644 --- a/tests/specs/benchmarks/overflow00-nooverflow-spec.k +++ b/tests/specs/benchmarks/overflow00-nooverflow-spec.k @@ -32,6 +32,9 @@ module OVERFLOW00-NOOVERFLOW-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/overflow00-overflow-spec.k b/tests/specs/benchmarks/overflow00-overflow-spec.k index 2859aaac4a..221dad7a06 100644 --- a/tests/specs/benchmarks/overflow00-overflow-spec.k +++ b/tests/specs/benchmarks/overflow00-overflow-spec.k @@ -32,6 +32,9 @@ module OVERFLOW00-OVERFLOW-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/requires01-a0gt0-spec.k b/tests/specs/benchmarks/requires01-a0gt0-spec.k index 42e689d712..a3f8e44b49 100644 --- a/tests/specs/benchmarks/requires01-a0gt0-spec.k +++ b/tests/specs/benchmarks/requires01-a0gt0-spec.k @@ -32,6 +32,9 @@ module REQUIRES01-A0GT0-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/requires01-a0le0-spec.k b/tests/specs/benchmarks/requires01-a0le0-spec.k index c4f7e01a1e..b89759ded5 100644 --- a/tests/specs/benchmarks/requires01-a0le0-spec.k +++ b/tests/specs/benchmarks/requires01-a0le0-spec.k @@ -32,6 +32,9 @@ module REQUIRES01-A0LE0-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/staticarray00-spec.k b/tests/specs/benchmarks/staticarray00-spec.k index e5f028dc57..0463cbe5cf 100644 --- a/tests/specs/benchmarks/staticarray00-spec.k +++ b/tests/specs/benchmarks/staticarray00-spec.k @@ -32,6 +32,9 @@ module STATICARRAY00-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/staticloop00-a0lt10-spec.k b/tests/specs/benchmarks/staticloop00-a0lt10-spec.k index f31c489f99..ff777efb0f 100644 --- a/tests/specs/benchmarks/staticloop00-a0lt10-spec.k +++ b/tests/specs/benchmarks/staticloop00-a0lt10-spec.k @@ -32,6 +32,9 @@ module STATICLOOP00-A0LT10-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/storagevar00-spec.k b/tests/specs/benchmarks/storagevar00-spec.k index b5eeeb731b..5c858d8784 100644 --- a/tests/specs/benchmarks/storagevar00-spec.k +++ b/tests/specs/benchmarks/storagevar00-spec.k @@ -32,6 +32,9 @@ module STORAGEVAR00-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/storagevar01-spec.k b/tests/specs/benchmarks/storagevar01-spec.k index 4404f900b1..fe56f5797d 100644 --- a/tests/specs/benchmarks/storagevar01-spec.k +++ b/tests/specs/benchmarks/storagevar01-spec.k @@ -32,6 +32,9 @@ module STORAGEVAR01-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/storagevar02-nooverflow-spec.k b/tests/specs/benchmarks/storagevar02-nooverflow-spec.k index 12f2da51c9..c61bce6745 100644 --- a/tests/specs/benchmarks/storagevar02-nooverflow-spec.k +++ b/tests/specs/benchmarks/storagevar02-nooverflow-spec.k @@ -32,6 +32,9 @@ module STORAGEVAR02-NOOVERFLOW-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/storagevar02-overflow-spec.k b/tests/specs/benchmarks/storagevar02-overflow-spec.k index fbdcc93d01..7d0d25c51a 100644 --- a/tests/specs/benchmarks/storagevar02-overflow-spec.k +++ b/tests/specs/benchmarks/storagevar02-overflow-spec.k @@ -32,6 +32,9 @@ module STORAGEVAR02-OVERFLOW-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/storagevar03-spec.k b/tests/specs/benchmarks/storagevar03-spec.k index 1b3460e85b..57bffb5dc9 100644 --- a/tests/specs/benchmarks/storagevar03-spec.k +++ b/tests/specs/benchmarks/storagevar03-spec.k @@ -32,6 +32,9 @@ module STORAGEVAR03-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/structarg00-spec.k b/tests/specs/benchmarks/structarg00-spec.k index 3e90ea3ea2..374e94c5cd 100644 --- a/tests/specs/benchmarks/structarg00-spec.k +++ b/tests/specs/benchmarks/structarg00-spec.k @@ -32,6 +32,9 @@ module STRUCTARG00-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/benchmarks/structarg01-spec.k b/tests/specs/benchmarks/structarg01-spec.k index 448692e60f..c680629fbe 100644 --- a/tests/specs/benchmarks/structarg01-spec.k +++ b/tests/specs/benchmarks/structarg01-spec.k @@ -32,6 +32,9 @@ module STRUCTARG01-SPEC _ => ?_ false // NOTE: non-static call CD + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/allowance-spec.k b/tests/specs/erc20/ds/allowance-spec.k index 934b1c87e9..07d6c416b3 100644 --- a/tests/specs/erc20/ds/allowance-spec.k +++ b/tests/specs/erc20/ds/allowance-spec.k @@ -40,6 +40,9 @@ module ALLOWANCE-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/approve-failure-spec.k b/tests/specs/erc20/ds/approve-failure-spec.k index 0943f848bc..47b564d96a 100644 --- a/tests/specs/erc20/ds/approve-failure-spec.k +++ b/tests/specs/erc20/ds/approve-failure-spec.k @@ -40,6 +40,9 @@ module APPROVE-FAILURE-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/approve-success-spec.k b/tests/specs/erc20/ds/approve-success-spec.k index 63fdb3f980..d9e8cfde05 100644 --- a/tests/specs/erc20/ds/approve-success-spec.k +++ b/tests/specs/erc20/ds/approve-success-spec.k @@ -40,6 +40,9 @@ module APPROVE-SUCCESS-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/balanceOf-spec.k b/tests/specs/erc20/ds/balanceOf-spec.k index 5c4abb4afe..2064dd0742 100644 --- a/tests/specs/erc20/ds/balanceOf-spec.k +++ b/tests/specs/erc20/ds/balanceOf-spec.k @@ -40,6 +40,9 @@ module BALANCEOF-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/totalSupply-spec.k b/tests/specs/erc20/ds/totalSupply-spec.k index e3c49138c0..8f12953dc4 100644 --- a/tests/specs/erc20/ds/totalSupply-spec.k +++ b/tests/specs/erc20/ds/totalSupply-spec.k @@ -40,6 +40,9 @@ module TOTALSUPPLY-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transfer-failure-1-a-spec.k b/tests/specs/erc20/ds/transfer-failure-1-a-spec.k index cb779e9ad6..0c9546b56a 100644 --- a/tests/specs/erc20/ds/transfer-failure-1-a-spec.k +++ b/tests/specs/erc20/ds/transfer-failure-1-a-spec.k @@ -40,6 +40,9 @@ module TRANSFER-FAILURE-1-A-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transfer-failure-1-b-spec.k b/tests/specs/erc20/ds/transfer-failure-1-b-spec.k index 501d69497a..46fb525d94 100644 --- a/tests/specs/erc20/ds/transfer-failure-1-b-spec.k +++ b/tests/specs/erc20/ds/transfer-failure-1-b-spec.k @@ -40,6 +40,9 @@ module TRANSFER-FAILURE-1-B-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transfer-failure-1-c-spec.k b/tests/specs/erc20/ds/transfer-failure-1-c-spec.k index 43077065cd..9adfff2d5d 100644 --- a/tests/specs/erc20/ds/transfer-failure-1-c-spec.k +++ b/tests/specs/erc20/ds/transfer-failure-1-c-spec.k @@ -40,6 +40,9 @@ module TRANSFER-FAILURE-1-C-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transfer-failure-2-a-spec.k b/tests/specs/erc20/ds/transfer-failure-2-a-spec.k index e5c437ab17..1216a3d79b 100644 --- a/tests/specs/erc20/ds/transfer-failure-2-a-spec.k +++ b/tests/specs/erc20/ds/transfer-failure-2-a-spec.k @@ -40,6 +40,9 @@ module TRANSFER-FAILURE-2-A-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transfer-failure-2-b-spec.k b/tests/specs/erc20/ds/transfer-failure-2-b-spec.k index 1cc4e2c018..64020f4276 100644 --- a/tests/specs/erc20/ds/transfer-failure-2-b-spec.k +++ b/tests/specs/erc20/ds/transfer-failure-2-b-spec.k @@ -40,6 +40,9 @@ module TRANSFER-FAILURE-2-B-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transfer-success-1-spec.k b/tests/specs/erc20/ds/transfer-success-1-spec.k index af4749cc45..86ec71f2be 100644 --- a/tests/specs/erc20/ds/transfer-success-1-spec.k +++ b/tests/specs/erc20/ds/transfer-success-1-spec.k @@ -40,6 +40,9 @@ module TRANSFER-SUCCESS-1-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transfer-success-2-spec.k b/tests/specs/erc20/ds/transfer-success-2-spec.k index cc6f7b788b..f2bdf76b6c 100644 --- a/tests/specs/erc20/ds/transfer-success-2-spec.k +++ b/tests/specs/erc20/ds/transfer-success-2-spec.k @@ -40,6 +40,9 @@ module TRANSFER-SUCCESS-2-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transferFrom-failure-1-a-spec.k b/tests/specs/erc20/ds/transferFrom-failure-1-a-spec.k index 0a2d99c25b..6a0899dd7a 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-1-a-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-1-a-spec.k @@ -40,6 +40,9 @@ module TRANSFERFROM-FAILURE-1-A-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transferFrom-failure-1-b-spec.k b/tests/specs/erc20/ds/transferFrom-failure-1-b-spec.k index 346efa5a32..49b711cf0e 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-1-b-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-1-b-spec.k @@ -40,6 +40,9 @@ module TRANSFERFROM-FAILURE-1-B-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transferFrom-failure-1-c-spec.k b/tests/specs/erc20/ds/transferFrom-failure-1-c-spec.k index b437141204..b867c02411 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-1-c-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-1-c-spec.k @@ -40,6 +40,9 @@ module TRANSFERFROM-FAILURE-1-C-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transferFrom-failure-1-d-spec.k b/tests/specs/erc20/ds/transferFrom-failure-1-d-spec.k index ec06fc50a3..f4760ac9ca 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-1-d-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-1-d-spec.k @@ -40,6 +40,9 @@ module TRANSFERFROM-FAILURE-1-D-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transferFrom-failure-2-a-spec.k b/tests/specs/erc20/ds/transferFrom-failure-2-a-spec.k index c6189f9b2d..4f086e3a95 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-2-a-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-2-a-spec.k @@ -40,6 +40,9 @@ module TRANSFERFROM-FAILURE-2-A-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transferFrom-failure-2-b-spec.k b/tests/specs/erc20/ds/transferFrom-failure-2-b-spec.k index 3fb413664a..74c140d44f 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-2-b-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-2-b-spec.k @@ -40,6 +40,9 @@ module TRANSFERFROM-FAILURE-2-B-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transferFrom-failure-2-c-spec.k b/tests/specs/erc20/ds/transferFrom-failure-2-c-spec.k index 5c9b85dc25..cfd883d3cf 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-2-c-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-2-c-spec.k @@ -40,6 +40,9 @@ module TRANSFERFROM-FAILURE-2-C-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transferFrom-success-1-spec.k b/tests/specs/erc20/ds/transferFrom-success-1-spec.k index ff4a14e3ea..e833fd3a84 100644 --- a/tests/specs/erc20/ds/transferFrom-success-1-spec.k +++ b/tests/specs/erc20/ds/transferFrom-success-1-spec.k @@ -40,6 +40,9 @@ module TRANSFERFROM-SUCCESS-1-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/ds/transferFrom-success-2-spec.k b/tests/specs/erc20/ds/transferFrom-success-2-spec.k index e178d80b53..7e088b83b9 100644 --- a/tests/specs/erc20/ds/transferFrom-success-2-spec.k +++ b/tests/specs/erc20/ds/transferFrom-success-2-spec.k @@ -40,6 +40,9 @@ module TRANSFERFROM-SUCCESS-2-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/hkg/allowance-spec.k b/tests/specs/erc20/hkg/allowance-spec.k index b8708739e4..3ce92d88a5 100644 --- a/tests/specs/erc20/hkg/allowance-spec.k +++ b/tests/specs/erc20/hkg/allowance-spec.k @@ -40,6 +40,9 @@ module ALLOWANCE-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/hkg/approve-spec.k b/tests/specs/erc20/hkg/approve-spec.k index 802b17e826..bbf0ff6c8e 100644 --- a/tests/specs/erc20/hkg/approve-spec.k +++ b/tests/specs/erc20/hkg/approve-spec.k @@ -40,6 +40,9 @@ module APPROVE-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/hkg/balanceOf-spec.k b/tests/specs/erc20/hkg/balanceOf-spec.k index 5d88158f4d..9c1b85fd9b 100644 --- a/tests/specs/erc20/hkg/balanceOf-spec.k +++ b/tests/specs/erc20/hkg/balanceOf-spec.k @@ -40,6 +40,9 @@ module BALANCEOF-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/hkg/totalSupply-spec.k b/tests/specs/erc20/hkg/totalSupply-spec.k index 7ed76733c0..738db057e6 100644 --- a/tests/specs/erc20/hkg/totalSupply-spec.k +++ b/tests/specs/erc20/hkg/totalSupply-spec.k @@ -40,6 +40,9 @@ module TOTALSUPPLY-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/hkg/transfer-failure-1-spec.k b/tests/specs/erc20/hkg/transfer-failure-1-spec.k index 893d364c9f..0ce32fd72f 100644 --- a/tests/specs/erc20/hkg/transfer-failure-1-spec.k +++ b/tests/specs/erc20/hkg/transfer-failure-1-spec.k @@ -40,6 +40,9 @@ module TRANSFER-FAILURE-1-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/hkg/transfer-failure-2-spec.k b/tests/specs/erc20/hkg/transfer-failure-2-spec.k index 7251a253d8..2d7e13d299 100644 --- a/tests/specs/erc20/hkg/transfer-failure-2-spec.k +++ b/tests/specs/erc20/hkg/transfer-failure-2-spec.k @@ -40,6 +40,9 @@ module TRANSFER-FAILURE-2-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/hkg/transfer-success-1-spec.k b/tests/specs/erc20/hkg/transfer-success-1-spec.k index 5184bfda6c..1a7e448d7d 100644 --- a/tests/specs/erc20/hkg/transfer-success-1-spec.k +++ b/tests/specs/erc20/hkg/transfer-success-1-spec.k @@ -40,6 +40,9 @@ module TRANSFER-SUCCESS-1-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/hkg/transfer-success-2-spec.k b/tests/specs/erc20/hkg/transfer-success-2-spec.k index e5d1e033e7..d2489e3e7c 100644 --- a/tests/specs/erc20/hkg/transfer-success-2-spec.k +++ b/tests/specs/erc20/hkg/transfer-success-2-spec.k @@ -40,6 +40,9 @@ module TRANSFER-SUCCESS-2-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/hkg/transferFrom-failure-1-spec.k b/tests/specs/erc20/hkg/transferFrom-failure-1-spec.k index a955344dcb..653d3cddbe 100644 --- a/tests/specs/erc20/hkg/transferFrom-failure-1-spec.k +++ b/tests/specs/erc20/hkg/transferFrom-failure-1-spec.k @@ -40,6 +40,9 @@ module TRANSFERFROM-FAILURE-1-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/hkg/transferFrom-failure-2-spec.k b/tests/specs/erc20/hkg/transferFrom-failure-2-spec.k index 6878d1b7c1..4481e930a8 100644 --- a/tests/specs/erc20/hkg/transferFrom-failure-2-spec.k +++ b/tests/specs/erc20/hkg/transferFrom-failure-2-spec.k @@ -40,6 +40,9 @@ module TRANSFERFROM-FAILURE-2-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/hkg/transferFrom-success-1-spec.k b/tests/specs/erc20/hkg/transferFrom-success-1-spec.k index 0ab15fddd0..38b47237bf 100644 --- a/tests/specs/erc20/hkg/transferFrom-success-1-spec.k +++ b/tests/specs/erc20/hkg/transferFrom-success-1-spec.k @@ -40,6 +40,9 @@ module TRANSFERFROM-SUCCESS-1-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/erc20/hkg/transferFrom-success-2-spec.k b/tests/specs/erc20/hkg/transferFrom-success-2-spec.k index e5750bd489..84970cacb5 100644 --- a/tests/specs/erc20/hkg/transferFrom-success-2-spec.k +++ b/tests/specs/erc20/hkg/transferFrom-success-2-spec.k @@ -40,6 +40,9 @@ module TRANSFERFROM-SUCCESS-2-SPEC false // NOTE: non-static call CALL_DEPTH + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k index 794199169c..6d4ee9c489 100644 --- a/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k +++ b/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k @@ -194,6 +194,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k index 324dd99803..250c8f747b 100644 --- a/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k +++ b/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k @@ -194,6 +194,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW_FAIL-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k index eb45dab25f..bf4f56883c 100644 --- a/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k +++ b/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k @@ -194,6 +194,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCALLSTOADDRESS-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k index f3e70f6c94..90e7abae84 100644 --- a/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k +++ b/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k @@ -194,6 +194,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -571,6 +574,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC 1 + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-arithmetictest-test_max1_broken-uint256-uint256-0-spec.k b/tests/specs/kontrol/test-arithmetictest-test_max1_broken-uint256-uint256-0-spec.k index a87b5bce51..7f36ddafdb 100644 --- a/tests/specs/kontrol/test-arithmetictest-test_max1_broken-uint256-uint256-0-spec.k +++ b/tests/specs/kontrol/test-arithmetictest-test_max1_broken-uint256-uint256-0-spec.k @@ -77,6 +77,9 @@ module TEST-ARITHMETICTEST-TEST_MAX1_BROKEN-UINT256-UINT256-0-SPEC 0 + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-countertest-testincrement-0-spec.k b/tests/specs/kontrol/test-countertest-testincrement-0-spec.k index e61cd9ecc8..400b46cb47 100644 --- a/tests/specs/kontrol/test-countertest-testincrement-0-spec.k +++ b/tests/specs/kontrol/test-countertest-testincrement-0-spec.k @@ -194,6 +194,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -554,6 +557,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC ( 1 => 0 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -891,6 +897,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-emitcontracttest-testexpectemit-0-spec.k b/tests/specs/kontrol/test-emitcontracttest-testexpectemit-0-spec.k index 9b7f455601..d81009567e 100644 --- a/tests/specs/kontrol/test-emitcontracttest-testexpectemit-0-spec.k +++ b/tests/specs/kontrol/test-emitcontracttest-testexpectemit-0-spec.k @@ -194,6 +194,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMIT-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k b/tests/specs/kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k index 682719f3b3..e55cbe9214 100644 --- a/tests/specs/kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k +++ b/tests/specs/kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k @@ -194,6 +194,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITCHECKEMITTER-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k b/tests/specs/kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k index 73e466655a..0afb861e3e 100644 --- a/tests/specs/kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k +++ b/tests/specs/kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k @@ -194,6 +194,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITDONOTCHECKDATA-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-expectcalltest-testexpectregularcall-0-spec.k b/tests/specs/kontrol/test-expectcalltest-testexpectregularcall-0-spec.k index b3d851e49d..6090505ee4 100644 --- a/tests/specs/kontrol/test-expectcalltest-testexpectregularcall-0-spec.k +++ b/tests/specs/kontrol/test-expectcalltest-testexpectregularcall-0-spec.k @@ -194,6 +194,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTREGULARCALL-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-expectcalltest-testexpectstaticcall-0-spec.k b/tests/specs/kontrol/test-expectcalltest-testexpectstaticcall-0-spec.k index 312105d380..94b1ad3365 100644 --- a/tests/specs/kontrol/test-expectcalltest-testexpectstaticcall-0-spec.k +++ b/tests/specs/kontrol/test-expectcalltest-testexpectstaticcall-0-spec.k @@ -194,6 +194,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTSTATICCALL-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k index b9f6665522..29ef4e650d 100644 --- a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k +++ b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k @@ -194,6 +194,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -526,6 +529,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC ( 1 => 0 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k index 3a5d7d58cf..e240315ae3 100644 --- a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k +++ b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k @@ -194,6 +194,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_MESSAGE-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k index 9092e46bf1..709150eb5a 100644 --- a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k +++ b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k @@ -194,6 +194,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_RETURNVALUE-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k index e044b6cfc4..19479003b5 100644 --- a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k +++ b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k @@ -194,6 +194,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_BYTES4-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k index c098a4cf2b..9942b43545 100644 --- a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k +++ b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k @@ -194,6 +194,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FAILANDSUCCESS-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k index b078c1324c..f730bc73fe 100644 --- a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k +++ b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k @@ -194,6 +194,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -412,6 +415,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC 0 + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k b/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k index da35c8b4fb..039b5c5261 100644 --- a/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k +++ b/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k @@ -194,6 +194,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -552,6 +555,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k b/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k index df84b79631..816a0dcc46 100644 --- a/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k +++ b/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k @@ -192,6 +192,9 @@ module TEST-SAFETEST-TESTWITHDRAWFUZZ-UINT96-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-storetest-testaccesses-0-spec.k b/tests/specs/kontrol/test-storetest-testaccesses-0-spec.k index 2feb990e5f..8182f858d2 100644 --- a/tests/specs/kontrol/test-storetest-testaccesses-0-spec.k +++ b/tests/specs/kontrol/test-storetest-testaccesses-0-spec.k @@ -194,6 +194,9 @@ module TEST-STORETEST-TESTACCESSES-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/kontrol/test-storetest-teststoreload-0-spec.k b/tests/specs/kontrol/test-storetest-teststoreload-0-spec.k index 9d88bf0cc8..4cc0aad1b2 100644 --- a/tests/specs/kontrol/test-storetest-teststoreload-0-spec.k +++ b/tests/specs/kontrol/test-storetest-teststoreload-0-spec.k @@ -194,6 +194,9 @@ module TEST-STORETEST-TESTSTORELOAD-0-SPEC ( 0 => 1 ) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/cat-exhaustiveness-spec.k b/tests/specs/mcd-structured/cat-exhaustiveness-spec.k index c28103faef..b334c957c0 100644 --- a/tests/specs/mcd-structured/cat-exhaustiveness-spec.k +++ b/tests/specs/mcd-structured/cat-exhaustiveness-spec.k @@ -32,6 +32,9 @@ module CAT-EXHAUSTIVENESS-SPEC _ => ?_ _VStatic VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/cat-file-addr-pass-rough-spec.k b/tests/specs/mcd-structured/cat-file-addr-pass-rough-spec.k index fabd449c83..b1da2fb969 100644 --- a/tests/specs/mcd-structured/cat-file-addr-pass-rough-spec.k +++ b/tests/specs/mcd-structured/cat-file-addr-pass-rough-spec.k @@ -32,6 +32,9 @@ module CAT-FILE-ADDR-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/dai-adduu-fail-rough-spec.k b/tests/specs/mcd-structured/dai-adduu-fail-rough-spec.k index 42298fa35c..20225970ac 100644 --- a/tests/specs/mcd-structured/dai-adduu-fail-rough-spec.k +++ b/tests/specs/mcd-structured/dai-adduu-fail-rough-spec.k @@ -32,6 +32,9 @@ module DAI-ADDUU-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/dai-symbol-pass-spec.k b/tests/specs/mcd-structured/dai-symbol-pass-spec.k index 020c1ced65..a3642e772f 100644 --- a/tests/specs/mcd-structured/dai-symbol-pass-spec.k +++ b/tests/specs/mcd-structured/dai-symbol-pass-spec.k @@ -32,6 +32,9 @@ module DAI-SYMBOL-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/dstoken-approve-fail-rough-spec.k b/tests/specs/mcd-structured/dstoken-approve-fail-rough-spec.k index ddbdcb5ff1..49e58911e5 100644 --- a/tests/specs/mcd-structured/dstoken-approve-fail-rough-spec.k +++ b/tests/specs/mcd-structured/dstoken-approve-fail-rough-spec.k @@ -32,6 +32,9 @@ module DSTOKEN-APPROVE-FAIL-ROUGH-SPEC _ => ?_ false VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/dsvalue-peek-pass-rough-spec.k b/tests/specs/mcd-structured/dsvalue-peek-pass-rough-spec.k index c9f243f115..7477926e99 100644 --- a/tests/specs/mcd-structured/dsvalue-peek-pass-rough-spec.k +++ b/tests/specs/mcd-structured/dsvalue-peek-pass-rough-spec.k @@ -32,6 +32,9 @@ module DSVALUE-PEEK-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/dsvalue-read-pass-spec.k b/tests/specs/mcd-structured/dsvalue-read-pass-spec.k index 60364af2b7..5215b6696c 100644 --- a/tests/specs/mcd-structured/dsvalue-read-pass-spec.k +++ b/tests/specs/mcd-structured/dsvalue-read-pass-spec.k @@ -32,6 +32,9 @@ module DSVALUE-READ-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/dsvalue-read-pass-summarize-spec.k b/tests/specs/mcd-structured/dsvalue-read-pass-summarize-spec.k index 00717307fb..0e1812fd4c 100644 --- a/tests/specs/mcd-structured/dsvalue-read-pass-summarize-spec.k +++ b/tests/specs/mcd-structured/dsvalue-read-pass-summarize-spec.k @@ -132,6 +132,9 @@ module DSVALUE-READ-PASS-SUMMARIZE-SPEC .Bytes => ?_ 0 => ?_ (_ => ?_) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ (_ => ?_) diff --git a/tests/specs/mcd-structured/end-cash-pass-rough-spec.k b/tests/specs/mcd-structured/end-cash-pass-rough-spec.k index 579625a314..10389c776f 100644 --- a/tests/specs/mcd-structured/end-cash-pass-rough-spec.k +++ b/tests/specs/mcd-structured/end-cash-pass-rough-spec.k @@ -32,6 +32,9 @@ module END-CASH-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -181,6 +184,9 @@ module END-CASH-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -291,6 +297,9 @@ module END-CASH-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -398,6 +407,9 @@ module END-CASH-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/end-pack-pass-rough-spec.k b/tests/specs/mcd-structured/end-pack-pass-rough-spec.k index 2ba7aa5fd9..35adeb324d 100644 --- a/tests/specs/mcd-structured/end-pack-pass-rough-spec.k +++ b/tests/specs/mcd-structured/end-pack-pass-rough-spec.k @@ -32,6 +32,9 @@ module END-PACK-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -189,6 +192,9 @@ module END-PACK-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -296,6 +302,9 @@ module END-PACK-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -403,6 +412,9 @@ module END-PACK-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/end-subuu-pass-spec.k b/tests/specs/mcd-structured/end-subuu-pass-spec.k index f29aed8b27..639c54307a 100644 --- a/tests/specs/mcd-structured/end-subuu-pass-spec.k +++ b/tests/specs/mcd-structured/end-subuu-pass-spec.k @@ -32,6 +32,9 @@ module END-SUBUU-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.k b/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.k index 6da86c3e06..f43017961f 100644 --- a/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.k +++ b/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.k @@ -32,6 +32,9 @@ module FLAPPER-YANK-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -199,6 +202,9 @@ module FLAPPER-YANK-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/flipper-addu48u48-fail-rough-spec.k b/tests/specs/mcd-structured/flipper-addu48u48-fail-rough-spec.k index f181dbf0ad..d6fedc8baa 100644 --- a/tests/specs/mcd-structured/flipper-addu48u48-fail-rough-spec.k +++ b/tests/specs/mcd-structured/flipper-addu48u48-fail-rough-spec.k @@ -32,6 +32,9 @@ module FLIPPER-ADDU48U48-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/flipper-bids-pass-rough-spec.k b/tests/specs/mcd-structured/flipper-bids-pass-rough-spec.k index 56b6b5bf66..896041b18d 100644 --- a/tests/specs/mcd-structured/flipper-bids-pass-rough-spec.k +++ b/tests/specs/mcd-structured/flipper-bids-pass-rough-spec.k @@ -32,6 +32,9 @@ module FLIPPER-BIDS-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/flipper-tau-pass-spec.k b/tests/specs/mcd-structured/flipper-tau-pass-spec.k index aeb06bb095..b2ffbd1afe 100644 --- a/tests/specs/mcd-structured/flipper-tau-pass-spec.k +++ b/tests/specs/mcd-structured/flipper-tau-pass-spec.k @@ -32,6 +32,9 @@ module FLIPPER-TAU-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/flipper-ttl-pass-spec.k b/tests/specs/mcd-structured/flipper-ttl-pass-spec.k index 7a2b968993..21cce7562b 100644 --- a/tests/specs/mcd-structured/flipper-ttl-pass-spec.k +++ b/tests/specs/mcd-structured/flipper-ttl-pass-spec.k @@ -32,6 +32,9 @@ module FLIPPER-TTL-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/flopper-cage-pass-spec.k b/tests/specs/mcd-structured/flopper-cage-pass-spec.k index c39551648b..23fe3d1f73 100644 --- a/tests/specs/mcd-structured/flopper-cage-pass-spec.k +++ b/tests/specs/mcd-structured/flopper-cage-pass-spec.k @@ -31,6 +31,9 @@ module FLOPPER-CAGE-PASS-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k b/tests/specs/mcd-structured/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k index aaf0ec13f8..3e322c2bf5 100644 --- a/tests/specs/mcd-structured/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k +++ b/tests/specs/mcd-structured/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k @@ -32,6 +32,9 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -211,6 +214,9 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -318,6 +324,9 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -425,6 +434,9 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/flopper-dent-guy-same-pass-rough-spec.k b/tests/specs/mcd-structured/flopper-dent-guy-same-pass-rough-spec.k index 349b8d50d6..236c9043c5 100644 --- a/tests/specs/mcd-structured/flopper-dent-guy-same-pass-rough-spec.k +++ b/tests/specs/mcd-structured/flopper-dent-guy-same-pass-rough-spec.k @@ -32,6 +32,9 @@ module FLOPPER-DENT-GUY-SAME-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -180,6 +183,9 @@ module FLOPPER-DENT-GUY-SAME-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -286,6 +292,9 @@ module FLOPPER-DENT-GUY-SAME-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/flopper-kick-pass-rough-spec.k b/tests/specs/mcd-structured/flopper-kick-pass-rough-spec.k index 9105a8647a..ac90ef293f 100644 --- a/tests/specs/mcd-structured/flopper-kick-pass-rough-spec.k +++ b/tests/specs/mcd-structured/flopper-kick-pass-rough-spec.k @@ -32,6 +32,9 @@ module FLOPPER-KICK-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -169,6 +172,9 @@ module FLOPPER-KICK-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/flopper-tick-pass-rough-spec.k b/tests/specs/mcd-structured/flopper-tick-pass-rough-spec.k index 3152e05385..1deb482180 100644 --- a/tests/specs/mcd-structured/flopper-tick-pass-rough-spec.k +++ b/tests/specs/mcd-structured/flopper-tick-pass-rough-spec.k @@ -32,6 +32,9 @@ module FLOPPER-TICK-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -158,6 +161,9 @@ module FLOPPER-TICK-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/pot-join-pass-rough-spec.k b/tests/specs/mcd-structured/pot-join-pass-rough-spec.k index cf80c35d31..345cc2eaac 100644 --- a/tests/specs/mcd-structured/pot-join-pass-rough-spec.k +++ b/tests/specs/mcd-structured/pot-join-pass-rough-spec.k @@ -32,6 +32,9 @@ module POT-JOIN-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -188,6 +191,9 @@ module POT-JOIN-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -298,6 +304,9 @@ module POT-JOIN-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -405,6 +414,9 @@ module POT-JOIN-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-addui-fail-rough-spec.k b/tests/specs/mcd-structured/vat-addui-fail-rough-spec.k index 3ef2b5aa31..948b9c2ee5 100644 --- a/tests/specs/mcd-structured/vat-addui-fail-rough-spec.k +++ b/tests/specs/mcd-structured/vat-addui-fail-rough-spec.k @@ -32,6 +32,9 @@ module VAT-ADDUI-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-arithmetic-spec.k b/tests/specs/mcd-structured/vat-arithmetic-spec.k index 03169c1628..f1a94ee2ac 100644 --- a/tests/specs/mcd-structured/vat-arithmetic-spec.k +++ b/tests/specs/mcd-structured/vat-arithmetic-spec.k @@ -31,6 +31,9 @@ module VAT-ARITHMETIC-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -136,6 +139,9 @@ module VAT-ARITHMETIC-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -235,6 +241,9 @@ module VAT-ARITHMETIC-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -340,6 +349,9 @@ module VAT-ARITHMETIC-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -442,6 +454,9 @@ module VAT-ARITHMETIC-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -544,6 +559,9 @@ module VAT-ARITHMETIC-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-dai-pass-spec.k b/tests/specs/mcd-structured/vat-dai-pass-spec.k index a5bbad4abf..e8b8fc5b81 100644 --- a/tests/specs/mcd-structured/vat-dai-pass-spec.k +++ b/tests/specs/mcd-structured/vat-dai-pass-spec.k @@ -31,6 +31,9 @@ module VAT-DAI-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-deny-diff-fail-rough-spec.k b/tests/specs/mcd-structured/vat-deny-diff-fail-rough-spec.k index 852150239b..5ce8ca79e5 100644 --- a/tests/specs/mcd-structured/vat-deny-diff-fail-rough-spec.k +++ b/tests/specs/mcd-structured/vat-deny-diff-fail-rough-spec.k @@ -32,6 +32,9 @@ module VAT-DENY-DIFF-FAIL-ROUGH-SPEC _ => ?_ false VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-flux-diff-pass-rough-spec.k b/tests/specs/mcd-structured/vat-flux-diff-pass-rough-spec.k index 4a770857b1..912409e88f 100644 --- a/tests/specs/mcd-structured/vat-flux-diff-pass-rough-spec.k +++ b/tests/specs/mcd-structured/vat-flux-diff-pass-rough-spec.k @@ -33,6 +33,9 @@ module VAT-FLUX-DIFF-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-flux-diff-pass-spec.k b/tests/specs/mcd-structured/vat-flux-diff-pass-spec.k index 62a07b6a57..085fe14e6b 100644 --- a/tests/specs/mcd-structured/vat-flux-diff-pass-spec.k +++ b/tests/specs/mcd-structured/vat-flux-diff-pass-spec.k @@ -31,6 +31,9 @@ module VAT-FLUX-DIFF-PASS-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-fold-pass-rough-spec.k b/tests/specs/mcd-structured/vat-fold-pass-rough-spec.k index 9e7b991b37..8aa16dbe5b 100644 --- a/tests/specs/mcd-structured/vat-fold-pass-rough-spec.k +++ b/tests/specs/mcd-structured/vat-fold-pass-rough-spec.k @@ -34,6 +34,9 @@ module VAT-FOLD-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-fork-diff-pass-rough-spec.k b/tests/specs/mcd-structured/vat-fork-diff-pass-rough-spec.k index 74ce126fb2..667e0f9f08 100644 --- a/tests/specs/mcd-structured/vat-fork-diff-pass-rough-spec.k +++ b/tests/specs/mcd-structured/vat-fork-diff-pass-rough-spec.k @@ -34,6 +34,9 @@ module VAT-FORK-DIFF-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-frob-diff-zero-dart-pass-rough-spec.k b/tests/specs/mcd-structured/vat-frob-diff-zero-dart-pass-rough-spec.k index 7e9ed0d030..ed33a69e36 100644 --- a/tests/specs/mcd-structured/vat-frob-diff-zero-dart-pass-rough-spec.k +++ b/tests/specs/mcd-structured/vat-frob-diff-zero-dart-pass-rough-spec.k @@ -34,6 +34,9 @@ module VAT-FROB-DIFF-ZERO-DART-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-heal-pass-spec.k b/tests/specs/mcd-structured/vat-heal-pass-spec.k index 10bbae717c..c1b6e61c45 100644 --- a/tests/specs/mcd-structured/vat-heal-pass-spec.k +++ b/tests/specs/mcd-structured/vat-heal-pass-spec.k @@ -31,6 +31,9 @@ module VAT-HEAL-PASS-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-move-diff-rough-spec.k b/tests/specs/mcd-structured/vat-move-diff-rough-spec.k index a20da419e0..ab75ecbf74 100644 --- a/tests/specs/mcd-structured/vat-move-diff-rough-spec.k +++ b/tests/specs/mcd-structured/vat-move-diff-rough-spec.k @@ -35,6 +35,9 @@ module VAT-MOVE-DIFF-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-sin-pass-spec.k b/tests/specs/mcd-structured/vat-sin-pass-spec.k index fcf4d9d609..90b56f7f35 100644 --- a/tests/specs/mcd-structured/vat-sin-pass-spec.k +++ b/tests/specs/mcd-structured/vat-sin-pass-spec.k @@ -31,6 +31,9 @@ module VAT-SIN-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-slip-pass-rough-spec.k b/tests/specs/mcd-structured/vat-slip-pass-rough-spec.k index e3e1086c92..9bc817be12 100644 --- a/tests/specs/mcd-structured/vat-slip-pass-rough-spec.k +++ b/tests/specs/mcd-structured/vat-slip-pass-rough-spec.k @@ -34,6 +34,9 @@ module VAT-SLIP-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vat-subui-fail-rough-spec.k b/tests/specs/mcd-structured/vat-subui-fail-rough-spec.k index f939bac495..a200ab007f 100644 --- a/tests/specs/mcd-structured/vat-subui-fail-rough-spec.k +++ b/tests/specs/mcd-structured/vat-subui-fail-rough-spec.k @@ -32,6 +32,9 @@ module VAT-SUBUI-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vow-fess-fail-rough-spec.k b/tests/specs/mcd-structured/vow-fess-fail-rough-spec.k index d42da544b9..cd1c2d26f5 100644 --- a/tests/specs/mcd-structured/vow-fess-fail-rough-spec.k +++ b/tests/specs/mcd-structured/vow-fess-fail-rough-spec.k @@ -32,6 +32,9 @@ module VOW-FESS-FAIL-ROUGH-SPEC _ => ?_ false VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -158,6 +161,9 @@ module VOW-FESS-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd-structured/vow-flog-fail-rough-spec.k b/tests/specs/mcd-structured/vow-flog-fail-rough-spec.k index be103aade8..c8ee9dc1c2 100644 --- a/tests/specs/mcd-structured/vow-flog-fail-rough-spec.k +++ b/tests/specs/mcd-structured/vow-flog-fail-rough-spec.k @@ -32,6 +32,9 @@ module VOW-FLOG-FAIL-ROUGH-SPEC _ => ?_ false VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -151,6 +154,9 @@ module VOW-FLOG-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -258,6 +264,9 @@ module VOW-FLOG-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/cat-exhaustiveness-spec.k b/tests/specs/mcd/cat-exhaustiveness-spec.k index fbfea5912b..b5049d64dc 100644 --- a/tests/specs/mcd/cat-exhaustiveness-spec.k +++ b/tests/specs/mcd/cat-exhaustiveness-spec.k @@ -32,6 +32,9 @@ module CAT-EXHAUSTIVENESS-SPEC _ => ?_ _VStatic VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/cat-file-addr-pass-rough-spec.k b/tests/specs/mcd/cat-file-addr-pass-rough-spec.k index 79b9fc6320..d14fd157d5 100644 --- a/tests/specs/mcd/cat-file-addr-pass-rough-spec.k +++ b/tests/specs/mcd/cat-file-addr-pass-rough-spec.k @@ -32,6 +32,9 @@ module CAT-FILE-ADDR-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/dai-adduu-fail-rough-spec.k b/tests/specs/mcd/dai-adduu-fail-rough-spec.k index 915ec716aa..62757f4b29 100644 --- a/tests/specs/mcd/dai-adduu-fail-rough-spec.k +++ b/tests/specs/mcd/dai-adduu-fail-rough-spec.k @@ -32,6 +32,9 @@ module DAI-ADDUU-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/dai-symbol-pass-spec.k b/tests/specs/mcd/dai-symbol-pass-spec.k index 664fbf93f4..2610437400 100644 --- a/tests/specs/mcd/dai-symbol-pass-spec.k +++ b/tests/specs/mcd/dai-symbol-pass-spec.k @@ -32,6 +32,9 @@ module DAI-SYMBOL-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/dstoken-approve-fail-rough-spec.k b/tests/specs/mcd/dstoken-approve-fail-rough-spec.k index cbcf6f072d..e697190f28 100644 --- a/tests/specs/mcd/dstoken-approve-fail-rough-spec.k +++ b/tests/specs/mcd/dstoken-approve-fail-rough-spec.k @@ -32,6 +32,9 @@ module DSTOKEN-APPROVE-FAIL-ROUGH-SPEC _ => ?_ false VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/dsvalue-peek-pass-rough-spec.k b/tests/specs/mcd/dsvalue-peek-pass-rough-spec.k index d005c3249b..62d830df14 100644 --- a/tests/specs/mcd/dsvalue-peek-pass-rough-spec.k +++ b/tests/specs/mcd/dsvalue-peek-pass-rough-spec.k @@ -32,6 +32,9 @@ module DSVALUE-PEEK-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/dsvalue-read-pass-spec.k b/tests/specs/mcd/dsvalue-read-pass-spec.k index 8bea6fc528..5a77a094dc 100644 --- a/tests/specs/mcd/dsvalue-read-pass-spec.k +++ b/tests/specs/mcd/dsvalue-read-pass-spec.k @@ -32,6 +32,9 @@ module DSVALUE-READ-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/dsvalue-read-pass-summarize-spec.k b/tests/specs/mcd/dsvalue-read-pass-summarize-spec.k index cfce1c6461..455f591bce 100644 --- a/tests/specs/mcd/dsvalue-read-pass-summarize-spec.k +++ b/tests/specs/mcd/dsvalue-read-pass-summarize-spec.k @@ -132,6 +132,9 @@ module DSVALUE-READ-PASS-SUMMARIZE-SPEC .Bytes => ?_ 0 => ?_ (_ => ?_) + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ (_ => ?_) diff --git a/tests/specs/mcd/end-cash-pass-rough-spec.k b/tests/specs/mcd/end-cash-pass-rough-spec.k index b75f0b164d..8c7fd0cb2b 100644 --- a/tests/specs/mcd/end-cash-pass-rough-spec.k +++ b/tests/specs/mcd/end-cash-pass-rough-spec.k @@ -32,6 +32,9 @@ module END-CASH-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -195,6 +198,9 @@ module END-CASH-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -307,6 +313,9 @@ module END-CASH-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -416,6 +425,9 @@ module END-CASH-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/end-pack-pass-rough-spec.k b/tests/specs/mcd/end-pack-pass-rough-spec.k index ab96dfc615..4a1052e9f9 100644 --- a/tests/specs/mcd/end-pack-pass-rough-spec.k +++ b/tests/specs/mcd/end-pack-pass-rough-spec.k @@ -32,6 +32,9 @@ module END-PACK-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -200,6 +203,9 @@ module END-PACK-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -309,6 +315,9 @@ module END-PACK-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -418,6 +427,9 @@ module END-PACK-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/end-subuu-pass-spec.k b/tests/specs/mcd/end-subuu-pass-spec.k index 2b58be3100..2041386ef2 100644 --- a/tests/specs/mcd/end-subuu-pass-spec.k +++ b/tests/specs/mcd/end-subuu-pass-spec.k @@ -32,6 +32,9 @@ module END-SUBUU-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/flapper-yank-pass-rough-spec.k b/tests/specs/mcd/flapper-yank-pass-rough-spec.k index fc72d0c070..c0e41dc21b 100644 --- a/tests/specs/mcd/flapper-yank-pass-rough-spec.k +++ b/tests/specs/mcd/flapper-yank-pass-rough-spec.k @@ -32,6 +32,9 @@ module FLAPPER-YANK-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -210,6 +213,9 @@ module FLAPPER-YANK-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k b/tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k index 08f38bf94d..f461749e4f 100644 --- a/tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k +++ b/tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k @@ -32,6 +32,9 @@ module FLIPPER-ADDU48U48-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/flipper-bids-pass-rough-spec.k b/tests/specs/mcd/flipper-bids-pass-rough-spec.k index d9e684e6c3..03446988c9 100644 --- a/tests/specs/mcd/flipper-bids-pass-rough-spec.k +++ b/tests/specs/mcd/flipper-bids-pass-rough-spec.k @@ -32,6 +32,9 @@ module FLIPPER-BIDS-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/flipper-tau-pass-spec.k b/tests/specs/mcd/flipper-tau-pass-spec.k index 49de5362a5..929f3c2d99 100644 --- a/tests/specs/mcd/flipper-tau-pass-spec.k +++ b/tests/specs/mcd/flipper-tau-pass-spec.k @@ -32,6 +32,9 @@ module FLIPPER-TAU-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/flipper-ttl-pass-spec.k b/tests/specs/mcd/flipper-ttl-pass-spec.k index 929e2b0983..81ec2dd117 100644 --- a/tests/specs/mcd/flipper-ttl-pass-spec.k +++ b/tests/specs/mcd/flipper-ttl-pass-spec.k @@ -32,6 +32,9 @@ module FLIPPER-TTL-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/flopper-cage-pass-spec.k b/tests/specs/mcd/flopper-cage-pass-spec.k index 657b39ad74..bdec88e7f4 100644 --- a/tests/specs/mcd/flopper-cage-pass-spec.k +++ b/tests/specs/mcd/flopper-cage-pass-spec.k @@ -31,6 +31,9 @@ module FLOPPER-CAGE-PASS-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k b/tests/specs/mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k index b9ee439151..4b847a48ef 100644 --- a/tests/specs/mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k +++ b/tests/specs/mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k @@ -32,6 +32,9 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -240,6 +243,9 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -349,6 +355,9 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -457,6 +466,9 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/flopper-dent-guy-same-pass-rough-spec.k b/tests/specs/mcd/flopper-dent-guy-same-pass-rough-spec.k index ba7cbec915..2f6dc6a6c9 100644 --- a/tests/specs/mcd/flopper-dent-guy-same-pass-rough-spec.k +++ b/tests/specs/mcd/flopper-dent-guy-same-pass-rough-spec.k @@ -32,6 +32,9 @@ module FLOPPER-DENT-GUY-SAME-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -206,6 +209,9 @@ module FLOPPER-DENT-GUY-SAME-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -314,6 +320,9 @@ module FLOPPER-DENT-GUY-SAME-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/flopper-kick-pass-rough-spec.k b/tests/specs/mcd/flopper-kick-pass-rough-spec.k index 23e12a3f71..2b533588f2 100644 --- a/tests/specs/mcd/flopper-kick-pass-rough-spec.k +++ b/tests/specs/mcd/flopper-kick-pass-rough-spec.k @@ -32,6 +32,9 @@ module FLOPPER-KICK-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -195,6 +198,9 @@ module FLOPPER-KICK-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/flopper-tick-pass-rough-spec.k b/tests/specs/mcd/flopper-tick-pass-rough-spec.k index d378731d10..6a5151eaf1 100644 --- a/tests/specs/mcd/flopper-tick-pass-rough-spec.k +++ b/tests/specs/mcd/flopper-tick-pass-rough-spec.k @@ -32,6 +32,9 @@ module FLOPPER-TICK-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -166,6 +169,9 @@ module FLOPPER-TICK-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/pot-join-pass-rough-spec.k b/tests/specs/mcd/pot-join-pass-rough-spec.k index 825c91860d..db5972dfe0 100644 --- a/tests/specs/mcd/pot-join-pass-rough-spec.k +++ b/tests/specs/mcd/pot-join-pass-rough-spec.k @@ -32,6 +32,9 @@ module POT-JOIN-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -204,6 +207,9 @@ module POT-JOIN-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -316,6 +322,9 @@ module POT-JOIN-PASS-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -425,6 +434,9 @@ module POT-JOIN-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-addui-fail-rough-spec.k b/tests/specs/mcd/vat-addui-fail-rough-spec.k index 2e4fcbdb4d..d011f393d4 100644 --- a/tests/specs/mcd/vat-addui-fail-rough-spec.k +++ b/tests/specs/mcd/vat-addui-fail-rough-spec.k @@ -32,6 +32,9 @@ module VAT-ADDUI-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-arithmetic-spec.k b/tests/specs/mcd/vat-arithmetic-spec.k index a5231bf555..ce1a706876 100644 --- a/tests/specs/mcd/vat-arithmetic-spec.k +++ b/tests/specs/mcd/vat-arithmetic-spec.k @@ -31,6 +31,9 @@ module VAT-ARITHMETIC-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -136,6 +139,9 @@ module VAT-ARITHMETIC-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -235,6 +241,9 @@ module VAT-ARITHMETIC-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -340,6 +349,9 @@ module VAT-ARITHMETIC-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -442,6 +454,9 @@ module VAT-ARITHMETIC-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -544,6 +559,9 @@ module VAT-ARITHMETIC-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-dai-pass-spec.k b/tests/specs/mcd/vat-dai-pass-spec.k index 898cef7596..d98955d931 100644 --- a/tests/specs/mcd/vat-dai-pass-spec.k +++ b/tests/specs/mcd/vat-dai-pass-spec.k @@ -31,6 +31,9 @@ module VAT-DAI-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-deny-diff-fail-rough-spec.k b/tests/specs/mcd/vat-deny-diff-fail-rough-spec.k index 7824f2669c..fc3ae903bc 100644 --- a/tests/specs/mcd/vat-deny-diff-fail-rough-spec.k +++ b/tests/specs/mcd/vat-deny-diff-fail-rough-spec.k @@ -32,6 +32,9 @@ module VAT-DENY-DIFF-FAIL-ROUGH-SPEC _ => ?_ false VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-flux-diff-pass-rough-spec.k b/tests/specs/mcd/vat-flux-diff-pass-rough-spec.k index 254a1298f5..3c048c1fd3 100644 --- a/tests/specs/mcd/vat-flux-diff-pass-rough-spec.k +++ b/tests/specs/mcd/vat-flux-diff-pass-rough-spec.k @@ -33,6 +33,9 @@ module VAT-FLUX-DIFF-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-flux-diff-pass-spec.k b/tests/specs/mcd/vat-flux-diff-pass-spec.k index c42a9c9189..1d3f81d284 100644 --- a/tests/specs/mcd/vat-flux-diff-pass-spec.k +++ b/tests/specs/mcd/vat-flux-diff-pass-spec.k @@ -31,6 +31,9 @@ module VAT-FLUX-DIFF-PASS-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-fold-pass-rough-spec.k b/tests/specs/mcd/vat-fold-pass-rough-spec.k index cd39116a0c..dffe9662fa 100644 --- a/tests/specs/mcd/vat-fold-pass-rough-spec.k +++ b/tests/specs/mcd/vat-fold-pass-rough-spec.k @@ -34,6 +34,9 @@ module VAT-FOLD-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-fork-diff-pass-rough-spec.k b/tests/specs/mcd/vat-fork-diff-pass-rough-spec.k index 7a586185df..db2a40e390 100644 --- a/tests/specs/mcd/vat-fork-diff-pass-rough-spec.k +++ b/tests/specs/mcd/vat-fork-diff-pass-rough-spec.k @@ -34,6 +34,9 @@ module VAT-FORK-DIFF-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k b/tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k index 9fe6074671..000356f9b6 100644 --- a/tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k +++ b/tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k @@ -34,6 +34,9 @@ module VAT-FROB-DIFF-ZERO-DART-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-heal-pass-spec.k b/tests/specs/mcd/vat-heal-pass-spec.k index 212c3b80d7..e3bd21b658 100644 --- a/tests/specs/mcd/vat-heal-pass-spec.k +++ b/tests/specs/mcd/vat-heal-pass-spec.k @@ -31,6 +31,9 @@ module VAT-HEAL-PASS-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-move-diff-rough-spec.k b/tests/specs/mcd/vat-move-diff-rough-spec.k index f776826786..5254c4f412 100644 --- a/tests/specs/mcd/vat-move-diff-rough-spec.k +++ b/tests/specs/mcd/vat-move-diff-rough-spec.k @@ -35,6 +35,9 @@ module VAT-MOVE-DIFF-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-sin-pass-spec.k b/tests/specs/mcd/vat-sin-pass-spec.k index 7bb38603fa..3dc4c3c990 100644 --- a/tests/specs/mcd/vat-sin-pass-spec.k +++ b/tests/specs/mcd/vat-sin-pass-spec.k @@ -31,6 +31,9 @@ module VAT-SIN-PASS-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-slip-pass-rough-spec.k b/tests/specs/mcd/vat-slip-pass-rough-spec.k index 6094fdce00..5dbc1d313c 100644 --- a/tests/specs/mcd/vat-slip-pass-rough-spec.k +++ b/tests/specs/mcd/vat-slip-pass-rough-spec.k @@ -34,6 +34,9 @@ module VAT-SLIP-PASS-ROUGH-SPEC _ => ?_ false VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vat-subui-fail-rough-spec.k b/tests/specs/mcd/vat-subui-fail-rough-spec.k index 677b570633..a9e7293d32 100644 --- a/tests/specs/mcd/vat-subui-fail-rough-spec.k +++ b/tests/specs/mcd/vat-subui-fail-rough-spec.k @@ -32,6 +32,9 @@ module VAT-SUBUI-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vow-fess-fail-rough-spec.k b/tests/specs/mcd/vow-fess-fail-rough-spec.k index e0a2322d21..ae3bb7e6ab 100644 --- a/tests/specs/mcd/vow-fess-fail-rough-spec.k +++ b/tests/specs/mcd/vow-fess-fail-rough-spec.k @@ -32,6 +32,9 @@ module VOW-FESS-FAIL-ROUGH-SPEC _ => ?_ false VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -158,6 +161,9 @@ module VOW-FESS-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ diff --git a/tests/specs/mcd/vow-flog-fail-rough-spec.k b/tests/specs/mcd/vow-flog-fail-rough-spec.k index 3079114f56..fb026972ba 100644 --- a/tests/specs/mcd/vow-flog-fail-rough-spec.k +++ b/tests/specs/mcd/vow-flog-fail-rough-spec.k @@ -32,6 +32,9 @@ module VOW-FLOG-FAIL-ROUGH-SPEC _ => ?_ false VCallDepth => ?_ + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -158,6 +161,9 @@ module VOW-FLOG-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ @@ -267,6 +273,9 @@ module VOW-FLOG-FAIL-ROUGH-SPEC _ => ?_ _ VCallDepth + 0:Gas => ?_ + 0:Gas => ?_ + false => ?_ _ From 934f66632b338d84d037eabc43245341bfa9e3a7 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Fri, 24 Jul 2026 13:49:10 +0300 Subject: [PATCH 10/11] kproj/{evm.md,lemmas/lemmas.k}: make zero state-gas charges symbolic no-ops Proof specs that omit or leave open get the three EIP-8037 cells framed as fresh symbolic variables, so `0 ~> #chargeStateGas` nondeterministically branched across the charge/spill/OOG rules (the `A <=Gas R` guard is undecidable for unconstrained R:Gas) and SSTORE claims died on a spurious EVMC_OUT_OF_GAS. SstoreStateGas/Credit are [concrete]-only, so symbolic storage arguments also wedged as stuck gas terms even though both provably evaluate to 0 on pre-state-gas schedules (Gstorageset is 0 there). Add priority(40) no-op rules for literal-0 charges to #chargeStateGas, #creditStateGas, #chargeStateGasForCreate, #chargeStateGasIntoCallGas, and [simplification] rules reducing SstoreStateGas/SstoreStateCredit to 0 when notBool Ghasstategas << SCHED >>. Validated: STORAGE-SPEC.{myBool,setMyBool} and ERC20-SPEC.approve.success (the two genuine prove-suite failures) now pass. Co-Authored-By: Claude Fable 5 --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 7 +++++++ kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 3 +++ 2 files changed, 10 insertions(+) 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 e21d921ef5..e9f9d6d638 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -2892,6 +2892,9 @@ Overall Gas syntax InternalOp ::= "#chargeStateGas" | "#creditStateGas" // ------------------------------------------------------------ + rule 0 ~> #chargeStateGas => .K ... [priority(40)] + rule 0 ~> #creditStateGas => .K ... [priority(40)] + rule A:Gas ~> #chargeStateGas => .K ... true R => R -Gas A @@ -2914,6 +2917,8 @@ Overall Gas syntax InternalOp ::= "#chargeStateGasForCreate" // ------------------------------------------------ + rule 0 ~> #chargeStateGasForCreate => .K ... [priority(40)] + rule A:Gas ~> #chargeStateGasForCreate => .K ... true R => R -Gas A @@ -2944,6 +2949,8 @@ Overall Gas syntax InternalOp ::= "#chargeStateGasIntoCallGas" // ---------------------------------------------------- + rule 0 ~> #chargeStateGasIntoCallGas => .K ... [priority(40)] + rule A:Gas ~> #chargeStateGasIntoCallGas => .K ... true R => R -Gas A diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 0dcf1b17a5..094d519e0e 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -173,6 +173,9 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] rule 0 <=Int Cmem(_, N) => true requires 0 <=Int N [simplification] rule 0 <=Int Caddraccess(_, _) => true [simplification] rule 0 <=Int Csstore(_, _, _, _) => true [simplification] + + rule SstoreStateGas(SCHED, _, _, _) => 0 requires notBool Ghasstategas << SCHED >> [simplification] + rule SstoreStateCredit(SCHED, _, _, _) => 0 requires notBool Ghasstategas << SCHED >> [simplification] rule 0 <=Int Cgascap(_, _:Int, _:Int, _) => true [simplification] rule 0 <=Int #allBut64th(_:Int) => true [simplification] rule 0 <=Int Cextra(_, _, _, _, _, _) => true [simplification] From f2a44bd247c40751e3421973f2a22ab1cbc7117a Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Mon, 27 Jul 2026 12:48:53 +0300 Subject: [PATCH 11/11] formatting --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 12 ++++++------ kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md | 4 ++-- 2 files changed, 8 insertions(+), 8 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 e9f9d6d638..ed0f0be596 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1971,7 +1971,7 @@ System Transaction Configuration rule [refund.noGas]: #refund _ => .K ... false syntax InternalOp ::= "#restoreStateGas" Gas Gas - // -------------------------------------------------- + // ------------------------------------------------ rule #restoreStateGas R S => .K ... _ => R PS => PS +Gas S @@ -2891,7 +2891,7 @@ Overall Gas rule _:Gas ~> #deductGas => .K ... false syntax InternalOp ::= "#chargeStateGas" | "#creditStateGas" - // ------------------------------------------------------------ + // ----------------------------------------------------------- rule 0 ~> #chargeStateGas => .K ... [priority(40)] rule 0 ~> #creditStateGas => .K ... [priority(40)] @@ -2948,7 +2948,7 @@ Overall Gas rule _:Gas ~> #creditStateGas => .K ... false syntax InternalOp ::= "#chargeStateGasIntoCallGas" - // ---------------------------------------------------- + // -------------------------------------------------- rule 0 ~> #chargeStateGasIntoCallGas => .K ... [priority(40)] rule A:Gas ~> #chargeStateGasIntoCallGas => .K ... @@ -2978,7 +2978,7 @@ Overall Gas rule _:Gas ~> #deductCallGas => .K ... false syntax InternalOp ::= "#chargeNewAccountStateGas" "(" Int "," Int ")" - // ------------------------------------------------------------- + // --------------------------------------------------------------------- rule true ~> #chargeNewAccountStateGas(VALUE, -1) => #if Ghasstategas << SCHED >> andBool VALUE =/=Int 0 #then Gnewaccount < SCHED > #else 0 #fi ~> #chargeStateGasIntoCallGas ... @@ -2997,7 +2997,7 @@ Overall Gas rule false ~> #chargeNewAccountStateGas(_, -1) => .K ... syntax InternalOp ::= "#chargeSelfdestructNewAccountStateGas" Int - // -------------------------------------------------------------------- + // ----------------------------------------------------------------- rule true ~> #chargeSelfdestructNewAccountStateGas(BAL) => #if Ghasstategas << SCHED >> andBool BAL =/=Int 0 #then Gnewaccount < SCHED > #else 0 #fi ~> #chargeStateGas ... @@ -3006,7 +3006,7 @@ Overall Gas rule false ~> #chargeSelfdestructNewAccountStateGas(_) => .K ... syntax InternalOp ::= "#chargeCreateNewAccountStateGas" Int - // -------------------------------------------------------------- + // ----------------------------------------------------------- rule true ~> #chargeCreateNewAccountStateGas(-1) => #if Ghasstategas << SCHED >> #then Gnewaccount < SCHED > #else 0 #fi ~> #chargeStateGasIntoCallGas ... 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 580626fca6..4afad50145 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md @@ -250,7 +250,7 @@ module GAS-FEES rule [Cblobfee]: Cblobfee(SCHED, EXCESS_BLOB_GAS, BLOB_VERSIONED_HASHES_SIZE) => Ctotalblob(SCHED, BLOB_VERSIONED_HASHES_SIZE) *Int Cbasefeeperblob(SCHED, EXCESS_BLOB_GAS) - rule [Cexcessblob]: Cexcessblob(SCHED, EXCESS_BLOB_GAS, BLOB_GAS_USED) => EXCESS_BLOB_GAS +Int BLOB_GAS_USED -Int Gtargetblobgas < SCHED > requires Gtargetblobgas < SCHED > <=Int EXCESS_BLOB_GAS +Int BLOB_GAS_USED + rule [Cexcessblob]: Cexcessblob(SCHED, EXCESS_BLOB_GAS, BLOB_GAS_USED) => EXCESS_BLOB_GAS +Int BLOB_GAS_USED -Int Gtargetblobgas < SCHED > requires Gtargetblobgas < SCHED > <=Int EXCESS_BLOB_GAS +Int BLOB_GAS_USED rule [Cexcessblob.owise]: Cexcessblob(_, _, _) => 0 [owise] rule [Cdelegationaccess]: Cdelegationaccess(SCHED, true, ISWARM) => Caddraccess(SCHED, ISWARM) @@ -285,7 +285,7 @@ module GAS-FEES rule G0(SCHED, WS, I, J, R) => G0(SCHED, WS, I +Int 1, J, R +Int #if WS[I] ==Int 0 #then Gtxdatazero < SCHED > #else Gtxdatanonzero < SCHED > #fi) [owise] syntax Int ::= #txStateGasReservoir ( Schedule , Int ) [symbol(#txStateGasReservoir), function, total] - // ------------------------------------------------------------------------------------------------------- + // ------------------------------------------------------------------------------------------------------ rule #txStateGasReservoir(SCHED, GLIMIT) => #if Ghasstategas << SCHED >> #then maxInt(0, GLIMIT -Int Gmaxtxgaslimit < SCHED >) #else 0 #fi syntax Int ::= #txStateGasUsed ( Schedule , Int , Int , Int ) [symbol(#txStateGasUsed), function, total]