SAW will not quickcheck for type Integer

[msaaltink]

Cryptol happily tests functions on Integers:

Cryptol> :check \ (x:Integer)-> x+1 == x
Using random testing.
(\(x : Integer) -> x + 1 == x) 240 = False

SAW, in contrast, does not:

sawscript> prove (quickcheck 10) {{ \ (x:Integer)-> x+1 == x }}
[19:56:22.922] WARNING: using quickcheck to prove goal...

Stack trace:
"prove" (<stdin>:1:1-1:6):
"quickcheck" (<stdin>:1:8-1:18):
quickcheck:
term has non-testable type:
[...]

This might be related to #669.

The Z types are similar; Cryptol can test them but SAW will not.

[brianhuffman]

This is a consequence of saw-script/saw-core and cryptol having completely separate implementations of quickcheck generators. The ones in the saw-core package is just way out of date, and was never updated to include type Integer or Z n.

I could go and add types Integer and Z n to the saw-core test generators. But probably a better long-term approach is to just reimplement saw-script's quickcheck tactic using Cryptol's quickcheck, and remove the out-of-date saw-core one completely. This would ensure that quickcheck remains consistent in both settings, even as new types (e.g. floating-point numbers and rationals) are added.

[brianhuffman]

The saw-core module Verifier/SAW/Testing/Random.hs even says right at the top that it is "based on 'Cryptol.Testing.Random'". Clearly this is unnecessary code duplication that we should get rid of.

[brianhuffman]

The current plan is to go ahead and implement the quick fix to add support for type Integer to the saw-core quickcheck. This will require it to switch from FiniteType to FirstOrderType for recognizing types that can be quantified over. We should still plan to unify the quickcheck code with cryptol in the long term.