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..adda0b7d59 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) ... @@ -159,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 @@ -167,7 +171,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 +208,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 +224,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 @@ -261,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) ... @@ -283,42 +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 - ... - - GLIMIT => GLIMIT -Int 25000 [owise] + SCHED + GLIMIT => GLIMIT -Int 25000 + requires notBool Ghasstategas << SCHED >> - syntax InternalOp ::= #setDelegation ( Account , Bytes , Bytes , Bytes ) [symbol(#setDelegation)] - // ------------------------------------------------------------------------------------------------- - rule #setDelegation(AUTHORITY, CID, NONCE, _ADDR) => .K ... ENV_CID + 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) + ... + SCHED + requires Ghasstategas << SCHED >> + + 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 @@ -328,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 > @@ -337,10 +363,52 @@ 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 ... + 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 + 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, 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 => @@ -354,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 fe6317d3e4..ed0f0be596 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,10 @@ In the comments next to each cell, we've marked which component of the YellowPap false 0 + 0:Gas + 0:Gas + false + .Account @@ -126,6 +130,8 @@ In the comments next to each cell, we've marked which component of the YellowPap 0 0 + 0:Gas + 0:Gas [ .JSONs ] @@ -309,6 +315,7 @@ Control Flow rule #halt ~> (_:Int => .K) ... rule #halt ~> (_:OpCode => .K) ... + rule #halt ~> (_:BExp => .K) ... ``` OpCode Execution @@ -642,6 +649,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 +681,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 +707,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 +958,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 +1608,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] @@ -1635,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 ) ... @@ -1648,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 @@ -1670,10 +1767,23 @@ The various `CALL*` (and other inter-contract control flow) operations will be d rule #callWithCode ACCTFROM ACCTTO ACCTCODE BYTES VALUE APPVALUE ARGS STATIC => #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 @@ -1825,7 +1935,7 @@ System Transaction Configuration rule [return.exception]: _:ExceptionalStatusCode #halt ~> #return _ _ - => #popCallStack ~> #popWorldState ~> 0 ~> #push + => #popCallStack ~> #popWorldState ~> #creditChargedNewAccount ~> 0 ~> #push ... _ => .Bytes @@ -1833,22 +1943,26 @@ System Transaction Configuration rule [return.revert]: EVMC_REVERT #halt ~> #return RETSTART RETWIDTH - => #popCallStack ~> #popWorldState - ~> 0 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT + => #popCallStack ~> #popWorldState ~> #creditChargedNewAccount + ~> 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 +1970,29 @@ 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 + PS => PS +Gas S + _ => false + true + rule #restoreStateGas _ _ => .K ... false + + syntax InternalOp ::= "#startFrameStateGas" + // ------------------------------------------- + rule #startFrameStateGas => .K ... + _ => 0 + _ => false + + syntax InternalOp ::= "#creditChargedNewAccount" + // ------------------------------------------------ + rule #creditChargedNewAccount => Gnewaccount < SCHED > ~> #creditStateGas ... + SCHED + true => false + rule #creditChargedNewAccount => .K ... + false + rule #setLocalMem START WIDTH WS => .K ... LM => LM [ START := #range(WS, 0, minInt(WIDTH, lengthBytes(WS))) ] @@ -1933,6 +2070,8 @@ 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 @@ -1940,11 +2079,25 @@ 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 @@ -1988,17 +2141,19 @@ 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 ~> 0 ~> #push ... + #halt ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #creditChargedNewAccount ~> #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 ... @@ -2006,17 +2161,20 @@ 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 ~> #creditChargedNewAccount ~> 0 ~> #push ... SCHED OUT => .Bytes requires notBool ( lengthBytes(OUT) <=Int maxCodeSize < SCHED > andBool #isValidCode(OUT, SCHED) ) rule #finishCodeDeposit ACCT OUT => #popCallStack ~> #dropWorldState + ~> #restoreStateGas SGR SGS ~> #refund GAVAIL ~> ACCT ~> #push ... GAVAIL + SGR + SGS ACCT _ => OUT @@ -2033,7 +2191,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 ~> #creditChargedNewAccount ~> 0 ~> #push ... SCHED requires SCHED =/=K FRONTIER @@ -2049,6 +2207,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) ... @@ -2061,6 +2222,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- ... SCHED + CD requires #hasValidInitCode(MEMWIDTH, SCHED) [preserves-definedness] @@ -2077,6 +2239,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)) ... @@ -2084,6 +2249,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]: @@ -2724,6 +2890,140 @@ 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 0 ~> #chargeStateGas => .K ... [priority(40)] + rule 0 ~> #creditStateGas => .K ... [priority(40)] + + 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 + + syntax InternalOp ::= "#chargeStateGasForCreate" + // ------------------------------------------------ + rule 0 ~> #chargeStateGasForCreate => .K ... [priority(40)] + + 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 ~> #allocateCreateGas ~> #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) + G => G +Gas minGas(A, S) + R => R +Gas (A -Gas minGas(A, S)) + + rule _:Gas ~> #creditStateGas => .K ... false + + syntax InternalOp ::= "#chargeStateGasIntoCallGas" + // -------------------------------------------------- + rule 0 ~> #chargeStateGasIntoCallGas => .K ... [priority(40)] + + 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 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) + => #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 + _ => Ghasstategas << SCHED >> andBool VALUE =/=Int 0 + requires CD =/=Int -1 + rule false ~> #chargeNewAccountStateGas(_, CD) => .K ... + _ => false + requires CD =/=Int -1 + 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 + ... + + 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 ~> #chargeStateGasForCreate + ... + + SCHED + _ => Ghasstategas << SCHED >> + requires CD =/=Int -1 + rule false ~> #chargeCreateNewAccountStateGas(CD) => .K ... + _ => false + requires CD =/=Int -1 + rule false ~> #chargeCreateNewAccountStateGas(-1) => .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] @@ -2828,7 +3128,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] ``` @@ -2884,6 +3184,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 @@ -2911,7 +3222,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 @@ -3048,6 +3364,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 @@ -3064,16 +3389,37 @@ 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)) ... 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..4afad50145 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) @@ -136,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]: @@ -148,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 @@ -164,7 +180,7 @@ module GAS-FEES 0 #fi #fi - requires Ghasdirtysstore << SCHED >> + requires Ghasdirtysstore << SCHED >> andBool notBool Ghasstategas << SCHED >> [concrete] rule [Rsstore.old]: @@ -173,13 +189,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 @@ -221,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) @@ -255,6 +284,24 @@ 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 , 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 >) + andBool TX_GAS_LIMIT <=Int (BLOCK_GAS_LIMIT -Int GASUSED) + #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/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] 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..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" - // ------------------------------------------------------------- + | "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 @@ -181,8 +185,10 @@ 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 + rule [GhasstategasDefault]: Ghasstategas << DEFAULT >> => false ``` ### Frontier Schedule @@ -491,12 +497,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 +528,36 @@ 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 [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 orBool SCHEDCONST ==K Blobbasefeeupdatefraction + orBool SCHEDCONST ==K Gsstoreset + orBool SCHEDCONST ==K Gnewaccount + 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 [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >> + rule [GhasauthbaserefundAmsterdam]: Ghasauthbaserefund << AMSTERDAM >> => false + rule [GhasstategasAmsterdam]: Ghasstategas << AMSTERDAM >> => true + rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >> + 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..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,9 @@ The `"rlp"` key loads the block information. SCHED BASE_FEE BLOCK_GAS_LIMIT + GASUSED + GASUSEDREG + GASUSEDSTATE ACCTFROM BAL @@ -626,6 +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, gas2Int(GASUSED), GASUSEDREG, GASUSEDSTATE) andBool size(TX_AUTH_LIST) >Int 0 andBool #checkAuthorityList(TX_AUTH_LIST) rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]] @@ -633,6 +637,9 @@ The `"rlp"` key loads the block information. BASE_FEE EXCESS_BLOB_GAS BLOCK_GAS_LIMIT + GASUSED + GASUSEDREG + GASUSEDSTATE ACCTFROM BAL @@ -662,12 +669,16 @@ 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, 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 ACCTFROM BAL @@ -691,11 +702,15 @@ 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, gas2Int(GASUSED), GASUSEDREG, GASUSEDSTATE) rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]] SCHED BASE_FEE BLOCK_GAS_LIMIT + GASUSED + GASUSEDREG + GASUSEDSTATE ACCTFROM BAL @@ -718,6 +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, gas2Int(GASUSED), GASUSEDREG, GASUSEDSTATE) rule #isValidTransaction (_, _) => false [owise] ``` 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 => ?_ _