def mask_segs

bend-osdev-acpi@0.1.1.0 · PROOF.bend:2021

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

2021def mask_segs(+ss: List<&2, B.Octets>) -> {N.nm.segs.list(ss) == B.mask(N.nm.segs.list(ss)) : List<&2, U32>}:
2022  match ss:
2023    case Nil{}:
2024      {==}
2025    case Con{s, t}:
2026      %mask_app(B.Octets.to_list(s), N.nm.segs.list(t)) : {B.append(B.Octets.to_list(s), N.nm.segs.list(t)) == _ : List<&2, U32>}
2027      %mask_tl(s) : {B.append(B.Octets.to_list(s), N.nm.segs.list(t)) == B.append(_, B.mask(N.nm.segs.list(t))) : List<&2, U32>}
2028      %mask_segs(t) : {B.append(B.Octets.to_list(s), N.nm.segs.list(t)) == B.append(B.Octets.to_list(s), _) : List<&2, U32>}
2029      {==}