def encrypt_matches

qasim-bend-kit@0.1.0.2 · proof/AES_KnownAnswerProof.bend:97

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

97def encrypt_matches(+key: AES.SecretKey, +nonce: AES.Nonce,
98    +aad: List<&2, U32>, +plaintext: List<&2, U32>,
99    +ciphertext: List<&2, U32>, +tag_bytes: List<&2, U32>,
100    aad_valid: {AES.aad_valid(aad) == True{} : Bool},
101    plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
102    ciphertext_matches: {Fields.output_ciphertext(AES.encrypt_valid_output(
103        key, nonce, aad, plaintext)) == ciphertext : List<&2, U32>},
104    tag_matches: {Fields.output_tag(AES.encrypt_valid_output(key, nonce, aad,
105        plaintext)) == tag_bytes : List<&2, U32>},
106    +tag_size: {List.length(&2, U32, tag_bytes) == 16n : Nat},
107    +tag_valid: {AES.bytes_valid(tag_bytes) == True{} : Bool},
108    +ciphertext_valid: {AES.bytes_valid(ciphertext) == True{} : Bool}) ->
109    {AES.encrypt(key, nonce, aad, plaintext) ==
110     Done{AES.Envelope{nonce, ciphertext,
111        AES.Tag{tag_bytes, tag_size, tag_valid}, ciphertext_valid}} :
112        Result<&2, &2, AES.Error, AES.Envelope>}:
113    aad_checked = Equal.cong(Bool,
114        Result<&2, &2, AES.Error, AES.Envelope>,
115        flag => AES.encrypt_checked(key, nonce, aad, plaintext, flag,
116            AES.plaintext_valid(plaintext)), AES.aad_valid(aad), True{},
117        aad_valid)
118    plaintext_checked = Equal.cong(Bool,
119        Result<&2, &2, AES.Error, AES.Envelope>,
120        flag => AES.encrypt_checked(key, nonce, aad, plaintext, True{}, flag),
121        AES.plaintext_valid(plaintext), True{}, plaintext_valid)
122    output_eq = output_matches(nonce,
123        AES.encrypt_valid_output(key, nonce, aad, plaintext), ciphertext,
124        tag_bytes, ciphertext_matches, tag_matches, tag_size, tag_valid,
125        ciphertext_valid)
126    Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
127        AES.encrypt(key, nonce, aad, plaintext),
128        AES.encrypt_valid(key, nonce, aad, plaintext),
129        Done{AES.Envelope{nonce, ciphertext,
130            AES.Tag{tag_bytes, tag_size, tag_valid}, ciphertext_valid}},
131        Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
132            AES.encrypt(key, nonce, aad, plaintext),
133            AES.encrypt_checked(key, nonce, aad, plaintext, True{},
134                AES.plaintext_valid(plaintext)),
135            AES.encrypt_valid(key, nonce, aad, plaintext),
136            aad_checked, plaintext_checked), output_eq)