diff --git a/Primitive/Keyless/Generator/DRBG.cry b/Primitive/Keyless/Generator/DRBG.cry
index 2af2a4c5..382ea6ae 100644
--- a/Primitive/Keyless/Generator/DRBG.cry
+++ b/Primitive/Keyless/Generator/DRBG.cry
@@ -5,9 +5,9 @@
 
 module Primitive::Keyless::Generator::DRBG where
 
-import Primitive::Symmetric::Cipher::Block::AES
+import Primitive::Symmetric::Cipher::Block::AES256 as AES256
 
-type keylen   = AESKeySize // bits
+type keylen   = AES256::KeySize // bits
 type blocklen = 128 // bits
 type seedlen  = 384 // bits, 384 bits fixed by table 3 for AES-256
 type reseed_limit = 2 ^^ 35 // max number of bytes to generate before reseeding
@@ -19,7 +19,7 @@ type seedsize = 48
 type cipher_ctx = { key : [keylen] }
 
 block_encrypt : [keylen] -> [blocklen] -> [blocklen]
-block_encrypt key data = aesEncrypt(data, key)
+block_encrypt key data = AES256::encrypt key data
 
 type s2n_drbg =
   { bytes_used : [64]
diff --git a/Primitive/Symmetric/Cipher/Authenticated/AES_256_GCM.cry b/Primitive/Symmetric/Cipher/Authenticated/AES_256_GCM.cry
index ceaf333c..58a0818e 100644
--- a/Primitive/Symmetric/Cipher/Authenticated/AES_256_GCM.cry
+++ b/Primitive/Symmetric/Cipher/Authenticated/AES_256_GCM.cry
@@ -1,10 +1,9 @@
 module Primitive::Symmetric::Cipher::Authenticated::AES_256_GCM where
 
-import Primitive::Symmetric::Cipher::Block::AES
-
+import Primitive::Symmetric::Cipher::Block::AES256 as AES256
 
 aes_hw_encrypt : [16][8] -> [32][8] -> [16][8]
-aes_hw_encrypt in key = split (aesEncrypt ((join in), (join key)))
+aes_hw_encrypt in key = split (AES256::encrypt (join key) (join in))
 
 
 gcm_pmult_pmod : [128] -> [128] -> [128]
diff --git a/Primitive/Symmetric/Cipher/Authenticated/AES_GCM.cry b/Primitive/Symmetric/Cipher/Authenticated/AES_GCM.cry
index 3f762fa4..6b6b02de 100644
--- a/Primitive/Symmetric/Cipher/Authenticated/AES_GCM.cry
+++ b/Primitive/Symmetric/Cipher/Authenticated/AES_GCM.cry
@@ -1,5 +1,5 @@
 
-// Cryptol AES GCM test vectors
+// Cryptol instatiation of AES128-GCM and AES256-GCM, and test vectors for each.
 // Copyright (c) 2010-2024, Galois Inc.
 // www.cryptol.net
 // Author: Ajay Kumar Eeralla
@@ -8,43 +8,52 @@
 
 module Primitive::Symmetric::Cipher::Authenticated::AES_GCM where
 import `Primitive::Symmetric::Cipher::Authenticated::GCM
-import Primitive::Symmetric::Cipher::Block::AES_parameterized as AES
+import Primitive::Symmetric::Cipher::Block::AES128 as AES128
+import Primitive::Symmetric::Cipher::Block::AES256 as AES256
+
+AES128_GCM_encrypt = GCM_AE `{K=128} {E=AES128::encrypt}
+AES128_GCM_decrypt = GCM_AD `{K=128} {E=AES128::encrypt}
+
+AES256_GCM_encrypt = GCM_AE `{K=256} {E=AES256::encrypt}
+AES256_GCM_decrypt = GCM_AD `{K=256} {E=AES256::encrypt}
 
 // GCM's symmetry property must hold for AES.
 // The other type parameter sizes are chosen arbitrarily.
 aesGcmIsSymmetric: [128] -> [96] -> [256] -> [0] -> Bool
-property aesGcmIsSymmetric key iv pt aad = gcmIsSymmetric `{T=128} { E=AES::encrypt } key iv pt aad
+property aesGcmIsSymmetric key iv pt aad = gcmIsSymmetric `{T=128} { E=AES128::encrypt } key iv pt aad
 
 // GCM's decryption API equivalence must hold for AES.
 // The other type parameter sizes are chosen arbitrarily.
 aesGcmDecryptionApisAreEquivalent: [128] -> [96] -> [256] -> [128] -> Bool
-property aesGcmDecryptionApisAreEquivalent key iv ct tag = decryptionApisAreEquivalent {E=AES::encrypt} key iv ct [] tag
+property aesGcmDecryptionApisAreEquivalent key iv ct tag = decryptionApisAreEquivalent {E=AES128::encrypt} key iv ct [] tag
 
 // GCM's encryption API equivalence must hold for AES.
 // The other type parameter sizes are chosen arbitrarily.
 aesGcmEncryptionApisAreEquivalent: [128] -> [96] -> [256] -> [128] -> Bool
-property aesGcmEncryptionApisAreEquivalent key iv pt = decryptionApisAreEquivalent {E=AES::encrypt} key iv pt []
+property aesGcmEncryptionApisAreEquivalent key iv pt = decryptionApisAreEquivalent {E=AES128::encrypt} key iv pt []
 
 property AES_GCM_test_vector_0 = ct == expected_ct /\ tag == expected_tag /\ valid_dec
     where
         pt = []
-        (ct, tag) = GCM_AE `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt} zero zero pt []
-        dec = GCM_AD `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt} zero zero ct [] tag
-        expected_ct = []
-        expected_tag = 0x58e2fccefa7e3061367f1d57a4e7455a
+        key = zero : [128]
+        iv = zero : [96]
+        (ct, tag) = AES128_GCM_encrypt key iv pt []
+        dec = AES128_GCM_decrypt key iv ct [] tag
+        expected_ct = [] : [0]
+        expected_tag = 0x58e2fccefa7e3061367f1d57a4e7455a : [128]
         valid_dec = dec.valid && (dec.pt == pt)
 
 property AES_GCM_test_vector_1 =
     ct == expected_ct /\ tag == expected_tag /\ valid_dec
     where
         key = zero
-        iv = zero
+        iv = zero : [96]
         pt = zero
         aad = []
-        expected_ct = 0x0388dace60b6a392f328c2b971b2fe78
+        expected_ct = 0x0388dace60b6a392f328c2b971b2fe78 : [128]
         expected_tag = 0xab6e47d42cec13bdf53a67b21257bddf : [128]
-        (ct, tag) = GCM_AE `{K=128, IV=96} {E=AES::encrypt} key iv pt aad
-        dec = GCM_AD `{K=128, IV=96} {E=AES::encrypt} key iv ct aad tag
+        (ct, tag) = AES128_GCM_encrypt key iv pt aad
+        dec = AES128_GCM_decrypt key iv ct aad tag
         valid_dec = dec.valid && (dec.pt == pt)
 
 property AES_GCM_test_vector_2 =
@@ -56,8 +65,8 @@ property AES_GCM_test_vector_2 =
         aad = []
         expected_ct = 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985
         expected_tag = 0x4d5c2af327cd64a62cf35abd2ba6fab4 : [128]
-        (ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
-        dec = GCM_AD {E=AES::encrypt} key iv ct aad tag
+        (ct, tag) = AES128_GCM_encrypt key iv pt aad
+        dec = AES128_GCM_decrypt key iv ct aad tag
         valid_dec = dec.valid && (dec.pt == pt)
 
 property AES_GCM_test_vector_3 =
@@ -69,8 +78,8 @@ property AES_GCM_test_vector_3 =
         aad = 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2
         expected_ct  = 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091
         expected_tag = 0x5bc94fbc3221a5db94fae95ae7121a47
-        (ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
-        dec = GCM_AD {E=AES::encrypt} key iv ct aad tag
+        (ct, tag) = AES128_GCM_encrypt key iv pt aad
+        dec = AES128_GCM_decrypt key iv ct aad tag
         valid_dec = dec.valid && (dec.pt == pt)
 
 // A test case from aesgcmtest.c
@@ -83,8 +92,8 @@ property AES_GCM_test_vector_4 =
         aad   = 0x4d23c3cec334b49bdb370c437fec78de : [128]
         expected_ct   = 0xf7264413a84c0e7cd536867eb9f21736
         expected_tag  = 0x67ba0510262ae487d737ee6298f77e0c
-        (ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
-        dec = GCM_AD {E=AES::encrypt} key iv ct aad tag
+        (ct, tag) = AES256_GCM_encrypt key iv pt aad
+        dec = AES256_GCM_decrypt key iv ct aad tag
         valid_dec = dec.valid && (dec.pt == pt)
 
 property AES_GCM_invalid_test_vector =
@@ -97,5 +106,5 @@ property AES_GCM_invalid_test_vector =
         expected_ct   = 0xf7264413a84c0e7cd536867eb9f21736
         expected_tag  = 0x67ba0510262ae487d737ee6298f77e0c
         invalid_tag  = 0x67ba0510262ae487d737ee6298f77888
-        (ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
-        dec = GCM_AD {E=AES::encrypt} key iv ct aad invalid_tag
\ No newline at end of file
+        (ct, tag) = AES256_GCM_encrypt key iv pt aad
+        dec = AES256_GCM_decrypt key iv ct aad invalid_tag
\ No newline at end of file
diff --git a/Primitive/Symmetric/Cipher/Authenticated/AES_GCM_SIV.cry b/Primitive/Symmetric/Cipher/Authenticated/AES_GCM_SIV.cry
index dfb09b3c..a7f58016 100644
--- a/Primitive/Symmetric/Cipher/Authenticated/AES_GCM_SIV.cry
+++ b/Primitive/Symmetric/Cipher/Authenticated/AES_GCM_SIV.cry
@@ -14,26 +14,33 @@
 
 module Primitive::Symmetric::Cipher::Authenticated::AES_GCM_SIV where
 
-import Primitive::Symmetric::Cipher::Block::AES_parameterized as AES
-
 parameter
-  /** 0: use AES128, 1: use AES256 */
-  type Mode : #
-  type constraint (1 >= Mode)
+  // This constraint enforces the standard key sizes of 128 and
+  // 256-bits recommended in the draft RFC.
+  type KeySize : #
+  type constraint (fin KeySize, KeySize % 128 == 0, KeySize / 128 >= 1, KeySize / 128 <= 2)
 
   type AAD : #
   type constraint ( (36 + 8) >= width AAD )
 
 
+/** This bit of algebra is here to satisfy the constraint solver.
+ * `K` should be the same as `KeySize`, but the type inference doesn't work
+ * if you set it directly equal.
+ * `Mode` is 0 for AES-128 and 1 for AES-256.
+ */
+type Mode = KeySize / 128 - 1
 type K  = 128 + 128 * Mode
-type KS = AES::EncKey (2 * Mode)
+import Primitive::Symmetric::Cipher::Block::AES_specification as AES where
+  type KeySize' = KeySize
+type KS = AES::EncryptionKey
 
 
 /** Note the weird byte-swapping business (also in `blockify` and `unblockify`)
-It is not quite clear in what format we want the inputs/outputs, but we
-do the swapping so that inputs/ouputs match the test vectors at
-https://tools.ietf.org/html/draft-irtf-cfrg-gcmsiv-06
-*/
+ * It is not quite clear in what format we want the inputs/outputs, but we
+ * do the swapping so that inputs/ouputs match the test vectors at
+ * https://tools.ietf.org/html/draft-irtf-cfrg-gcmsiv-06
+ */
 aes_gcm_siv :
   {n} ((36 + 8) >= width n) =>
       { key   : [K]
@@ -73,7 +80,7 @@ gcm_siv_plus (K1,K2) N AAD MSG = (unblockify Cs,TAG)
   T       = polyvalFrom K1 (A # M # [msg_len # aad_len]) 0
   A       = blockify AAD
   M       = blockify MSG
-  aad_len = `AAD : [64]
+  aad_len = `AAD: [64]
   msg_len = `n   : [64]
 
   _ # tUpper # tLower = TAG
@@ -115,4 +122,3 @@ unblockify xs = take (join [ byteSwap b | b <- xs ])
 // This function changes back and forth.
 byteSwap : {n} (fin n) => [8 * n] -> [8 * n]
 byteSwap xs = join (reverse (split`{each=8} xs))
-
diff --git a/Primitive/Symmetric/Cipher/Authenticated/SIV_rfc5297.md b/Primitive/Symmetric/Cipher/Authenticated/SIV_rfc5297.md
index 28f6bfca..842c8da7 100644
--- a/Primitive/Symmetric/Cipher/Authenticated/SIV_rfc5297.md
+++ b/Primitive/Symmetric/Cipher/Authenticated/SIV_rfc5297.md
@@ -1,9 +1,9 @@
 ```
 module Primitive::Symmetric::Cipher::Authenticated::SIV_rfc5297 where
 
-import Primitive::Symmetric::Cipher::Block::AES
+import Primitive::Symmetric::Cipher::Block::AES128 as AES128
 
-type Key = [AESKeySize]
+type Key = [AES128::KeySize]
 ```
 
 Network Working Group                                         D. Harkins
@@ -307,7 +307,7 @@ bitand a b = a && b
 
 ```
 E : (Key,[128]) -> [128]
-E(K,X) = aesEncrypt (X,K)
+E(K,X) = AES128::encrypt K X
 
 // 1. Apply the subkey generation process in Sec. 6.1 to K to produce K1 and K2.
 // 2. If Mlen = 0, let n = 1; else, let n = ⎡Mlen/b⎤.
diff --git a/Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat b/Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat
index f4c630d5..bd5795c8 100644
--- a/Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat
+++ b/Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat
@@ -20,7 +20,7 @@
 // This property is independent of the type parameters but we have to specify
 // them anyway.
 // It takes more than 25 minutes to `:prove`.
-:check dotAndMultAreEquivalent `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt}
+:check dotAndMultAreEquivalent `{K=128, IV=96, AAD=0, T=128} {E=AES128::encrypt}
 
 // Make sure that decryption is the inverse of encryption
 // This property takes more than 20 minutes to `:prove`.
diff --git a/Primitive/Symmetric/Cipher/Block/AES.cry b/Primitive/Symmetric/Cipher/Block/AES.cry
deleted file mode 100644
index 879fc045..00000000
--- a/Primitive/Symmetric/Cipher/Block/AES.cry
+++ /dev/null
@@ -1,248 +0,0 @@
-// Cryptol AES Implementation
-// Copyright (c) 2010-2018, Galois Inc.
-// www.cryptol.net
-
-// This is a fairly close implementation of the FIPS-197 standard:
-//   http://csrc.nist.gov/publications/fips/fips197/fips-197.pdf
-
-// Nk: Number of blocks in the key
-// Must be one of 4 (AES128), 6 (AES192), or 8 (AES256)
-// Aside from this line, no other code below needs to change for
-// implementing AES128, AES192, or AES256
-module Primitive::Symmetric::Cipher::Block::AES where
-
-import Common::GF28
-
-type AES128 = 4
-type AES192 = 6
-type AES256 = 8
-
-type Nk = AES256
-
-// For Cryptol 2.x | x > 0
-// NkValid: `Nk -> Bit
-// property NkValid k = (k == `AES128) || (k == `AES192) || (k == `AES256)
-
-// Number of blocks and Number of rounds
-type Nb = 4
-type Nr = 6 + Nk
-
-type AESKeySize  = (Nk*32)
-
-// Helper type definitions
-type State       = [4][Nb]GF28
-type RoundKey    = State
-type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey)
-
-// The affine transform and its inverse
-xformByte : GF28 -> GF28
-xformByte b = gf28Add [b, (b >>> 4), (b >>> 5), (b >>> 6), (b >>> 7), c]
-   where c = 0x63
-
-xformByte' : GF28 -> GF28
-xformByte' b = gf28Add [(b >>> 2), (b >>> 5), (b >>> 7), d] where d = 0x05
-// The SubBytes transform and its inverse
-SubByte : GF28 -> GF28
-SubByte b = xformByte (gf28Inverse b)
-
-SubByte' : GF28 -> GF28
-SubByte' b = sbox@b
-
-SubBytes : State -> State
-SubBytes state = [ [ SubByte' b | b <- row ] | row <- state ]
-
-
-InvSubByte : GF28 -> GF28
-InvSubByte b = gf28Inverse (xformByte' b)
-
-InvSubBytes : State -> State
-InvSubBytes state = [ [ InvSubByte b | b <- row ] | row <- state ]
-
-// The ShiftRows transform and its inverse
-ShiftRows : State -> State
-ShiftRows state = [ row <<< shiftAmount | row <- state
-                                        | shiftAmount <- [0 .. 3]
-                  ]
-
-InvShiftRows : State -> State
-InvShiftRows state = [ row >>> shiftAmount | row <- state
-                                           | shiftAmount <- [0 .. 3]
-                     ]
-
-// The MixColumns transform and its inverse
-MixColumns : State -> State
-MixColumns state = gf28MatrixMult m state
-    where m = [[2, 3, 1, 1],
-               [1, 2, 3, 1],
-               [1, 1, 2, 3],
-               [3, 1, 1, 2]]
-
-InvMixColumns : State -> State
-InvMixColumns state = gf28MatrixMult m state
-    where m = [[0x0e, 0x0b, 0x0d, 0x09],
-               [0x09, 0x0e, 0x0b, 0x0d],
-               [0x0d, 0x09, 0x0e, 0x0b],
-               [0x0b, 0x0d, 0x09, 0x0e]]
-
-// The AddRoundKey transform
-AddRoundKey : (RoundKey, State) -> State
-AddRoundKey (rk, s) = rk ^ s
-// Key expansion
-Rcon : [8] -> [4]GF28
-Rcon i = [ gf28Pow (<| x |>) (i-1), 0, 0, 0 ]
-
-SubWord : [4]GF28 -> [4]GF28
-SubWord bs = [ SubByte' b | b <- bs ]
-
-RotWord : [4]GF28 -> [4]GF28
-RotWord [a0, a1, a2, a3] = [a1, a2, a3, a0]
-
-NextWord : ([8],[4][8],[4][8]) -> [4][8]
-NextWord(i, prev, old) = old ^ mask
-   where mask = if i % `Nk == 0
-                then SubWord(RotWord(prev)) ^ Rcon (i / `Nk)
-                else if (`Nk > 6) /\ (i % `Nk == 4)
-                     then SubWord(prev)
-                     else prev
-
-
-ExpandKeyForever : [Nk][4][8] -> [inf]RoundKey
-ExpandKeyForever seed = [ transpose g | g <- groupBy`{4} (keyWS seed) ]
-
-keyWS : [Nk][4][8] -> [inf][4][8]
-keyWS seed    = xs
-     where xs = seed # [ NextWord(i, prev, old)
-                       | i    <- [ `Nk ... ]
-                       | prev <- drop`{Nk-1} xs
-                       | old  <- xs
-                       ]
-
-ExpandKey : [AESKeySize] -> KeySchedule
-ExpandKey key = (keys @ 0, keys @@ [1 .. (Nr - 1)], keys @ `Nr)
-  where   seed : [Nk][4][8]
-          seed = split (split key)
-          keys = ExpandKeyForever seed
-
-fromKS : KeySchedule -> [Nr+1][4][32]
-fromKS (f, ms, l) = [ formKeyWords (transpose k) | k <- [f] # ms # [l] ]
-    where formKeyWords bbs = [ join bs | bs <- bbs ]
-
-// AES rounds and inverses
-AESRound : (RoundKey, State) -> State
-AESRound (rk, s) = AddRoundKey (rk, MixColumns (ShiftRows (SubBytes s)))
-
-AESFinalRound : (RoundKey, State) -> State
-AESFinalRound (rk, s) = AddRoundKey (rk, ShiftRows (SubBytes s))
-
-AESInvRound : (RoundKey, State) -> State
-AESInvRound (rk, s) =
-      InvMixColumns (AddRoundKey (rk, InvSubBytes (InvShiftRows s)))
-AESFinalInvRound : (RoundKey, State) -> State
-AESFinalInvRound (rk, s) = AddRoundKey (rk, InvSubBytes (InvShiftRows s))
-
-// Converting a 128 bit message to a State and back
-msgToState : [128] -> State
-msgToState msg = transpose (split (split msg))
-
-stateToMsg : State -> [128]
-stateToMsg st = join (join (transpose st))
-
-// AES Encryption
-aesEncrypt : ([128], [AESKeySize]) -> [128]
-aesEncrypt (pt, key) = aesEncryptWithKeySchedule pt (ExpandKey key)
-
-aesEncryptWithKeySchedule : [128] -> KeySchedule -> [128]
-aesEncryptWithKeySchedule pt (kInit, ks, kFinal) = stateToMsg (AESFinalRound (kFinal, rounds ! 0))
-  where
-    state0 = AddRoundKey(kInit, msgToState pt)
-    rounds = [state0] # [ AESRound (rk, s) | rk <- ks | s <- rounds ]
-
-// AES Decryption
-aesDecrypt : ([128], [AESKeySize]) -> [128]
-aesDecrypt (ct, key) = stateToMsg (AESFinalInvRound (kFinal, rounds ! 0))
-  where   (kFinal, ks, kInit) = ExpandKey key
-          state0 = AddRoundKey(kInit, msgToState ct)
-          rounds = [state0] # [ AESInvRound (rk, s)
-                              | rk <- reverse ks
-                              | s  <- rounds
-                              ]
-
-sbox : [256]GF28
-sbox = [
- 0x63, 0x7c, 0x77, 0x7b, 0xf2, 0x6b, 0x6f, 0xc5, 0x30, 0x01, 0x67,
- 0x2b, 0xfe, 0xd7, 0xab, 0x76, 0xca, 0x82, 0xc9, 0x7d, 0xfa, 0x59,
- 0x47, 0xf0, 0xad, 0xd4, 0xa2, 0xaf, 0x9c, 0xa4, 0x72, 0xc0, 0xb7,
- 0xfd, 0x93, 0x26, 0x36, 0x3f, 0xf7, 0xcc, 0x34, 0xa5, 0xe5, 0xf1,
- 0x71, 0xd8, 0x31, 0x15, 0x04, 0xc7, 0x23, 0xc3, 0x18, 0x96, 0x05,
- 0x9a, 0x07, 0x12, 0x80, 0xe2, 0xeb, 0x27, 0xb2, 0x75, 0x09, 0x83,
- 0x2c, 0x1a, 0x1b, 0x6e, 0x5a, 0xa0, 0x52, 0x3b, 0xd6, 0xb3, 0x29,
- 0xe3, 0x2f, 0x84, 0x53, 0xd1, 0x00, 0xed, 0x20, 0xfc, 0xb1, 0x5b,
- 0x6a, 0xcb, 0xbe, 0x39, 0x4a, 0x4c, 0x58, 0xcf, 0xd0, 0xef, 0xaa,
- 0xfb, 0x43, 0x4d, 0x33, 0x85, 0x45, 0xf9, 0x02, 0x7f, 0x50, 0x3c,
- 0x9f, 0xa8, 0x51, 0xa3, 0x40, 0x8f, 0x92, 0x9d, 0x38, 0xf5, 0xbc,
- 0xb6, 0xda, 0x21, 0x10, 0xff, 0xf3, 0xd2, 0xcd, 0x0c, 0x13, 0xec,
- 0x5f, 0x97, 0x44, 0x17, 0xc4, 0xa7, 0x7e, 0x3d, 0x64, 0x5d, 0x19,
- 0x73, 0x60, 0x81, 0x4f, 0xdc, 0x22, 0x2a, 0x90, 0x88, 0x46, 0xee,
- 0xb8, 0x14, 0xde, 0x5e, 0x0b, 0xdb, 0xe0, 0x32, 0x3a, 0x0a, 0x49,
- 0x06, 0x24, 0x5c, 0xc2, 0xd3, 0xac, 0x62, 0x91, 0x95, 0xe4, 0x79,
- 0xe7, 0xc8, 0x37, 0x6d, 0x8d, 0xd5, 0x4e, 0xa9, 0x6c, 0x56, 0xf4,
- 0xea, 0x65, 0x7a, 0xae, 0x08, 0xba, 0x78, 0x25, 0x2e, 0x1c, 0xa6,
- 0xb4, 0xc6, 0xe8, 0xdd, 0x74, 0x1f, 0x4b, 0xbd, 0x8b, 0x8a, 0x70,
- 0x3e, 0xb5, 0x66, 0x48, 0x03, 0xf6, 0x0e, 0x61, 0x35, 0x57, 0xb9,
- 0x86, 0xc1, 0x1d, 0x9e, 0xe1, 0xf8, 0x98, 0x11, 0x69, 0xd9, 0x8e,
- 0x94, 0x9b, 0x1e, 0x87, 0xe9, 0xce, 0x55, 0x28, 0xdf, 0x8c, 0xa1,
- 0x89, 0x0d, 0xbf, 0xe6, 0x42, 0x68, 0x41, 0x99, 0x2d, 0x0f, 0xb0,
- 0x54, 0xbb, 0x16]
-
-// Test runs:
-
-// cryptol> aesEncrypt (0x3243f6a8885a308d313198a2e0370734,   \
-//                      0x2b7e151628aed2a6abf7158809cf4f3c)
-// 0x3925841d02dc09fbdc118597196a0b32
-// cryptol> aesEncrypt (0x00112233445566778899aabbccddeeff,   \
-//                      0x000102030405060708090a0b0c0d0e0f)
-// 0x69c4e0d86a7b0430d8cdb78070b4c55a
-property AESCorrect msg key = aesDecrypt (aesEncrypt (msg, key), key) == msg
-
-testmsgs = [0x6bc1bee22e409f96e93d7e117393172a
-           ,0xae2d8a571e03ac9c9eb76fac45af8e51
-           ,0x30c81c46a35ce411e5fbc1191a0a52ef
-           ,0xf69f2445df4f9b17ad2b417be66c3710]
-
-
-// AES128 tests
-
-// testkey128 = 0x2b7e151628aed2a6abf7158809cf4f3c
-
-// testct128 = [0x3ad77bb40d7a3660a89ecaf32466ef97
-//             ,0xf5d3d58503b9699de785895a96fdbaaf
-//             ,0x43b1cd7f598ece23881b00e3ed030688
-//             ,0x7b0c785e27e8ad3f8223207104725dd4]
-
-// property testsPass = and [ aesEncrypt (msg, testkey128) == ct
-//                          | msg <- testmsgs | ct <- testct128 ]
-
-
-// AES192 tests
-
-// testkey192 = 0x8e73b0f7da0e6452c810f32b809079e562f8ead2522c6b7b
-
-// testct192 = [0xbd334f1d6e45f25ff712a214571fa5cc
-//             ,0x974104846d0ad3ad7734ecb3ecee4eef
-//             ,0xef7afd2270e2e60adce0ba2face6444e
-//             ,0x9a4b41ba738d6c72fb16691603c18e0e]
-
-// property testsPass = and [ aesEncrypt (msg, testkey192) == ct
-//                          | msg <- testmsgs | ct <- testct192 ]
-
-
-// AES256 tests
-
-testkey256 = 0x603deb1015ca71be2b73aef0857d77811f352c073b6108d72d9810a30914dff4
-testct256 = [0xf3eed1bdb5d2a03c064b5a7e3db181f8
-            ,0x591ccb10d410ed26dc5ba74a31362870
-            ,0xb6ed21b99ca6f4f9f153e7b1beafed1d
-            ,0x23304b7a39f9f3ff067d8d8f9e24ecc7]
-
-property testsPass = and [ aesEncrypt (msg, testkey256) == ct
-                         | msg <- testmsgs | ct <- testct256 ]
diff --git a/Primitive/Symmetric/Cipher/Block/AES128.cry b/Primitive/Symmetric/Cipher/Block/AES128.cry
new file mode 100644
index 00000000..acf36e04
--- /dev/null
+++ b/Primitive/Symmetric/Cipher/Block/AES128.cry
@@ -0,0 +1,4 @@
+module Primitive::Symmetric::Cipher::Block::AES128 =
+    Primitive::Symmetric::Cipher::Block::AES_specification where
+    // This produces a key size of 128
+    type KeySize' = 128
diff --git a/Primitive/Symmetric/Cipher/Block/AES192.cry b/Primitive/Symmetric/Cipher/Block/AES192.cry
new file mode 100644
index 00000000..4fed395e
--- /dev/null
+++ b/Primitive/Symmetric/Cipher/Block/AES192.cry
@@ -0,0 +1,4 @@
+module Primitive::Symmetric::Cipher::Block::AES192 =
+    Primitive::Symmetric::Cipher::Block::AES_specification where
+    // This produces a key size of 192
+    type KeySize' = 192
diff --git a/Primitive/Symmetric/Cipher/Block/AES256.cry b/Primitive/Symmetric/Cipher/Block/AES256.cry
new file mode 100644
index 00000000..d08ff9f4
--- /dev/null
+++ b/Primitive/Symmetric/Cipher/Block/AES256.cry
@@ -0,0 +1,4 @@
+module Primitive::Symmetric::Cipher::Block::AES256 =
+    Primitive::Symmetric::Cipher::Block::AES_specification where
+    // This produces a key size of 256
+    type KeySize' = 256
diff --git a/Primitive/Symmetric/Cipher/Block/AESKeyWrap.cry b/Primitive/Symmetric/Cipher/Block/AESKeyWrap.cry
index 2652af3a..686df8e3 100644
--- a/Primitive/Symmetric/Cipher/Block/AESKeyWrap.cry
+++ b/Primitive/Symmetric/Cipher/Block/AESKeyWrap.cry
@@ -8,9 +8,15 @@
 // shifting and the other using indexing.  This specification closely matches
 // the index-based algorithm description as that description is more similar
 // to the BoringSSL AES Key Wrap implementation.
+//
+// One important deviation: this is currently instantiated only for AES256;
+// the RFC supports all three standardized AES key sizes.
+//
 
 module Primitive::Symmetric::Cipher::Block::AESKeyWrap where
-import Primitive::Symmetric::Cipher::Block::AES
+import Primitive::Symmetric::Cipher::Block::AES256 as AES256
+
+type AESKeySize = AES256::KeySize
 
 // Default intial value (Section 2.2.3)
 DefaultIV : [8][8]
@@ -77,7 +83,7 @@ private
   wrapBlock : {n} (fin n, width n <= 64) =>
               [AESKeySize] -> ([64], [n][64]) -> [64] -> [64] -> ([64], [n][64])
   wrapBlock key (A, R) j i = (A', R')
-    where B  = aesEncrypt (A # (R @ (i-1)), key)
+    where B  = AES256::encrypt key (A # (R @ (i-1)))
           A' = (take`{64} B) ^ (((`n : [64]) * j) + i)
           R' = update R (i-1) (drop`{64} B)
 
@@ -85,7 +91,7 @@ private
   unwrapBlock : {n} (fin n, width n <= 64) =>
                 [AESKeySize] -> ([64], [n][64]) -> [64] -> [64] -> ([64], [n][64])
   unwrapBlock key (A, R) j i = (A', R')
-    where B  = aesDecrypt ((A ^ (((`n : [64]) * j) + i)) # (R @ (i-1)), key)
+    where B  = AES256::decrypt key ((A ^ (((`n : [64]) * j) + i)) # (R @ (i-1)))
           A' = take`{64} B
           R' = update R (i-1) (drop`{64} B)
 
diff --git a/Primitive/Symmetric/Cipher/Block/AESKeyWrapPadded.cry b/Primitive/Symmetric/Cipher/Block/AESKeyWrapPadded.cry
index 47bfce76..ca36e709 100644
--- a/Primitive/Symmetric/Cipher/Block/AESKeyWrapPadded.cry
+++ b/Primitive/Symmetric/Cipher/Block/AESKeyWrapPadded.cry
@@ -4,11 +4,16 @@
 
 // This is a close implementation of RFC 5649:
 // https://tools.ietf.org/html/rfc5649
+//
+// One important deviation: this is currently instantiated only for AES256;
+// the RFC supports all three standardized AES key sizes.
 
 module Primitive::Symmetric::Cipher::Block::AESKeyWrapPadded where
-import Primitive::Symmetric::Cipher::Block::AES
+import Primitive::Symmetric::Cipher::Block::AES256 as AES256
 import Primitive::Symmetric::Cipher::Block::AESKeyWrap
 
+type AESKeySize = AES256::KeySize
+
 // Most significant bits of alternate initial value (Section 3)
 AlternativeIV : [4][8]
 AlternativeIV = [0xA6, 0x59, 0x59, 0xA6]
@@ -27,7 +32,7 @@ aesWrapKeyPadded key iv plaintext =
   // If padded plaintext is 8 bytes, encrypt in AEC ECB mode.  The `drop` and
   // append of `zero` have no effect at runtime and exist to make the types
   // work out, as the type checker cannot deduce that `n <= 8` in this branch.
-  then (split (aesEncrypt (drop (join (AIV # P)), key))) # zero
+  then (split (AES256::encrypt key (drop (join (AIV # P))))) # zero
   // Otherwise perform standard key wrap algorithm on padded plaintext.  The
   // `drop` and append of `zero` have runtime effect and exist to make the
   // types work out, as the type checker cannot deduce that `n >= 16` in this
@@ -60,7 +65,7 @@ aesUnwrapKeyPadded key iv ciphertext = if valid
         // and append of `zero` have no effect at runtime and exist to make the
         // types work out, as the type checker cannot deduce that `n == 16` in
         // this branch.
-        then (split (aesDecrypt (drop (join ciphertext), key))) # zero
+        then (split (AES256::decrypt key (drop (join ciphertext)))) # zero
         // Otherwise perform the standard key unwrap algorithm.  The `drop`
         // and append of `zero` have no effect at runtime and exist to make the
         // types work out, as the type checker cannot deduce that `n >= 24` in
diff --git a/Primitive/Symmetric/Cipher/Block/AES_parameterized.cry b/Primitive/Symmetric/Cipher/Block/AES_parameterized.cry
deleted file mode 100644
index 00e8e557..00000000
--- a/Primitive/Symmetric/Cipher/Block/AES_parameterized.cry
+++ /dev/null
@@ -1,43 +0,0 @@
-/*
-   Copyright (c) 2018 Galois, Inc.
-   www.cryptol.net
-*/
-
-module Primitive::Symmetric::Cipher::Block::AES_parameterized where
-
-import `Primitive::Symmetric::Cipher::Block::AES::Algorithm as AES
-import `Primitive::Symmetric::Cipher::Block::AES::ExpandKey
-import Primitive::Symmetric::Cipher::Block::AES::TBox
-
-type constraint ValidKey k m = (k == 128 + m * 64, 2 >= m)
-
-type EncKey m = AES::KeySchedule m
-type DecKey m = AES::KeySchedule m
-
-
-encrypt : {k,m} ValidKey k m => [k] -> [128] -> [128]
-encrypt k = encryptWithSchedule (expandKeyEnc k)
-
-decrypt : {k,m} ValidKey k m => [k] -> [128] -> [128]
-decrypt k = decryptWithSchedule (expandKeyDec k)
-
-
-expandKeyEnc : {k,m} ValidKey k m => [k] -> EncKey m
-expandKeyEnc = expandKey`{Nk = AES::Nk m, Nr = AES::Nr m}
-
-encryptWithSchedule : {k,m} ValidKey k m => EncKey m -> [128] -> [128]
-encryptWithSchedule = AES::encrypt params
-
-
-
-expandKeyDec : {k,m} ValidKey k m => [k] -> EncKey m
-expandKeyDec k = makeDecKey (expandKey`{Nk = AES::Nk m, Nr = AES::Nr m} k)
-
-decryptWithSchedule : {k,m} ValidKey k m => DecKey m -> [128] -> [128]
-decryptWithSchedule = AES::decrypt params
-
-
-params = { encRound = AESRound, decRound = AESInvRound }
-
-property test k pt = decrypt k (encrypt k pt) == pt
-
diff --git a/Primitive/Symmetric/Cipher/Block/AES_specification.cry b/Primitive/Symmetric/Cipher/Block/AES_specification.cry
new file mode 100644
index 00000000..77f90641
--- /dev/null
+++ b/Primitive/Symmetric/Cipher/Block/AES_specification.cry
@@ -0,0 +1,64 @@
+/*
+   Copyright (c) 2018 Galois, Inc.
+   www.cryptol.net
+
+   This provides the basic AES block cipher, abstracted over the key length.
+
+   It operates over 128-bit blocks. To use AES with any practical application,
+   use it with a mode of operation, like CTR or GCM-SIV.
+*/
+
+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
+   // 256-bits [FIPS-PUB-197 Sections 1, 5, and 6.1].
+   type KeySize' : #
+   type constraint (fin KeySize', KeySize' % 64 == 0, KeySize' / 64 >= 2, KeySize' / 64 <= 4)
+
+// The AES implementation uses the `Mode` type to compute other parameters.
+// The mode corresponds directly to the key size:
+// Mode 0 = 128 bits; Mode 1 = 192 bits; Mode 2 = 256 bits
+type Mode = (KeySize / 64) - 2
+
+// Make KeySize accessible outside the module.
+type KeySize = KeySize'
+
+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 k = encryptWithSchedule (expandKeyEnc k)
+
+decrypt : [KeySize] -> [128] -> [128]
+decrypt k = decryptWithSchedule (expandKeyDec k)
+
+expandKeyEnc : [KeySize] -> EncryptionKey
+expandKeyEnc = expandKey`{Nk = AES::Nk Mode, Nr = AES::Nr Mode}
+
+encryptWithSchedule : EncryptionKey -> [128] -> [128]
+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 = AES::decrypt params
+
+params = { encRound = AESRound, decRound = AESInvRound }
+
+// This property should be true; it's not provable as-is because it's not monomorphic.
+// It should be instantiated separately for each key size.
+property aesIsCorrect k pt = decrypt k (encrypt k pt) == pt
+
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/AES128_CBC.cry b/Primitive/Symmetric/Cipher/Block/Modes/AES128_CBC.cry
new file mode 100644
index 00000000..6ecdec2e
--- /dev/null
+++ b/Primitive/Symmetric/Cipher/Block/Modes/AES128_CBC.cry
@@ -0,0 +1,53 @@
+// Cryptol AES CBC test vectors
+// Copyright (c) 2010-2018, Galois Inc.
+// www.cryptol.net
+// Author: Ajay Kumar Eeralla
+
+module Primitive::Symmetric::Cipher::Block::Modes::AES128_CBC where
+import Primitive::Symmetric::Cipher::Block::Modes::CBC
+import Primitive::Symmetric::Cipher::Block::AES128 as AES128
+
+AES128_CBC_encrypt: {n} (fin n) => [AES128::KeySize] -> iv -> [n]block -> [n]block
+AES128_CBC_encrypt = cbcEnc AES128::encrypt
+
+AES128_CBC_decrypt: {n} (fin n) => [AES128::KeySize] -> iv -> [n]block -> [n]block
+AES128_CBC_decrypt = cbcDec AES128::decrypt
+// Test vectors from https://tools.ietf.org/html/rfc3602
+
+// No. of blocks := 1
+property testEncCbcPassB1 = and [ (AES128_CBC_encrypt k iv ps) == cs
+                                | k <- testKey | iv <- testIv | ps <- testPt | cs <- testCt ]
+    where
+        testKey = [0x06a9214036b8a15b512e03d534120006]
+        testIv = [0x3dafba429d9eb430b422da802c9fac41]
+        testPt = [[join "Single block msg"]]
+        testCt = [[0xe353779c1079aeb82708942dbe77181a]]
+
+
+// No. of blocks := 2
+property testEncCbcPassB2 = and [ (AES128_CBC_encrypt k iv ps) == cs
+                                | k <- testKey2 | iv <- testIv2 | ps <- testPt2 | cs <- testCt2 ]
+    where
+        testKey2 = [0xc286696d887c9aa0611bbb3e2025a45a]
+        testIv2 = [0x562e17996d093d28ddb3ba695a2e6f58]
+        testPt2 = [[0x000102030405060708090a0b0c0d0e0f, 0x101112131415161718191a1b1c1d1e1f]]
+        testCt2 = [[0xd296cd94c2cccf8a3a863028b5e1dc0a, 0x7586602d253cfff91b8266bea6d61ab1]]
+
+
+// No. of blocks := 3
+property testEncCbcPassB3 = and [ (AES128_CBC_encrypt k iv ps) == cs
+                                | k <- testKey3 | iv <- testIv3 | ps <- testPt3 | cs <- testCt3 ]
+    where
+        testKey3 = [0x6c3ea0477630ce21a2ce334aa746c2cd]
+        testIv3 = [0xc782dc4c098c66cbd9cd27d825682c81]
+        testPt3 = [[0x5468697320697320612034382d627974, 0x65206d65737361676520286578616374, 0x6c7920332041455320626c6f636b7329]]
+        testCt3 = [[0xd0a02b3836451753d493665d33f0e886, 0x2dea54cdb293abc7506939276772f8d5, 0x021c19216bad525c8579695d83ba2684]]
+
+// No. of blocks := 4
+property testEncCbcPassB4 = and [ (AES128_CBC_encrypt k iv ps) == cs
+                                | k <- testKey4 | iv <- testIv4 | ps <- testPt4 | cs <- testCt4 ]
+    where
+        testKey4 = [0x56e47a38c5598974bc46903dba290349]
+        testIv4 = [0x8ce82eefbea0da3c44699ed7db51b7d9]
+        testPt4 = [[0xa0a1a2a3a4a5a6a7a8a9aaabacadaeaf, 0xb0b1b2b3b4b5b6b7b8b9babbbcbdbebf, 0xc0c1c2c3c4c5c6c7c8c9cacbcccdcecf, 0xd0d1d2d3d4d5d6d7d8d9dadbdcdddedf]]
+        testCt4 = [[0xc30e32ffedc0774e6aff6af0869f71aa, 0x0f3af07a9a31a9c684db207eb0ef8e4e, 0x35907aa632c3ffdf868bb7b29d3d46ad, 0x83ce9f9a102ee99d49a53e87f4c3da55]]
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/AES128_CFB.cry b/Primitive/Symmetric/Cipher/Block/Modes/AES128_CFB.cry
new file mode 100644
index 00000000..76ca1f4e
--- /dev/null
+++ b/Primitive/Symmetric/Cipher/Block/Modes/AES128_CFB.cry
@@ -0,0 +1,37 @@
+// Cryptol AES CFB test vectors
+// Copyright (c) 2010-2018, Galois Inc.
+// www.cryptol.net
+// You can freely use this source code for educational purposes.
+// Author: Ajay Kumar Eeralla
+
+module Primitive::Symmetric::Cipher::Block::Modes::AES128_CFB where
+import Primitive::Symmetric::Cipher::Block::Modes::CFB
+import Primitive::Symmetric::Cipher::Block::AES128 as AES128
+
+AES128_CFB_encrypt: {n} (fin n) => [AES128::KeySize] -> iv -> [n]block -> [n]block
+AES128_CFB_encrypt = cfbEnc AES128::encrypt
+
+AES128_CFB_decrypt: {n} (fin n) => [AES128::KeySize] -> iv -> [n]block -> [n]block
+AES128_CFB_decrypt = cfbDec AES128::decrypt
+
+// Test vectors from https://nvlpubs.nist.gov/nistpubs/Legacy/SP/nistspecialpublication800-38a.pdf
+// No. of blocks := 1
+property testEncCfbPassB1 = and [ (AES128_CFB_encrypt k iv ps) == cs
+                                | k <- testKey | iv <- testIv | ps <- testPt | cs <- testCt ]
+    where
+        testKey = [0x2b7e151628aed2a6abf7158809cf4f3c]
+        testIv = [0x000102030405060708090a0b0c0d0e0f]
+        testPt = [[0x6bc1bee22e409f96e93d7e117393172a]]
+        testCt = [[0x3b3fd92eb72dad20333449f8e83cfb4a]]
+
+
+// No. of blocks := 2
+property testEncCfbPassB2 = and [ (AES128_CFB_encrypt k iv ps) == cs
+                                | k <- testKey2 | iv <- testIv2 | ps <- testPt2 | cs <- testCt2 ]
+    where
+        testKey2 = [0x2b7e151628aed2a6abf7158809cf4f3c]
+        testIv2 = [0x000102030405060708090a0b0c0d0e0f]
+        testPt2 = [[0x6bc1bee22e409f96e93d7e117393172a, 0xae2d8a571e03ac9c9eb76fac45af8e51, 0x30c81c46a35ce411e5fbc1191a0a52ef, 0xf69f2445df4f9b17ad2b417be66c3710]]
+        testCt2 = [[0x3b3fd92eb72dad20333449f8e83cfb4a, 0xc8a64537a0b3a93fcde3cdad9f1ce58b, 0x26751f67a3cbb140b1808cf187a4f4df, 0xc04b05357c5d1c0eeac4c66f9ff7f2e6]]
+
+
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/AES128_CTR.cry b/Primitive/Symmetric/Cipher/Block/Modes/AES128_CTR.cry
new file mode 100644
index 00000000..167f82fb
--- /dev/null
+++ b/Primitive/Symmetric/Cipher/Block/Modes/AES128_CTR.cry
@@ -0,0 +1,23 @@
+// Cryptol AES CTR test vectors
+// Copyright (c) 2010-2018, Galois Inc.
+// www.cryptol.net
+// Author: Ajay Kumar Eeralla
+// Test vector from https://nvlpubs.nist.gov/nistpubs/Legacy/SP nistspecialpublication800-38a.pdf
+
+module Primitive::Symmetric::Cipher::Block::Modes::AES128_CTR where
+import Primitive::Symmetric::Cipher::Block::Modes::CTR
+import Primitive::Symmetric::Cipher::Block::AES128 as AES128
+
+AES128_CTR_encrypt: {n} (fin n) => [AES128::KeySize] -> ic -> [n]block -> [n]block
+AES128_CTR_encrypt = ctrEnc AES128::encrypt
+
+AES128_CTR_decrypt: {n} (fin n) => [AES128::KeySize] -> ic -> [n]block -> [n]block
+AES128_CTR_decrypt = ctrDec AES128::decrypt
+
+// This `:prove`s quickly!
+property aes128_ctr_enc_test_vector_passes = (AES128_CTR_encrypt k ic plaintext) == ciphertext
+    where
+    k = 0x2b7e151628aed2a6abf7158809cf4f3c
+    ic = 0xf0f1f2f3f4f5f6f7f8f9fafbfcfdfeff
+    plaintext = [0x6bc1bee22e409f96e93d7e117393172a, 0xae2d8a571e03ac9c9eb76fac45af8e51, 0x30c81c46a35ce411e5fbc1191a0a52ef, 0xf69f2445df4f9b17ad2b417be66c3710]
+    ciphertext = [0x874d6191b620e3261bef6864990db6ce, 0x9806f66b7970fdff8617187bb9fffdff, 0x5ae4df3edbd5d35e5b4f09020db03eab, 0x1e031dda2fbe03d1792170a0f3009cee]
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/AES_CBC.cry b/Primitive/Symmetric/Cipher/Block/Modes/AES_CBC.cry
deleted file mode 100644
index 6c08af7f..00000000
--- a/Primitive/Symmetric/Cipher/Block/Modes/AES_CBC.cry
+++ /dev/null
@@ -1,53 +0,0 @@
-// Cryptol AES CBC test vectors
-// Copyright (c) 2010-2018, Galois Inc.
-// www.cryptol.net
-// Author: Ajay Kumar Eeralla
-
-module Primitive::Symmetric::Cipher::Block::Modes::AES_CBC where
-import Primitive::Symmetric::Cipher::Block::Modes::CBC
-import Primitive::Symmetric::Cipher::Block::AES_parameterized
-
-property cbcEncCorrect encrypt k c ps = (cbcDec encrypt k c (cbcEnc encrypt k c ps)) == ps
-
-// Test vectors from https://tools.ietf.org/html/rfc3602
-
-// No. of blocks := 1
-
-testKey = [0x06a9214036b8a15b512e03d534120006]
-testIv = [0x3dafba429d9eb430b422da802c9fac41]
-testPt = [[join "Single block msg"]]
-testCt = [[0xe353779c1079aeb82708942dbe77181a]]
-
-property testEncCbcPassB1 = and [ (cbcEnc encrypt k iv ps) == cs
-                                | k <- testKey | iv <- testIv | ps <- testPt | cs <- testCt ]
-
-// No. of blocks := 2
-
-testKey2 = [0xc286696d887c9aa0611bbb3e2025a45a]
-testIv2 = [0x562e17996d093d28ddb3ba695a2e6f58]
-testPt2 = [[0x000102030405060708090a0b0c0d0e0f, 0x101112131415161718191a1b1c1d1e1f]]
-testCt2 = [[0xd296cd94c2cccf8a3a863028b5e1dc0a, 0x7586602d253cfff91b8266bea6d61ab1]]
-
-property testEncCbcPassB2 = and [ (cbcEnc encrypt k iv ps) == cs
-                                | k <- testKey2 | iv <- testIv2 | ps <- testPt2 | cs <- testCt2 ]
-                                
-
-// No. of blocks := 3
-
-testKey3 = [0x6c3ea0477630ce21a2ce334aa746c2cd]
-testIv3 = [0xc782dc4c098c66cbd9cd27d825682c81]
-testPt3 = [[0x5468697320697320612034382d627974, 0x65206d65737361676520286578616374, 0x6c7920332041455320626c6f636b7329]]
-testCt3 = [[0xd0a02b3836451753d493665d33f0e886, 0x2dea54cdb293abc7506939276772f8d5, 0x021c19216bad525c8579695d83ba2684]]
-
-property testEncCbcPassB3 = and [ (cbcEnc encrypt k iv ps) == cs
-                                | k <- testKey3 | iv <- testIv3 | ps <- testPt3 | cs <- testCt3 ]
-
-// No. of blocks := 4
-
-testKey4 = [0x56e47a38c5598974bc46903dba290349]
-testIv4 = [0x8ce82eefbea0da3c44699ed7db51b7d9]
-testPt4 = [[0xa0a1a2a3a4a5a6a7a8a9aaabacadaeaf, 0xb0b1b2b3b4b5b6b7b8b9babbbcbdbebf, 0xc0c1c2c3c4c5c6c7c8c9cacbcccdcecf, 0xd0d1d2d3d4d5d6d7d8d9dadbdcdddedf]]
-testCt4 = [[0xc30e32ffedc0774e6aff6af0869f71aa, 0x0f3af07a9a31a9c684db207eb0ef8e4e, 0x35907aa632c3ffdf868bb7b29d3d46ad, 0x83ce9f9a102ee99d49a53e87f4c3da55]]
-
-property testEncCbcPassB4 = and [ (cbcEnc encrypt k iv ps) == cs
-                                | k <- testKey4 | iv <- testIv4 | ps <- testPt4 | cs <- testCt4 ]
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/AES_CFB.cry b/Primitive/Symmetric/Cipher/Block/Modes/AES_CFB.cry
deleted file mode 100644
index 67899af8..00000000
--- a/Primitive/Symmetric/Cipher/Block/Modes/AES_CFB.cry
+++ /dev/null
@@ -1,33 +0,0 @@
-// Cryptol AES CFB test vectors
-// Copyright (c) 2010-2018, Galois Inc.
-// www.cryptol.net
-// You can freely use this source code for educational purposes.
-// Author: Ajay Kumar Eeralla
-
-module Primitive::Symmetric::Cipher::Block::Modes::AES_CFB where
-import Primitive::Symmetric::Cipher::Block::Modes::CFB
-import Primitive::Symmetric::Cipher::Block::AES_parameterized
-
-property cfbEncCorrect encrypt k c ps = (cfbDec encrypt k c (cfbEnc encrypt k c ps)) == ps
-
-// Test vectors from https://nvlpubs.nist.gov/nistpubs/Legacy/SP/nistspecialpublication800-38a.pdf
-// No. of blocks := 1
-
-testKey = [0x2b7e151628aed2a6abf7158809cf4f3c]
-testIv = [0x000102030405060708090a0b0c0d0e0f]
-testPt = [[0x6bc1bee22e409f96e93d7e117393172a]]
-testCt = [[0x3b3fd92eb72dad20333449f8e83cfb4a]]
-
-property testEncCfbPassB1 = and [ (cfbEnc encrypt k iv ps) == cs
-                                | k <- testKey | iv <- testIv | ps <- testPt | cs <- testCt ]
-
-// No. of blocks := 2
-
-testKey2 = [0x2b7e151628aed2a6abf7158809cf4f3c]
-testIv2 = [0x000102030405060708090a0b0c0d0e0f]
-testPt2 = [[0x6bc1bee22e409f96e93d7e117393172a, 0xae2d8a571e03ac9c9eb76fac45af8e51, 0x30c81c46a35ce411e5fbc1191a0a52ef, 0xf69f2445df4f9b17ad2b417be66c3710]]
-testCt2 = [[0x3b3fd92eb72dad20333449f8e83cfb4a, 0xc8a64537a0b3a93fcde3cdad9f1ce58b, 0x26751f67a3cbb140b1808cf187a4f4df, 0xc04b05357c5d1c0eeac4c66f9ff7f2e6]]
-
-property testEncCfbPassB2 = and [ (cfbEnc encrypt k iv ps) == cs
-                                | k <- testKey2 | iv <- testIv2 | ps <- testPt2 | cs <- testCt2 ]
-
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/AES_CTR.cry b/Primitive/Symmetric/Cipher/Block/Modes/AES_CTR.cry
deleted file mode 100644
index ffe15e5c..00000000
--- a/Primitive/Symmetric/Cipher/Block/Modes/AES_CTR.cry
+++ /dev/null
@@ -1,19 +0,0 @@
-// Cryptol AES CTR test vectors
-// Copyright (c) 2010-2018, Galois Inc.
-// www.cryptol.net
-// Author: Ajay Kumar Eeralla
-// Test vectors from https://nvlpubs.nist.gov/nistpubs/Legacy/SP nistspecialpublication800-38a.pdf
-
-module Primitive::Symmetric::Cipher::Block::Modes::AES_CTR where
-import Primitive::Symmetric::Cipher::Block::Modes::CTR
-import Primitive::Symmetric::Cipher::Block::AES_parameterized
-
-property ctrEncCorrect enc k c ps = (ctrDec enc k c (ctrEnc enc k c ps)) == ps
-
-k = 0x2b7e151628aed2a6abf7158809cf4f3c
-ic = 0xf0f1f2f3f4f5f6f7f8f9fafbfcfdfeff
-plaintext = [0x6bc1bee22e409f96e93d7e117393172a, 0xae2d8a571e03ac9c9eb76fac45af8e51, 0x30c81c46a35ce411e5fbc1191a0a52ef, 0xf69f2445df4f9b17ad2b417be66c3710]
-ciphertext = [0x874d6191b620e3261bef6864990db6ce, 0x9806f66b7970fdff8617187bb9fffdff, 0x5ae4df3edbd5d35e5b4f09020db03eab, 0x1e031dda2fbe03d1792170a0f3009cee]
-
-property testPass = (ctrEnc encrypt k ic plaintext) == ciphertext
-
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry
index 470ea0e0..6cc68637 100644
--- a/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry
+++ b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry
@@ -17,4 +17,5 @@ cbcEnc enc k iv ps = cs
 cbcDec : {n, k} (fin n, fin k) => ([k]->block -> block) -> [k] -> iv -> [n]block -> [n]block
 cbcDec dec k iv cs = [ (dec k c) ^ c' | c <- cs | c' <- [iv] # cs ]
 
-
+// This will need to be parameterized with a specific encryption function before it can be proved
+property cbcEncCorrect encrypt k c ps = (cbcDec encrypt k c (cbcEnc encrypt k c ps)) == ps
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/CFB.cry b/Primitive/Symmetric/Cipher/Block/Modes/CFB.cry
index f7c0195e..8a4d887a 100644
--- a/Primitive/Symmetric/Cipher/Block/Modes/CFB.cry
+++ b/Primitive/Symmetric/Cipher/Block/Modes/CFB.cry
@@ -18,4 +18,6 @@ cfbEnc enc k iv ps = cs
 cfbDec : {n, k} (fin n, fin k) => ([k]->block -> block) -> [k] -> iv -> [n]block -> [n]block
 cfbDec enc k iv cs = [ (enc k c')^c | c <- cs | c' <- [iv] # cs ]
 
+// This will need to be parameterized with a specific encryption function before it can be proved
+property cfbEncCorrect encrypt k c ps = (cfbDec encrypt k c (cfbEnc encrypt k c ps)) == ps
 
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/CTR.cry b/Primitive/Symmetric/Cipher/Block/Modes/CTR.cry
index 0641d00e..2be695cb 100644
--- a/Primitive/Symmetric/Cipher/Block/Modes/CTR.cry
+++ b/Primitive/Symmetric/Cipher/Block/Modes/CTR.cry
@@ -20,6 +20,7 @@ ctrDec enc k c cs = ps
     where ps = [(enc k c')^ct | ct <- cs | c' <- ctrs]
           ctrs = [c+i | i<- [0...]]
 
-
+// This will need to be parameterized with a specific encryption function before it can be proved
+property ctrEncCorrect enc k c ps = (ctrDec enc k c (ctrEnc enc k c ps)) == ps
 
 
diff --git a/Primitive/Symmetric/Cipher/Block/README.md b/Primitive/Symmetric/Cipher/Block/README.md
index 75e57515..763757d9 100644
--- a/Primitive/Symmetric/Cipher/Block/README.md
+++ b/Primitive/Symmetric/Cipher/Block/README.md
@@ -1 +1,45 @@
 Symmetric ciphers that work on a block at a time.
+
+## AES Migration Guide
+In [PR #79](https://github.com/GaloisInc/cryptol-specs/pull/79), we simplified the AES modules and in doing so changed the public API used for AES.
+To update to the new module structure, you may need to make changes to your cryptol specs that use AES.
+The new module structure provides concrete instantiations for `AES128`, `AES192`, and `AES256`.
+It also provides a spec `AES_specification` that is generic over the key size, in case you want to implement something that supports multiple key sizes.
+Note that these are only the block cipher, operating over a single block at a time.
+For encryption over longer plaintexts, use a mode of operation.
+
+If you previously used `AES.cry`, you were implicitly using AES256. Update your import line to use `AES256.cry`, and update your encrypt and decrypt functions to change the name and order of arguments.
+Before:
+```haskell
+import Primitive::Symmetric::Cipher::Block::AES
+ct = aesEncrypt(data, key)
+pt = aesDecrypt(ct, key)
+```
+After:
+```haskell
+import Primitive::Symmetric::Cipher::Block::AES256 as AES256
+ct = AES256::encrypt key data
+pt = AES256::decrypt key ct
+```
+
+If you previously used `AES_parameterized.cry`, or if you want to implement something using AES with an arbitrary key length, update your import line to use `AES_specification.cry`, parameterized
+with your own key length parameter. The remaining API is unchanged, although we added a publicly accessible `KeySize` type.
+Before:
+```haskell
+import Primitive::Symmetric::Cipher::Block::AES_parameterized as AES
+
+parameter
+  /** 0: use AES128, 1: use AES192, 2: use AES256 */
+  type Mode : #
+  type constraint (2 >= Mode)
+```
+After:
+```haskell
+parameter
+  // This constraint enforces the standard key sizes of 128, 192, and 256 bits.
+  type KeySize : #
+  type constraint (fin KeySize, KeySize % 64 == 0, KeySize / 64 >= 2, KeySize / 64 <= 4)
+
+import Primitive::Symmetric::Cipher::Block::AES_specification as AES where
+  type KeySize' = KeySize
+```
\ No newline at end of file
diff --git a/Primitive/Symmetric/Cipher/Block/Tests/TestAES.cry b/Primitive/Symmetric/Cipher/Block/Tests/TestAES.cry
new file mode 100644
index 00000000..bab6e5ab
--- /dev/null
+++ b/Primitive/Symmetric/Cipher/Block/Tests/TestAES.cry
@@ -0,0 +1,47 @@
+/**
+ * Test vectors for AES256
+ * I don't actually know where these are sourced from.
+ */
+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]
+
+property aes128TestVectorsPass = and [ AES128::encrypt key msg == ct
+                     | msg <- pts | ct <- expected_cts]
+    where
+        key = 0x2b7e151628aed2a6abf7158809cf4f3c
+        expected_cts = [0x3ad77bb40d7a3660a89ecaf32466ef97
+          ,0xf5d3d58503b9699de785895a96fdbaaf
+          ,0x43b1cd7f598ece23881b00e3ed030688
+          ,0x7b0c785e27e8ad3f8223207104725dd4]
+
+
+property aes192TestVectorsPass = and [ AES192::encrypt key msg == ct
+                          | msg <- pts | ct <- expected_cts]
+    where
+        key = 0x8e73b0f7da0e6452c810f32b809079e562f8ead2522c6b7b
+        expected_cts = [0xbd334f1d6e45f25ff712a214571fa5cc
+          ,0x974104846d0ad3ad7734ecb3ecee4eef
+          ,0xef7afd2270e2e60adce0ba2face6444e
+          ,0x9a4b41ba738d6c72fb16691603c18e0e]
+
+property aes256TestVectorsPass = and [ AES256::encrypt key msg == ct
+                     | msg <- pts | ct <- expected_cts]
+    where
+        key = 0x603deb1015ca71be2b73aef0857d77811f352c073b6108d72d9810a30914dff4
+        expected_cts = [0xf3eed1bdb5d2a03c064b5a7e3db181f8
+          ,0x591ccb10d410ed26dc5ba74a31362870
+          ,0xb6ed21b99ca6f4f9f153e7b1beafed1d
+          ,0x23304b7a39f9f3ff067d8d8f9e24ecc7]
\ No newline at end of file
diff --git a/Primitive/Symmetric/Cipher/Block/Tests/TestAESKeyWrap.cry b/Primitive/Symmetric/Cipher/Block/Tests/TestAESKeyWrap.cry
index c823b93c..86ef3b62 100644
--- a/Primitive/Symmetric/Cipher/Block/Tests/TestAESKeyWrap.cry
+++ b/Primitive/Symmetric/Cipher/Block/Tests/TestAESKeyWrap.cry
@@ -1,6 +1,5 @@
 module Primitive::Symmetric::Cipher::Block::Tests::TestAESKeyWrap where
 
-import Primitive::Symmetric::Cipher::Block::AES
 import Primitive::Symmetric::Cipher::Block::AESKeyWrap
 
 // This section contains tests of the Key Wrap specifications using test
diff --git a/Primitive/Symmetric/Cipher/Block/Tests/TestAESKeyWrapPadded.cry b/Primitive/Symmetric/Cipher/Block/Tests/TestAESKeyWrapPadded.cry
index 920700a6..e70d44bb 100644
--- a/Primitive/Symmetric/Cipher/Block/Tests/TestAESKeyWrapPadded.cry
+++ b/Primitive/Symmetric/Cipher/Block/Tests/TestAESKeyWrapPadded.cry
@@ -1,6 +1,5 @@
 module Primitive::Symmetric::Cipher::Block::Tests::TestAESKeyWrapPadded where
 
-import Primitive::Symmetric::Cipher::Block::AES
 import Primitive::Symmetric::Cipher::Block::AESKeyWrapPadded
 
 testUnwrap : {a, b} ( fin a