law hpet_whole

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

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/header.bend as H
import bend-osdev-acpi@0.1.2.0/gas.bend as G
import bend-osdev-acpi@0.1.2.0/hpet.bend as Hp

46# The HPET table
47law hpet_whole:
48  for +h0: H.AcpiHeader
49  for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat}
50  for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat}
51  for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat}
52  for +rev8b: {B.byte(H.AcpiHeader.revision(h0)) == H.AcpiHeader.revision(h0) : U32}
53  for +id: U32
54  for +gs: U32
55  for +gw: U32
56  for +go: U32
57  for +ga: U32
58  for +gaddr: W.W64
59  for +n: U32
60  for +m: U32
61  for +p: U32
62  for +gs8: {B.byte(gs) == gs : U32}
63  for +gw8: {B.byte(gw) == gw : U32}
64  for +go8: {B.byte(go) == go : U32}
65  for +ga8: {B.byte(ga) == ga : U32}
66  for +n8: {B.byte(n) == n : U32}
67  for +m16: {B.low16(m) == m : U32}
68  for +p8: {B.byte(p) == p : U32}
69  {Hp.AcpiHpet.parse(Hp.AcpiHpet.build(Hp.AcpiHpet{h0, id, G.AcpiGas{gs, gw, go, ga, gaddr}, n, m, p})) == Done{Hp.AcpiHpet{acpilaw.written(B.Octets.of_string("HPET"), h0, Hp.AcpiHpet.build(Hp.AcpiHpet{h0, id, G.AcpiGas{gs, gw, go, ga, gaddr}, n, m, p})), id, G.AcpiGas{gs, gw, go, ga, gaddr}, n, m, p}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}