quickcheck fails on goals that quantify over tuple or record types

[brianhuffman]

Quantified variables with tuple or record types produce a "term has non-testable type" error message. Tuple and record types should definitely be considered testable.

sawscript> prove (quickcheck 100) {{ \(x:([8],[8])) -> x.0 == x.1 }}
[03:19:09.799] WARNING: using quickcheck to prove goal...

user error ("prove" (<stdin>:1:1-1:6):
"quickcheck" (<stdin>:1:8-1:18):
quickcheck:
term has non-testable type:
let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in (x : (x@1 * x@1))
-> Prelude.Bool, for term: let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in \(x : (x@1 * x@1)) ->
      Cryptol.ecEq x@1 (Cryptol.PCmpSeqBool (Cryptol.TCNum 8)) x.1 x.2)
sawscript> prove (quickcheck 100) {{ \(x:{a:Bit, b:Bit}) -> x.a \/ x.b }}
[03:20:54.542] WARNING: using quickcheck to prove goal...

user error ("prove" (<stdin>:1:1-1:6):
"quickcheck" (<stdin>:1:8-1:18):
quickcheck:
term has non-testable type:
(x : (Prelude.Bool * Prelude.Bool))
-> Prelude.Bool, for term: \(x : (Prelude.Bool * Prelude.Bool)) -> \/ x.1 x.2)

The same error occurs if the variable was created with fresh_symbolic.

sawscript> x <- fresh_symbolic "x" {| (Bit, Bit) |}
sawscript> prove (quickcheck 100) {{ x.0 \/ x.1 }}
[03:22:34.481] WARNING: using quickcheck to prove goal...

user error ("prove" (<stdin>:1:1-1:6):
"quickcheck" (<stdin>:1:8-1:18):
quickcheck:
term has non-testable type:
(x : (Prelude.Bool * Prelude.Bool))
-> Prelude.Bool, for term: \(x : (Prelude.Bool * Prelude.Bool)) -> \/ x.1 x.2)

[brianhuffman]

It looks like the problem originates in the function asFiniteTypePure from module Verifier.SAW.FiniteValue in the saw-core package, which is defined in terms of Verifier.SAW.Recognizer.asTupleType. Apparently, the asTupleType recognizer still expects tuples to be encoded as nested pair types with the unit type at the end; we have not used this encoding of tuples since December 2018 (GaloisInc/saw-core@5c0f54e).

[brianhuffman]

PR GaloisInc/saw-core#51 fixes the problem, but we should probably leave the ticket open until we add a saw-script regression test and update the saw-core submodule.