AESNistObservationProof.finish_decrypt: 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 230-258 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=230&end_line=258

import Base
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_decrypt(+key: AES.SecretKey, +aad: List<&2, U32>, +envelope: AES.Envelope,
    +words: List<&2, U32>, +result: Result<&2, &2, AES.Error, List<&2, U32>>,
    aad_ok: {AES.aad_valid(aad) == True{} : Bool},
    ciphertext_ok: {AES.plaintext_valid(AES.ciphertext(envelope)) == True{} : Bool},
    key_matches: {Core.aes256_expand(AES.secret_key_bytes(key)) == words : List<&2, U32>},
    expanded_matches: {decrypt_expanded(words, aad, envelope) == result : Result<&2, &2, AES.Error, List<&2, U32>>}) ->
    {AES.decrypt(key, aad, envelope) == result : Result<&2, &2, AES.Error, List<&2, U32>>}:
    Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
        AES.decrypt(key, aad, envelope), AES.decrypt_authenticated(key, aad, envelope), result,
        Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
            AES.decrypt_checked(key, aad, envelope, AES.aad_valid(aad), AES.plaintext_valid(AES.ciphertext(envelope))),
            AES.decrypt_checked(key, aad, envelope, True{}, AES.plaintext_valid(AES.ciphertext(envelope))),
            AES.decrypt_checked(key, aad, envelope, True{}, True{}),
            Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>, flag =>
                AES.decrypt_checked(key, aad, envelope, flag, AES.plaintext_valid(AES.ciphertext(envelope))),
                AES.aad_valid(aad), True{}, aad_ok),
            Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>, flag =>
                AES.decrypt_checked(key, aad, envelope, True{}, flag),
                AES.plaintext_valid(AES.ciphertext(envelope)), True{}, ciphertext_ok)),
        Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
            AES.decrypt_authenticated(key, aad, envelope),
            decrypt_expanded(Core.aes256_expand(AES.secret_key_bytes(key)), aad, envelope), result,
            decrypt_key_shape(key, aad, envelope),
            Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
                decrypt_expanded(Core.aes256_expand(AES.secret_key_bytes(key)), aad, envelope),
                decrypt_expanded(words, aad, envelope), result,
                Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>, expanded_words =>
                    decrypt_expanded(expanded_words, aad, envelope),
                    Core.aes256_expand(AES.secret_key_bytes(key)), words, key_matches), expanded_matches)))

Uses (19):
  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=Result
  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/AES256GCM.bend&name=Envelope
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Error
  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=ciphertext
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=decrypt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=decrypt_authenticated
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=decrypt_checked
  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=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/proof/AES_NistObservationProof.bend&name=decrypt_expanded
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=decrypt_key_shape