aes: add code fences to property checking #77

Adds an explicit demo of how to prove / check each property

Common/GF28.cry

@@ -73,7 +73,9 @@ matrixMult xss yss = [ vectorMult xs yss' | xs <- xss ]
 
 /**
  * [FIPS-197u1] Section 4.4, Algorithm 4.10
- * This proves quickly!
+ * ```cryptol
+ * :prove inverseDefined
+ * ```
  */
 property inverseDefined x =
   if x == 0 then inverse x == 0
@@ -91,6 +93,9 @@ inverse : GF28 -> GF28
 inverse x = pow x 254
 
 /**
- * Correctness property for inverses. This proves quickly!
+ * Correctness property for inverses.
+ * ```cryptol
+ * :prove inverseCorrect
+ * ```
  */
 property inverseCorrect x = inverse (inverse x) == x

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

@@ -130,14 +130,35 @@ InvMixColumns : State -> State
 InvMixColumns state = GF28::matrixMult m state
     where m = [[0x0e, 0x0b, 0x0d, 0x09] >>> i | i <- [0 .. 3] ]
 
-// This proves.
+/**
+ * SubBytes inversion must be correctly defined.
+ * ```cryptol
+ * :prove subBytesInverts `{Mode=0}
+ * :prove subBytesInverts `{Mode=1}
+ * :prove subBytesInverts `{Mode=2}
+ * ```
+ */
 subBytesInverts : State -> Bool
 property subBytesInverts s = InvSubBytes (SubBytes s) == s
 
-// This proves.
+/**
+ * ShiftRows inversion must be correctly defined.
+ * ```cryptol
+ * :prove shiftRowsInverts `{Mode=0}
+ * :prove shiftRowsInverts `{Mode=1}
+ * :prove shiftRowsInverts `{Mode=2}
+ * ```
+ */
 shiftRowsInverts : State -> Bool
 property shiftRowsInverts s = InvShiftRows (ShiftRows s) == s
 
-// This checks (non-exhaustively).
+/**
+ * MixColumns inversion must be correctly defined.
+ * ```cryptol
+ * :check mixColumnsInverts `{Mode=0}
+ * :check mixColumnsInverts `{Mode=1}
+ * :check mixColumnsInverts `{Mode=2}
+ * ```
+ */
 mixColumnsInverts : State -> Bool
 property mixColumnsInverts s = InvMixColumns (MixColumns s) == s

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

@@ -34,5 +34,10 @@ sboxInv = [ GF28::inverse (transformInv b) | b <- [0 .. 255] ] where
     transformInv b = GF28::add [(b >>> 2), (b >>> 5), (b >>> 7), d]
     d = 0x05
 
-// This `:prove`s efficiently.
+/**
+ * S-box inversion must be correctly defined.
+ * ```cryptol
+ * :prove sBoxInverts
+ * ```
+ */
 property sBoxInverts b = sboxInv @ ( sbox @ b) == b

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

@@ -44,7 +44,9 @@ stateToMsg st = join (join (transpose st))
  * Note that we don't ever need this property in the execution of AES,
  * but it should hold true anyway.
  *
- * This `:prove`s quickly.
+ * ```cryptol
+ * :prove ioInverts
+ * ```
  */
 property ioInverts msg = stateToMsg (msgToState msg) == msg
 

Primitive/Symmetric/Cipher/Block/AES_specification.cry

@@ -42,8 +42,14 @@ encrypt k = encryptWithSchedule (keyExpansion k)
 decrypt : [KeySize] -> [BlockSize] -> [BlockSize]
 decrypt k = decryptWithSchedule (keyExpansion 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.
+/*
+ * This property must be true for each instantiation.
+ * With high probability, it will be extremely slow to prove.
+ *
+ * ```cryptol
+ * :check aesIsCorrect
+ * ```
+ */
 property aesIsCorrect k pt = decrypt k (encrypt k pt) == pt
 
 // The following methods should not be used in general. They are public

Primitive/Symmetric/Cipher/Block/Tests/TestAES.cry

@@ -11,18 +11,17 @@ import Primitive::Symmetric::Cipher::Block::AES192 as AES192
 import Primitive::Symmetric::Cipher::Block::AES128 as AES128
 import Primitive::Symmetric::Cipher::Block::AES256 as AES256
 
-// These properties must be true, but they will probably take an
-// extraordinarily long time to prove.
-property aes128Correct msg key = AES128::decrypt key (AES128::encrypt key msg) == msg
-property aes192Correct msg key = AES192::decrypt key (AES192::encrypt key msg) == msg
-property aes256Correct msg key = AES256::decrypt key (AES256::encrypt key msg) == msg
-
 // These test vectors must all come from the same place, because they use the same plaintexts
 pts = [0x6bc1bee22e409f96e93d7e117393172a
   ,0xae2d8a571e03ac9c9eb76fac45af8e51
   ,0x30c81c46a35ce411e5fbc1191a0a52ef
   ,0xf69f2445df4f9b17ad2b417be66c3710]
 
+/**
+ * ```cryptol
+ * :prove aes128TestVectorsPass
+ * ```
+ */
 property aes128TestVectorsPass = and encryptions /\ and decryptions
     where
         key = 0x2b7e151628aed2a6abf7158809cf4f3c
@@ -33,7 +32,11 @@ property aes128TestVectorsPass = and encryptions /\ and decryptions
         encryptions = [ AES128::encrypt key msg == ct | msg <- pts | ct <- expected_cts ]
         decryptions = [ AES128::decrypt key ct == pt | pt <- pts | ct <- expected_cts ]
 
-
+/**
+ * ```cryptol
+ * :prove aes192TestVectorsPass
+ * ```
+ */
 property aes192TestVectorsPass = and encryptions /\ and decryptions
     where
         key = 0x8e73b0f7da0e6452c810f32b809079e562f8ead2522c6b7b
@@ -44,6 +47,11 @@ property aes192TestVectorsPass = and encryptions /\ and decryptions
         encryptions = [ AES192::encrypt key msg == ct | msg <- pts | ct <- expected_cts ]
         decryptions = [ AES192::decrypt key ct == pt | pt <- pts | ct <- expected_cts ]
 
+/**
+ * ```cryptol
+ * :prove aes256TestVectorsPass
+ * ```
+ */
 property aes256TestVectorsPass = and encryptions /\ and decryptions
     where
         key = 0x603deb1015ca71be2b73aef0857d77811f352c073b6108d72d9810a30914dff4