AESNistObservationProof.finish_cipher: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend as AESNistObservationProof
Lines 41-48 of qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&start_line=41&end_line=48

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

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

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_ctr_encrypt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_ctr_stream_exact
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_decrypt_expanded
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_inc32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_j0
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_zip_xor
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=ciphertext
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=ciphertext_shape
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=xor_from_stream