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

Proof conventions #1102

Merged
merged 18 commits into from
Mar 15, 2021
Merged

Proof conventions #1102

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
3bd55bc
bump saw-core
robdockins Mar 8, 2021
c1c3bf9
Push more details of the proof calculus into SAWScript.Proof
robdockins Mar 2, 2021
c8921f1
Continue making the SAWScript proof abstractions stronger.
robdockins Mar 2, 2021
14b9dcd
Rework checking of "local hypothesis" theorems.
robdockins Mar 2, 2021
532b0b0
Refactor `Tactic` and make it opaque.
robdockins Mar 3, 2021
37f59ae
Change the SBV provers to use the new SATQuery datatype
robdockins Mar 3, 2021
2aeeef2
More work on making proof and solver conventions more uniform.
robdockins Mar 4, 2021
4485d7c
Update random testing to use first order values instead of
robdockins Mar 4, 2021
4e231c5
Use the new RME bitblasting method based on the SATQuery datatype.
robdockins Mar 5, 2021
b6d8660
Change the ABC prover to use the new SATQuery datatype
robdockins Mar 8, 2021
9efbe60
Update the What4-based solvers to use the new SATQuery convention
robdockins Mar 9, 2021
7dea5f9
Switch the external SAT solver to use the new SATQuery convention.
robdockins Mar 9, 2021
96c2eab
Change the `quickcheck` primitives to use the new random testing
robdockins Mar 10, 2021
899290c
Use evaulation to compute first order types instead of WHNF reduction.
robdockins Mar 10, 2021
f5a7384
Spellcheck
robdockins Mar 12, 2021
b9a4076
Fix a todo
robdockins Mar 12, 2021
af9556d
Move the external sat and abc prover into the ABC prover module
robdockins Mar 12, 2021
6ba092b
Merge remote-tracking branch 'origin/master' into proof-conventions
robdockins Mar 15, 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 12 files
+1 −1 cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+37 −3 saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs
+84 −1 saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
+23 −43 saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+1 −0 saw-core/saw-core.cabal
+42 −20 saw-core/src/Verifier/SAW/FiniteValue.hs
+1 −1 saw-core/src/Verifier/SAW/Prelude.hs
+68 −0 saw-core/src/Verifier/SAW/SATQuery.hs
+1 −1 saw-core/src/Verifier/SAW/SharedTerm.hs
+7 −5 saw-core/src/Verifier/SAW/Simulator/Concrete.hs
+38 −4 saw-core/src/Verifier/SAW/Simulator/RME.hs
+91 −131 saw-core/src/Verifier/SAW/Testing/Random.hs
524 changes: 156 additions & 368 deletions src/SAWScript/Builtins.hs
View file
Open in desktop

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions src/SAWScript/Crucible/JVM/Builtins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -268,9 +268,9 @@ verifyObligations cc mspec tactic assumes asserts =
let nm = mspec ^. csMethodName
stats <- forM (zip [(0::Int)..] asserts) $ \(n, (msg, assert)) -> do
goal <- io $ scImplies sc assume assert
goal' <- io $ scEqTrue sc goal
goal' <- io $ predicateToProp sc Universal goal
let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"]
proofgoal = ProofGoal n "vc" goalname (Prop goal')
proofgoal = ProofGoal n "vc" goalname goal'
r <- evalStateT tactic (startProof proofgoal)
case r of
Unsat stats -> return stats
Expand Down
12 changes: 6 additions & 6 deletions src/SAWScript/Crucible/LLVM/Builtins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -598,9 +598,9 @@ verifyObligations cc mspec tactic assumes asserts =
stats <-
forM (zip [(0::Int)..] asserts) $ \(n, (msg, assert)) ->
do goal <- io $ scImplies sc assume assert
goal' <- io $ scEqTrue sc goal
goal' <- io $ predicateToProp sc Universal goal
let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"]
proofgoal = ProofGoal n "vc" goalname (Prop goal')
proofgoal = ProofGoal n "vc" goalname goal'
r <- evalStateT tactic (startProof proofgoal)
case r of
Unsat stats -> return stats
Expand Down Expand Up @@ -751,7 +751,7 @@ assumptionsContainContradiction ::
TopLevel Bool
assumptionsContainContradiction cc tactic assumptions =
do
proofGoal <- io $
pgl <- io $
do
let sym = cc^.ccBackend
st <- Common.sawCoreState sym
Expand All @@ -760,9 +760,9 @@ assumptionsContainContradiction cc tactic assumptions =
assume <- scAndList sc (toListOf (folded . Crucible.labeledPred) assumptions)
-- implies falsehood
goal <- scImplies sc assume =<< toSC sym st (W4.falsePred sym)
goal' <- scEqTrue sc goal
return $ ProofGoal 0 "vc" "vacuousness check" (Prop goal')
evalStateT tactic (startProof proofGoal) >>= \case
goal' <- predicateToProp sc Universal goal
return $ ProofGoal 0 "vc" "vacuousness check" goal'
evalStateT tactic (startProof pgl) >>= \case
Unsat _stats -> return True
SatMulti _stats _vals -> return False

Expand Down
Loading