Fix msg.value balance accounting in invariant tests

src/halmos/__main__.py

@@ -567,11 +567,8 @@ def run_target_contract(
                 else None
             )
 
-            # create a symbolic msg.value
-            msg_value = BitVec(
-                f"halmos_msg_value_{id_str(addr)}_{uid()}_{ex.new_symbol_id():>02}",
-                BitVecSort256,
-            )
+            state_mutability = abi[fun_sig]["stateMutability"]
+            msg_value = mk_invariant_msg_value(ex, addr, state_mutability)
 
             yield from run_target_function(
                 args,
@@ -592,6 +589,22 @@ def run_target_contract(
             continue
 
 
+def mk_invariant_msg_value(
+    ex: Exec, addr: Address, state_mutability: str
+) -> Word:
+    """Return the call value modeled for an invariant target transaction."""
+    # Solidity dispatchers reject value before entering nonpayable functions.
+    # Model that value as zero up front so rejected calls do not create spurious
+    # balance histories in the invariant frontier.
+    if state_mutability != "payable":
+        return ZERO
+
+    return BitVec(
+        f"halmos_msg_value_{id_str(addr)}_{uid()}_{ex.new_symbol_id():>02}",
+        BitVecSort256,
+    )
+
+
 def _compute_frontier(ctx: ContractContext, depth: int) -> Iterator[Exec]:
     """
     Computes the frontier states at a given depth.

src/halmos/sevm.py

@@ -2310,22 +2310,29 @@ def transfer_value(
         if value.is_concrete and value.value == 0:
             return
 
+        caller = uint160(caller).as_z3()
+        to = uint160(to).as_z3()
         caller_balance: BitVecRef = ex.balance_of(caller)
 
         # assume balance is enough; otherwise ignore this path
         # note: evm requires enough balance even for self-transfer
         balance_cond = simplify(UGE(caller_balance, value.as_z3()))
-        if is_false(balance_cond):
+        if is_false(balance_cond) or ex.check(balance_cond) == unsat:
             raise InfeasiblePath("transfer_value: balance is not enough")
 
         ex.path.append(balance_cond)
 
+        # A self-transfer still requires sufficient funds, but has no net state
+        # change.  Check both structural equality and equality established by
+        # the current path before creating balance-array identities.
+        if eq(caller, to) or ex.check(caller != to) == unsat:
+            return
+
         # conditional transfer
         if condition is not None:
             value = If(condition, value, Z3_ZERO)
 
         ex.balance_update(caller, BV(caller_balance).sub(value))
-        # NOTE: ex.balance_of(to) must be called **after** updating the caller's balance above, to correctly handle the self-transfer case
         ex.balance_update(to, BV(ex.balance_of(to)).add(value))
 
     def call(
@@ -3009,11 +3016,14 @@ def run_message(self, pre_ex: Exec, message: Message, path: Path) -> Iterator[Ex
         Executes the given transaction from the given input state.
 
         Note: As this involves executing a new transaction, the transient storage is reset to empty instead of being inherited from the input state.
+        Failed top-level calls yield an error state with persistent network state
+        restored to the input transaction state. Transient storage remains at its
+        fresh transaction-start state.
         """
         ex0 = Exec(
             code=pre_ex.code.copy(),  # shallow copy
             storage=deepcopy(pre_ex.storage),
-            transient_storage=self.fresh_transient_storage(pre_ex),  # empty
+            transient_storage=self.fresh_transient_storage(pre_ex),
             balance=pre_ex.balance,
             #
             block=deepcopy(pre_ex.block),
@@ -3035,7 +3045,30 @@ def run_message(self, pre_ex: Exec, message: Message, path: Path) -> Iterator[Ex
             storages=pre_ex.storages.copy(),
             balances=pre_ex.balances.copy(),
         )
-        yield from self.run(ex0)
+
+        # Apply the top-level CALL value transfer to the copied transaction state.
+        # An underfunded transaction is invalid and therefore has no output state.
+        if message.call_scheme == OP_CALL:
+            try:
+                self.transfer_value(
+                    ex0,
+                    message.caller,
+                    message.target,
+                    uint256(message.value),
+                )
+            except InfeasiblePath:
+                return
+
+        for post_ex in self.run(ex0):
+            if isinstance(post_ex.context.output.error, EvmException):
+                post_ex.code = pre_ex.code.copy()
+                post_ex.storage = deepcopy(pre_ex.storage)
+                post_ex.transient_storage = self.fresh_transient_storage(pre_ex)
+                post_ex.balance = pre_ex.balance
+                post_ex.storages = pre_ex.storages.copy()
+                post_ex.balances = pre_ex.balances.copy()
+
+            yield post_ex
 
     def run(self, ex0: Exec) -> Iterator[Exec]:
         next_ex: Exec | None = ex0

tests/expected/all.json

@@ -2329,6 +2329,26 @@
                 "num_bounded_loops": null
             }
         ],
+        "test/InvariantMsgValue.t.sol:InvariantMsgValueTest": [
+            {
+                "name": "invariant_msg_value_can_be_positive()",
+                "exitcode": 1,
+                "num_models": 1,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "invariant_msg_value_transfer()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
         "test/InvariantProbes.t.sol:InvariantProbesTest": [
             {
                 "name": "invariant_probes_found()",
@@ -6734,4 +6754,4 @@
             }
         ]
     }
-}
+}

tests/regression/test/InvariantMsgValue.t.sol

@@ -0,0 +1,54 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import "forge-std/Test.sol";
+
+contract InvariantMsgValueTarget {
+    uint256 public totalMsgValue;
+    uint256 public nonpayableCalls;
+
+    function deposit() external payable {
+        totalMsgValue += msg.value;
+    }
+
+    function touch() external {
+        nonpayableCalls++;
+    }
+}
+
+contract InvariantMsgValueTest is Test {
+    address constant SENDER = address(0xbeef);
+    uint256 constant SENDER_INITIAL_BALANCE = 2 ether;
+    uint256 constant TARGET_INITIAL_BALANCE = 1 ether;
+
+    InvariantMsgValueTarget target;
+
+    function setUp() public {
+        target = new InvariantMsgValueTarget();
+
+        vm.deal(SENDER, SENDER_INITIAL_BALANCE);
+        vm.deal(address(target), TARGET_INITIAL_BALANCE);
+
+        targetContract(address(target));
+        targetSender(SENDER);
+    }
+
+    /// @custom:halmos --invariant-depth 1
+    function invariant_msg_value_transfer() public view {
+        // At depth one, this is the msg.value observed by the target call.
+        uint256 totalMsgValue = target.totalMsgValue();
+
+        assertLe(totalMsgValue, SENDER_INITIAL_BALANCE);
+        assertEq(SENDER.balance + totalMsgValue, SENDER_INITIAL_BALANCE);
+        assertEq(
+            address(target).balance,
+            TARGET_INITIAL_BALANCE + totalMsgValue
+        );
+    }
+
+    /// @custom:halmos --invariant-depth 1
+    function invariant_msg_value_can_be_positive() public view {
+        // Expected counterexample: deposit receives a positive, funded msg.value.
+        assertEq(target.totalMsgValue(), 0);
+    }
+}

tests/test_cli.py

@@ -8,12 +8,20 @@
     eq,
 )
 
-from halmos.bitvec import HalmosBitVec as BV
+from halmos.__main__ import mk_invariant_msg_value
+from halmos.bitvec import ZERO, HalmosBitVec as BV
 from halmos.calldata import str_abi
 from halmos.sevm import Contract, Instruction
 from halmos.utils import EVM, hexify
 
 
+@pytest.mark.parametrize("state_mutability", ["nonpayable", "view", "pure"])
+def test_nonpayable_invariant_target_has_zero_msg_value(state_mutability):
+    # Neither address formatting nor symbol allocation should be reached for a
+    # target that the ABI says cannot accept value.
+    assert mk_invariant_msg_value(None, None, state_mutability) is ZERO
+
+
 @pytest.fixture
 def setup_abi():
     return json.loads(