Update AES-GCM to meet "gold standard" requirements

[marsella]

The GCM spec and AES instantiation of it needs a bit of work to meet our "gold standard" for specs. This was initially flagged in discussion on #75; see that PR for more details.

Some things to review:

• [ ] There's a duplicated version (AES_256_GCM.cry and AES_GCM.cry). Determine whether we can remove this duplication or improve documentation to explain why we need two versions (maybe blocked on #77)
  • [ ] Consider rewriting GCM.cry in terms of Cipher so that the instantiation is simpler and it can be reused for other (non-AES) block ciphers
  • [ ] Consider making separate modules for different key sizes (AES256_GCM and AES128_GCM)
• [ ] Review parameter choices to make sure they are as tight as the NIST spec requires
• [ ] Check for properties defined in the NIST spec and make sure they are explicit in the cryptol spec
  • [ ] GCTR: if X is empty, the return value should be the empty string
• [ ] Convert into a literate spec
• [ ] Add warnings in the spec and readme about failure modes that Cryptol cannot prevent (IV reuse)
• [ ] Switch to using options instead of record return
• [ ] Note any additional proposed changes in this issue

[marsella]

Here are my notes on the parameter requirements in the NIST spec:

• P17: t may be any one of the following five values: 128, 120, 112, 104, or 96
• P15: the block size shall be 128 bits
• P15: the key size shall be at least 128 bits
• P16: len(P) $\le 2^{39}-256$; len(P) is a multiple of 8
• P16: len(A) $\le 2^{64}-1$; len(A) is a multiple of 8
• P16: $1 \le \text{len(IV)} \le 2^64-1$; len(IV) is a multiple of 8
• encrypt and decrypt have to support the same len(C, A, IV)s.