feat: empty initial network state (#352)

.github/workflows/test-external.yml

@@ -87,7 +87,7 @@ jobs:
         run: docker run halmos-image --version
 
       - name: Test external repo
-        run: docker run -v .:/workspace halmos-image ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 --solver-threads 4 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}
+        run: docker run -v .:/workspace halmos-image ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 --solver-threads 3 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}
         working-directory: ${{ matrix.project.dir }}
         env:
           FOUNDRY_PROFILE: ${{ matrix.project.profile }}

.github/workflows/test-long.yml

@@ -48,4 +48,4 @@ jobs:
 
       - name: Run pytest
         run: |
-          docker run -v .:/workspace --entrypoint pytest halmos-image -x -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options='-st --solver-timeout-assertion 0 --solver-threads 4 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}' -s --log-cli-level=
+          docker run -v .:/workspace --entrypoint pytest halmos-image -x -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options='-st --solver-timeout-assertion 0 --solver-threads 3 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}' -s --log-cli-level=

src/halmos/__main__.py

@@ -19,16 +19,13 @@
 
 from z3 import (
     Z3_OP_CONCAT,
-    Array,
     BitVec,
     BitVecNumRef,
     BitVecRef,
-    BitVecSort,
     Bool,
     CheckSatResult,
     Context,
     ModelRef,
-    ZeroExt,
     is_app,
     is_bv,
     sat,
@@ -44,8 +41,14 @@
 from .exceptions import HalmosException
 from .mapper import DeployAddressMapper, Mapper
 from .sevm import (
+    EMPTY_BALANCE,
     EVM,
+    FOUNDRY_CALLER,
+    FOUNDRY_ORIGIN,
+    FOUNDRY_TEST,
+    ONE,
     SEVM,
+    ZERO,
     Address,
     Block,
     CallContext,
@@ -58,14 +61,13 @@
     Path,
     SMTQuery,
     State,
-    Word,
     con_addr,
     jumpid_str,
-    magic_address,
     mnemonic,
 )
 from .utils import (
     NamedTimer,
+    address,
     byte_length,
     color_error,
     con,
@@ -221,41 +223,29 @@ def mk_calldata(
     calldata.create(fun_abi, cd)
 
 
-def mk_callvalue() -> Word:
-    return BitVec("msg_value", 256)
-
-
-def mk_balance() -> Word:
-    return Array("balance_0", BitVecSort(160), BitVecSort(256))
-
-
 def mk_block() -> Block:
+    # foundry default values
     block = Block(
-        basefee=ZeroExt(160, BitVec("block_basefee", 96)),  # practical limit 96 bit
-        chainid=ZeroExt(192, BitVec("block_chainid", 64)),  # chainid 64 bit
-        coinbase=mk_addr("block_coinbase"),  # address 160 bit
-        difficulty=BitVec("block_difficulty", 256),
-        gaslimit=ZeroExt(160, BitVec("block_gaslimit", 96)),  # practical limit 96 bit
-        number=ZeroExt(192, BitVec("block_number", 64)),  # practical limit 64 bit
-        timestamp=ZeroExt(192, BitVec("block_timestamp", 64)),  # practical limit 64 bit
+        basefee=ZERO,
+        chainid=con(31337),
+        coinbase=address(0),
+        difficulty=ZERO,
+        gaslimit=con(2**63 - 1),
+        number=ONE,
+        timestamp=ONE,
     )
-    block.chainid = con(1)  # for ethereum
     return block
 
 
 def mk_addr(name: str) -> Address:
     return BitVec(name, 160)
 
 
-def mk_caller(args: HalmosConfig) -> Address:
-    return mk_addr("msg_sender") if args.symbolic_msg_sender else magic_address
-
-
 def mk_this() -> Address:
     # NOTE: Do NOT remove the `con_addr()` wrapper.
     #       The return type should be BitVecSort(160) as it is used as a key for ex.code.
     #       The keys of ex.code are compared using structural equality with other BitVecRef addresses.
-    return con_addr(magic_address + 1)
+    return con_addr(FOUNDRY_TEST)
 
 
 def mk_solver(args: HalmosConfig, logic="QF_AUFBV", ctx=None, assertion=False):
@@ -416,8 +406,8 @@ def deploy_test(
     this = mk_this()
     message = Message(
         target=this,
-        caller=mk_caller(args),
-        origin=mk_addr("tx_origin"),
+        caller=FOUNDRY_CALLER,
+        origin=FOUNDRY_ORIGIN,
         value=0,
         data=ByteVec(),
         call_scheme=EVM.CREATE,
@@ -426,7 +416,7 @@ def deploy_test(
     ex = sevm.mk_exec(
         code={this: Contract(b"")},
         storage={this: {}},
-        balance=mk_balance(),
+        balance=EMPTY_BALANCE,
         block=mk_block(),
         context=CallContext(message=message),
         pgm=None,  # to be added
@@ -443,13 +433,6 @@ def deploy_test(
     creation_bytecode = Contract.from_hexcode(creation_hexcode)
     ex.pgm = creation_bytecode
 
-    # use the given deployed bytecode if --no-test-constructor is enabled
-    if args.no_test_constructor:
-        deployed_bytecode = Contract.from_hexcode(deployed_hexcode)
-        ex.set_code(this, deployed_bytecode)
-        ex.pgm = deployed_bytecode
-        return ex
-
     # create test contract
     exs = list(sevm.run(ex))
 
@@ -1597,8 +1580,8 @@ def on_signal(signum, frame):
         contract_path = f"{contract_json['ast']['absolutePath']}:{contract_name}"
         print(f"\nRunning {num_found} tests for {contract_path}")
 
-        # Set 0xaaaa0001 in DeployAddressMapper
-        DeployAddressMapper().add_deployed_contract("0xaaaa0001", contract_name)
+        # Set the test contract address in DeployAddressMapper
+        DeployAddressMapper().add_deployed_contract(hexify(mk_this()), contract_name)
 
         # support for `/// @custom:halmos` annotations
         contract_args = with_natspec(args, contract_name, natspec)

src/halmos/cheatcodes.py

@@ -409,7 +409,7 @@ class hevm_cheat_code:
     label_sig: int = 0xC657C718
 
     # bytes4(keccak256("getBlockNumber()"))
-    get_block_nunber_sig: int = 0x42CBB15C
+    get_block_number_sig: int = 0x42CBB15C
 
     @staticmethod
     def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None:
@@ -581,7 +581,7 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None:
 
             return ret
 
-        # ffi(string[]) returns (bytes)
+        # vm.ffi(string[]) returns (bytes)
         elif funsig == hevm_cheat_code.ffi_sig:
             if not sevm.options.ffi:
                 error_msg = "ffi cheatcode is disabled. Run again with `--ffi` if you want to enable it"
@@ -615,6 +615,7 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None:
 
             return stringified_bytes_to_bytes(out_str)
 
+        # vm.addr(uint256 privateKey) returns (address keyAddr)
         elif funsig == hevm_cheat_code.addr_sig:
             private_key = uint256(extract_bytes(arg, 4, 32))
 
@@ -630,6 +631,7 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None:
             ret.append(uint256(addr))
             return ret
 
+        # vm.sign(uint256 privateKey, bytes32 digest) returns (uint8 v, bytes32 r, bytes32 s)
         elif funsig == hevm_cheat_code.sign_sig:
             key = extract_bytes(arg, 4, 32)
             digest = extract_bytes(arg, 4 + 32, 32)
@@ -679,6 +681,7 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None:
             ret.append(s)
             return ret
 
+        # vm.label(address account, string calldata newLabel)
         elif funsig == hevm_cheat_code.label_sig:
             addr = extract_bytes(arg, 4, 32)
 
@@ -687,8 +690,8 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None:
 
             return ret
 
-        # getBlockNumber() return (uint256)
-        elif funsig == hevm_cheat_code.get_block_nunber_sig:
+        # vm.getBlockNumber() return (uint256)
+        elif funsig == hevm_cheat_code.get_block_number_sig:
             ret.append(uint256(ex.block.number))
             return ret
 

src/halmos/config.py

@@ -165,16 +165,6 @@ class Config:
         global_default=False,
     )
 
-    symbolic_msg_sender: bool = arg(
-        help="set msg.sender symbolic",
-        global_default=False,
-    )
-
-    no_test_constructor: bool = arg(
-        help="do not run the constructor of test contracts",
-        global_default=False,
-    )
-
     ffi: bool = arg(
         help="allow the usage of FFI to call external functions",
         global_default=False,

src/halmos/sevm.py

@@ -122,19 +122,21 @@
 ZERO, ONE = con(0), con(1)
 MAX_CALL_DEPTH = 1024
 
+EMPTY_BALANCE = Array("balance_00", BitVecSort160, BitVecSort256)
+
 # TODO: make this configurable
 MAX_MEMORY_SIZE = 2**20
 
+FOUNDRY_CALLER = 0x1804C8AB1F12E6BBF3894D4083F33E07309D1F38
+FOUNDRY_ORIGIN = FOUNDRY_CALLER
+FOUNDRY_TEST = 0x7FA9385BE102AC3EAC297483DD6233D62B3E1496
+
 # (pc, (jumpdest, ...))
 # the jumpdests are stored as strings to avoid the cost of converting bv values
 JumpID = tuple[int, tuple[str]]
 
 # symbolic states
 
-# extcodesize(target address)
-f_extcodesize = Function("f_extcodesize", BitVecSort160, BitVecSort256)
-# extcodehash(target address)
-f_extcodehash = Function("f_extcodehash", BitVecSort160, BitVecSort256)
 # blockhash(block number)
 f_blockhash = Function("f_blockhash", BitVecSort256, BitVecSort256)
 # gas(cnt)
@@ -964,21 +966,25 @@ def select(self, array: Any, key: Word, arrays: dict) -> Word:
                 if self.check(key != key0) == unsat:  # key == key0
                     return val0
         # empty array
-        elif not self.symbolic and re.search(r"^storage_.+_00$", str(array)):
+        elif not self.symbolic and re.search(r"^(storage_.+|balance)_00$", str(array)):
             # note: simplifying empty array access might have a negative impact on solver performance
             return ZERO
         return Select(array, key)
 
     def balance_of(self, addr: Word) -> Word:
         assert_address(addr)
-        value = self.select(self.balance, uint160(addr), self.balances)
+        addr = uint160(addr)
+        value = self.select(self.balance, addr, self.balances)
+        # generate emptyness axiom for each array index, instead of using quantified formula
+        self.path.append(Select(EMPTY_BALANCE, addr) == ZERO)
         # practical assumption on the max balance per account
         self.path.append(ULT(value, con(2**96)))
         return value
 
     def balance_update(self, addr: Word, value: Word) -> None:
         assert_address(addr)
         assert_uint256(value)
+        addr = uint160(addr)
         new_balance_var = Array(
             f"balance_{1+len(self.balances):>02}", BitVecSort160, BitVecSort256
         )

tests/expected/all.json

@@ -125,6 +125,15 @@
                 "time": null,
                 "num_bounded_loops": null
             },
+            {
+                "name": "check_gaslimit()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
             {
                 "name": "check_roll(uint256)",
                 "exitcode": 0,
@@ -820,6 +829,15 @@
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
+            },
+            {
+                "name": "check_initial_balance(address)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
             }
         ],
         "test/Extcodehash.t.sol:ExtcodehashTest": [
@@ -1018,6 +1036,15 @@
                 "time": null,
                 "num_bounded_loops": null
             },
+            {
+                "name": "check_caller()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
             {
                 "name": "check_deployCode(uint256)",
                 "exitcode": 0,
@@ -1053,6 +1080,24 @@
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
+            },
+            {
+                "name": "check_origin()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_this()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
             }
         ],
         "test/Getter.t.sol:GetterTest": [

tests/regression/halmos.toml

@@ -28,25 +28,13 @@ depth = 0
 # set the length of dynamic-sized arrays including bytes and string (default: loop unrolling bound)
 # array-lengths = NAME1=LENGTH1,NAME2=LENGTH2,...
 
-# use uninterpreted abstractions for unknown external calls with the given function signatures
-uninterpreted-unknown-calls = "0x150b7a02,0x1626ba7e,0xf23a6e61,0xbc197c81"
-
-# set the byte size of return data from uninterpreted unknown external calls
-return-size-of-unknown-calls = 32
-
 # Select one of the available storage layout models
 # The generic model should only be necessary for vyper, huff, or unconventional storage patterns in yul.
 storage-layout = "solidity"
 
 # set default storage values to symbolic
 symbolic-storage = false
 
-# set msg.sender symbolic
-symbolic-msg-sender = false
-
-# do not run the constructor of test contracts
-no-test-constructor = false
-
 # allow the usage of FFI to call external functions
 ffi = false
 
@@ -125,9 +113,6 @@ solver-max-memory = 0
 # use the given command when invoking the solver
 # solver-command = COMMAND
 
-# run assertion solvers in parallel
-solver-parallel = false
-
 # set the number of threads for parallel solvers
 # solver-threads = N