AES cleanup fixes pt 1 for #179

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

@@ -52,13 +52,13 @@ cipher: KeySchedule -> [128] -> [128]
 cipher (kInit,ks,kFinal) pt = stateToMsg final_state // Line 13
   where
     // Lines 2-3
-    state0 = kInit ^ msgToState pt
+    state0 = AddRoundKey kInit (msgToState pt)
     // Line 4
     rounds = [state0] # [ transform w state | w <- ks | state <- rounds ]
-    // Liens 5-8
-    transform w state = w ^ MixColumns (ShiftRows (SubBytes state))
+    // Lines 5-8
+    transform w state = AddRoundKey w (MixColumns (ShiftRows (SubBytes state)))
     // Lines 10-12
-    final_state = kFinal ^ ShiftRows (SubBytes (rounds ! 0))
+    final_state = AddRoundKey kFinal (ShiftRows (SubBytes (rounds ! 0)))
 
 /**
  * SubBytes applies an invertible, non-linear transformation to the state.
@@ -67,7 +67,7 @@ cipher (kInit,ks,kFinal) pt = stateToMsg final_state // Line 13
  * It does so by applying the AES S-box independently to each byte in the state.
  */
 SubBytes : State -> State
-SubBytes state = [ [ sbox @ b | b <- row ] | row <- state ]
+SubBytes state = [ [ sbox b | b <- row ] | row <- state ]
 
 /**
  * ShiftRows transforms the state by cycling the last three rows.
@@ -84,6 +84,13 @@ MixColumns : State -> State
 MixColumns state = GF28::matrixMult m state
     where m = [ [2,3,1,1] >>> i | i <- [0 .. 3] ]
 
+/**
+ * AddRoundKey combines the state with a round key via the
+ * bitwise XOR operator
+ * [FIPS-197u1] Section 5.1.4
+ */
+AddRoundKey : RoundKey -> State -> State
+AddRoundKey w state = w ^ state
 
 /**
  * The general function for inverting AES with 128-, 192-, or 256-bit keys.
@@ -100,13 +107,13 @@ invCipher: KeySchedule -> [128] -> [128]
 invCipher (kInit, ks, kFinal) ct = stateToMsg final_state // Line 13
   where
     // Lines 2-3
-    state0 = kFinal ^ msgToState ct
+    state0 = AddRoundKey kFinal ( msgToState ct)
     // Line 4
     rounds = [state0] # [ transform w state | w <- (reverse ks) | state <- rounds ]
     // Lines 5-8
-    transform w state = InvMixColumns (w ^ InvSubBytes (InvShiftRows state))
+    transform w state = InvMixColumns (AddRoundKey w (InvSubBytes (InvShiftRows state)))
     // Lines 10-12
-    final_state = kInit ^ InvSubBytes (InvShiftRows (rounds ! 0))
+    final_state = AddRoundKey kInit (InvSubBytes (InvShiftRows (rounds ! 0)))
 
 /**
  * Inverts the `ShiftRows` function.
@@ -120,7 +127,7 @@ InvShiftRows state = [ row >>> i | row <- state | i : [2] <- [0 .. 3] ]
  * [FIPS-197u1] Section 5.3.2
  */
 InvSubBytes : State -> State
-InvSubBytes state = [ [ sboxInv @ b | b <- row ] | row <- state ]
+InvSubBytes state = [ [ sboxInv b | b <- row ] | row <- state ]
 
 /**
  * Inverts the `MixColumns` function.

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

@@ -56,7 +56,7 @@ RotWord [a0, a1, a2, a3] = [a1, a2, a3, a0]
  * [FIPS-197u1] Equation 5.11.
  */
 SubWord : [4]GF28 -> [4]GF28
-SubWord as = [ Sbox::sbox @ a | a <- as ]
+SubWord [a0, a1, a2, a3] = [ Sbox::sbox a0, Sbox::sbox a1, Sbox::sbox a2, Sbox::sbox a3 ]
 
 /**
  * KeyExpansion() routine.

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

@@ -13,31 +13,45 @@ private type GF28 = GF28::GF28
 type SBox = [256] GF28
 
 /**
- * SBox: A non-linear substitution table for AES.
- * [FIPS-197u1] Section 5.1.1.
- *
- * `GF28::inverse b` corresponds to Equation 5.2.
+ * The substitution table as given in Table 4. The table is pulled out here
+ * for efficiency, letting us compute the table once per access in AES.
  */
-sbox : SBox
-sbox = [ transform (GF28::inverse b) | b <- [0 .. 255] ] where
+sboxTable : SBox
+private sboxTable = [ transform (GF28::inverse b) | b <- [0 .. 255] ] where
     // Equation 5.3.
     transform b = GF28::add [b, (b >>> 4), (b >>> 5), (b >>> 6), (b >>> 7), c]
     // The constant byte {01100011}.
     c = 0x63
 
 /**
- * Inverted substitution table for AES.
- * [FIPS-197u1] Section 5.3.2.
+ * SBox: A non-linear substitution table for AES.
+ * [FIPS-197u1] Section 5.1.1.
+ *
+ * `GF28::inverse b` corresponds to Equation 5.2.
  */
-sboxInv : SBox
-sboxInv = [ GF28::inverse (transformInv b) | b <- [0 .. 255] ] where
+sbox : GF28 -> GF28
+sbox b = sboxTable @ b
+
+/**
+ * The substitution table as given in Table 6. The table is pulled out here
+ * for efficiency, letting us compute the table once per access in AES.
+ */
+sboxInvTable : SBox
+private sboxInvTable = [ GF28::inverse (transformInv b) | b <- [0 .. 255] ] where
     transformInv b = GF28::add [(b >>> 2), (b >>> 5), (b >>> 7), d]
     d = 0x05
 
+/**
+ * Inverted substitution table for AES.
+ * [FIPS-197u1] Section 5.3.2.
+ */
+sboxInv : GF28 -> GF28
+sboxInv b = sboxInvTable @ b
+
 /**
  * S-box inversion must be correctly defined.
  * ```repl
  * :prove sBoxInverts
  * ```
  */
-property sBoxInverts b = sboxInv @ ( sbox @ b) == b
+property sBoxInverts b = sboxInv (sbox b) == b