Change example in Generate test vector section to not reference crypt…

…ol specs.

Keep example as a polymporphic function using multiple inputs and a non Bit output to show that it can handle that case now.

Also fix up some minor typos and clarify a few sentences.

docs/ProgrammingCryptol/highAssurance/HighAssurance.tex

@@ -178,44 +178,31 @@ \subsection{Capturing test vectors}
 \subsection{Generating test vectors}
 \label{sec:gentestvec}
 
-Cryptol has the ability to generate test vectors for simple function types using the \texttt{:dumptests} REPL command.
+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.
-The output will contain a tab delimited file in which the first column contains the output, and each column after contains the inputs to the function.
-The command \texttt{:dumptests} uses the same settings as \texttt{:check} \ref{sec:quickcheck}, this means you can set the number of tests you want using the \texttt{:set tests=100} command.
-
-The following is an example using \href{https://github.com/GaloisInc/cryptol-specs/blob/7468d170f5e9e3913cd12e29c76d8c041ef99dd0/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry}{SHA2-256 implemntation} in \href{https://github.com/GaloisInc/cryptol-specs}{cryptol-specs}.
-The output file was modified slightly by putting the input on the next line tabbed in. 
 \begin{Verbatim}
-Cryptol> :load Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry
-Loading module Cryptol
-Loading module `where` argument of Primitive::Keyless::Hash::SHA2::Instantiations::SHA256
-Loading interface module `parameter` interface of 
-  Primitive::Keyless::Hash::SHA2::Specification
-Loading module Primitive::Keyless::Hash::SHA2::Specification
-Loading module Primitive::Keyless::Hash::SHA2::Instantiations::SHA256
-Primitive::Keyless::Hash::SHA2::Instantiations::SHA256> :dumptests output.txt hash`{256}
-Primitive::Keyless::Hash::SHA2::Instantiations::SHA256> :quit
-% head output.txt                                                        
-0x6055ba8ba7ae5a07b972f621b0a1953e8769a8fba9e767b70016fe00b8173c61
-  0x49e27d1e5be42afd7e48e78fc3133789376f3f5b14b712bf9f1b89e0a55ed4e7
-0xf457465cfe89b634d3ccbe7b0e8671ecc8a02108b14f3d9847d9b2f1867b56e2
-  0xb89fa0030b4bcb8fb05ade0ce21811995cf2d284a703e2263511b9c83f732acf
-0x0ea5dbd2b3c2563008e3059ad1a85baa518a62d665f082f494ce2b4e6a6a6d9c
-  0xc5bda3e97b96d3f2f72deec8e84e192a9130fbff9e77f82f866f2dd85b064ef3
-0x9135e2fc9a6a8198bda8b5c22b791ce53e4221e047869f0c8dc80d65d03ff68e
-  0x1d8a51245e39533af8c627b22c5a80fafc37710e40fda01a381abf04d913a945
-0x21fbd5917a0824945a8f063f09fb648fbf1a6b6b766fbe4bf431adbb3e255354
-  0xd7cc5b5c8f847b22db392631c0c0fa7a442e326c7708d96664c6097eba265671
-0x3145d5381d91ba57b2a003bb28fff4ba17dc967fd428d4bfa19bcfa84dfe8f55
-  0x83b38cfd665c4c73b0b0e284ceff3e9c7b45052ae414570658844bc9eec83847
-0xad7755c148344f7cd40f823d7cdae6572888051da324ce43aa11c910344b8cee
-  0xc3b7611ad29286aaedda565c0a5c4aff2b28afb62bebc310bcb7e87260351a51
-0x0ba711d34a2e560a6649c30ae7f48f86dc6134d94ac03c2f34f2e9816ace7bed
-  0x84fc8a7fca63821541b7f0bd3d637763eb914bcd37c9b3583d6411b1fdbfdb4f
-0x2ac9cc5903aa65bfae08a20baf5209b94de588ea136bf96ec1708bf9f30d28b2
-  0x7fda970c107a9e0e21e38cada68402734b9aad3ac5b2602518e36830d4673600
-0x891f22fa71c6652e859996fbaac4b1561a19e9021afe301f4462bd52400981dd
-  0xb99e3e2b8f00885080194c98480f04ca03afb8f8a08ae3c21c425cacb37337bc
+  :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.
+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}.
+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]
+  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}