AESNistObservationProof.finish_encrypt: 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 105-136 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=105&end_line=136

import Base
import qasim-bend-kit@0.1.0.2/LAWS.bend as L
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

def finish_encrypt(+key: AES.SecretKey, +nonce: AES.Nonce,
    +aad: List<&2, U32>, +plaintext: List<&2, U32>,
    +words: List<&2, U32>, +bytes: List<&2, U32>, +tag: List<&2, U32>,
    aad_ok: {AES.aad_valid(aad) == True{} : Bool},
    plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool},
    key_matches: {Core.aes256_expand(AES.secret_key_bytes(key)) == words : List<&2, U32>},
    ciphertext_matches: {ciphertext(Core.gcm_ctr_encrypt(words, AES.raw_nonce_bytes(nonce), plaintext)) == bytes : List<&2, U32>},
    tag_matches: {Core.gcm_tag_bytes(Core.gcm_tag_output(words, AES.raw_nonce_bytes(nonce), aad, bytes)) == tag : List<&2, U32>}) ->
    {L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)) ==
     List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag)) : List<&2, U32>}:
    Equal.trans(List<&2, U32>,
        L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)),
        expanded(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad, plaintext),
        List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag)),
        checked_encrypt(key, nonce, aad, plaintext, aad_ok, plaintext_ok),
        Equal.trans(List<&2, U32>,
            expanded(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad, plaintext),
            expanded(words, nonce, aad, plaintext),
            List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag)),
            Equal.cong(List<&2, U32>, List<&2, U32>, expanded_words =>
                expanded(expanded_words, nonce, aad, plaintext),
                Core.aes256_expand(AES.secret_key_bytes(key)), words, key_matches),
            Equal.trans(List<&2, U32>, expanded(words, nonce, aad, plaintext),
                parts(words, nonce, aad, bytes),
                List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag)),
                Equal.cong(List<&2, U32>, List<&2, U32>, encrypted => parts(words, nonce, aad, encrypted),
                    ciphertext(Core.gcm_ctr_encrypt(words, AES.raw_nonce_bytes(nonce), plaintext)), bytes,
                    ciphertext_matches),
                Equal.cong(List<&2, U32>, List<&2, U32>, tag_bytes =>
                    List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag_bytes)),
                    Core.gcm_tag_bytes(Core.gcm_tag_output(words, AES.raw_nonce_bytes(nonce), aad, bytes)),
                    tag, tag_matches))))

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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.append
  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/LAWS.bend&name=aes256gcm_nist_encrypt_observation
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Nonce
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=SecretKey
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=aad_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=encrypt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=plaintext_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=raw_nonce_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=secret_key_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=aes256_expand
  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_tag_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_tag_output
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=checked_encrypt
  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=expanded
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=parts