def finish_decrypt
qasim-bend-kit@0.1.0.2 · proof/AES_NistObservationProof.bend:230
import qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend as AESNistObservationProof
import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
230def finish_decrypt(+key: AES.SecretKey, +aad: List<&2, U32>, +envelope: AES.Envelope,
231 +words: List<&2, U32>, +result: Result<&2, &2, AES.Error, List<&2, U32>>,
232 aad_ok: {AES.aad_valid(aad) == True{} : Bool},
233 ciphertext_ok: {AES.plaintext_valid(AES.ciphertext(envelope)) == True{} : Bool},
234 key_matches: {Core.aes256_expand(AES.secret_key_bytes(key)) == words : List<&2, U32>},
235 expanded_matches: {decrypt_expanded(words, aad, envelope) == result : Result<&2, &2, AES.Error, List<&2, U32>>}) ->
236 {AES.decrypt(key, aad, envelope) == result : Result<&2, &2, AES.Error, List<&2, U32>>}:
237 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
238 AES.decrypt(key, aad, envelope), AES.decrypt_authenticated(key, aad, envelope), result,
239 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
240 AES.decrypt_checked(key, aad, envelope, AES.aad_valid(aad), AES.plaintext_valid(AES.ciphertext(envelope))),
241 AES.decrypt_checked(key, aad, envelope, True{}, AES.plaintext_valid(AES.ciphertext(envelope))),
242 AES.decrypt_checked(key, aad, envelope, True{}, True{}),
243 Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>, flag =>
244 AES.decrypt_checked(key, aad, envelope, flag, AES.plaintext_valid(AES.ciphertext(envelope))),
245 AES.aad_valid(aad), True{}, aad_ok),
246 Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>, flag =>
247 AES.decrypt_checked(key, aad, envelope, True{}, flag),
248 AES.plaintext_valid(AES.ciphertext(envelope)), True{}, ciphertext_ok)),
249 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
250 AES.decrypt_authenticated(key, aad, envelope),
251 decrypt_expanded(Core.aes256_expand(AES.secret_key_bytes(key)), aad, envelope), result,
252 decrypt_key_shape(key, aad, envelope),
253 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
254 decrypt_expanded(Core.aes256_expand(AES.secret_key_bytes(key)), aad, envelope),
255 decrypt_expanded(words, aad, envelope), result,
256 Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>, expanded_words =>
257 decrypt_expanded(expanded_words, aad, envelope),
258 Core.aes256_expand(AES.secret_key_bytes(key)), words, key_matches), expanded_matches)))