Primitives.tex

\chapter{Cryptol prelude functions}

\commentout{
\begin{code}
primsPlaceHolder=1;
\end{code}
}

\paragraph*{Bitwise and logical operations}
\begin{Verbatim}
    True, False : Bit
    &&, ||, ^   : {a} (Logic a) => a -> a -> a
    ~           : {a} (Logic a) => a -> a
    ==>, /\, \/ : Bit -> Bit -> Bit
\end{Verbatim}
\paragraph*{Comparisons}
\begin{Verbatim}
    ==, !=           : {a} (Eq a) => a -> a -> Bit
    <, >, <=, >=     : {a} (Cmp a) => a -> a -> Bit
    <$, >$, <=$, >=$ : {a} (SignedCmp a) => a -> a -> Bit
    min, max         : {a} (Cmp a) => a -> a -> a
    ===, !==         : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit
\end{Verbatim}
\paragraph*{Arithmetic}
\begin{Verbatim}
    +, -, *           : {a} (Ring a) => a -> a -> a
    negate            : {a} (Ring a) => a -> a
    fromInteger       : {a} (Ring a) => Integer -> a
    ^^                : {a, e} (Ring a, Integral e) => a -> e -> a
    abs               : {a} (Cmp a, Ring a) => a -> a
    /, %              : {a} (Integral a) => a -> a -> a
    toInteger         : {a} (Integral a) => a -> Integer
    lg2               : {n} (fin n) => [n] -> [n]
    /$, %$            : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
    carry             : {n} (fin n) => [n] -> [n] -> Bit
    scarry, sborrow   : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
    zext              : {m, n} (fin m, m >= n) => [n] -> [m]
    sext              : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]
    ratio             : Integer -> Integer -> Rational
    /.                : {a} (Field a) => a -> a -> a
    recip             : {a} (Field a) => a -> a
    floor             : {a} (Round a) => a -> Integer
    ceiling           : {a} (Round a) => a -> Integer
    trunc             : {a} (Round a) => a -> Integer
    roundAway         : {a} (Round a) => a -> Integer
    roundToEven       : {a} (Round a) => a -> Integer
\end{Verbatim}
\paragraph*{GF(2) polynomial arithmetic}
\begin{Verbatim}
    pdiv  : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
    pmod  : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
    pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]
\end{Verbatim}
\paragraph*{Sequences}
\begin{Verbatim}
    take      : {front, back, a} => [front + back]a -> [front]a
    drop      : {front, back, a} (fin front) => [front + back]a -> [back]a
    #         : {front, back, a} (fin front) => [front]a -> [back]a -> [front + back]a
    join      : {parts, each, a} (fin each) => [parts][each]a -> [parts * each]a
    split     : {parts, each, a} (fin each) => [parts * each]a -> [parts][each]a
    groupBy   : {each, parts, a} (fin each) => [parts * each]a -> [parts][each]a
    transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
    reverse   : {n, a} (fin n) => [n]a -> [n]a
    head      : {n, a} [1 + n]a -> a
    tail      : {n, a} [1 + n]a -> [n]a
    last      : {n, a} (fin n) => [1 + n]a -> a
\end{Verbatim}
\paragraph*{Indexing, updates}
\begin{Verbatim}
    @       : {n, a, ix} (Integral ix) => [n]a -> ix -> a
    !       : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a
    @@      : {n, k, ix, a} (Integral ix) => [n]a -> [k]ix -> [k]a
    !!      : {n, k, ix, a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a
    update     : {n, a, ix} (fin ix) => [n]a -> [ix] -> a -> [n]a
    updateEnd  : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a -> [n]a
    updates    : {n, k, ix, a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a
    updatesEnd : {n, k, ix, a} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a
\end{Verbatim}
\paragraph*{Shifting, rotating}
\begin{Verbatim}
    >>>, <<< : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a
    >>, <<   : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
    >>$      : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
\end{Verbatim}
\paragraph*{Functional programming}
\begin{Verbatim}
    iterate  : {a} (a -> a) -> a -> [inf]a
    repeat   : {n, a} a -> [n]a
    map      : {n, a, b} (a -> b) -> [n]a -> [n]b
    zip      : {n, a, b} [n]a -> [n]b -> [n](a, b)
    zipWith  : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c
    foldl    : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
    foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a
    foldr    : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
    foldr' : {n, a, b} (fin n, Eq b) => (a -> b -> b) -> b -> [n]a -> b
    scanl    : {n, b, a} (b -> a -> b) -> b -> [n]a -> [1 + n]b
    scanr    : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b
    sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a
    product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a
    and, or  : {n} (fin n) => [n] -> Bit
    all, any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
    curry    : {a, b, c} ((a, b) -> c) -> a -> b -> c
    uncurry  : {a, b, c} (a -> b -> c) -> (a, b) -> c
    elem     : {n, a} (fin n, Eq a) => a -> [n]a -> Bit
\end{Verbatim}
\paragraph*{Miscellaneous}
\begin{Verbatim}
    deepseq : {a, b} Eq a => a -> b -> b
    rnf : {a} Eq a => a -> a
    length : {n, a, b} (fin n, Literal n b) => [n]a -> b
    zero    : {a} (Zero a) => a
\end{Verbatim}
\paragraph*{Representing exceptions}
\begin{Verbatim}
    undefined : {a} a
    error     : {a, n} (fin n) => String n -> a
    assert    : {a, n} (fin n) => Bit -> String n -> a -> a
    trace     : {n, a, b} [n][8] -> a -> b -> b
    traceVal  : {n, a} [n][8] -> a -> a
\end{Verbatim}
\todo[inline]{\texttt{error} and \texttt{undefined} are not covered in
  the book at the moment.}

\todo[inline]{What is the state of debugging (\texttt{trace},
  \texttt{ASSERT}), randomness (\texttt{random}), and pretty-printing
  (\texttt{format}) built-ins?}
%\paragraph*{Debugging}
%\begin{Verbatim}
%    trace  : {a b c} ([a][8],b,c) -> c
%    ASSERT : {a b} (Bit,[a][8],b) -> b
%\end{Verbatim}
%\paragraph*{Generating random numbers}
%\begin{Verbatim}
%    random : {a b} (32 >= a) => [a] -> b
%\end{Verbatim}
%\paragraph*{Pretty printing}
%\begin{Verbatim}
%    format
%\end{Verbatim}

%    (%$) : {a} (Arith a) => a -> a -> a
%    (/$) : {a} (Arith a) => a -> a -> a
%    number : {val, rep} (Literal val rep) => rep
%    elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
%    fromThenTo :
%      {first, next, last, a, len} (fin first, fin next, fin last,
%                                   Literal first a, Literal next a, Literal last a, first != next,
%                                   lengthFromThenTo first next last == len) =>
%        [len]a
%    fromTo :
%      {first, last, a} (fin last, last >= first, Literal last a) =>
%        [1 + (last - first)]a
%    fromZ : {n} (fin n, n >= 1) => Z n -> Integer
%    infFrom : {a} (Arith a) => a -> [inf]a
%    infFromThen : {a} (Arith a) => a -> a -> [inf]a
%    splitAt :
%      {front, back, a} (fin front) =>
%        [front + back]a -> ([front]a, [back]a)
%    toInteger : {bits} (fin bits) => [bits] -> Integer
%    trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
%    traceVal : {n, a} (fin n) => [n][8] -> a -> a
%    undefined : {a} a
%    zext : {m, n} (fin m, m >= n) => [n] -> [m]
%    sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]
%    carry : {n} (fin n) => [n] -> [n] -> Bit
%    scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
%    sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "../main/Cryptol"
%%% End: