add periods

Primitive/Symmetric/Cipher/Block/Speck/Specification.cry

@@ -73,7 +73,7 @@ encrypt key plaintext = join (Speck_k (split plaintext))
  * The Speck decryption function is the inverse of the encryption function.
  * To derive the inverse, the round functions are composed in reverse order.
  *
- * Reference: [SPECK], Section 4.1
+ * Reference: [SPECK], Section 4.1.
  */
 decrypt : [m * n] -> [2 * n] -> [2 * n]
 decrypt key ciphertext = join (Speck_k (split ciphertext))
@@ -100,7 +100,7 @@ private
      * on the constituent functions that make up the round
      * function.
      *
-     * Reference: [Speck], Section 4.2
+     * Reference: [Speck], Section 4.2.
      */
     keySchedule : [m][n] -> [T][n]
     keySchedule K = ks
@@ -117,7 +117,7 @@ private
      * this formula leaves the definitions folded to illuminate the usage of
      * the constituent functions.
      *
-     * Reference: [SPECK], Section 4.2
+     * Reference: [SPECK], Section 4.2.
      */
     keySchedule' : [m][n] -> [T][n]
     keySchedule' K = ks
@@ -145,7 +145,7 @@ private
             result = keySchedule k != keySchedule v
 
     /**
-     * The key schedule formulations are equiavalent
+     * The key schedule formulations are equiavalent.
      *
      * ```repl
      * :prove keySchedulesEquivalent
@@ -157,15 +157,15 @@ private
      * The Speck round function. This function is parameterized by a key.
      * This function is a composition of shifts and modular additions.
      *
-     * Reference: [SPECK], Section 4.1
+     * Reference: [SPECK], Section 4.1.
      */
     R : [n] -> [2][n] -> [2][n]
     R k [x, y] = [(Sa_Inv x + y) ^ k, Sb y ^ (Sa_Inv x + y) ^ k]
 
     /**
      * The inverse Speck round function.
      *
-     * Reference: [SPECK], Section 4.1
+     * Reference: [SPECK], Section 4.1.
      */
     R_Inv : [n] -> [2][n] -> [2][n]
     R_Inv k [x, y] = [Sa ((x ^ k) - Sb_Inv (x ^ y)), Sb_Inv (x ^ y)]
@@ -185,7 +185,7 @@ private
      * map with addition modulo `2^n`. Part of this function's
      * output is used in the key schedule.
      *
-     * Reference: [SPECK], Section 4.1, 4.2
+     * Reference: [SPECK], Section 4.1, 4.2.
      */
     Rf1 : [n] -> [2][n] -> [2][n]
     Rf1 k [x, y] = [y, (Sa_Inv x + y) ^ k]
@@ -198,7 +198,7 @@ private
      *
      * Note that this function has no key dependence.
      *
-     * Reference: [SPECK], Section 4.1, 4.2
+     * Reference: [SPECK], Section 4.1, 4.2.
      */
     Rf2 : [2][n] -> [2][n]
     Rf2 [x, y] = [y, Sb x ^ y]