Redo the sawscript ProofScript primitives

[brianhuffman]

There are various inconsistencies in the types of sawscript primitives related to ProofScripts. Currently we have:

simplify : Simpset -> ProofScript ()
unfolding : [String] -> ProofScript ()
abc, boolector, cvc4, mathsat, yices, z3 : ProofScript SatResult
offline_aig, offline_cnf, offline_extcore, offline_smtlib1, offline_smtlib2 : String -> ProofScript SatResult
external_aig_solver, external_cnf_solver : String -> [String] -> ProofScript SatResult
assume_unsat : ProofScript SatResult
assume_valid : ProofScript ProofResult
quickcheck : Int -> ProofScript SatResult

cec : AIG -> AIG -> TopLevel ProofResult
prove : {b} ProofScript b -> Term -> TopLevel ProofResult
prove_print : {b} ProofScript b -> Term -> TopLevel Theorem
sat : {b} ProofScript b -> Term -> TopLevel SatResult
sat_print : {b} ProofScript b -> Term -> TopLevel ()

java_verify_tactic : ProofScript SatResult -> JavaSetup ()
llvm_verify_tactic : ProofScript SatResult -> LLVMSetup ()

caseProofResult : {b} ProofResult -> b -> (Term -> b) -> b
caseSatResult : {b} SatResult -> b -> (Term -> b) -> b

Some proof tactics have type ProofScript (), some ProofScript SatResult, and others are ProofScript ProofResult. So far we don't have any examples of binding values within the ProofScript monad (e.g. sat do { x <- assume_valid; ... x ... }) so the types are not really helpful. The prove and sat commands work on type ProofScript b for any b; but for some reason java_verify_tactic and llvm_verify_tactic require ProofScript SatResult, which makes it impossible to use a proof script that uses only simplify, for example.

A related problem is the return types of prove vs prove_print. To create new rewrite rules for the simplifier, you need to produce a Theorem, but right now prove_print is the only way to do that; there is no way to produce a Theorem from a ProofResult, even using caseProofResult.

[brianhuffman]

A discussion is planned for Wednesday, June 10 to decide how we should implement proof goal states and proof tactics in saw-script. It appears that the representations of these will need to change significantly to get the features we want.

Here is a list of items we should cover during our discussion:

• Proof tactics should be able to fail
• Some (but not all) proof scripts should be able to return counterexamples to the user
• Proof tactics should be able to create multiple subgoals (e.g. induction over type Nat)
• How to represent variables: as lambda abstractions (as we do now) or as ExtCns (i.e. free variables) or both
• How to represent universally quantified vs. existentially quantified variables
• Proof states and theorems should keep track of which axioms and externally proved facts were used

@robdockins, @atomb, @ntc2: Anything to add?

[brianhuffman]

Some notes from the discussion yesterday (June 24):

• Some proof scripts should be able to return counterexamples. (Perhaps this can be determined by the type a in ProofScript a.)
• Counterexamples to subgoals should be converted to counterexamples of the original goal when possible. (This subsumes the idea of sending abstracted goals to e.g. z3 with uninterpreted functions. We can check to see if counterexamples involving uninterpreted functions are real or not before reporting them.)
• The ProofScript monad should support partial decision procedures: The result can be a proof, a counterexample, or nothing (failure). This covers tactics like trivial, which is just a really weak partial decision procedure.
• Handling failure: Tactics like abc might fail (timeout or unknown). The ProofScript monad should be based on a maybe monad. We probably don't need full backtracking yet (i.e. list monad), but it would be nice to leave that possibility open for the future.
• We need support for multiple subgoals. One use case is Java verifications that require multiple proofs: We can present them as a single proof state with a list of goals. Also, induction rules or case
  splitting rules can create multiple goals. When a tactic solves a goal it is removed from the list. A proof is complete when the list of goals is empty.
• SAT solving should be completely separated from proof scripts. The sat command should take only a solver argument, not a ProofScript argument. Tactics like abc and z3 should have type
  Solver instead of ProofScript. There should be a solve tactic of type Solver -> ProofScript.
• Proof states should only contain universally quantified variables. Existential quantifications are for the sat command only.
• An admit tactic will replace assume_unsat. It should take a string argument saying why we believe the truth of the goal.
• We should add a first-class ProofState type to SAWScript. This will let us do a bit of interactive proofs. What we'll need:
  1. A ProofScript command that saves the current ProofState to a file.
  2. TopLevel commands that load and save ProofStates to and from files.
  3. A TopLevel command (or pure function) for creating a ProofState from a Term.
  4. A TopLevel command that runs a ProofScript on a ProofState and returns the resulting ProofState.
• Dealing with local assumptions within ProofScripts: We should have a way to transform a goal of the form a --> b into a new subproof for b, giving the user a local Theorem object asserting a. This will be useful in particular for goals of the form x = y --> p, where we can use the theorem x = y to rewrite p.
• Theorems should be sequents (as in Isabelle) so that we can represent local assumptions as Theorems.
• Theorems should contain independently checkable proof certificates. Having them be independently checkable means that we don't have to worry as much about corner cases in the SAWCore semantics; the semantics will be handled by the checkers. Proof certificates should keep track of all subproofs that were completed by external oracles.
• TODO: Check polarity (i.e. logical negation or not) conventions for commands and tactics that save formulas to files.

[brianhuffman]

Based on the discussion, I'm thinking that the ProofScript monad will be encoded something like this in Haskell, like a state+IO+maybe monad:

newtype ProofScript a = ProofScript (ProofState -> IO (ProofResult a))

data ProofResult a = ProofFail | ProofCE CounterExample | ProofOK ProofState a

(In place of IO we will probably use TopLevel, so that proof scripts can access all the SAWScript-specific state and environment.)

In the definition of >>=, a ProofFail in either argument will cause the entire result to be ProofFail. A ProofCE in the first argument will cause the result to be the same counterexample. A ProofCE in the right argument is a bit more interesting: This is where we need to check to see whether the counterexample is still a counterexample for the original ProofState that was passed into the left argument.

[weaversa]

Is QBF support existing/planned? I just ask because of the note above --- "Proof states should only contain universally quantified variables."

It would be nice to have proofs with alternating quantifiers, though I guess we could assert that a proof always start with the universal quantifier.

[brianhuffman]

We still have the option of putting explicit exists and forall constants inside the proof goal. That note is supposed to mean that free variables in the goal are always interpreted as universally quantified.

[robdockins]

I think the bulk of what is discussed here has now been implemented via #1134.