This repository has been archived by the owner on Jun 11, 2021. It is now read-only.
Make test binary load, translate, and typecheck Cryptol.cry.
#30
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Marked as draft until I get the test passing. |
|
As of 0042988, the test should be passing. |
brianhuffman
force-pushed
the
check-cryptol-prelude
branch
from
0042988
to
e3febda
Compare
added 3 commits
July 30, 2020 14:14
(This addresses part of #25.)
Previously the translator would try to apply the dictionary constructor `PSignedCmpWord`, which expects an argument of type `Nat`, to an argument of type `Num`. We now have a new function `PSignedCmpSeqBool` which expects an argument of type `Num`, just like the existing `PCmpSeqBool`.
This is another step toward addressing #25.
brianhuffman
force-pushed
the
check-cryptol-prelude
branch
from
e3febda
to
a48cce3
Compare
added 2 commits
July 30, 2020 14:33
Three cryptol fp primitives were missing: * fpIsFinite * fpToRational * fpFromRational Currently they are all implemented using the saw-core `error` function; real implementations will be needed eventually.
The extra cryptol code comprises two files: * superclass.cry * instance.cry These two files are copied from tests/regression in the cryptol repository, and are intended to test all the implicit subclass relationships and class instance rules of cryptol.
|
As of dc58a40 (which adds tests of cryptol code exercising all instance and subclass rules), there are a lot of translation failures due to missing class dictionaries. I'll have to implement all of them to get the test passing again. |
This is accomplished by defining new dictionary constructors in Cryptol.sawcore (currently mostly filled with `error` stubs) and then adding cases to the translator to use them to discharge class constraints. NOTE: This revision of cryptol-verifier uses the cryptol library functions `tIsRational` and `tIsFloat`, which were added in GaloisInc/cryptol#855. New instance rules: * Eq Rational * Cmp Rational * Zero Rational * Ring Rational * Field Rational * Round Rational * Literal Rational * Eq (Float e p) * Cmp (Float e p) * Field (Float e p) * Round (Float e p)
|
I think this is a good stopping point to merge the PR. |
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
(This addresses part of #25.)