diff --git a/src/kontrol/kdist/assert.md b/src/kontrol/kdist/assert.md index ec47dc7ab..850f75395 100644 --- a/src/kontrol/kdist/assert.md +++ b/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") ... + #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") ... 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 ... + #assert (ARG1_VALUE ==K ARG2_VALUE) ERR_BYTES ... 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 -``` \ No newline at end of file +``` diff --git a/src/tests/integration/test-data/foundry-fail b/src/tests/integration/test-data/foundry-fail index 9b7014a8a..4aeef3647 100644 --- a/src/tests/integration/test-data/foundry-fail +++ b/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() diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all index c37ddfc25..852d24477 100644 --- a/src/tests/integration/test-data/foundry-prove-all +++ b/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() diff --git a/src/tests/integration/test-data/foundry/test/AssertEqDynamicTest.t.sol b/src/tests/integration/test-data/foundry/test/AssertEqDynamicTest.t.sol new file mode 100644 index 000000000..aaf680f0b --- /dev/null +++ b/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"); + } +}