def preserves_nonce

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

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

445def preserves_nonce(+key: AES.SecretKey, +nonce: AES.Nonce,
446    +aad: List<&2, U32>, +plaintext: List<&2, U32>,
447    +envelope: AES.Envelope,
448    encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
449        Result<&2, &2, AES.Error, AES.Envelope>}) ->
450    {AES.envelope_nonce(envelope) == nonce : AES.Nonce}:
451    Equal.trans(AES.Nonce,
452        result_nonce(nonce, Done{envelope}),
453        result_nonce(nonce, AES.encrypt(key, nonce, aad, plaintext)),
454        nonce,
455        Equal.sym(AES.Nonce,
456            result_nonce(nonce, AES.encrypt(key, nonce, aad, plaintext)),
457            result_nonce(nonce, Done{envelope}),
458            Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, AES.Nonce,
459                result => result_nonce(nonce, result),
460                AES.encrypt(key, nonce, aad, plaintext), Done{envelope},
461                encrypted)),
462        encrypt_nonce(key, nonce, aad, plaintext))