SPEC.md: Describe top-level EVP_* AES-GCM functions

SPEC.md

@@ -37,14 +37,14 @@ The AES_(un)wrap_key_* functions are verified to have the following properties r
 
 ## AES-GCM
 
-These functions are verified to have the following properties related to AES-GCM using AES-256. These functions are defined in [NIST SP 800-38D](https://nvlpubs.nist.gov/nistpubs/Legacy/SP/nistspecialpublication800-38d.pdf). For more detailed specifications, see [AES-GCM.saw](SAW/proof/AES/AES-GCM.saw).
+The EVP_* functions are verified to have the following properties related to AES-GCM using AES-256. These functions are defined in [NIST SP 800-38D](https://nvlpubs.nist.gov/nistpubs/Legacy/SP/nistspecialpublication800-38d.pdf). For more detailed specifications, see [AES-GCM.saw](SAW/proof/AES/AES-GCM.saw).
 
 | Function  | Preconditions |  Postconditions |
 | ---------------| -------------| --------------- |
-| gcm_ghash_avx | <ul><li>The hash table parameter points to values precomputed by calling the `gcm_init_Htable` Cryptol function on a symbolic 128-bit value.</li><li>The input length is a symbolic integer 16 * k such that 0 < k < 18.</li></ul> | <ul><li>The Xi buffer holds the correct hash value as defined by the AES-GCM specification.</li></ul> |
-| aes_hw_ctr32_encrypt_blocks | <ul><li>The global variable `OPENSSL_ia32cap_P` exists and points to a value that [disables `AVX512[F|DQ|BW|VL]` instructions](https://www.openssl.org/docs/manmaster/man3/OPENSSL_ia32cap.html).</li><li>The length is a symbolic integer 16 * k such that 0 < k < 18.</li><li>The key parameter points to a 32-byte AES-256 key.</li></ul> | <ul><li>The global variable `OPENSSL_ia32cap_P` continues to point to the same value.</li><li>The output buffer holds the value produced by the GCTR function as defined by the AES-GCM specification.</li></ul> |
-| aesni_gcm_encrypt | <ul><li>The input length is a symbolic integer k such that k < 2^36.</li><li>The key parameter points to a 32-byte AES-256 key.</li><li>The hash table parameter points to values precomputed by calling the `get_Htable` Cryptol function on the AES-256 key.</li></ul> | <ul><li>If k >= 288, then the first k bytes of the output buffer will point to the ciphertext produced by the GCM-AE_K function as defined by the AES-GCM specification. If k < 288, then the output buffer will not be modified.</li><li>If k >= 288, then the Xi buffer will point to the updated Xi value computed by the `aesni_gcm_encrypt` Cryptol function. If k < 288, then the Xi buffer will not be modified.</li><li>If k >= 288, then the initialization vector buffer will point to the updated initialization vector value computed by the `aesni_gcm_encrypt` Cryptol function. If k < 288, then the initialization vector will not be updated.</li><li>The return value will be equal to 96 * floor(k / 96).</li></ul> |
-| aesni_gcm_decrypt | <ul><li>The input length is a symbolic integer k such that k < 2^36.</li><li>The key parameter points to a 32-byte AES-256 key.</li><li>The hash table parameter points to values precomputed by calling `get_Htable` on the AES-256 key.</li></ul> | <ul><li>If k >= 96, then the first k bytes of the output buffer will point to the ciphertext produced by the GCM-AD_K function as defined by the AES-GCM specification. If k < 96, then the output buffer will not be modified.</li><li>If k >= 96, then the Xi buffer will point to the updated Xi value computed by the `aesni_gcm_decrypt` Cryptol function. If k < 96, then the Xi buffer will not be modified.</li><li>If k >= 96, then the initialization vector buffer will point to the updated initialization vector value computed by the `aesni_gcm_decrypt` Cryptol function. If k < 96, then the initialization vector will not be updated.</li><li>The return value will be equal to 96 * floor(k / 96).</li></ul> |
+| EVP_CipherInit_ex | <ul><li>The global variable `OPENSSL_ia32cap_P` exists and points to a value that [disables `AVX512[F|DQ|BW|VL]` instructions](https://www.openssl.org/docs/manmaster/man3/OPENSSL_ia32cap.html).</li><li>The `ctx` parameter's `cipher` field is null.</li><li>The `cipher` parameter is a valid `EVP_CIPHER` such as the value returned by `EVP_aes_256_gcm()`.</li></ul> | <ul><li>The global variable `OPENSSL_ia32cap_P` continues to point to the same value.</li><li>The `ctx` field is initialized for AES-GCM using AES-256.</li><li>The `ctx` parameter's `cipher_data` field is initialized such that `mres` is `0`, `iv_set` is `1`, and `taglen` is `-1`.</li></ul> |
+| EVP_{Encrypt,Decrypt}Update | <ul><li>The global variable `OPENSSL_ia32cap_P` exists and points to a value that [disables `AVX512[F|DQ|BW|VL]` instructions](https://www.openssl.org/docs/manmaster/man3/OPENSSL_ia32cap.html).</li><li>The `ctx` field is initialized for AES-GCM using AES-256.</li><li>The `ctx` field's `cipher` parameter is a valid `EVP_CIPHER` such as the value returned by `EVP_aes_256_gcm()`.</li><li>The `ctx` parameter's `cipher_data` field is initialized such that `iv_set` is `1` and `taglen` is `-1`.</li><li>The `in_len` parameter is less than `2 ^^ 31`.</li><li>`ctx->gcm->msg.len` is less than `TOTAL_MESSAGE_MAX_LENGTH`, and `ctx->gcm->msg.len` plus `in_len` is less than `TOTAL_MESSAGE_MAX_LENGTH`.</li></ul> | <ul><li>The `out_len` parameter points to `in_len`.</li><li>Let `(ctx_updated, out_updated)` be the result of calling the `aes_gcm_{encrypt,decrypt}_update ctx in in_len out` Cryptol function, where `in`, `in_len`, and `out` correspond to the input parameters to the function.</li><li>The `ctx` parameter points to the key, length, hash table, and Xi values contained in `ctx_updated`.</li><li>The `ctx` parameter's `cipher_data` field is set such that `iv_set` is `1` and `taglen` is `-1`.</li><li>The `out` parameter points to `out_updated`.</li><li>The return value is `1`.</li></ul> |
+| EVP_EncryptFinal_ex | <ul><li>The `ctx` field is initialized for AES-GCM using AES-256.</li><li>The `ctx` field's `cipher` parameter is a valid `EVP_CIPHER` such as the value returned by `EVP_aes_256_gcm()`.</li><li>The `ctx` parameter's `cipher_data` field is initialized such that `iv_set` is `1` and `taglen` is `-1`.</li></ul> | <ul><li>The `ctx` parameter's `buf` field points to the result of calling the `cipher_final ctx` Cryptol function.</li><li>The `ctx` parameter's `cipher_data` field is set such that the `mres` value is the same as before calling the function, `iv_set` is `0`, and `taglen` is `AES_BLOCK_SIZE`.</li><li>The `out_len` parameter points to 0.</li><li>The return value is 1.</li></ul> |
+| EVP_DecryptFinal_ex | <ul><li>The `ctx` field is initialized for AES-GCM using AES-256.</li><li>The `ctx` field's `cipher` parameter is a valid `EVP_CIPHER` such as the value returned by `EVP_aes_256_gcm()`.</li><li>The `ctx` parameter's `cipher_data` field is initialized such that `iv_set` is `1` and `taglen` is `AES_BLOCK_SIZE`.</li><li>The `ctx` parameter's `buf` field is allocated.</li></ul> | <ul><li>The `ctx` parameter's `buf` field points to the result of calling the `cipher_final ctx` Cryptol function.</li><li>The `ctx` parameter's `cipher_data` field is set such that the `mres` value is the same as before calling the function, `iv_set` is `1` if the initial value of the `ctx` parameter's `buf` field is equal to the result of calling the `cipher_final ctx` Cryptol functio (and `0` otherwise), and `taglen` is `AES_BLOCK_SIZE`.</li><li>The `out_len` parameter points to 0.</li><li>If the initial value of the `ctx` parameter's `buf` field is equal to the result of calling the `cipher_final ctx` Cryptol function, then the return value will be 1. Otherwise, the return value will be 0.</li></ul> |
 
 ## Elliptic Curve Keys and Parameters