Proof conventions #1102
Proof conventions #1102
Conversation
|
@brianhuffman, this PR isn't really done yet, but there are a number of changes I'm working on to the proof state management and such that I think it would be worthwhile to have your early input on. |
robdockins
force-pushed
the
proof-conventions
branch
5 times, most recently
from
8598350 to
f4f53d7
Compare
robdockins
force-pushed
the
proof-conventions
branch
2 times, most recently
from
37681e4 to
7344a1b
Compare
|
I think this PR is a cohesive unit of work now, and hopefully passes CI. I don't know that it does everything we want to do on this front yet, but I think it's better to get it reviewed and merged before it gets even bigger. |
| do p' <- unfoldProp sc vars p | ||
| check hyps e' p' | ||
|
|
||
| RewriteEvidence ss e' -> |
There was a problem hiding this comment.
Note: this rule provides a bit of a soundness loophole. Local assumptions can be added to simpsets, and we currently don't have any way to track their provenance, so they might be used out of their scope. To fix this we will need to add some additional bookeeping to the Simpset type, which might be a bit awkward.
| { thmProp :: Prop | ||
| , thmStats :: SolverStats | ||
| { _thmProp :: Prop | ||
| , _thmStats :: SolverStats |
There was a problem hiding this comment.
Is this field redundant? It seems like you could extract SolverStats from the Evidence field. Is it just used to cache the value so we don't have to recompute it multiple times?
There was a problem hiding this comment.
I agree, it feels a bit redundant, and it probably makes sense to remove it at some point. However, at this stage I wanted to minimize observable changes in behavior, so I retained the SolverStats alongside the new Evidence type.
| , psTimeout :: Maybe Integer | ||
| { _psGoals :: [ProofGoal] | ||
| , _psConcl :: ProofGoal | ||
| , _psStats :: SolverStats |
There was a problem hiding this comment.
Similar question here as with the Theorem type: SolverStats seems like a more limited view of Evidence; is it redundant?
Make `Prop` an opaque newtype and make all operations that manipulate it local to the Proof module.
The `Theorem` and `ProofState` data types are now abstract, and changes in proof state are mostly mediated by the new `Tactic` concept. Theorems now contain `Evidence` which explains the reasoning for why we accept a particular proposition as true. Proof states now explicitly construct evidence as part of tactic execution, and evidence is checked against the proposition to be proved when finishing a proof. Forms of evidence we accept are: 1) Explicit proof terms, according to types-as-propositions 2) Black-box propositions either directly admitted, random checked via quickcheck or proved by solvers 3) Rewriting, unfolding and conversion steps on goals 4) Sequent calculus reasoning rules (theorem application, cut, introduction of local hypotheses, etc). This isolates the core soundness concepts to the "SAWScript.Proof" module, where the key invariants can be maintained relatively easily.
Add documentation, especially for the `Evidence` datatype.
for dispatching queries.
Use the SATQuery type for the "offline" proof exporters, and a variety of other tweaks.
finite values. Fixes #1058
methods. This removes the last uses of the `propToPredicate` method, so delete it.
and clean up the interfaces a bit.
robdockins
force-pushed
the
proof-conventions
branch
from
7344a1b to
af9556d
Compare
|
I think this is ready to go, except perhaps the discussion regarding what to do with |
robdockins
added
the
PR: ready to merge
Start refactoring some of the core SAWScript proof primitives. This strengthens the abstractions surrounding these soundness-critical operations and paves the way to rework some of the underlying data representations in a safe way.