def mask_len

bend-osdev-crypto@0.1.0.0 · PROOF.bend:476

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B

476def mask_len(xs: List<&2, U32>) -> {B.len(B.mask(xs)) == B.len(xs) : Nat}:
477  match xs:
478    case Nil{}:
479      {==}
480    case Con{h, t}:
481      %mask_len(t) : {B.len(B.mask(Con{h, t})) == 1n+_ : Nat}
482      {==}