Skip to content

Fix dynamic bytes and string assertEq equality - #1163

Open
DicksonWu654 wants to merge 1 commit into
runtimeverification:masterfrom
DicksonWu654:fix/dynamic-bytes-assertions
Open

Fix dynamic bytes and string assertEq equality#1163
DicksonWu654 wants to merge 1 commit into
runtimeverification:masterfrom
DicksonWu654:fix/dynamic-bytes-assertions

Conversation

@DicksonWu654

Copy link
Copy Markdown

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.

@DicksonWu654
DicksonWu654 marked this pull request as ready for review September 1, 2026 02:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant