LAWS_whole.bend
bend-osdev-acpi@0.1.2.0 · 141 lines · 0 definitions
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).
13import Base
14import bend-osdev-word64@0.1.1.1/word64.bend as W
15import bend-osdev-bytes@0.1.1.1/bytes.bend as B
16import bend-osdev-acpi@0.1.2.0/error.bend as E
17import bend-osdev-acpi@0.1.2.0/header.bend as H
18import bend-osdev-acpi@0.1.2.0/gas.bend as G
19import bend-osdev-acpi@0.1.2.0/hpet.bend as Hp
20import bend-osdev-acpi@0.1.2.0/bgrt.bend as Bg
21import bend-osdev-acpi@0.1.2.0/rsdt.bend as R
22import bend-osdev-acpi@0.1.2.0/mcfg.bend as Mc
23import bend-osdev-acpi@0.1.2.0/dsdt.bend as Ds
24import bend-osdev-acpi@0.1.2.0/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
28def 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
34law 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
47law 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
72law 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
90law 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
102law 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
114law 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)
126law 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
140law 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}