Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add ecEq back to cryptol_ss #1347

Open
RyanGlScott opened this issue Jun 21, 2021 · 2 comments · May be fixed by #1350
Open

Add ecEq back to cryptol_ss #1347

RyanGlScott opened this issue Jun 21, 2021 · 2 comments · May be fixed by #1350
Labels
subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core

Comments

@RyanGlScott
Copy link
Contributor

RyanGlScott commented Jun 21, 2021

As of 606c2f9, ecEq is excluded from cryptol_ss. 606c2f9 justified this exclusion due to the presence of ecEq_refl, but ecEq_refl was removed later in 45959b9. In light of this, we should revisit whether ecEq should be added back to cryptol_ss.

@RyanGlScott RyanGlScott added the subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core label Jun 21, 2021
RyanGlScott added a commit that referenced this issue Jun 22, 2021
@RyanGlScott RyanGlScott linked a pull request Jun 22, 2021 that will close this issue
@kiniry
Copy link
Member

kiniry commented Mar 29, 2024

It sounds like, given the conversation going on right now with Matt, we should prioritize this issue, assign it to a milestone associated with either our next release or ASAP, and assign it to a performer.

@RyanGlScott RyanGlScott changed the title Add ecEq back to cryptol_simpset Add ecEq back to cryptol_ss Mar 29, 2024
@RyanGlScott
Copy link
Contributor Author

To relay some additional context back from #1350:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants