def successful_encrypt_aad_valid

qasim-bend-kit@0.1.0.2 · proof/AES_EncryptProof.bend:123

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

123def successful_encrypt_aad_valid(+key: AES.SecretKey,
124    +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>,
125    +aad_flag: Bool, +plaintext_flag: Bool,
126    aad_ok: {AES.aad_valid(aad) == aad_flag : Bool},
127    plaintext_ok: {AES.plaintext_valid(plaintext) == plaintext_flag : Bool},
128    +envelope: AES.Envelope,
129    encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
130        Result<&2, &2, AES.Error, AES.Envelope>}) ->
131    {aad_flag == True{} : Bool}:
132    match aad_flag:
133        case True{}: {==}
134        case False{}:
135            checked = encrypt_checked_with_flags(key, nonce, aad, plaintext,
136                aad_flag, plaintext_flag, aad_ok, plaintext_ok, envelope,
137                encrypted)
138            Equal.trans(Bool, False{},
139                Result.is_done(&2, &2, AES.Error, AES.Envelope,
140                    AES.encrypt_checked(key, nonce, aad, plaintext,
141                        aad_flag, plaintext_flag)),
142                True{}, {==},
143                Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, Bool,
144                    result => Result.is_done(&2, &2, AES.Error, AES.Envelope,
145                        result),
146                    AES.encrypt_checked(key, nonce, aad, plaintext,
147                        aad_flag, plaintext_flag), Done{envelope}, checked))