def aes_nonce_from_no_valid

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

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

580def aes_nonce_from_no_valid(+bytes: List<&2, U32>,
581    size: Maybe<&0, {List.length(&2, U32, bytes) == 12n : Nat}>) ->
582    {AES.nonce_from_proofs(bytes, size, None{}) == Fail{AES.InvalidNonce{}} :
583      Result<&2, &2, AES.Error, AES.Nonce>}:
584    match size:
585        case None{}: {==}
586        case Some{size}: {==}