law header_round_trip

bend-osdev-acpi@0.1.1.0 · LAWS.bend:51

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-acpi@0.1.1.0/error.bend as E
import bend-osdev-acpi@0.1.1.0/header.bend as H

51law header_round_trip:
52  for +h: H.AcpiHeader
53  for +sig4: {B.Octets.len(H.AcpiHeader.signature(h)) == 4n : Nat}
54  for +oem6: {B.Octets.len(H.AcpiHeader.oem_id(h)) == 6n : Nat}
55  for +tid8: {B.Octets.len(H.AcpiHeader.oem_table_id(h)) == 8n : Nat}
56  for +cid4: {B.Octets.len(H.AcpiHeader.creator_id(h)) == 4n : Nat}
57  for +rev8: {B.byte(H.AcpiHeader.revision(h)) == H.AcpiHeader.revision(h) : U32}
58  for +ck8: {B.byte(H.AcpiHeader.checksum(h)) == H.AcpiHeader.checksum(h) : U32}
59  {H.AcpiHeader.decode(H.AcpiHeader.encode(h)) == Done{h} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}