PROOF_tables.bend

bend-osdev-acpi@0.1.1.0 · 521 lines · 59 definitions

1import Base
2import bend-osdev-word64@0.1.1.0/word64.bend as W
3import bend-osdev-bytes@0.1.1.0/bytes.bend as B
4import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL
5import bend-osdev-bytes@0.1.1.0/PROOF.bend as BP
6import bend-osdev-word64@0.1.1.0/LAWS.bend as WL
7import bend-osdev-word64@0.1.1.0/PROOF.bend as WP
8import bend-osdev-acpi@0.1.1.0/error.bend as E
9import bend-osdev-acpi@0.1.1.0/header.bend as H
10import bend-osdev-acpi@0.1.1.0/checksum.bend as C
11import bend-osdev-acpi@0.1.1.0/fields.bend as F
12import bend-osdev-acpi@0.1.1.0/gas.bend as G
13import bend-osdev-acpi@0.1.1.0/hpet.bend as Hp
14import bend-osdev-acpi@0.1.1.0/bgrt.bend as Bg
15import bend-osdev-acpi@0.1.1.0/facs.bend as Fa
16import bend-osdev-acpi@0.1.1.0/rsdt.bend as R
17import bend-osdev-acpi@0.1.1.0/mcfg.bend as Mc
18import bend-osdev-acpi@0.1.1.0/dsdt.bend as Ds
19import bend-osdev-acpi@0.1.1.0/LAWS_tables.bend as Laws
20import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
21import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
22
23# Lemmas are mostly stated as {value == expression}, the direction a rewrite
24# needs: %e : P replaces the expression (marked _ in P) by the value.
25#
26# The fields of a structure are read by bytes' laws for fields at offsets
27# inside joined bytes, or, where every 16-, 32- and 64-bit field is split
28# into its bits, by computing (as bytes' own proofs do); a W64 is split
29# through word64's parts_of (from_parts of its halves), and from_parts and
30# le64 then compute through word64's definitions.
31
32# The Generic Address Structure: its byte fields from the 4 bytes in front,
33# its address from the le64 after them
34
35def tb.gas_b(+a: B.Octets, +q: B.Octets, +r: B.Octets, +k: Nat, +hk: {Nat.is_lt(k, B.Octets.len(q)) == True{} : Bool}) -> {B.Octets.at(q, k) == B.Octets.at(B.Octets.append(a, B.Octets.append(q, r)), Nat.add(B.Octets.len(a), k)) : Maybe<&2, U32>}:
36  Equal.trans(Maybe<&2, U32>, B.Octets.at(q, k), B.Octets.at(B.Octets.append(q, r), k), B.Octets.at(B.Octets.append(a, B.Octets.append(q, r)), Nat.add(B.Octets.len(a), k)), Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(q, r), k), B.Octets.at(q, k), BL.octets_at_append_lt(q, r, k, hk)), Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(a, B.Octets.append(q, r)), Nat.add(B.Octets.len(a), k)), B.Octets.at(B.Octets.append(q, r), k), BL.octets_at_append_add(a, B.Octets.append(q, r), k)))
37
38def tb.l64(+v: W.W64) -> {Nat.is_le(8n, B.Octets.len(B.Octets.le64(v))) == True{} : Bool}:
39  %Equal.sym(Nat, B.Octets.len(B.Octets.le64(v)), 8n, BL.octets_len_le64(v)) : {Nat.is_le(8n, _) == True{} : Bool}
40  {==}
41
42def tb.gas_a(+a: B.Octets, +s: U32, +w: U32, +off: U32, +acc: U32, +addr: W.W64, +b: B.Octets) -> {Some{addr} == B.Octets.le64_at(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n)) : Maybe<&2, W.W64>}:
43  Equal.sym(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n)), Some{addr}, Equal.trans(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n)), B.Octets.le64_at(B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b)), 4n), Some{addr}, BL.octets_le64_at_append_add(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b)), 4n), Equal.trans(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b)), 4n), B.Octets.le64_at(B.Octets.append(B.Octets.le64(addr), b), 0n), Some{addr}, BL.octets_le64_at_append_add(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b), 0n), Equal.trans(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(B.Octets.le64(addr), b), 0n), B.Octets.le64_at(B.Octets.le64(addr), 0n), Some{addr}, BL.octets_le64_at_append_le(B.Octets.le64(addr), b, 0n, tb.l64(addr)), BL.octets_le64_round_trip(addr)))))
44
45def Laws.gas_round_trip(a, s, w, off, acc, addr, b, s8, w8, off8, acc8):
46  %Equal.sym(B.Octets, B.Octets.append(B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.le64(addr)), b), B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b)), BL.octets_append_assoc(B.Octets.of_list([s, w, off, acc]), B.Octets.le64(addr), b)) : {G.AcpiGas.at(B.Octets.append(a, _), B.Octets.len(a)) == G.AcpiGas{s, w, off, acc, addr} : G.AcpiGas}
47  %UL.nat_add_zero(B.Octets.len(a)) : {G.AcpiGas{F.AcpiF.u8(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), _), F.AcpiF.u8(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 1n)), F.AcpiF.u8(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 2n)), F.AcpiF.u8(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 3n)), F.AcpiF.u64(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n))} == G.AcpiGas{s, w, off, acc, addr} : G.AcpiGas}
48  %tb.gas_b(a, B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b), 0n, {==}) : {G.AcpiGas{Maybe.default(&2, U32, _, 0), F.AcpiF.u8(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 1n)), F.AcpiF.u8(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 2n)), F.AcpiF.u8(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 3n)), F.AcpiF.u64(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n))} == G.AcpiGas{s, w, off, acc, addr} : G.AcpiGas}
49  %tb.gas_b(a, B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b), 1n, {==}) : {G.AcpiGas{B.byte(s), Maybe.default(&2, U32, _, 0), F.AcpiF.u8(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 2n)), F.AcpiF.u8(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 3n)), F.AcpiF.u64(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n))} == G.AcpiGas{s, w, off, acc, addr} : G.AcpiGas}
50  %tb.gas_b(a, B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b), 2n, {==}) : {G.AcpiGas{B.byte(s), B.byte(w), Maybe.default(&2, U32, _, 0), F.AcpiF.u8(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 3n)), F.AcpiF.u64(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n))} == G.AcpiGas{s, w, off, acc, addr} : G.AcpiGas}
51  %tb.gas_b(a, B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b), 3n, {==}) : {G.AcpiGas{B.byte(s), B.byte(w), B.byte(off), Maybe.default(&2, U32, _, 0), F.AcpiF.u64(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n))} == G.AcpiGas{s, w, off, acc, addr} : G.AcpiGas}
52  %tb.gas_a(a, s, w, off, acc, addr, b) : {G.AcpiGas{B.byte(s), B.byte(w), B.byte(off), B.byte(acc), Maybe.default(&2, W.W64, _, W.W64.zero())} == G.AcpiGas{s, w, off, acc, addr} : G.AcpiGas}
53  %s8 : {G.AcpiGas{B.byte(s), B.byte(w), B.byte(off), B.byte(acc), addr} == G.AcpiGas{_, w, off, acc, addr} : G.AcpiGas}
54  %w8 : {G.AcpiGas{B.byte(s), B.byte(w), B.byte(off), B.byte(acc), addr} == G.AcpiGas{B.byte(s), _, off, acc, addr} : G.AcpiGas}
55  %off8 : {G.AcpiGas{B.byte(s), B.byte(w), B.byte(off), B.byte(acc), addr} == G.AcpiGas{B.byte(s), B.byte(w), _, acc, addr} : G.AcpiGas}
56  %acc8 : {G.AcpiGas{B.byte(s), B.byte(w), B.byte(off), B.byte(acc), addr} == G.AcpiGas{B.byte(s), B.byte(w), B.byte(off), _, addr} : G.AcpiGas}
57  {==}
58
59# The FACS: with every word split into its bits, parsing computes
60
61def tb.facs_bits(+l: U32, +hs: U32, +wv: U32, +gl: U32, +fl: U32, +ah: U32, +al: U32, +v: U32, +of: U32) -> {Fa.AcpiFacs.parse(Fa.AcpiFacs.build(Fa.AcpiFacs{l, hs, wv, gl, fl, W.W64.from_parts(ah, al), v, of})) == Done{Fa.AcpiFacs{64, hs, wv, gl, fl, W.W64.from_parts(ah, al), B.byte(v), of}} : Result<&2, &2, E.AcpiError, Fa.AcpiFacs>}:
62  match hs wv gl fl ah al of:
63    case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{d0, WCon{d1, WCon{d2, WCon{d3, WCon{d4, WCon{d5, WCon{d6, WCon{d7, WCon{d8, WCon{d9, WCon{d10, WCon{d11, WCon{d12, WCon{d13, WCon{d14, WCon{d15, WCon{d16, WCon{d17, WCon{d18, WCon{d19, WCon{d20, WCon{d21, WCon{d22, WCon{d23, WCon{d24, WCon{d25, WCon{d26, WCon{d27, WCon{d28, WCon{d29, WCon{d30, WCon{d31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{e0, WCon{e1, WCon{e2, WCon{e3, WCon{e4, WCon{e5, WCon{e6, WCon{e7, WCon{e8, WCon{e9, WCon{e10, WCon{e11, WCon{e12, WCon{e13, WCon{e14, WCon{e15, WCon{e16, WCon{e17, WCon{e18, WCon{e19, WCon{e20, WCon{e21, WCon{e22, WCon{e23, WCon{e24, WCon{e25, WCon{e26, WCon{e27, WCon{e28, WCon{e29, WCon{e30, WCon{e31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{f0, WCon{f1, WCon{f2, WCon{f3, WCon{f4, WCon{f5, WCon{f6, WCon{f7, WCon{f8, WCon{f9, WCon{f10, WCon{f11, WCon{f12, WCon{f13, WCon{f14, WCon{f15, WCon{f16, WCon{f17, WCon{f18, WCon{f19, WCon{f20, WCon{f21, WCon{f22, WCon{f23, WCon{f24, WCon{f25, WCon{f26, WCon{f27, WCon{f28, WCon{f29, WCon{f30, WCon{f31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{g0, WCon{g1, WCon{g2, WCon{g3, WCon{g4, WCon{g5, WCon{g6, WCon{g7, WCon{g8, WCon{g9, WCon{g10, WCon{g11, WCon{g12, WCon{g13, WCon{g14, WCon{g15, WCon{g16, WCon{g17, WCon{g18, WCon{g19, WCon{g20, WCon{g21, WCon{g22, WCon{g23, WCon{g24, WCon{g25, WCon{g26, WCon{g27, WCon{g28, WCon{g29, WCon{g30, WCon{g31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
64      {==}
65
66def Laws.facs_round_trip(l, hs, wv, gl, fl, xw, v, of, v8):
67  %WL.parts_of(xw) : {Fa.AcpiFacs.parse(Fa.AcpiFacs.build(Fa.AcpiFacs{l, hs, wv, gl, fl, _, v, of})) == Done{Fa.AcpiFacs{64, hs, wv, gl, fl, _, v, of}} : Result<&2, &2, E.AcpiError, Fa.AcpiFacs>}
68  %v8 : {Fa.AcpiFacs.parse(Fa.AcpiFacs.build(Fa.AcpiFacs{l, hs, wv, gl, fl, W.W64.from_parts(W.W64.hi(xw), W.W64.lo(xw)), v, of})) == Done{Fa.AcpiFacs{64, hs, wv, gl, fl, W.W64.from_parts(W.W64.hi(xw), W.W64.lo(xw)), _, of}} : Result<&2, &2, E.AcpiError, Fa.AcpiFacs>}
69  tb.facs_bits(l, hs, wv, gl, fl, W.W64.hi(xw), W.W64.lo(xw), v, of)
70
71# A table built by AcpiSdt.build: its header is 36 bytes (when its text
72# fields have their sizes), the checksum byte replaces byte 9, and the bytes
73# after the header are the body as given
74
75def tb.la(+a: B.Octets, +b: B.Octets) -> {Nat.add(B.Octets.len(a), B.Octets.len(b)) == B.Octets.len(B.Octets.append(a, b)) : Nat}:
76  Equal.sym(Nat, B.Octets.len(B.Octets.append(a, b)), Nat.add(B.Octets.len(a), B.Octets.len(b)), BL.octets_len_append(a, b))
77
78def tb.elen(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}) -> {B.Octets.len(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr})) == 36n : Nat}:
79  %tb.la(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))))) : {_ == 36n : Nat}
80  %Equal.sym(Nat, B.Octets.len(s), 4n, sig4) : {Nat.add(_, B.Octets.len(B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))))) == 36n : Nat}
81  %tb.la(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))) : {Nat.add(4n, _) == 36n : Nat}
82  %Equal.sym(Nat, B.Octets.len(B.Octets.le32(l)), 4n, BL.octets_len_le32(l)) : {Nat.add(4n, Nat.add(_, B.Octets.len(B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))))) == 36n : Nat}
83  %tb.la(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))) : {Nat.add(8n, _) == 36n : Nat}
84  %tb.la(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))) : {Nat.add(9n, _) == 36n : Nat}
85  %tb.la(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))) : {Nat.add(10n, _) == 36n : Nat}
86  %Equal.sym(Nat, B.Octets.len(o), 6n, oem6) : {Nat.add(10n, Nat.add(_, B.Octets.len(B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))) == 36n : Nat}
87  %tb.la(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))) : {Nat.add(16n, _) == 36n : Nat}
88  %Equal.sym(Nat, B.Octets.len(t), 8n, tid8) : {Nat.add(16n, Nat.add(_, B.Octets.len(B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))) == 36n : Nat}
89  %tb.la(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))) : {Nat.add(24n, _) == 36n : Nat}
90  %Equal.sym(Nat, B.Octets.len(B.Octets.le32(orv)), 4n, BL.octets_len_le32(orv)) : {Nat.add(24n, Nat.add(_, B.Octets.len(B.Octets.append(ci, B.Octets.le32(cr))))) == 36n : Nat}
91  %tb.la(ci, B.Octets.le32(cr)) : {Nat.add(28n, _) == 36n : Nat}
92  %Equal.sym(Nat, B.Octets.len(ci), 4n, cid4) : {Nat.add(28n, Nat.add(_, B.Octets.len(B.Octets.le32(cr)))) == 36n : Nat}
93  %Equal.sym(Nat, B.Octets.len(B.Octets.le32(cr)), 4n, BL.octets_len_le32(cr)) : {Nat.add(32n, _) == 36n : Nat}
94  {==}
95
96def tb.lenchk(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +body: B.Octets) -> {Nat.add(36n, B.Octets.len(body)) == B.Octets.len(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body)) : Nat}:
97  %tb.elen(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4) : {Nat.add(_, B.Octets.len(body)) == B.Octets.len(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body)) : Nat}
98  tb.la(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body)
99
100def tb.r8(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +body: B.Octets, +k: Nat) -> {F.AcpiF.u8(body, k) == F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, k)) : U32}:
101  %tb.elen(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4) : {F.AcpiF.u8(body, k) == Maybe.default(&2, U32, B.Octets.at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(_, k)), 0) : U32}
102  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(B.Octets.len(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr})), k)), B.Octets.at(body, k), BL.octets_at_append_add(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body, k)) : {F.AcpiF.u8(body, k) == Maybe.default(&2, U32, _, 0) : U32}
103  {==}
104
105def tb.r16(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +body: B.Octets, +k: Nat) -> {F.AcpiF.u16(body, k) == F.AcpiF.u16(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, k)) : U32}:
106  %tb.elen(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4) : {F.AcpiF.u16(body, k) == Maybe.default(&2, U32, B.Octets.le16_at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(_, k)), 0) : U32}
107  %Equal.sym(Maybe<&2, U32>, B.Octets.le16_at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(B.Octets.len(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr})), k)), B.Octets.le16_at(body, k), BL.octets_le16_at_append_add(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body, k)) : {F.AcpiF.u16(body, k) == Maybe.default(&2, U32, _, 0) : U32}
108  {==}
109
110def tb.r32(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +body: B.Octets, +k: Nat) -> {F.AcpiF.u32(body, k) == F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, k)) : U32}:
111  %tb.elen(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4) : {F.AcpiF.u32(body, k) == Maybe.default(&2, U32, B.Octets.le32_at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(_, k)), 0) : U32}
112  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(B.Octets.len(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr})), k)), B.Octets.le32_at(body, k), BL.octets_le32_at_append_add(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body, k)) : {F.AcpiF.u32(body, k) == Maybe.default(&2, U32, _, 0) : U32}
113  {==}
114
115def tb.r64(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +body: B.Octets, +k: Nat) -> {F.AcpiF.u64(body, k) == F.AcpiF.u64(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, k)) : W.W64}:
116  %tb.elen(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4) : {F.AcpiF.u64(body, k) == Maybe.default(&2, W.W64, B.Octets.le64_at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(_, k)), W.W64.zero()) : W.W64}
117  %Equal.sym(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(B.Octets.len(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr})), k)), B.Octets.le64_at(body, k), BL.octets_le64_at_append_add(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body, k)) : {F.AcpiF.u64(body, k) == Maybe.default(&2, W.W64, _, W.W64.zero()) : W.W64}
118  {==}
119
120def tb.rgas(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +body: B.Octets, +k: Nat) -> {G.AcpiGas.at(body, k) == G.AcpiGas.at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, k)) : G.AcpiGas}:
121  %tb.r8(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body, k) : {G.AcpiGas.at(body, k) == G.AcpiGas{_, F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, Nat.add(k, 1n))), F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, Nat.add(k, 2n))), F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, Nat.add(k, 3n))), F.AcpiF.u64(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, Nat.add(k, 4n)))} : G.AcpiGas}
122  %tb.r8(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body, Nat.add(k, 1n)) : {G.AcpiGas.at(body, k) == G.AcpiGas{F.AcpiF.u8(body, k), _, F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, Nat.add(k, 2n))), F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, Nat.add(k, 3n))), F.AcpiF.u64(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, Nat.add(k, 4n)))} : G.AcpiGas}
123  %tb.r8(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body, Nat.add(k, 2n)) : {G.AcpiGas.at(body, k) == G.AcpiGas{F.AcpiF.u8(body, k), F.AcpiF.u8(body, Nat.add(k, 1n)), _, F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, Nat.add(k, 3n))), F.AcpiF.u64(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, Nat.add(k, 4n)))} : G.AcpiGas}
124  %tb.r8(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body, Nat.add(k, 3n)) : {G.AcpiGas.at(body, k) == G.AcpiGas{F.AcpiF.u8(body, k), F.AcpiF.u8(body, Nat.add(k, 1n)), F.AcpiF.u8(body, Nat.add(k, 2n)), _, F.AcpiF.u64(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), Nat.add(36n, Nat.add(k, 4n)))} : G.AcpiGas}
125  %tb.r64(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body, Nat.add(k, 4n)) : {G.AcpiGas.at(body, k) == G.AcpiGas{F.AcpiF.u8(body, k), F.AcpiF.u8(body, Nat.add(k, 1n)), F.AcpiF.u8(body, Nat.add(k, 2n)), F.AcpiF.u8(body, Nat.add(k, 3n)), _} : G.AcpiGas}
126  {==}
127
128def tb.h9(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +body: B.Octets) -> {Nat.is_le(9n, B.Octets.len(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))) == True{} : Bool}:
129  %tb.lenchk(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body) : {Nat.is_le(9n, _) == True{} : Bool}
130  {==}
131
132def tb.e36(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +body: B.Octets) -> {Nat.add(B.Octets.len(B.Octets.take(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))), 27n) == 36n : Nat}:
133  %Equal.sym(Nat, B.Octets.len(B.Octets.take(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))), 9n, BL.octets_len_take_le(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body), tb.h9(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body))) : {Nat.add(_, 27n) == 36n : Nat}
134  {==}
135
136def tb.e0(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +body: B.Octets) -> {Nat.add(B.Octets.len(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr})), 0n) == 36n : Nat}:
137  %Equal.sym(Nat, B.Octets.len(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr})), 36n, tb.elen(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr, sig4, oem6, tid8, cid4)) : {Nat.add(_, 0n) == 36n : Nat}
138  {==}
139
140def tb.sdt_body(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +body: B.Octets) -> {body == B.Octets.drop(36n, H.AcpiSdt.build(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, body)) : B.Octets}:
141  %tb.lenchk(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body) : {body == B.Octets.drop(36n, C.ck.fix.pick(Nat.is_lt(9n, _), 9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))) : B.Octets}
142  %Equal.sym(B.Octets, B.Octets.concat([B.Octets.take(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.append(B.Octets.take(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), B.Octets.concat([B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))])), BL.octets_concat_cons(B.Octets.take(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), [B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))])) : {body == B.Octets.drop(36n, _) : B.Octets}
143  %Equal.sym(B.Octets, B.Octets.concat([B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.concat([B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))])), BL.octets_concat_cons(B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), [B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))])) : {body == B.Octets.drop(36n, B.Octets.append(B.Octets.take(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), _)) : B.Octets}
144  %Equal.sym(B.Octets, B.Octets.concat([B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.append(B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), B.Octets.concat(Nil{})), BL.octets_concat_cons(B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), Nil{})) : {body == B.Octets.drop(36n, B.Octets.append(B.Octets.take(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), _))) : B.Octets}
145  %Equal.sym(B.Octets, B.Octets.concat(Nil{}), B.Octets.empty(), BL.octets_concat_nil()) : {body == B.Octets.drop(36n, B.Octets.append(B.Octets.take(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.append(B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), _)))) : B.Octets}
146  %Equal.sym(B.Octets, B.Octets.append(B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), B.Octets.empty()), B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), BL.octets_append_empty_r(B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)))) : {body == B.Octets.drop(36n, B.Octets.append(B.Octets.take(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), _))) : B.Octets}
147  %tb.e36(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body) : {body == B.Octets.drop(_, B.Octets.append(B.Octets.take(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))))) : B.Octets}
148  %Equal.sym(B.Octets, B.Octets.drop(Nat.add(B.Octets.len(B.Octets.take(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))), 27n), B.Octets.append(B.Octets.take(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))))), B.Octets.drop(27n, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)))), BL.octets_drop_append_add(B.Octets.take(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), 27n, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))))) : {body == _ : B.Octets}
149  %Equal.sym(B.Octets, B.Octets.drop(Nat.add(B.Octets.len(B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))])), 26n), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)))), B.Octets.drop(26n, B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))), BL.octets_drop_append_add(B.Octets.of_list([C.AcpiChecksum.byte_for(9n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))]), 26n, B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)))) : {body == _ : B.Octets}
150  %Equal.sym(B.Octets, B.Octets.drop(26n, B.Octets.drop(10n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))), B.Octets.drop(Nat.add(10n, 26n), B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), BL.octets_drop_drop(10n, 26n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body))) : {body == _ : B.Octets}
151  %tb.e0(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body) : {body == B.Octets.drop(_, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)) : B.Octets}
152  %Equal.sym(B.Octets, B.Octets.drop(Nat.add(B.Octets.len(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr})), 0n), B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), body)), B.Octets.drop(0n, body), BL.octets_drop_append_add(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr}), 0n, body)) : {body == _ : B.Octets}
153  %Equal.sym(B.Octets, B.Octets.drop(0n, body), body, BL.octets_drop_zero(body)) : {body == _ : B.Octets}
154  {==}
155
156# The HPET and BGRT bodies: the header skipped by bytes' laws (tb.r8 ...),
157# then, with every 16-, 32- and 64-bit field split into its bits, the reads
158# computed
159
160def tb.hp_len(+id: U32, +gs: U32, +gw: U32, +go: U32, +ga: U32, +ah: U32, +al: U32, +n: U32, +m: U32, +p: U32) -> {56n == Nat.add(36n, B.Octets.len(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]))) : Nat}:
161  match id ah al m:
162    case U32{WCon{id0, WCon{id1, WCon{id2, WCon{id3, WCon{id4, WCon{id5, WCon{id6, WCon{id7, WCon{id8, WCon{id9, WCon{id10, WCon{id11, WCon{id12, WCon{id13, WCon{id14, WCon{id15, WCon{id16, WCon{id17, WCon{id18, WCon{id19, WCon{id20, WCon{id21, WCon{id22, WCon{id23, WCon{id24, WCon{id25, WCon{id26, WCon{id27, WCon{id28, WCon{id29, WCon{id30, WCon{id31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{ah0, WCon{ah1, WCon{ah2, WCon{ah3, WCon{ah4, WCon{ah5, WCon{ah6, WCon{ah7, WCon{ah8, WCon{ah9, WCon{ah10, WCon{ah11, WCon{ah12, WCon{ah13, WCon{ah14, WCon{ah15, WCon{ah16, WCon{ah17, WCon{ah18, WCon{ah19, WCon{ah20, WCon{ah21, WCon{ah22, WCon{ah23, WCon{ah24, WCon{ah25, WCon{ah26, WCon{ah27, WCon{ah28, WCon{ah29, WCon{ah30, WCon{ah31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{al0, WCon{al1, WCon{al2, WCon{al3, WCon{al4, WCon{al5, WCon{al6, WCon{al7, WCon{al8, WCon{al9, WCon{al10, WCon{al11, WCon{al12, WCon{al13, WCon{al14, WCon{al15, WCon{al16, WCon{al17, WCon{al18, WCon{al19, WCon{al20, WCon{al21, WCon{al22, WCon{al23, WCon{al24, WCon{al25, WCon{al26, WCon{al27, WCon{al28, WCon{al29, WCon{al30, WCon{al31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{m0, WCon{m1, WCon{m2, WCon{m3, WCon{m4, WCon{m5, WCon{m6, WCon{m7, WCon{m8, WCon{m9, WCon{m10, WCon{m11, WCon{m12, WCon{m13, WCon{m14, WCon{m15, WCon{m16, WCon{m17, WCon{m18, WCon{m19, WCon{m20, WCon{m21, WCon{m22, WCon{m23, WCon{m24, WCon{m25, WCon{m26, WCon{m27, WCon{m28, WCon{m29, WCon{m30, WCon{m31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
163      {==}
164
165def tb.hp_vals(+h: H.AcpiHeader, +id: U32, +gs: U32, +gw: U32, +go: U32, +ga: U32, +ah: U32, +al: U32, +n: U32, +m: U32, +p: U32) -> {Done{Hp.AcpiHpet{h, F.AcpiF.u32(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 0n), G.AcpiGas.at(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 4n), F.AcpiF.u8(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 16n), F.AcpiF.u16(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 17n), F.AcpiF.u8(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 19n)}} == Done{Hp.AcpiHpet{h, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}:
166  match id ah al m:
167    case U32{WCon{id0, WCon{id1, WCon{id2, WCon{id3, WCon{id4, WCon{id5, WCon{id6, WCon{id7, WCon{id8, WCon{id9, WCon{id10, WCon{id11, WCon{id12, WCon{id13, WCon{id14, WCon{id15, WCon{id16, WCon{id17, WCon{id18, WCon{id19, WCon{id20, WCon{id21, WCon{id22, WCon{id23, WCon{id24, WCon{id25, WCon{id26, WCon{id27, WCon{id28, WCon{id29, WCon{id30, WCon{id31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{ah0, WCon{ah1, WCon{ah2, WCon{ah3, WCon{ah4, WCon{ah5, WCon{ah6, WCon{ah7, WCon{ah8, WCon{ah9, WCon{ah10, WCon{ah11, WCon{ah12, WCon{ah13, WCon{ah14, WCon{ah15, WCon{ah16, WCon{ah17, WCon{ah18, WCon{ah19, WCon{ah20, WCon{ah21, WCon{ah22, WCon{ah23, WCon{ah24, WCon{ah25, WCon{ah26, WCon{ah27, WCon{ah28, WCon{ah29, WCon{ah30, WCon{ah31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{al0, WCon{al1, WCon{al2, WCon{al3, WCon{al4, WCon{al5, WCon{al6, WCon{al7, WCon{al8, WCon{al9, WCon{al10, WCon{al11, WCon{al12, WCon{al13, WCon{al14, WCon{al15, WCon{al16, WCon{al17, WCon{al18, WCon{al19, WCon{al20, WCon{al21, WCon{al22, WCon{al23, WCon{al24, WCon{al25, WCon{al26, WCon{al27, WCon{al28, WCon{al29, WCon{al30, WCon{al31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{m0, WCon{m1, WCon{m2, WCon{m3, WCon{m4, WCon{m5, WCon{m6, WCon{m7, WCon{m8, WCon{m9, WCon{m10, WCon{m11, WCon{m12, WCon{m13, WCon{m14, WCon{m15, WCon{m16, WCon{m17, WCon{m18, WCon{m19, WCon{m20, WCon{m21, WCon{m22, WCon{m23, WCon{m24, WCon{m25, WCon{m26, WCon{m27, WCon{m28, WCon{m29, WCon{m30, WCon{m31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
168      {==}
169
170def tb.hp(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +id: U32, +gs: U32, +gw: U32, +go: U32, +ga: U32, +ah: U32, +al: U32, +n: U32, +m: U32, +p: U32) -> {Hp.AcpiHpet.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])}) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}:
171  %tb.lenchk(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])) : {Hp.hpet.read(Nat.is_le(56n, _), H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]))) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
172  %tb.hp_len(id, gs, gw, go, ga, ah, al, n, m, p) : {Hp.hpet.read(Nat.is_le(56n, _), H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]))) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
173  %tb.r32(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 0n) : {Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, _, G.AcpiGas.at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 40n), F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 52n), F.AcpiF.u16(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 53n), F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 55n)}} == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
174  %tb.rgas(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 4n) : {Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u32(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 0n), _, F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 52n), F.AcpiF.u16(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 53n), F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 55n)}} == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
175  %tb.r8(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 16n) : {Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u32(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 0n), G.AcpiGas.at(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 4n), _, F.AcpiF.u16(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 53n), F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 55n)}} == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
176  %tb.r16(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 17n) : {Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u32(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 0n), G.AcpiGas.at(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 4n), F.AcpiF.u8(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 16n), _, F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 55n)}} == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
177  %tb.r8(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 19n) : {Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u32(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 0n), G.AcpiGas.at(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 4n), F.AcpiF.u8(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 16n), F.AcpiF.u16(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 17n), _}} == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
178  tb.hp_vals(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, gs, gw, go, ga, ah, al, n, m, p)
179
180def tb.bg_len(+v: U32, +st: U32, +it: U32, +ah: U32, +al: U32, +x: U32, +y: U32) -> {56n == Nat.add(36n, B.Octets.len(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]))) : Nat}:
181  match v ah al x y:
182    case U32{WCon{v0, WCon{v1, WCon{v2, WCon{v3, WCon{v4, WCon{v5, WCon{v6, WCon{v7, WCon{v8, WCon{v9, WCon{v10, WCon{v11, WCon{v12, WCon{v13, WCon{v14, WCon{v15, WCon{v16, WCon{v17, WCon{v18, WCon{v19, WCon{v20, WCon{v21, WCon{v22, WCon{v23, WCon{v24, WCon{v25, WCon{v26, WCon{v27, WCon{v28, WCon{v29, WCon{v30, WCon{v31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{ah0, WCon{ah1, WCon{ah2, WCon{ah3, WCon{ah4, WCon{ah5, WCon{ah6, WCon{ah7, WCon{ah8, WCon{ah9, WCon{ah10, WCon{ah11, WCon{ah12, WCon{ah13, WCon{ah14, WCon{ah15, WCon{ah16, WCon{ah17, WCon{ah18, WCon{ah19, WCon{ah20, WCon{ah21, WCon{ah22, WCon{ah23, WCon{ah24, WCon{ah25, WCon{ah26, WCon{ah27, WCon{ah28, WCon{ah29, WCon{ah30, WCon{ah31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{al0, WCon{al1, WCon{al2, WCon{al3, WCon{al4, WCon{al5, WCon{al6, WCon{al7, WCon{al8, WCon{al9, WCon{al10, WCon{al11, WCon{al12, WCon{al13, WCon{al14, WCon{al15, WCon{al16, WCon{al17, WCon{al18, WCon{al19, WCon{al20, WCon{al21, WCon{al22, WCon{al23, WCon{al24, WCon{al25, WCon{al26, WCon{al27, WCon{al28, WCon{al29, WCon{al30, WCon{al31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x0, WCon{x1, WCon{x2, WCon{x3, WCon{x4, WCon{x5, WCon{x6, WCon{x7, WCon{x8, WCon{x9, WCon{x10, WCon{x11, WCon{x12, WCon{x13, WCon{x14, WCon{x15, WCon{x16, WCon{x17, WCon{x18, WCon{x19, WCon{x20, WCon{x21, WCon{x22, WCon{x23, WCon{x24, WCon{x25, WCon{x26, WCon{x27, WCon{x28, WCon{x29, WCon{x30, WCon{x31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y0, WCon{y1, WCon{y2, WCon{y3, WCon{y4, WCon{y5, WCon{y6, WCon{y7, WCon{y8, WCon{y9, WCon{y10, WCon{y11, WCon{y12, WCon{y13, WCon{y14, WCon{y15, WCon{y16, WCon{y17, WCon{y18, WCon{y19, WCon{y20, WCon{y21, WCon{y22, WCon{y23, WCon{y24, WCon{y25, WCon{y26, WCon{y27, WCon{y28, WCon{y29, WCon{y30, WCon{y31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
183      {==}
184
185def tb.bg_vals(+h: H.AcpiHeader, +v: U32, +st: U32, +it: U32, +ah: U32, +al: U32, +x: U32, +y: U32) -> {Done{Bg.AcpiBgrt{h, F.AcpiF.u16(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 0n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 2n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 3n), F.AcpiF.u64(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 4n), F.AcpiF.u32(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 12n), F.AcpiF.u32(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 16n)}} == Done{Bg.AcpiBgrt{h, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}:
186  match v ah al x y:
187    case U32{WCon{v0, WCon{v1, WCon{v2, WCon{v3, WCon{v4, WCon{v5, WCon{v6, WCon{v7, WCon{v8, WCon{v9, WCon{v10, WCon{v11, WCon{v12, WCon{v13, WCon{v14, WCon{v15, WCon{v16, WCon{v17, WCon{v18, WCon{v19, WCon{v20, WCon{v21, WCon{v22, WCon{v23, WCon{v24, WCon{v25, WCon{v26, WCon{v27, WCon{v28, WCon{v29, WCon{v30, WCon{v31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{ah0, WCon{ah1, WCon{ah2, WCon{ah3, WCon{ah4, WCon{ah5, WCon{ah6, WCon{ah7, WCon{ah8, WCon{ah9, WCon{ah10, WCon{ah11, WCon{ah12, WCon{ah13, WCon{ah14, WCon{ah15, WCon{ah16, WCon{ah17, WCon{ah18, WCon{ah19, WCon{ah20, WCon{ah21, WCon{ah22, WCon{ah23, WCon{ah24, WCon{ah25, WCon{ah26, WCon{ah27, WCon{ah28, WCon{ah29, WCon{ah30, WCon{ah31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{al0, WCon{al1, WCon{al2, WCon{al3, WCon{al4, WCon{al5, WCon{al6, WCon{al7, WCon{al8, WCon{al9, WCon{al10, WCon{al11, WCon{al12, WCon{al13, WCon{al14, WCon{al15, WCon{al16, WCon{al17, WCon{al18, WCon{al19, WCon{al20, WCon{al21, WCon{al22, WCon{al23, WCon{al24, WCon{al25, WCon{al26, WCon{al27, WCon{al28, WCon{al29, WCon{al30, WCon{al31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x0, WCon{x1, WCon{x2, WCon{x3, WCon{x4, WCon{x5, WCon{x6, WCon{x7, WCon{x8, WCon{x9, WCon{x10, WCon{x11, WCon{x12, WCon{x13, WCon{x14, WCon{x15, WCon{x16, WCon{x17, WCon{x18, WCon{x19, WCon{x20, WCon{x21, WCon{x22, WCon{x23, WCon{x24, WCon{x25, WCon{x26, WCon{x27, WCon{x28, WCon{x29, WCon{x30, WCon{x31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y0, WCon{y1, WCon{y2, WCon{y3, WCon{y4, WCon{y5, WCon{y6, WCon{y7, WCon{y8, WCon{y9, WCon{y10, WCon{y11, WCon{y12, WCon{y13, WCon{y14, WCon{y15, WCon{y16, WCon{y17, WCon{y18, WCon{y19, WCon{y20, WCon{y21, WCon{y22, WCon{y23, WCon{y24, WCon{y25, WCon{y26, WCon{y27, WCon{y28, WCon{y29, WCon{y30, WCon{y31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
188      {==}
189
190def tb.bg(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +v: U32, +st: U32, +it: U32, +ah: U32, +al: U32, +x: U32, +y: U32) -> {Bg.AcpiBgrt.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])}) == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}:
191  %tb.lenchk(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])) : {Bg.bgrt.read(Nat.is_le(56n, _), H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]))) == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
192  %tb.bg_len(v, st, it, ah, al, x, y) : {Bg.bgrt.read(Nat.is_le(56n, _), H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]))) == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
193  %tb.r16(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 0n) : {Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, _, F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 38n), F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 39n), F.AcpiF.u64(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 40n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 48n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 52n)}} == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
194  %tb.r8(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 2n) : {Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u16(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 0n), _, F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 39n), F.AcpiF.u64(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 40n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 48n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 52n)}} == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
195  %tb.r8(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 3n) : {Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u16(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 0n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 2n), _, F.AcpiF.u64(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 40n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 48n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 52n)}} == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
196  %tb.r64(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 4n) : {Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u16(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 0n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 2n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 3n), _, F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 48n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 52n)}} == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
197  %tb.r32(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 12n) : {Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u16(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 0n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 2n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 3n), F.AcpiF.u64(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 4n), _, F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 52n)}} == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
198  %tb.r32(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 16n) : {Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u16(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 0n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 2n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 3n), F.AcpiF.u64(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 4n), F.AcpiF.u32(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 12n), _}} == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
199  tb.bg_vals(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, v, st, it, ah, al, x, y)
200
201def Laws.hpet_round_trip(h, sig4, oem6, tid8, cid4, h0, oem6b, tid8b, cid4b, id, gs, gw, go, ga, gaddr, n, m, p, gs8, gw8, go8, ga8, n8, m16, p8):
202  match h:
203    case H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
204      match h0:
205        case H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}:
206          %tb.sdt_body(B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0, {==}, oem6b, tid8b, cid4b, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, gaddr}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])) : {Hp.AcpiHpet.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, _}) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{gs, gw, go, ga, gaddr}, n, m, p}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
207          %WL.parts_of(gaddr) : {Hp.AcpiHpet.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, _}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])}) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{gs, gw, go, ga, _}, n, m, p}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
208          %gs8 : {Hp.AcpiHpet.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])}) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{_, gw, go, ga, W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}, n, m, p}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
209          %gw8 : {Hp.AcpiHpet.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])}) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), _, go, ga, W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}, n, m, p}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
210          %go8 : {Hp.AcpiHpet.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])}) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), _, ga, W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}, n, m, p}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
211          %ga8 : {Hp.AcpiHpet.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])}) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), _, W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}, n, m, p}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
212          %n8 : {Hp.AcpiHpet.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])}) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}, _, m, p}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
213          %m16 : {Hp.AcpiHpet.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])}) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}, B.byte(n), _, p}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
214          %p8 : {Hp.AcpiHpet.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])}) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(W.W64.hi(gaddr), W.W64.lo(gaddr))}, B.byte(n), B.low16(m), _}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
215          tb.hp(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, id, gs, gw, go, ga, W.W64.hi(gaddr), W.W64.lo(gaddr), n, m, p)
216
217def Laws.bgrt_round_trip(h, sig4, oem6, tid8, cid4, h0, oem6b, tid8b, cid4b, v, st, it, a, x, y, v16, st8, it8):
218  match h:
219    case H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
220      match h0:
221        case H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}:
222          %tb.sdt_body(B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0, {==}, oem6b, tid8b, cid4b, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(a), B.Octets.le32(x), B.Octets.le32(y)])) : {Bg.AcpiBgrt.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, _}) == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, v, st, it, a, x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
223          %WL.parts_of(a) : {Bg.AcpiBgrt.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(_), B.Octets.le32(x), B.Octets.le32(y)])}) == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, v, st, it, _, x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
224          %v16 : {Bg.AcpiBgrt.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(W.W64.hi(a), W.W64.lo(a))), B.Octets.le32(x), B.Octets.le32(y)])}) == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, _, st, it, W.W64.from_parts(W.W64.hi(a), W.W64.lo(a)), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
225          %st8 : {Bg.AcpiBgrt.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(W.W64.hi(a), W.W64.lo(a))), B.Octets.le32(x), B.Octets.le32(y)])}) == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), _, it, W.W64.from_parts(W.W64.hi(a), W.W64.lo(a)), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
226          %it8 : {Bg.AcpiBgrt.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(W.W64.hi(a), W.W64.lo(a))), B.Octets.le32(x), B.Octets.le32(y)])}) == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), _, W.W64.from_parts(W.W64.hi(a), W.W64.lo(a)), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
227          tb.bg(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, v, st, it, W.W64.hi(a), W.W64.lo(a), x, y)
228
229# Lists of entries: lengths are multiples of the entry size, and Nat's
230# division by it counts them
231
232def gapp_nil(-A: Data, +xs: List<&2, A>) -> {xs == List.append(&2, A, xs, Nil{}) : List<&2, A>}:
233  match xs:
234    case Nil{}:
235      {==}
236    case Con{h, t}:
237      %gapp_nil(A, t) : {Con{h, t} == Con{h, _} : List<&2, A>}
238      {==}
239
240def rev_app(-A: Data, +xs: List<&2, A>, +a: List<&2, A>, +b: List<&2, A>) -> {List.reverse.go(&2, A, a, List.append(&2, A, xs, b)) == List.reverse.go(&2, A, List.reverse.go(&2, A, xs, a), b) : List<&2, A>}:
241  match xs:
242    case Nil{}:
243      {==}
244    case Con{h, t}:
245      rev_app(A, t, Con{h, a}, b)
246
247def revrev(-A: Data, +xs: List<&2, A>) -> {xs == List.reverse(&2, A, List.reverse.go(&2, A, xs, Nil{})) : List<&2, A>}:
248  Equal.trans(List<&2, A>, xs, List.append(&2, A, xs, Nil{}), List.reverse(&2, A, List.reverse.go(&2, A, xs, Nil{})), gapp_nil(A, xs), rev_app(A, xs, Nil{}, Nil{}))
249
250def tb.asr(+x: Nat, +a: Nat) -> {1n+Nat.add(x, a) == Nat.add(x, 1n+a) : Nat}:
251  match x:
252    case 0n:
253      {==}
254    case 1n+p:
255      %tb.asr(p, a) : {1n+1n+Nat.add(p, a) == 1n+_ : Nat}
256      {==}
257
258def tb.srv(+xs: List<&2, W.W64>, +acc: List<&2, W.W64>) -> {List.reverse.go(&2, W.W64, xs, acc) == R.sl.rev(xs, acc) : List<&2, W.W64>}:
259  match xs:
260    case Nil{}:
261      {==}
262    case Con{h, t}:
263      tb.srv(t, Con{h, acc})
264
265def tb.srev(+xs: List<&2, W.W64>) -> {xs == R.sl.rev(R.sl.rev(xs, Nil{}), Nil{}) : List<&2, W.W64>}:
266  %tb.srv(R.sl.rev(xs, Nil{}), Nil{}) : {xs == _ : List<&2, W.W64>}
267  %tb.srv(xs, Nil{}) : {xs == List.reverse.go(&2, W.W64, _, Nil{}) : List<&2, W.W64>}
268  revrev(W.W64, xs)
269
270def tb.dm4(+n: Nat, +d: Nat) -> {Nat.divmod.go(Nat.mul(n, 4n), 3n, d, 0n) == (Nat.add(n, d), 0n) : Nat & Nat}:
271  match n:
272    case 0n:
273      {==}
274    case 1n+p:
275      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.mul(p, 4n), 3n, 1n+d, 0n), (Nat.add(p, 1n+d), 0n), tb.dm4(p, 1n+d)) : {_ == (Nat.add(1n+p, d), 0n) : Nat & Nat}
276      %tb.asr(p, d) : {(_, 0n) == (Nat.add(1n+p, d), 0n) : Nat & Nat}
277      {==}
278
279def tb.dm8(+n: Nat, +d: Nat) -> {Nat.divmod.go(Nat.mul(n, 8n), 7n, d, 0n) == (Nat.add(n, d), 0n) : Nat & Nat}:
280  match n:
281    case 0n:
282      {==}
283    case 1n+p:
284      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.mul(p, 8n), 7n, 1n+d, 0n), (Nat.add(p, 1n+d), 0n), tb.dm8(p, 1n+d)) : {_ == (Nat.add(1n+p, d), 0n) : Nat & Nat}
285      %tb.asr(p, d) : {(_, 0n) == (Nat.add(1n+p, d), 0n) : Nat & Nat}
286      {==}
287
288def tb.dm16(+n: Nat, +d: Nat) -> {Nat.divmod.go(Nat.mul(n, 16n), 15n, d, 0n) == (Nat.add(n, d), 0n) : Nat & Nat}:
289  match n:
290    case 0n:
291      {==}
292    case 1n+p:
293      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.mul(p, 16n), 15n, 1n+d, 0n), (Nat.add(p, 1n+d), 0n), tb.dm16(p, 1n+d)) : {_ == (Nat.add(1n+p, d), 0n) : Nat & Nat}
294      %tb.asr(p, d) : {(_, 0n) == (Nat.add(1n+p, d), 0n) : Nat & Nat}
295      {==}
296
297def tb.xlen(+xs: List<&2, W.W64>) -> {Nat.mul(List.length(&2, W.W64, xs), 8n) == B.Octets.len(B.Octets.concat(R.sl.enc(xs, True{}))) : Nat}:
298  match xs:
299    case Nil{}:
300      {==}
301    case Con{x, t}:
302      %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.le64(x), R.sl.enc(t, True{})}), B.Octets.append(B.Octets.le64(x), B.Octets.concat(R.sl.enc(t, True{}))), BL.octets_concat_cons(B.Octets.le64(x), R.sl.enc(t, True{}))) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 8n) == B.Octets.len(_) : Nat}
303      %tb.la(B.Octets.le64(x), B.Octets.concat(R.sl.enc(t, True{}))) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 8n) == _ : Nat}
304      %Equal.sym(Nat, B.Octets.len(B.Octets.le64(x)), 8n, BL.octets_len_le64(x)) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 8n) == Nat.add(_, B.Octets.len(B.Octets.concat(R.sl.enc(t, True{})))) : Nat}
305      %tb.xlen(t) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 8n) == Nat.add(8n, _) : Nat}
306      {==}
307
308def tb.rlen(+xs: List<&2, W.W64>) -> {Nat.mul(List.length(&2, W.W64, xs), 4n) == B.Octets.len(B.Octets.concat(R.sl.enc(xs, False{}))) : Nat}:
309  match xs:
310    case Nil{}:
311      {==}
312    case Con{x, t}:
313      %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.le32(W.W64.lo(x)), R.sl.enc(t, False{})}), B.Octets.append(B.Octets.le32(W.W64.lo(x)), B.Octets.concat(R.sl.enc(t, False{}))), BL.octets_concat_cons(B.Octets.le32(W.W64.lo(x)), R.sl.enc(t, False{}))) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 4n) == B.Octets.len(_) : Nat}
314      %tb.la(B.Octets.le32(W.W64.lo(x)), B.Octets.concat(R.sl.enc(t, False{}))) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 4n) == _ : Nat}
315      %Equal.sym(Nat, B.Octets.len(B.Octets.le32(W.W64.lo(x))), 4n, BL.octets_len_le32(W.W64.lo(x))) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 4n) == Nat.add(_, B.Octets.len(B.Octets.concat(R.sl.enc(t, False{})))) : Nat}
316      %tb.rlen(t) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 4n) == Nat.add(4n, _) : Nat}
317      {==}
318
319def tb.l32(+v: U32) -> {Nat.is_le(4n, B.Octets.len(B.Octets.le32(v))) == True{} : Bool}:
320  %Equal.sym(Nat, B.Octets.len(B.Octets.le32(v)), 4n, BL.octets_len_le32(v)) : {Nat.is_le(4n, _) == True{} : Bool}
321  {==}
322
323def tb.e8(+v: W.W64) -> {Nat.add(B.Octets.len(B.Octets.le64(v)), 0n) == 8n : Nat}:
324  %Equal.sym(Nat, B.Octets.len(B.Octets.le64(v)), 8n, BL.octets_len_le64(v)) : {Nat.add(_, 0n) == 8n : Nat}
325  {==}
326
327def tb.e4(+v: U32) -> {Nat.add(B.Octets.len(B.Octets.le32(v)), 0n) == 4n : Nat}:
328  %Equal.sym(Nat, B.Octets.len(B.Octets.le32(v)), 4n, BL.octets_len_le32(v)) : {Nat.add(_, 0n) == 4n : Nat}
329  {==}
330
331def tb.d8(+v: W.W64, +rest: B.Octets) -> {rest == B.Octets.drop(8n, B.Octets.append(B.Octets.le64(v), rest)) : B.Octets}:
332  %tb.e8(v) : {rest == B.Octets.drop(_, B.Octets.append(B.Octets.le64(v), rest)) : B.Octets}
333  %Equal.sym(B.Octets, B.Octets.drop(Nat.add(B.Octets.len(B.Octets.le64(v)), 0n), B.Octets.append(B.Octets.le64(v), rest)), B.Octets.drop(0n, rest), BL.octets_drop_append_add(B.Octets.le64(v), 0n, rest)) : {rest == _ : B.Octets}
334  %Equal.sym(B.Octets, B.Octets.drop(0n, rest), rest, BL.octets_drop_zero(rest)) : {rest == _ : B.Octets}
335  {==}
336
337def tb.d4(+v: U32, +rest: B.Octets) -> {rest == B.Octets.drop(4n, B.Octets.append(B.Octets.le32(v), rest)) : B.Octets}:
338  %tb.e4(v) : {rest == B.Octets.drop(_, B.Octets.append(B.Octets.le32(v), rest)) : B.Octets}
339  %Equal.sym(B.Octets, B.Octets.drop(Nat.add(B.Octets.len(B.Octets.le32(v)), 0n), B.Octets.append(B.Octets.le32(v), rest)), B.Octets.drop(0n, rest), BL.octets_drop_append_add(B.Octets.le32(v), 0n, rest)) : {rest == _ : B.Octets}
340  %Equal.sym(B.Octets, B.Octets.drop(0n, rest), rest, BL.octets_drop_zero(rest)) : {rest == _ : B.Octets}
341  {==}
342
343def tb.g8(+v: W.W64, +rest: B.Octets) -> {v == F.AcpiF.u64(B.Octets.append(B.Octets.le64(v), rest), 0n) : W.W64}:
344  %Equal.sym(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(B.Octets.le64(v), rest), 0n), B.Octets.le64_at(B.Octets.le64(v), 0n), BL.octets_le64_at_append_le(B.Octets.le64(v), rest, 0n, tb.l64(v))) : {v == Maybe.default(&2, W.W64, _, W.W64.zero()) : W.W64}
345  %Equal.sym(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.le64(v), 0n), Some{v}, BL.octets_le64_round_trip(v)) : {v == Maybe.default(&2, W.W64, _, W.W64.zero()) : W.W64}
346  {==}
347
348def tb.g4(+v: U32, +rest: B.Octets) -> {v == F.AcpiF.u32(B.Octets.append(B.Octets.le32(v), rest), 0n) : U32}:
349  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(B.Octets.le32(v), rest), 0n), B.Octets.le32_at(B.Octets.le32(v), 0n), BL.octets_le32_at_append_le(B.Octets.le32(v), rest, 0n, tb.l32(v))) : {v == Maybe.default(&2, U32, _, 0) : U32}
350  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.le32(v), 0n), Some{v}, BL.octets_le32_round_trip(v)) : {v == Maybe.default(&2, U32, _, 0) : U32}
351  {==}
352
353def tb.xread(+xs: List<&2, W.W64>, +acc: List<&2, W.W64>) -> {R.sl.read(List.length(&2, W.W64, xs), True{}, B.Octets.concat(R.sl.enc(xs, True{})), acc) == R.sl.rev(R.sl.rev(xs, acc), Nil{}) : List<&2, W.W64>}:
354  match xs:
355    case Nil{}:
356      {==}
357    case Con{+x, t}:
358      %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.le64(x), R.sl.enc(t, True{})}), B.Octets.append(B.Octets.le64(x), B.Octets.concat(R.sl.enc(t, True{}))), BL.octets_concat_cons(B.Octets.le64(x), R.sl.enc(t, True{}))) : {R.sl.read(List.length(&2, W.W64, t), True{}, B.Octets.drop(8n, _), Con{F.AcpiF.u64(_, 0n), acc}) == R.sl.rev(R.sl.rev(Con{x, t}, acc), Nil{}) : List<&2, W.W64>}
359      %tb.d8(x, B.Octets.concat(R.sl.enc(t, True{}))) : {R.sl.read(List.length(&2, W.W64, t), True{}, _, Con{F.AcpiF.u64(B.Octets.append(B.Octets.le64(x), B.Octets.concat(R.sl.enc(t, True{}))), 0n), acc}) == R.sl.rev(R.sl.rev(Con{x, t}, acc), Nil{}) : List<&2, W.W64>}
360      %tb.g8(x, B.Octets.concat(R.sl.enc(t, True{}))) : {R.sl.read(List.length(&2, W.W64, t), True{}, B.Octets.concat(R.sl.enc(t, True{})), Con{_, acc}) == R.sl.rev(R.sl.rev(Con{x, t}, acc), Nil{}) : List<&2, W.W64>}
361      tb.xread(t, Con{x, acc})
362
363def tb.rread(+xs: List<&2, W.W64>, +acc: List<&2, W.W64>) -> {R.sl.read(List.length(&2, W.W64, xs), False{}, B.Octets.concat(R.sl.enc(xs, False{})), acc) == R.sl.rev(R.sl.rev(Laws.acpilaw.low32(xs), acc), Nil{}) : List<&2, W.W64>}:
364  match xs:
365    case Nil{}:
366      {==}
367    case Con{+x, t}:
368      %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.le32(W.W64.lo(x)), R.sl.enc(t, False{})}), B.Octets.append(B.Octets.le32(W.W64.lo(x)), B.Octets.concat(R.sl.enc(t, False{}))), BL.octets_concat_cons(B.Octets.le32(W.W64.lo(x)), R.sl.enc(t, False{}))) : {R.sl.read(List.length(&2, W.W64, t), False{}, B.Octets.drop(4n, _), Con{W.W64.from_u32(F.AcpiF.u32(_, 0n)), acc}) == R.sl.rev(R.sl.rev(Laws.acpilaw.low32(Con{x, t}), acc), Nil{}) : List<&2, W.W64>}
369      %tb.d4(W.W64.lo(x), B.Octets.concat(R.sl.enc(t, False{}))) : {R.sl.read(List.length(&2, W.W64, t), False{}, _, Con{W.W64.from_u32(F.AcpiF.u32(B.Octets.append(B.Octets.le32(W.W64.lo(x)), B.Octets.concat(R.sl.enc(t, False{}))), 0n)), acc}) == R.sl.rev(R.sl.rev(Laws.acpilaw.low32(Con{x, t}), acc), Nil{}) : List<&2, W.W64>}
370      %tb.g4(W.W64.lo(x), B.Octets.concat(R.sl.enc(t, False{}))) : {R.sl.read(List.length(&2, W.W64, t), False{}, B.Octets.concat(R.sl.enc(t, False{})), Con{W.W64.from_u32(_), acc}) == R.sl.rev(R.sl.rev(Laws.acpilaw.low32(Con{x, t}), acc), Nil{}) : List<&2, W.W64>}
371      tb.rread(t, Con{W.W64.from_u32(W.W64.lo(x)), acc})
372
373def Laws.xsdt_round_trip(h, h0, oem6b, tid8b, cid4b, xs):
374  match h0:
375    case H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}:
376      %tb.sdt_body(B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0, {==}, oem6b, tid8b, cid4b, B.Octets.concat(R.sl.enc(xs, True{}))) : {R.AcpiXsdt.of_sdt(H.AcpiSdt{h, _}) == Done{R.AcpiSdtList{h, xs}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
377      %tb.xlen(xs) : {R.sl.body(Nat.is_eq(Nat.mod(_, 8n), 0n), True{}, h, B.Octets.concat(R.sl.enc(xs, True{}))) == Done{R.AcpiSdtList{h, xs}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
378      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.mul(List.length(&2, W.W64, xs), 8n), 7n, 0n, 0n), (Nat.add(List.length(&2, W.W64, xs), 0n), 0n), tb.dm8(List.length(&2, W.W64, xs), 0n)) : {R.sl.body(Nat.is_eq(Pair.snd(Nat, Nat, _), 0n), True{}, h, B.Octets.concat(R.sl.enc(xs, True{}))) == Done{R.AcpiSdtList{h, xs}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
379      %tb.xlen(xs) : {Done{R.AcpiSdtList{h, R.sl.read(Nat.div(_, 8n), True{}, B.Octets.concat(R.sl.enc(xs, True{})), Nil{})}} == Done{R.AcpiSdtList{h, xs}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
380      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.mul(List.length(&2, W.W64, xs), 8n), 7n, 0n, 0n), (Nat.add(List.length(&2, W.W64, xs), 0n), 0n), tb.dm8(List.length(&2, W.W64, xs), 0n)) : {Done{R.AcpiSdtList{h, R.sl.read(Pair.fst(Nat, Nat, _), True{}, B.Octets.concat(R.sl.enc(xs, True{})), Nil{})}} == Done{R.AcpiSdtList{h, xs}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
381      %Equal.sym(Nat, Nat.add(List.length(&2, W.W64, xs), 0n), List.length(&2, W.W64, xs), UL.nat_add_zero(List.length(&2, W.W64, xs))) : {Done{R.AcpiSdtList{h, R.sl.read(_, True{}, B.Octets.concat(R.sl.enc(xs, True{})), Nil{})}} == Done{R.AcpiSdtList{h, xs}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
382      %Equal.sym(List<&2, W.W64>, R.sl.read(List.length(&2, W.W64, xs), True{}, B.Octets.concat(R.sl.enc(xs, True{})), Nil{}), R.sl.rev(R.sl.rev(xs, Nil{}), Nil{}), tb.xread(xs, Nil{})) : {Done{R.AcpiSdtList{h, _}} == Done{R.AcpiSdtList{h, xs}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
383      %tb.srev(xs) : {Done{R.AcpiSdtList{h, _}} == Done{R.AcpiSdtList{h, xs}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
384      {==}
385
386def Laws.rsdt_round_trip(h, h0, oem6b, tid8b, cid4b, xs):
387  match h0:
388    case H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}:
389      %tb.sdt_body(B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0, {==}, oem6b, tid8b, cid4b, B.Octets.concat(R.sl.enc(xs, False{}))) : {R.AcpiRsdt.of_sdt(H.AcpiSdt{h, _}) == Done{R.AcpiSdtList{h, Laws.acpilaw.low32(xs)}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
390      %tb.rlen(xs) : {R.sl.body(Nat.is_eq(Nat.mod(_, 4n), 0n), False{}, h, B.Octets.concat(R.sl.enc(xs, False{}))) == Done{R.AcpiSdtList{h, Laws.acpilaw.low32(xs)}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
391      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.mul(List.length(&2, W.W64, xs), 4n), 3n, 0n, 0n), (Nat.add(List.length(&2, W.W64, xs), 0n), 0n), tb.dm4(List.length(&2, W.W64, xs), 0n)) : {R.sl.body(Nat.is_eq(Pair.snd(Nat, Nat, _), 0n), False{}, h, B.Octets.concat(R.sl.enc(xs, False{}))) == Done{R.AcpiSdtList{h, Laws.acpilaw.low32(xs)}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
392      %tb.rlen(xs) : {Done{R.AcpiSdtList{h, R.sl.read(Nat.div(_, 4n), False{}, B.Octets.concat(R.sl.enc(xs, False{})), Nil{})}} == Done{R.AcpiSdtList{h, Laws.acpilaw.low32(xs)}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
393      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.mul(List.length(&2, W.W64, xs), 4n), 3n, 0n, 0n), (Nat.add(List.length(&2, W.W64, xs), 0n), 0n), tb.dm4(List.length(&2, W.W64, xs), 0n)) : {Done{R.AcpiSdtList{h, R.sl.read(Pair.fst(Nat, Nat, _), False{}, B.Octets.concat(R.sl.enc(xs, False{})), Nil{})}} == Done{R.AcpiSdtList{h, Laws.acpilaw.low32(xs)}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
394      %Equal.sym(Nat, Nat.add(List.length(&2, W.W64, xs), 0n), List.length(&2, W.W64, xs), UL.nat_add_zero(List.length(&2, W.W64, xs))) : {Done{R.AcpiSdtList{h, R.sl.read(_, False{}, B.Octets.concat(R.sl.enc(xs, False{})), Nil{})}} == Done{R.AcpiSdtList{h, Laws.acpilaw.low32(xs)}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
395      %Equal.sym(List<&2, W.W64>, R.sl.read(List.length(&2, W.W64, xs), False{}, B.Octets.concat(R.sl.enc(xs, False{})), Nil{}), R.sl.rev(R.sl.rev(Laws.acpilaw.low32(xs), Nil{}), Nil{}), tb.rread(xs, Nil{})) : {Done{R.AcpiSdtList{h, _}} == Done{R.AcpiSdtList{h, Laws.acpilaw.low32(xs)}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
396      %tb.srev(Laws.acpilaw.low32(xs)) : {Done{R.AcpiSdtList{h, _}} == Done{R.AcpiSdtList{h, Laws.acpilaw.low32(xs)}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
397      {==}
398
399# MCFG: each 16-byte structure, its fields split into bits, computed; the
400# structures after it are reached through bytes' laws
401
402def tb.clen(+ah: U32, +al: U32, +s: U32, +lo: U32, +hi: U32) -> {16n == B.Octets.len(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)])) : Nat}:
403  match ah al s:
404    case U32{WCon{ah0, WCon{ah1, WCon{ah2, WCon{ah3, WCon{ah4, WCon{ah5, WCon{ah6, WCon{ah7, WCon{ah8, WCon{ah9, WCon{ah10, WCon{ah11, WCon{ah12, WCon{ah13, WCon{ah14, WCon{ah15, WCon{ah16, WCon{ah17, WCon{ah18, WCon{ah19, WCon{ah20, WCon{ah21, WCon{ah22, WCon{ah23, WCon{ah24, WCon{ah25, WCon{ah26, WCon{ah27, WCon{ah28, WCon{ah29, WCon{ah30, WCon{ah31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{al0, WCon{al1, WCon{al2, WCon{al3, WCon{al4, WCon{al5, WCon{al6, WCon{al7, WCon{al8, WCon{al9, WCon{al10, WCon{al11, WCon{al12, WCon{al13, WCon{al14, WCon{al15, WCon{al16, WCon{al17, WCon{al18, WCon{al19, WCon{al20, WCon{al21, WCon{al22, WCon{al23, WCon{al24, WCon{al25, WCon{al26, WCon{al27, WCon{al28, WCon{al29, WCon{al30, WCon{al31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{s0, WCon{s1, WCon{s2, WCon{s3, WCon{s4, WCon{s5, WCon{s6, WCon{s7, WCon{s8, WCon{s9, WCon{s10, WCon{s11, WCon{s12, WCon{s13, WCon{s14, WCon{s15, WCon{s16, WCon{s17, WCon{s18, WCon{s19, WCon{s20, WCon{s21, WCon{s22, WCon{s23, WCon{s24, WCon{s25, WCon{s26, WCon{s27, WCon{s28, WCon{s29, WCon{s30, WCon{s31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
405      {==}
406
407def tb.cvals(+ah: U32, +al: U32, +s: U32, +lo: U32, +hi: U32) -> {Mc.AcpiMcfgEntry{W.W64.from_parts(ah, al), B.low16(s), B.byte(lo), B.byte(hi)} == Mc.AcpiMcfgEntry{F.AcpiF.u64(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 0n), F.AcpiF.u16(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 8n), F.AcpiF.u8(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 10n), F.AcpiF.u8(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 11n)} : Mc.AcpiMcfgEntry}:
408  match ah al s:
409    case U32{WCon{ah0, WCon{ah1, WCon{ah2, WCon{ah3, WCon{ah4, WCon{ah5, WCon{ah6, WCon{ah7, WCon{ah8, WCon{ah9, WCon{ah10, WCon{ah11, WCon{ah12, WCon{ah13, WCon{ah14, WCon{ah15, WCon{ah16, WCon{ah17, WCon{ah18, WCon{ah19, WCon{ah20, WCon{ah21, WCon{ah22, WCon{ah23, WCon{ah24, WCon{ah25, WCon{ah26, WCon{ah27, WCon{ah28, WCon{ah29, WCon{ah30, WCon{ah31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{al0, WCon{al1, WCon{al2, WCon{al3, WCon{al4, WCon{al5, WCon{al6, WCon{al7, WCon{al8, WCon{al9, WCon{al10, WCon{al11, WCon{al12, WCon{al13, WCon{al14, WCon{al15, WCon{al16, WCon{al17, WCon{al18, WCon{al19, WCon{al20, WCon{al21, WCon{al22, WCon{al23, WCon{al24, WCon{al25, WCon{al26, WCon{al27, WCon{al28, WCon{al29, WCon{al30, WCon{al31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{s0, WCon{s1, WCon{s2, WCon{s3, WCon{s4, WCon{s5, WCon{s6, WCon{s7, WCon{s8, WCon{s9, WCon{s10, WCon{s11, WCon{s12, WCon{s13, WCon{s14, WCon{s15, WCon{s16, WCon{s17, WCon{s18, WCon{s19, WCon{s20, WCon{s21, WCon{s22, WCon{s23, WCon{s24, WCon{s25, WCon{s26, WCon{s27, WCon{s28, WCon{s29, WCon{s30, WCon{s31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
410      {==}
411
412def tb.ile(+k: Nat, +c: B.Octets, +h16: {16n == B.Octets.len(c) : Nat}, +ok: {Nat.is_le(k, 16n) == True{} : Bool}) -> {Nat.is_le(k, B.Octets.len(c)) == True{} : Bool}:
413  %h16 : {Nat.is_le(k, _) == True{} : Bool}
414  ok
415
416def tb.ilt(+k: Nat, +c: B.Octets, +h16: {16n == B.Octets.len(c) : Nat}, +ok: {Nat.is_lt(k, 16n) == True{} : Bool}) -> {Nat.is_lt(k, B.Octets.len(c)) == True{} : Bool}:
417  %h16 : {Nat.is_lt(k, _) == True{} : Bool}
418  ok
419
420def tb.c64(+c: B.Octets, +rest: B.Octets, +h16: {16n == B.Octets.len(c) : Nat}) -> {F.AcpiF.u64(c, 0n) == F.AcpiF.u64(B.Octets.append(c, rest), 0n) : W.W64}:
421  %Equal.sym(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(c, rest), 0n), B.Octets.le64_at(c, 0n), BL.octets_le64_at_append_le(c, rest, 0n, tb.ile(8n, c, h16, {==}))) : {F.AcpiF.u64(c, 0n) == Maybe.default(&2, W.W64, _, W.W64.zero()) : W.W64}
422  {==}
423
424def tb.c16(+c: B.Octets, +rest: B.Octets, +h16: {16n == B.Octets.len(c) : Nat}) -> {F.AcpiF.u16(c, 8n) == F.AcpiF.u16(B.Octets.append(c, rest), 8n) : U32}:
425  %Equal.sym(Maybe<&2, U32>, B.Octets.le16_at(B.Octets.append(c, rest), 8n), B.Octets.le16_at(c, 8n), BL.octets_le16_at_append_le(c, rest, 8n, tb.ile(10n, c, h16, {==}))) : {F.AcpiF.u16(c, 8n) == Maybe.default(&2, U32, _, 0) : U32}
426  {==}
427
428def tb.c8(+c: B.Octets, +rest: B.Octets, +k: Nat, +hk: {Nat.is_lt(k, B.Octets.len(c)) == True{} : Bool}) -> {F.AcpiF.u8(c, k) == F.AcpiF.u8(B.Octets.append(c, rest), k) : U32}:
429  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(c, rest), k), B.Octets.at(c, k), BL.octets_at_append_lt(c, rest, k, hk)) : {F.AcpiF.u8(c, k) == Maybe.default(&2, U32, _, 0) : U32}
430  {==}
431
432def tb.cdrop(+c: B.Octets, +rest: B.Octets, +h16: {16n == B.Octets.len(c) : Nat}) -> {rest == B.Octets.drop(16n, B.Octets.append(c, rest)) : B.Octets}:
433  %Equal.sym(Nat, 16n, Nat.add(B.Octets.len(c), 0n), Equal.trans(Nat, 16n, B.Octets.len(c), Nat.add(B.Octets.len(c), 0n), h16, Equal.sym(Nat, Nat.add(B.Octets.len(c), 0n), B.Octets.len(c), UL.nat_add_zero(B.Octets.len(c))))) : {rest == B.Octets.drop(_, B.Octets.append(c, rest)) : B.Octets}
434  %Equal.sym(B.Octets, B.Octets.drop(Nat.add(B.Octets.len(c), 0n), B.Octets.append(c, rest)), B.Octets.drop(0n, rest), BL.octets_drop_append_add(c, 0n, rest)) : {rest == _ : B.Octets}
435  %Equal.sym(B.Octets, B.Octets.drop(0n, rest), rest, BL.octets_drop_zero(rest)) : {rest == _ : B.Octets}
436  {==}
437
438def tb.ment_b(+ah: U32, +al: U32, +s: U32, +lo: U32, +hi: U32, +rest: B.Octets) -> {Mc.AcpiMcfgEntry{W.W64.from_parts(ah, al), B.low16(s), B.byte(lo), B.byte(hi)} == Mc.AcpiMcfgEntry{F.AcpiF.u64(B.Octets.append(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 0n), F.AcpiF.u16(B.Octets.append(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 8n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 10n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 11n)} : Mc.AcpiMcfgEntry}:
439  %tb.c64(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest, tb.clen(ah, al, s, lo, hi)) : {Mc.AcpiMcfgEntry{W.W64.from_parts(ah, al), B.low16(s), B.byte(lo), B.byte(hi)} == Mc.AcpiMcfgEntry{_, F.AcpiF.u16(B.Octets.append(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 8n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 10n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 11n)} : Mc.AcpiMcfgEntry}
440  %tb.c16(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest, tb.clen(ah, al, s, lo, hi)) : {Mc.AcpiMcfgEntry{W.W64.from_parts(ah, al), B.low16(s), B.byte(lo), B.byte(hi)} == Mc.AcpiMcfgEntry{F.AcpiF.u64(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 0n), _, F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 10n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 11n)} : Mc.AcpiMcfgEntry}
441  %tb.c8(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest, 10n, tb.ilt(10n, B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), tb.clen(ah, al, s, lo, hi), {==})) : {Mc.AcpiMcfgEntry{W.W64.from_parts(ah, al), B.low16(s), B.byte(lo), B.byte(hi)} == Mc.AcpiMcfgEntry{F.AcpiF.u64(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 0n), F.AcpiF.u16(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 8n), _, F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 11n)} : Mc.AcpiMcfgEntry}
442  %tb.c8(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest, 11n, tb.ilt(11n, B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), tb.clen(ah, al, s, lo, hi), {==})) : {Mc.AcpiMcfgEntry{W.W64.from_parts(ah, al), B.low16(s), B.byte(lo), B.byte(hi)} == Mc.AcpiMcfgEntry{F.AcpiF.u64(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 0n), F.AcpiF.u16(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 8n), F.AcpiF.u8(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 10n), _} : Mc.AcpiMcfgEntry}
443  tb.cvals(ah, al, s, lo, hi)
444
445def tb.clen_g(+b: W.W64, +s: U32, +lo: U32, +hi: U32) -> {16n == B.Octets.len(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)])) : Nat}:
446  %WL.parts_of(b) : {16n == B.Octets.len(B.Octets.concat([B.Octets.le64(_), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)])) : Nat}
447  tb.clen(W.W64.hi(b), W.W64.lo(b), s, lo, hi)
448
449def tb.ment(+b: W.W64, +s: U32, +lo: U32, +hi: U32, +rest: B.Octets) -> {Mc.AcpiMcfgEntry{b, B.low16(s), B.byte(lo), B.byte(hi)} == Mc.AcpiMcfgEntry{F.AcpiF.u64(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 0n), F.AcpiF.u16(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 8n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 10n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 11n)} : Mc.AcpiMcfgEntry}:
450  %WL.parts_of(b) : {Mc.AcpiMcfgEntry{_, B.low16(s), B.byte(lo), B.byte(hi)} == Mc.AcpiMcfgEntry{F.AcpiF.u64(B.Octets.append(B.Octets.concat([B.Octets.le64(_), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 0n), F.AcpiF.u16(B.Octets.append(B.Octets.concat([B.Octets.le64(_), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 8n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(_), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 10n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(_), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest), 11n)} : Mc.AcpiMcfgEntry}
451  tb.ment_b(W.W64.hi(b), W.W64.lo(b), s, lo, hi, rest)
452
453def tb.mdrop(+b: W.W64, +s: U32, +lo: U32, +hi: U32, +rest: B.Octets) -> {rest == B.Octets.drop(16n, B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest)) : B.Octets}:
454  tb.cdrop(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), rest, tb.clen_g(b, s, lo, hi))
455
456def tb.mlen(+es: List<&2, Mc.AcpiMcfgEntry>) -> {Nat.mul(List.length(&2, Mc.AcpiMcfgEntry, es), 16n) == B.Octets.len(B.Octets.concat(Mc.mcfg.enc(es))) : Nat}:
457  match es:
458    case Nil{}:
459      {==}
460    case Con{e, t}:
461      match e:
462        case Mc.AcpiMcfgEntry{+b, +s, +lo, +hi}:
463          %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), Mc.mcfg.enc(t)}), B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), BL.octets_concat_cons(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), Mc.mcfg.enc(t))) : {Nat.mul(List.length(&2, Mc.AcpiMcfgEntry, Con{Mc.AcpiMcfgEntry{b, s, lo, hi}, t}), 16n) == B.Octets.len(_) : Nat}
464          %tb.la(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))) : {Nat.mul(List.length(&2, Mc.AcpiMcfgEntry, Con{Mc.AcpiMcfgEntry{b, s, lo, hi}, t}), 16n) == _ : Nat}
465          %tb.clen_g(b, s, lo, hi) : {Nat.mul(List.length(&2, Mc.AcpiMcfgEntry, Con{Mc.AcpiMcfgEntry{b, s, lo, hi}, t}), 16n) == Nat.add(_, B.Octets.len(B.Octets.concat(Mc.mcfg.enc(t)))) : Nat}
466          %tb.mlen(t) : {Nat.mul(List.length(&2, Mc.AcpiMcfgEntry, Con{Mc.AcpiMcfgEntry{b, s, lo, hi}, t}), 16n) == Nat.add(16n, _) : Nat}
467          {==}
468
469def tb.mread(+es: List<&2, Mc.AcpiMcfgEntry>) -> {Laws.acpilaw.mcfg_fit(es) == Mc.mcfg.read(List.length(&2, Mc.AcpiMcfgEntry, es), B.Octets.concat(Mc.mcfg.enc(es))) : List<&2, Mc.AcpiMcfgEntry>}:
470  match es:
471    case Nil{}:
472      {==}
473    case Con{e, t}:
474      match e:
475        case Mc.AcpiMcfgEntry{+b, +s, +lo, +hi}:
476          %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), Mc.mcfg.enc(t)}), B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), BL.octets_concat_cons(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), Mc.mcfg.enc(t))) : {Con{Mc.AcpiMcfgEntry{b, B.low16(s), B.byte(lo), B.byte(hi)}, Laws.acpilaw.mcfg_fit(t)} == Con{Mc.AcpiMcfgEntry{F.AcpiF.u64(_, 0n), F.AcpiF.u16(_, 8n), F.AcpiF.u8(_, 10n), F.AcpiF.u8(_, 11n)}, Mc.mcfg.read(List.length(&2, Mc.AcpiMcfgEntry, t), B.Octets.drop(16n, _))} : List<&2, Mc.AcpiMcfgEntry>}
477          %tb.mdrop(b, s, lo, hi, B.Octets.concat(Mc.mcfg.enc(t))) : {Con{Mc.AcpiMcfgEntry{b, B.low16(s), B.byte(lo), B.byte(hi)}, Laws.acpilaw.mcfg_fit(t)} == Con{Mc.AcpiMcfgEntry{F.AcpiF.u64(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 0n), F.AcpiF.u16(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 8n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 10n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 11n)}, Mc.mcfg.read(List.length(&2, Mc.AcpiMcfgEntry, t), _)} : List<&2, Mc.AcpiMcfgEntry>}
478          %tb.mread(t) : {Con{Mc.AcpiMcfgEntry{b, B.low16(s), B.byte(lo), B.byte(hi)}, Laws.acpilaw.mcfg_fit(t)} == Con{Mc.AcpiMcfgEntry{F.AcpiF.u64(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 0n), F.AcpiF.u16(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 8n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 10n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 11n)}, _} : List<&2, Mc.AcpiMcfgEntry>}
479          %tb.ment(b, s, lo, hi, B.Octets.concat(Mc.mcfg.enc(t))) : {Con{Mc.AcpiMcfgEntry{b, B.low16(s), B.byte(lo), B.byte(hi)}, Laws.acpilaw.mcfg_fit(t)} == Con{_, Laws.acpilaw.mcfg_fit(t)} : List<&2, Mc.AcpiMcfgEntry>}
480          {==}
481
482def tb.le8(+x: Nat) -> {True{} == Nat.is_le(8n, Nat.add(8n, x)) : Bool}:
483  match x:
484    case 0n:
485      {==}
486    case 1n+p:
487      {==}
488
489def tb.sb8(+x: Nat) -> {x == Nat.sub(Nat.add(8n, x), 8n) : Nat}:
490  match x:
491    case 0n:
492      {==}
493    case 1n+p:
494      {==}
495
496def tb.z8(+c: B.Octets) -> {c == B.Octets.drop(8n, B.Octets.append(B.Octets.zeros(8n), c)) : B.Octets}:
497  %Equal.sym(B.Octets, B.Octets.drop(Nat.add(B.Octets.len(B.Octets.zeros(8n)), 0n), B.Octets.append(B.Octets.zeros(8n), c)), B.Octets.drop(0n, c), BL.octets_drop_append_add(B.Octets.zeros(8n), 0n, c)) : {c == _ : B.Octets}
498  %Equal.sym(B.Octets, B.Octets.drop(0n, c), c, BL.octets_drop_zero(c)) : {c == _ : B.Octets}
499  {==}
500
501def Laws.mcfg_round_trip(h, h0, oem6b, tid8b, cid4b, es):
502  match h0:
503    case H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}:
504      %tb.sdt_body(B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0, {==}, oem6b, tid8b, cid4b, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))) : {Mc.AcpiMcfg.of_sdt(H.AcpiSdt{h, _}) == Done{Mc.AcpiMcfg{h, Laws.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
505      %tb.la(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es))) : {Mc.mcfg.body(Bool.and(Nat.is_le(8n, _), Nat.is_eq(Nat.mod(Nat.sub(_, 8n), 16n), 0n)), h, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))) == Done{Mc.AcpiMcfg{h, Laws.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
506      %tb.le8(B.Octets.len(B.Octets.concat(Mc.mcfg.enc(es)))) : {Mc.mcfg.body(Bool.and(_, Nat.is_eq(Nat.mod(Nat.sub(Nat.add(8n, B.Octets.len(B.Octets.concat(Mc.mcfg.enc(es)))), 8n), 16n), 0n)), h, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))) == Done{Mc.AcpiMcfg{h, Laws.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
507      %tb.sb8(B.Octets.len(B.Octets.concat(Mc.mcfg.enc(es)))) : {Mc.mcfg.body(Nat.is_eq(Nat.mod(_, 16n), 0n), h, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))) == Done{Mc.AcpiMcfg{h, Laws.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
508      %tb.mlen(es) : {Mc.mcfg.body(Nat.is_eq(Nat.mod(_, 16n), 0n), h, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))) == Done{Mc.AcpiMcfg{h, Laws.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
509      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.mul(List.length(&2, Mc.AcpiMcfgEntry, es), 16n), 15n, 0n, 0n), (Nat.add(List.length(&2, Mc.AcpiMcfgEntry, es), 0n), 0n), tb.dm16(List.length(&2, Mc.AcpiMcfgEntry, es), 0n)) : {Mc.mcfg.body(Nat.is_eq(Pair.snd(Nat, Nat, _), 0n), h, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))) == Done{Mc.AcpiMcfg{h, Laws.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
510      %tb.z8(B.Octets.concat(Mc.mcfg.enc(es))) : {Done{Mc.AcpiMcfg{h, Mc.mcfg.read(Nat.div(B.Octets.len(_), 16n), _)}} == Done{Mc.AcpiMcfg{h, Laws.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
511      %tb.mlen(es) : {Done{Mc.AcpiMcfg{h, Mc.mcfg.read(Nat.div(_, 16n), B.Octets.concat(Mc.mcfg.enc(es)))}} == Done{Mc.AcpiMcfg{h, Laws.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
512      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.mul(List.length(&2, Mc.AcpiMcfgEntry, es), 16n), 15n, 0n, 0n), (Nat.add(List.length(&2, Mc.AcpiMcfgEntry, es), 0n), 0n), tb.dm16(List.length(&2, Mc.AcpiMcfgEntry, es), 0n)) : {Done{Mc.AcpiMcfg{h, Mc.mcfg.read(Pair.fst(Nat, Nat, _), B.Octets.concat(Mc.mcfg.enc(es)))}} == Done{Mc.AcpiMcfg{h, Laws.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
513      %Equal.sym(Nat, Nat.add(List.length(&2, Mc.AcpiMcfgEntry, es), 0n), List.length(&2, Mc.AcpiMcfgEntry, es), UL.nat_add_zero(List.length(&2, Mc.AcpiMcfgEntry, es))) : {Done{Mc.AcpiMcfg{h, Mc.mcfg.read(_, B.Octets.concat(Mc.mcfg.enc(es)))}} == Done{Mc.AcpiMcfg{h, Laws.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
514      %tb.mread(es) : {Done{Mc.AcpiMcfg{h, _}} == Done{Mc.AcpiMcfg{h, Laws.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
515      {==}
516
517def Laws.aml_round_trip(h, h0, sig4b, oem6b, tid8b, cid4b, a):
518  match h0:
519    case H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}:
520      %tb.sdt_body(s0, l0, r0, c0, o0, t0, orv0, ci0, cr0, sig4b, oem6b, tid8b, cid4b, a) : {Ds.AcpiAml.of_sdt(H.AcpiSdt{h, _}) == Done{Ds.AcpiAml{h, a}} : Result<&2, &2, E.AcpiError, Ds.AcpiAml>}
521      {==}