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 Refactor AES spec to meet "gold standard" requirements #77) Based on discussion, this will now be handled in Distinguish between spec-conformant and SAW-optimized Cryptol #86
  • 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 This will be handled in Convert GCM mode to a Literate spec #87
• 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.