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) ^ (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) | 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)

/**
 * 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 ]