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	# LAWS_checksum.bend, and the whole round trips are LAWS_whole.bend.
19	import Base
20	import bend-osdev-word64@0.1.1.1/word64.bend as W
21	import bend-osdev-bytes@0.1.1.1/bytes.bend as B
22	import ./error.bend as E
23	import ./header.bend as H
24	import ./gas.bend as G
25	import ./hpet.bend as Hp
26	import ./bgrt.bend as Bg
27	import ./facs.bend as Fa
28	import ./rsdt.bend as R
29	import ./mcfg.bend as Mc
30	import ./dsdt.bend as Ds
31	
32	# A Generic Address Structure, at offset len(a) of a ++ encode(g) ++ b
33	law 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
48	law 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
77	law 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
99	law 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)
112	def 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
121	def 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
131	law 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
141	law 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
151	law 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)
162	law 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>}