search

GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 126 forks source link

dumptests undocumented #611

Closed kiniry closed 1 month ago

kiniry commented 5 years ago

The dumptests REPL command was added by @david-christiansen, but it is undocumented in Programming Cryptol. There are also no examples of its use shipped with Cryptol.

weaversa commented 4 years ago 
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.

brianhuffman commented 4 years ago

We do have in-REPL documentation for :dumptests. So if we implement #612 to give us an auto-generated markdown file containing all the REPL command help text, we can just include that as an appendix to the book and that should take care of this issue as well.

kiniry commented 1 month ago

Ensuring that dumpTests is in the Cryptol book and reference manual ASAP is now of high priority. CC @andrew-bivin @mccleeary-galois

mccleeary-galois commented 1 month ago 
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.

Just an FYI this appears to be the functionality now in which it can work on any function and generate test vectors for you. See example in #1760