law sdt_round_trip

bend-osdev-acpi@0.1.2.0 · LAWS_whole.bend:33

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/header.bend as H

33# Any table: its header and body back
34law sdt_round_trip:
35  for +h: H.AcpiHeader
36  for +sig4: {B.Octets.len(H.AcpiHeader.signature(h)) == 4n : Nat}
37  for +oem6: {B.Octets.len(H.AcpiHeader.oem_id(h)) == 6n : Nat}
38  for +tid8: {B.Octets.len(H.AcpiHeader.oem_table_id(h)) == 8n : Nat}
39  for +cid4: {B.Octets.len(H.AcpiHeader.creator_id(h)) == 4n : Nat}
40  for +rev8: {B.byte(H.AcpiHeader.revision(h)) == H.AcpiHeader.revision(h) : U32}
41  for +body: B.Octets
42  for +z: U32
43  for +fit: {Nat.is_le(B.Octets.len(H.AcpiSdt.build(h, body)), U32.to_nat(z)) == True{} : Bool}
44  {H.AcpiSdt.parse(H.AcpiSdt.build(h, body)) == Done{H.AcpiSdt{acpilaw.written(H.AcpiHeader.signature(h), h, H.AcpiSdt.build(h, body)), body}} : Result<&2, &2, E.AcpiError, H.AcpiSdt>}