diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 6064e4d877..9c0fe1f60b 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.636" +version = "1.0.637" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 6284b18225..1637255cd7 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '1.0.636' +VERSION: Final = '1.0.637' diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/asm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/asm.md index 897e3d4228..0964a84034 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/asm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/asm.md @@ -117,6 +117,8 @@ Operator `#revOps` can be used to reverse a program. rule #asmOpCode( MSIZE ) => 89 rule #asmOpCode( GAS ) => 90 rule #asmOpCode( JUMPDEST ) => 91 + rule #asmOpCode( TLOAD ) => 92 + rule #asmOpCode( TSTORE ) => 93 rule #asmOpCode( PUSHZERO ) => 95 rule #asmOpCode( PUSH(1) ) => 96 rule #asmOpCode( PUSH(2) ) => 97 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 c3c9ce37e6..f047efd85e 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -133,12 +133,13 @@ In the comments next to each cell, we've marked which component of the YellowPap - 0 - 0 - .Bytes:AccountCode - .Map - .Map - 0 + 0 + 0 + .Bytes:AccountCode + .Map + .Map + .Map + 0 @@ -419,6 +420,7 @@ The `#next [_]` operator initiates execution by: rule #changesState(CREATE , _) => true rule #changesState(CREATE2 , _) => true rule #changesState(SELFDESTRUCT , _) => true + rule #changesState(TSTORE , _) => true rule #changesState(_ , _) => false [owise] ``` @@ -762,11 +764,12 @@ These are just used by the other operators for shuffling local execution state a => ACCT - 0 - .Bytes:AccountCode - .Map - .Map - 0 + 0 + .Bytes:AccountCode + .Map + .Map + 0 + .Map ) ... @@ -1225,6 +1228,29 @@ These rules reach into the network state and load/store from account storage: ... [preserves-definedness] + + syntax UnStackOp ::= "TLOAD" + // ---------------------------- + rule [tload]: + TLOAD INDEX => #lookup(TSTORAGE, INDEX) ~> #push ... + ACCT + + ACCT + TSTORAGE + ... + + + syntax BinStackOp ::= "TSTORE" + // ------------------------------ + rule [tstore]: + TSTORE INDEX NEW => .K ... + ACCT + + ACCT + TSTORAGE => TSTORAGE [ INDEX <- NEW ] + ... + + [preserves-definedness] ``` ### Call Operations @@ -2042,9 +2068,15 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). - `#gasExec` loads all the relevant surrounding state and uses that to compute the intrinsic execution gas of each opcode. +- Gas cost for `TSTORE` is the same as a warm `SSTORE` of a dirty slot (i.e. original value is not new value, original is not current value, currently 100 gas). +- Gas cost of `TLOAD` is the same as a hot `SLOAD` (value has been read before, currently 100 gas). +- Gas cost cannot be on par with memory access due to transient storage’s interactions with reverts. ```k syntax InternalOp ::= #gasExec ( Schedule , OpCode ) [symbol(#gasExec)] // ----------------------------------------------------------------------- + rule #gasExec(SCHED, TLOAD _ ) => Gwarmstorageread < SCHED > ... + rule #gasExec(SCHED, TSTORE _ _) => Gwarmstoragedirtystore < SCHED > ... + rule #gasExec(SCHED, SSTORE INDEX NEW) => Csstore(SCHED, NEW, #lookup(STORAGE, INDEX), #lookup(ORIGSTORAGE, INDEX)) ... ACCT GAVAIL @@ -2363,7 +2395,9 @@ After interpreting the strings representing programs as a `WordStack`, it should rule #dasmOpCode( 89, _ ) => MSIZE rule #dasmOpCode( 90, _ ) => GAS rule #dasmOpCode( 91, _ ) => JUMPDEST - rule #dasmOpCode( 95, SCHED ) => PUSHZERO requires Ghaspushzero << SCHED >> + rule #dasmOpCode( 92, SCHED ) => TLOAD requires Ghastransient << SCHED >> + rule #dasmOpCode( 93, SCHED ) => TSTORE requires Ghastransient << SCHED >> + rule #dasmOpCode( 95, SCHED ) => PUSHZERO requires Ghaspushzero << SCHED >> rule #dasmOpCode( 96, _ ) => PUSH(1) rule #dasmOpCode( 97, _ ) => PUSH(2) rule #dasmOpCode( 98, _ ) => PUSH(3) 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 83e0834835..f37bd55423 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -28,8 +28,8 @@ module SCHEDULE | "Ghasdirtysstore" | "Ghascreate2" | "Ghasextcodehash" | "Ghasselfbalance" | "Ghassstorestipend" | "Ghaschainid" | "Ghasaccesslist" | "Ghasbasefee" | "Ghasrejectedfirstbyte" | "Ghasprevrandao" | "Ghasmaxinitcodesize" | "Ghaspushzero" - | "Ghaswarmcoinbase" - // ------------------------------------------ + | "Ghaswarmcoinbase" | "Ghastransient" + // ------------------------------------------------------------------- ``` ### Schedule Constants @@ -47,8 +47,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. | "Gtransaction" | "Glog" | "Glogdata" | "Glogtopic" | "Gsha3" | "Gsha3word" | "Gcopy" | "Gblockhash" | "Gquadcoeff" | "maxCodeSize" | "Rb" | "Gquaddivisor" | "Gecadd" | "Gecmul" | "Gecpairconst" | "Gecpaircoeff" | "Gfround" | "Gcoldsload" | "Gcoldaccountaccess" | "Gwarmstorageread" | "Gaccesslistaddress" - | "Gaccessliststoragekey" | "Rmaxquotient" | "Ginitcodewordcost" | "maxInitCodeSize" - // ---------------------------------------------------------------------------------------------------------------------- + | "Gaccessliststoragekey" | "Rmaxquotient" | "Ginitcodewordcost" | "maxInitCodeSize" | "Gwarmstoragedirtystore" + // ---------------------------------------------------------------------------------------------------------------------------------------------------- ``` ### Default Schedule @@ -112,9 +112,10 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule maxCodeSize < DEFAULT > => 2 ^Int 32 -Int 1 rule Rb < DEFAULT > => 5 *Int (10 ^Int 18) - rule Gcoldsload < DEFAULT > => 0 - rule Gcoldaccountaccess < DEFAULT > => 0 - rule Gwarmstorageread < DEFAULT > => 0 + rule Gcoldsload < DEFAULT > => 0 + rule Gcoldaccountaccess < DEFAULT > => 0 + rule Gwarmstorageread < DEFAULT > => 0 + rule Gwarmstoragedirtystore < DEFAULT > => 0 rule Gaccessliststoragekey < DEFAULT > => 0 rule Gaccesslistaddress < DEFAULT > => 0 @@ -145,6 +146,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule Ghasmaxinitcodesize << DEFAULT >> => false rule Ghaspushzero << DEFAULT >> => false rule Ghaswarmcoinbase << DEFAULT >> => false + rule Ghastransient << DEFAULT >> => false ``` ### Frontier Schedule @@ -379,9 +381,13 @@ A `ScheduleConst` is a constant determined by the fee schedule. ```k syntax Schedule ::= "CANCUN" [symbol(CANCUN_EVM), smtlib(schedule_CANCUN)] // -------------------------------------------------------------------------- - rule SCHEDCONST < CANCUN > => SCHEDCONST < SHANGHAI > + rule Gwarmstoragedirtystore < CANCUN > => Gwarmstorageread < CANCUN > + rule SCHEDCONST < CANCUN > => SCHEDCONST < SHANGHAI > + requires notBool (SCHEDCONST ==K Gwarmstoragedirtystore) - rule SCHEDFLAG << CANCUN >> => SCHEDFLAG << SHANGHAI >> + rule Ghastransient << CANCUN >> => true + rule SCHEDFLAG << CANCUN >> => SCHEDFLAG << SHANGHAI >> + requires notBool (SCHEDFLAG ==K Ghastransient) ``` ```k endmodule diff --git a/kevm-pyk/src/tests/integration/test_conformance.py b/kevm-pyk/src/tests/integration/test_conformance.py index b3da8ac9d1..9373b433e7 100644 --- a/kevm-pyk/src/tests/integration/test_conformance.py +++ b/kevm-pyk/src/tests/integration/test_conformance.py @@ -118,7 +118,7 @@ def test_rest_vm(test_file: Path) -> None: ids=[str(test_file.relative_to(ALL_TEST_DIR)) for test_file in BCHAIN_TESTS], ) def test_bchain(test_file: Path) -> None: - _test(test_file, 'SHANGHAI', 'NORMAL', 1, True) + _test(test_file, 'CANCUN', 'NORMAL', 1, True) @pytest.mark.skip(reason='failing / slow blockchain tests') @@ -128,4 +128,4 @@ def test_bchain(test_file: Path) -> None: ids=[str(test_file.relative_to(ALL_TEST_DIR)) for test_file in SKIPPED_BCHAIN_TESTS], ) def test_rest_bchain(test_file: Path) -> None: - _test(test_file, 'SHANGHAI', 'NORMAL', 1, True) + _test(test_file, 'CANCUN', 'NORMAL', 1, True) diff --git a/package/version b/package/version index 8895d5daf4..e79d803c40 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.636 +1.0.637 diff --git a/tests/failing.llvm b/tests/failing.llvm index fcc549d250..63ac3c70b7 100644 --- a/tests/failing.llvm +++ b/tests/failing.llvm @@ -1,14 +1,6 @@ BlockchainTests/GeneralStateTests/VMTests/vmTests/suicide.json,suicide_d0g0v0_Cancun BlockchainTests/GeneralStateTests/VMTests/vmTests/suicide.json,suicide_d1g0v0_Cancun BlockchainTests/GeneralStateTests/VMTests/vmTests/suicide.json,suicide_d2g0v0_Cancun -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/contract_creation.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/gas_usage.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/tload_after_tstore_is_zero.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/tload_after_sstore.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/subcall.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/transient_storage_unset_values.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/reentrant_call.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/tload_after_tstore.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/reentrant_selfdestructing_call.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/multi_block_beacon_root_timestamp_calls.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/beacon_root_contract_timestamps.json,* diff --git a/tests/failing/ContractCreationSpam_d0g0v0.json.expected b/tests/failing/ContractCreationSpam_d0g0v0.json.expected index 071a3d9e1c..e6afcd0544 100644 --- a/tests/failing/ContractCreationSpam_d0g0v0.json.expected +++ b/tests/failing/ContractCreationSpam_d0g0v0.json.expected @@ -192,6 +192,9 @@ .Map + + .Map + 0 @@ -211,6 +214,9 @@ .Map + + .Map + 0 @@ -230,6 +236,9 @@ .Map + + .Map + 1 @@ -249,6 +258,9 @@ .Map + + .Map + 0 diff --git a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected index a5c16f7ae5..a80fbdb5a4 100644 --- a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected +++ b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected @@ -194,6 +194,9 @@ 0 |-> 0 1 |-> 85121 + + .Map + 0 @@ -213,6 +216,9 @@ .Map + + .Map + 0 @@ -232,6 +238,9 @@ .Map + + .Map + 0 @@ -251,6 +260,9 @@ .Map + + .Map + 0 @@ -270,6 +282,9 @@ .Map + + .Map + 0 @@ -289,6 +304,9 @@ .Map + + .Map + 1 diff --git a/tests/specs/benchmarks/address00-spec.k b/tests/specs/benchmarks/address00-spec.k index 40f48c7f4b..99037341b8 100644 --- a/tests/specs/benchmarks/address00-spec.k +++ b/tests/specs/benchmarks/address00-spec.k @@ -81,6 +81,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -94,6 +97,9 @@ _ _ CALLEE_NONCE + + _ + @@ -104,6 +110,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/bytes00-spec.k b/tests/specs/benchmarks/bytes00-spec.k index 6a0bdfaa72..32c3523965 100644 --- a/tests/specs/benchmarks/bytes00-spec.k +++ b/tests/specs/benchmarks/bytes00-spec.k @@ -81,6 +81,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -94,6 +97,9 @@ _ _ CALLEE_NONCE + + _ + @@ -104,6 +110,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/dynamicarray00-spec.k b/tests/specs/benchmarks/dynamicarray00-spec.k index 6040136888..45a095199b 100644 --- a/tests/specs/benchmarks/dynamicarray00-spec.k +++ b/tests/specs/benchmarks/dynamicarray00-spec.k @@ -81,6 +81,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -94,6 +97,9 @@ _ _ CALLEE_NONCE + + _ + @@ -104,6 +110,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/ecrecover00-siginvalid-spec.k b/tests/specs/benchmarks/ecrecover00-siginvalid-spec.k index fe0b5abb9c..47166f7782 100644 --- a/tests/specs/benchmarks/ecrecover00-siginvalid-spec.k +++ b/tests/specs/benchmarks/ecrecover00-siginvalid-spec.k @@ -81,6 +81,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -94,6 +97,9 @@ _ _ CALLEE_NONCE + + _ + @@ -104,6 +110,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/ecrecover00-sigvalid-spec.k b/tests/specs/benchmarks/ecrecover00-sigvalid-spec.k index 8d9706507f..ff97e0bb39 100644 --- a/tests/specs/benchmarks/ecrecover00-sigvalid-spec.k +++ b/tests/specs/benchmarks/ecrecover00-sigvalid-spec.k @@ -81,6 +81,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -94,6 +97,9 @@ _ _ CALLEE_NONCE + + _ + @@ -104,6 +110,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k b/tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k index 49d88f11d6..7ddcd7ef89 100644 --- a/tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k +++ b/tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k @@ -84,6 +84,9 @@ _ _ _ + + _ + @@ -97,6 +100,9 @@ _ _ _ + + _ + @@ -107,6 +113,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k b/tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k index 08686c5d37..ef7ec45955 100644 --- a/tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k +++ b/tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k @@ -84,6 +84,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -97,6 +100,9 @@ _ _ CALLEE_NONCE + + _ + @@ -107,6 +113,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k b/tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k index 22cc7b838e..d55a0baf6a 100644 --- a/tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k +++ b/tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k @@ -84,6 +84,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -97,6 +100,9 @@ _ _ CALLEE_NONCE + + _ + @@ -107,6 +113,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k b/tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k index 16fa6327e5..9ce8610234 100644 --- a/tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k +++ b/tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k @@ -85,6 +85,9 @@ _ _ _ + + _ + @@ -98,6 +101,9 @@ _ _ _ + + _ + @@ -108,6 +114,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k b/tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k index dd76071271..55592c3e45 100644 --- a/tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k +++ b/tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k @@ -85,6 +85,9 @@ _ _ _ + + _ + @@ -98,6 +101,9 @@ _ _ _ + + _ + @@ -108,6 +114,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k b/tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k index 64c708788e..e47f1f2c04 100644 --- a/tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k +++ b/tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k @@ -85,6 +85,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -98,6 +101,9 @@ _ _ CALLEE_NONCE + + _ + @@ -108,6 +114,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/encode-keccak00-spec.k b/tests/specs/benchmarks/encode-keccak00-spec.k index a88e72b6b6..eed4357f5d 100644 --- a/tests/specs/benchmarks/encode-keccak00-spec.k +++ b/tests/specs/benchmarks/encode-keccak00-spec.k @@ -81,6 +81,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -94,6 +97,9 @@ _ _ CALLEE_NONCE + + _ + @@ -104,6 +110,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/encodepacked-keccak01-spec.k b/tests/specs/benchmarks/encodepacked-keccak01-spec.k index b563c2c75b..f80b2b961f 100644 --- a/tests/specs/benchmarks/encodepacked-keccak01-spec.k +++ b/tests/specs/benchmarks/encodepacked-keccak01-spec.k @@ -81,6 +81,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -94,6 +97,9 @@ _ _ CALLEE_NONCE + + _ + @@ -104,6 +110,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/keccak00-spec.k b/tests/specs/benchmarks/keccak00-spec.k index e111efa7b2..fdabcc1028 100644 --- a/tests/specs/benchmarks/keccak00-spec.k +++ b/tests/specs/benchmarks/keccak00-spec.k @@ -81,6 +81,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -94,6 +97,9 @@ _ _ CALLEE_NONCE + + _ + @@ -104,6 +110,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/overflow00-nooverflow-spec.k b/tests/specs/benchmarks/overflow00-nooverflow-spec.k index 74060be5f2..468d0e4a36 100644 --- a/tests/specs/benchmarks/overflow00-nooverflow-spec.k +++ b/tests/specs/benchmarks/overflow00-nooverflow-spec.k @@ -81,6 +81,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -94,6 +97,9 @@ _ _ CALLEE_NONCE + + _ + @@ -104,9 +110,9 @@ _ .Map .Map 0 + .Map - ... _ diff --git a/tests/specs/benchmarks/overflow00-overflow-spec.k b/tests/specs/benchmarks/overflow00-overflow-spec.k index d4f39b4926..0b1a472680 100644 --- a/tests/specs/benchmarks/overflow00-overflow-spec.k +++ b/tests/specs/benchmarks/overflow00-overflow-spec.k @@ -81,6 +81,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -94,6 +97,9 @@ _ _ CALLEE_NONCE + + _ + @@ -104,6 +110,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/requires01-a0gt0-spec.k b/tests/specs/benchmarks/requires01-a0gt0-spec.k index 8653df2498..c8c209c0fc 100644 --- a/tests/specs/benchmarks/requires01-a0gt0-spec.k +++ b/tests/specs/benchmarks/requires01-a0gt0-spec.k @@ -77,6 +77,9 @@ module REQUIRES01-A0GT0-SPEC _S _OS CONTRACT_NONCE + + _ + @@ -90,6 +93,9 @@ module REQUIRES01-A0GT0-SPEC _ CALLEE_NONCE + + _ + @@ -100,6 +106,7 @@ module REQUIRES01-A0GT0-SPEC .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/requires01-a0le0-spec.k b/tests/specs/benchmarks/requires01-a0le0-spec.k index c7d149cf43..47e9c7c92f 100644 --- a/tests/specs/benchmarks/requires01-a0le0-spec.k +++ b/tests/specs/benchmarks/requires01-a0le0-spec.k @@ -77,6 +77,9 @@ module REQUIRES01-A0LE0-SPEC _S _OS CONTRACT_NONCE + + _ + @@ -90,6 +93,9 @@ module REQUIRES01-A0LE0-SPEC _ CALLEE_NONCE + + _ + @@ -100,6 +106,7 @@ module REQUIRES01-A0LE0-SPEC .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/staticarray00-spec.k b/tests/specs/benchmarks/staticarray00-spec.k index 62c3d909ab..e7e4388abb 100644 --- a/tests/specs/benchmarks/staticarray00-spec.k +++ b/tests/specs/benchmarks/staticarray00-spec.k @@ -81,6 +81,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -94,6 +97,9 @@ _ _ CALLEE_NONCE + + _ + @@ -104,6 +110,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/staticloop00-a0lt10-spec.k b/tests/specs/benchmarks/staticloop00-a0lt10-spec.k index 9e7fff0c74..613a5c43af 100644 --- a/tests/specs/benchmarks/staticloop00-a0lt10-spec.k +++ b/tests/specs/benchmarks/staticloop00-a0lt10-spec.k @@ -81,6 +81,9 @@ _ _ CONTRACT_NONCE + + _ + @@ -94,6 +97,9 @@ _ _ CALLEE_NONCE + + _ + @@ -104,6 +110,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/storagevar00-spec.k b/tests/specs/benchmarks/storagevar00-spec.k index a8af7b8d17..b7cbcc4806 100644 --- a/tests/specs/benchmarks/storagevar00-spec.k +++ b/tests/specs/benchmarks/storagevar00-spec.k @@ -77,6 +77,9 @@ module STORAGEVAR00-SPEC S S CONTRACT_NONCE + + _ + @@ -86,6 +89,9 @@ module STORAGEVAR00-SPEC _S _OS CALLEE_NONCE + + _ + @@ -96,6 +102,7 @@ module STORAGEVAR00-SPEC .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/storagevar01-spec.k b/tests/specs/benchmarks/storagevar01-spec.k index f7cf527fd0..122ee10741 100644 --- a/tests/specs/benchmarks/storagevar01-spec.k +++ b/tests/specs/benchmarks/storagevar01-spec.k @@ -77,6 +77,9 @@ module STORAGEVAR01-SPEC S => S [ #hashedLocation("Solidity", 0, .IntList) <- 5 ] _OS => ?_OS CONTRACT_NONCE + + _ + @@ -90,6 +93,9 @@ module STORAGEVAR01-SPEC _ CALLEE_NONCE + + _ + @@ -100,6 +106,7 @@ module STORAGEVAR01-SPEC .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/storagevar02-nooverflow-spec.k b/tests/specs/benchmarks/storagevar02-nooverflow-spec.k index 490dbd8f17..08656b446b 100644 --- a/tests/specs/benchmarks/storagevar02-nooverflow-spec.k +++ b/tests/specs/benchmarks/storagevar02-nooverflow-spec.k @@ -77,6 +77,9 @@ module STORAGEVAR02-NOOVERFLOW-SPEC S => S [ #hashedLocation("Solidity", 0, .IntList) <- N0 +Int 1 ] _OS => ?_OS CONTRACT_NONCE + + _ + @@ -90,6 +93,9 @@ module STORAGEVAR02-NOOVERFLOW-SPEC _ CALLEE_NONCE + + _ + @@ -100,6 +106,7 @@ module STORAGEVAR02-NOOVERFLOW-SPEC .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/storagevar02-overflow-spec.k b/tests/specs/benchmarks/storagevar02-overflow-spec.k index 362f0be9d2..a777951320 100644 --- a/tests/specs/benchmarks/storagevar02-overflow-spec.k +++ b/tests/specs/benchmarks/storagevar02-overflow-spec.k @@ -77,6 +77,9 @@ module STORAGEVAR02-OVERFLOW-SPEC S => S [ #hashedLocation("Solidity", 0, .IntList) <- 0 ] _OS => ?_OS CONTRACT_NONCE + + _ + @@ -90,6 +93,9 @@ module STORAGEVAR02-OVERFLOW-SPEC _ CALLEE_NONCE + + _ + @@ -100,6 +106,7 @@ module STORAGEVAR02-OVERFLOW-SPEC .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/storagevar03-spec.k b/tests/specs/benchmarks/storagevar03-spec.k index 1de200c3c3..f2da984998 100644 --- a/tests/specs/benchmarks/storagevar03-spec.k +++ b/tests/specs/benchmarks/storagevar03-spec.k @@ -77,6 +77,9 @@ module STORAGEVAR03-SPEC _S => ?_S _OS CONTRACT_NONCE + + _ + @@ -90,6 +93,9 @@ module STORAGEVAR03-SPEC _ CALLEE_NONCE + + _ + @@ -100,6 +106,7 @@ module STORAGEVAR03-SPEC .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/structarg00-spec.k b/tests/specs/benchmarks/structarg00-spec.k index d1386176ad..a2a77111cc 100644 --- a/tests/specs/benchmarks/structarg00-spec.k +++ b/tests/specs/benchmarks/structarg00-spec.k @@ -81,8 +81,10 @@ _ _ CONTRACT_NONCE + + _ + - CALLEE_ID CALLEE_BAL @@ -94,6 +96,9 @@ _ _ CALLEE_NONCE + + _ + @@ -104,6 +109,7 @@ _ .Map .Map 0 + .Map diff --git a/tests/specs/benchmarks/structarg01-spec.k b/tests/specs/benchmarks/structarg01-spec.k index e900587726..3a7ba382f3 100644 --- a/tests/specs/benchmarks/structarg01-spec.k +++ b/tests/specs/benchmarks/structarg01-spec.k @@ -81,8 +81,10 @@ module STRUCTARG01-SPEC _ CONTRACT_NONCE + + _ + - CALLEE_ID CALLEE_BAL @@ -94,6 +96,9 @@ module STRUCTARG01-SPEC _ CALLEE_NONCE + + _ + ... diff --git a/tests/specs/erc20/ds/allowance-spec.k b/tests/specs/erc20/ds/allowance-spec.k index aaa8e31c6d..da953c057b 100644 --- a/tests/specs/erc20/ds/allowance-spec.k +++ b/tests/specs/erc20/ds/allowance-spec.k @@ -90,6 +90,7 @@ module ALLOWANCE-SPEC _:Map _ _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/ds/approve-failure-spec.k b/tests/specs/erc20/ds/approve-failure-spec.k index 18508dd7dc..9fc24ef1ee 100644 --- a/tests/specs/erc20/ds/approve-failure-spec.k +++ b/tests/specs/erc20/ds/approve-failure-spec.k @@ -90,6 +90,7 @@ module APPROVE-FAILURE-SPEC _:Map _ _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/ds/approve-success-spec.k b/tests/specs/erc20/ds/approve-success-spec.k index 20623b3d5d..e631637149 100644 --- a/tests/specs/erc20/ds/approve-success-spec.k +++ b/tests/specs/erc20/ds/approve-success-spec.k @@ -93,6 +93,7 @@ _:Map #hashedLocation("Solidity", 2, CALLER_ID SPENDER) |-> ORIG_VAL _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/ds/balanceOf-spec.k b/tests/specs/erc20/ds/balanceOf-spec.k index c995e284e2..b09884928c 100644 --- a/tests/specs/erc20/ds/balanceOf-spec.k +++ b/tests/specs/erc20/ds/balanceOf-spec.k @@ -90,6 +90,7 @@ module BALANCEOF-SPEC _:Map _ _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/ds/totalSupply-spec.k b/tests/specs/erc20/ds/totalSupply-spec.k index 98c3e7b88b..c3f78de8b4 100644 --- a/tests/specs/erc20/ds/totalSupply-spec.k +++ b/tests/specs/erc20/ds/totalSupply-spec.k @@ -90,6 +90,7 @@ module TOTALSUPPLY-SPEC _:Map _ _ + _ // ... // TODO: fix 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 c01bcbdfb4..0b8cc655d2 100644 --- a/tests/specs/erc20/ds/transfer-failure-1-a-spec.k +++ b/tests/specs/erc20/ds/transfer-failure-1-a-spec.k @@ -95,6 +95,7 @@ _:Map #hashedLocation("Solidity", 1, TO_ID) |-> BAL_TO _:Map _ + _ // ... // TODO: fix 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 873a2a2425..3b09a180aa 100644 --- a/tests/specs/erc20/ds/transfer-failure-1-b-spec.k +++ b/tests/specs/erc20/ds/transfer-failure-1-b-spec.k @@ -95,6 +95,7 @@ _:Map #hashedLocation("Solidity", 1, TO_ID) |-> BAL_TO _:Map _ + _ // ... // TODO: fix 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 5fee6d38b5..0f74410f8f 100644 --- a/tests/specs/erc20/ds/transfer-failure-1-c-spec.k +++ b/tests/specs/erc20/ds/transfer-failure-1-c-spec.k @@ -95,6 +95,7 @@ _:Map #hashedLocation("Solidity", 1, TO_ID) |-> BAL_TO _:Map _ + _ // ... // TODO: fix 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 791aaa2c9b..6fe65bd1fb 100644 --- a/tests/specs/erc20/ds/transfer-failure-2-a-spec.k +++ b/tests/specs/erc20/ds/transfer-failure-2-a-spec.k @@ -93,6 +93,7 @@ _:Map #hashedLocation("Solidity", 1, CALLER_ID) |-> BAL_FROM _:Map _ + _ // ... // TODO: fix 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 341af69b3b..6317b7de8b 100644 --- a/tests/specs/erc20/ds/transfer-failure-2-b-spec.k +++ b/tests/specs/erc20/ds/transfer-failure-2-b-spec.k @@ -93,6 +93,7 @@ _:Map #hashedLocation("Solidity", 1, CALLER_ID) |-> BAL_FROM _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/ds/transfer-success-1-spec.k b/tests/specs/erc20/ds/transfer-success-1-spec.k index e09cf3e858..835eec38fc 100644 --- a/tests/specs/erc20/ds/transfer-success-1-spec.k +++ b/tests/specs/erc20/ds/transfer-success-1-spec.k @@ -95,6 +95,7 @@ _:Map #hashedLocation("Solidity", 1, TO_ID) |-> BAL_TO _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/ds/transfer-success-2-spec.k b/tests/specs/erc20/ds/transfer-success-2-spec.k index 87a4fe46cc..101b33599d 100644 --- a/tests/specs/erc20/ds/transfer-success-2-spec.k +++ b/tests/specs/erc20/ds/transfer-success-2-spec.k @@ -93,6 +93,7 @@ _:Map #hashedLocation("Solidity", 1, CALLER_ID) |-> BAL_FROM _:Map _ + _ // ... // TODO: fix 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 5267952c74..39646e8e72 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-1-a-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-1-a-spec.k @@ -97,6 +97,7 @@ _:Map #hashedLocation("Solidity", 2, FROM_ID CALLER_ID) |-> ALLOW _:Map _ + _ // ... // TODO: fix 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 1b551f154b..36a3f47b29 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-1-b-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-1-b-spec.k @@ -97,6 +97,7 @@ _:Map #hashedLocation("Solidity", 2, FROM_ID CALLER_ID) |-> ALLOW _:Map _ + _ // ... // TODO: fix 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 ec84e8d1d9..9e85a2eaa4 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-1-c-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-1-c-spec.k @@ -97,6 +97,7 @@ _:Map #hashedLocation("Solidity", 2, FROM_ID CALLER_ID) |-> ALLOW _:Map _ + _ // ... // TODO: fix 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 421a9a8e68..f242b0d10b 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-1-d-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-1-d-spec.k @@ -97,6 +97,7 @@ _:Map #hashedLocation("Solidity", 2, FROM_ID CALLER_ID) |-> ALLOW _:Map _ + _ // ... // TODO: fix 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 6259fbaf74..f81b103f97 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-2-a-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-2-a-spec.k @@ -95,6 +95,7 @@ _:Map #hashedLocation("Solidity", 2, FROM_ID CALLER_ID) |-> ALLOW _:Map _ + _ // ... // TODO: fix 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 d9885c1a23..5625bc7db8 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-2-b-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-2-b-spec.k @@ -95,6 +95,7 @@ _:Map #hashedLocation("Solidity", 2, FROM_ID CALLER_ID) |-> ALLOW _:Map _ + _ // ... // TODO: fix 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 6f38c028d7..92465c142d 100644 --- a/tests/specs/erc20/ds/transferFrom-failure-2-c-spec.k +++ b/tests/specs/erc20/ds/transferFrom-failure-2-c-spec.k @@ -95,6 +95,7 @@ _:Map #hashedLocation("Solidity", 2, FROM_ID CALLER_ID) |-> ALLOW _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/ds/transferFrom-success-1-spec.k b/tests/specs/erc20/ds/transferFrom-success-1-spec.k index dd682596cb..262a4fa623 100644 --- a/tests/specs/erc20/ds/transferFrom-success-1-spec.k +++ b/tests/specs/erc20/ds/transferFrom-success-1-spec.k @@ -97,6 +97,7 @@ _:Map #hashedLocation("Solidity", 2, FROM_ID CALLER_ID) |-> ALLOW _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/ds/transferFrom-success-2-spec.k b/tests/specs/erc20/ds/transferFrom-success-2-spec.k index ad8e37f101..cfc7e395e7 100644 --- a/tests/specs/erc20/ds/transferFrom-success-2-spec.k +++ b/tests/specs/erc20/ds/transferFrom-success-2-spec.k @@ -95,6 +95,7 @@ _:Map #hashedLocation("Solidity", 2, FROM_ID CALLER_ID) |-> ALLOW _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/hkg/allowance-spec.k b/tests/specs/erc20/hkg/allowance-spec.k index 68561000c0..c7f193f7e7 100644 --- a/tests/specs/erc20/hkg/allowance-spec.k +++ b/tests/specs/erc20/hkg/allowance-spec.k @@ -90,6 +90,7 @@ module ALLOWANCE-SPEC _:Map _ _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/hkg/approve-spec.k b/tests/specs/erc20/hkg/approve-spec.k index a0610d875d..ff997612b6 100644 --- a/tests/specs/erc20/hkg/approve-spec.k +++ b/tests/specs/erc20/hkg/approve-spec.k @@ -91,6 +91,7 @@ _:Map #hashedLocation("Solidity", 2, CALLER_ID SPENDER) |-> INIT_VALUE _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/hkg/balanceOf-spec.k b/tests/specs/erc20/hkg/balanceOf-spec.k index c0f6244ea4..41ad3508d0 100644 --- a/tests/specs/erc20/hkg/balanceOf-spec.k +++ b/tests/specs/erc20/hkg/balanceOf-spec.k @@ -90,6 +90,7 @@ module BALANCEOF-SPEC _:Map _ _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/hkg/totalSupply-spec.k b/tests/specs/erc20/hkg/totalSupply-spec.k index 43d91e65e1..0e72b094e8 100644 --- a/tests/specs/erc20/hkg/totalSupply-spec.k +++ b/tests/specs/erc20/hkg/totalSupply-spec.k @@ -89,6 +89,7 @@ module TOTALSUPPLY-SPEC _:Map _ _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/hkg/transfer-failure-1-spec.k b/tests/specs/erc20/hkg/transfer-failure-1-spec.k index b16ee11a8d..85930aa450 100644 --- a/tests/specs/erc20/hkg/transfer-failure-1-spec.k +++ b/tests/specs/erc20/hkg/transfer-failure-1-spec.k @@ -93,6 +93,7 @@ _:Map #hashedLocation("Solidity", 1, TO_ID) |-> BAL_TO _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/hkg/transfer-failure-2-spec.k b/tests/specs/erc20/hkg/transfer-failure-2-spec.k index b8156fac9e..94a111efb4 100644 --- a/tests/specs/erc20/hkg/transfer-failure-2-spec.k +++ b/tests/specs/erc20/hkg/transfer-failure-2-spec.k @@ -90,6 +90,7 @@ module TRANSFER-FAILURE-2-SPEC _:Map _ _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/hkg/transfer-success-1-spec.k b/tests/specs/erc20/hkg/transfer-success-1-spec.k index fa42355f81..000f1f568e 100644 --- a/tests/specs/erc20/hkg/transfer-success-1-spec.k +++ b/tests/specs/erc20/hkg/transfer-success-1-spec.k @@ -93,6 +93,7 @@ _:Map #hashedLocation("Solidity", 1, TO_ID) |-> BAL_TO _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/hkg/transfer-success-2-spec.k b/tests/specs/erc20/hkg/transfer-success-2-spec.k index 46441b1347..72e8c7aa35 100644 --- a/tests/specs/erc20/hkg/transfer-success-2-spec.k +++ b/tests/specs/erc20/hkg/transfer-success-2-spec.k @@ -91,6 +91,7 @@ _:Map #hashedLocation("Solidity", 1, CALLER_ID) |-> BAL_FROM _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/hkg/transferFrom-failure-1-spec.k b/tests/specs/erc20/hkg/transferFrom-failure-1-spec.k index 4bef9b5071..878c48a2a8 100644 --- a/tests/specs/erc20/hkg/transferFrom-failure-1-spec.k +++ b/tests/specs/erc20/hkg/transferFrom-failure-1-spec.k @@ -95,6 +95,7 @@ _:Map #hashedLocation("Solidity", 2, FROM_ID CALLER_ID) |-> ALLOW _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/hkg/transferFrom-failure-2-spec.k b/tests/specs/erc20/hkg/transferFrom-failure-2-spec.k index e512c5bb8f..418f194796 100644 --- a/tests/specs/erc20/hkg/transferFrom-failure-2-spec.k +++ b/tests/specs/erc20/hkg/transferFrom-failure-2-spec.k @@ -92,6 +92,7 @@ _:Map _ _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/hkg/transferFrom-success-1-spec.k b/tests/specs/erc20/hkg/transferFrom-success-1-spec.k index d21d9d6839..8dc6a16a99 100644 --- a/tests/specs/erc20/hkg/transferFrom-success-1-spec.k +++ b/tests/specs/erc20/hkg/transferFrom-success-1-spec.k @@ -95,6 +95,7 @@ _:Map #hashedLocation("Solidity", 2, FROM_ID CALLER_ID) |-> ALLOW _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/erc20/hkg/transferFrom-success-2-spec.k b/tests/specs/erc20/hkg/transferFrom-success-2-spec.k index 8b11c0f281..896a9acec5 100644 --- a/tests/specs/erc20/hkg/transferFrom-success-2-spec.k +++ b/tests/specs/erc20/hkg/transferFrom-success-2-spec.k @@ -93,6 +93,7 @@ _:Map #hashedLocation("Solidity", 2, FROM_ID CALLER_ID) |-> ALLOW _:Map _ + _ // ... // TODO: fix diff --git a/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k index 1c63306b7a..6339907705 100644 --- a/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k +++ b/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k @@ -94,6 +94,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW-0-SPEC 2 + + .Map + ) ) ) ... 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 4b4b5dbbfa..243d0bacc9 100644 --- a/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k +++ b/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k @@ -94,6 +94,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW_FAIL-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW_FAIL-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW_FAIL-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW_FAIL-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW_FAIL-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW_FAIL-0-SPEC 2 + + .Map + ) ) ) ... diff --git a/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k index 547ecdac68..eacc2cd323 100644 --- a/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k +++ b/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k @@ -94,6 +94,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCALLSTOADDRESS-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCALLSTOADDRESS-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCALLSTOADDRESS-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCALLSTOADDRESS-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCALLSTOADDRESS-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCALLSTOADDRESS-0-SPEC 2 + + .Map + ) ) ) ... diff --git a/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k index 766492f68a..93422249af 100644 --- a/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k +++ b/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k @@ -94,6 +94,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC 2 + + .Map + ) ) ) ... @@ -401,6 +419,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -421,6 +442,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC 2 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -440,6 +464,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC 0 + + .Map + @@ -460,6 +487,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC 3 + + .Map + ) ) ) | @@ -575,6 +605,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC 1 + + .Map + ( @@ -595,6 +628,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -615,6 +651,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC 2 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -634,6 +673,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC 0 + + .Map + @@ -654,6 +696,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC 3 + + .Map + ) ) ) ) ... 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 dab02dae0e..387aea25f9 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 @@ -119,6 +119,9 @@ module TEST-ARITHMETICTEST-TEST_MAX1_BROKEN-UINT256-UINT256-0-SPEC 0 + + .Map + @@ -139,6 +142,9 @@ module TEST-ARITHMETICTEST-TEST_MAX1_BROKEN-UINT256-UINT256-0-SPEC 1 + + .Map + ) ... diff --git a/tests/specs/kontrol/test-arithmetictest-test_wdiv_rounding-uint256-uint256-0-spec.k b/tests/specs/kontrol/test-arithmetictest-test_wdiv_rounding-uint256-uint256-0-spec.k index 0f02b58ee5..fbbb94d683 100644 --- a/tests/specs/kontrol/test-arithmetictest-test_wdiv_rounding-uint256-uint256-0-spec.k +++ b/tests/specs/kontrol/test-arithmetictest-test_wdiv_rounding-uint256-uint256-0-spec.k @@ -113,6 +113,9 @@ module TEST-ARITHMETICTEST-TEST_WDIV_ROUNDING-UINT256-UINT256-0-SPEC 0 + + .Map + @@ -133,6 +136,9 @@ module TEST-ARITHMETICTEST-TEST_WDIV_ROUNDING-UINT256-UINT256-0-SPEC 1 + + .Map + ) ... diff --git a/tests/specs/kontrol/test-arithmetictest-test_wmul_weakly_increasing_positive-uint256-uint256-0-spec.k b/tests/specs/kontrol/test-arithmetictest-test_wmul_weakly_increasing_positive-uint256-uint256-0-spec.k index d7dcc24c51..3c5f047c50 100644 --- a/tests/specs/kontrol/test-arithmetictest-test_wmul_weakly_increasing_positive-uint256-uint256-0-spec.k +++ b/tests/specs/kontrol/test-arithmetictest-test_wmul_weakly_increasing_positive-uint256-uint256-0-spec.k @@ -113,6 +113,9 @@ module TEST-ARITHMETICTEST-TEST_WMUL_WEAKLY_INCREASING_POSITIVE-UINT256-UINT256- 0 + + .Map + @@ -133,6 +136,9 @@ module TEST-ARITHMETICTEST-TEST_WMUL_WEAKLY_INCREASING_POSITIVE-UINT256-UINT256- 1 + + .Map + ) ... @@ -266,6 +272,9 @@ module TEST-ARITHMETICTEST-TEST_WMUL_WEAKLY_INCREASING_POSITIVE-UINT256-UINT256- 0 + + .Map + @@ -286,6 +295,9 @@ module TEST-ARITHMETICTEST-TEST_WMUL_WEAKLY_INCREASING_POSITIVE-UINT256-UINT256- 1 + + .Map + ) ... diff --git a/tests/specs/kontrol/test-countertest-testincrement-0-spec.k b/tests/specs/kontrol/test-countertest-testincrement-0-spec.k index c47ff94a6a..242031be60 100644 --- a/tests/specs/kontrol/test-countertest-testincrement-0-spec.k +++ b/tests/specs/kontrol/test-countertest-testincrement-0-spec.k @@ -94,6 +94,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 2 + + .Map + ) ) ) ... @@ -403,6 +421,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 1 + + .Map + ( @@ -423,6 +444,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 0 + + .Map + @@ -443,6 +467,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 2 + + .Map + ) ) | @@ -562,6 +589,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 1 + + .Map + ( @@ -582,6 +612,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 0 + + .Map + @@ -602,6 +635,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 2 + + .Map + ) ) ... @@ -713,6 +749,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 1 + + .Map + ( @@ -733,6 +772,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 0 + + .Map + @@ -753,6 +795,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 2 + + .Map + ) ) | @@ -872,6 +917,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 1 + + .Map + ( @@ -892,6 +940,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 0 + + .Map + @@ -912,6 +963,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC 2 + + .Map + ) ) ... diff --git a/tests/specs/kontrol/test-emitcontracttest-testexpectemit-0-spec.k b/tests/specs/kontrol/test-emitcontracttest-testexpectemit-0-spec.k index e6041ef404..0d2b6fce68 100644 --- a/tests/specs/kontrol/test-emitcontracttest-testexpectemit-0-spec.k +++ b/tests/specs/kontrol/test-emitcontracttest-testexpectemit-0-spec.k @@ -94,6 +94,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMIT-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMIT-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMIT-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMIT-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMIT-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMIT-0-SPEC 2 + + .Map + ) ) ) ... diff --git a/tests/specs/kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k b/tests/specs/kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k index 1c3391f7d8..10071c2745 100644 --- a/tests/specs/kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k +++ b/tests/specs/kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k @@ -94,6 +94,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITCHECKEMITTER-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITCHECKEMITTER-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITCHECKEMITTER-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITCHECKEMITTER-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITCHECKEMITTER-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITCHECKEMITTER-0-SPEC 2 + + .Map + ) ) ) ... diff --git a/tests/specs/kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k b/tests/specs/kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k index f066f645f2..fefa3508a7 100644 --- a/tests/specs/kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k +++ b/tests/specs/kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k @@ -94,6 +94,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITDONOTCHECKDATA-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITDONOTCHECKDATA-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITDONOTCHECKDATA-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITDONOTCHECKDATA-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITDONOTCHECKDATA-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITDONOTCHECKDATA-0-SPEC 2 + + .Map + ) ) ) ... diff --git a/tests/specs/kontrol/test-expectcalltest-testexpectregularcall-0-spec.k b/tests/specs/kontrol/test-expectcalltest-testexpectregularcall-0-spec.k index 7524c5b8b9..00245de39e 100644 --- a/tests/specs/kontrol/test-expectcalltest-testexpectregularcall-0-spec.k +++ b/tests/specs/kontrol/test-expectcalltest-testexpectregularcall-0-spec.k @@ -94,6 +94,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTREGULARCALL-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTREGULARCALL-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTREGULARCALL-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTREGULARCALL-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTREGULARCALL-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTREGULARCALL-0-SPEC 2 + + .Map + ) ) ) ... diff --git a/tests/specs/kontrol/test-expectcalltest-testexpectstaticcall-0-spec.k b/tests/specs/kontrol/test-expectcalltest-testexpectstaticcall-0-spec.k index b7431618d5..f5c6165f7a 100644 --- a/tests/specs/kontrol/test-expectcalltest-testexpectstaticcall-0-spec.k +++ b/tests/specs/kontrol/test-expectcalltest-testexpectstaticcall-0-spec.k @@ -94,6 +94,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTSTATICCALL-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTSTATICCALL-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTSTATICCALL-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTSTATICCALL-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTSTATICCALL-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTSTATICCALL-0-SPEC 2 + + .Map + ) ) ) ... 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 e781ffce34..2fbb8eb869 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 @@ -94,6 +94,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC 2 + + .Map + ) ) ) ... @@ -399,6 +417,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC 0 + + .Map + @@ -419,6 +440,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC 2 + + .Map + ) | @@ -536,6 +560,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC 1 + + .Map + ( @@ -556,6 +583,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC 0 + + .Map + @@ -576,6 +606,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC 2 + + .Map + ) ) ... 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 c734325212..59c6d2c45c 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 @@ -94,6 +94,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_MESSAGE-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_MESSAGE-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_MESSAGE-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_MESSAGE-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_MESSAGE-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_MESSAGE-0-SPEC 2 + + .Map + ) ) ) ... 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 d38cf61064..fbd3d49843 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 @@ -94,6 +94,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_RETURNVALUE-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_RETURNVALUE-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_RETURNVALUE-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_RETURNVALUE-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_RETURNVALUE-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_RETURNVALUE-0-SPEC 2 + + .Map + ) ) ) ... 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 7f22e03bbf..e50b45ce4c 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 @@ -94,6 +94,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_BYTES4-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_BYTES4-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_BYTES4-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_BYTES4-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_BYTES4-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_BYTES4-0-SPEC 2 + + .Map + ) ) ) ... 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 0a512b16d0..9eafd13acd 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 @@ -94,6 +94,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FAILANDSUCCESS-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FAILANDSUCCESS-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FAILANDSUCCESS-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FAILANDSUCCESS-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FAILANDSUCCESS-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FAILANDSUCCESS-0-SPEC 2 + + .Map + ) ) ) ... 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 90d06ab658..72972087f4 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 @@ -94,6 +94,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC 2 + + .Map + ) ) ) ... @@ -427,6 +445,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC 1 + + .Map + ( @@ -447,6 +468,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC 0 + + .Map + @@ -467,6 +491,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC 2 + + .Map + ) ) ... diff --git a/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k b/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k index 06c76cdae6..88a5157ab4 100644 --- a/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k +++ b/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k @@ -94,6 +94,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC 2 + + .Map + ) ) ) ... @@ -401,6 +419,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC 1 + + .Map + ( @@ -421,6 +442,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC 0 + + .Map + @@ -441,6 +465,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC 2 + + .Map + ) ) | @@ -551,6 +578,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC 1 + + .Map + ( @@ -571,6 +601,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC 0 + + .Map + @@ -591,6 +624,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC 2 + + .Map + ) ) ... 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 7ccde5a34f..eda0aceb42 100644 --- a/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k +++ b/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k @@ -94,6 +94,9 @@ module TEST-SAFETEST-TESTWITHDRAWFUZZ-UINT96-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-SAFETEST-TESTWITHDRAWFUZZ-UINT96-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-SAFETEST-TESTWITHDRAWFUZZ-UINT96-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-SAFETEST-TESTWITHDRAWFUZZ-UINT96-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-SAFETEST-TESTWITHDRAWFUZZ-UINT96-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-SAFETEST-TESTWITHDRAWFUZZ-UINT96-0-SPEC 2 + + .Map + ) ) ) ... diff --git a/tests/specs/kontrol/test-storetest-testaccesses-0-spec.k b/tests/specs/kontrol/test-storetest-testaccesses-0-spec.k index cb9d7fd463..5cc0c575f8 100644 --- a/tests/specs/kontrol/test-storetest-testaccesses-0-spec.k +++ b/tests/specs/kontrol/test-storetest-testaccesses-0-spec.k @@ -94,6 +94,9 @@ module TEST-STORETEST-TESTACCESSES-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-STORETEST-TESTACCESSES-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-STORETEST-TESTACCESSES-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-STORETEST-TESTACCESSES-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-STORETEST-TESTACCESSES-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-STORETEST-TESTACCESSES-0-SPEC 2 + + .Map + ) ) ) ... diff --git a/tests/specs/kontrol/test-storetest-teststoreload-0-spec.k b/tests/specs/kontrol/test-storetest-teststoreload-0-spec.k index ccc43eafbf..f7268914a9 100644 --- a/tests/specs/kontrol/test-storetest-teststoreload-0-spec.k +++ b/tests/specs/kontrol/test-storetest-teststoreload-0-spec.k @@ -94,6 +94,9 @@ module TEST-STORETEST-TESTSTORELOAD-0-SPEC 0 + + .Map + @@ -114,6 +117,9 @@ module TEST-STORETEST-TESTSTORELOAD-0-SPEC 2 + + .Map + ) | @@ -231,6 +237,9 @@ module TEST-STORETEST-TESTSTORELOAD-0-SPEC ( 0 => 1 ) + + .Map + ( @@ -251,6 +260,9 @@ module TEST-STORETEST-TESTSTORELOAD-0-SPEC 1 + + .Map + => ( 645326474426547203313410069153905908525362434349 @@ -270,6 +282,9 @@ module TEST-STORETEST-TESTSTORELOAD-0-SPEC 0 + + .Map + @@ -290,6 +305,9 @@ module TEST-STORETEST-TESTSTORELOAD-0-SPEC 2 + + .Map + ) ) ) ... 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 2f6cc994a8..5ad8f93d1b 100644 --- a/tests/specs/mcd/cat-file-addr-pass-rough-spec.k +++ b/tests/specs/mcd/cat-file-addr-pass-rough-spec.k @@ -76,6 +76,7 @@ module CAT-FILE-ADDR-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Cat.vow <- ABI_data ] ACCT_ID_ORIG_STORAGE Nonce_Cat + _ ... diff --git a/tests/specs/mcd/dai-adduu-fail-rough-spec.k b/tests/specs/mcd/dai-adduu-fail-rough-spec.k index ad5206e722..c566bd4007 100644 --- a/tests/specs/mcd/dai-adduu-fail-rough-spec.k +++ b/tests/specs/mcd/dai-adduu-fail-rough-spec.k @@ -76,6 +76,7 @@ module DAI-ADDUU-FAIL-ROUGH-SPEC ACCT_ID_STORAGE => ?_ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_Dai + _ ... diff --git a/tests/specs/mcd/dai-symbol-pass-spec.k b/tests/specs/mcd/dai-symbol-pass-spec.k index 0b0205fc26..4af11a26fc 100644 --- a/tests/specs/mcd/dai-symbol-pass-spec.k +++ b/tests/specs/mcd/dai-symbol-pass-spec.k @@ -76,6 +76,7 @@ module DAI-SYMBOL-PASS-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE _Nonce_Dai => ?_ + _ ... diff --git a/tests/specs/mcd/dstoken-approve-fail-rough-spec.k b/tests/specs/mcd/dstoken-approve-fail-rough-spec.k index c087f1c751..27748067b8 100644 --- a/tests/specs/mcd/dstoken-approve-fail-rough-spec.k +++ b/tests/specs/mcd/dstoken-approve-fail-rough-spec.k @@ -76,6 +76,7 @@ module DSTOKEN-APPROVE-FAIL-ROUGH-SPEC ACCT_ID_STORAGE => ?_ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE _Nonce_DSToken => ?_ + _ ... diff --git a/tests/specs/mcd/dsvalue-peek-pass-rough-spec.k b/tests/specs/mcd/dsvalue-peek-pass-rough-spec.k index 09bee5bdae..7210d407a1 100644 --- a/tests/specs/mcd/dsvalue-peek-pass-rough-spec.k +++ b/tests/specs/mcd/dsvalue-peek-pass-rough-spec.k @@ -76,6 +76,7 @@ module DSVALUE-PEEK-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE _Nonce_DSValue => ?_ + _ ... diff --git a/tests/specs/mcd/dsvalue-read-pass-spec.k b/tests/specs/mcd/dsvalue-read-pass-spec.k index 7418183fa1..192d755369 100644 --- a/tests/specs/mcd/dsvalue-read-pass-spec.k +++ b/tests/specs/mcd/dsvalue-read-pass-spec.k @@ -76,6 +76,7 @@ module DSVALUE-READ-PASS-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_DSValue + _ ... diff --git a/tests/specs/mcd/end-cash-pass-rough-spec.k b/tests/specs/mcd/end-cash-pass-rough-spec.k index 4449b94b44..b00150ae6e 100644 --- a/tests/specs/mcd/end-cash-pass-rough-spec.k +++ b/tests/specs/mcd/end-cash-pass-rough-spec.k @@ -76,6 +76,7 @@ module END-CASH-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #End.out[ABI_ilk][CALLER_ID] <- Out +Int ABI_wad ] ACCT_ID_ORIG_STORAGE Nonce_End + _ Vat @@ -84,6 +85,7 @@ module END-CASH-PASS-ROUGH-SPEC Vat_STORAGE => Vat_STORAGE [ #Vat.gem[ABI_ilk][ACCT_ID] <- Gem_e -Int #rmul(ABI_wad, Fix) ] [ #Vat.gem[ABI_ilk][CALLER_ID] <- Gem_c +Int #rmul(ABI_wad, Fix) ] Vat_ORIG_STORAGE Nonce_Vat + _ ... @@ -232,6 +234,7 @@ module END-CASH-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_End + _ ... @@ -338,6 +341,7 @@ module END-CASH-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_End + _ ... @@ -441,6 +445,7 @@ module END-CASH-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.gem[ABI_ilk][ABI_src] <- Gem_src -Int ABI_wad ] [ #Vat.gem[ABI_ilk][ABI_dst] <- Gem_dst +Int ABI_wad ] ACCT_ID_ORIG_STORAGE Nonce_Vat + _ ... diff --git a/tests/specs/mcd/end-pack-pass-rough-spec.k b/tests/specs/mcd/end-pack-pass-rough-spec.k index 77a56c05c6..116594a1c9 100644 --- a/tests/specs/mcd/end-pack-pass-rough-spec.k +++ b/tests/specs/mcd/end-pack-pass-rough-spec.k @@ -76,6 +76,7 @@ module END-PACK-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #End.bag[CALLER_ID] <- Bag +Int ABI_wad ] ACCT_ID_ORIG_STORAGE Nonce_End + _ Vat @@ -84,6 +85,7 @@ module END-PACK-PASS-ROUGH-SPEC Vat_STORAGE => Vat_STORAGE [ #Vat.dai[CALLER_ID] <- Dai -Int ABI_wad *Int #Ray ] [ #Vat.dai[Vow] <- Joy +Int ABI_wad *Int #Ray ] Vat_ORIG_STORAGE Nonce_Vat + _ ... @@ -237,6 +239,7 @@ module END-PACK-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE _ACCT_ID_ORIG_STORAGE Nonce_End + _ ... @@ -340,6 +343,7 @@ module END-PACK-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE _ACCT_ID_ORIG_STORAGE Nonce_End + _ ... @@ -443,6 +447,7 @@ module END-PACK-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.dai[ABI_src] <- Dai_src -Int ABI_rad ] [ #Vat.dai[ABI_dst] <- Dai_dst +Int ABI_rad ] ACCT_ID_ORIG_STORAGE Nonce_Vat + _ ... diff --git a/tests/specs/mcd/end-subuu-pass-spec.k b/tests/specs/mcd/end-subuu-pass-spec.k index d44f3a6a17..c6ad53ce58 100644 --- a/tests/specs/mcd/end-subuu-pass-spec.k +++ b/tests/specs/mcd/end-subuu-pass-spec.k @@ -76,6 +76,7 @@ module END-SUBUU-PASS-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE _ACCT_ID_ORIG_STORAGE _Nonce_End => ?_ + _ ... diff --git a/tests/specs/mcd/flapper-yank-pass-rough-spec.k b/tests/specs/mcd/flapper-yank-pass-rough-spec.k index 7ecc30a186..b13c85d850 100644 --- a/tests/specs/mcd/flapper-yank-pass-rough-spec.k +++ b/tests/specs/mcd/flapper-yank-pass-rough-spec.k @@ -76,6 +76,7 @@ module FLAPPER-YANK-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Flapper.bids[ABI_id].bid <- 0 ] [ #Flapper.bids[ABI_id].lot <- 0 ] [ #Flapper.bids[ABI_id].guy_tic_end <- 0 ] ACCT_ID_ORIG_STORAGE Nonce_Flapper + _ DSToken @@ -84,6 +85,7 @@ module FLAPPER-YANK-PASS-ROUGH-SPEC DSToken_STORAGE => DSToken_STORAGE [ #DSToken.balances[ACCT_ID] <- Gem_a -Int Bid ] [ #DSToken.balances[Guy] <- Gem_g +Int Bid ] DSToken_ORIG_STORAGE Nonce_DSToken + _ ... @@ -247,6 +249,7 @@ module FLAPPER-YANK-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #DSToken.allowance[ABI_src][CALLER_ID] <- #if (ABI_src ==Int CALLER_ID orBool Allowance ==Int maxUInt256) #then Allowance #else Allowance -Int ABI_wad #fi ] [ #DSToken.balances[ABI_src] <- Gem_s -Int ABI_wad ] [ #DSToken.balances[ABI_dst] <- Gem_d +Int ABI_wad ] ACCT_ID_ORIG_STORAGE Nonce_DSToken + _ ... diff --git a/tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k b/tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k index c3d4894a1f..6b03538888 100644 --- a/tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k +++ b/tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k @@ -76,6 +76,7 @@ module FLIPPER-ADDU48U48-FAIL-ROUGH-SPEC ACCT_ID_STORAGE => ?_ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_Flipper + _ ... diff --git a/tests/specs/mcd/flipper-bids-pass-rough-spec.k b/tests/specs/mcd/flipper-bids-pass-rough-spec.k index d86e88e00a..566e8ef1e0 100644 --- a/tests/specs/mcd/flipper-bids-pass-rough-spec.k +++ b/tests/specs/mcd/flipper-bids-pass-rough-spec.k @@ -76,6 +76,7 @@ module FLIPPER-BIDS-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE _Nonce_Flipper => ?_ + _ ... diff --git a/tests/specs/mcd/flipper-tau-pass-spec.k b/tests/specs/mcd/flipper-tau-pass-spec.k index 830bc45801..086a42b96a 100644 --- a/tests/specs/mcd/flipper-tau-pass-spec.k +++ b/tests/specs/mcd/flipper-tau-pass-spec.k @@ -76,6 +76,7 @@ module FLIPPER-TAU-PASS-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_Flipper + _ ... diff --git a/tests/specs/mcd/flipper-ttl-pass-spec.k b/tests/specs/mcd/flipper-ttl-pass-spec.k index 0bcf84bddb..ce0c668aae 100644 --- a/tests/specs/mcd/flipper-ttl-pass-spec.k +++ b/tests/specs/mcd/flipper-ttl-pass-spec.k @@ -76,6 +76,7 @@ module FLIPPER-TTL-PASS-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE _Nonce_Flipper => ?_ + _ ... diff --git a/tests/specs/mcd/flopper-cage-pass-spec.k b/tests/specs/mcd/flopper-cage-pass-spec.k index 4bf657b6e4..0d02f1c751 100644 --- a/tests/specs/mcd/flopper-cage-pass-spec.k +++ b/tests/specs/mcd/flopper-cage-pass-spec.k @@ -75,6 +75,7 @@ module FLOPPER-CAGE-PASS-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Flopper.live <- 0 ] [ #Flopper.vow <- CALLER_ID ] ACCT_ID_ORIG_STORAGE _Nonce_Flopper => ?_ + _ ... 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 8d67f27f9f..9f57d585af 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 @@ -76,6 +76,7 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Flopper.bids[ABI_id].lot <- ABI_lot ] [ #Flopper.bids[ABI_id].guy_tic_end <- #WordPackAddrUInt48UInt48(CALLER_ID, TIME +Int Ttl, End) ] ACCT_ID_ORIG_STORAGE Nonce_Flopper + _ Vat @@ -84,6 +85,7 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC Vat_STORAGE => Vat_STORAGE [ #Vat.dai[CALLER_ID] <- Dai_a -Int ABI_bid ] [ #Vat.dai[Guy] <- Dai_g +Int ABI_bid ] Vat_ORIG_STORAGE Nonce_Vat + _ ... @@ -277,6 +279,7 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE _ACCT_ID_ORIG_STORAGE Nonce_Flopper + _ ... @@ -380,6 +383,7 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE _ACCT_ID_ORIG_STORAGE Nonce_Flopper + _ ... @@ -482,6 +486,7 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.dai[ABI_src] <- Dai_src -Int ABI_rad ] [ #Vat.dai[ABI_dst] <- Dai_dst +Int ABI_rad ] ACCT_ID_ORIG_STORAGE Nonce_Vat + _ ... 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 823c82a4e3..0ec581f240 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 @@ -76,6 +76,7 @@ module FLOPPER-DENT-GUY-SAME-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Flopper.bids[ABI_id].lot <- ABI_lot ] [ #Flopper.bids[ABI_id].guy_tic_end <- #WordPackAddrUInt48UInt48(Guy, TIME +Int Ttl, End) ] ACCT_ID_ORIG_STORAGE _Nonce_Flopper => ?_ + _ ... @@ -244,6 +245,7 @@ module FLOPPER-DENT-GUY-SAME-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE _Nonce_Flopper => ?_ + _ ... @@ -346,6 +348,7 @@ module FLOPPER-DENT-GUY-SAME-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE _Nonce_Flopper => ?_ + _ ... diff --git a/tests/specs/mcd/flopper-file-pass-rough-spec.k b/tests/specs/mcd/flopper-file-pass-rough-spec.k index 296a4c3b56..7395af44f2 100644 --- a/tests/specs/mcd/flopper-file-pass-rough-spec.k +++ b/tests/specs/mcd/flopper-file-pass-rough-spec.k @@ -76,6 +76,7 @@ module FLOPPER-FILE-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Flopper.beg <- (#if ABI_what ==Int #string2Word("beg") #then ABI_data #else Beg #fi) ] [ #Flopper.pad <- (#if ABI_what ==Int #string2Word("pad") #then ABI_data #else Pad #fi) ] [ #Flopper.ttl_tau <- (#if ABI_what ==Int #string2Word("ttl") #then #WordPackUInt48UInt48(maxUInt48 &Int ABI_data, Tau) #else (#if ABI_what ==Int #string2Word("tau") #then #WordPackUInt48UInt48(Ttl, maxUInt48 &Int ABI_data) #else #WordPackUInt48UInt48(Ttl, Tau) #fi) #fi) ] ACCT_ID_ORIG_STORAGE _Nonce_Flopper => ?_ + _ ... diff --git a/tests/specs/mcd/flopper-kick-pass-rough-spec.k b/tests/specs/mcd/flopper-kick-pass-rough-spec.k index 55fcf832c4..30f3a71fa2 100644 --- a/tests/specs/mcd/flopper-kick-pass-rough-spec.k +++ b/tests/specs/mcd/flopper-kick-pass-rough-spec.k @@ -76,6 +76,7 @@ module FLOPPER-KICK-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Flopper.kicks <- 1 +Int Kicks ] [ #Flopper.bids[1 +Int Kicks].bid <- ABI_bid ] [ #Flopper.bids[1 +Int Kicks].lot <- ABI_lot ] [ #Flopper.bids[1 +Int Kicks].guy_tic_end <- #WordPackAddrUInt48UInt48(ABI_gal, Old_tic, TIME +Int Tau) ] ACCT_ID_ORIG_STORAGE _Nonce_Flopper => ?_ + _ ... @@ -233,6 +234,7 @@ module FLOPPER-KICK-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE _Nonce_Flopper => ?_ + _ ... diff --git a/tests/specs/mcd/flopper-tick-pass-rough-spec.k b/tests/specs/mcd/flopper-tick-pass-rough-spec.k index 29382e2ecb..8bf1541993 100644 --- a/tests/specs/mcd/flopper-tick-pass-rough-spec.k +++ b/tests/specs/mcd/flopper-tick-pass-rough-spec.k @@ -76,6 +76,7 @@ module FLOPPER-TICK-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Flopper.bids[ABI_id].lot <- (Pad *Int Lot) /Int #Wad ] [ #Flopper.bids[ABI_id].guy_tic_end <- #WordPackAddrUInt48UInt48(Guy, Tic, TIME +Int Tau) ] ACCT_ID_ORIG_STORAGE _Nonce_Flopper => ?_ + _ ... @@ -204,6 +205,7 @@ module FLOPPER-TICK-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE _Nonce_Flopper => ?_ + _ ... diff --git a/tests/specs/mcd/pot-join-pass-rough-spec.k b/tests/specs/mcd/pot-join-pass-rough-spec.k index 7371eeee1c..a6fdaef7c4 100644 --- a/tests/specs/mcd/pot-join-pass-rough-spec.k +++ b/tests/specs/mcd/pot-join-pass-rough-spec.k @@ -76,6 +76,7 @@ module POT-JOIN-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Pot.pie[CALLER_ID] <- Pie_u +Int ABI_wad ] [ #Pot.Pie <- Pie_tot +Int ABI_wad ] ACCT_ID_ORIG_STORAGE Nonce_Pot + _ Vat @@ -84,6 +85,7 @@ module POT-JOIN-PASS-ROUGH-SPEC Vat_STORAGE => Vat_STORAGE [ #Vat.dai[CALLER_ID] <- Dai_u -Int Chi *Int ABI_wad ] [ #Vat.dai[ACCT_ID] <- Dai_p +Int Chi *Int ABI_wad ] Vat_ORIG_STORAGE Nonce_Vat + _ ... @@ -241,6 +243,7 @@ module POT-JOIN-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE _ACCT_ID_ORIG_STORAGE Nonce_Pot + _ ... @@ -347,6 +350,7 @@ module POT-JOIN-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE _ACCT_ID_ORIG_STORAGE Nonce_Pot + _ ... @@ -450,6 +454,7 @@ module POT-JOIN-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.dai[ABI_src] <- Dai_src -Int ABI_rad ] [ #Vat.dai[ABI_dst] <- Dai_dst +Int ABI_rad ] ACCT_ID_ORIG_STORAGE Nonce_Vat + _ ... diff --git a/tests/specs/mcd/vat-addui-fail-rough-spec.k b/tests/specs/mcd/vat-addui-fail-rough-spec.k index f827d3ab65..8518a6f30a 100644 --- a/tests/specs/mcd/vat-addui-fail-rough-spec.k +++ b/tests/specs/mcd/vat-addui-fail-rough-spec.k @@ -76,6 +76,7 @@ module VAT-ADDUI-FAIL-ROUGH-SPEC ACCT_ID_STORAGE => ?_ACCT_ID_STORAGE _ACCT_ID_ORIG_STORAGE Nonce_Vat + _ ... diff --git a/tests/specs/mcd/vat-dai-pass-spec.k b/tests/specs/mcd/vat-dai-pass-spec.k index 7d67b3c3a1..0eefc764fa 100644 --- a/tests/specs/mcd/vat-dai-pass-spec.k +++ b/tests/specs/mcd/vat-dai-pass-spec.k @@ -75,6 +75,7 @@ module VAT-DAI-PASS-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_Vat + _ ... 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 e201760c1a..c68578f74f 100644 --- a/tests/specs/mcd/vat-deny-diff-fail-rough-spec.k +++ b/tests/specs/mcd/vat-deny-diff-fail-rough-spec.k @@ -76,6 +76,7 @@ module VAT-DENY-DIFF-FAIL-ROUGH-SPEC ACCT_ID_STORAGE => ?_ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_Vat + _ ... 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 40c7e94e44..308e20dd64 100644 --- a/tests/specs/mcd/vat-flux-diff-pass-rough-spec.k +++ b/tests/specs/mcd/vat-flux-diff-pass-rough-spec.k @@ -77,6 +77,7 @@ module VAT-FLUX-DIFF-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.gem[ABI_ilk][ABI_src] <- Gem_src -Int ABI_wad ] [ #Vat.gem[ABI_ilk][ABI_dst] <- Gem_dst +Int ABI_wad ] ACCT_ID_ORIG_STORAGE _Nonce_Vat => ?_ + _ ... diff --git a/tests/specs/mcd/vat-flux-diff-pass-spec.k b/tests/specs/mcd/vat-flux-diff-pass-spec.k index 270580b0d5..9de7d4843c 100644 --- a/tests/specs/mcd/vat-flux-diff-pass-spec.k +++ b/tests/specs/mcd/vat-flux-diff-pass-spec.k @@ -75,6 +75,7 @@ module VAT-FLUX-DIFF-PASS-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.gem[ABI_ilk][ABI_src] <- Gem_src -Int ABI_wad ] [ #Vat.gem[ABI_ilk][ABI_dst] <- Gem_dst +Int ABI_wad ] ACCT_ID_ORIG_STORAGE Nonce_Vat + _ ... diff --git a/tests/specs/mcd/vat-fold-pass-rough-spec.k b/tests/specs/mcd/vat-fold-pass-rough-spec.k index d36fabfa9d..0c738ac7b4 100644 --- a/tests/specs/mcd/vat-fold-pass-rough-spec.k +++ b/tests/specs/mcd/vat-fold-pass-rough-spec.k @@ -78,6 +78,7 @@ module VAT-FOLD-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.ilks[ABI_i].rate <- Rate_i +Int ABI_rate ] [ #Vat.dai[ABI_u] <- Dai_u +Int Art_i *Int ABI_rate ] [ #Vat.debt <- Debt +Int Art_i *Int ABI_rate ] ACCT_ID_ORIG_STORAGE _Nonce_Vat => ?_ + _ ... 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 ac72f77811..7a1a3942e0 100644 --- a/tests/specs/mcd/vat-fork-diff-pass-rough-spec.k +++ b/tests/specs/mcd/vat-fork-diff-pass-rough-spec.k @@ -78,6 +78,7 @@ module VAT-FORK-DIFF-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.urns[ABI_ilk][ABI_src].ink <- Ink_u -Int ABI_dink ] [ #Vat.urns[ABI_ilk][ABI_src].art <- Art_u -Int ABI_dart ] [ #Vat.urns[ABI_ilk][ABI_dst].ink <- Ink_v +Int ABI_dink ] [ #Vat.urns[ABI_ilk][ABI_dst].art <- Art_v +Int ABI_dart ] ACCT_ID_ORIG_STORAGE _Nonce_Vat => ?_ + _ ... 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 8ab8af36c0..b0162c6a7c 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 @@ -78,6 +78,7 @@ module VAT-FROB-DIFF-ZERO-DART-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.gem[ABI_i][ABI_v] <- Gem_iv -Int ABI_dink ] [ #Vat.urns[ABI_i][ABI_u].ink <- Urn_ink +Int ABI_dink ] ACCT_ID_ORIG_STORAGE _Nonce_Vat => ?_ + _ ... diff --git a/tests/specs/mcd/vat-heal-pass-spec.k b/tests/specs/mcd/vat-heal-pass-spec.k index 3cfac33aab..6f7a95133d 100644 --- a/tests/specs/mcd/vat-heal-pass-spec.k +++ b/tests/specs/mcd/vat-heal-pass-spec.k @@ -75,6 +75,7 @@ module VAT-HEAL-PASS-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.sin[CALLER_ID] <- Sin -Int ABI_rad ] [ #Vat.dai[CALLER_ID] <- Dai -Int ABI_rad ] [ #Vat.vice <- Vice -Int ABI_rad ] [ #Vat.debt <- Debt -Int ABI_rad ] ACCT_ID_ORIG_STORAGE Nonce_Vat + _ ... diff --git a/tests/specs/mcd/vat-move-diff-rough-spec.k b/tests/specs/mcd/vat-move-diff-rough-spec.k index 22e0ebc562..7a2640d0b4 100644 --- a/tests/specs/mcd/vat-move-diff-rough-spec.k +++ b/tests/specs/mcd/vat-move-diff-rough-spec.k @@ -79,6 +79,7 @@ module VAT-MOVE-DIFF-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.dai[ABI_src] <- Dai_src -Int ABI_rad ] [ #Vat.dai[ABI_dst] <- Dai_dst +Int ABI_rad ] ACCT_ID_ORIG_STORAGE Nonce_Vat + _ ... diff --git a/tests/specs/mcd/vat-sin-pass-spec.k b/tests/specs/mcd/vat-sin-pass-spec.k index fcf1b10c3a..a0dbe0122c 100644 --- a/tests/specs/mcd/vat-sin-pass-spec.k +++ b/tests/specs/mcd/vat-sin-pass-spec.k @@ -75,6 +75,7 @@ module VAT-SIN-PASS-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_Vat + _ ... diff --git a/tests/specs/mcd/vat-slip-pass-rough-spec.k b/tests/specs/mcd/vat-slip-pass-rough-spec.k index bec3496611..d3f8605a67 100644 --- a/tests/specs/mcd/vat-slip-pass-rough-spec.k +++ b/tests/specs/mcd/vat-slip-pass-rough-spec.k @@ -78,6 +78,7 @@ module VAT-SLIP-PASS-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.gem[ABI_ilk][ABI_usr] <- Gem +Int ABI_wad ] ACCT_ID_ORIG_STORAGE _Nonce_Vat => ?_ + _ ... diff --git a/tests/specs/mcd/vat-subui-fail-rough-spec.k b/tests/specs/mcd/vat-subui-fail-rough-spec.k index b79ae13953..9fd6f9827b 100644 --- a/tests/specs/mcd/vat-subui-fail-rough-spec.k +++ b/tests/specs/mcd/vat-subui-fail-rough-spec.k @@ -76,6 +76,7 @@ module VAT-SUBUI-FAIL-ROUGH-SPEC ACCT_ID_STORAGE => ?_ACCT_ID_STORAGE _ACCT_ID_ORIG_STORAGE Nonce_Vat + _ ... diff --git a/tests/specs/mcd/vow-fess-fail-rough-spec.k b/tests/specs/mcd/vow-fess-fail-rough-spec.k index 5786381399..10e58bd43a 100644 --- a/tests/specs/mcd/vow-fess-fail-rough-spec.k +++ b/tests/specs/mcd/vow-fess-fail-rough-spec.k @@ -76,6 +76,7 @@ module VOW-FESS-FAIL-ROUGH-SPEC ACCT_ID_STORAGE => ?_ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_Vow => ?_ + _ ... @@ -196,6 +197,7 @@ module VOW-FESS-FAIL-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_Vow => ?_ + _ ... diff --git a/tests/specs/mcd/vow-flog-fail-rough-spec.k b/tests/specs/mcd/vow-flog-fail-rough-spec.k index 7d0c4cf11b..98dfbfa8f5 100644 --- a/tests/specs/mcd/vow-flog-fail-rough-spec.k +++ b/tests/specs/mcd/vow-flog-fail-rough-spec.k @@ -76,6 +76,7 @@ module VOW-FLOG-FAIL-ROUGH-SPEC ACCT_ID_STORAGE => ?_ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_Vow => ?_ + _ ... @@ -196,6 +197,7 @@ module VOW-FLOG-FAIL-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_Vow => ?_ + _ ... @@ -299,6 +301,7 @@ module VOW-FLOG-FAIL-ROUGH-SPEC ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE Nonce_Vow => ?_ + _ ...