PROOF.aes_bytes_proof_none_if_invalid: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/PROOF.bend as PROOF
Lines 450-464 of qasim-bend-kit@0.1.0.2/PROOF.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/PROOF.bend&start_line=450&end_line=464

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

def aes_bytes_proof_none_if_invalid(+bytes: List<&2, U32>,
    generated: Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>,
    no: {AES.bytes_valid(bytes) == False{} : Bool}) ->
    {generated == None{} : Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>}:
    match generated:
        case None{}: {==}
        case Some{valid}:
            contradiction = Equal.trans(Bool, True{}, AES.bytes_valid(bytes),
                False{}, Equal.sym(Bool, AES.bytes_valid(bytes), True{}, valid),
                no)
            PrimitiveProof.absurd(
                {Some{valid} == None{} :
                  Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>},
                PrimitiveProof.false_true(Equal.sym(Bool, True{}, False{},
                    contradiction)))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Maybe
  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=bytes_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=absurd
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=false_true