Skip to content

Fixing the implementation of uint128 - #396

Open
KelvinMYYZJ wants to merge 3 commits into
AeneasVerif:mainfrom
ssyram:int128_fix
Open

Fixing the implementation of uint128#396
KelvinMYYZJ wants to merge 3 commits into
AeneasVerif:mainfrom
ssyram:int128_fix

Conversation

@KelvinMYYZJ

Copy link
Copy Markdown

As discussed in #389, the AI-generated fallback implementation of uint128 contains several correctness issues.

This PR checks the implementation and fixes multiple problems:

  • Rewrite the multiplication implementation, with detailed comments explaining its correctness.
  • Fix signed integer comparison to correctly handle the sign bit.
  • Fix signed integer division to conform to the C standard semantics.
  • Fix right shift on signed integers to use arithmetic shifting, preserving the sign for negative values.

These changes improve the correctness and consistency of the fallback implementation, especially for signed arithmetic edge cases.

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