def aes_masked_size_is_some

qasim-bend-kit@0.1.0.2 · proof/AES_EnvelopeProof.bend:744

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

744def aes_masked_size_is_some(+bytes: List<&2, U32>, +expected: Nat,
745    size: {List.length(&2, U32, bytes) == expected : Nat}) ->
746    {Maybe.is_some(&0,
747        {List.length(&2, U32, aes_hex_mask_bytes(bytes)) == expected : Nat},
748        AES.aes_nat_eq_proof(
749            List.length(&2, U32, aes_hex_mask_bytes(bytes)), expected)) ==
750        True{} : Bool}:
751    aes_nat_eq_is_some(
752        List.length(&2, U32, aes_hex_mask_bytes(bytes)),
753        expected,
754        Equal.trans(Nat,
755            List.length(&2, U32, aes_hex_mask_bytes(bytes)),
756            List.length(&2, U32, bytes), expected,
757            aes_hex_mask_bytes_length(bytes), size))