cryptol/docs/CryptolPrims.md

Typeclass Heriarchy

      Zero
      /  \
  Logic  Ring          Eq
         /  \         /  \
  Integral  Field   Cmp  SignedCmp
                \   /
                Round

This diagram describes how the various typeclasses in Cryptol are related. A type which is an instance of a subclass is also always a member of all of its superclasses. For example, any type which is a member of Field is also a member of Ring and Zero.

Literals

type Literal : # -> * -> Prop
type LiteralLessThan : # -> * -> Prop

number : {val, rep} Literal val rep => rep
length : {n, a, b} (fin n, Literal n b) => [n]a -> b

// '[x..y]' is syntactic sugar for 'fromTo`{first=x,last=y}'
fromTo : {first, last, a}
           (fin last, last >= first,
           Literal first a, Literal last a) =>
           [1 + (last - first)]a

// '[x .. < y]' is syntactic sugar for
//   'fromToLessThan`{first=x,bound=y}'
fromToLessThan : {first, bound, a}
     (fin first, bound >= first, LiteralLessThan bound a) =>
     [bound - first]a

// '[x,y..z]' is syntactic sugar for
//   'fromThenTo`{first=x,next=y,last=z}'
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

// '[x .. y by n]' is syntactic sugar for
//    'fromToBy`{first=x,last=y,stride=n}'.
primitive fromToBy : {first, last, stride, a}
  (fin last, fin stride, stride >= 1, last >= first, Literal last a) =>
  [1 + (last - first)/stride]a

// '[x ..< y by n]' is syntactic sugar for
//   'fromToByLessThan`{first=x,bound=y,stride=n}'.
primitive fromToByLessThan : {first, bound, stride, a}
  (fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) =>
  [(bound - first)/^stride]a

// '[x .. y down by n]' is syntactic sugar for
//   'fromToDownBy`{first=x,last=y,stride=n}'.
primitive fromToDownBy : {first, last, stride, a}
  (fin first, fin stride, stride >= 1, first >= last, Literal first a) =>
  [1 + (first - last)/stride]a

// '[x ..> y down by n]' is syntactic sugar for
//   'fromToDownByGreaterThan`{first=x,bound=y,stride=n}'.
primitive fromToDownByGreaterThan : {first, bound, stride, a}
  (fin first, fin stride, stride >= 1, first >= bound, Literal first a) =>
  [(first - bound)/^stride]a

Fractional Literals

The predicate FLiteral m n r a asserts that the type a contains the fraction m/n. The flag r indicates if we should round (r >= 1) or report an error if the number can't be represented exactly.

type FLiteral : # -> # -> # -> * -> Prop

Fractional literals are desugared into calls to the primitive fraction:

fraction : { m, n, r, a } FLiteral m n r a => a

Zero

type Zero  : * -> Prop

zero       : {a} (Zero a) => a

Every base and structured type in Cryptol is a member of class Zero.

Boolean

type Logic : * -> Prop

False      : Bit
True       : Bit

(&&)       : {a} (Logic a) => a -> a -> a
(||)       : {a} (Logic a) => a -> a -> a
(^)        : {a} (Logic a) => a -> a -> a
complement : {a} (Logic a) => a -> a
  // The prefix notation '~ x' is syntactic
  // sugar for 'complement x'.

(==>)      : Bit -> Bit -> Bit
(/\)       : Bit -> Bit -> Bit
(\/)       : Bit -> Bit -> Bit

instance                       Logic Bit
instance (Logic a)          => Logic ([n]a)
instance (Logic b)          => Logic (a -> b)
instance (Logic a, Logic b) => Logic (a, b)
instance (Logic a, Logic b) => Logic { x : a, y : b }
// No instance for `Logic Integer`.
// No instance for `Logic (Z n)`.
// No instance for `Logic Rational`.

Arithmetic

type Ring   : * -> Prop

fromInteger : {a} (Ring a) => Integer -> a
(+) : {a} (Ring a) => a -> a -> a
(-) : {a} (Ring a) => a -> a -> a
(*) : {a} (Ring a) => a -> a -> a
negate : {a} (Ring a) => a -> a
  // The prefix notation `- x` is syntactic
  // sugar for `negate x`.


type Integral : * -> Prop

(/) : {a} (Integral a) => a -> a -> a
(%) : {a} (Integral a) => a -> a -> a
toInteger : {a} (Integral a) => a -> Integer
infFrom : {a} (Integral a) => a -> [inf]a
  // '[x...]' is syntactic sugar for 'infFrom x'
infFromThen : {a} (Integral a) => a -> a -> [inf]a
  // [x,y...]' is syntactic sugar for 'infFromThen x y'


type Field : * -> Prop

(/.)  : {a} (Field a) => a -> a -> a
recip : {a} (Field a) => a -> a


type Round : * -> Prop

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

(^^) : {a, e} (Ring a, Integral e) => a -> e -> a

// No instance for `Bit`.
instance (fin n)          => Ring ([n]Bit)
instance (Ring a)         => Ring ([n]a)
instance (Ring b)         => Ring (a -> b)
instance (Ring a, Ring b) => Ring (a, b)
instance (Ring a, Ring b) => Ring { x : a, y : b }
instance                     Ring Integer
instance (fin n, n>=1)    => Ring (Z n)
instance                     Ring Rational
instance (ValidFloat e p) => Ring (Float e p)

Note that because there is no instance for Ring Bit the top two instances do not actually overlap.

instance                  Integral Integer
instance (fin n)       => Integral ([n]Bit)

instance Field Rational
instance (prime p) => Field (Z p)
instance (ValidFloat e p) => Field (Float e p)

instance Round Rational
instance (ValidFloat e p) => Round (Float e p)

Equality Comparisons

type Eq : * -> Prop

(==)  :  {a}   (Eq a) => a -> a -> Bit
(!=)  :  {a}   (Eq a) => a -> a -> Bit
(===) :  {a,b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit
(!==) :  {a,b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit

instance                  Eq Bit
instance (Eq a, fin n) => Eq [n]a
instance (Eq a, Eq b)  => Eq (a, b)
instance (Eq a, Eq b)  => Eq { x : a, y : b }
instance                  Eq Integer
instance                  Eq Rational
instance (fin n, n>=1) => Eq (Z n)
// No instance for functions.

Comparisons and Ordering

type Cmp : * -> Prop

(<)  : {a} (Cmp a) => a -> a -> Bit
(>)  : {a} (Cmp a) => a -> a -> Bit
(<=) : {a} (Cmp a) => a -> a -> Bit
(>=) : {a} (Cmp a) => a -> a -> Bit

min  : {a} (Cmp a) => a -> a -> a
max  : {a} (Cmp a) => a -> a -> a

abs  : {a} (Cmp a, Ring a) => a -> a

instance                   Cmp Bit
instance (Cmp a, fin n) => Cmp [n]a
instance (Cmp a, Cmp b) => Cmp (a, b)
instance (Cmp a, Cmp b) => Cmp { x : a, y : b }
instance                   Cmp Integer
instance                   Cmp Rational
// No instance for functions.

Signed Comparisons

type SignedCmp : * -> Prop

(<$)  : {a} (SignedCmp a) => a -> a -> Bit
(>$)  : {a} (SignedCmp a) => a -> a -> Bit
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
(>=$) : {a} (SignedCmp a) => a -> a -> Bit

// No instance for Bit
instance (fin n, n >= 1)            => SignedCmp [n]
instance (SignedCmp a, fin n)       => SignedCmp [n]a
        // (for [n]a, where a is other than Bit)
instance (SignedCmp a, SignedCmp b) => SignedCmp (a, b)
instance (SignedCmp a, SignedCmp b) => SignedCmp { x : a, y : b }
// No instance for functions.

Bitvectors

(/$)    : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
(%$)    : {n} (fin n, n >= 1) => [n] -> [n] -> [n]

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

zext    : {m, n} (fin m, m >= n) => [n] -> [m]
sext    : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]

lg2     : {n} (fin n) => [n] -> [n]

// Arithmetic shift only for bitvectors
(>>$)   : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]

Rationals

ratio : Integer -> Integer -> Rational

Z(n)

fromZ : {n} (fin n, n >= 1) => Z n -> Integer

Sequences

join       : {parts,each,a} (fin each) => [parts][each]a -> [parts * each]a
split      : {parts,each,a} (fin each) => [parts * each]a -> [parts][each]a

(#)        : {front,back,a} (fin front) => [front]a -> [back]a -> [front + back]a
splitAt    : {front,back,a} (fin front) => [from + back] a -> ([front] a, [back] a)

reverse    : {n,a} (fin n) => [n]a -> [n]a
transpose  : {n,m,a} [n][m]a -> [m][n]a

(@)        : {n,a,ix}   (Integral ix) =>  [n]a -> ix    -> a
(@@)       : {n,k,ix,a} (Integral ix) =>  [n]a -> [k]ix -> [k]a
(!)        : {n,a,ix}   (fin n, Integral ix) => [n]a -> ix    -> a
(!!)       : {n,k,ix,a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a
update     : {n,a,ix}   (Integral 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,d} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a

take       : {front,back,elem} [front + back]elem -> [front]elem
drop       : {front,back,elem} (fin front) => [front + back]elem -> [back]elem
head       : {a, b} [1 + a]b -> b
tail       : {a, b} [1 + a]b -> [a]b
last       : {a, b} [1 + a]b -> b

// Declarations of the form 'x @ i = e' are syntactic
// sugar for 'x = generate (\i -> e)'.
generate : {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a

groupBy    : {each,parts,elem} (fin each) => [parts * each]elem -> [parts][each]elem

Function groupBy is the same as split but with its type arguments in a different order.

Shift And Rotate

(<<)  : {n,ix,a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
(>>)  : {n,ix,a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
(<<<) : {n,ix,a} (fin n, Integral ix)  => [n]a -> ix -> [n]a
(>>>) : {n,ix,a} (fin n, Integral ix)  => [n]a -> ix -> [n]a

GF(2) polynomials

pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]
pdiv  : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
pmod  : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]

Random Values

random : {a} => [256] -> a

Errors and Assertions

undefined : {a} a
error     : {a,n} (fin n) => String n -> a
assert    : {a,n} (fin n) => Bit -> String n -> a -> a

Debugging

trace     : {n, a, b} (fin n) => String n -> a -> b -> b
traceVal  : {n, a} (fin n) => String n -> a -> a

Utility operations

and   : {n} (fin n) => [n]Bit -> Bit
or    : {n} (fin n) => [n]Bit -> Bit
all   : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
any   : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
elem  : {n, a} (fin n, Eq a) => a -> [n]a -> Bit

deepseq : {a, b} Eq a => a -> b -> b
rnf : {a} Eq a => a -> a

map     : {n, a, b} (a -> b) -> [n]a -> [n]b
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
foldl'  : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a
scanl   : {n, b, a}  (b -> a -> b) -> b -> [n]a -> [n+1]b
scanr   : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]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

iterate : {a} (a -> a) -> a -> [inf]a
repeat  : {n, a} a -> [n]a
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
uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c
curry   : {a, b, c} ((a, b) -> c) -> a -> b -> c