Merge pull request #1134 from GaloisInc/proof-conventions2

Proof conventions 2
GaloisInc · Apr 13, 2021 · 9b51cd1 · 9b51cd1
2 parents 46249db + 84012ac
commit 9b51cd1
Show file tree

Hide file tree

Showing 18 changed files with 552 additions and 392 deletions.
diff --git a/deps/saw-core b/deps/saw-core
diff --git a/examples/misc/prove.saw b/examples/misc/prove.saw
@@ -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.";
diff --git a/intTests/support/prove_or_die.saw b/intTests/support/prove_or_die.saw
@@ -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;

diff --git a/saw-remote-api/src/SAWServer/ProofScript.hs b/saw-remote-api/src/SAWServer/ProofScript.hs
@@ -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,
@@ -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
+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