Skip to content

Conversation

@jberthold
Copy link
Member

@jberthold jberthold commented Oct 28, 2025

  • The rvalueDiscriminant operation was unconditionally returning 128-bit integers, which turns out to be wrong. We now consult the layout to return the correct bit width (but still always unsigned as this seems to be an invariant).
    Closes Inconsistent uint types in proofs initialize_account* solana-token#41
  • Two special cases of transmute are implemented, removing thunks that transmute would have created before.
    • round-trip transmutes through a given type back to the original type are eliminated
    • for a transmute from an Integer to an enum without fields followed by a discriminant operation, the original integer value is returned as the discriminant.
  • the (partial) onInt function was missing preserves-definedness attributes on its equation so booster did not apply it

@jberthold jberthold marked this pull request as ready for review October 28, 2025 08:44
Copy link
Collaborator

@dkcumming dkcumming left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is good, no changes necessary from what I can see.

@jberthold jberthold merged commit 7d1807d into master Oct 28, 2025
7 checks passed
@jberthold jberthold deleted the better-discriminant-types branch October 28, 2025 23:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Inconsistent uint types in proofs initialize_account*

3 participants