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

Opaque constants #1453

Merged
merged 3 commits into from
Sep 13, 2021
Merged

Opaque constants #1453

merged 3 commits into from
Sep 13, 2021

Conversation

robdockins
Copy link
Contributor

This PR adds a notion of "opaque constant" to saw-core. These are Constant nodes that have no definition. They are similar in many ways to ExtCns, but are explicitly not subject to substitution.

In particular, opaque constants are allowed to appear in the definition of other constants, whereas ExtCns are not (CF discussion on #1430).

In cryptol-saw-core, if a primitive declaration appears in a Cryptol module that is not one of the well-known primitives from the built-in modules we support, it is translated into an opaque constant. In saw-core-coq, opaque constants are translated into Coq Parameter declarations. The end result is that we can posit and reason about abstract Cryptol functions in Coq.

Note, this is based on #1423, only the final two commits properly belong to this PR.

@robdockins
Copy link
Contributor Author

Whoops, I rebased those commits in the wrong order. I'll fix that in a rebase after #1423 lands.

Copy link
Contributor

@brianhuffman brianhuffman left a comment

Choose a reason for hiding this comment

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

Looks good to me, just like we talked about.

These are just `Constant` terms that have no definition.
They are similar to `ExtCns`, except that they are not subject
to substitution.  As a consequence, opaque constants are allowed
to appear in the definition of other constants without being
abstracted over.  Opauqe constants never reduce, and must be
treated as unintepreted in proofs.
`primitive` declarations from Cryptol into `Parameter`
declarations in Coq.

In the Coq generator, distinguish between `ExtCns` values
and opauqe constants.  ExtCns values are translated using
the Coq `Variable` declaration, wherease opaque constants
are translated using the `Parameter` declaration.
At top-level, these declarations are essentially the same.
However `Parameter` interacts with the module system,
whereas `Variable` interacts with the section mechanism.
Currently, we make use of neither, but the distinction
may eventually be useful.
@robdockins robdockins marked this pull request as ready for review September 13, 2021 21:58
@robdockins robdockins merged commit ec73f82 into master Sep 13, 2021
@mergify mergify bot deleted the primitive-parameter branch September 13, 2021 22:00
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.

2 participants