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.

Sign up for GitHub

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

Jump to bottom

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 tech debt Issues that document or involve technical debt type: enhancement Issues describing an improvement to an existing feature or capability
Milestone
2025T1

Comments

@RyanGlScott
Copy link
Contributor

RyanGlScott commented Jun 21, 2021 •
edited
Loading

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
Include ecEq in cryptol_simpset
ea4ba3a 
Fixes #1347.
@RyanGlScott RyanGlScott linked a pull request Jun 22, 2021 that will close this issue
Draft
@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:

@sauclovian-g sauclovian-g added type: enhancement Issues describing an improvement to an existing feature or capability tech debt Issues that document or involve technical debt labels Nov 1, 2024
@sauclovian-g sauclovian-g added this to the 2025T1 milestone Nov 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core tech debt Issues that document or involve technical debt type: enhancement Issues describing an improvement to an existing feature or capability
Projects
None yet
Milestone
2025T1
Development

Successfully merging a pull request may close this issue.

Include ecEq in cryptol_ss GaloisInc/saw-script
3 participants
@kiniry @RyanGlScott @sauclovian-g