def mask_len

bend-osdev-aead@0.1.0.0 · PROOF.bend:133

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

133def mask_len(xs: List<&2, U32>) -> {B.len(xs) == B.len(B.mask(xs)) : Nat}:
134  match xs:
135    case Nil{}:
136      {==}
137    case Con{h, t}:
138      %mask_len(t) : {1n+B.len(t) == 1n+_ : Nat}
139      {==}