def aes_key_from_no_valid

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

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

537def aes_key_from_no_valid(+bytes: List<&2, U32>,
538    size: Maybe<&0, {List.length(&2, U32, bytes) == 32n : Nat}>) ->
539    {AES.key_from_proofs(bytes, size, None{}) == Fail{AES.InvalidKey{}} :
540      Result<&2, &2, AES.Error, AES.SecretKey>}:
541    match size:
542        case None{}: {==}
543        case Some{size}: {==}