Proof conventions 2 #1134
Merged
Proof conventions 2 #1134
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
force-pushed
the
proof-conventions2
branch
2 times, most recently
from
85a38f8
to
f39fd01
Compare
robdockins
force-pushed
the
proof-conventions2
branch
from
96c3688
to
8995741
Compare
atomb
approved these changes
Mar 31, 2021
| SatMulti stats vals -> do | ||
| res <- runProofScript tactic proofgoal | ||
| case res of | ||
| ValidProof stats _thm -> return stats -- TODO, do something with these theorems! |
There was a problem hiding this comment.
It might be valuable to store theorems in MethodSpecs? We'd want to check that it doesn't lead to significantly increased memory use, though, and it doesn't have to happen as part of this PR.
There was a problem hiding this comment.
Agreed. I discuss this a bit in #1136
| InvalidProof _ _ _ -> return False | ||
| UnfinishedProof _ -> | ||
| -- TODO? is this the right behavior? | ||
| do printOutLnTop Warn "Could not determine if preconditions are vacuous" |
There was a problem hiding this comment.
It seems like reasonable behavior to me, at least unless we see evidence to the contrary.
| , "Prefer to use 'admit', this command will eventually be removed." | ||
| ] | ||
|
|
||
| , prim "admit" "String -> ProofScript ()" |
There was a problem hiding this comment.
I like this change! Having an explanation for admitting a proof will help generate useful verification summaries, among other benefits.
| , "if '<prop>' is false, where '<example>' is a counter example." | ||
| , "If '<prop>' is a curried function, then '<example>' will be a tuple." | ||
| , "If the proof of <prop> was not finished, but we did not find a counterexample," | ||
| , "the example will run '<false> {{ () }}'" |
There was a problem hiding this comment.
This will likely lead to a type error in an argument designed to process a counter-example, but perhaps that's fine.
There was a problem hiding this comment.
Yeah, I wasn't entirely sure what else to do here.
It now accepts a `ProofGoal` and computes a `ProofResult`, which is either a completed proof, a counterexample to a subgoal of the proof, or an incomplete proof. All the primitives accepting `ProofScript` arguments are now work independently of what the proof script action computes. In addition, verification methods are more careful to check that all proof obligations are discharged, whereas previously they were not.
to return () instead of SatResult.
This takes a string message from the user describing why this goal is being admitted. We gently suggest in the help text to use `admit` instead of `assume_unsat` or `assume_valid` to start laying the groundwork for deprecating the latter.
to take a `Theorem` argument. Update the help documenation for `caseProofResult` and `caseSatResult` to indicate what happens in case of an "unknown" or "unfinished" result.
We strengthen the invariants on Prop to require that they have type saw-core type `Prop`, which is now possible because we fixed a bug in `scTypeOf`. Implement `boolToProp` to treat boolean terms as propositions.
robdockins
force-pushed
the
proof-conventions2
branch
from
8995741
to
eed686f
Compare
robdockins
added
the
PR: ready to merge
This was referenced Apr 14, 2021
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.
Round 2 of updating proof conventions. This mostly focuses on fixing #9 and #1099.