:dumptests doesn't work for return types other than Bit

[brianhuffman]

Cryptol> :dumptests "test" \(x : [32]) -> x + 1

The expression is not of a testable type.
Type: [32] -> [32]

:dumptests only seems to support functions that return type Bit. I'm feeling like supporting expressions in general (not just theorems) would be helpful. Here I just want to generate some input/output pairs for a function so that when I modify/optimize/etc it I can test to see if I've messed it up.

Originally posted by @weaversa in #611 (comment)

[brianhuffman]

Based on this comment in Cryptol/Testing/Random.hs, it's clear that this feature is supposed to work for non-Bit return types. Also these types used to work with :dumptests in version 2.7.

cryptol/src/Cryptol/Testing/Random.hs

Lines 106 to 118 in ee0f60c

	{- | Given a (function) type, compute generators for the function's
	arguments. This is like 'testableTypeGenerators', but allows the result to be
	any finite type instead of just @Bit@. -}
	dumpableType :: forall g. RandomGen g => Type -> Maybe [Gen g Concrete]
	dumpableType ty =
	case tIsFun ty of
	Just (t1, t2) ->
	do g <- randomValue Concrete t1
	as <- testableTypeGenerators t2
	return (g : as)
	Nothing ->
	do (_ :: Gen g Concrete) <- randomValue Concrete ty
	return []

[brianhuffman]

Bisecting shows that 64423cb (one of mine; a fix for #615) is the first bad commit.

[brianhuffman]

It looks like there's a copy-and-paste error in the definition of dumpableType, which was based on the previously-existing function testableTypeGenerators. The call to testableTypeGenerators on line 114 should actually be a recursive call to dumpableType instead.

[weaversa]

I’ve been thinking about dumptest recently and ran across some work on automated sampling. I’m just going to paste the references here, but the gist would be to enhance dumptests so that it generated tests based on the structure of the function, rather than purely random tests. It seems like the current research uses SMT techniques to generate good tests, which facilitates integration into Cryptol.

https://people.eecs.berkeley.edu/~rtd/papers/GuidedSampler.pdf

https://arxiv.org/pdf/1905.05358.pdf