diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index a690ea6fd..90308fa61 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -20,10 +20,19 @@ from kevm_pyk.kevm import KEVM, KEVMNodePrinter, KEVMSemantics from kevm_pyk.utils import byte_offset_to_lines, legacy_explore, print_failure_info, print_model from pyk.cterm import CTerm -from pyk.kast.inner import KApply, KInner, KSort, KToken, KVariable -from pyk.kast.manip import cell_label_to_var_name, collect, extract_lhs, flatten_label, minimize_term, top_down +from pyk.kast.inner import KApply, KInner, KSequence, KSort, KToken, KVariable, Subst +from pyk.kast.manip import ( + cell_label_to_var_name, + collect, + extract_lhs, + flatten_label, + minimize_term, + set_cell, + top_down, +) from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire from pyk.kcfg import KCFG +from pyk.kcfg.kcfg import Step from pyk.kcfg.minimize import KCFGMinimizer from pyk.prelude.bytes import bytesToken from pyk.prelude.collections import map_empty @@ -44,6 +53,7 @@ _read_digest_file, append_to_file, empty_lemmas_file_contents, + ensure_name_is_unique, foundry_toml_extra_contents, kontrol_file_contents, kontrol_toml_file_contents, @@ -55,8 +65,10 @@ from collections.abc import Iterable from typing import Any, Final + from pyk.cterm import CTermSymbolic from pyk.kast.outer import KAst from pyk.kcfg.kcfg import NodeIdLike + from pyk.kcfg.semantics import KCFGExtendResult from pyk.kcfg.tui import KCFGElem from pyk.proof.implies import RefutationProof from pyk.proof.show import NodePrinter @@ -82,6 +94,77 @@ _LOGGER: Final = logging.getLogger(__name__) +class KontrolSemantics(KEVMSemantics): + + @staticmethod + def cut_point_rules( + break_on_jumpi: bool, + break_on_jump: bool, + break_on_calls: bool, + break_on_storage: bool, + break_on_basic_blocks: bool, + break_on_load_program: bool, + ) -> list[str]: + return ['FOUNDRY-CHEAT-CODES.rename'] + KEVMSemantics.cut_point_rules( + break_on_jumpi, + break_on_jump, + break_on_calls, + break_on_storage, + break_on_basic_blocks, + break_on_load_program, + ) + + def _check_rename_pattern(self, cterm: CTerm) -> bool: + """Given a CTerm, check if the rule 'FOUNDRY-CHEAT-CODES.rename' is at the top of the K_CELL. + + :param cterm: The CTerm representing the current state of the proof node. + :return: `True` if the pattern matches and a custom step can be made; `False` otherwise. + """ + abstract_pattern = KSequence( + [ + KApply('foundry_rename', [KVariable('###RENAME_TARGET'), KVariable('###NEW_NAME')]), + KVariable('###CONTINUATION'), + ] + ) + self._cached_subst = abstract_pattern.match(cterm.cell('K_CELL')) + return self._cached_subst is not None + + def _exec_rename_custom_step(self, cterm: CTerm) -> KCFGExtendResult | None: + subst = self._cached_subst + assert subst is not None + + # Extract the target var and new name from the substitution + target_var = subst['###RENAME_TARGET'] + name_token = subst['###NEW_NAME'] + assert type(target_var) is KVariable + assert type(name_token) is KToken + + # Ensure the name is unique + name_str = name_token.token[1:-1] + if len(name_str) == 0: + _LOGGER.warning('Name of symbolic variable cannot be empty. Reverting to the default name.') + return None + name = ensure_name_is_unique(name_str, cterm) + + # Replace var in configuration and constraints + rename_subst = Subst({target_var.name: KVariable(name, target_var.sort)}) + config = rename_subst(cterm.config) + constraints = [rename_subst(constraint) for constraint in cterm.constraints] + new_cterm = CTerm.from_kast(set_cell(config, 'K_CELL', KSequence(subst['###CONTINUATION']))) + + _LOGGER.info(f'Renaming {target_var.name} to {name}') + return Step(CTerm(new_cterm.config, constraints), 1, (), ['foundry_rename'], cut=True) + + def custom_step(self, cterm: CTerm, _cterm_symbolic: CTermSymbolic) -> KCFGExtendResult | None: + if self._check_rename_pattern(cterm): + return self._exec_rename_custom_step(cterm) + else: + return super().custom_step(cterm, _cterm_symbolic) + + def can_make_custom_step(self, cterm: CTerm) -> bool: + return self._check_rename_pattern(cterm) or super().can_make_custom_step(cterm) + + class FoundryKEVM(KEVM): foundry: Foundry @@ -841,7 +924,7 @@ def foundry_show( if options.failure_info: with legacy_explore( foundry.kevm, - kcfg_semantics=KEVMSemantics(), + kcfg_semantics=KontrolSemantics(), id=test_id, smt_timeout=options.smt_timeout, smt_retry_limit=options.smt_retry_limit, @@ -908,7 +991,7 @@ def _collect_klabel(_k: KInner) -> None: ] sentences = [sent for sent in sentences if not _contains_foundry_klabel(sent.body)] sentences = [ - sent for sent in sentences if not KEVMSemantics().is_terminal(CTerm.from_kast(extract_lhs(sent.body))) + sent for sent in sentences if not KontrolSemantics().is_terminal(CTerm.from_kast(extract_lhs(sent.body))) ] if len(sentences) == 0: _LOGGER.warning(f'No claims or rules retained for proof {proof.id}') @@ -1098,7 +1181,7 @@ def foundry_simplify_node( with legacy_explore( foundry.kevm, - kcfg_semantics=KEVMSemantics(), + kcfg_semantics=KontrolSemantics(), id=apr_proof.id, bug_report=options.bug_report, kore_rpc_command=kore_rpc_command, @@ -1146,7 +1229,7 @@ def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool: check_cells_ne = [check_cell for check_cell in check_cells if not check_cells_equal(check_cell, nodes)] if check_cells_ne: - if not all(KEVMSemantics().same_loop(nodes[0].cterm, nd.cterm) for nd in nodes): + if not all(KontrolSemantics().same_loop(nodes[0].cterm, nd.cterm) for nd in nodes): raise ValueError(f'Nodes {options.nodes} cannot be merged because they differ in: {check_cells_ne}') anti_unification = nodes[0].cterm @@ -1186,7 +1269,7 @@ def foundry_step_node( with legacy_explore( foundry.kevm, - kcfg_semantics=KEVMSemantics(), + kcfg_semantics=KontrolSemantics(), id=apr_proof.id, bug_report=options.bug_report, kore_rpc_command=kore_rpc_command, @@ -1262,7 +1345,7 @@ def foundry_section_edge( with legacy_explore( foundry.kevm, - kcfg_semantics=KEVMSemantics(), + kcfg_semantics=KontrolSemantics(), id=apr_proof.id, bug_report=options.bug_report, kore_rpc_command=kore_rpc_command, @@ -1313,7 +1396,7 @@ def foundry_get_model( with legacy_explore( foundry.kevm, - kcfg_semantics=KEVMSemantics(), + kcfg_semantics=KontrolSemantics(), id=proof.id, bug_report=options.bug_report, kore_rpc_command=kore_rpc_command, diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md index 35892fc00..c7c4ffcc9 100644 --- a/src/kontrol/kdist/cheatcodes.md +++ b/src/kontrol/kdist/cheatcodes.md @@ -339,6 +339,10 @@ This rule then takes the address using `#asWord(#range(ARGS, 0, 32))` and makes #cheatcode_call SELECTOR ARGS => #loadAccount #asWord(ARGS) ~> #setSymbolicStorage #asWord(ARGS) ... requires SELECTOR ==Int selector ( "symbolicStorage(address)" ) orBool SELECTOR ==Int selector ( "setArbitraryStorage(address)") + + rule [cheatcode.call.withName.symbolicStorage]: + #cheatcode_call SELECTOR ARGS => #loadAccount #asWord(#range(ARGS,0,32)) ~> #setSymbolicStorage #asWord(#range(ARGS,0,32)) Bytes2String(#range(ARGS, 96, #asWord(#range(ARGS, 64, 32)))) ... + requires SELECTOR ==Int selector ( "symbolicStorage(address,string)" ) ``` #### `copyStorage` - Copies the storage of one account into another. @@ -376,6 +380,14 @@ This rule returns a symbolic integer of up to the bit width that was sent as an andBool 0 #cheatcode_call SELECTOR ARGS => #rename(?WORD, Bytes2String(#range(ARGS, 96, #asWord(#range(ARGS, 64, 32))))) ... + _ => #buf(32, ?WORD) + requires SELECTOR ==Int selector ( "freshUInt(uint8,string)" ) + andBool 0 #cheatcode_call SELECTOR ARGS => #rename(?WORD, Bytes2String(#range(ARGS, 64, #asWord(#range(ARGS, 32, 32))))) ... + _ => #buf(32, ?WORD) + requires SELECTOR ==Int selector ( "freshBool(string)" ) + ensures #rangeBool(?WORD) + [preserves-definedness] ``` #### `freshBytes` - Returns a fully symbolic byte array value of the given length. @@ -466,6 +485,16 @@ This rule returns a fully symbolic byte array value of the given length. orBool SELECTOR ==Int selector ( "randomBytes(uint256)" ) ensures lengthBytes(?BYTES) ==Int #asWord(ARGS) [preserves-definedness] + + rule [cheatcode.call.withName.freshBytes]: + #cheatcode_call SELECTOR ARGS => #rename(?BYTES, Bytes2String(#range(ARGS, 96, #asWord(#range(ARGS, 64, 32))))) ... + _ => + #buf(32, 32) +Bytes #buf(32, #asWord(#range(ARGS, 0, 32))) +Bytes ?BYTES + +Bytes #buf ( ( ( notMaxUInt5 &Int ( #asWord(#range(ARGS, 0, 32)) +Int maxUInt5 ) ) -Int #asWord(#range(ARGS, 0, 32)) ) , 0 ) + + requires SELECTOR ==Int selector ( "freshBytes(uint256,string)" ) + ensures lengthBytes(?BYTES) ==Int #asWord(#range(ARGS, 0, 32)) + [preserves-definedness] ``` This rule returns a fully symbolic byte array value of length 4. @@ -512,6 +541,13 @@ This rule returns a symbolic address value. orBool SELECTOR ==Int selector ( "randomAddress()" ) ensures #rangeAddress(?WORD) andBool ?WORD =/=Int #address(FoundryTest) andBool ?WORD =/=Int #address(FoundryCheat) [preserves-definedness] + + rule [foundry.call.withName.freshAddress]: + #cheatcode_call SELECTOR ARGS => #rename(?WORD, Bytes2String(#range(ARGS, 64, #asWord(#range(ARGS, 32, 32))))) ... + _ => #buf(32, ?WORD) + requires SELECTOR ==Int selector ( "freshAddress(string)" ) + ensures #rangeAddress(?WORD) andBool ?WORD =/=Int #address(FoundryTest) andBool ?WORD =/=Int #address(FoundryCheat) + [preserves-definedness] ``` Expecting the next call to revert @@ -1109,6 +1145,15 @@ Mock functions Utils ----- + - Defining a new production `#rename` for all the types for which we generate symbolic values. +We don't care about the values because they will be processed in the `custom_step` function in Python. + +```k + syntax RenameTarget ::= Int | Bytes | Map + syntax KItem ::= #rename ( RenameTarget , String ) [symbol(foundry_rename)] + // --------------------------------------------------------------------------- + rule [rename]: #rename(_,_) => .K ... +``` - `#loadAccount ACCT` creates a new, empty account for `ACCT` if it does not already exist. Otherwise, it has no effect. ```k @@ -1202,7 +1247,9 @@ Utils - `#setSymbolicStorage ACCTID` takes a given account and makes its storage fully symbolic. ```k - syntax KItem ::= "#setSymbolicStorage" Int [symbol(foundry_setSymbolicStorage)] + syntax KItem ::= "#setSymbolicStorage" Int [symbol(foundry_setSymbolicStorage)] + | "#setSymbolicStorage" Int String [symbol(foundry_setSymbolicStorageWithName)] + // ---------------------------------------------------------------------------------------------- ``` ```{.k .symbolic} @@ -1213,6 +1260,14 @@ Utils _ => ?STORAGE ... + + rule #setSymbolicStorage ACCTID NAME => #rename(?STORAGE, NAME) ... + + ACCTID + _ => ?STORAGE + _ => ?STORAGE + ... + ``` - `#copyStorage ACCTFROM ACCTTO` copies the storage of ACCTFROM to be the storage of ACCTTO @@ -1669,18 +1724,23 @@ Selectors for **implemented** cheat code functions. rule ( selector ( "expectEmit(bool,bool,bool,bool,address)" ) => 2176505587 ) rule ( selector ( "sign(uint256,bytes32)" ) => 3812747940 ) rule ( selector ( "symbolicStorage(address)" ) => 769677742 ) + rule ( selector ( "symbolicStorage(address,string)" ) => 745143816 ) rule ( selector ( "setArbitraryStorage(address)" ) => 3781367863 ) rule ( selector ( "freshUInt(uint8)" ) => 625253732 ) + rule ( selector ( "freshUInt(uint8,string)" ) => 1530912521 ) rule ( selector ( "randomUint(uint256)" ) => 3481396892 ) rule ( selector ( "randomUint()" ) => 621954864 ) rule ( selector ( "randomUint(uint256,uint256)" ) => 3592095003 ) rule ( selector ( "freshBool()" ) => 2935720297 ) + rule ( selector ( "freshBool(string)" ) => 525694724 ) rule ( selector ( "randomBool()" ) => 3451987645 ) rule ( selector ( "freshBytes(uint256)" ) => 1389402351 ) + rule ( selector ( "freshBytes(uint256,string)" ) => 390682600 ) rule ( selector ( "randomBytes(uint256)" ) => 1818047145 ) rule ( selector ( "randomBytes4()" ) => 2608649593 ) rule ( selector ( "randomBytes8()" ) => 77050021 ) rule ( selector ( "freshAddress()" ) => 2363359817 ) + rule ( selector ( "freshAddress(string)" ) => 1202084987 ) rule ( selector ( "randomAddress()" ) => 3586058741 ) rule ( selector ( "prank(address)" ) => 3395723175 ) rule ( selector ( "prank(address,address)" ) => 1206193358 ) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 3f0446730..58fa15991 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -11,7 +11,7 @@ from typing import TYPE_CHECKING, Any, ContextManager, NamedTuple from kevm_pyk.cli import EVMChainOptions -from kevm_pyk.kevm import KEVM, KEVMSemantics, _process_jumpdests +from kevm_pyk.kevm import KEVM, _process_jumpdests from kevm_pyk.utils import KDefinition__expand_macros, abstract_cell_vars, run_prover from multiprocess.pool import Pool # type: ignore from pyk.cterm import CTerm, CTermSymbolic @@ -35,7 +35,7 @@ from pyk.utils import hash_str, run_process_2, single, unique from rich.progress import Progress, SpinnerColumn, TaskID, TextColumn, TimeElapsedColumn -from .foundry import Foundry, foundry_to_xml +from .foundry import Foundry, KontrolSemantics, foundry_to_xml from .hevm import Hevm from .options import ConfigType, TraceOptions from .solc_to_k import Contract, hex_string_to_int @@ -381,7 +381,7 @@ def create_kcfg_explore() -> KCFGExplore: ) return KCFGExplore( cterm_symbolic, - kcfg_semantics=KEVMSemantics(auto_abstract_gas=options.auto_abstract_gas), + kcfg_semantics=KontrolSemantics(auto_abstract_gas=options.auto_abstract_gas), id=test.id, ) @@ -425,7 +425,7 @@ def create_kcfg_explore() -> KCFGExplore: } ), ) - cut_point_rules = KEVMSemantics.cut_point_rules( + cut_point_rules = KontrolSemantics.cut_point_rules( options.break_on_jumpi, options.break_on_jump, options.break_on_calls, @@ -465,7 +465,7 @@ def create_kcfg_explore() -> KCFGExplore: max_depth=options.max_depth, max_iterations=options.max_iterations, cut_point_rules=cut_point_rules, - terminal_rules=KEVMSemantics.terminal_rules(options.break_every_step), + terminal_rules=KontrolSemantics.terminal_rules(options.break_every_step), counterexample_info=options.counterexample_info, max_frontier_parallel=options.max_frontier_parallel, fail_fast=options.fail_fast, diff --git a/src/kontrol/utils.py b/src/kontrol/utils.py index d84254a54..a5ea7361c 100644 --- a/src/kontrol/utils.py +++ b/src/kontrol/utils.py @@ -10,6 +10,7 @@ if TYPE_CHECKING: from typing import Final + from pyk.cterm import CTerm from argparse import Namespace import os @@ -25,6 +26,21 @@ _LOGGER: Final = logging.getLogger(__name__) +def ensure_name_is_unique(name: str, cterm: CTerm) -> str: + """Ensure that a given name for a KVariable is unique within the context of a CTerm. + + :param name: name of a KVariable + :param cterm: cterm + :return: Returns the name if it's not used, otherwise appends a suffix. + :rtype: str + """ + if name not in cterm.free_vars: + return name + + index = next(i for i in range(len(cterm.free_vars) + 1) if f'{name}_{i}' not in cterm.free_vars) + return f'{name}_{index}' + + def check_k_version() -> None: expected_k_version = KVersion.parse(f'v{pyk.__version__}') actual_k_version = k_version() diff --git a/src/tests/integration/test-data/end-to-end-prove-all b/src/tests/integration/test-data/end-to-end-prove-all index 18565c4ce..6a2bc826c 100644 --- a/src/tests/integration/test-data/end-to-end-prove-all +++ b/src/tests/integration/test-data/end-to-end-prove-all @@ -1,4 +1,5 @@ CounterTest.test_Increment() +RandomVarTest.test_custom_names() RandomVarTest.test_randomBool() RandomVarTest.test_randomAddress() RandomVarTest.test_randomUint() diff --git a/src/tests/integration/test-data/end-to-end-prove-show b/src/tests/integration/test-data/end-to-end-prove-show new file mode 100644 index 000000000..028eb6cd8 --- /dev/null +++ b/src/tests/integration/test-data/end-to-end-prove-show @@ -0,0 +1 @@ +RandomVarTest.test_custom_names() diff --git a/src/tests/integration/test-data/show/RandomVarTest.test_custom_names().expected b/src/tests/integration/test-data/show/RandomVarTest.test_custom_names().expected new file mode 100644 index 000000000..4301f1d13 --- /dev/null +++ b/src/tests/integration/test-data/show/RandomVarTest.test_custom_names().expected @@ -0,0 +1,4014 @@ + +┌─ 1 (root, init) +│ k: #execute ~> CONTINUATION:K +│ pc: 0 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/RandomVar.t.sol:7:68 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (371 steps) +├─ 3 +│ k: #rename ( ?WORD:Int , "BOOLEAN" ) ~> #cheatcode_return 128 32 ~> #pc [ CALL ] ~> ... +│ pc: 2947 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/RandomVar.t.sol:58:58 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (1 step) +├─ 4 +│ k: #cheatcode_return 128 32 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K +│ pc: 2947 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/RandomVar.t.sol:58:58 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (456 steps) +├─ 5 +│ k: #rename ( ?WORD:Int , "BOOLEAN" ) ~> #cheatcode_return 160 32 ~> #pc [ CALL ] ~> ... +│ pc: 3083 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/RandomVar.t.sol:59:59 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (1 step) +├─ 6 +│ k: #cheatcode_return 160 32 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K +│ pc: 3083 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/RandomVar.t.sol:59:59 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (1000 steps) +├─ 7 +│ k: #execute ~> CONTINUATION:K +│ pc: 6972 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ method: test%RandomVarTest.test_custom_names() +│ +│ (253 steps) +├─ 8 +│ k: #rename ( ?WORD:Int , "NEW_SLOT" ) ~> #cheatcode_return 256 32 ~> #pc [ CALL ] ~ ... +│ pc: 5602 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:276:276 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (1 step) +├─ 9 +│ k: #cheatcode_return 256 32 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K +│ pc: 5602 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:276:276 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (452 steps) +├─ 10 +│ k: #rename ( ?WORD:Int , "NEW_ACCOUNT" ) ~> #cheatcode_return 288 32 ~> #pc [ CALL ... +│ pc: 3448 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/RandomVar.t.sol:63:63 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (1 step) +├─ 11 +│ k: #cheatcode_return 288 32 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K +│ pc: 3448 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/RandomVar.t.sol:63:63 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (551 steps) +├─ 12 +│ k: #rename ( ?STORAGE:Map , "NEW_ACCOUNT_STORAGE" ) ~> #cheatcode_return 320 0 ~> # ... +│ pc: 3624 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/RandomVar.t.sol:64:64 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (1 step) +├─ 13 +│ k: #cheatcode_return 320 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K +│ pc: 3624 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/RandomVar.t.sol:64:64 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (263 steps) +├─ 14 +│ k: #rename ( ?BYTES:Bytes , "NEW_BYTES" ) ~> #cheatcode_return 320 0 ~> #pc [ CALL ... +│ pc: 3735 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/RandomVar.t.sol:65:65 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (1 step) +├─ 15 +│ k: #cheatcode_return 320 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K +│ pc: 3735 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/RandomVar.t.sol:65:65 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (1000 steps) +├─ 16 +│ k: POP 1 ~> #pc [ POP ] ~> #execute ~> CONTINUATION:K +│ pc: 3923 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/RandomVar.t.sol:57:67 +│ method: test%RandomVarTest.test_custom_names() +│ +│ (26 steps) +├─ 17 (terminal) +│ k: #halt ~> CONTINUATION:K +│ pc: 371 +│ callDepth: 0 +│ statusCode: EVMC_SUCCESS +│ src: test/RandomVar.t.sol:45:50 +│ method: test%RandomVarTest.test_custom_names() +│ +┊ constraint: +┊ ( notBool NEW_ACCOUNT:Int ==Int 645326474426547203313410069153905908525362434349 ) +┊ ( notBool NEW_ACCOUNT:Int ==Int 728815563385977040452943777879061427756277306518 ) +┊ subst: ... +└─ 2 (leaf, target, terminal) + k: #halt ~> CONTINUATION:K + pc: PC_CELL_5d410f2a:Int + callDepth: CALLDEPTH_CELL_5d410f2a:Int + statusCode: STATUSCODE_FINAL:StatusCode + + + + +module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 + + + rule [BASIC-BLOCK-1-TO-3]: + + + ( .K => #rename ( ??WORD , "BOOLEAN" ) + ~> #cheatcode_return 128 32 + ~> #pc [ CALL ] ) + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + ( b"" => #buf ( 32 , ??WORD ) ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( .WordStack => ( 228 : ( selector ( "freshBool(string)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( 370 : ( selector ( "test_custom_names()" ) : .WordStack ) ) ) ) ) ) ) + + + ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x1fUw\x04\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x07BOOLEAN\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( pow24 + + + ( #rename ( ?WORD:Int , "BOOLEAN" ) ~> .K => .K ) + ~> #cheatcode_return 128 32 + ~> #pc [ CALL ] + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + #buf ( 32 , ( ?WORD:Int => ?BOOLEAN ) ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( 228 : ( selector ( "freshBool(string)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( 370 : ( selector ( "test_custom_names()" ) : .WordStack ) ) ) ) ) ) + + + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x1fUw\x04\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x07BOOLEAN\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( ?WORD:Int + + + ( #cheatcode_return 128 32 ~> .K => #rename ( ??WORD , "BOOLEAN" ) + ~> #cheatcode_return 160 32 ) + ~> #pc [ CALL ] + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + #buf ( 32 , ( BOOLEAN:Int => ??WORD ) ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( ( 228 => 260 ) : ( selector ( "freshBool(string)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( ( 370 => BOOLEAN:Int ) : ( ( selector ( "test_custom_names()" ) => 370 ) : ( .WordStack => ( selector ( "test_custom_names()" ) : .WordStack ) ) ) ) ) ) ) ) + + + ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x1fUw\x04\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x07BOOLEAN\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xa0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , BOOLEAN:Int ) +Bytes b"\x1fUw\x04\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x07BOOLEAN\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( BOOLEAN:Int + + + ( #rename ( ?WORD:Int , "BOOLEAN" ) ~> .K => .K ) + ~> #cheatcode_return 160 32 + ~> #pc [ CALL ] + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + #buf ( 32 , ( ?WORD:Int => ?BOOLEAN_0 ) ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( 260 : ( selector ( "freshBool(string)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( BOOLEAN:Int : ( 370 : ( selector ( "test_custom_names()" ) : .WordStack ) ) ) ) ) ) ) + + + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xa0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , BOOLEAN:Int ) +Bytes b"\x1fUw\x04\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x07BOOLEAN\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( ?WORD:Int + + + ( #cheatcode_return 160 32 + ~> #pc [ CALL ] => .K ) + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + ( #buf ( 32 , BOOLEAN_0:Int ) => b"" ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( ( 260 => 0 ) : ( ( selector ( "freshBool(string)" ) => 260 ) : ( ( 645326474426547203313410069153905908525362434349 => 192 ) : ( ( 0 => 32 ) : ( ( BOOLEAN:Int => 5589 ) : ( ( 370 => selector ( "freshUInt(uint8,string)" ) ) : ( ( selector ( "test_custom_names()" ) => 645326474426547203313410069153905908525362434349 ) : ( .WordStack => ( 0 : ( 192 : ( 3359 : ( 0 : ( 0 : ( 1 : ( 370 : ( selector ( "test_custom_names()" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + + + ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xa0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , BOOLEAN:Int ) +Bytes b"\x1fUw\x04\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x07BOOLEAN\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00[?\xdf\t\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" ) + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( BOOLEAN:Int + + + ( .K => #rename ( ??WORD , "NEW_SLOT" ) + ~> #cheatcode_return 256 32 + ~> #pc [ CALL ] ) + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + ( b"" => #buf ( 32 , ??WORD ) ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( ( 0 => 388 ) : ( ( 260 => selector ( "freshUInt(uint8,string)" ) ) : ( ( 192 => 645326474426547203313410069153905908525362434349 ) : ( ( 32 => 0 ) : ( ( 5589 => 192 ) : ( ( selector ( "freshUInt(uint8,string)" ) => 3359 ) : ( ( 645326474426547203313410069153905908525362434349 => 0 ) : ( 0 : ( ( 192 => 1 ) : ( ( 3359 => 370 ) : ( ( 0 => selector ( "test_custom_names()" ) ) : ( ( 0 : ( 1 : ( 370 : ( selector ( "test_custom_names()" ) : .WordStack ) ) ) ) => .WordStack ) ) ) ) ) ) ) ) ) ) ) ) + + + ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00[?\xdf\t\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00[?\xdf\t\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( _BOOLEAN ==Int 1 + andBool ( _BOOLEAN_0 ==Int 0 + andBool ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( pow24 + + + ( #rename ( ?WORD:Int , "NEW_SLOT" ) ~> .K => .K ) + ~> #cheatcode_return 256 32 + ~> #pc [ CALL ] + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + #buf ( 32 , ( ?WORD:Int => ?NEW_SLOT ) ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( 388 : ( selector ( "freshUInt(uint8,string)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( 192 : ( 3359 : ( 0 : ( 0 : ( 1 : ( 370 : ( selector ( "test_custom_names()" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) + + + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00[?\xdf\t\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( _BOOLEAN ==Int 1 + andBool ( _BOOLEAN_0 ==Int 0 + andBool ( 0 <=Int ?WORD:Int + andBool ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( pow24 + + + ( #cheatcode_return 256 32 ~> .K => #rename ( ??WORD , "NEW_ACCOUNT" ) + ~> #cheatcode_return 288 32 ) + ~> #pc [ CALL ] + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + #buf ( 32 , ( NEW_SLOT:Int => ??WORD ) ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( 388 : ( ( selector ( "freshUInt(uint8,string)" ) => selector ( "freshAddress(string)" ) ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( ( 192 => NEW_SLOT:Int ) : ( ( 3359 => 0 ) : ( ( 0 => 1 ) : ( ( 0 => 370 ) : ( ( 1 => selector ( "test_custom_names()" ) ) : ( ( 370 : ( selector ( "test_custom_names()" ) : .WordStack ) ) => .WordStack ) ) ) ) ) ) ) ) ) ) + + + ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00[?\xdf\t\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , NEW_SLOT:Int ) +Bytes b"G\xa6\\{\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0bNEW_ACCOUNT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( _BOOLEAN ==Int 1 + andBool ( _BOOLEAN_0 ==Int 0 + andBool ( 0 <=Int NEW_SLOT:Int + andBool ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( pow24 + + + ( #rename ( ?WORD:Int , "NEW_ACCOUNT" ) ~> .K => .K ) + ~> #cheatcode_return 288 32 + ~> #pc [ CALL ] + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + #buf ( 32 , ( ?WORD:Int => ?NEW_ACCOUNT ) ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( 388 : ( selector ( "freshAddress(string)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( NEW_SLOT:Int : ( 0 : ( 1 : ( 370 : ( selector ( "test_custom_names()" ) : .WordStack ) ) ) ) ) ) ) ) ) + + + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , NEW_SLOT:Int ) +Bytes b"G\xa6\\{\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0bNEW_ACCOUNT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( _BOOLEAN ==Int 1 + andBool ( _BOOLEAN_0 ==Int 0 + andBool ( 0 <=Int ?WORD:Int + andBool ( 0 <=Int NEW_SLOT:Int + andBool ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( pow24 + + + ( #cheatcode_return 288 32 ~> .K => #rename ( ??STORAGE , "NEW_ACCOUNT_STORAGE" ) + ~> #cheatcode_return 320 0 ) + ~> #pc [ CALL ] + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + ( #buf ( 32 , NEW_ACCOUNT:Int ) => b"" ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( ( 388 => 452 ) : ( ( selector ( "freshAddress(string)" ) => selector ( "symbolicStorage(address,string)" ) ) : ( 645326474426547203313410069153905908525362434349 : ( ( 0 => NEW_ACCOUNT:Int ) : ( NEW_SLOT:Int : ( 0 : ( 1 : ( 370 : ( selector ( "test_custom_names()" ) : .WordStack ) ) ) ) ) ) ) ) ) + + + ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) +Bytes #buf ( 32 , NEW_SLOT:Int ) +Bytes ( b"G\xa6\\{\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0bNEW_ACCOUNT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => #buf ( 32 , NEW_ACCOUNT:Int ) +Bytes b",i\xfe\x08" +Bytes #buf ( 32 , NEW_ACCOUNT:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x13NEW_ACCOUNT_STORAGE\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + ( SetItem ( 645326474426547203313410069153905908525362434349 ) => SetItem ( 645326474426547203313410069153905908525362434349 ) |Set SetItem ( NEW_ACCOUNT:Int ) ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + ( + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + => ( + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + + + + NEW_ACCOUNT:Int + + + 0 + + + ??STORAGE + + + ??STORAGE + + + .Map + + + 0 + + ... + ) ) ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( _BOOLEAN ==Int 1 + andBool ( _BOOLEAN_0 ==Int 0 + andBool ( 0 <=Int NEW_SLOT:Int + andBool ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( 0 <=Int NEW_ACCOUNT:Int + andBool ( pow24 + + + ( #rename ( ?STORAGE:Map , "NEW_ACCOUNT_STORAGE" ) ~> .K => .K ) + ~> #cheatcode_return 320 0 + ~> #pc [ CALL ] + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + b"" + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( 452 : ( selector ( "symbolicStorage(address,string)" ) : ( 645326474426547203313410069153905908525362434349 : ( NEW_ACCOUNT:Int : ( NEW_SLOT:Int : ( 0 : ( 1 : ( 370 : ( selector ( "test_custom_names()" ) : .WordStack ) ) ) ) ) ) ) ) ) + + + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , NEW_SLOT:Int ) +Bytes #buf ( 32 , NEW_ACCOUNT:Int ) +Bytes b",i\xfe\x08" +Bytes #buf ( 32 , NEW_ACCOUNT:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x13NEW_ACCOUNT_STORAGE\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) |Set SetItem ( NEW_ACCOUNT:Int ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + ( + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + + + + NEW_ACCOUNT:Int + + + 0 + + + ( ?STORAGE:Map => ?NEW_ACCOUNT_STORAGE ) + + + ( ?STORAGE:Map => ?NEW_ACCOUNT_STORAGE ) + + + .Map + + + 0 + + ... + ) ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( _BOOLEAN ==Int 1 + andBool ( _BOOLEAN_0 ==Int 0 + andBool ( 0 <=Int NEW_SLOT:Int + andBool ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( 0 <=Int NEW_ACCOUNT:Int + andBool ( pow24 + + + ( .K => #rename ( ??BYTES , "NEW_BYTES" ) ~> .K ) + ~> #cheatcode_return 320 0 + ~> #pc [ CALL ] + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " +Bytes ??BYTES ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( 452 : ( ( selector ( "symbolicStorage(address,string)" ) => selector ( "freshBytes(uint256,string)" ) ) : ( 645326474426547203313410069153905908525362434349 : ( ( NEW_ACCOUNT:Int => 0 ) : ( ( NEW_SLOT:Int => NEW_ACCOUNT:Int ) : ( ( 0 => NEW_SLOT:Int ) : ( ( 1 => 0 ) : ( ( 370 => 1 ) : ( ( selector ( "test_custom_names()" ) => 370 ) : ( .WordStack => ( selector ( "test_custom_names()" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) + + + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , NEW_SLOT:Int ) +Bytes #buf ( 32 , NEW_ACCOUNT:Int ) +Bytes ( b",i\xfe\x08" +Bytes #buf ( 32 , NEW_ACCOUNT:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x13NEW_ACCOUNT_STORAGE\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x17IW\xe8\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\tNEW_BYTES\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + ( SetItem ( 645326474426547203313410069153905908525362434349 ) => SetItem ( 645326474426547203313410069153905908525362434349 ) |Set SetItem ( NEW_ACCOUNT:Int ) ) |Set SetItem ( ( NEW_ACCOUNT:Int => 645326474426547203313410069153905908525362434349 ) ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + ( + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + + + + NEW_ACCOUNT:Int + + + 0 + + + NEW_ACCOUNT_STORAGE:Map + + + NEW_ACCOUNT_STORAGE:Map + + + .Map + + + 0 + + ... + ) ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( _BOOLEAN ==Int 1 + andBool ( _BOOLEAN_0 ==Int 0 + andBool ( 0 <=Int NEW_SLOT:Int + andBool ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( 0 <=Int NEW_ACCOUNT:Int + andBool ( pow24 + + + ( #rename ( ?BYTES:Bytes , "NEW_BYTES" ) ~> .K => .K ) + ~> #cheatcode_return 320 0 + ~> #pc [ CALL ] + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " +Bytes ( ?BYTES:Bytes => ?NEW_BYTES ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( 452 : ( selector ( "freshBytes(uint256,string)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( NEW_ACCOUNT:Int : ( NEW_SLOT:Int : ( 0 : ( 1 : ( 370 : ( selector ( "test_custom_names()" ) : .WordStack ) ) ) ) ) ) ) ) ) ) + + + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , NEW_SLOT:Int ) +Bytes #buf ( 32 , NEW_ACCOUNT:Int ) +Bytes b"\x17IW\xe8\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\tNEW_BYTES\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) |Set SetItem ( NEW_ACCOUNT:Int ) |Set SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + ( + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + + + + NEW_ACCOUNT:Int + + + 0 + + + NEW_ACCOUNT_STORAGE:Map + + + NEW_ACCOUNT_STORAGE:Map + + + .Map + + + 0 + + ... + ) ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( _BOOLEAN ==Int 1 + andBool ( _BOOLEAN_0 ==Int 0 + andBool ( 0 <=Int NEW_SLOT:Int + andBool ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( 0 <=Int NEW_ACCOUNT:Int + andBool ( pow24 + + + ( #cheatcode_return 320 0 + ~> #pc [ CALL ] => POP 1 + ~> #pc [ POP ] ) + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " +Bytes NEW_BYTES:Bytes => b"" ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( ( 452 => 370 ) : ( ( selector ( "freshBytes(uint256,string)" ) => selector ( "test_custom_names()" ) ) : ( ( 645326474426547203313410069153905908525362434349 : ( 0 : ( NEW_ACCOUNT:Int : ( NEW_SLOT:Int : ( 0 : ( 1 : ( 370 : ( selector ( "test_custom_names()" ) : .WordStack ) ) ) ) ) ) ) ) => .WordStack ) ) ) + + + ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\xe0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) +Bytes #buf ( 32 , NEW_SLOT:Int ) +Bytes #buf ( 32 , NEW_ACCOUNT:Int ) +Bytes ( b"\x17IW\xe8\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\tNEW_BYTES\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " +Bytes NEW_BYTES:Bytes +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " +Bytes NEW_BYTES:Bytes +Bytes b"p\xca\x10\xbb" +Bytes #buf ( 32 , NEW_ACCOUNT:Int ) +Bytes #buf ( 32 , NEW_SLOT:Int ) +Bytes NEW_BYTES:Bytes ) + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) |Set SetItem ( NEW_ACCOUNT:Int ) |Set SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + ( + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + + + + NEW_ACCOUNT:Int + + + 0 + + + ( NEW_ACCOUNT_STORAGE:Map => NEW_ACCOUNT_STORAGE:Map [ NEW_SLOT:Int <- #asWord ( NEW_BYTES:Bytes ) ] ) + + + NEW_ACCOUNT_STORAGE:Map + + + .Map + + + 0 + + ... + ) ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( _BOOLEAN ==Int 1 + andBool ( _BOOLEAN_0 ==Int 0 + andBool ( 0 <=Int NEW_SLOT:Int + andBool ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( 0 <=Int NEW_ACCOUNT:Int + andBool ( pow24 + + + ( POP 1 + ~> #pc [ POP ] + ~> #execute => #halt ~> .K ) + ~> _CONTINUATION + + + NORMAL + + + CANCUN + + + false + + + + + b"" + + + ( _STATUSCODE => EVMC_SUCCESS ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x86>\xc7\xa9" + + + 0 + + + ( ( 370 => selector ( "test_custom_names()" ) ) : ( ( selector ( "test_custom_names()" ) : .WordStack ) => .WordStack ) ) + + + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\xe0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08NEW_SLOT\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , NEW_SLOT:Int ) +Bytes #buf ( 32 , NEW_ACCOUNT:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " +Bytes NEW_BYTES:Bytes +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " +Bytes NEW_BYTES:Bytes +Bytes b"p\xca\x10\xbb" +Bytes #buf ( 32 , NEW_ACCOUNT:Int ) +Bytes #buf ( 32 , NEW_SLOT:Int ) +Bytes NEW_BYTES:Bytes + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) |Set SetItem ( NEW_ACCOUNT:Int ) |Set SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + ( + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + + + + NEW_ACCOUNT:Int + + + 0 + + + NEW_ACCOUNT_STORAGE:Map [ NEW_SLOT:Int <- #asWord ( NEW_BYTES:Bytes ) ] + + + NEW_ACCOUNT_STORAGE:Map + + + .Map + + + 0 + + ... + ) ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( _BOOLEAN ==Int 1 + andBool ( _BOOLEAN_0 ==Int 0 + andBool ( 0 <=Int NEW_SLOT:Int + andBool ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( 0 <=Int NEW_ACCOUNT:Int + andBool ( pow24 = type(uint256).min); assertTrue(rand <= type(uint256).max); } + function test_custom_names() public { + bool x = kevm.freshBool("BOOLEAN"); + bool y = kevm.freshBool("BOOLEAN"); + vm.assume(x == true); + vm.assume(y == false); + uint256 slot = freshUInt256("NEW_SLOT"); + address new_account = kevm.freshAddress("NEW_ACCOUNT"); + kevm.symbolicStorage(new_account, "NEW_ACCOUNT_STORAGE"); + bytes memory value = kevm.freshBytes(32, "NEW_BYTES"); + vm.store(new_account, bytes32(slot), bytes32(value)); + } } \ No newline at end of file diff --git a/src/tests/integration/test_kontrol.py b/src/tests/integration/test_kontrol.py index cf77002ef..14d1c68d7 100644 --- a/src/tests/integration/test_kontrol.py +++ b/src/tests/integration/test_kontrol.py @@ -9,13 +9,13 @@ from pyk.kore.rpc import kore_server from pyk.utils import single -from kontrol.foundry import Foundry, init_project +from kontrol.foundry import Foundry, foundry_show, init_project from kontrol.kompile import foundry_kompile -from kontrol.options import BuildOptions, ProveOptions +from kontrol.options import BuildOptions, ProveOptions, ShowOptions from kontrol.prove import foundry_prove from kontrol.utils import append_to_file, foundry_toml_cancun_schedule -from .utils import TEST_DATA_DIR, assert_pass +from .utils import TEST_DATA_DIR, assert_or_update_show_output, assert_pass if TYPE_CHECKING: from collections.abc import Iterator @@ -79,7 +79,8 @@ def foundry_end_to_end(foundry_root_dir: Path | None, tmp_path_factory: TempPath ALL_PROVE_TESTS: Final = tuple((TEST_DATA_DIR / 'end-to-end-prove-all').read_text().splitlines()) -SKIPPED_PROVE_TESTS: Final = set((TEST_DATA_DIR / 'end-to-end-prove-skip').read_text().splitlines()) +SKIPPED_PROVE_TESTS: Final = tuple((TEST_DATA_DIR / 'end-to-end-prove-skip').read_text().splitlines()) +SHOW_TESTS: Final = tuple((TEST_DATA_DIR / 'end-to-end-prove-show').read_text().splitlines()) @pytest.mark.parametrize('test_id', ALL_PROVE_TESTS) @@ -96,7 +97,7 @@ def test_kontrol_end_to_end( if ( test_id in SKIPPED_PROVE_TESTS or (no_use_booster and test_id in SKIPPED_PROVE_TESTS) - or (update_expected_output) + or (update_expected_output and test_id not in SHOW_TESTS) ): pytest.skip() @@ -115,9 +116,33 @@ def test_kontrol_end_to_end( 'port': server_end_to_end.port, 'force_sequential': force_sequential, 'schedule': 'CANCUN', + 'stack_checks': False, } ), ) # Then assert_pass(test_id, single(prove_res)) + + if test_id not in SHOW_TESTS or no_use_booster: + return + + # And when + show_res = foundry_show( + foundry=foundry_end_to_end, + options=ShowOptions( + { + 'test': test_id, + 'to_module': True, + 'sort_collections': True, + 'omit_unstable_output': True, + 'pending': True, + 'failing': True, + 'failure_info': True, + 'port': server_end_to_end.port, + } + ), + ) + + # Then + assert_or_update_show_output(show_res, TEST_DATA_DIR / f'show/{test_id}.expected', update=update_expected_output) diff --git a/src/tests/unit/test_foundry_prove.py b/src/tests/unit/test_foundry_prove.py index 11b14626a..bf6063a74 100644 --- a/src/tests/unit/test_foundry_prove.py +++ b/src/tests/unit/test_foundry_prove.py @@ -2,16 +2,20 @@ from typing import TYPE_CHECKING -from pyk.kast.inner import KApply, KLabel, KSort, KToken +import pytest +from pyk.cterm import CTerm +from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KToken, KVariable from kontrol.foundry import read_recorded_state_diff from kontrol.prove import recorded_state_to_account_cells +from kontrol.utils import ensure_name_is_unique from .utils import TEST_DATA_DIR if TYPE_CHECKING: from typing import Final + ACCESSES_INPUT_FILE: Final = TEST_DATA_DIR / 'accesses.json' ACCOUNTS_EXPECTED: Final = [ KApply( @@ -62,3 +66,25 @@ def test_recorded_state_to_account_cells() -> None: # Then assert actual == ACCOUNTS_EXPECTED + + +TEST_DATA = [ + ('single-var', 'NEWVAR', CTerm(KApply('', KVariable('NEWVAR')), []), 'NEWVAR_0'), + ( + 'sequence-check', + 'NEWVAR', + CTerm(KApply('', KSequence(KApply('_+Int_', [KVariable('NEWVAR'), KVariable('NEWVAR_0')]))), []), + 'NEWVAR_1', + ), +] + + +@pytest.mark.parametrize('test_id,name,config,expected', TEST_DATA, ids=[test_id for test_id, *_ in TEST_DATA]) +def test_ensure_name_is_unique(test_id: str, name: str, config: CTerm, expected: str) -> None: + # Given + + # When + actual = ensure_name_is_unique(name, config) + + # Then + assert actual == expected