AESEnvelopeProof.aes_masked_size_is_some: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend as AESEnvelopeProof
Lines 744-757 of qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&start_line=744&end_line=757

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

def aes_masked_size_is_some(+bytes: List<&2, U32>, +expected: Nat,
    size: {List.length(&2, U32, bytes) == expected : Nat}) ->
    {Maybe.is_some(&0,
        {List.length(&2, U32, aes_hex_mask_bytes(bytes)) == expected : Nat},
        AES.aes_nat_eq_proof(
            List.length(&2, U32, aes_hex_mask_bytes(bytes)), expected)) ==
        True{} : Bool}:
    aes_nat_eq_is_some(
        List.length(&2, U32, aes_hex_mask_bytes(bytes)),
        expected,
        Equal.trans(Nat,
            List.length(&2, U32, aes_hex_mask_bytes(bytes)),
            List.length(&2, U32, bytes), expected,
            aes_hex_mask_bytes_length(bytes), size))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.is_some
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=aes_nat_eq_proof
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_hex_mask_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_hex_mask_bytes_length
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_nat_eq_is_some