Reintroduce ":safe"/"assert"

[LeventErkok]

@acfoltzer @brianhuffman

In the good old days of Cryptol 1, there was the :safe command, which checked whether there's div-by-0, index-out-of-bounds, log-of-0, etc,; and violations of any user given asserts. This functionality seems to have evaporated in Cryptol 2: I can neither find the :safe command, nor the assert expression.

The latest github version of SBV comes with sAssert and safe functions, which can be directly used to introduce similar functionality in Cryptol. See here: http://github.com/LeventErkok/sbv/blob/master/Data/SBV/Provers/Prover.hs#L350
and here: http://github.com/LeventErkok/sbv/blob/master/Data/SBV/BitVectors/Model.hs#L1106

An example use case is here: http://github.com/LeventErkok/sbv/blob/master/Data/SBV/Examples/Misc/NoDiv0.hs

I'm intending to do a new SBV release on Hackage soon, containing this functionality. I understand that you guys probably don't have the bandwidth right now to look at this and give me an OK on the API; but we can always make a new SBV release to fit Cryptol's needs when/if you implement the :safe command and its assert counterpart. As usual, send a pull request with the mods you need!

[LeventErkok]

SBV 5.4 is now out on hackage, with sAssert and safe

[acfoltzer]

Thanks! We might not be able to take advantage of the new features for a while, but I've got a PR incoming to keep 7.8 on life support

[robdockins]

With the new evaluator in the IO monad, it probably makes sense to revisit this soon.

[robdockins]

As part of the refactoring I'm doing in #684, I'm making the internal changes necessary to compute safety conditions during symbolic evaluation. The result of a symbolic evaluation will either be an error (if all inputs obviously cause an error) or a pair of a safety predicate and a value.

At this point, the slightly tricky bit is to figure out what to do with them, from a UI perspective. How should safety predicates interact with :sat and :prove? Should the behavior be configurable? Do we want a separate :safe command, as suggested originally? etc.

[robdockins]

After thinking about this for a bit, here's my proposal. Let's add a new :set option (name suggestions?) that controls if we pay attention to safety conditions. If set, we add the safety conditions as assumptions for :sat queries and add them to the goal for :prove queries. If unset, they are ignored (the current behavior). I think the default should be for this option to be on.

We can also add a separate :safe query which just attempts to prove the safety condition associated with a term.

We can also add to the Prelude:

assert : {a, n} Bit -> [n][8] -> a -> a
assert pred msg x = if pred then x else error msg

Alternately, make assert a primitive with essentially the same semantics.

[brianhuffman]

When printing a counterexample from :check or :prove, we should not display it as foo <args> = False if the counterexample is instead a violation of the safety predicate. Rather, we should display something like foo <args> = <run-time error>.

[robdockins]

As of 60dcbd1 both SBV and What4 backends automatically include safety predicates as part of :prove and :sat statements.

We still need to implement the user-configurable settings that control this behavior, and improve the output generated when displaying counterexamples.

[robdockins]

Fixed via #770