def finish_cipher

qasim-bend-kit@0.1.0.2 · proof/AES_NistObservationProof.bend:41

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

41def finish_cipher(+words: List<&2, U32>, +nonce: List<&2, U32>, +input: List<&2, U32>, +stream: List<&2, U32>, +output: List<&2, U32>,
42    computed: {Core.gcm_ctr_stream_exact(List.length(&2, U32, input), words, Core.gcm_inc32(Core.gcm_j0(nonce))) == stream : List<&2, U32>},
43    xor_matches: {Core.gcm_zip_xor(input, stream) == output : List<&2, U32>}) ->
44    {ciphertext(Core.gcm_ctr_encrypt(words, nonce, input)) == output : List<&2, U32>}:
45    Equal.trans(List<&2, U32>, ciphertext(Core.gcm_ctr_encrypt(words, nonce, input)),
46        Core.gcm_decrypt_expanded(words, nonce, input), output, ciphertext_shape(words, nonce, input),
47        Equal.trans(List<&2, U32>, Core.gcm_decrypt_expanded(words, nonce, input),
48            Core.gcm_zip_xor(input, stream), output, xor_from_stream(words, nonce, input, stream, computed), xor_matches))