:safe is not safe

[ghost]

Using SBV-backed :safe (and :prove) on an unsafe term containing recip will crash:

$ cryptol
version 2.10.0
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :safe \(x : Z 7) -> x * (recip x) == 1
Counterexample
cryptol: src/Cryptol/Symbolic/SBV.hs:401:9-37: Non-exhaustive patterns in (vs, [])

$

What4 catches the division by 0, though:

$ cryptol
version 2.10.0
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :set prover = w4-z3
Cryptol> :safe \(x : Z 7) -> x * (recip x) == 1
Counterexample
(\(x : Z 7) -> x * (recip x) == 1) 0 ~> ERROR
(Total Elapsed Time: 0.053s, using "z3")
Cryptol> 

[brianhuffman]

Here's the place in source code where the failed pattern match is happening:

cryptol/src/Cryptol/Symbolic/SBV.hs

Lines 420 to 427 in 70442e4

	mkTevs prims result = do
	-- It's a bit fragile, but the value of the safety predicate seems
	-- to always be the first value in the model assignment list.
	let Right (_, (safetyCV : cvs)) = SBV.getModelAssignment result
	safety = SBV.cvToBool safetyCV
	(vs, []) = parseValues ts cvs
	mdl = computeModel prims ts vs
	return (safety, mdl)

Basically what's going on here is that in the SBV query, the quantified variables in the Cryptol predicate may have been split up into a larger number of SBV variables with simpler types. SBV returns a counterexample in the form of a list of values with simple types, and then parseValues assembles them back together (if necessary) to make values of the possibly-complex Cryptol types.

Usually this parsing process completes with nothing leftover. But it looks like if you use recip, the SBV counterexample includes some extra junk. I expect this has to do with the fact that in the SBV backend, recip is implemented by generating a new fresh variable for its result value and then asserting something about it.

cryptol/src/Cryptol/Backend/SBV.hs

Lines 393 to 401 in 70442e4

	-- Create a fresh constant and assert that it is the
	-- multiplicitive inverse of x; return the constant.
	-- Such an inverse must exist under the precondition
	-- that the modulus is prime and the input is nonzero.
	sModRecip ::
	SBV ->
	Integer {- ^ modulus: must be prime -} ->
	SInteger SBV ->
	SEval SBV (SInteger SBV)

The extra junk in the counterexample is probably the values for these variables that were introduced for the result of recip. I modified Cryptol to print out the full list of leftover values if the list is non-null; in your example the extra value is the integer 1. I also found that for each additional occurrence of recip you add to the proposition, you get one additional value in that list.

[robdockins]

Looks like the same issue as #986

I thought that was related to records, but it seems clear that it is actually related to finite field inverses. I'll see what we can do to fix the counterexample parsing code.

[robdockins]

Fixed via #1067