Fix dynamic bytes and string assertEq equality

[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?