def olen_of

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

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

141# the length of a list made Octets
142def olen_of(+xs: List<&2, U32>) -> {B.len(xs) == B.Octets.len(B.Octets.of_list(xs)) : Nat}:
143  %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(xs)), B.len(B.Octets.to_list(B.Octets.of_list(xs))), BL.octets_len_list(B.Octets.of_list(xs))) : {B.len(xs) == _ : Nat}
144  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(xs)), B.mask(xs), BL.octets_to_of(xs)) : {B.len(xs) == B.len(_) : Nat}
145  mask_len(xs)