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.

Sign up for GitHub

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

Jump to bottom

Proof conventions 2 #1134

Merged
merged 11 commits into from
Apr 13, 2021
Merged

Proof conventions 2 #1134

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
4c314b6
Make `ProofScript` into a newtype.
robdockins Mar 16, 2021
0bd1faf
Rework the `runProofScript` method.
robdockins Mar 17, 2021
34c36d4
Change the user-facing type of prover tactics
robdockins Mar 17, 2021
20c4e6f
Use new bitblasting primitives intead of old ones slated for removal.
robdockins Mar 17, 2021
186dba4
bump saw-core to remove some obsolete code
robdockins Mar 17, 2021
aa02aef
Add a new `admit` tactic.
robdockins Mar 17, 2021
e057bef
Haddocs for the `CEX` and `ProofResult` types.
robdockins Mar 17, 2021
7ff1680
Update `caseProofResult` to allow the valid branch
robdockins Mar 17, 2021
099eeac
Communicate counterexamples with `ExtCns` names instead of `String`.
robdockins Mar 17, 2021
eed686f
Check `Prop` more strictly; implement `boolToProp`.
robdockins Mar 18, 2021
84012ac
bump saw-core to master
robdockins Apr 13, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion deps/saw-core
Open in desktop
Submodule saw-core updated 7 files
+2 −0 cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
+1 −16 saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs
+10 −86 saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
+2 −3 saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+1 −1 saw-core/prelude/Prelude.sawcore
+7 −1 saw-core/src/Verifier/SAW/SharedTerm.hs
+1 −28 saw-core/src/Verifier/SAW/Simulator/RME.hs
2 changes: 1 addition & 1 deletion examples/misc/prove.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,6 @@
let f = {{ \ (x : [8]) -> (x + x) == (1 * x) }};
r <- prove abc f;
caseProofResult r
(print "Q.E.D.")
(\thm -> print "Q.E.D.")
(\v -> do { print "Oops." ; print v; print {{ f v }}; });
print "Done.";
2 changes: 1 addition & 1 deletion intTests/support/prove_or_die.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ let prove_or_die name thm = do {
print name;
r <- prove abc thm;
caseProofResult r
(print "True")
(\thm -> print "True")
(\c -> do {
print "False";
exit 1;
Expand Down
8 changes: 5 additions & 3 deletions saw-remote-api/src/SAWServer/ProofScript.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ import qualified Argo
import qualified Argo.Doc as Doc
import qualified SAWScript.Builtins as SB
import qualified SAWScript.Value as SV
import qualified SAWScript.Proof as PF
import SAWServer
( ServerVal(VTerm, VSimpset),
ServerName,
Expand Down Expand Up @@ -170,10 +171,11 @@ prove params = do
proofScript <- interpretProofScript (ppScript params)
res <- tl $ SB.provePrim proofScript t
case res of
SV.Valid _ -> return ProofValid
SV.InvalidMulti _ _ -> return ProofInvalid
PF.ValidProof{} -> return ProofValid
PF.InvalidProof{} -> return ProofInvalid
PF.UnfinishedProof{} -> return ProofInvalid

interpretProofScript :: ProofScript -> Argo.Command SAWState (SV.ProofScript SV.SatResult)
interpretProofScript :: ProofScript -> Argo.Command SAWState (SV.ProofScript ())
interpretProofScript (ProofScript ts) = go ts
where go [UseProver ABC] = return $ SB.proveABC
go [UseProver (CVC4 unints)] = return $ SB.proveUnintCVC4 unints
Expand Down
Loading