Type checker not following conditional control flow.

[ramsdell]

The type checker fails to accept the following program.

recbug : {n, a} (fin n) => [2 ^^ n]a -> [2 ^^ n]a
recbug a =
  if `n == 0 then
    a
  else
    even # odd
    where
      even = recbug`{n - 1} (take a)
      odd = recbug`{n - 1} (drop a)

It appears that the problem is that the type checker doesn't infer
that n >= 1 in the else branch.

[error] at recbug.cry:2:1--9:36:
  Failed to validate user-specified signature.
    in the definition of 'Main::recbug', at recbug.cry:2:1--2:7,
    we need to show that
      for any type n, a
      assuming
        • fin n
      the following constraints hold:
        • 2 ^^ n == 2 * 2 ^^ (n - 1)
            arising from
            matching types
            at recbug.cry:6:5--6:15
        • n >= 1
            arising from
            use of partial type function (-)
            at recbug.cry:8:14--8:20
        • 2 ^^ n >= 2 ^^ (n - 1)
            arising from
            matching types
            at recbug.cry:8:35--8:36

This kind of function is useful for implementing O(n log n) number
theoretic transforms such as is used in Dilithium. I using Cryptol
version 2.12.0.

[robdockins]

CF #701, #325 and #704

This is something we've talked about quite a bit and would like to do, but requires some pretty complicated extensions to the typechecker to do correctly (our current thinking is that doing this properly requires implementing the OutsideIn typechecking algorithm instead of one based on Hindley-Milner).

Also, I think that even if you had n >= 1, you might still have problems getting Cryptol to reason about the exponents.

The coerceSize idea from #704 is probably the easiest workaround for the moment.

[jldodds]

Closing as duplicate with #701. @ramsdell please reach out if we can help with the workaround.

[weaversa]

Here's a working solution for @ramsdell's problem. Both coerceSize and max 1 n - 1 at the appropriate places are necessary.

rec : {n, a} (fin n) => [2 ^^ n]a -> [2 ^^ n]a
rec a =
    if `n == 0 then a
    else coerceSize (l' # r')
  where
    l # r = coerceSize a
    l' = rec`{max 1 n - 1} l
    r' = rec`{max 1 n - 1} r

coerceSize : {m, n, a} (fin m, fin n) => [m]a -> [n]a
coerceSize xs = assert (`m == `n) "coerceSize failed" [ xs @ i | i <- [0 .. <n]]

[ramsdell]

And with that knowledge, here is an O(n log n) NTT that type checks! (I haven't tested it yet with data.)

/* Recursive NTT for Dilithium. */

/*
 * Dilithium parameters:
 * q = 8380417
 * n = 256
 * r = 1753
 */

type q = 8380417

type Fld = Z q

/**
 * Primitive 512-th root of unity r mod q
 */
r : Fld
r = 1753

/**
 * Powers of the roots of unity
 * roots @ i = r ^^ i
 */
roots : [inf]Fld
roots = stream
  where stream = [ 1 ] # [ r * x | x <- stream ]

/**
 * An attempt at an O(n log(n)) number theortic transform for
 * Dilithium.  It type checks, but I haven't tested it with data yet.
 */
ntt : {n} (fin n) => [2 ^^ n]Fld -> [2 ^^ n]Fld
ntt a =
  if `n == 0 then
    a
  else
    coerceSize (butterfly even odd)
    where
      (lft, rht) = shuffle (coerceSize a)
      even = ntt`{max 1 n - 1} lft
      odd = ntt`{max 1 n - 1} rht

coerceSize : {m, n, a} [m]a -> [n]a
coerceSize xs = [ xs @ i | i <- [0 .. <n]]

/**
 * Group even indices in first half and odd indices in second half.
 */
shuffle : {n, a} (fin n, n > 0) => [2 * n]a -> ([n]a, [n]a)
shuffle a =
  ([ a @ (i * 2) | i <- [0 .. <n]], [ a @ (i * 2 + 1) | i <- [0 .. <n]])

/**
 * Perform the butterfly operation.
 */
butterfly : {n} (fin n, n > 0) => [n]Fld -> [n]Fld -> [2 * n]Fld
butterfly even odd =
  lft # rht
  where
    lft = [ even @ i + roots @ i * odd @ i | i <- [0 .. <n] ]
    rht = [ even @ i - roots @ i * odd @ i | i <- [0 .. <n] ]

[weaversa]

That reminds me of Knuth

Beware of bugs in the above code; I have only proved it correct, not tried it.

Some polish just for fun.

/* Recursive NTT for Dilithium. */

/*
 * Dilithium parameters:
 * q = 8380417
 * n = 256
 * r = 1753
 */

type q = 8380417

type Fld = Z q

/**
 * Primitive 512-th root of unity r mod q.
 */

r : Fld
r = 1753

/**
 * Powers of the roots of unity.
 */

roots : {a} [a]Fld
roots @ i = r ^^ i

/**
 * An attempt at an O(n log(n)) number theortic transform for
 * Dilithium. It type checks, but I haven't tested it with data yet.
 */

ntt : {n} (fin n) => [2 ^^ n]Fld -> [2 ^^ n]Fld
ntt a =
    if `n == 0 then a
    // Adventure!
    else coerceSize <~ butterfly <~ map ntt`{max 1 n - 1} <~ shuffle <~ coerceSize <~ a

/* or this...
else coerceSize (butterfly [ even, odd ])
  where
    [ lft, rht ] = shuffle (coerceSize a)
    even = ntt`{max 1 n - 1} lft
    odd  = ntt`{max 1 n - 1} rht
*/

/**
 * Group even indices in first half and odd indices in second half.
 */

shuffle : {n, a} [2 * n]a -> [2][n]a
shuffle a = transpose (split a)

/**
 * Perform the butterfly operation.
 */

butterfly : {n} (fin n) => [2][n]Fld -> [2 * n]Fld
butterfly [ even, odd ] = lft # rht
  where
    lft = even + roots * odd
    rht = even - roots * odd

private

(<~) : {a, b} (a -> b) -> a -> b
(<~) f x = f x
infixr 1 <~

coerceSize : {m, n, a} (fin m, fin n) => [m]a -> [n]a
coerceSize xs =
    assert
      (`m == `n)
      "Type error at runtime due to improper use of coerceSize"
      [ xs @ i | i <- [0 .. <n]]

[ramsdell]

And here is a version of the NTT that both type checks and along with the inverse NTT, checks out that applying the inverse NTT to the NTT is the identity function. Notice the correction in the butterfly operation.

/* Recursive NTT for Dilithium. */

/* It type checks, and it succeeds in meeting the nttCorrect property
   below which says that the inverse ntt applied to the ntt is the
   identity function. */

/*
 * Dilithium parameters:
 * q = 8380417
 * n = 256
 * r = 1753
 */

type q = 8380417

type Fld = Z q

type nn = 256

/**
 * Primitive 512-th root of unity r mod q
 */
r : Fld
r = 1753

/**
 * Powers of the squares of the primitive root of unity
 */
roots : [inf]Fld
roots = stream
  where stream = [ 1 ] # [ r * r * x | x <- stream ]

/**
 * An O(n log n) number theortic transform for Dilithium.
 */
ntt : {n} (fin n) => [2 ^^ n]Fld -> [2 ^^ n]Fld
ntt a = nttR`{n} 0 a

nttR : {n} (fin n) => Integer -> [2 ^^ n]Fld -> [2 ^^ n]Fld
nttR depth a =
  if `n == 0 then
    a
  else
    coerceSize (butterfly depth even odd)
    where
      (lft, rht) = shuffle (coerceSize a)
      even = nttR`{max 1 n - 1} (depth + 1) lft
      odd = nttR`{max 1 n - 1} (depth + 1) rht

coerceSize : {m, n, a} [m]a -> [n]a
coerceSize xs = [ xs @ i | i <- [0 .. <n]]

/**
 * Group even indices in first half and odd indices in second half.
 * This implementation uses list comprehension to make the code
 * obviously correct.
 */
shuffle : {n, a} (fin n, n > 0) => [2 * n]a -> ([n]a, [n]a)
shuffle a =
  ([ a @ (i * 2) | i <- [0 .. <n]], [ a @ (i * 2 + 1) | i <- [0 .. <n]])

/**
 * Perform the butterfly operation.
 */
butterfly : {n} (fin n, n > 0) => Integer -> [n]Fld -> [n]Fld -> [2 * n]Fld
butterfly depth even odd =
  lft # rht
  where
    j = 2 ^^ depth
    lft = [ even @ i + roots @ (i * j) * odd @ i | i <- [0 .. <n] ]
    rht = [ even @ i - roots @ (i * j) * odd @ i | i <- [0 .. <n] ]