AESEncryptProof.successful_encrypt_decrypt_roundtrip: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend as AESEncryptProof
Lines 565-610 of qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend&start_line=565&end_line=610

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

def successful_encrypt_decrypt_roundtrip(+key: AES.SecretKey,
    +nonce: AES.Nonce, +aad: List<&2, U32>,
    +plaintext: List<&2, U32>, +envelope: AES.Envelope,
    +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
        Result<&2, &2, AES.Error, AES.Envelope>}) ->
    {AES.decrypt(key, aad, envelope) == Done{plaintext} :
        Result<&2, &2, AES.Error, List<&2, U32>>}:
    +aad_ok = successful_encrypt_aad_valid(key, nonce, aad, plaintext,
        AES.aad_valid(aad), AES.plaintext_valid(plaintext), {==}, {==},
        envelope, encrypted)
    +plaintext_ok = successful_encrypt_plaintext_valid(key, nonce, aad,
        plaintext, AES.aad_valid(aad), AES.plaintext_valid(plaintext),
        {==}, {==}, envelope, encrypted)
    ciphertext_ok = successful_encrypt_ciphertext_valid(key, nonce, aad,
        plaintext, envelope, aad_ok, plaintext_ok, encrypted)
    authenticated = successful_encrypt_decrypt_authenticated(key, nonce,
        aad, plaintext, envelope, aad_ok, plaintext_ok, encrypted)
    aad_checked = Equal.cong(Bool,
        Result<&2, &2, AES.Error, List<&2, U32>>,
        flag => AES.decrypt_checked(key, aad, envelope, flag,
            AES.plaintext_valid(AES.ciphertext(envelope))),
        AES.aad_valid(aad), True{}, aad_ok)
    ciphertext_checked = Equal.cong(Bool,
        Result<&2, &2, AES.Error, List<&2, U32>>,
        flag => AES.decrypt_checked(key, aad, envelope, True{}, flag),
        AES.plaintext_valid(AES.ciphertext(envelope)), True{}, ciphertext_ok)
    Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
        AES.decrypt(key, aad, envelope),
        AES.decrypt_checked(key, aad, envelope, True{}, True{}),
        Done{plaintext},
        Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
            AES.decrypt(key, aad, envelope),
            AES.decrypt_checked(key, aad, envelope,
                AES.aad_valid(aad),
                AES.plaintext_valid(AES.ciphertext(envelope))),
            AES.decrypt_checked(key, aad, envelope, True{}, True{}),
            {==},
            Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
                AES.decrypt_checked(key, aad, envelope,
                    AES.aad_valid(aad),
                    AES.plaintext_valid(AES.ciphertext(envelope))),
                AES.decrypt_checked(key, aad, envelope, True{},
                    AES.plaintext_valid(AES.ciphertext(envelope))),
                AES.decrypt_checked(key, aad, envelope, True{}, True{}),
                aad_checked, ciphertext_checked)),
        authenticated)

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Envelope
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Nonce
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=SecretKey
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=aad_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=ciphertext
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=decrypt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=decrypt_checked
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=encrypt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=plaintext_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend&name=successful_encrypt_aad_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend&name=successful_encrypt_ciphertext_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend&name=successful_encrypt_decrypt_authenticated
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend&name=successful_encrypt_plaintext_valid