law hpet_round_trip

bend-osdev-acpi@0.1.1.0 · LAWS_tables.bend:47

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W
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
import bend-osdev-acpi@0.1.1.0/gas.bend as G
import bend-osdev-acpi@0.1.1.0/hpet.bend as Hp

47# The HPET table's body, read back with any header h
48law hpet_round_trip:
49  for +h: H.AcpiHeader
50  for +sig4: {B.Octets.len(H.AcpiHeader.signature(h)) == 4n : Nat}
51  for +oem6: {B.Octets.len(H.AcpiHeader.oem_id(h)) == 6n : Nat}
52  for +tid8: {B.Octets.len(H.AcpiHeader.oem_table_id(h)) == 8n : Nat}
53  for +cid4: {B.Octets.len(H.AcpiHeader.creator_id(h)) == 4n : Nat}
54  for +h0: H.AcpiHeader
55  for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat}
56  for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat}
57  for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat}
58  for +id: U32
59  for +gs: U32
60  for +gw: U32
61  for +go: U32
62  for +ga: U32
63  for +gaddr: W.W64
64  for +n: U32
65  for +m: U32
66  for +p: U32
67  for +gs8: {B.byte(gs) == gs : U32}
68  for +gw8: {B.byte(gw) == gw : U32}
69  for +go8: {B.byte(go) == go : U32}
70  for +ga8: {B.byte(ga) == ga : U32}
71  for +n8: {B.byte(n) == n : U32}
72  for +m16: {B.low16(m) == m : U32}
73  for +p8: {B.byte(p) == p : U32}
74  {Hp.AcpiHpet.of_sdt(H.AcpiSdt{h, B.Octets.drop(36n, Hp.AcpiHpet.build(Hp.AcpiHpet{h0, id, G.AcpiGas{gs, gw, go, ga, gaddr}, n, m, p}))}) == Done{Hp.AcpiHpet{h, id, G.AcpiGas{gs, gw, go, ga, gaddr}, n, m, p}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}