law rsdp_v2_round_trip

bend-osdev-acpi@0.1.2.0 · LAWS_rsdp.bend:22

import Base
import bend-osdev-word64@0.1.1.1/word64.bend as W
import bend-osdev-bytes@0.1.1.1/bytes.bend as B
import bend-osdev-acpi@0.1.2.0/error.bend as E
import bend-osdev-acpi@0.1.2.0/rsdp.bend as P

22law rsdp_v2_round_trip:
23  for +oem: B.Octets
24  for +oem6: {B.Octets.len(oem) == 6n : Nat}
25  for +rev: U32
26  for +rev8: {B.byte(rev) == rev : U32}
27  for +rev2: {U32.is_lt(rev, 2) == False{} : Bool}
28  for +rsdt: U32
29  for +l: U32
30  for +x: W.W64
31  {P.AcpiRsdp.parse(P.AcpiRsdp.build(P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{l, x}}})) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}