law rsdp_v1_round_trip

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

import Base
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

13law rsdp_v1_round_trip:
14  for +oem: B.Octets
15  for +oem6: {B.Octets.len(oem) == 6n : Nat}
16  for +rev: U32
17  for +rev8: {B.byte(rev) == rev : U32}
18  for +rev2: {U32.is_lt(rev, 2) == True{} : Bool}
19  for +rsdt: U32
20  {P.AcpiRsdp.parse(P.AcpiRsdp.build(P.AcpiRsdp{oem, rev, rsdt, None{}})) == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}