gf28: update GF28 module to match spec #77

- modify naming and call sites
- modifies the order a little bit
- adds documentation, esp. references to where things live in the spec.

Common/GF28.cry

@@ -1,43 +1,91 @@
+//
+// Implementation of the finite field GF(2^8).
+//
+// @copyright Galois, Inc
+// @author Nichole Shimanski <[email protected]>
+// @author Alannah Carr
+// @author Marcella Hastings <[email protected]>
+//
+// This implementation is drawn from the description of the Galois Field
+// GF(2^8) in [FIPS-197u1], Section 4.
+//
+// References
+// [FIPS-197u1]: Morris J. Dworkin, Elaine B. Barker, James R. Nechvatal,
+// James Foti, Lawrence E. Bassham, E. Roback, and James F. Dray Jr.
+// Advanced Encryption Standard (AES). Federal Inf. Process. Stds. (NIST FIPS)
+// 197, update 1. May 2023.
+//
 module Common::GF28 where
 
+/**
+ * The GF28 type represents a byte, where each bit is the coefficient of a
+ * polynomial. [FIPS-197u1] Section 4, Algorithm 4.1.
+ *
+ * Both the spec and this implementation represent GF28 elements in big-endian
+ * format.
+ */
 type GF28 = [8]
 
-/** The irreducable polynomial */
-irreducible = <| x^^8 + x^^4 + x^^3 + x + 1 |>
+/**
+ * Add a set of `n` elements in GF28. [FIPS-197u1] Section 4.1.
+ *
+ * Addition is computed by pairwise adding the coefficients modulo 2.
+ */
+add : {n} (fin n) => [n]GF28 -> GF28
+add ps = foldl (^) zero ps
 
-/** Sum up a bunch of GF28 values */
-gf28Add : {n} (fin n) => [n]GF28 -> GF28
-gf28Add ps = foldl (^) zero ps
+/**
+ * The irreducable polynomial used in multiplication.
+ * [FIPS-197u1] Section 4.2, Algorithm 4.3
+ */
+irreducible = <| x^^8 + x^^4 + x^^3 + x + 1 |>
 
-/** Multiply two GF28 values */
-gf28Mult : GF28 -> GF28 -> GF28
-gf28Mult x y = pmod (pmult x y) irreducible
+/**
+ * Multiply two elements in GF28. [FIPS-197u1] Section 4.2.
+ */
+mult : GF28 -> GF28 -> GF28
+mult x y = pmod (pmult x y) irreducible
 
 /** A GF28 value to a scalar power */
-gf28Pow : GF28 -> [8] -> GF28
-gf28Pow n k = pow k
-  where   sq x  = gf28Mult x x
-          pow i = if i == 0 then 1
+pow : GF28 -> [8] -> GF28
+pow n k = pow' k
+  where   sq x  = mult x x
+          pow' i = if i == 0 then 1
                   else if i ! 0  // if odd
-                       then gf28Mult n (sq (pow (i >> 1)))
-                       else sq (pow (i >> 1))
-
-/** Compute the inverse of a value */
-gf28Inverse : GF28 -> GF28
-gf28Inverse x = gf28Pow x 254
-
-property gf28InverseCorrect x = gf28Inverse (gf28Inverse x) == x
+                       then mult n (sq (pow' (i >> 1)))
+                       else sq (pow' (i >> 1))
 
 /** Dot product of two vectors */
-gf28DotProduct : {n} (fin n) => [n]GF28 -> [n]GF28 -> GF28
-gf28DotProduct xs ys = gf28Add [ gf28Mult x y | x <- xs | y <- ys ]
+dotProduct : {n} (fin n) => [n]GF28 -> [n]GF28 -> GF28
+dotProduct xs ys = add [ mult x y | x <- xs | y <- ys ]
 
 /** Multiply a matrix by a vector */
-gf28VectorMult : {n, m} (fin n) => [n]GF28 -> [m][n]GF28 -> [m]GF28
-gf28VectorMult v ms = [ gf28DotProduct v m | m <- ms ]
+vectorMult : {n, m} (fin n) => [n]GF28 -> [m][n]GF28 -> [m]GF28
+vectorMult v ms = [ dotProduct v m | m <- ms ]
 
-/** Multiply two matrices */
-gf28MatrixMult : {n, m, k} (fin m)
+/**
+ * Multiply two matrices. [FIPS-197u1] Section 4.3
+ */
+matrixMult : {n, m, k} (fin m)
               => [n][m]GF28 -> [m][k]GF28 -> [n][k]GF28
-gf28MatrixMult xss yss = [ gf28VectorMult xs yss' | xs <- xss ]
+matrixMult xss yss = [ vectorMult xs yss' | xs <- xss ]
    where yss' = transpose yss
+
+/**
+ * [FIPS-197u1] Section 4.4, Algorithm 4.10
+ * This proves quickly!
+ */
+property inverseDefined x =
+  if x == 0 then True
+  else mult x (inverse x) == 1
+
+/**
+ * Compute the inverse of a value. [FIPS-197u1 Section 4.4, Algorithm 4.11
+ */
+inverse : GF28 -> GF28
+inverse x = pow x 254
+
+/**
+ * Correctness property for inverses. This proves quickly!
+ */
+property inverseCorrect x = inverse (inverse x) == x

Primitive/Symmetric/Cipher/Block/AES/ExpandKey.cry

@@ -1,6 +1,7 @@
 module Primitive::Symmetric::Cipher::Block::AES::ExpandKey where
 
-import Common::GF28
+import Common::GF28 as GF28
+private type GF28 = GF28::GF28
 import Primitive::Symmetric::Cipher::Block::AES::State
 import Primitive::Symmetric::Cipher::Block::AES::SubByteSBox
 
@@ -36,7 +37,7 @@ keyWS seed    = xs
 
 // Key expansion
 Rcon : [8] -> [4]GF28
-Rcon i = [ gf28Pow <| x |> (i-1), 0, 0, 0]
+Rcon i = [ GF28::pow <| x |> (i-1), 0, 0, 0]
 
 SubWord : [4]GF28 -> [4]GF28
 SubWord bs = [ SubByte b | b <- bs ]

Primitive/Symmetric/Cipher/Block/AES/Round.cry

@@ -1,6 +1,6 @@
 module Primitive::Symmetric::Cipher::Block::AES::Round where
 
-import Common::GF28
+import Common::GF28 as GF28
 import Primitive::Symmetric::Cipher::Block::AES::State
 import Primitive::Symmetric::Cipher::Block::AES::SubByteSBox
 
@@ -15,7 +15,7 @@ ShiftRows : State -> State
 ShiftRows state = [ row <<< i | row <- state | i : [2] <- [0 .. 3] ]
 
 MixColumns : State -> State
-MixColumns state = gf28MatrixMult m state
+MixColumns state = GF28::matrixMult m state
     where m = [ [2,3,1,1] >>> i | i <- [0 .. 3] ]
 
 /** The final AES round */
@@ -37,7 +37,7 @@ InvShiftRows state = [ row >>> shiftAmount | row <- state
                      ]
 
 InvMixColumns : State -> State
-InvMixColumns state = gf28MatrixMult m state
+InvMixColumns state = GF28::matrixMult m state
     where m = [[0x0e, 0x0b, 0x0d, 0x09] >>> i | i <- [0 .. 3] ]
 
 /** The final inverted AES round */

Primitive/Symmetric/Cipher/Block/AES/SubBytePlain.cry

@@ -1,19 +1,20 @@
 module Primitive::Symmetric::Cipher::Block::AES::SubBytePlain where
 
-import Common::GF28
+import Common::GF28 as GF28'
+private type GF28 = GF28'::GF28
 
 // The SubBytes transform and its inverse
 SubByte : GF28 -> GF28
-SubByte b = xformByte (gf28Inverse b)
+SubByte b = xformByte (GF28'::inverse b)
 
 InvSubByte : GF28 -> GF28
-InvSubByte b = gf28Inverse (xformByte' b)
+InvSubByte b = GF28'::inverse (xformByte' b)
 
 
 // The affine transform and its inverse
 xformByte : GF28 -> GF28
-xformByte b = gf28Add [b, (b >>> 4), (b >>> 5), (b >>> 6), (b >>> 7), c]
+xformByte b = GF28'::add [b, (b >>> 4), (b >>> 5), (b >>> 6), (b >>> 7), c]
    where c = 0x63
 
 xformByte' : GF28 -> GF28
-xformByte' b = gf28Add [(b >>> 2), (b >>> 5), (b >>> 7), d] where d = 0x05
+xformByte' b = GF28'::add [(b >>> 2), (b >>> 5), (b >>> 7), d] where d = 0x05

Primitive/Symmetric/Cipher/Block/AES/TBox.cry

@@ -1,6 +1,7 @@
 module Primitive::Symmetric::Cipher::Block::AES::TBox where
 
-import Common::GF28
+import Common::GF28 as GF28'
+private type GF28 = GF28'::GF28
 import Primitive::Symmetric::Cipher::Block::AES::State
 import Primitive::Symmetric::Cipher::Block::AES::SBox
 import Primitive::Symmetric::Cipher::Block::AES::Round
@@ -33,4 +34,4 @@ tboxInv = mkTBox [ 0x0e, 0x09, 0x0d, 0x0b ] sboxInv
 mkTBox : [4]GF28 -> SBox -> TBox
 mkTBox seed box = [ [ a >>> i | a <- t0 ] | i <- [0 .. 3] ]
   where
-  t0 = [ [ gf28Mult c s | c <- seed ] | s <- box ]
+  t0 = [ [ GF28'::mult c s | c <- seed ] | s <- box ]

Primitive/Symmetric/Cipher/Block/AES_specification.cry

@@ -38,6 +38,13 @@ encrypt k = encryptWithSchedule (expandKeyEnc k)
 decrypt : [KeySize] -> [BlockSize] -> [BlockSize]
 decrypt k = decryptWithSchedule (expandKeyDec k)
 
+// This property must be true. It should be proven for each instantiation.
+// With high probability, it will be extremely slow to prove and should be `:check`ed.
+property aesIsCorrect k pt = decrypt k (encrypt k pt) == pt
+
+// The following methods should not be used in general. They are public
+// to support a confusing endianness issue in the implementation of
+// AES-GCM-SIV.
 type EncryptionKey = AES::KeySchedule Mode
 type DecryptionKey = AES::KeySchedule Mode
 
@@ -47,17 +54,14 @@ expandKeyEnc = expandKey`{Nk = AES::Nk Mode, Nr = AES::Nr Mode}
 encryptWithSchedule : EncryptionKey -> [BlockSize] -> [BlockSize]
 encryptWithSchedule = AES::encrypt params
 
-expandKeyDec : [KeySize] -> EncryptionKey
-expandKeyDec k = makeDecKey (expandKey`{Nk = AES::Nk Mode, Nr = AES::Nr Mode} k)
+private
+   expandKeyDec : [KeySize] -> EncryptionKey
+   expandKeyDec k = makeDecKey (expandKey`{Nk = AES::Nk Mode, Nr = AES::Nr Mode} k)
 
-// AES decryption with a specified KeySchedule
-decryptWithSchedule : DecryptionKey -> [BlockSize] -> [BlockSize]
-decryptWithSchedule = AES::decrypt params
+   // AES decryption with a specified KeySchedule
+   decryptWithSchedule : DecryptionKey -> [BlockSize] -> [BlockSize]
+   decryptWithSchedule = AES::decrypt params
 
-params = { encRound = AESRound, decRound = AESInvRound }
+   params = { encRound = AESRound, decRound = AESInvRound }
 
-// This property must be true; it's not provable as-is because it's not monomorphic.
-// It should be instantiated separately for each key size.
-// With high probability, it will be extremely slow to prove and should be `:check`ed.
-property aesIsCorrect k pt = decrypt k (encrypt k pt) == pt