~/jendhub

def aes_bytes_proof_none_if_invalid

qasim-bend-kit@0.1.0.2 · PROOF.bend:450

import qasim-bend-kit@0.1.0.2/PROOF.bend as PROOF
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

450def aes_bytes_proof_none_if_invalid(+bytes: List<&2, U32>,
451    generated: Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>,
452    no: {AES.bytes_valid(bytes) == False{} : Bool}) ->
453    {generated == None{} : Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>}:
454    match generated:
455        case None{}: {==}
456        case Some{valid}:
457            contradiction = Equal.trans(Bool, True{}, AES.bytes_valid(bytes),
458                False{}, Equal.sym(Bool, AES.bytes_valid(bytes), True{}, valid),
459                no)
460            PrimitiveProof.absurd(
461                {Some{valid} == None{} :
462                  Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>},
463                PrimitiveProof.false_true(Equal.sym(Bool, True{}, False{},
464                    contradiction)))

Uses (9)

Used by (1)