LAWS_tables.bend

bend-osdev-acpi@0.1.1.0 · 170 lines · 10 definitions

1# The structures inside the tables, for every input: each reads back as it
2# is written.
3#
4#   - a Generic Address Structure at any offset of any bytes (5.2.3.2);
5#   - the body that AcpiHpet.build and AcpiBgrt.build write (everything
6#     after the 36-byte header) is read back by of_sdt, whatever header it
7#     is read with, when the text fields of the headers have their sizes,
8#     byte fields are bytes and 16-bit fields fit 16 bits;
9#   - the same for the XSDT's entries, the RSDT's (each address's low 32
10#     bits, which is what an RSDT entry holds), the MCFG's structures (each
11#     segment's low 16 bits and each bus number's low 8 bits), and a DSDT's
12#     or SSDT's definition block;
13#   - a FACS reads back through AcpiFacs.parse (it has no header and no
14#     checksum), its Length being the 64 that build writes.
15#
16# A table's whole round trip, parse(build(t)), also needs build's checksum
17# byte to make the bytes sum to zero modulo 256, for every content; that is
18# not proved (README, Laws).
19import Base
20import bend-osdev-word64@0.1.1.0/word64.bend as W
21import bend-osdev-bytes@0.1.1.0/bytes.bend as B
22import bend-osdev-acpi@0.1.1.0/error.bend as E
23import bend-osdev-acpi@0.1.1.0/header.bend as H
24import bend-osdev-acpi@0.1.1.0/gas.bend as G
25import bend-osdev-acpi@0.1.1.0/hpet.bend as Hp
26import bend-osdev-acpi@0.1.1.0/bgrt.bend as Bg
27import bend-osdev-acpi@0.1.1.0/facs.bend as Fa
28import bend-osdev-acpi@0.1.1.0/rsdt.bend as R
29import bend-osdev-acpi@0.1.1.0/mcfg.bend as Mc
30import bend-osdev-acpi@0.1.1.0/dsdt.bend as Ds
31
32# A Generic Address Structure, at offset len(a) of a ++ encode(g) ++ b
33law gas_round_trip:
34  for +a: B.Octets
35  for +s: U32
36  for +w: U32
37  for +off: U32
38  for +acc: U32
39  for +addr: W.W64
40  for +b: B.Octets
41  for +s8: {B.byte(s) == s : U32}
42  for +w8: {B.byte(w) == w : U32}
43  for +off8: {B.byte(off) == off : U32}
44  for +acc8: {B.byte(acc) == acc : U32}
45  {G.AcpiGas.at(B.Octets.append(a, B.Octets.append(G.AcpiGas.encode(G.AcpiGas{s, w, off, acc, addr}), b)), B.Octets.len(a)) == G.AcpiGas{s, w, off, acc, addr} : G.AcpiGas}
46
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>}
75
76# The BGRT table's body, read back with any header h
77law bgrt_round_trip:
78  for +h: H.AcpiHeader
79  for +sig4: {B.Octets.len(H.AcpiHeader.signature(h)) == 4n : Nat}
80  for +oem6: {B.Octets.len(H.AcpiHeader.oem_id(h)) == 6n : Nat}
81  for +tid8: {B.Octets.len(H.AcpiHeader.oem_table_id(h)) == 8n : Nat}
82  for +cid4: {B.Octets.len(H.AcpiHeader.creator_id(h)) == 4n : Nat}
83  for +h0: H.AcpiHeader
84  for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat}
85  for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat}
86  for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat}
87  for +v: U32
88  for +st: U32
89  for +it: U32
90  for +a: W.W64
91  for +x: U32
92  for +y: U32
93  for +v16: {B.low16(v) == v : U32}
94  for +st8: {B.byte(st) == st : U32}
95  for +it8: {B.byte(it) == it : U32}
96  {Bg.AcpiBgrt.of_sdt(H.AcpiSdt{h, B.Octets.drop(36n, Bg.AcpiBgrt.build(Bg.AcpiBgrt{h0, v, st, it, a, x, y}))}) == Done{Bg.AcpiBgrt{h, v, st, it, a, x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
97
98# The FACS: parsed back as built, with the Length 64 that build writes
99law facs_round_trip:
100  for +l: U32
101  for +hs: U32
102  for +wv: U32
103  for +gl: U32
104  for +fl: U32
105  for +xw: W.W64
106  for +v: U32
107  for +of: U32
108  for +v8: {B.byte(v) == v : U32}
109  {Fa.AcpiFacs.parse(Fa.AcpiFacs.build(Fa.AcpiFacs{l, hs, wv, gl, fl, xw, v, of})) == Done{Fa.AcpiFacs{64, hs, wv, gl, fl, xw, v, of}} : Result<&2, &2, E.AcpiError, Fa.AcpiFacs>}
110
111# the low 32 bits of each address, as a W64 (what an RSDT entry holds)
112def acpilaw.low32(xs: List<&2, W.W64>) -> List<&2, W.W64>:
113  match xs:
114    case Nil{}:
115      Nil{}
116    case Con{x, t}:
117      Con{W.W64.from_u32(W.W64.lo(x)), acpilaw.low32(t)}
118
119# each MCFG structure as it is stored: the segment group's low 16 bits, the
120# bus numbers' low 8 bits
121def acpilaw.mcfg_fit(es: List<&2, Mc.AcpiMcfgEntry>) -> List<&2, Mc.AcpiMcfgEntry>:
122  match es:
123    case Nil{}:
124      Nil{}
125    case Con{e, t}:
126      match e:
127        case Mc.AcpiMcfgEntry{b, s, lo, hi}:
128          Con{Mc.AcpiMcfgEntry{b, B.low16(s), B.byte(lo), B.byte(hi)}, acpilaw.mcfg_fit(t)}
129
130# The XSDT's entries, read back with any header h
131law xsdt_round_trip:
132  for +h: H.AcpiHeader
133  for +h0: H.AcpiHeader
134  for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat}
135  for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat}
136  for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat}
137  for +xs: List<&2, W.W64>
138  {R.AcpiXsdt.of_sdt(H.AcpiSdt{h, B.Octets.drop(36n, R.AcpiXsdt.build(h0, xs))}) == Done{R.AcpiSdtList{h, xs}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
139
140# The RSDT's entries: each address's low 32 bits
141law rsdt_round_trip:
142  for +h: H.AcpiHeader
143  for +h0: H.AcpiHeader
144  for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat}
145  for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat}
146  for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat}
147  for +xs: List<&2, W.W64>
148  {R.AcpiRsdt.of_sdt(H.AcpiSdt{h, B.Octets.drop(36n, R.AcpiRsdt.build(h0, xs))}) == Done{R.AcpiSdtList{h, acpilaw.low32(xs)}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
149
150# The MCFG's allocation structures, as stored
151law mcfg_round_trip:
152  for +h: H.AcpiHeader
153  for +h0: H.AcpiHeader
154  for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat}
155  for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat}
156  for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat}
157  for +es: List<&2, Mc.AcpiMcfgEntry>
158  {Mc.AcpiMcfg.of_sdt(H.AcpiSdt{h, B.Octets.drop(36n, Mc.AcpiMcfg.build(Mc.AcpiMcfg{h0, es}))}) == Done{Mc.AcpiMcfg{h, acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
159
160# A DSDT's or SSDT's definition block (the header's signature is kept, so
161# it too must have its size)
162law aml_round_trip:
163  for +h: H.AcpiHeader
164  for +h0: H.AcpiHeader
165  for +sig4b: {B.Octets.len(H.AcpiHeader.signature(h0)) == 4n : Nat}
166  for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat}
167  for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat}
168  for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat}
169  for +a: B.Octets
170  {Ds.AcpiAml.of_sdt(H.AcpiSdt{h, B.Octets.drop(36n, Ds.AcpiAml.build(Ds.AcpiAml{h0, a}))}) == Done{Ds.AcpiAml{h, a}} : Result<&2, &2, E.AcpiError, Ds.AcpiAml>}