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 support for SuiteB and ECC primitives #1098

Closed
weaversa opened this issue Mar 1, 2021 · 3 comments · Fixed by #1342
Closed

Add support for SuiteB and ECC primitives #1098

weaversa opened this issue Mar 1, 2021 · 3 comments · Fixed by #1342
Assignees
Milestone

Comments

@weaversa
Copy link
Contributor

weaversa commented Mar 1, 2021

For my needs, I want to do a proof using w4_unint_yices and uninterpret these functions, but I can't currently load a Cryptol file that references these primitives.

You have encountered a bug in cryptol-saw-core's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-core/issues

%< --------------------------------------------------- 
  Revision:  ed0d14aa85818be4eb258832115ed77348ea8846
  Branch:    HEAD
  Location:  Unknown Cryptol primitive name
  Message:   PrimIdent (ModName "SuiteB") "AESKeyExpand"
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:628:29 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol
%< --------------------------------------------------- 
@brianhuffman brianhuffman self-assigned this Mar 12, 2021
@brianhuffman brianhuffman added this to the 0.8 milestone Mar 12, 2021
@brianhuffman
Copy link
Contributor

It shouldn't be too much work to add a stub for this primitive that can be treated as an uninterpreted function.

@atomb atomb modified the milestones: 0.8, 0.9 Apr 19, 2021
@weaversa
Copy link
Contributor Author

weaversa commented May 18, 2021

I think a quick and simple stub could be for saw to simply define these as undefined.

@brianhuffman
Copy link
Contributor

Yes, I'll just stub these out as undefined for now. Also I should extend the cryptol-test-suite to translate all of Cryptol's built-in modules, instead of just translating Cryptol.cry as it does now.

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 a pull request may close this issue.

3 participants