GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-10-04 01:17:40 +03:00
Code Issues Projects Releases Wiki Activity

Fix some typos I noticed in the Programming Cryptol book. (#1631)

Browse Source 
- p-1 bits in an IEEE float refers to the significand, not the
  mantissa, at least according to the latest preferred terminology,
  which aims to keep the word "mantissa" for the full mantissa
  including the units bit;
- reciprocal rather than reciprocol;
- the example in 1.23 had the wrong module declarations; also insert a
  separator word between the verbatim blocks so they can be told
  apart.
This commit is contained in:
David Holland 2024-02-23 08:16:07 -05:00 committed by GitHub
parent 707257e79f
commit facc682fe8
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 6 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
View File

@ -365,7 +365,7 @@ and integers.
The family of types \texttt{Float e p}\indTheFloatType represent IEEE 754 The family of types \texttt{Float e p}\indTheFloatType represent IEEE 754
floating point numbers with \texttt{e} bits in the exponent and floating point numbers with \texttt{e} bits in the exponent and
\texttt{p-1} bits in the mantissa. The family is defined in a built-in \texttt{p-1} bits in the significand. The family is defined in a built-in
module called \texttt{Float} so to use it you'd need to either import module called \texttt{Float} so to use it you'd need to either import
it in your Cryptol specification or use \texttt{:m Float} on the it in your Cryptol specification or use \texttt{:m Float} on the
Cryptol REPL. Cryptol REPL.
@ -3206,7 +3206,7 @@ Bitvectors and integers members of \texttt{Integral}.
The \texttt{Field} typeclass represents values that, in addition to The \texttt{Field} typeclass represents values that, in addition to
being a \texttt{Ring}, have multiplictive inverses. being a \texttt{Ring}, have multiplictive inverses.
It includes the field division operation \texttt{/.} and the It includes the field division operation \texttt{/.} and the
\texttt{recip} operation for computing the reciprocol of a value. \texttt{recip} operation for computing the reciprocal of a value.
Currently, only type \texttt{Rational} is a member of this class. Currently, only type \texttt{Rational} is a member of this class.
\item \item
@ -3598,6 +3598,7 @@ accessing it from \verb+HMAC.cry+ you would need to name the modules
accordingly: accordingly:
\begin{verbatim} \begin{verbatim}
module Hash::SHA3 where
sha3 : {n} (fin n) => [n] -> [512] sha3 : {n} (fin n) => [n] -> [512]
sha3 = error "Stubbed, for demonstration only: sha3-512" sha3 = error "Stubbed, for demonstration only: sha3-512"
@ -3606,8 +3607,10 @@ blocksize : {n} (fin n, n >= 10) => [n]
blocksize = 576 blocksize = 576
\end{verbatim} \end{verbatim}
and
\begin{verbatim} \begin{verbatim}
module Hash::SHA3 where module HMAC where
import Hash::SHA3 import Hash::SHA3
hmac : {keySize, msgSize} (fin keySize, fin msgSize) => [keySize] -> [msgSize] -> [512] hmac : {keySize, msgSize} (fin keySize, fin msgSize) => [keySize] -> [msgSize] -> [512]