halmos-differential-erc20

Halmos Differential Tests for Common ERC-20 Token Implementations

Description

This test uses N msg.senders to execute N arbitrary calls (using the new createCalldata cheatcode) and 1 arbitrary staticcall to see if the view functions return the same thing after changing the state

Notes

• Error messages won't be the same, so checking for call success & return value does not work if the call fails
• OpenZeppelin will revert when transferring to address(0) while the others won't. There's a concrete counterexample showing that
• Manually introducing a bug in any of the implementations is quickly detected by the Halmos test

Results

$ halmos
[⠢] Compiling...
[⠑] Compiling 3 files with Solc 0.8.27
[⠃] Solc 0.8.27 finished in 1.43s
Compiler run successful with warnings:
Warning (5740): Unreachable code.
   --> lib/solmate/src/tokens/ERC20.sol:135:25:
    |
135 |                         keccak256(
    |                         ^ (Relevant source part starts here and spans across multiple lines).

Warning (5740): Unreachable code.
   --> lib/solmate/src/tokens/ERC20.sol:156:13:
    |
156 |             allowance[recoveredAddress][spender] = value;
    |             ^ (Relevant source part starts here and spans across multiple lines).


Running 1 tests for test/ERC20.t.sol:ERC20Test
[PASS] check_differential_erc20(address[]) (paths: 15657, time: 2119.80s, bounds: [senders=[2]])
Symbolic test result: 1 passed; 0 failed; time: 2120.02s