def decrypt_inputs

qasim-bend-kit@0.1.0.2 · proof/AES_NistInputProof.bend:28

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

28def decrypt_inputs(+key: AES.SecretKey, +fixture_key: AES.SecretKey,
29    +aad: List<&2, U32>, +fixture_aad: List<&2, U32>,
30    +envelope: AES.Envelope, +fixture_envelope: AES.Envelope,
31    +expected: Result<&2, &2, AES.Error, List<&2, U32>>,
32    key_matches: {key == fixture_key : AES.SecretKey},
33    aad_matches: {aad == fixture_aad : List<&2, U32>},
34    envelope_matches: {envelope == fixture_envelope : AES.Envelope},
35    computed: {AES.decrypt(fixture_key, fixture_aad, fixture_envelope) == expected : Result<&2, &2, AES.Error, List<&2, U32>>}) ->
36    {AES.decrypt(key, aad, envelope) == expected : Result<&2, &2, AES.Error, List<&2, U32>>}:
37    Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
38        AES.decrypt(key, aad, envelope), AES.decrypt(fixture_key, aad, envelope), expected,
39        Equal.cong(AES.SecretKey, Result<&2, &2, AES.Error, List<&2, U32>>,
40            value => AES.decrypt(value, aad, envelope), key, fixture_key, key_matches),
41        Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
42            AES.decrypt(fixture_key, aad, envelope), AES.decrypt(fixture_key, fixture_aad, envelope), expected,
43            Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>,
44                value => AES.decrypt(fixture_key, value, envelope), aad, fixture_aad, aad_matches),
45            Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
46                AES.decrypt(fixture_key, fixture_aad, envelope), AES.decrypt(fixture_key, fixture_aad, fixture_envelope), expected,
47                Equal.cong(AES.Envelope, Result<&2, &2, AES.Error, List<&2, U32>>,
48                    value => AES.decrypt(fixture_key, fixture_aad, value), envelope, fixture_envelope, envelope_matches), computed)))