literate cryptol specifications

Common/GF24.cry

@@ -0,0 +1,47 @@
+module Common::GF24 where
+
+type GF24 = [4]
+
+irreducible = <| x^^4 + x + 1 |>
+
+// Addition in GF24
+gf24Add : {n} (fin n) => [n]GF24 -> GF24
+gf24Add ps = foldl (^) zero ps
+
+// Polynomial multiplication in GF24
+gf24Mult : GF24 -> GF24 -> GF24
+gf24Mult x y = pmod (pmult x y) irreducible
+
+// Define a power of an element in GF24
+gf24Pow : GF24 -> GF24 -> GF24
+gf24Pow n k = pow k
+    where
+        sq x = gf24Mult x x
+        pow i = if i == 0 then 1
+                else if i ! 0
+                     then gf24Mult n (sq (pow (i >> 1)))
+                     else sq (pow (i >> 1))
+
+// Self adding gives zero
+polySelfAdd' : GF24 -> Bit
+property polySelfAdd' x = x ^ x == zero
+
+// Inverse of an element in GF24
+gf24Inverse : GF24 -> GF24
+gf24Inverse x = gf24Pow x 14
+
+property gf24InverseCorrect x = gf24Inverse (gf24Inverse x) == x
+
+// Dot product in GF24
+gf24DotProduct : {n} (fin n) => [n]GF24 -> [n]GF24 -> GF24
+gf24DotProduct xs ys = gf24Add [ gf24Mult x y | x <- xs | y <- ys ]
+
+// Vector multiplication in GF24
+gf24VectorMult : {n, m} (fin n) => [n]GF24 -> [m][n]GF24 -> [m]GF24
+gf24VectorMult v ms = [ gf24DotProduct v m | m <- ms ]
+
+// Matrix multiplication in GF24
+gf24MatrixMult : {n, m, k} (fin m) => [n][m]GF24 -> [m][k]GF24 -> [n][k]GF24
+gf24MatrixMult xss yss = [ gf24VectorMult xs yss' | xs <- xss ]
+    where
+        yss' = transpose yss

Primitive/Symmetric/Cipher/Block/AES/GF28.cry → Common/GF28.cry

@@ -1,4 +1,4 @@
-module Primitive::Symmetric::Cipher::Block::AES::GF28 where
+module Common::GF28 where
 
 type GF28 = [8]
 
@@ -7,8 +7,7 @@ irreducible = <| x^^8 + x^^4 + x^^3 + x + 1 |>
 
 /** Sum up a bunch of GF28 values */
 gf28Add : {n} (fin n) => [n]GF28 -> GF28
-gf28Add ps = sums ! 0
-  where sums = [zero] # [  p ^ s | p <- ps | s <- sums ]
+gf28Add ps = foldl (^) zero ps
 
 /** Multiply two GF28 values */
 gf28Mult : GF28 -> GF28 -> GF28
@@ -18,16 +17,17 @@ gf28Mult x y = pmod (pmult x y) irreducible
 gf28Pow : GF28 -> [8] -> GF28
 gf28Pow n k = pow k
   where   sq x  = gf28Mult x x
-          odd x = x ! 0
           pow i = if i == 0 then 1
-                  else if odd i
+                  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
+
 /** 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 ]
@@ -37,8 +37,7 @@ gf28VectorMult : {n, m} (fin n) => [n]GF28 -> [m][n]GF28 -> [m]GF28
 gf28VectorMult v ms = [ gf28DotProduct v m | m <- ms ]
 
 /** Multiply two matrices */
-gf28MatrixMult : {n, m, k} (fin m) => [n][m]GF28 -> [m][k]GF28 -> [n][k]GF28
+gf28MatrixMult : {n, m, k} (fin m)
+              => [n][m]GF28 -> [m][k]GF28 -> [n][k]GF28
 gf28MatrixMult xss yss = [ gf28VectorMult xs yss' | xs <- xss ]
    where yss' = transpose yss
-
-