modes: add cipher interface, define for AES #80

Primitive/Symmetric/Cipher/Block/AES_specification.cry

@@ -13,7 +13,6 @@ module Primitive::Symmetric::Cipher::Block::AES_specification where
 import `Primitive::Symmetric::Cipher::Block::AES::Algorithm as AES
 import `Primitive::Symmetric::Cipher::Block::AES::ExpandKey
 import Primitive::Symmetric::Cipher::Block::AES::TBox
-import Primitive::Symmetric::Cipher::Block::Cipher(Cipher)
 
 parameter
    // This constraint enforces the standard key sizes of 128, 192, and
@@ -26,39 +25,37 @@ parameter
 // Mode 0 = 128 bits; Mode 1 = 192 bits; Mode 2 = 256 bits
 type Mode = (KeySize / 64) - 2
 
-// Make KeySize accessible outside the module.
+// Make `KeySize` and `BlockSize` accessible outside the module.
+// This also lets us use AES as an instantiation of `CipherInterface`
 type KeySize = KeySize'
+type BlockSize = 128
 
-type EncryptionKey = AES::KeySchedule Mode
-type DecryptionKey = AES::KeySchedule Mode
-
-AES: Cipher KeySize 128
-AES = { encrypt key pt = encrypt key pt
-      , decrypt key ct = decrypt key ct
-      }
-
-encrypt : [KeySize] -> [128] -> [128]
+encrypt : [KeySize] -> [BlockSize] -> [BlockSize]
 encrypt k = encryptWithSchedule (expandKeyEnc k)
 
-decrypt : [KeySize] -> [128] -> [128]
+decrypt : [KeySize] -> [BlockSize] -> [BlockSize]
 decrypt k = decryptWithSchedule (expandKeyDec k)
 
+type EncryptionKey = AES::KeySchedule Mode
+type DecryptionKey = AES::KeySchedule Mode
+
 expandKeyEnc : [KeySize] -> EncryptionKey
 expandKeyEnc = expandKey`{Nk = AES::Nk Mode, Nr = AES::Nr Mode}
 
-encryptWithSchedule : EncryptionKey -> [128] -> [128]
+encryptWithSchedule : EncryptionKey -> [BlockSize] -> [BlockSize]
 encryptWithSchedule = AES::encrypt params
 
 expandKeyDec : [KeySize] -> EncryptionKey
 expandKeyDec k = makeDecKey (expandKey`{Nk = AES::Nk Mode, Nr = AES::Nr Mode} k)
 
 // AES decryption with a specified KeySchedule
-decryptWithSchedule : DecryptionKey -> [128] -> [128]
+decryptWithSchedule : DecryptionKey -> [BlockSize] -> [BlockSize]
 decryptWithSchedule = AES::decrypt params
 
 params = { encRound = AESRound, decRound = AESInvRound }
 
-// This property should be true; it's not provable as-is because it's not monomorphic.
+// This property must be true; it's not provable as-is because it's not monomorphic.
 // It should be instantiated separately for each key size.
+// With high probability, it will be extremely slow to prove and should be `:check`ed.
 property aesIsCorrect k pt = decrypt k (encrypt k pt) == pt
 

Primitive/Symmetric/Cipher/Block/CipherInterface.cry

@@ -0,0 +1,12 @@
+/*
+ * This is a basic interface for block ciphers that can be used with most
+ * modes of operation.
+ *
+ */
+
+interface module Primitive::Symmetric::Cipher::Block::CipherInterface where
+  type KeySize : #
+  type BlockSize : #
+  type constraint (fin BlockSize, fin KeySize)
+  encrypt : [KeySize] -> [BlockSize] -> [BlockSize]
+  decrypt : [KeySize] -> [BlockSize] -> [BlockSize]