def aes_hex_mask_bytes_length

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

import Base

663def aes_hex_mask_bytes_length(+bytes: List<&2, U32>) ->
664    {List.length(&2, U32, aes_hex_mask_bytes(bytes)) ==
665     List.length(&2, U32, bytes) : Nat}:
666    match bytes:
667        case Nil{}: {==}
668        case byte <> tail:
669            Equal.cong(Nat, Nat, n => 1n+n,
670                List.length(&2, U32, aes_hex_mask_bytes(tail)),
671                List.length(&2, U32, tail), aes_hex_mask_bytes_length(tail))