Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add documentation for :dumptests via a new section in the High Assurance chapter of Programming in Cryptol Book #1760

Merged
merged 3 commits into from
Oct 2, 2024
Merged

Add documentation for :dumptests via a new section in the High Assurance chapter of Programming in Cryptol Book #1760

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7f8780e
Close #611: Add new section to the High Assurance chapter of the Prog…
mccleeary-galois Oct 1, 2024
ce8e3f1
Change example in Generate test vector section to not reference crypt…
mccleeary-galois Oct 1, 2024
75a61ec
Update Generate Test Vector Example
mccleeary-galois Oct 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file modified docs/ProgrammingCryptol.pdf
View file
Open in desktop
Binary file not shown.
32 changes: 32 additions & 0 deletions docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -174,6 +174,38 @@ \subsection{Capturing test vectors}
sure the tweak to the above example (removal of dummy single formal
parameter) works.}

%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\subsection{Generating test vectors}
\label{sec:gentestvec}

Cryptol has the ability to generate test vectors for non-polymorphic functions (there is limited support for polymorphic types) using the \texttt{:dumptests} REPL command.
When \texttt{:dumptests} is given a file to dump the output and a function in scope, it will randomly generate inputs for the function and run them for you.
mccleeary-galois marked this conversation as resolved.
Show resolved Hide resolved
\begin{Verbatim}
:dumptests <results file> <function>
:dumptests results.txt myFunction
\end{Verbatim}
The results file will contain a tab delimited file in which the first column contains the output, and each column after contains the inputs to the function in order.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

suggested rephrase: "tab delimited file" -> "tab delimited table"? I don't love the phrasing of "the file contains a file" but I'm struggling to find a better word.

You can set the number of tests you want to generate in your test vector by using the \texttt{:set tests=100} command. Additionally, you can also change base using \texttt{:set base=2}.
mccleeary-galois marked this conversation as resolved.
Show resolved Hide resolved
This is because the command \texttt{:dumptests} uses the same settings for random generation that is used in \ref{sec:quickcheck}.
The example below shows \texttt{:dumptests} run on an instance of a function polymorphic \texttt{f} which has two inputs.
\begin{code}
f : {n} (fin n, n >= 2) => [n] -> [n] -> [n]
mccleeary-galois marked this conversation as resolved.
Show resolved Hide resolved
f x y = x + 2 * y
\end{code}
\begin{Verbatim}
Cryptol> :set tests = 5
Cryptol> :set base = 2
Cryptol> :dumptests result.txt f`{8}
Cryptol> :quit
% cat result.txt
0b11011110 0b10010010 0b00100110
0b10101111 0b01010011 0b00101110
0b10100001 0b01001001 0b10101100
0b10111110 0b11101100 0b01101001
0b00110000 0b11111100 0b10011010
\end{Verbatim}


%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\subsection{Polymorphic properties}
\label{sec:polythm}
Expand Down
Loading