Reference.cry

module Cryptol::Reference where

/**
 * Performs multiplication of polynomials over GF(2).
 * Reference implementation.
 */
pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]
pmult x y = last zs
  where
    zs = [0] # [ (z << (1 : [8])) ^ (if yi then 0 # x else 0) | yi <- y | z <- zs ]

/**
 * Performs division of polynomials over GF(2).
 * Reference implementation.
 */
pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
pdiv x y = [ z ! degree | z <- zs ]
  where
    degree : [width v]
    degree = last (ds : [1 + v]_)
      where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]

    reduce : [v] -> [v]
    reduce u = if u ! degree then u ^ y else u

    zs : [u][v]
    zs = [ tail (reduce z # [xi]) | z <- [0] # zs | xi <- x ]

/**
 * Performs modulus of polynomials over GF(2).
 * Reference implementation.
 */
pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
pmod x y = if y == 0 then 0/0 else last zs
  where
    degree : [width v]
    degree = last (ds : [2 + v]_)
      where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]

    reduce : [1 + v] -> [1 + v]
    reduce u = if u ! degree then u ^ y else u

    powers : [inf][1 + v]
    powers = [reduce 1] # [ reduce (p << (1 : [8])) | p <- powers ]

    zs = [0] # [ z ^ (if xi then tail p else 0) | xi <- reverse x | p <- powers | z <- zs ]

/**
 * Functional left fold.
 *
 * foldl (+) 0 [1,2,3] = ((0 + 1) + 2) + 3
 *
 * Reference implementation.
 */
foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
foldl f z bs = last (scanl f z bs)

/**
 * Functional left fold, with strict evaluation of the accumulator value.
 *
 * The reference evaluator does not model evaluation strategy, so for the
 * purpose of giving semantics this is identical to `foldl`.
 *
 * Reference implementation.
 */
foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a
foldl' f z bs = foldl f z bs

/**
 * Functional left fold that can conditionally stop early.
 *
 * Returns the accumulator when the array has been fully traversed
 * or when the function returns `False`.
 *
 * let f = \a b -> (b < 10, max a b)
 * foldWhile f 0 [1, 2, 3] == 3
 * foldWhile f 0 [1, 2, 10, 8] == 10
 * foldWhile f 0 [10, 8, 6] == 10
 */
foldWhile : {n, a, b} (fin n) => (a -> b -> (Bool, a)) -> a -> [n]b -> a
foldWhile f z bs
  | n == 0 => z
  | n > 0 => if c then foldWhile f z' ys else z'
    where
      [y] # ys = bs
      (c, z') = f z y

/**
 * Scan left is like a foldl that also emits the intermediate values.
 *
 * Reference implementation.
 */
scanl : {n, a, b}  (a -> b -> a) -> a -> [n]b -> [1+n]a
scanl f z bs = as
  where
    as = [z] # [ f a b | a <- as | b <- bs ]

/**
 * Map a function iteratively over a seed value, producing an infinite
 * list of successive function applications.
 *
 * Reference implementation.
 */
iterate : {a} (a -> a) -> a -> [inf]a
iterate f z = xs
  where xs = [z] # [ f x | x <- xs ]