Skip to content

Commit

Permalink
Fix comments
Browse files Browse the repository at this point in the history
  • Loading branch information
pennyannn committed Sep 6, 2024
1 parent e49f75d commit db779ef
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion Tests/AES-GCM/AESGCMDecKernelProgram.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Tests/AES-GCM/AESGCMEncKernelProgram.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion Tests/AES-GCM/GCMInitV8Program.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down

0 comments on commit db779ef

Please sign in to comment.