LAWS.bend
bend-osdev-acpi@0.1.0.0 · 202 lines · 0 definitions
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.
15import Base
16import bend-osdev-word64@0.1.0.0/word64.bend as W
17import bend-osdev-bytes@0.1.0.0/bytes.bend as B
18import bend-osdev-acpi@0.1.0.0/error.bend as E
19import bend-osdev-acpi@0.1.0.0/aml_pkglength.bend as K
20import bend-osdev-acpi@0.1.0.0/aml_name.bend as N
21import bend-osdev-acpi@0.1.0.0/header.bend as H
22import bend-osdev-acpi@0.1.0.0/checksum.bend as C
23import bend-osdev-acpi@0.1.0.0/fields.bend as F
24import bend-osdev-acpi@0.1.0.0/rsdp.bend as P
25import bend-osdev-acpi@0.1.0.0/registry.bend as R
26import bend-osdev-acpi@0.1.0.0/aml_value.bend as V
27import bend-osdev-acpi@0.1.0.0/aml_host.bend as Hs
28import bend-osdev-acpi@0.1.0.0/aml_interp.bend as I
29import bend-osdev-acpi@0.1.0.0/aml.bend as A
30import bend-osdev-acpi@0.1.0.0/aml_term.bend as T
31import bend-osdev-acpi@0.1.0.0/aml_device.bend as Dv
32import bend-osdev-acpi@0.1.0.0/mcfg.bend as Mc
33import bend-osdev-acpi@0.1.0.0/example.bend as X
34
35# The AML encodings (20.2.4, 20.2.2)
36
37law 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
43law 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
51law 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
63law 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
69law 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
76law 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
82law 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
92law 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
97law 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
103law 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
114law 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
117law 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
120law 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
124law check_example:
125 {Result.is_done(&2, &2, E.AcpiError, B.Octets, H.AcpiSdt.check(Mc.AcpiMcfg.build(X.AcpiExample.mcfg()))) == True{} : Bool}
126
127law 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
130law rsdp_example:
131 {Result.is_done(&2, &2, E.AcpiError, P.AcpiRsdp, P.AcpiRsdp.parse(P.AcpiRsdp.build(X.AcpiExample.rsdp()))) == True{} : Bool}
132
133law 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
139law pkglength_63:
140 {B.Octets.hex(K.AmlPkgLength.encode(63)) == "3f" : String}
141
142law pkglength_64:
143 {B.Octets.hex(K.AmlPkgLength.encode(64)) == "4004" : String}
144
145law pkglength_4095:
146 {B.Octets.hex(K.AmlPkgLength.encode(4095)) == "4fff" : String}
147
148law pkglength_4096:
149 {B.Octets.hex(K.AmlPkgLength.encode(4096)) == "800001" : String}
150
151law pkglength_max:
152 {B.Octets.hex(K.AmlPkgLength.encode(268435455)) == "cfffffff" : String}
153
154# bits 5-4 set in a multi-byte form
155law 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
160law name_dual:
161 {B.Octets.hex(N.AmlName.encode(N.AmlName.of_text("\\_SB.PCI0"))) == "5c2e5f53425f50434930" : String}
162
163law name_multi:
164 {B.Octets.hex(N.AmlName.encode(N.AmlName.of_text("\\_SB.PCI0.LPCB"))) == "5c2f035f53425f504349304c504342" : String}
165
166law name_parents:
167 {B.Octets.hex(N.AmlName.encode(N.AmlName.of_text("^^_STA"))) == "5e5e5f535441" : String}
168
169law name_root:
170 {B.Octets.hex(N.AmlName.encode(N.AmlName.of_text("\\"))) == "5c00" : String}
171
172law 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)
177law eisaid_power_button:
178 {T.AmlT.eisaid_value("PNP0C0C") == 202166337 : U32}
179
180law 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
186law aml_name_hid:
187 {B.Octets.hex(T.AmlT.encode1(T.AmlT.name("_HID", T.AmlT.eisaid("PNP0C0C")))) == "085f4849440c41d00c0c" : String}
188
189law 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
193law checksum_built:
194 {C.AcpiChecksum.ok(Mc.AcpiMcfg.build(X.AcpiExample.mcfg())) == True{} : Bool}
195
196law 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
201law 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>}