Keccak lemma can cause important cases to be overlooked in a test

[lucasmt]

The keccak.md file currently includes a set of lemmas that can lead to important cases being missed in a test. Specifically, the problem are these lemmas (number 6 in the keccak.md file):

    rule [keccak-eq-conc-false]: keccak(_A)  ==Int _B => false [symbolic(_A), concrete(_B), simplification(30), comm]
    rule [keccak-neq-conc-true]: keccak(_A) =/=Int _B => true  [symbolic(_A), concrete(_B), simplification(30), comm]

    rule [keccak-eq-conc-false-ml-lr]: { keccak(A) #Equals B } => { true #Equals keccak(A) ==Int B } [symbolic(A), concrete(B), simplification]
    rule [keccak-eq-conc-false-ml-rl]: { B #Equals keccak(A) } => { true #Equals keccak(A) ==Int B } [symbolic(A), concrete(B), simplification]

The issue is that if B is the result of keccak(C), where C is a concrete value, then this lemma is unsound if A ==Int C, which is a case that's not hard to run into. In the example below, the test should fail in the case receiver == address(this), but instead it passes because the lemmas above cause the test to ignore this case. On the other hand, if we add the assumption receiver == address(this), the test fails as expected.

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.13;

import {Test} from "forge-std/Test.sol";
import {ERC20} from "@openzeppelin/contracts/token/ERC20/ERC20.sol";

contract MyERC20 is ERC20("TestToken", "TT") {}

contract SlotsDisjointTest is Test {
    MyERC20 public token;

    uint256 constant ETH_MAX = 2 ** 96 - 1;

    function setUp() public {
        token = new MyERC20();
        vm.setArbitraryStorage(address(token));
        uint256 totalSupply = vm.randomUint(0, ETH_MAX);
        vm.store(address(token), bytes32(uint256(2)), bytes32(totalSupply));

        uint256 balance = vm.randomUint(0, totalSupply);
        bytes32 balanceAccountSlot = keccak256(abi.encode(address(this), 0));
        vm.store(address(token), balanceAccountSlot, bytes32(balance));
    }

    function testReceiver(address receiver, uint256 amount) public {
        vm.assume(receiver != address(0));

        uint256 balance = token.balanceOf(address(this));
        vm.assume(amount <= balance);

        token.transfer(receiver, amount);

        vm.assertEq(token.balanceOf(address(this)), balance - amount);
    }
}

We should remove these lemmas from the keccak.md file and switch to an alternative way of handling comparisons between symbolic keccaks and concrete values. Two options would be

1. Add the necessary assumptions (e.g. keccak256(receiver) != keccak256(100)) directly to the test.
2. Turn off evaluation of keccak(C) even in the case where C is a constant. This would allow keccak(A) ==Int keccak(C) to be resolved by keccak lemma 5 (pseudo-injectiveness of keccak), and it would have the added benefit of making debugging easier, since otherwise it can be hard to figure out where a keccak hash comes from.

[braulov]

Hi! Is this issue still relevant?

I can take a look if helpful.