Fast F2 polynomial arithmetic #923
Merged
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
robdockins
commented
Oct 2, 2020
| @@ -257,12 +260,22 @@ prepareQuery sym ProverCommand { .. } = | |||
| simulate args = | |||
| do let lPutStrLn = M.withLogger logPutStrLn | |||
| when pcVerbose (lPutStrLn "Simulating...") | |||
|
|
|||
There was a problem hiding this comment.
This following sequence feels like a bit of a hack. Binding the top-level decls of the module using EWhere does seem to work, but feels pretty dirty. Any ideas how to handle this better, @brianhuffman, @yav?
|
I haven't thought of any especially better way to handle the primitive redirection. We'll just have to be sure we don't rely too much on CAFs being evaluated only once. |
robdockins
force-pushed
the
fast-f2
branch
2 times, most recently
from
cfee6a7 to
7bf93c1
Compare
Ths allows larger concrete bitvector values before falling back on the "sparse" representation. This is a bit of a bandaid for the underlying problem, which I have some ideas how to fix later.
a new `Cryptol::Reference` module. Change the evaluator API slightly so that primitives can be bound to expressions, in addition to values. We can use this to inject the reference implementations of the above operations into the symbolic evaluators. Because of the exact way evaluation environments are piped around, the bound expression will be evaluated in the environment that the primitive symbol is declared. So, we can't just reference the name of the reference implementation when we inject it. Instead, we abuse the `EWhere` construct to add local definitions corresponding to the entire module. This works, but is a bit unsatisfying, as any top-level CAFs will not be shared across different invocations. This doesn't matter for these functions, but might for e.g, AES.
the reference implementations. The `:check` commands are really the only ones of interest for correctness of the algorithms. The `:prove` commands end up just checking the reference implementation against itself, but this checks that the primitive redirection code is working properly.
"Loading module" message. This is used when we implicitly load reference implementation modules.
This was referenced Oct 28, 2020
robdockins
added a commit
to GaloisInc/saw-core
that referenced
this pull request
Oct 28, 2020
Updates to track Cryptol PRs GaloisInc/cryptol#923 and GaloisInc/cryptol#940
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Add new primitives for
pmult,pdivandpmod. Currently, these are exposed in the prelude via new symbols namedfast_pmult,fast_pdivandfast_pmod. The plan is to relocate the current in-Cryptol implementations to a reference implementation module and continue to use these definitions for the symbolic backends, along the lines suggested in #922.These still require additional testing, but seem to work correctly on a limited selection of tests.