AESEncryptProof.encrypt_checked_with_flags: 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 79-121 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=79&end_line=121

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

def encrypt_checked_with_flags(+key: AES.SecretKey, +nonce: AES.Nonce,
    +aad: List<&2, U32>, +plaintext: List<&2, U32>,
    +aad_flag: Bool, +plaintext_flag: Bool,
    aad_ok: {AES.aad_valid(aad) == aad_flag : Bool},
    plaintext_ok: {AES.plaintext_valid(plaintext) == plaintext_flag : Bool},
    +envelope: AES.Envelope,
    +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
        Result<&2, &2, AES.Error, AES.Envelope>}) ->
    {AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
        plaintext_flag) == Done{envelope} :
        Result<&2, &2, AES.Error, AES.Envelope>}:
    changed_flags = Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
            AES.encrypt(key, nonce, aad, plaintext),
            AES.encrypt_checked(key, nonce, aad, plaintext,
                AES.aad_valid(aad), AES.plaintext_valid(plaintext)),
            AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
                plaintext_flag), {==},
            Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
                AES.encrypt_checked(key, nonce, aad, plaintext,
                    AES.aad_valid(aad), AES.plaintext_valid(plaintext)),
                AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
                    AES.plaintext_valid(plaintext)),
                AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
                    plaintext_flag),
                Equal.cong(Bool, Result<&2, &2, AES.Error, AES.Envelope>,
                    flag => AES.encrypt_checked(key, nonce, aad, plaintext,
                        flag, AES.plaintext_valid(plaintext)),
                    AES.aad_valid(aad), aad_flag, aad_ok),
                Equal.cong(Bool, Result<&2, &2, AES.Error, AES.Envelope>,
                    flag => AES.encrypt_checked(key, nonce, aad, plaintext,
                        aad_flag, flag),
                    AES.plaintext_valid(plaintext), plaintext_flag,
                    plaintext_ok)))
    Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
        AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
            plaintext_flag),
        AES.encrypt(key, nonce, aad, plaintext),
        Done{envelope},
        Equal.sym(Result<&2, &2, AES.Error, AES.Envelope>,
            AES.encrypt(key, nonce, aad, plaintext),
            AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
                plaintext_flag), changed_flags),
        encrypted)

Uses (15):
  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.sym
  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=encrypt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=encrypt_checked
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=plaintext_valid