aes: improve state documentation #77

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

@@ -2,12 +2,51 @@ module Primitive::Symmetric::Cipher::Block::AES::State where
 
 import Common::GF28
 
-type State       = [4][Nb]GF28
-type Nb          = 4
-type RoundKey    = State
+/**
+ * The number of words in the state is generic for the underlying Rijndael
+ * algorithm, but in the standard it is fixed to 4.
+ * [FIPS-197u1] Section 5.
+ */
+type Nb = 4
 
+/**
+ * The algorithms for AES block ciphers are performed on a 4x4 array of bytes.
+ * [FIPS-197u1] Section 3.4.
+ */
+type State = [4][Nb]GF28
+
+/**
+ * In the specifications for AES, the first step is to copy the input array
+ * of 16 bytes into the state array.
+ *
+ * [FIPS-197u1] Section 3.4, Equation 3.6.
+ */
 msgToState : [128] -> State
 msgToState msg = transpose (split (split msg))
 
+/**
+ * After the state array is transformed, its final value is copied to the
+ * output array of bytes.
+ *
+ * [FIPS-197u1] Section 3.4, Equation 3.7.
+ */
 stateToMsg : State -> [128]
 stateToMsg st = join (join (transpose st))
+
+/**
+ * This demonstrates the property in [FIPS-197u1] Section 3.4, Figure 1.
+ * Note that we don't ever need this property in the execution of AES,
+ * but it should hold true anyway.
+ *
+ * This `:prove`s quickly.
+ */
+property ioInverts msg = stateToMsg (msgToState msg) == msg
+
+
+/**
+ * The round key is a block that is usually represented as a sequence of four words.
+ * [FIPS-197u1] Section 5.
+ *
+ * A word is a sequence of four bytes. [FIPS-197u1] Section 3.5.
+ */
+type RoundKey = [4][4]GF28

Primitive/Symmetric/Cipher/Block/AES_specification.cry

@@ -22,7 +22,7 @@ import `Primitive::Symmetric::Cipher::Block::AES::ExpandKey
 
 parameter
    // This constraint enforces the standard key sizes of 128, 192, and
-   // 256-bits [FIPS-PUB-197 Sections 1, 5, and 6.1].
+   // 256-bits. [FIPS-197u1] Sections 1, 5, and 6.1.
    type KeySize' : #
    type constraint (fin KeySize', KeySize' % 64 == 0, KeySize' / 64 >= 2, KeySize' / 64 <= 4)