Fix dynamic bytes and string assertEq equality

src/kontrol/kdist/assert.md

@@ -97,9 +97,9 @@ Capturing cheat code calls
                #let ARG2_START = #asWord(#range(ARGS, 32, 32)) #in
                #let ARG1_LEN   = #asWord(#range(ARGS, ARG1_START, 32)) #in
                #let ARG2_LEN   = #asWord(#range(ARGS, ARG2_START, 32)) #in
-               #let ARG1_VALUE = #asWord(#range(ARGS, 32 +Int ARG1_START, ARG1_LEN)) #in
-               #let ARG2_VALUE = #asWord(#range(ARGS, 32 +Int ARG2_START, ARG2_LEN)) #in
-                 #assert_eq ARG1_VALUE ARG2_VALUE String2Bytes("assertion failed") ... </k>
+               #let ARG1_VALUE = #range(ARGS, 32 +Int ARG1_START, ARG1_LEN) #in
+               #let ARG2_VALUE = #range(ARGS, 32 +Int ARG2_START, ARG2_LEN) #in
+                 #assert (ARG1_VALUE ==K ARG2_VALUE) String2Bytes("assertion failed") ... </k>
       requires SELECTOR ==Int selector ( "assertEq(string,string)" )
         orBool SELECTOR ==Int selector ( "assertEq(bytes,bytes)" )
     [preserves-definedness]
@@ -140,10 +140,10 @@ Capturing cheat code calls
               #let ARG1_LEN   = #asWord(#range(ARGS, ARG1_START, 32)) #in
               #let ARG2_LEN   = #asWord(#range(ARGS, ARG2_START, 32)) #in
               #let ERR_LEN    = #asWord(#range(ARGS,  ERR_START, 32)) #in
-              #let ARG1_VALUE = #asWord(#range(ARGS, 32 +Int ARG1_START, ARG1_LEN)) #in
-              #let ARG2_VALUE = #asWord(#range(ARGS, 32 +Int ARG2_START, ARG2_LEN)) #in
+              #let ARG1_VALUE = #range(ARGS, 32 +Int ARG1_START, ARG1_LEN) #in
+              #let ARG2_VALUE = #range(ARGS, 32 +Int ARG2_START, ARG2_LEN) #in
               #let ERR_BYTES  = #range(ARGS, 32 +Int ERR_START, ERR_LEN) #in
-                #assert_eq ARG1_VALUE ARG2_VALUE ERR_BYTES ... </k>
+                #assert (ARG1_VALUE ==K ARG2_VALUE) ERR_BYTES ... </k>
       requires SELECTOR ==Int selector ( "assertEq(string,string,string)" )
         orBool SELECTOR ==Int selector ( "assertEq(bytes,bytes,string)" )
     [preserves-definedness]
@@ -330,4 +330,4 @@ Function selectors
 
 ```k
 endmodule
-```
+```

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

@@ -6,3 +6,7 @@ AssertTest.test_revert_branch(uint256,uint256)
 AssumeTest.test_assume_false(uint256,uint256)
 AssumeTest.testFail_assume_false(uint256,uint256)
 ImmutableVarsTest.test_run_deployment(uint256)
+AssertEqDynamicTest.test_assert_eq_bytes_distinguishes_leading_zero()
+AssertEqDynamicTest.test_assert_eq_bytes_with_message_distinguishes_leading_zero()
+AssertEqDynamicTest.test_assert_eq_string_distinguishes_leading_zero()
+AssertEqDynamicTest.test_assert_eq_string_with_message_distinguishes_leading_zero()

src/tests/integration/test-data/foundry-prove-all

@@ -356,3 +356,4 @@ WarpTest.test_warp_setup()
 FreshBytesTest.test_symbolic_bytes_1
 FreshBytesTest.test_symbolic_bytes_3
 FreshBytesTest.test_symbolic_bytes_length
+AssertEqDynamicTest.test_assert_eq_equal_dynamic_values()

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

@@ -0,0 +1,44 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+import "forge-std/Test.sol";
+
+contract AssertEqDynamicTest is Test {
+    function test_assert_eq_bytes_distinguishes_leading_zero() public {
+        bytes memory shortValue = hex"01";
+        bytes memory leadingZeroValue = hex"0001";
+
+        assertEq(shortValue, leadingZeroValue);
+    }
+
+    function test_assert_eq_bytes_with_message_distinguishes_leading_zero() public {
+        bytes memory shortValue = hex"01";
+        bytes memory leadingZeroValue = hex"0001";
+
+        assertEq(shortValue, leadingZeroValue, "different byte sequences");
+    }
+
+    function test_assert_eq_string_distinguishes_leading_zero() public {
+        bytes memory shortValue = hex"01";
+        bytes memory leadingZeroValue = hex"0001";
+
+        assertEq(string(shortValue), string(leadingZeroValue));
+    }
+
+    function test_assert_eq_string_with_message_distinguishes_leading_zero() public {
+        bytes memory shortValue = hex"01";
+        bytes memory leadingZeroValue = hex"0001";
+
+        assertEq(string(shortValue), string(leadingZeroValue), "different string sequences");
+    }
+
+    function test_assert_eq_equal_dynamic_values() public {
+        bytes memory first = hex"0001";
+        bytes memory second = hex"0001";
+
+        assertEq(first, second);
+        assertEq(first, second, "equal byte sequences");
+        assertEq(string(first), string(second));
+        assertEq(string(first), string(second), "equal string sequences");
+    }
+}