PROOF_whole.bend
bend-osdev-acpi@0.1.2.0 · 288 lines · 0 definitions
1# The proof of LAWS_whole.bend.
2#
3# AcpiSdt.build(h, body) is fix(9, encode(h0) ++ body), h0 being h with
4# its Length computed and its Checksum 0. The header's first 9 bytes and
5# the bytes from 10 on are untouched by fix, so the table is encode(hk) ++
6# body, hk being h with the Length and the Checksum k that fix writes
7# (ckw.bl1, through bytes' take, drop and append laws, ckw.gfix). Its
8# bytes sum to zero (LAWS_checksum.bend: fix_ok); its Length field reads
9# 36 + len(body) back (ckw.p1, ckw.fnv: the U32 of a Nat no more than a
10# U32's value has that value), which is the table's length (tb.lenchk), so
11# AcpiSdt.check accepts the whole table (ckw.chk); its header decodes as hk
12# with any bytes after it (ckw.dec, as PROOF.bend's hdr_rt does without
13# them), and the bytes after the header are the body (tb.elen). Each
14# table's parse then checks the signature build wrote and reads the body
15# by the laws of LAWS_tables.bend.
16import Base
17import bend-osdev-word64@0.1.1.1/word64.bend as W
18import bend-osdev-word64@0.1.1.1/LAWS.bend as WL
19import bend-osdev-word64@0.1.1.1/PROOF.bend as WP
20import bend-osdev-bytes@0.1.1.1/bytes.bend as B
21import bend-osdev-bytes@0.1.1.1/LAWS.bend as BL
22import bend-osdev-bytes@0.1.1.1/PROOF.bend as BP
23import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
24import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
25import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO
26import bend-osdev-u32@0.1.0.0/PROOF_order.bend as UOP
27import bend-osdev-acpi@0.1.2.0/error.bend as E
28import bend-osdev-acpi@0.1.2.0/header.bend as H
29import bend-osdev-acpi@0.1.2.0/checksum.bend as C
30import bend-osdev-acpi@0.1.2.0/gas.bend as G
31import bend-osdev-acpi@0.1.2.0/hpet.bend as Hp
32import bend-osdev-acpi@0.1.2.0/bgrt.bend as Bg
33import bend-osdev-acpi@0.1.2.0/rsdt.bend as R
34import bend-osdev-acpi@0.1.2.0/mcfg.bend as Mc
35import bend-osdev-acpi@0.1.2.0/dsdt.bend as Ds
36import bend-osdev-acpi@0.1.2.0/LAWS_tables.bend as TL
37import bend-osdev-acpi@0.1.2.0/PROOF_tables.bend as TP
38import bend-osdev-acpi@0.1.2.0/LAWS_checksum.bend as CL
39import bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend as CP
40import bend-osdev-acpi@0.1.2.0/LAWS_whole.bend as Laws
41
42# The U32 of a Nat no more than a U32's value has that value
43
44def ckw.fnh(+p: Nat, +z: U32, +h: {Nat.is_le(1n+p, U32.to_nat(z)) == True{} : Bool}, +ih: {U32.to_nat(U32.from_nat(p)) == p : Nat}) -> {Nat.is_le(1n+U32.to_nat(U32.from_nat(p)), U32.to_nat(z)) == True{} : Bool}:
45 %Equal.sym(Nat, U32.to_nat(U32.from_nat(p)), p, ih) : {Nat.is_le(1n+_, U32.to_nat(z)) == True{} : Bool}
46 h
47
48def ckw.fnv(+n: Nat, +z: U32, +h: {Nat.is_le(n, U32.to_nat(z)) == True{} : Bool}) -> {U32.to_nat(U32.from_nat(n)) == n : Nat}:
49 match n:
50 case 0n:
51 {==}
52 case 1n+p:
53 %Equal.sym(Nat, U32.to_nat(U32.inc(U32.from_nat(p))), 1n+U32.to_nat(U32.from_nat(p)), UL.u32_inc_value(U32.from_nat(p), z, ckw.fnh(p, z, h, ckw.fnv(p, z, UO.nat_le_trans(p, 1n+p, U32.to_nat(z), UL.nat_le_add(p, 1n), h))))) : {_ == 1n+p : Nat}
54 %Equal.sym(Nat, U32.to_nat(U32.from_nat(p)), p, ckw.fnv(p, z, UO.nat_le_trans(p, 1n+p, U32.to_nat(z), UL.nat_le_add(p, 1n), h))) : {1n+_ == 1n+p : Nat}
55 {==}
56
57# Small facts about lengths
58
59def ckw.l4(+v: U32) -> {Nat.is_le(Nat.add(0n, 4n), B.Octets.len(B.Octets.le32(v))) == True{} : Bool}:
60 %Equal.sym(Nat, B.Octets.len(B.Octets.le32(v)), 4n, BL.octets_len_le32(v)) : {Nat.is_le(Nat.add(0n, 4n), _) == True{} : Bool}
61 {==}
62
63def ckw.lt01(+k: U32) -> {Nat.is_lt(0n, B.Octets.len(H.hd.byte(k))) == True{} : Bool}:
64 %Equal.sym(Nat, B.Octets.len(B.Octets.of_list([k])), B.len([k]), BL.octets_len_of_list([k])) : {Nat.is_lt(0n, _) == True{} : Bool}
65 {==}
66
67# A header's fields and the bytes after it, reassociated
68
69def ckw.ra(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +body: B.Octets) -> {B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body) == B.Octets.append(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.append(B.Octets.le32(cr), body))))))))) : B.Octets}:
70 %Equal.sym(B.Octets, B.Octets.append(B.Octets.append(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))))))))), body), B.Octets.append(s, B.Octets.append(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)))))))), body)), BL.octets_append_assoc(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)))))))), body)) : {_ == B.Octets.append(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.append(B.Octets.le32(cr), body))))))))) : B.Octets}
71 %Equal.sym(B.Octets, B.Octets.append(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)))))))), body), B.Octets.append(B.Octets.le32(l), B.Octets.append(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))))))), body)), BL.octets_append_assoc(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))))))), body)) : {B.Octets.append(s, _) == B.Octets.append(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.append(B.Octets.le32(cr), body))))))))) : B.Octets}
72 %Equal.sym(B.Octets, B.Octets.append(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))))))), body), B.Octets.append(H.hd.byte(r), B.Octets.append(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)))))), body)), BL.octets_append_assoc(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)))))), body)) : {B.Octets.append(s, B.Octets.append(B.Octets.le32(l), _)) == B.Octets.append(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.append(B.Octets.le32(cr), body))))))))) : B.Octets}
73 %Equal.sym(B.Octets, B.Octets.append(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)))))), body), B.Octets.append(H.hd.byte(c), B.Octets.append(B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))), body)), BL.octets_append_assoc(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))))), body)) : {B.Octets.append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), _))) == B.Octets.append(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.append(B.Octets.le32(cr), body))))))))) : B.Octets}
74 %Equal.sym(B.Octets, B.Octets.append(B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))), body), B.Octets.append(o, B.Octets.append(B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))), body)), BL.octets_append_assoc(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))), body)) : {B.Octets.append(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(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.append(B.Octets.le32(cr), body))))))))) : B.Octets}
75 %Equal.sym(B.Octets, B.Octets.append(B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))), body), B.Octets.append(t, B.Octets.append(B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))), body)), BL.octets_append_assoc(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))), body)) : {B.Octets.append(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(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.append(B.Octets.le32(cr), body))))))))) : B.Octets}
76 %Equal.sym(B.Octets, B.Octets.append(B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))), body), B.Octets.append(B.Octets.le32(orv), B.Octets.append(B.Octets.append(ci, B.Octets.le32(cr)), body)), BL.octets_append_assoc(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)), body)) : {B.Octets.append(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(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.append(B.Octets.le32(cr), body))))))))) : B.Octets}
77 %Equal.sym(B.Octets, B.Octets.append(B.Octets.append(ci, B.Octets.le32(cr)), body), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)), BL.octets_append_assoc(ci, B.Octets.le32(cr), body)) : {B.Octets.append(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(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.append(B.Octets.le32(cr), body))))))))) : B.Octets}
78 {==}
79
80def ckw.dec(+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) -> {H.AcpiHeader.decode(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body)) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}:
81 %Equal.sym(B.Octets, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), ckw.ra(s, l, r, c, o, t, orv, ci, cr, body)) : {H.AcpiHeader.decode(_) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
82 %sig4 : {H.hd.d1(B.Octets.split_at(_, B.Octets.append(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.append(B.Octets.le32(cr), body)))))))))), B.Octets.append(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.append(B.Octets.le32(cr), body)))))))))) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
83 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(s), B.Octets.append(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.append(B.Octets.le32(cr), body)))))))))), Some{B.OctetsSplit{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.append(B.Octets.le32(cr), body))))))))}}, BL.octets_split_at_append(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.append(B.Octets.le32(cr), body)))))))))) : {H.hd.d1(_, B.Octets.append(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.append(B.Octets.le32(cr), body)))))))))) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
84 %BL.octets_len_le32(l) : {H.hd.d2(B.Octets.split_at(_, 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.append(B.Octets.le32(cr), body))))))))), B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
85 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(B.Octets.le32(l)), 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.append(B.Octets.le32(cr), body))))))))), Some{B.OctetsSplit{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.append(B.Octets.le32(cr), body)))))))}}, BL.octets_split_at_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.append(B.Octets.le32(cr), body))))))))) : {H.hd.d2(_, B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
86 %BL.octets_len_of_list([r]) : {H.hd.d3(B.Octets.split_at(_, 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.append(B.Octets.le32(cr), body)))))))), B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l))) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
87 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(H.hd.byte(r)), 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.append(B.Octets.le32(cr), body)))))))), Some{B.OctetsSplit{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.append(B.Octets.le32(cr), body))))))}}, BL.octets_split_at_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.append(B.Octets.le32(cr), body)))))))) : {H.hd.d3(_, B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l))) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
88 %BL.octets_len_of_list([c]) : {H.hd.d4(B.Octets.split_at(_, 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.append(B.Octets.le32(cr), body))))))), B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r))) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
89 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(H.hd.byte(c)), 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.append(B.Octets.le32(cr), body))))))), Some{B.OctetsSplit{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.append(B.Octets.le32(cr), body)))))}}, BL.octets_split_at_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.append(B.Octets.le32(cr), body))))))) : {H.hd.d4(_, B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r))) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
90 %oem6 : {H.hd.d5(B.Octets.split_at(_, B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))))), B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c))) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
91 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(o), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))))), Some{B.OctetsSplit{o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))}}, BL.octets_split_at_append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))))) : {H.hd.d5(_, B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c))) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
92 %tid8 : {H.hd.d6(B.Octets.split_at(_, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))), B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
93 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(t), B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))), Some{B.OctetsSplit{t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))}}, BL.octets_split_at_append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))) : {H.hd.d6(_, B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
94 %BL.octets_len_le32(orv) : {H.hd.d7(B.Octets.split_at(_, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))), B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
95 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(B.Octets.le32(orv)), B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))), Some{B.OctetsSplit{B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))}}, BL.octets_split_at_append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))) : {H.hd.d7(_, B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
96 %cid4 : {H.hd.d8(B.Octets.split_at(_, B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))), B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv))) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
97 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(ci), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))), Some{B.OctetsSplit{ci, B.Octets.append(B.Octets.le32(cr), body)}}, BL.octets_split_at_append(ci, B.Octets.append(B.Octets.le32(cr), body))) : {H.hd.d8(_, B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv))) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
98 %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.le32(cr), body)), Nat.add(B.Octets.len(B.Octets.le32(cr)), B.Octets.len(body)), BL.octets_len_append(B.Octets.le32(cr), body)) : {H.hd.d9(Nat.is_le(4n, _), B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv)), ci, B.Octets.append(B.Octets.le32(cr), body)) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
99 %Equal.sym(Nat, B.Octets.len(B.Octets.le32(cr)), 4n, BL.octets_len_le32(cr)) : {H.hd.d9(Nat.is_le(4n, Nat.add(_, B.Octets.len(body))), B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv)), ci, B.Octets.append(B.Octets.le32(cr), body)) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
100 %Equal.sym(Bool, Nat.is_le(4n, Nat.add(4n, B.Octets.len(body))), True{}, UO.nat_le_add_r(4n, B.Octets.len(body))) : {H.hd.d9(_, B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv)), ci, B.Octets.append(B.Octets.le32(cr), body)) == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
101 %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.le32(l), 0n), Some{l}, BL.octets_le32_round_trip(l)) : {Done{H.AcpiHeader{s, Maybe.default(&2, U32, _, 0), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv)), ci, H.hd.u32(B.Octets.append(B.Octets.le32(cr), body))}} == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
102 %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.le32(orv), 0n), Some{orv}, BL.octets_le32_round_trip(orv)) : {Done{H.AcpiHeader{s, l, H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, Maybe.default(&2, U32, _, 0), ci, H.hd.u32(B.Octets.append(B.Octets.le32(cr), body))}} == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
103 %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(B.Octets.le32(cr), body), 0n), B.Octets.le32_at(B.Octets.le32(cr), 0n), BL.octets_le32_at_append_le(B.Octets.le32(cr), body, 0n, ckw.l4(cr))) : {Done{H.AcpiHeader{s, l, H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, orv, ci, Maybe.default(&2, U32, _, 0)}} == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
104 %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.le32(cr), 0n), Some{cr}, BL.octets_le32_round_trip(cr)) : {Done{H.AcpiHeader{s, l, H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, orv, ci, Maybe.default(&2, U32, _, 0)}} == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
105 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list([r])), B.mask([r]), BL.octets_to_of([r])) : {Done{H.AcpiHeader{s, l, H.hd.u8.list(_), H.hd.u8(H.hd.byte(c)), o, t, orv, ci, cr}} == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
106 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list([c])), B.mask([c]), BL.octets_to_of([c])) : {Done{H.AcpiHeader{s, l, B.byte(r), H.hd.u8.list(_), o, t, orv, ci, cr}} == Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
107 {==}
108
109# The header as its first 9 bytes, its checksum byte, and the rest
110
111def ckw.enc(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +body: B.Octets) -> {B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body) == B.Octets.append(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), 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.append(B.Octets.le32(cr), body))))))) : B.Octets}:
112 %Equal.sym(B.Octets, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), body), B.Octets.append(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.append(B.Octets.le32(cr), body))))))))), ckw.ra(s, l, r, c, o, t, orv, ci, cr, body)) : {_ == B.Octets.append(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), 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.append(B.Octets.le32(cr), body))))))) : B.Octets}
113 %Equal.sym(B.Octets, B.Octets.append(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), 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.append(B.Octets.le32(cr), body))))))), B.Octets.append(s, B.Octets.append(B.Octets.append(B.Octets.le32(l), 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.append(B.Octets.le32(cr), body)))))))), BL.octets_append_assoc(s, B.Octets.append(B.Octets.le32(l), 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.append(B.Octets.le32(cr), body)))))))) : {B.Octets.append(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.append(B.Octets.le32(cr), body))))))))) == _ : B.Octets}
114 %Equal.sym(B.Octets, B.Octets.append(B.Octets.append(B.Octets.le32(l), 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.append(B.Octets.le32(cr), body))))))), 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.append(B.Octets.le32(cr), body)))))))), BL.octets_append_assoc(B.Octets.le32(l), 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.append(B.Octets.le32(cr), body)))))))) : {B.Octets.append(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.append(B.Octets.le32(cr), body))))))))) == B.Octets.append(s, _) : B.Octets}
115 {==}
116
117def ckw.plen(+s: B.Octets, +l: U32, +r: U32, +sig4: {B.Octets.len(s) == 4n : Nat}) -> {B.Octets.len(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))) == 9n : Nat}:
118 %Equal.sym(Nat, B.Octets.len(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))), Nat.add(B.Octets.len(s), B.Octets.len(B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))), BL.octets_len_append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))) : {_ == 9n : Nat}
119 %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.le32(l), H.hd.byte(r))), Nat.add(B.Octets.len(B.Octets.le32(l)), B.Octets.len(H.hd.byte(r))), BL.octets_len_append(B.Octets.le32(l), H.hd.byte(r))) : {Nat.add(B.Octets.len(s), _) == 9n : Nat}
120 %Equal.sym(Nat, B.Octets.len(s), 4n, sig4) : {Nat.add(_, Nat.add(B.Octets.len(B.Octets.le32(l)), B.Octets.len(H.hd.byte(r)))) == 9n : Nat}
121 %Equal.sym(Nat, B.Octets.len(B.Octets.le32(l)), 4n, BL.octets_len_le32(l)) : {Nat.add(4n, Nat.add(_, B.Octets.len(H.hd.byte(r)))) == 9n : Nat}
122 %Equal.sym(Nat, B.Octets.len(B.Octets.of_list([r])), B.len([r]), BL.octets_len_of_list([r])) : {Nat.add(4n, Nat.add(4n, _)) == 9n : Nat}
123 {==}
124
125# fix at i, with i bytes before it, keeps those bytes and the bytes after it
126
127def ckw.ltadd(+i: Nat, +r: Nat) -> {Nat.is_lt(i, Nat.add(i, 1n+r)) == True{} : Bool}:
128 match i:
129 case 0n:
130 {==}
131 case 1n+p:
132 ckw.ltadd(p, r)
133
134def ckw.glt(+i: Nat, +p: B.Octets, +q: U32, +rest: B.Octets, +hp: {B.Octets.len(p) == i : Nat}) -> {Nat.is_lt(i, B.Octets.len(B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))) == True{} : Bool}:
135 %Equal.sym(Nat, B.Octets.len(B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), Nat.add(B.Octets.len(p), B.Octets.len(B.Octets.append(B.Octets.of_list([q]), rest))), BL.octets_len_append(p, B.Octets.append(B.Octets.of_list([q]), rest))) : {Nat.is_lt(i, _) == True{} : Bool}
136 %Equal.sym(Nat, B.Octets.len(p), i, hp) : {Nat.is_lt(i, Nat.add(_, B.Octets.len(B.Octets.append(B.Octets.of_list([q]), rest)))) == True{} : Bool}
137 %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.of_list([q]), rest)), Nat.add(B.Octets.len(B.Octets.of_list([q])), B.Octets.len(rest)), BL.octets_len_append(B.Octets.of_list([q]), rest)) : {Nat.is_lt(i, Nat.add(i, _)) == True{} : Bool}
138 %Equal.sym(Nat, B.Octets.len(B.Octets.of_list([q])), B.len([q]), BL.octets_len_of_list([q])) : {Nat.is_lt(i, Nat.add(i, Nat.add(_, B.Octets.len(rest)))) == True{} : Bool}
139 ckw.ltadd(i, B.Octets.len(rest))
140
141def ckw.gfix(+i: Nat, +p: B.Octets, +q: U32, +rest: B.Octets, +hp: {B.Octets.len(p) == i : Nat}) -> {C.AcpiChecksum.fix(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}:
142 %Equal.sym(Bool, Nat.is_lt(i, B.Octets.len(B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))), True{}, ckw.glt(i, p, q, rest, hp)) : {C.ck.fix.pick(_, i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
143 %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), [B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]}), B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.concat([B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))])), BL.octets_concat_cons(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), [B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))])) : {_ == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
144 %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), [B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]}), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.concat([B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))])), BL.octets_concat_cons(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), [B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))])) : {B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), _) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
145 %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), Nil{}}), B.Octets.append(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.concat(Nil{})), BL.octets_concat_cons(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), Nil{})) : {B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), _)) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
146 %Equal.sym(B.Octets, B.Octets.concat(Nil{}), B.Octets.empty(), BL.octets_concat_nil()) : {B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.append(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), _))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
147 %Equal.sym(B.Octets, B.Octets.append(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.empty()), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), BL.octets_append_empty_r(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))))) : {B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), _)) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
148 %hp : {B.Octets.append(B.Octets.take(_, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
149 %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(p), B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), p, BL.octets_take_append(p, B.Octets.append(B.Octets.of_list([q]), rest))) : {B.Octets.append(_, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
150 %Equal.trans(Nat, Nat.add(B.Octets.len(p), 1n), Nat.add(i, 1n), Nat.add(1n, i), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), B.Octets.len(p), i, hp), UL.nat_add_comm(i, 1n)) : {B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(_, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
151 %Equal.sym(B.Octets, B.Octets.drop(Nat.add(B.Octets.len(p), 1n), B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.drop(1n, B.Octets.append(B.Octets.of_list([q]), rest)), BL.octets_drop_append_add(p, 1n, B.Octets.append(B.Octets.of_list([q]), rest))) : {B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), _)) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
152 %BL.octets_len_of_list([q]) : {B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(_, B.Octets.append(B.Octets.of_list([q]), rest)))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
153 %Equal.sym(B.Octets, B.Octets.drop(B.Octets.len(B.Octets.of_list([q])), B.Octets.append(B.Octets.of_list([q]), rest)), rest, BL.octets_drop_append(B.Octets.of_list([q]), rest)) : {B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), _)) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
154 {==}
155
156# The table build writes: the header with Length and Checksum, then the body
157
158def ckw.bl1(+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}, +body: B.Octets) -> {H.AcpiSdt.build(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, body) == B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body) : B.Octets}:
159 %Equal.sym(B.Octets, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body), B.Octets.append(B.Octets.append(s, B.Octets.append(B.Octets.le32(U32.from_nat(Nat.add(36n, B.Octets.len(body)))), H.hd.byte(r))), B.Octets.append(H.hd.byte(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(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))), ckw.enc(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr, body)) : {C.AcpiChecksum.fix(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}
160 %Equal.sym(B.Octets, 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.append(s, B.Octets.append(B.Octets.le32(U32.from_nat(Nat.add(36n, B.Octets.len(body)))), H.hd.byte(r))), B.Octets.append(H.hd.byte(0), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))), ckw.enc(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 0, o, t, orv, ci, cr, body)) : {C.AcpiChecksum.fix(9n, _) == B.Octets.append(B.Octets.append(s, B.Octets.append(B.Octets.le32(U32.from_nat(Nat.add(36n, B.Octets.len(body)))), H.hd.byte(r))), B.Octets.append(H.hd.byte(C.AcpiChecksum.byte_for(9n, _)), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))) : B.Octets}
161 ckw.gfix(9n, B.Octets.append(s, B.Octets.append(B.Octets.le32(U32.from_nat(Nat.add(36n, B.Octets.len(body)))), H.hd.byte(r))), 0, B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))), ckw.plen(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, sig4))
162
163# The Length field, and the byte at offset 9
164
165def ckw.p1(+s: B.Octets, +l: U32, +r: U32, +k: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +body: B.Octets) -> {B.Octets.le32_at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, k, o, t, orv, ci, cr}), body), 4n) == Some{l} : Maybe<&2, U32>}:
166 %Equal.sym(B.Octets, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, k, o, t, orv, ci, cr}), body), B.Octets.append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))))), ckw.ra(s, l, r, k, o, t, orv, ci, cr, body)) : {B.Octets.le32_at(_, 4n) == Some{l} : Maybe<&2, U32>}
167 %Equal.cong(Nat, Nat, z => Nat.add(z, 0n), B.Octets.len(s), 4n, sig4) : {B.Octets.le32_at(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))))), _) == Some{l} : Maybe<&2, U32>}
168 %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))))), Nat.add(B.Octets.len(s), 0n)), B.Octets.le32_at(B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))))))), 0n), BL.octets_le32_at_append_add(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))))))), 0n)) : {_ == Some{l} : Maybe<&2, U32>}
169 %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))))))), 0n), B.Octets.le32_at(B.Octets.le32(l), 0n), BL.octets_le32_at_append_le(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))), 0n, ckw.l4(l))) : {_ == Some{l} : Maybe<&2, U32>}
170 BL.octets_le32_round_trip(l)
171
172def ckw.at9(+s: B.Octets, +l: U32, +r: U32, +zz: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +body: B.Octets) -> {B.Octets.at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, U32.and(255, zz), o, t, orv, ci, cr}), body), 9n) == Some{U32.and(255, zz)} : Maybe<&2, U32>}:
173 %Equal.sym(B.Octets, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, U32.and(255, zz), o, t, orv, ci, cr}), body), B.Octets.append(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r))), B.Octets.append(H.hd.byte(U32.and(255, zz)), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))), ckw.enc(s, l, r, U32.and(255, zz), o, t, orv, ci, cr, body)) : {B.Octets.at(_, 9n) == Some{U32.and(255, zz)} : Maybe<&2, U32>}
174 %Equal.cong(Nat, Nat, z => Nat.add(z, 0n), B.Octets.len(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))), 9n, ckw.plen(s, l, r, sig4)) : {B.Octets.at(B.Octets.append(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r))), B.Octets.append(H.hd.byte(U32.and(255, zz)), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))), _) == Some{U32.and(255, zz)} : Maybe<&2, U32>}
175 %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r))), B.Octets.append(H.hd.byte(U32.and(255, zz)), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))), Nat.add(B.Octets.len(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))), 0n)), B.Octets.at(B.Octets.append(H.hd.byte(U32.and(255, zz)), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))))), 0n), BL.octets_at_append_add(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r))), B.Octets.append(H.hd.byte(U32.and(255, zz)), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))))), 0n)) : {_ == Some{U32.and(255, zz)} : Maybe<&2, U32>}
176 %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(H.hd.byte(U32.and(255, zz)), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))))), 0n), B.Octets.at(H.hd.byte(U32.and(255, zz)), 0n), BL.octets_at_append_lt(H.hd.byte(U32.and(255, zz)), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))), 0n, ckw.lt01(U32.and(255, zz)))) : {_ == Some{U32.and(255, zz)} : Maybe<&2, U32>}
177 %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.of_list([U32.and(255, zz)]), 0n), B.at(B.Octets.to_list(B.Octets.of_list([U32.and(255, zz)])), 0n), BL.octets_at_list(B.Octets.of_list([U32.and(255, zz)]), 0n)) : {_ == Some{U32.and(255, zz)} : Maybe<&2, U32>}
178 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list([U32.and(255, zz)])), B.mask([U32.and(255, zz)]), BL.octets_to_of([U32.and(255, zz)])) : {B.at(_, 0n) == Some{U32.and(255, zz)} : Maybe<&2, U32>}
179 %Equal.sym(U32, B.byte(U32.and(255, zz)), U32.and(255, zz), CP.ckp.bb2(zz)) : {Some{B.byte(_)} == Some{U32.and(255, zz)} : Maybe<&2, U32>}
180 %Equal.sym(U32, B.byte(U32.and(255, zz)), U32.and(255, zz), CP.ckp.bb2(zz)) : {Some{_} == Some{U32.and(255, zz)} : Maybe<&2, U32>}
181 {==}
182
183# The checks pass
184
185def ckw.chk(+s: B.Octets, +r: U32, +k: 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, +z: U32, +fit: {Nat.is_le(Nat.add(36n, B.Octets.len(body)), U32.to_nat(z)) == True{} : Bool}, +okq: {C.AcpiChecksum.ok(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)) == True{} : Bool}) -> {H.AcpiSdt.check(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)) == Done{B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)} : Result<&2, &2, E.AcpiError, B.Octets>}:
186 %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body), 4n), Some{U32.from_nat(Nat.add(36n, B.Octets.len(body)))}, ckw.p1(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr, sig4, body)) : {H.sdt.c1(_, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)) == Done{B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)} : Result<&2, &2, E.AcpiError, B.Octets>}
187 %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.add(36n, B.Octets.len(body)))), Nat.add(36n, B.Octets.len(body)), ckw.fnv(Nat.add(36n, B.Octets.len(body)), z, fit)) : {H.sdt.c2(Bool.and(Nat.is_le(36n, _), Nat.is_le(_, B.Octets.len(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)))), U32.from_nat(Nat.add(36n, B.Octets.len(body))), B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)) == Done{B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)} : Result<&2, &2, E.AcpiError, B.Octets>}
188 %TP.tb.lenchk(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body) : {H.sdt.c2(Bool.and(Nat.is_le(36n, Nat.add(36n, B.Octets.len(body))), Nat.is_le(Nat.add(36n, B.Octets.len(body)), _)), U32.from_nat(Nat.add(36n, B.Octets.len(body))), B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)) == Done{B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)} : Result<&2, &2, E.AcpiError, B.Octets>}
189 %Equal.sym(Bool, Nat.is_le(36n, Nat.add(36n, B.Octets.len(body))), True{}, UO.nat_le_add_r(36n, B.Octets.len(body))) : {H.sdt.c2(Bool.and(_, Nat.is_le(Nat.add(36n, B.Octets.len(body)), Nat.add(36n, B.Octets.len(body)))), U32.from_nat(Nat.add(36n, B.Octets.len(body))), B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)) == Done{B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)} : Result<&2, &2, E.AcpiError, B.Octets>}
190 %Equal.sym(Bool, Nat.is_le(Nat.add(36n, B.Octets.len(body)), Nat.add(36n, B.Octets.len(body))), True{}, UL.nat_le_refl(Nat.add(36n, B.Octets.len(body)))) : {H.sdt.c2(Bool.and(True{}, _), U32.from_nat(Nat.add(36n, B.Octets.len(body))), B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)) == Done{B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)} : Result<&2, &2, E.AcpiError, B.Octets>}
191 %Equal.trans(Nat, B.Octets.len(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)), Nat.add(36n, B.Octets.len(body)), U32.to_nat(U32.from_nat(Nat.add(36n, B.Octets.len(body)))), Equal.sym(Nat, Nat.add(36n, B.Octets.len(body)), B.Octets.len(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)), TP.tb.lenchk(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body)), Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.add(36n, B.Octets.len(body)))), Nat.add(36n, B.Octets.len(body)), ckw.fnv(Nat.add(36n, B.Octets.len(body)), z, fit))) : {H.sdt.c3(C.AcpiChecksum.ok(B.Octets.take(_, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body))), B.Octets.take(_, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body))) == Done{B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)} : Result<&2, &2, E.AcpiError, B.Octets>}
192 %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)), B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)), B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body), BL.octets_take_len(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body))) : {H.sdt.c3(C.AcpiChecksum.ok(_), _) == Done{B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)} : Result<&2, &2, E.AcpiError, B.Octets>}
193 %Equal.sym(Bool, C.AcpiChecksum.ok(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)), True{}, okq) : {H.sdt.c3(_, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)) == Done{B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, k, o, t, orv, ci, cr}), body)} : Result<&2, &2, E.AcpiError, B.Octets>}
194 {==}
195
196def ckw.blen(+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(H.AcpiSdt.build(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, body)) : Nat}:
197 %Equal.sym(B.Octets, H.AcpiSdt.build(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, body), B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body), ckw.bl1(s, l, r, c, o, t, orv, ci, cr, sig4, body)) : {Nat.add(36n, B.Octets.len(body)) == B.Octets.len(_) : Nat}
198 TP.tb.lenchk(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body)
199
200def ckw.hlt(+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_lt(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}:
201 %TP.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_lt(9n, _) == True{} : Bool}
202 {==}
203
204def ckw.okq(+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) -> {C.AcpiChecksum.ok(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body)) == True{} : Bool}:
205 %ckw.bl1(s, l, r, c, o, t, orv, ci, cr, sig4, body) : {C.AcpiChecksum.ok(_) == True{} : Bool}
206 CL.fix_ok(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), ckw.hlt(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body))
207
208def ckw.fitq(+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, +z: U32, +fit: {Nat.is_le(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, body)), U32.to_nat(z)) == True{} : Bool}) -> {Nat.is_le(Nat.add(36n, B.Octets.len(body)), U32.to_nat(z)) == True{} : Bool}:
209 %Equal.sym(Nat, Nat.add(36n, B.Octets.len(body)), B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, body)), ckw.blen(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body)) : {Nat.is_le(_, U32.to_nat(z)) == True{} : Bool}
210 fit
211
212# Any table
213
214def ckw.core(+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}, +rev8: {B.byte(r) == r : U32}, +body: B.Octets, +z: U32, +fit: {Nat.is_le(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, body)), U32.to_nat(z)) == True{} : Bool}) -> {H.AcpiSdt.parse(H.AcpiSdt.build(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, body)) == Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, body))), r, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, body), 9n), 0), o, t, orv, ci, cr}, body}} : Result<&2, &2, E.AcpiError, H.AcpiSdt>}:
215 %Equal.sym(B.Octets, H.AcpiSdt.build(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, body), B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body), ckw.bl1(s, l, r, c, o, t, orv, ci, cr, sig4, body)) : {H.AcpiSdt.parse(_) == Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(B.Octets.len(_)), r, Maybe.default(&2, U32, B.Octets.at(_, 9n), 0), o, t, orv, ci, cr}, body}} : Result<&2, &2, E.AcpiError, H.AcpiSdt>}
216 %TP.tb.lenchk(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body) : {H.AcpiSdt.parse(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body)) == Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(_), r, Maybe.default(&2, U32, B.Octets.at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body), 9n), 0), o, t, orv, ci, cr}, body}} : Result<&2, &2, E.AcpiError, H.AcpiSdt>}
217 %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body), 9n), Some{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))}, ckw.at9(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, U32.sub(256, U32.and(255, U32.sub(C.AcpiChecksum.sum(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)), U32.and(255, Maybe.default(&2, U32, B.Octets.at(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), 0))))), o, t, orv, ci, cr, sig4, body)) : {H.AcpiSdt.parse(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body)) == Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, Maybe.default(&2, U32, _, 0), o, t, orv, ci, cr}, body}} : Result<&2, &2, E.AcpiError, H.AcpiSdt>}
218 %Equal.sym(Result<&2, &2, E.AcpiError, B.Octets>, H.AcpiSdt.check(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body)), Done{B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body)}, ckw.chk(s, r, 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)), o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body, z, ckw.fitq(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body, z, fit), ckw.okq(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body))) : {H.sdt.parse.go(_) == Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}, body}} : Result<&2, &2, E.AcpiError, H.AcpiSdt>}
219 %Equal.sym(Result<&2, &2, E.AcpiError, H.AcpiHeader>, H.AcpiHeader.decode(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body)), Done{H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), B.byte(r), B.byte(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))), o, t, orv, ci, cr}}, ckw.dec(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr, sig4, oem6, tid8, cid4, body)) : {H.sdt.split(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body), _) == Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}, body}} : Result<&2, &2, E.AcpiError, H.AcpiSdt>}
220 %Equal.sym(U32, B.byte(r), r, rev8) : {Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), _, B.byte(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))), o, t, orv, ci, cr}, B.Octets.drop(36n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body))}} == Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}, body}} : Result<&2, &2, E.AcpiError, H.AcpiSdt>}
221 %Equal.sym(U32, B.byte(U32.and(255, U32.sub(256, U32.and(255, U32.sub(C.AcpiChecksum.sum(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)), U32.and(255, Maybe.default(&2, U32, B.Octets.at(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), 0))))))), U32.and(255, U32.sub(256, U32.and(255, U32.sub(C.AcpiChecksum.sum(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)), U32.and(255, Maybe.default(&2, U32, B.Octets.at(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), 0)))))), CP.ckp.bb2(U32.sub(256, U32.and(255, U32.sub(C.AcpiChecksum.sum(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)), U32.and(255, Maybe.default(&2, U32, B.Octets.at(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), 0))))))) : {Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, _, o, t, orv, ci, cr}, B.Octets.drop(36n, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body))}} == Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}, body}} : Result<&2, &2, E.AcpiError, H.AcpiSdt>}
222 %TP.tb.elen(s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr, sig4, oem6, tid8, cid4) : {Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}, B.Octets.drop(_, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body))}} == Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}, body}} : Result<&2, &2, E.AcpiError, H.AcpiSdt>}
223 %Equal.sym(B.Octets, B.Octets.drop(B.Octets.len(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr})), B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body)), body, BL.octets_drop_append(H.AcpiHeader.encode(H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}), body)) : {Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}, _}} == Done{H.AcpiSdt{H.AcpiHeader{s, U32.from_nat(Nat.add(36n, B.Octets.len(body))), r, 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)), o, t, orv, ci, cr}, body}} : Result<&2, &2, E.AcpiError, H.AcpiSdt>}
224 {==}
225
226# The laws
227
228def Laws.sdt_round_trip(h, sig4, oem6, tid8, cid4, rev8, body, z, fit):
229 match h:
230 case H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
231 ckw.core(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, rev8, body, z, fit)
232
233# the HPET and the BGRT are 56 bytes long
234def ckw.hpfit(+l0: U32, +r0: U32, +c0: U32, +o0: B.Octets, +t0: B.Octets, +orv0: U32, +ci0: B.Octets, +cr0: U32, +oem6b: {B.Octets.len(o0) == 6n : Nat}, +tid8b: {B.Octets.len(t0) == 8n : Nat}, +cid4b: {B.Octets.len(ci0) == 4n : Nat}, +id: U32, +gs: U32, +gw: U32, +go: U32, +ga: U32, +gaddr: W.W64, +n: U32, +m: U32, +p: U32) -> {Nat.is_le(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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])]))), U32.to_nat(56)) == True{} : Bool}:
235 %ckw.blen(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])])) : {Nat.is_le(_, U32.to_nat(56)) == True{} : Bool}
236 %WL.parts_of(gaddr) : {Nat.is_le(Nat.add(36n, B.Octets.len(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])]))), U32.to_nat(56)) == True{} : Bool}
237 %TP.tb.hp_len(id, gs, gw, go, ga, W.W64.hi(gaddr), W.W64.lo(gaddr), n, m, p) : {Nat.is_le(_, U32.to_nat(56)) == True{} : Bool}
238 {==}
239
240def Laws.hpet_whole(h0, oem6b, tid8b, cid4b, rev8b, id, gs, gw, go, ga, gaddr, n, m, p, gs8, gw8, go8, ga8, n8, m16, p8):
241 match h0:
242 case H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}:
243 %Equal.sym(Result<&2, &2, E.AcpiError, H.AcpiSdt>, H.AcpiSdt.parse(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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])]))), Done{H.AcpiSdt{H.AcpiHeader{B.Octets.of_string("HPET"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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])])))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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])])), 9n), 0), o0, t0, orv0, ci0, cr0}, 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])])}}, Laws.sdt_round_trip(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, {==}, oem6b, tid8b, cid4b, rev8b, 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])]), 56, ckw.hpfit(l0, r0, c0, o0, t0, orv0, ci0, cr0, oem6b, tid8b, cid4b, id, gs, gw, go, ga, gaddr, n, m, p))) : {Hp.hpet.parse(H.sdt.sig.go(B.Octets.of_string("HPET"), _)) == Done{Hp.AcpiHpet{H.AcpiHeader{B.Octets.of_string("HPET"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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])])))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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])])), 9n), 0), o0, t0, orv0, ci0, cr0}, id, G.AcpiGas{gs, gw, go, ga, gaddr}, n, m, p}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
244 %Equal.sym(B.Octets, 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])]), B.Octets.drop(36n, H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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])]))), TP.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{B.Octets.of_string("HPET"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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])])))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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])])), 9n), 0), o0, t0, orv0, ci0, cr0}, _}) == Done{Hp.AcpiHpet{H.AcpiHeader{B.Octets.of_string("HPET"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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])])))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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])])), 9n), 0), o0, t0, orv0, ci0, cr0}, id, G.AcpiGas{gs, gw, go, ga, gaddr}, n, m, p}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
245 TL.hpet_round_trip(H.AcpiHeader{B.Octets.of_string("HPET"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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])])))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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])])), 9n), 0), o0, t0, orv0, ci0, cr0}, {==}, oem6b, tid8b, cid4b, H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}, oem6b, tid8b, cid4b, id, gs, gw, go, ga, gaddr, n, m, p, gs8, gw8, go8, ga8, n8, m16, p8)
246
247def ckw.bgfit(+l0: U32, +r0: U32, +c0: U32, +o0: B.Octets, +t0: B.Octets, +orv0: U32, +ci0: B.Octets, +cr0: U32, +oem6b: {B.Octets.len(o0) == 6n : Nat}, +tid8b: {B.Octets.len(t0) == 8n : Nat}, +cid4b: {B.Octets.len(ci0) == 4n : Nat}, +v: U32, +st: U32, +it: U32, +a: W.W64, +x: U32, +y: U32) -> {Nat.is_le(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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)]))), U32.to_nat(56)) == True{} : Bool}:
248 %ckw.blen(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)])) : {Nat.is_le(_, U32.to_nat(56)) == True{} : Bool}
249 %WL.parts_of(a) : {Nat.is_le(Nat.add(36n, B.Octets.len(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(_), B.Octets.le32(x), B.Octets.le32(y)]))), U32.to_nat(56)) == True{} : Bool}
250 %TP.tb.bg_len(v, st, it, W.W64.hi(a), W.W64.lo(a), x, y) : {Nat.is_le(_, U32.to_nat(56)) == True{} : Bool}
251 {==}
252
253def Laws.bgrt_whole(h0, oem6b, tid8b, cid4b, rev8b, v, st, it, a, x, y, v16, st8, it8):
254 match h0:
255 case H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}:
256 %Equal.sym(Result<&2, &2, E.AcpiError, H.AcpiSdt>, H.AcpiSdt.parse(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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)]))), Done{H.AcpiSdt{H.AcpiHeader{B.Octets.of_string("BGRT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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)])))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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)])), 9n), 0), o0, t0, orv0, ci0, cr0}, 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)])}}, Laws.sdt_round_trip(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, {==}, oem6b, tid8b, cid4b, rev8b, 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)]), 56, ckw.bgfit(l0, r0, c0, o0, t0, orv0, ci0, cr0, oem6b, tid8b, cid4b, v, st, it, a, x, y))) : {Bg.bgrt.parse(H.sdt.sig.go(B.Octets.of_string("BGRT"), _)) == Done{Bg.AcpiBgrt{H.AcpiHeader{B.Octets.of_string("BGRT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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)])))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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)])), 9n), 0), o0, t0, orv0, ci0, cr0}, v, st, it, a, x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
257 %Equal.sym(B.Octets, 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)]), B.Octets.drop(36n, H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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)]))), TP.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{B.Octets.of_string("BGRT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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)])))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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)])), 9n), 0), o0, t0, orv0, ci0, cr0}, _}) == Done{Bg.AcpiBgrt{H.AcpiHeader{B.Octets.of_string("BGRT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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)])))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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)])), 9n), 0), o0, t0, orv0, ci0, cr0}, v, st, it, a, x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
258 TL.bgrt_round_trip(H.AcpiHeader{B.Octets.of_string("BGRT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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)])))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, 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)])), 9n), 0), o0, t0, orv0, ci0, cr0}, {==}, oem6b, tid8b, cid4b, H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}, oem6b, tid8b, cid4b, v, st, it, a, x, y, v16, st8, it8)
259
260def Laws.xsdt_whole(h0, oem6b, tid8b, cid4b, rev8b, xs, z, fit):
261 match h0:
262 case H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}:
263 %Equal.sym(Result<&2, &2, E.AcpiError, H.AcpiSdt>, H.AcpiSdt.parse(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, True{})))), Done{H.AcpiSdt{H.AcpiHeader{B.Octets.of_string("XSDT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, True{}))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, True{}))), 9n), 0), o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, True{}))}}, Laws.sdt_round_trip(H.AcpiHeader{B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, {==}, oem6b, tid8b, cid4b, rev8b, B.Octets.concat(R.sl.enc(xs, True{})), z, fit)) : {R.sl.parse(True{}, H.sdt.sig.go(B.Octets.of_string("XSDT"), _)) == Done{R.AcpiSdtList{H.AcpiHeader{B.Octets.of_string("XSDT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, True{}))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, True{}))), 9n), 0), o0, t0, orv0, ci0, cr0}, xs}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
264 %Equal.sym(B.Octets, B.Octets.concat(R.sl.enc(xs, True{})), B.Octets.drop(36n, H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, True{})))), TP.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.AcpiHeader{B.Octets.of_string("XSDT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, True{}))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, True{}))), 9n), 0), o0, t0, orv0, ci0, cr0}, _}) == Done{R.AcpiSdtList{H.AcpiHeader{B.Octets.of_string("XSDT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, True{}))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, True{}))), 9n), 0), o0, t0, orv0, ci0, cr0}, xs}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
265 TL.xsdt_round_trip(H.AcpiHeader{B.Octets.of_string("XSDT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, True{}))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("XSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, True{}))), 9n), 0), o0, t0, orv0, ci0, cr0}, H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}, oem6b, tid8b, cid4b, xs)
266
267def Laws.rsdt_whole(h0, oem6b, tid8b, cid4b, rev8b, xs, z, fit):
268 match h0:
269 case H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}:
270 %Equal.sym(Result<&2, &2, E.AcpiError, H.AcpiSdt>, H.AcpiSdt.parse(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, False{})))), Done{H.AcpiSdt{H.AcpiHeader{B.Octets.of_string("RSDT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, False{}))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, False{}))), 9n), 0), o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, False{}))}}, Laws.sdt_round_trip(H.AcpiHeader{B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, {==}, oem6b, tid8b, cid4b, rev8b, B.Octets.concat(R.sl.enc(xs, False{})), z, fit)) : {R.sl.parse(False{}, H.sdt.sig.go(B.Octets.of_string("RSDT"), _)) == Done{R.AcpiSdtList{H.AcpiHeader{B.Octets.of_string("RSDT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, False{}))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, False{}))), 9n), 0), o0, t0, orv0, ci0, cr0}, TL.acpilaw.low32(xs)}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
271 %Equal.sym(B.Octets, B.Octets.concat(R.sl.enc(xs, False{})), B.Octets.drop(36n, H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, False{})))), TP.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.AcpiHeader{B.Octets.of_string("RSDT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, False{}))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, False{}))), 9n), 0), o0, t0, orv0, ci0, cr0}, _}) == Done{R.AcpiSdtList{H.AcpiHeader{B.Octets.of_string("RSDT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, False{}))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, False{}))), 9n), 0), o0, t0, orv0, ci0, cr0}, TL.acpilaw.low32(xs)}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>}
272 TL.rsdt_round_trip(H.AcpiHeader{B.Octets.of_string("RSDT"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, False{}))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("RSDT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat(R.sl.enc(xs, False{}))), 9n), 0), o0, t0, orv0, ci0, cr0}, H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}, oem6b, tid8b, cid4b, xs)
273
274def Laws.mcfg_whole(h0, oem6b, tid8b, cid4b, rev8b, es, z, fit):
275 match h0:
276 case H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}:
277 %Equal.sym(Result<&2, &2, E.AcpiError, H.AcpiSdt>, H.AcpiSdt.parse(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es))))), Done{H.AcpiSdt{H.AcpiHeader{B.Octets.of_string("MCFG"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))), 9n), 0), o0, t0, orv0, ci0, cr0}, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))}}, Laws.sdt_round_trip(H.AcpiHeader{B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, {==}, oem6b, tid8b, cid4b, rev8b, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es))), z, fit)) : {Mc.mcfg.parse(H.sdt.sig.go(B.Octets.of_string("MCFG"), _)) == Done{Mc.AcpiMcfg{H.AcpiHeader{B.Octets.of_string("MCFG"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))), 9n), 0), o0, t0, orv0, ci0, cr0}, TL.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
278 %Equal.sym(B.Octets, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es))), B.Octets.drop(36n, H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es))))), TP.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.AcpiHeader{B.Octets.of_string("MCFG"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))), 9n), 0), o0, t0, orv0, ci0, cr0}, _}) == Done{Mc.AcpiMcfg{H.AcpiHeader{B.Octets.of_string("MCFG"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))), 9n), 0), o0, t0, orv0, ci0, cr0}, TL.acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>}
279 TL.mcfg_round_trip(H.AcpiHeader{B.Octets.of_string("MCFG"), U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("MCFG"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.append(B.Octets.zeros(8n), B.Octets.concat(Mc.mcfg.enc(es)))), 9n), 0), o0, t0, orv0, ci0, cr0}, H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}, oem6b, tid8b, cid4b, es)
280
281def Laws.aml_whole(h0, sig4b, oem6b, tid8b, cid4b, rev8b, a, z, fit):
282 match h0:
283 case H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}:
284 %Equal.sym(Result<&2, &2, E.AcpiError, H.AcpiSdt>, H.AcpiSdt.parse(H.AcpiSdt.build(H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}, a)), Done{H.AcpiSdt{H.AcpiHeader{s0, U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}, a))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}, a), 9n), 0), o0, t0, orv0, ci0, cr0}, a}}, Laws.sdt_round_trip(H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}, sig4b, oem6b, tid8b, cid4b, rev8b, a, z, fit)) : {Ds.aml.parse(_) == Done{Ds.AcpiAml{H.AcpiHeader{s0, U32.from_nat(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}, a))), r0, Maybe.default(&2, U32, B.Octets.at(H.AcpiSdt.build(H.AcpiHeader{s0, l0, r0, c0, o0, t0, orv0, ci0, cr0}, a), 9n), 0), o0, t0, orv0, ci0, cr0}, a}} : Result<&2, &2, E.AcpiError, Ds.AcpiAml>}
285 {==}
286
287def Laws.whole_example():
288 {==}