Various bugfixes #717
Various bugfixes #717
Conversation
The checking of argument types has been moved from `resolveArguments` into a separate function `checkSpecArgumentTypes`, which is called from both `crucible_llvm_verify` and `crucible_llvm_unsafe_assume_spec`. Fixes #707.
|
This seems to have broken the kyber proofs, possibly because of the argument type checking: http://fryingpan.dev.galois.com/hydra/build/3412946/log |
|
What I think you meant to say is, this has revealed that the kyber proofs were already broken :) |
|
But seriously, where can I find these kyber proofs so I can test them and fix them? |
|
I've fixed this problem- a Cryptol literal being passed as an argument was annotated as The Kyber proof is available on the external GitLab. I think you should have access there @brianhuffman. |
There was a problem hiding this comment.
I've looked at all the different changes, they look good! Thank you @brianhuffman
| @@ -180,10 +180,10 @@ ppOverrideFailureReason :: | |||
| ) => OverrideFailureReason ext -> PP.Doc | |||
| ppOverrideFailureReason rsn = case rsn of | |||
| AmbiguousPointsTos pts -> | |||
| PP.text "ambiguous collection of points-to assertions" PP.<$$> | |||
| PP.text "LHS of points-to assertion(s) not reachable via points-tos from inputs/outputs:" PP.<$$> | |||
There was a problem hiding this comment.
"not reachable" -> "not uniquely determined"?
There was a problem hiding this comment.
Is there a situation where a variable could be determined, but not uniquely so?
| (PP.indent 2 $ PP.vcat (map PP.pretty pts)) | ||
| AmbiguousVars vs -> | ||
| PP.text "ambiguous collection of variables" PP.<$$> | ||
| PP.text "Fresh variable(s) not reachable via points-tos from function inputs/outputs:" PP.<$$> |
There was a problem hiding this comment.
"not reachable" -> "not uniquely determined"?
There was a problem hiding this comment.
All of the small changes look good. Some of the large blocks of additions and deletions are clearly just reformatting, but some aren't quite as obvious. I haven't carefully looked over some of those. If they do include functional changes, I can look more closely.
|
@atomb you might like to try looking at each commit separately, instead of the overall diff. The reformatting was separated into its own commit. |
|
Ah, right, of course. Looking at the individual commits (but ignoring the reformatting one), I think it all looks good. |
Having a bunch of separate parallel pull requests was going to get unwieldy, and merging was going to make a big mess of the commit history, so I'm combining a few separate PRs into this new one (#714, #715, #716).
This PR contains fixes for #691, #698, and #707.
EDIT: Also #701.