test: regression for payable-multicall counterexample (#178)

[michael-moffett]

Closes #178.

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

What the test does

• Defines an abstract Multicall mirroring the Uniswap V3 Periphery
  shape (payable, address(this).delegatecall per element).
• Defines VulnerableWETH, a minimal deposit-shaped contract that
  reads msg.value for accounting.
• check_multicall_no_double_credit_fail(uint256) asserts that a
  caller's balance after a two-element multicall of deposit() is
  bounded by msg.value. Halmos finds the counterexample: any positive
  amount credits the caller 2 * amount.
• check_single_deposit_no_over_credit_pass(uint256) is a control:
  the invariant holds under a plain single deposit(), which anchors
  the failure to the payable-multicall pattern rather than to
  deposit() itself.

Local verification

$ halmos --root tests/regression --contract PayableMulticallTest
Running 2 tests for test/PayableMulticall.t.sol:PayableMulticallTest
Counterexample:
    p_amount_uint256_..._00 = 0x80000000000000000000000000000000
[FAIL] check_multicall_no_double_credit_fail(uint256) (paths: 3, ...)
[PASS] check_single_deposit_no_over_credit_pass(uint256) (paths: 1, ...)
Symbolic test result: 1 passed; 1 failed; time: 0.18s

Full regression harness (pytest tests/test_halmos.py -k tests/regression)
passes with the corresponding entries added to tests/expected/all.json.

Notes

• Naming follows the halmos _fail / _pass suffix convention seen in
  Arith.t.sol and elsewhere to make the intended verdict explicit.
• The Multicall and VulnerableWETH contracts are inlined in the
  test file, matching the style used by SmolWETH.t.sol.
• No changes to src/, solver config, or CI wiring.
• Drafted with AI assistance; the shape, contract minimization, and
  counterexample were validated by running halmos locally against the
  full regression suite (12/13 pytest targets green on this workstation;
  the tests/ffi target failure is unrelated; it needs --ffi
  enabled and does not intersect with this PR).