From d5a24a52c29b7ee425e1418c7f5649b4c9a58cc6 Mon Sep 17 00:00:00 2001
From: Michael Moffett <moffett.michael1@gmail.com>
Date: Tue, 14 Jul 2026 18:36:12 -0600
Subject: [PATCH] test: regression for payable-multicall counterexample (#178)

Adds a regression test under tests/regression/test/ that reproduces the
counterexample described in issue #178: the payable multicall pattern
used by Uniswap V3 Periphery lets a single msg.value be counted more
than once by any subcall that reads msg.value for accounting.

- New test file: tests/regression/test/PayableMulticall.t.sol
- Expected results added to tests/expected/all.json for the two new
  test names (one expected fail, one expected pass control).

Local verification:
  halmos --root tests/regression --contract PayableMulticallTest
  => 1 passed; 1 failed (counterexample at any positive amount)

Drafted with AI assistance; contract shape and counterexample were
validated locally against the full regression suite.
---
 tests/expected/all.json                      | 20 +++++
 tests/regression/test/PayableMulticall.t.sol | 83 ++++++++++++++++++++
 2 files changed, 103 insertions(+)
 create mode 100644 tests/regression/test/PayableMulticall.t.sol

diff --git a/tests/expected/all.json b/tests/expected/all.json
index b9cb7594..0d13c064 100644
--- a/tests/expected/all.json
+++ b/tests/expected/all.json
@@ -4240,6 +4240,26 @@
                 "num_bounded_loops": null
             }
         ],
+        "test/PayableMulticall.t.sol:PayableMulticallTest": [
+            {
+                "name": "check_multicall_no_double_credit_fail(uint256)",
+                "exitcode": 1,
+                "num_models": 1,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_single_deposit_no_over_credit_pass(uint256)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
         "test/Prank.t.sol:PrankSetUpTest": [
             {
                 "name": "check_prank(address)",
diff --git a/tests/regression/test/PayableMulticall.t.sol b/tests/regression/test/PayableMulticall.t.sol
new file mode 100644
index 00000000..164bda6d
--- /dev/null
+++ b/tests/regression/test/PayableMulticall.t.sol
@@ -0,0 +1,83 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import {Test} from "forge-std/Test.sol";
+
+// resolves https://github.com/a16z/halmos/issues/178
+//
+// Demonstrates the payable-multicall pattern popularized by
+// Uniswap/v3-periphery (see Uniswap/v3-periphery#52).
+//
+// The `payable` on `multicall` lets msg.value flow through delegatecall
+// to every subcall unchanged, so a single msg.value can be counted more
+// than once by any subcall that reads `msg.value` for accounting
+// (deposit-shaped functions, in particular).
+//
+// The counterexample halmos finds: with any positive `amount`, batching
+// two `deposit()` subcalls credits the caller `2 * amount` for a single
+// `amount` payment.
+
+abstract contract Multicall {
+    function multicall(bytes[] calldata data) external payable returns (bytes[] memory results) {
+        results = new bytes[](data.length);
+        for (uint256 i = 0; i < data.length; i++) {
+            (bool success, bytes memory result) = address(this).delegatecall(data[i]);
+            require(success, "multicall subcall reverted");
+            results[i] = result;
+        }
+    }
+}
+
+/// @notice WETH-shaped contract that credits msg.value on deposit.
+///         Inheriting the payable Multicall makes deposit accountable for
+///         the same msg.value more than once per batch.
+contract VulnerableWETH is Multicall {
+    mapping(address => uint256) public balanceOf;
+
+    function deposit() external payable {
+        balanceOf[msg.sender] += msg.value;
+    }
+}
+
+contract PayableMulticallTest is Test {
+    VulnerableWETH weth;
+    address alice = address(0xA11CE);
+
+    function setUp() public {
+        weth = new VulnerableWETH();
+    }
+
+    /// @notice counterexample: for any positive amount, batching two
+    ///         deposit() subcalls credits alice 2 * amount while she only
+    ///         paid amount. The `_fail` suffix follows the halmos
+    ///         convention that the assertion is expected to be violated.
+    function check_multicall_no_double_credit_fail(uint256 amount) external {
+        vm.assume(amount > 0);
+        vm.assume(amount < 2 ** 128);
+        vm.deal(alice, amount);
+
+        bytes[] memory data = new bytes[](2);
+        data[0] = abi.encodeWithSelector(VulnerableWETH.deposit.selector);
+        data[1] = abi.encodeWithSelector(VulnerableWETH.deposit.selector);
+
+        vm.prank(alice);
+        weth.multicall{value: amount}(data);
+
+        // credit should never exceed what alice actually paid
+        assertLe(weth.balanceOf(alice), amount);
+    }
+
+    /// @notice single-deposit control: without multicall, the invariant
+    ///         holds. This anchors the counterexample above to the
+    ///         payable-multicall pattern rather than to deposit() itself.
+    function check_single_deposit_no_over_credit_pass(uint256 amount) external {
+        vm.assume(amount > 0);
+        vm.assume(amount < 2 ** 128);
+        vm.deal(alice, amount);
+
+        vm.prank(alice);
+        weth.deposit{value: amount}();
+
+        assertLe(weth.balanceOf(alice), amount);
+    }
+}