Skip to content

Conversation

@Stevengre
Copy link

No description provided.

@Stevengre Stevengre self-assigned this Jan 8, 2026
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 misses the mark. This does not match the p-token specification, it is similar but it is not the same. Our definition of equivalence is that we are using the same specification (with strictly necessary adjustments to account for the difference in the types included) to prove both implementations. Either the p-token harness needs to be changed to be same, or this should be changed to be the same as p-token. Realistically we should be able to diff the two postconditions and the only changes are because of the difference in the types.

@Stevengre
Copy link
Author

Stevengre commented Jan 8, 2026

we should be able to diff the two postconditions and the only changes are because of the difference in the types.

I love this idea. Let me align these two specs and try me best to make the diff to be minimal. If you think it is good, I can present another pr for all the other specs.

@Stevengre Stevengre requested a review from dkcumming January 9, 2026 02:52
@Stevengre Stevengre force-pushed the jh/fix_mint_to_checked_remote branch from 751e821 to c9c0883 Compare January 9, 2026 04:26
@Stevengre Stevengre force-pushed the jh/fix_mint_to_checked_remote branch from a77406d to 5352304 Compare January 12, 2026 04:41
@Stevengre
Copy link
Author

Maybe we can close this and use #150 directly.

@Stevengre Stevengre closed this Jan 14, 2026
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.

3 participants