def encrypt_checked_with_flags

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

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

79def encrypt_checked_with_flags(+key: AES.SecretKey, +nonce: AES.Nonce,
80    +aad: List<&2, U32>, +plaintext: List<&2, U32>,
81    +aad_flag: Bool, +plaintext_flag: Bool,
82    aad_ok: {AES.aad_valid(aad) == aad_flag : Bool},
83    plaintext_ok: {AES.plaintext_valid(plaintext) == plaintext_flag : Bool},
84    +envelope: AES.Envelope,
85    +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
86        Result<&2, &2, AES.Error, AES.Envelope>}) ->
87    {AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
88        plaintext_flag) == Done{envelope} :
89        Result<&2, &2, AES.Error, AES.Envelope>}:
90    changed_flags = Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
91            AES.encrypt(key, nonce, aad, plaintext),
92            AES.encrypt_checked(key, nonce, aad, plaintext,
93                AES.aad_valid(aad), AES.plaintext_valid(plaintext)),
94            AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
95                plaintext_flag), {==},
96            Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
97                AES.encrypt_checked(key, nonce, aad, plaintext,
98                    AES.aad_valid(aad), AES.plaintext_valid(plaintext)),
99                AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
100                    AES.plaintext_valid(plaintext)),
101                AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
102                    plaintext_flag),
103                Equal.cong(Bool, Result<&2, &2, AES.Error, AES.Envelope>,
104                    flag => AES.encrypt_checked(key, nonce, aad, plaintext,
105                        flag, AES.plaintext_valid(plaintext)),
106                    AES.aad_valid(aad), aad_flag, aad_ok),
107                Equal.cong(Bool, Result<&2, &2, AES.Error, AES.Envelope>,
108                    flag => AES.encrypt_checked(key, nonce, aad, plaintext,
109                        aad_flag, flag),
110                    AES.plaintext_valid(plaintext), plaintext_flag,
111                    plaintext_ok)))
112    Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
113        AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
114            plaintext_flag),
115        AES.encrypt(key, nonce, aad, plaintext),
116        Done{envelope},
117        Equal.sym(Result<&2, &2, AES.Error, AES.Envelope>,
118            AES.encrypt(key, nonce, aad, plaintext),
119            AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
120                plaintext_flag), changed_flags),
121        encrypted)