AESNistInputProof.decrypt_inputs: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_NistInputProof.bend as AESNistInputProof
Lines 28-48 of qasim-bend-kit@0.1.0.2/proof/AES_NistInputProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistInputProof.bend&start_line=28&end_line=48

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES

def decrypt_inputs(+key: AES.SecretKey, +fixture_key: AES.SecretKey,
    +aad: List<&2, U32>, +fixture_aad: List<&2, U32>,
    +envelope: AES.Envelope, +fixture_envelope: AES.Envelope,
    +expected: Result<&2, &2, AES.Error, List<&2, U32>>,
    key_matches: {key == fixture_key : AES.SecretKey},
    aad_matches: {aad == fixture_aad : List<&2, U32>},
    envelope_matches: {envelope == fixture_envelope : AES.Envelope},
    computed: {AES.decrypt(fixture_key, fixture_aad, fixture_envelope) == expected : Result<&2, &2, AES.Error, List<&2, U32>>}) ->
    {AES.decrypt(key, aad, envelope) == expected : 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(fixture_key, aad, envelope), expected,
        Equal.cong(AES.SecretKey, Result<&2, &2, AES.Error, List<&2, U32>>,
            value => AES.decrypt(value, aad, envelope), key, fixture_key, key_matches),
        Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
            AES.decrypt(fixture_key, aad, envelope), AES.decrypt(fixture_key, fixture_aad, envelope), expected,
            Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>,
                value => AES.decrypt(fixture_key, value, envelope), aad, fixture_aad, aad_matches),
            Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
                AES.decrypt(fixture_key, fixture_aad, envelope), AES.decrypt(fixture_key, fixture_aad, fixture_envelope), expected,
                Equal.cong(AES.Envelope, Result<&2, &2, AES.Error, List<&2, U32>>,
                    value => AES.decrypt(fixture_key, fixture_aad, value), envelope, fixture_envelope, envelope_matches), computed)))

Uses (9):
  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=decrypt