1	# Properties, for every input:
2	#   - the AML encodings read back as written: a PkgLength below 2^28, and a
3	#     NameString of NameSegs (at most 255, not rooted and going up at once),
4	#     whatever follows them;
5	#   - a system description table header reads back as written, when its
6	#     text fields have their sizes and its byte fields are bytes;
7	#   - every table accepted sums to zero modulo 256: what AcpiSdt.check
8	#     answers, and every table AcpiTable.parse reads through any registry;
9	#     the RSDP's first 20 bytes, and all its bytes for revision 2;
10	#   - the interpreter never takes more steps than its bound, nor do loading
11	#     a definition block and evaluating an object.
12	# Witnesses that every hypothesis can hold, then vectors: the boundaries
13	# of PkgLength, NameStrings of each form, EISA IDs and AML encodings from
14	# the specification's examples, checksums, and a method evaluated.
15	import Base
16	import bend-osdev-word64@0.1.1.0/word64.bend as W
17	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
18	import ./error.bend as E
19	import ./aml_pkglength.bend as K
20	import ./aml_name.bend as N
21	import ./header.bend as H
22	import ./checksum.bend as C
23	import ./fields.bend as F
24	import ./rsdp.bend as P
25	import ./registry.bend as R
26	import ./aml_value.bend as V
27	import ./aml_host.bend as Hs
28	import ./aml_interp.bend as I
29	import ./aml.bend as A
30	import ./aml_term.bend as T
31	import ./aml_device.bend as Dv
32	import ./mcfg.bend as Mc
33	import ./example.bend as X
34	
35	# The AML encodings (20.2.4, 20.2.2)
36	
37	law pkglength_round_trip:
38	  for +v: U32
39	  for +rest: B.Octets
40	  for +fits: {K.AmlPkgLength.fits(v) == True{} : Bool}
41	  {K.AmlPkgLength.decode(B.Octets.append(K.AmlPkgLength.encode(v), rest)) == Done{K.AmlPkgLen{v, rest}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}
42	
43	law namestring_round_trip:
44	  for +n: N.AmlName
45	  for +rest: B.Octets
46	  for +ok: {N.AmlName.valid(n) == True{} : Bool}
47	  {N.AmlName.decode(B.Octets.append(N.AmlName.encode(n), rest)) == Done{N.AmlNameParsed{n, rest}} : Result<&2, &2, E.AcpiError, N.AmlNameParsed>}
48	
49	# The table header (5.2.6)
50	
51	law header_round_trip:
52	  for +h: H.AcpiHeader
53	  for +sig4: {B.Octets.len(H.AcpiHeader.signature(h)) == 4n : Nat}
54	  for +oem6: {B.Octets.len(H.AcpiHeader.oem_id(h)) == 6n : Nat}
55	  for +tid8: {B.Octets.len(H.AcpiHeader.oem_table_id(h)) == 8n : Nat}
56	  for +cid4: {B.Octets.len(H.AcpiHeader.creator_id(h)) == 4n : Nat}
57	  for +rev8: {B.byte(H.AcpiHeader.revision(h)) == H.AcpiHeader.revision(h) : U32}
58	  for +ck8: {B.byte(H.AcpiHeader.checksum(h)) == H.AcpiHeader.checksum(h) : U32}
59	  {H.AcpiHeader.decode(H.AcpiHeader.encode(h)) == Done{h} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
60	
61	# Checksums: every table accepted sums to zero modulo 256
62	
63	law sdt_check_sums:
64	  for +o: B.Octets
65	  for +raw: B.Octets
66	  for +e: {H.AcpiSdt.check(o) == Done{raw} : Result<&2, &2, E.AcpiError, B.Octets>}
67	  {C.AcpiChecksum.ok(raw) == True{} : Bool}
68	
69	law table_checksums:
70	  for +reg: R.AcpiRegistry
71	  for +o: B.Octets
72	  for +t: R.AcpiTable<R.AcpiNoExt>
73	  for +e: {R.AcpiTable.parse(reg, o) == Done{t} : Result<&2, &2, E.AcpiError, R.AcpiTable<R.AcpiNoExt>>}
74	  {C.AcpiChecksum.ok(H.AcpiSdt.bytes(o)) == True{} : Bool}
75	
76	law rsdp_checksum:
77	  for +o: B.Octets
78	  for +r: P.AcpiRsdp
79	  for +e: {P.AcpiRsdp.parse(o) == Done{r} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
80	  {C.AcpiChecksum.ok(B.Octets.take(20n, o)) == True{} : Bool}
81	
82	law rsdp_ext_checksum:
83	  for +o: B.Octets
84	  for +r: P.AcpiRsdp
85	  for +e: {P.AcpiRsdp.parse(o) == Done{r} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
86	  {C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}
87	
88	# The interpreter never takes more steps than its bound, whatever the
89	# machine (a step reads one opcode or gives one value), and so neither does
90	# loading a definition block or evaluating an object
91	
92	law run_steps_bound:
93	  for +n: Nat
94	  for +m: I.AmlMachine<Hs.AmlMemHost>
95	  {Nat.is_le(I.AmlRun.steps(Hs.AmlMemHost, I.AmlM.run(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, n, m)), n) == True{} : Bool}
96	
97	law load_steps_bound:
98	  for +s: A.AmlSystem<Hs.AmlMemHost>
99	  for +aml: B.Octets
100	  for +n: Nat
101	  {Nat.is_le(A.AmlOutcome.steps(Hs.AmlMemHost, A.Aml.load(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, s, aml, n)), n) == True{} : Bool}
102	
103	law eval_steps_bound:
104	  for +s: A.AmlSystem<Hs.AmlMemHost>
105	  for +p: String
106	  for +args: List<&2, V.AmlValue>
107	  for +n: Nat
108	  {Nat.is_le(A.AmlOutcome.steps(Hs.AmlMemHost, A.Aml.eval(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, s, p, args, n)), n) == True{} : Bool}
109	
110	# Satisfiability witnesses: each hypothesis above holds for an ordinary
111	# input, so no law is vacuous. The first three are the laws themselves at
112	# an example, their hypotheses proved by computation.
113	
114	law pkglength_example:
115	  {K.AmlPkgLength.decode(B.Octets.append(K.AmlPkgLength.encode(1000), B.Octets.of_string("AML"))) == Done{K.AmlPkgLen{1000, B.Octets.of_string("AML")}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}
116	
117	law namestring_example:
118	  {N.AmlName.decode(B.Octets.append(N.AmlName.encode(N.AmlName.of_text("\\_SB.PCI0.LPCB")), B.Octets.of_string("x"))) == Done{N.AmlNameParsed{N.AmlName.of_text("\\_SB.PCI0.LPCB"), B.Octets.of_string("x")}} : Result<&2, &2, E.AcpiError, N.AmlNameParsed>}
119	
120	law header_example:
121	  {H.AcpiHeader.decode(H.AcpiHeader.encode(X.ex.hdr("APIC", 5))) == Done{X.ex.hdr("APIC", 5)} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
122	
123	# the checks pass for a table and an RSDP of each revision
124	law check_example:
125	  {Result.is_done(&2, &2, E.AcpiError, B.Octets, H.AcpiSdt.check(Mc.AcpiMcfg.build(X.AcpiExample.mcfg()))) == True{} : Bool}
126	
127	law parse_example:
128	  {Result.is_done(&2, &2, E.AcpiError, R.AcpiTable<R.AcpiNoExt>, R.AcpiTable.parse(R.AcpiRegistry.default(), Mc.AcpiMcfg.build(X.AcpiExample.mcfg()))) == True{} : Bool}
129	
130	law rsdp_example:
131	  {Result.is_done(&2, &2, E.AcpiError, P.AcpiRsdp, P.AcpiRsdp.parse(P.AcpiRsdp.build(X.AcpiExample.rsdp()))) == True{} : Bool}
132	
133	law rsdp_v1_example:
134	  {Result.is_done(&2, &2, E.AcpiError, P.AcpiRsdp, P.AcpiRsdp.parse(P.AcpiRsdp.build(P.AcpiRsdp{B.Octets.of_string("BENDOS"), 0, 4096, None{}}))) == True{} : Bool}
135	
136	# Vectors
137	
138	# PkgLength (20.2.4): the boundaries of the four forms
139	law pkglength_63:
140	  {B.Octets.hex(K.AmlPkgLength.encode(63)) == "3f" : String}
141	
142	law pkglength_64:
143	  {B.Octets.hex(K.AmlPkgLength.encode(64)) == "4004" : String}
144	
145	law pkglength_4095:
146	  {B.Octets.hex(K.AmlPkgLength.encode(4095)) == "4fff" : String}
147	
148	law pkglength_4096:
149	  {B.Octets.hex(K.AmlPkgLength.encode(4096)) == "800001" : String}
150	
151	law pkglength_max:
152	  {B.Octets.hex(K.AmlPkgLength.encode(268435455)) == "cfffffff" : String}
153	
154	# bits 5-4 set in a multi-byte form
155	law pkglength_reserved:
156	  {K.AmlPkgLength.decode(B.Octets.of_list([112, 0])) == Fail{E.AcpiAmlBadPkgLength{}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}
157	
158	# NameString (20.2.2): a DualNamePath, a MultiNamePath, parent prefixes,
159	# the root alone (NullName), and a segment that is not a NameSeg
160	law name_dual:
161	  {B.Octets.hex(N.AmlName.encode(N.AmlName.of_text("\\_SB.PCI0"))) == "5c2e5f53425f50434930" : String}
162	
163	law name_multi:
164	  {B.Octets.hex(N.AmlName.encode(N.AmlName.of_text("\\_SB.PCI0.LPCB"))) == "5c2f035f53425f504349304c504342" : String}
165	
166	law name_parents:
167	  {B.Octets.hex(N.AmlName.encode(N.AmlName.of_text("^^_STA"))) == "5e5e5f535441" : String}
168	
169	law name_root:
170	  {B.Octets.hex(N.AmlName.encode(N.AmlName.of_text("\\"))) == "5c00" : String}
171	
172	law name_bad_seg:
173	  {N.AmlName.decode(B.Octets.of_string("1ABC")) == Fail{E.AcpiAmlBadName{}} : Result<&2, &2, E.AcpiError, N.AmlNameParsed>}
174	
175	# EISAID (chapter 19, the ASL operator), with the IDs of the examples of
176	# 6.1.5 (the power button) and 6.1.2 (a PCI root bridge's compatible ID)
177	law eisaid_power_button:
178	  {T.AmlT.eisaid_value("PNP0C0C") == 202166337 : U32}
179	
180	law eisaid_pci:
181	  {Dv.AmlEisaId.text(51040321) == "PNP0A03" : String}
182	
183	# AML encodings (20.2.5.2, DefName; 20.2.5.2, DefMethod; 20.2.5.3,
184	# DefReturn): Name (_HID, EISAID ("PNP0C0C")) and
185	# Method (_STA) { Return (0x0F) }, as ASL compilers write them
186	law aml_name_hid:
187	  {B.Octets.hex(T.AmlT.encode1(T.AmlT.name("_HID", T.AmlT.eisaid("PNP0C0C")))) == "085f4849440c41d00c0c" : String}
188	
189	law aml_method_sta:
190	  {B.Octets.hex(T.AmlT.encode1(T.AmlT.method("_STA", 0n, False{}, [T.AmlT.ret(T.AmlT.int32(15))]))) == "14095f53544100a40a0f" : String}
191	
192	# Checksums: a table built here sums to zero; one byte changed, it does not
193	law checksum_built:
194	  {C.AcpiChecksum.ok(Mc.AcpiMcfg.build(X.AcpiExample.mcfg())) == True{} : Bool}
195	
196	law checksum_broken:
197	  {C.AcpiChecksum.ok(B.Octets.append(Mc.AcpiMcfg.build(X.AcpiExample.mcfg()), B.Octets.of_list([1]))) == False{} : Bool}
198	
199	# the interpreter: Method (_STA) { Return (0x0F) } loaded at the root, and
200	# called
201	law aml_eval_sta:
202	  {A.AmlOutcome.result(Hs.AmlMemHost, A.Aml.eval_mem(A.AmlSystem.after(Hs.AmlMemHost, A.Aml.mem_system(True{}), A.Aml.load_mem(A.Aml.mem_system(True{}), T.AmlT.encode([T.AmlT.method("_STA", 0n, False{}, [T.AmlT.ret(T.AmlT.int32(15))])]), 100n)), "\\_STA", Nil{}, 100n)) == Done{V.AmlInt{W.W64.from_u32(15)}} : Result<&2, &2, E.AcpiError, V.AmlValue>}