diff --git a/Tests/AES-GCM/AESGCMDecKernelProgram.lean b/Tests/AES-GCM/AESGCMDecKernelProgram.lean index 8d9131d5..06bd110d 100644 --- a/Tests/AES-GCM/AESGCMDecKernelProgram.lean +++ b/Tests/AES-GCM/AESGCMDecKernelProgram.lean @@ -21,7 +21,7 @@ open BitVec Xi -- current hash/tag value, should match with input to aes_gcm_enc_kernel (x3) ivec -- counter, should match with input to aes_gcm_enc_kernel (x4) key -- AES key schedule and rounds (x5) - Htable -- powers of H precomputed up to H^12 (x6) + Htable -- powers of H precomputed up to H^8 (x6) output: out -- plaintext (x2) Xi -- current hash/tag value, decryption function will recalculate the hash based on the ciphertext, the top-level c function diff --git a/Tests/AES-GCM/AESGCMEncKernelProgram.lean b/Tests/AES-GCM/AESGCMEncKernelProgram.lean index 193af54e..8a9c201b 100644 --- a/Tests/AES-GCM/AESGCMEncKernelProgram.lean +++ b/Tests/AES-GCM/AESGCMEncKernelProgram.lean @@ -21,7 +21,7 @@ open BitVec Xi -- current hash/tag value (x3) ivec -- counter (x4) key -- AES key schedule and rounds (x5) - Htable -- powers of H precomputed up to H^12 (x6) + Htable -- powers of H precomputed up to H^8 (x6) output: out -- ciphertext (x2) Xi -- current hash/tag value (x3) diff --git a/Tests/AES-GCM/GCMInitV8Program.lean b/Tests/AES-GCM/GCMInitV8Program.lean index 70c51518..10c43638 100644 --- a/Tests/AES-GCM/GCMInitV8Program.lean +++ b/Tests/AES-GCM/GCMInitV8Program.lean @@ -14,7 +14,7 @@ open BitVec void gcm_init_v8(u128 Htable[16], const uint64_t H[2]); input: H - initial hash (x1) - output: Htable - powers of H precomputed up to H^12 (x0) + output: Htable - powers of H precomputed up to H^8 (x0) -/ def gcm_init_v8_program : Program :=