def p_octets_to_of

bend-osdev-bytes@0.1.1.0 · PROOF.bend:365

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

365def p_octets_to_of(+xs: List<&2, U32>) -> {B.Octets.to_list(B.Octets.of_list(xs)) == B.mask(xs) : List<&2, U32>}:
366  %F_to(B.w8s.of_list.fast(xs)) : {_ == B.mask(xs) : List<&2, U32>}
367  %F_of(xs) : {B.w8s.to_list(_) == B.mask(xs) : List<&2, U32>}
368  w8s_to_of(xs)