1	# The whole round trips, for every input: a table AcpiSdt.build writes is
2	# read back by AcpiSdt.parse, its checks passing (Length from 36 to the
3	# bytes given, the bytes summing to zero modulo 256: LAWS_checksum.bend),
4	# and so is each table whose body LAWS_tables.bend reads back, through its
5	# parse: the HPET, BGRT, XSDT, RSDT, MCFG and a DSDT or SSDT.
6	#
7	# The header read back is the header given with the fields build computes:
8	# the signature build writes, the Length (the table's length) and the
9	# Checksum (the byte at offset 9 of the table). The text fields must have
10	# their sizes and the revision must be a byte, and the table's length must
11	# fit the 32-bit Length field (no more than a U32's value; the HPET and the
12	# BGRT are 56 bytes long, so their laws need no such hypothesis).
13	import Base
14	import bend-osdev-word64@0.1.1.1/word64.bend as W
15	import bend-osdev-bytes@0.1.1.1/bytes.bend as B
16	import ./error.bend as E
17	import ./header.bend as H
18	import ./gas.bend as G
19	import ./hpet.bend as Hp
20	import ./bgrt.bend as Bg
21	import ./rsdt.bend as R
22	import ./mcfg.bend as Mc
23	import ./dsdt.bend as Ds
24	import ./LAWS_tables.bend as TL
25	
26	# the header h with the signature sig and the fields build computes for the
27	# table o: Length the length of o, Checksum the byte at offset 9 of o
28	def acpilaw.written(sig: B.Octets, h: H.AcpiHeader, +o: B.Octets) -> H.AcpiHeader:
29	  match h:
30	    case H.AcpiHeader{s, l, r, c, oi, t, orv, ci, cr}:
31	      H.AcpiHeader{sig, U32.from_nat(B.Octets.len(o)), r, Maybe.default(&2, U32, B.Octets.at(o, 9n), 0), oi, t, orv, ci, cr}
32	
33	# Any table: its header and body back
34	law 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>}
45	
46	# The HPET table
47	law 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>}
70	
71	# The BGRT table
72	law bgrt_whole:
73	  for +h0: H.AcpiHeader
74	  for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat}
75	  for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat}
76	  for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat}
77	  for +rev8b: {B.byte(H.AcpiHeader.revision(h0)) == H.AcpiHeader.revision(h0) : U32}
78	  for +v: U32
79	  for +st: U32
80	  for +it: U32
81	  for +a: W.W64
82	  for +x: U32
83	  for +y: U32
84	  for +v16: {B.low16(v) == v : U32}
85	  for +st8: {B.byte(st) == st : U32}
86	  for +it8: {B.byte(it) == it : U32}
87	  {Bg.AcpiBgrt.parse(Bg.AcpiBgrt.build(Bg.AcpiBgrt{h0, v, st, it, a, x, y})) == Done{Bg.AcpiBgrt{acpilaw.written(B.Octets.of_string("BGRT"), h0, Bg.AcpiBgrt.build(Bg.AcpiBgrt{h0, v, st, it, a, x, y})), v, st, it, a, x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
88	
89	# The XSDT
90	law xsdt_whole:
91	  for +h0: H.AcpiHeader
92	  for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat}
93	  for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat}
94	  for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat}
95	  for +rev8b: {B.byte(H.AcpiHeader.revision(h0)) == H.AcpiHeader.revision(h0) : U32}
96	  for +xs: List<&2, W.W64>
97	  for +z: U32
98	  for +fit: {Nat.is_le(B.Octets.len(R.AcpiXsdt.build(h0, xs)), U32.to_nat(z)) == True{} : Bool}
99	  {R.AcpiXsdt.parse(R.AcpiXsdt.build(h0, xs)) == Done{R.AcpiSdtList{acpilaw.written(B.Octets.of_string("XSDT"), h0, R.AcpiXsdt.build(h0, xs)), xs}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
100	
101	# The RSDT: each address's low 32 bits
102	law rsdt_whole:
103	  for +h0: H.AcpiHeader
104	  for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat}
105	  for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat}
106	  for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat}
107	  for +rev8b: {B.byte(H.AcpiHeader.revision(h0)) == H.AcpiHeader.revision(h0) : U32}
108	  for +xs: List<&2, W.W64>
109	  for +z: U32
110	  for +fit: {Nat.is_le(B.Octets.len(R.AcpiRsdt.build(h0, xs)), U32.to_nat(z)) == True{} : Bool}
111	  {R.AcpiRsdt.parse(R.AcpiRsdt.build(h0, xs)) == Done{R.AcpiSdtList{acpilaw.written(B.Octets.of_string("RSDT"), h0, R.AcpiRsdt.build(h0, xs)), TL.acpilaw.low32(xs)}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
112	
113	# The MCFG: its allocation structures as stored
114	law mcfg_whole:
115	  for +h0: H.AcpiHeader
116	  for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat}
117	  for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat}
118	  for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat}
119	  for +rev8b: {B.byte(H.AcpiHeader.revision(h0)) == H.AcpiHeader.revision(h0) : U32}
120	  for +es: List<&2, Mc.AcpiMcfgEntry>
121	  for +z: U32
122	  for +fit: {Nat.is_le(B.Octets.len(Mc.AcpiMcfg.build(Mc.AcpiMcfg{h0, es})), U32.to_nat(z)) == True{} : Bool}
123	  {Mc.AcpiMcfg.parse(Mc.AcpiMcfg.build(Mc.AcpiMcfg{h0, es})) == Done{Mc.AcpiMcfg{acpilaw.written(B.Octets.of_string("MCFG"), h0, Mc.AcpiMcfg.build(Mc.AcpiMcfg{h0, es})), TL.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
124	
125	# A DSDT or SSDT (AcpiAml.parse, which takes either signature)
126	law aml_whole:
127	  for +h0: H.AcpiHeader
128	  for +sig4b: {B.Octets.len(H.AcpiHeader.signature(h0)) == 4n : Nat}
129	  for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat}
130	  for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat}
131	  for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat}
132	  for +rev8b: {B.byte(H.AcpiHeader.revision(h0)) == H.AcpiHeader.revision(h0) : U32}
133	  for +a: B.Octets
134	  for +z: U32
135	  for +fit: {Nat.is_le(B.Octets.len(Ds.AcpiAml.build(Ds.AcpiAml{h0, a})), U32.to_nat(z)) == True{} : Bool}
136	  {Ds.AcpiAml.parse(Ds.AcpiAml.build(Ds.AcpiAml{h0, a})) == Done{Ds.AcpiAml{acpilaw.written(H.AcpiHeader.signature(h0), h0, Ds.AcpiAml.build(Ds.AcpiAml{h0, a})), a}} : Result<&2, &2, E.AcpiError, Ds.AcpiAml>}
137	
138	# the hypotheses hold at an example: a header AcpiHeader.make fits, and a
139	# 39-byte table
140	law whole_example:
141	  {(B.Octets.len(H.AcpiHeader.signature(H.AcpiHeader.make(B.Octets.of_string("SSDT"), 2, B.Octets.of_string("BEND"), B.Octets.of_string("TABLE")))), B.Octets.len(H.AcpiHeader.oem_id(H.AcpiHeader.make(B.Octets.of_string("SSDT"), 2, B.Octets.of_string("BEND"), B.Octets.of_string("TABLE")))), B.Octets.len(H.AcpiHeader.oem_table_id(H.AcpiHeader.make(B.Octets.of_string("SSDT"), 2, B.Octets.of_string("BEND"), B.Octets.of_string("TABLE")))), B.Octets.len(H.AcpiHeader.creator_id(H.AcpiHeader.make(B.Octets.of_string("SSDT"), 2, B.Octets.of_string("BEND"), B.Octets.of_string("TABLE")))), B.byte(H.AcpiHeader.revision(H.AcpiHeader.make(B.Octets.of_string("SSDT"), 2, B.Octets.of_string("BEND"), B.Octets.of_string("TABLE")))), Nat.is_le(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader.make(B.Octets.of_string("SSDT"), 2, B.Octets.of_string("BEND"), B.Octets.of_string("TABLE")), B.Octets.of_list([1, 2, 3]))), U32.to_nat(39))) == (4n, 6n, 8n, 4n, 2, True{}) : Nat & Nat & Nat & Nat & U32 & Bool}