[DicksonWu654]

Summary

• compare decoded bytes and string payloads as complete byte sequences with ==K
• apply the same comparison to the message overloads
• leave integer assertion decoding and comparison unchanged

Problem

The dynamic assertEq rules projected each decoded payload through #asWord before comparing it as an integer. Distinct ABI values can therefore collide: 0x01 and 0x0001 both project to integer 1, allowing an unequal bytes or string assertion to pass.

Fix

Keep the ABI offsets and lengths as integers, but retain the decoded dynamic payloads as Bytes and pass their full ==K equality result to #assert. This makes both content and length significant for the bytes and string overloads, including their message variants.

Regression coverage

• unequal bytes values 0x01 and 0x0001, with and without a message, are expected to fail
• unequal string byte sequences 0x01 and 0x0001, with and without a message, are expected to fail
• independently allocated equal 0x0001 values remain accepted for both types and both message forms

Validation

• git diff --check
• Tests were not run locally under the review constraint; upstream CI may perform execution.

[anvacaru]

@DicksonWu654The bug is real and the ==K fix in assert.md looks right (it also fixes the >32-byte case, where #asWord's chop keeps only the last 32 bytes, so two 33-byte strings differing only in the first byte compared equal).

However, the new tests don't exercise the changed rules. test-data/foundry/ installs an older version of forge-std 75f1746, where StdAssertions inherits DSTest and assertEq(bytes, bytes)/assertEq(string, string) are implemented in Solidity (keccak comparison + fail()), never calling the vm.assertEq cheatcode. So these tests should behave the same on main without the fix.

Cheatcode-level assertion tests live in the end-to-end project (src/tests/integration/test-data/test/Unit.t.sol, registered in end-to-end-prove-all), which is built via kontrol init with a current forge-std that routes to vm.assertEq. Please move the tests there. For example:

function test_assertEq_bytes_leading_zero_err() public {
    bytes memory a = hex"01";
    bytes memory b = hex"0001";
    vm.expectRevert("assertion failed");
    assertEq(a, b);
}

plus the string and , string err variants, a >32-byte case differing only in the first byte, and a positive equal-values case. You might also have to drop AssertEqDynamicTest.t.sol and the foundry-fail/foundry-prove-all entries.

Two related points:

• assertEq.Darray / assertEq.Darray.err have the same bug: #asWord(#range(ARGS, START, 32 *Int (1 +Int LEN))) keeps only the last element, so [1,5] vs [2,5] passes. The same ==K fix applies (the range already includes the length word). You can consider adding it here or in a follow-up.
• Could you add a symbolic case (e.g., bytes memory b = vm.freshBytes(40); assertEq(b, b);) to confirm ==K over symbolic Bytes still closes the proof?

[DicksonWu654]

@anvacaru sorry for the slow reply, and thanks for the really thorough review! Moved everything into Unit.t.sol, applied ==K to both Darray rules too (449e024 + f7741fd) and merged master. Two things differ from your example:

• the negative tests go through a small external helper, since Kontrol doesn't count a direct cheatcode call inside the expectRevert boundary (your example as written failed for that reason)
• I swapped the anonymous #let decoders for named functions. With the pinned K the anonymous helpers got mismatched Haskell/LLVM signatures and the booster segfaulted

All 12 proofs pass locally on K 7.1.337, including the freshBytes(40) symbolic case. With the old #asWord comparisons put back, the 10 negative tests fail and the 2 positive ones still pass