Remove lemma 6 from keccak.md

src/kontrol/kdist/keccak.md

@@ -47,16 +47,6 @@ This assumption reflects that hypothesis in the context of formal verification,
     rule [keccak-inj-ml]: { keccak(A) #Equals keccak(B) } => { true #Equals A ==K B } [simplification]
 ```
 
-6. `keccak` of a symbolic parameter does not equal a concrete value. This lemma is based on our experience in Foundry-supported testing and is specific to how `keccak` functions are used in practical symbolic execution. The underlying hypothesis that justifies it is that the storage slots of a given mapping are presumed to be disjoint from slots of other mappings and also the non-mapping slots of a contract.
-
-```k
-    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]
-```
-
 ```k
 endmodule
 ```

src/tests/integration/test-data/foundry-fail

@@ -6,3 +6,4 @@ AssertTest.test_revert_branch(uint256,uint256)
 AssumeTest.test_assume_false(uint256,uint256)
 AssumeTest.testFail_assume_false(uint256,uint256)
 ImmutableVarsTest.test_run_deployment(uint256)
+SlotsDisjointTest.testReceiver(address,uint256)

src/tests/integration/test-data/foundry/test/SlotsDisjoint.t.sol

@@ -0,0 +1,78 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.20;
+
+import {Test} from "forge-std/Test.sol";
+import {KontrolCheats} from "kontrol-cheatcodes/KontrolCheats.sol";
+
+contract MyERC20 {
+    mapping(address account => uint256) private _balances;
+
+    uint256 private _totalSupply;
+
+    function totalSupply() public view virtual returns (uint256) {
+        return _totalSupply;
+    }
+
+    function balanceOf(address account) public view virtual returns (uint256) {
+        return _balances[account];
+    }
+
+    function transfer(address to, uint256 value) public virtual returns (bool) {
+        require(to != address(0));
+        require(value <= _balances[msg.sender]);
+
+        _balances[msg.sender] -= value;
+        _balances[to] += value;
+
+        return true;
+    }
+}
+
+/**
+ * This test demonstrates a problem with the keccak lemmas previously present in
+ * the keccak.md file, which could cause us to miss edge cases in a test. In
+ * particular, the lemma
+ *
+ * rule [keccak-eq-conc-false]: keccak(_A)  ==Int _B => false
+ *     [symbolic(_A), concrete(_B), simplification(30), comm]
+ *
+ * overlooks the case when _B is the keccak of a concrete value and that value
+ * can be equal to _A. With this lemma, the test below passes when it shouldn´t.
+ */
+contract SlotsDisjointTest is Test, KontrolCheats {
+    MyERC20 public token;
+
+    function setUp() public {
+        token = new MyERC20();
+        kevm.symbolicStorage(address(token));
+        uint256 totalSupply = freshUInt256();
+        vm.store(address(token), bytes32(uint256(2)), bytes32(totalSupply));
+
+        // Assign balance to the test contract
+        uint256 balance = freshUInt256();
+        bytes32 balanceAccountSlot = keccak256(abi.encode(address(this), 0));
+        vm.store(address(token), balanceAccountSlot, bytes32(balance));
+    }
+
+    /**
+     * This test should fail because it's possible for receiver == address(this)
+     * in which case the final assertion doesn't hold. With the above lemma, we
+     * miss this case and the test passes. Without the lemma, the tests fails as
+     * it should.
+     */
+    function testReceiver(address receiver, uint256 amount) public {
+        vm.assume(receiver != address(0));
+
+        uint256 senderBalance = token.balanceOf(address(this));
+        vm.assume(amount <= senderBalance);
+
+        uint256 receiverBalance = token.balanceOf(receiver);
+        vm.assume(receiverBalance <= type(uint256).max - amount);
+
+        token.transfer(receiver, amount);
+
+        // This should fail when receiver == address(this)
+        assertEq(token.balanceOf(address(this)), senderBalance - amount);
+        assertEq(token.balanceOf(receiver), receiverBalance + amount);
+    }
+}

src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected

@@ -4,7 +4,6 @@
 │   pc: 0
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: test/nested/SimpleNested.t.sol:7:11
 │   method: test%AssertTest.setUp()
 │
 │  (182 steps)
@@ -13,7 +12,6 @@
 │   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
-│   src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
 │   method: test%AssertTest.setUp()
 │
 │  (1 step)
@@ -22,7 +20,6 @@
 │   pc: 0
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: test/nested/SimpleNested.t.sol:7:11
 │   method: test%AssertTest.checkFail_assert_false()
 │
 │  (307 steps)

src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected

@@ -4,7 +4,6 @@
 │   pc: 0
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: test/nested/SimpleNested.t.sol:7:11
 │   method: test%AssertTest.setUp()
 │
 │  (182 steps)
@@ -13,7 +12,6 @@
 │   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
-│   src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
 │   method: test%AssertTest.setUp()
 │
 │  (1 step)
@@ -22,7 +20,6 @@
 │   pc: 0
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: test/nested/SimpleNested.t.sol:7:11
 │   method: test%AssertTest.testFail_assert_true()
 │
 │  (200 steps)
@@ -31,7 +28,6 @@
 │   pc: 328
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
 │   method: test%AssertTest.testFail_assert_true()
 │
 │  (1 step)
@@ -40,7 +36,6 @@
 │   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
-│   src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
 │   method: test%AssertTest.testFail_assert_true()
 │
 │  (2 steps)
@@ -49,7 +44,6 @@
     pc: 328
     callDepth: 0
     statusCode: EVMC_SUCCESS
-    src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
     method: test%AssertTest.testFail_assert_true()
 
 

src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected

@@ -4,7 +4,6 @@
 │   pc: 0
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: test/nested/SimpleNested.t.sol:7:11
 │   method: test%AssertTest.setUp()
 │
 │  (182 steps)
@@ -13,7 +12,6 @@
 │   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
-│   src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
 │   method: test%AssertTest.setUp()
 │
 │  (1 step)
@@ -22,7 +20,6 @@
 │   pc: 0
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: test/nested/SimpleNested.t.sol:7:11
 │   method: test%AssertTest.testFail_expect_revert()
 │
 │  (417 steps)
@@ -31,7 +28,6 @@
 │   pc: 811
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: lib/forge-std/src/StdInvariant.sol:78:78
 │   method: test%AssertTest.testFail_expect_revert()
 │
 │  (1 step)
@@ -40,7 +36,6 @@
 │   pc: 811
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: lib/forge-std/src/StdInvariant.sol:78:78
 │   method: test%AssertTest.testFail_expect_revert()
 │
 │  (230 steps)
@@ -49,7 +44,6 @@
 │   pc: 892
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: lib/forge-std/src/StdInvariant.sol:78:78
 │   method: test%AssertTest.testFail_expect_revert()
 │
 │  (1 step)
@@ -58,7 +52,6 @@
 │   pc: 892
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: lib/forge-std/src/StdInvariant.sol:78:78
 │   method: test%AssertTest.testFail_expect_revert()
 │
 │  (18 steps)
@@ -67,7 +60,6 @@
 │   pc: 0
 │   callDepth: 1
 │   statusCode: STATUSCODE:StatusCode
-│   src: test/nested/SimpleNested.t.sol:7:11
 │   method: test%AssertTest.call_assert_false()
 │
 │  (1 step)
@@ -76,7 +68,6 @@
 │   pc: 0
 │   callDepth: 1
 │   statusCode: STATUSCODE:StatusCode
-│   src: test/nested/SimpleNested.t.sol:7:11
 │   method: test%AssertTest.call_assert_false()
 │
 │  (319 steps)
@@ -117,7 +108,6 @@
 │   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
-│   src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
 │   method: test%AssertTest.testFail_expect_revert()
 │
 │  (1 step)
@@ -126,7 +116,6 @@
 │   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
-│   src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
 │   method: test%AssertTest.testFail_expect_revert()
 │
 │  (2 steps)
@@ -135,7 +124,6 @@
     pc: 328
     callDepth: 0
     statusCode: EVMC_SUCCESS
-    src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
     method: test%AssertTest.testFail_expect_revert()
 
 

src/tests/integration/test-data/show/AssertTest.test_assert_false().expected

@@ -4,7 +4,6 @@
 │   pc: 0
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: test/nested/SimpleNested.t.sol:7:11
 │   method: test%AssertTest.setUp()
 │
 │  (182 steps)
@@ -13,7 +12,6 @@
 │   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
-│   src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
 │   method: test%AssertTest.setUp()
 │
 │  (1 step)
@@ -22,7 +20,6 @@
 │   pc: 0
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: test/nested/SimpleNested.t.sol:7:11
 │   method: test%AssertTest.test_assert_false()
 │
 │  (307 steps)

src/tests/integration/test-data/show/AssertTest.test_assert_true().expected

@@ -4,7 +4,6 @@
 │   pc: 0
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: test/nested/SimpleNested.t.sol:7:11
 │   method: test%AssertTest.setUp()
 │
 │  (182 steps)
@@ -13,7 +12,6 @@
 │   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
-│   src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
 │   method: test%AssertTest.setUp()
 │
 │  (1 step)
@@ -22,7 +20,6 @@
 │   pc: 0
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: test/nested/SimpleNested.t.sol:7:11
 │   method: test%AssertTest.test_assert_true()
 │
 │  (263 steps)
@@ -31,7 +28,6 @@
 │   pc: 328
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
-│   src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
 │   method: test%AssertTest.test_assert_true()
 │
 │  (1 step)
@@ -40,7 +36,6 @@
 │   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
-│   src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
 │   method: test%AssertTest.test_assert_true()
 │
 │  (2 steps)
@@ -49,7 +44,6 @@
 │   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
-│   src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
 │   method: test%AssertTest.test_assert_true()
 │
 ┊  constraint: true