handle truncated hashes

[karmacoma-eth]

Take these tests:

    function to_address(uint256 x) public pure returns (address) {
        return address(uint160(uint256(keccak256(abi.encode(x)))));
    }

    function test_uint256_collision(uint256 x, uint256 y) public {
        vm.assume(x != y);
        assertNotEq(keccak256(abi.encode(x)), keccak256(abi.encode(y)));
    }

    function test_uint160_collision(uint256 x, uint256 y) public {
        vm.assume(x != y);
        assertNotEq(
            to_address(x),
            to_address(y)
        );
    }

In practice, users expect both of these tests to pass, but we currently get this:

Counterexample: 
    p_x_uint256 = 0xc9f9ba1f6e4b6808f3aa7cdab4bc14386192bed28358d371c87772dbf274b154 (91356112056560583959377845884879365238336603841050490034690531698008218972500)
    p_y_uint256 = 0x0000000000000000000000000000000000000000000100000000000000000000 (1208925819614629174706176)
[FAIL] test_uint160_collision(uint256,uint256) (paths: 2, time: 0.08s (paths: 0.06s, models: 0.01s), bounds: [])
[PASS] test_uint256_collision(uint256,uint256) (paths: 1, time: 0.02s (paths: 0.02s, models: 0.00s), bounds: [])

This is because we model the injectivity of keccak256, but injectivity is lost once values are truncated. We can probably make a special case when the truncated value is 160 bits or more, because we don't really expect collisions at these sizes in practice.