def tag_from_proofs

qasim-bend-kit@0.1.0.2 · libs/AES256GCM.bend:398

import Base

398def tag_from_proofs(bytes: List<&2, U32>,
399    size: Maybe<&0, {List.length(&2, U32, bytes) == 16n : Nat}>,
400    valid: Maybe<&0, {bytes_valid(bytes) == True{} : Bool}>) -> Maybe<&2, Tag>:
401    match size valid:
402        case Some{size} Some{valid}: Some{Tag{bytes, size, valid}}
403        case _ _: None{}