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

Allow importing Cryptol foreign functions #1920

Merged
merged 11 commits into from
Sep 1, 2023
Merged

Allow importing Cryptol foreign functions #1920

merged 11 commits into from
Sep 1, 2023

Conversation

qsctr
Copy link
Contributor

@qsctr qsctr commented Aug 29, 2023

If there exists a Cryptol implementation of the foreign function, then we import it into SAWCore as a Cryptol expression, in the same way that we do for normal Cryptol bindings. If not, then we introduce it as an opaque constant with no definition, the same way we deal with unknown primitives.

This requires an update of the cryptol submodule so that we have support for Cryptol implementations of foreign functions.

qsctr added 2 commits August 28, 2023 16:47
to access cryptol implementations of foreign functions
@qsctr qsctr added type: enhancement Issues describing an improvement to an existing feature or capability PR: submodule bump Pull requests that include a submodule bump labels Aug 29, 2023
@qsctr qsctr self-assigned this Aug 29, 2023
@qsctr qsctr marked this pull request as ready for review August 29, 2023 01:26
@qsctr qsctr requested a review from andreistefanescu August 29, 2023 01:26
Copy link
Contributor

@RyanGlScott RyanGlScott left a comment

Choose a reason for hiding this comment

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

Thanks, @qsctr! Aside from the comments below, it would be worth mentioning this in the CHANGES.md file and the SAW manual (under doc/manual), as this is a user-facing feature.

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs Outdated Show resolved Hide resolved
cryptol-saw-core/src/Verifier/SAW/Cryptol.hs Outdated Show resolved Hide resolved
cryptol-saw-core/src/Verifier/SAW/Cryptol.hs Outdated Show resolved Hide resolved
cryptol-saw-core/src/Verifier/SAW/Cryptol.hs Outdated Show resolved Hide resolved
Copy link
Contributor

@andreistefanescu andreistefanescu left a comment

Choose a reason for hiding this comment

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

👍

@qsctr qsctr added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Sep 1, 2023
@mergify mergify bot merged commit d565fe6 into master Sep 1, 2023
@mergify mergify bot deleted the import-foreign branch September 1, 2023 11:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run PR: submodule bump Pull requests that include a submodule bump type: enhancement Issues describing an improvement to an existing feature or capability
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants