add :smartcheck command

[kiniry]

Introduce a new :smartcheck command that intelligently uses the context of value generation to produce smaller and more useful counter-examples more frequently. Discussed at some length with @TomMD.

Testing.Random.randomWord is being patched to produce proper uniform distributions as :check was never documented to generated biased values.

@brianhuffman @yav @acfoltzer @dmwit @dmzimmerman probably have opinions about this. ;)

[LeventErkok]

Here's something related.. I wanted to do this on Cryptol-1, but never got around to, but it should be easier now with the likes of sBranch and on-the-fly SMT interface available.

• Use the symbolic simulation engine to start the simulation; either with completely symbolic inputs, or carefully chosen dynamic/static set. (Possibly user guided.)
• Keep track of a depth, incrementing it by 1 each time you go through a choice point (i.e., if-then-else)
• Use the SMT solver at each decision point to give you an assignment that takes you to that path
• Stop at a given depth, possibly user configured, but deeper you go, the simulation will blow; so can also be dynamic based on the generated expression length. (Variable number as generated by SBV can be a crude measure.)
• Using the thus collected choice-points, use the SMT solver to generate test-vectors that'll take you to every single path down that tree. The deeper the tree, the better test vectors you get. Of course, the deeper the tree, the more likely it'll blow.

This is essentially the concolic testing idea (http://en.wikipedia.org/wiki/Concolic_testing)

Note that such systems hardly ever worth building for crypto-algorithms: Good crypto is always designed to be oblivious to data values for their branching, if there's any branching at all. So, it's not clear if this is really a good idea if all you want is crypto.

But if you're targeting Cryptol for other embedded work, then it could indeed be a nice addition to the tool-suite. (For instance, if you ran this algorithm on AES, you'll get zero good test vectors since AES has no choice points based on data+key. But if you run it on a fixed-point number implementation like CORDIC, it'll give you really nice test cases. Ask Adam Wick for the latter!)

[atomb]

PR #1028 provides an interesting start on a solution to this problem.