Remove the internal "predicate" convention

[robdockins]

A user-interface convention that SAW inherited from Cryptol is the "function as predicate" style. In this style, theorems to prove or SAT queries to issue are specified as terms of function type that return booleans.

This convention is still used internally inside SAW to communicate problems down to solvers. However, it has been partially replaced with the Prop type that appears in proof states, which uses a "types as propositions" approach instead. The two forms are interrelated via the propToPredicate and predicateToProp operations. Solver communication is generally done with the "function a predicate" style. However, internally to the solvers, the lambda lists are usually "unbound", making the arguments into top-level free variables, which is how solvers generally expect to have problems stated. If you follow through the various code paths, you'll see terms pass through a variety of these conventions before finally arriving where they need to go, and some paths use a combination of the styles, which is quite confusing.

We should be more explicit, via internal data types, about which convention we are using at any given moment, and reduce the number of conversions between conventions we use. In particular, I think we should remove the internal "function as predicate" style and relegate it (only) to a user-interface convention.

SAT-based solvers want to receive a boolean term with free variables (as does the symbolic simulator), proof tactics want to work with propositions, and users want to input functions written in Cryptol syntax. We should have separate data types representing these conventions and rearrange internal functions to accept the most natural one, and we should work to eliminate as many of the translations back-and-forth between these conventions as possible.

[robdockins]

@brianhuffman, I'm particularly interested on your thoughts regarding this idea.

[brianhuffman]

This sounds like a good idea to me. It would probably simplify the code for various backends, because as it stands currently, they have to include code for dealing with both lambda-bound and free (i.e. ExtCns) variables. It would be nice if we could just rip out all the code from the proof backends for dealing with lambda-bound variables.

I suppose we don't even really have to do this simplification all at once; we can just go around to all the saw backends one by one and remove all the extra cruft for handling lambdas-as-quantifiers. As we do that, we just need to make sure that none of the code in saw-script ever tries to pass lambda-quantifiers into any of the backends.

[brianhuffman]

Another thing we might consider doing is moving the definition of the Prop newtype wrapper down into the saw-core package (either that or introduce one or more variants or refinements of it into saw-core). Basically the newtype wrappers would identify Term values that have the saw-core type Prop (and possibly the sort n types as well). This would let us put more precise Haskell types on various functions exported by the saw-core backend packages.

[robdockins]

I'm currently thinking my first step is to introduce a SATQuery type in the saw-core package that is intended to replace the predicate convention for issuing queries.

data SATQuery =
  SATQuery
  { satVariables :: Set (ExtCns FirstOrderType)
  , satUninterp  :: Set VarIndex
  , satAsserts   :: [Term]
  }

Maybe it also makes sense to push Prop down to about the same level. It's less clear to me what a wrapper for sort n types would be used for.

In both cases (sat queries and prop), I'm considering allowing What4 terms to stand directly in for boolean-valued SAWCore terms so that we can avoid doing a W4->SAW->W4 trip in cases where that makes sense. The concern then becomes: do we want the saw-core package to depend on What4?

[brianhuffman]

Why would the saw-core package need to depend on what4? If you want to put what4 terms inside saw-core terms, we could just use ExtCns variables for that, and the saw-core-what4 package can use a side table that maps ExtCns variables to their what4 values. (Basically the converse of what the SAW backend for what4 did.) Do we need anything more than that?

[robdockins]

Perhaps, I haven't thought it all the way through. I'm a bit concerned that just using ExtCns with a side-lookup table might be really error prone, though, as now every use site has to know that they might need to resolve those variables in the lookup table.

[robdockins]

Major progress on this issue in #1102. I believe all the SAT-based proof backends are now using the new SATQuery type. In addition, several of the proof abstractions were significantly strengthened. In a second pass, I intend to remove the old predicate-based methods and generally clean up dangling code.

[robdockins]

This is now finished in #1134