def w8s_to_of

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

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

166def w8s_to_of(xs: List<&2, U32>) -> {B.w8s.to_list(B.w8s.of_list(xs)) == B.mask(xs) : List<&2, U32>}:
167  match xs:
168    case Nil{}:
169      {==}
170    case Con{h, t}:
171      %w8s_to_of(t) : {Con{B.oct.to(B.oct.of(h)), B.w8s.to_list(B.w8s.of_list(t))} == Con{B.byte(h), _} : List<&2, U32>}
172      %oct_byte(h) : {Con{B.oct.to(B.oct.of(h)), B.w8s.to_list(B.w8s.of_list(t))} == Con{_, B.w8s.to_list(B.w8s.of_list(t))} : List<&2, U32>}
173      {==}