PROOF_rsdp.bend

bend-osdev-acpi@0.1.2.0 · 260 lines · 0 definitions

1# The proof of LAWS_rsdp.bend.
2#
3# The first 20 bytes build writes are fix(8, signature ++ [0] ++ OEMID ++
4# [revision] ++ RsdtAddress), which is the same bytes with the checksum
5# byte k1 at offset 8 (ckr.fa, by PROOF_whole.bend's ckw.gfix, the OEMID
6# being 6 bytes already: ckr.fit); every field parse reads is then found by
7# bytes' laws for fields inside joined bytes (ckr.at15, ckr.u16, ckr.sl9),
8# and the bytes sum to zero (LAWS_checksum.bend: fix_ok). Revision 2 adds
9# Length 36, XsdtAddress and three reserved bytes after those 20, fixed at
10# offset 32 (ckr.f2); its reads go through the first 32 bytes to the first
11# 20 (ckr.t8 ... ckr.q24).
12import Base
13import bend-osdev-word64@0.1.1.1/word64.bend as W
14import bend-osdev-bytes@0.1.1.1/bytes.bend as B
15import bend-osdev-bytes@0.1.1.1/LAWS.bend as BL
16import bend-osdev-bytes@0.1.1.1/PROOF.bend as BP
17import bend-osdev-word64@0.1.1.1/LAWS.bend as WL
18import bend-osdev-word64@0.1.1.1/PROOF.bend as WP
19import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
20import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
21import bend-osdev-acpi@0.1.2.0/error.bend as E
22import bend-osdev-acpi@0.1.2.0/checksum.bend as C
23import bend-osdev-acpi@0.1.2.0/fields.bend as F
24import bend-osdev-acpi@0.1.2.0/rsdp.bend as P
25import bend-osdev-acpi@0.1.2.0/LAWS_checksum.bend as CL
26import bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend as CP
27import bend-osdev-acpi@0.1.2.0/PROOF_whole.bend as WH
28import bend-osdev-acpi@0.1.2.0/LAWS_rsdp.bend as Laws
29
30# The OEMID, fitted to 6 bytes, is the OEMID
31
32def ckr.subn(+n: Nat) -> {Nat.sub(n, n) == 0n : Nat}:
33  match n:
34    case 0n:
35      {==}
36    case 1n+q:
37      ckr.subn(q)
38
39def ckr.z0() -> {B.Octets.zeros(0n) == B.Octets.empty() : B.Octets}:
40  {==}
41
42def ckr.fit(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}) -> {F.AcpiF.fit(6n, oem) == oem : B.Octets}:
43  %oem6 : {B.Octets.append(B.Octets.take(_, oem), B.Octets.zeros(Nat.sub(_, B.Octets.len(B.Octets.take(_, oem))))) == oem : B.Octets}
44  %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(oem), oem), oem, BL.octets_take_len(oem)) : {B.Octets.append(_, B.Octets.zeros(Nat.sub(B.Octets.len(oem), B.Octets.len(_)))) == oem : B.Octets}
45  %Equal.sym(Nat, Nat.sub(B.Octets.len(oem), B.Octets.len(oem)), 0n, ckr.subn(B.Octets.len(oem))) : {B.Octets.append(oem, B.Octets.zeros(_)) == oem : B.Octets}
46  %Equal.sym(B.Octets, B.Octets.zeros(0n), B.Octets.empty(), ckr.z0()) : {B.Octets.append(oem, _) == oem : B.Octets}
47  BL.octets_append_empty_r(oem)
48
49# The first 20 bytes, with the checksum byte k1 at offset 8
50
51def ckr.vr(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32) -> {B.Octets.concat([P.AcpiRsdp.signature(), B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}:
52  %Equal.sym(B.Octets, B.Octets.concat(Con{P.AcpiRsdp.signature(), [B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]}), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.concat([B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)])), BL.octets_concat_cons(P.AcpiRsdp.signature(), [B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)])) : {_ == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
53  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.of_list([0]), [F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]}), B.Octets.append(B.Octets.of_list([0]), B.Octets.concat([F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)])), BL.octets_concat_cons(B.Octets.of_list([0]), [F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)])) : {B.Octets.append(P.AcpiRsdp.signature(), _) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
54  %Equal.sym(B.Octets, B.Octets.concat(Con{F.AcpiF.fit(6n, oem), [B.Octets.of_list([rev]), B.Octets.le32(rsdt)]}), B.Octets.append(F.AcpiF.fit(6n, oem), B.Octets.concat([B.Octets.of_list([rev]), B.Octets.le32(rsdt)])), BL.octets_concat_cons(F.AcpiF.fit(6n, oem), [B.Octets.of_list([rev]), B.Octets.le32(rsdt)])) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), _)) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
55  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.of_list([rev]), [B.Octets.le32(rsdt)]}), B.Octets.append(B.Octets.of_list([rev]), B.Octets.concat([B.Octets.le32(rsdt)])), BL.octets_concat_cons(B.Octets.of_list([rev]), [B.Octets.le32(rsdt)])) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(F.AcpiF.fit(6n, oem), _))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
56  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.le32(rsdt), Nil{}}), B.Octets.append(B.Octets.le32(rsdt), B.Octets.concat(Nil{})), BL.octets_concat_cons(B.Octets.le32(rsdt), Nil{})) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(F.AcpiF.fit(6n, oem), B.Octets.append(B.Octets.of_list([rev]), _)))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
57  %Equal.sym(B.Octets, B.Octets.concat(Nil{}), B.Octets.empty(), BL.octets_concat_nil()) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(F.AcpiF.fit(6n, oem), B.Octets.append(B.Octets.of_list([rev]), B.Octets.append(B.Octets.le32(rsdt), _))))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
58  %Equal.sym(B.Octets, B.Octets.append(B.Octets.le32(rsdt), B.Octets.empty()), B.Octets.le32(rsdt), BL.octets_append_empty_r(B.Octets.le32(rsdt))) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(F.AcpiF.fit(6n, oem), B.Octets.append(B.Octets.of_list([rev]), _)))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
59  %Equal.sym(B.Octets, F.AcpiF.fit(6n, oem), oem, ckr.fit(oem, oem6)) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(_, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
60  {==}
61
62def ckr.fa(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32) -> {P.rs.v1(oem, rev, rsdt) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}:
63  %Equal.sym(B.Octets, B.Octets.concat([P.AcpiRsdp.signature(), B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), ckr.vr(oem, oem6, rev, rsdt)) : {C.AcpiChecksum.fix(8n, _) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
64  WH.ckw.gfix(8n, P.AcpiRsdp.signature(), 0, B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))), {==})
65
66# Its length and its fields
67
68def ckr.l20(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32) -> {B.Octets.len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) == 20n : Nat}:
69  %Equal.sym(Nat, B.Octets.len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), Nat.add(B.Octets.len(P.AcpiRsdp.signature()), B.Octets.len(B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), BL.octets_len_append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) : {_ == 20n : Nat}
70  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), Nat.add(B.Octets.len(B.Octets.of_list([k])), B.Octets.len(B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), BL.octets_len_append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : {Nat.add(B.Octets.len(P.AcpiRsdp.signature()), _) == 20n : Nat}
71  %Equal.sym(Nat, B.Octets.len(B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), Nat.add(B.Octets.len(oem), B.Octets.len(B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), BL.octets_len_append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))) : {Nat.add(B.Octets.len(P.AcpiRsdp.signature()), Nat.add(B.Octets.len(B.Octets.of_list([k])), _)) == 20n : Nat}
72  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))), Nat.add(B.Octets.len(B.Octets.of_list([rev])), B.Octets.len(B.Octets.le32(rsdt))), BL.octets_len_append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))) : {Nat.add(B.Octets.len(P.AcpiRsdp.signature()), Nat.add(B.Octets.len(B.Octets.of_list([k])), Nat.add(B.Octets.len(oem), _))) == 20n : Nat}
73  %Equal.sym(Nat, B.Octets.len(oem), 6n, oem6) : {Nat.add(B.Octets.len(P.AcpiRsdp.signature()), Nat.add(B.Octets.len(B.Octets.of_list([k])), Nat.add(_, Nat.add(B.Octets.len(B.Octets.of_list([rev])), B.Octets.len(B.Octets.le32(rsdt)))))) == 20n : Nat}
74  %Equal.sym(Nat, B.Octets.len(B.Octets.of_list([k])), B.len([k]), BL.octets_len_of_list([k])) : {Nat.add(B.Octets.len(P.AcpiRsdp.signature()), Nat.add(_, Nat.add(6n, Nat.add(B.Octets.len(B.Octets.of_list([rev])), B.Octets.len(B.Octets.le32(rsdt)))))) == 20n : Nat}
75  %Equal.sym(Nat, B.Octets.len(B.Octets.of_list([rev])), B.len([rev]), BL.octets_len_of_list([rev])) : {Nat.add(B.Octets.len(P.AcpiRsdp.signature()), Nat.add(B.len([k]), Nat.add(6n, Nat.add(_, B.Octets.len(B.Octets.le32(rsdt)))))) == 20n : Nat}
76  %Equal.sym(Nat, B.Octets.len(B.Octets.le32(rsdt)), 4n, BL.octets_len_le32(rsdt)) : {Nat.add(B.Octets.len(P.AcpiRsdp.signature()), Nat.add(B.len([k]), Nat.add(6n, Nat.add(B.len([rev]), _)))) == 20n : Nat}
77  {==}
78
79def ckr.at15(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +rev8: {B.byte(rev) == rev : U32}) -> {B.Octets.at(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 15n) == Some{rev} : Maybe<&2, U32>}:
80  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), Nat.add(B.Octets.len(P.AcpiRsdp.signature()), 7n)), B.Octets.at(B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), 7n), BL.octets_at_append_add(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), 7n)) : {_ == Some{rev} : Maybe<&2, U32>}
81  %Equal.cong(Nat, Nat, z => Nat.add(z, 6n), B.Octets.len(B.Octets.of_list([k])), B.len([k]), BL.octets_len_of_list([k])) : {B.Octets.at(B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), _) == Some{rev} : Maybe<&2, U32>}
82  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), Nat.add(B.Octets.len(B.Octets.of_list([k])), 6n)), B.Octets.at(B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))), 6n), BL.octets_at_append_add(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))), 6n)) : {_ == Some{rev} : Maybe<&2, U32>}
83  %Equal.cong(Nat, Nat, z => Nat.add(z, 0n), B.Octets.len(oem), 6n, oem6) : {B.Octets.at(B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))), _) == Some{rev} : Maybe<&2, U32>}
84  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))), Nat.add(B.Octets.len(oem), 0n)), B.Octets.at(B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)), 0n), BL.octets_at_append_add(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)), 0n)) : {_ == Some{rev} : Maybe<&2, U32>}
85  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)), 0n), B.Octets.at(B.Octets.of_list([rev]), 0n), BL.octets_at_append_lt(B.Octets.of_list([rev]), B.Octets.le32(rsdt), 0n, WH.ckw.lt01(rev))) : {_ == Some{rev} : Maybe<&2, U32>}
86  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.of_list([rev]), 0n), B.at(B.Octets.to_list(B.Octets.of_list([rev])), 0n), BL.octets_at_list(B.Octets.of_list([rev]), 0n)) : {_ == Some{rev} : Maybe<&2, U32>}
87  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list([rev])), B.mask([rev]), BL.octets_to_of([rev])) : {B.at(_, 0n) == Some{rev} : Maybe<&2, U32>}
88  %Equal.sym(U32, B.byte(rev), rev, rev8) : {Some{B.byte(_)} == Some{rev} : Maybe<&2, U32>}
89  %Equal.sym(U32, B.byte(rev), rev, rev8) : {Some{_} == Some{rev} : Maybe<&2, U32>}
90  {==}
91
92def ckr.u16(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32) -> {B.Octets.le32_at(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 16n) == Some{rsdt} : Maybe<&2, U32>}:
93  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), Nat.add(B.Octets.len(P.AcpiRsdp.signature()), 8n)), B.Octets.le32_at(B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), 8n), BL.octets_le32_at_append_add(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), 8n)) : {_ == Some{rsdt} : Maybe<&2, U32>}
94  %Equal.cong(Nat, Nat, z => Nat.add(z, 7n), B.Octets.len(B.Octets.of_list([k])), B.len([k]), BL.octets_len_of_list([k])) : {B.Octets.le32_at(B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), _) == Some{rsdt} : Maybe<&2, U32>}
95  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), Nat.add(B.Octets.len(B.Octets.of_list([k])), 7n)), B.Octets.le32_at(B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))), 7n), BL.octets_le32_at_append_add(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))), 7n)) : {_ == Some{rsdt} : Maybe<&2, U32>}
96  %Equal.cong(Nat, Nat, z => Nat.add(z, 1n), B.Octets.len(oem), 6n, oem6) : {B.Octets.le32_at(B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))), _) == Some{rsdt} : Maybe<&2, U32>}
97  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))), Nat.add(B.Octets.len(oem), 1n)), B.Octets.le32_at(B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)), 1n), BL.octets_le32_at_append_add(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)), 1n)) : {_ == Some{rsdt} : Maybe<&2, U32>}
98  %Equal.cong(Nat, Nat, z => Nat.add(z, 0n), B.Octets.len(B.Octets.of_list([rev])), B.len([rev]), BL.octets_len_of_list([rev])) : {B.Octets.le32_at(B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)), _) == Some{rsdt} : Maybe<&2, U32>}
99  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)), Nat.add(B.Octets.len(B.Octets.of_list([rev])), 0n)), B.Octets.le32_at(B.Octets.le32(rsdt), 0n), BL.octets_le32_at_append_add(B.Octets.of_list([rev]), B.Octets.le32(rsdt), 0n)) : {_ == Some{rsdt} : Maybe<&2, U32>}
100  BL.octets_le32_round_trip(rsdt)
101
102def ckr.le6(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}) -> {Nat.is_le(Nat.add(0n, 6n), B.Octets.len(oem)) == True{} : Bool}:
103  %Equal.sym(Nat, B.Octets.len(oem), 6n, oem6) : {Nat.is_le(Nat.add(0n, 6n), _) == True{} : Bool}
104  {==}
105
106def ckr.sl9(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32) -> {B.Octets.slice(9n, 6n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) == oem : B.Octets}:
107  %Equal.sym(B.Octets, B.Octets.slice(Nat.add(B.Octets.len(P.AcpiRsdp.signature()), 1n), 6n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), B.Octets.slice(1n, 6n, B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), BL.octets_slice_append_add(P.AcpiRsdp.signature(), 1n, 6n, B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) : {_ == oem : B.Octets}
108  %Equal.cong(Nat, Nat, z => Nat.add(z, 0n), B.Octets.len(B.Octets.of_list([k])), B.len([k]), BL.octets_len_of_list([k])) : {B.Octets.slice(_, 6n, B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) == oem : B.Octets}
109  %Equal.sym(B.Octets, B.Octets.slice(Nat.add(B.Octets.len(B.Octets.of_list([k])), 0n), 6n, B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.slice(0n, 6n, B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), BL.octets_slice_append_add(B.Octets.of_list([k]), 0n, 6n, B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : {_ == oem : B.Octets}
110  %Equal.sym(B.Octets, B.Octets.slice(0n, 6n, B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), B.Octets.slice(0n, 6n, oem), BL.octets_slice_append_le(0n, 6n, oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)), ckr.le6(oem, oem6))) : {_ == oem : B.Octets}
111  %Equal.sym(B.Octets, B.Octets.drop(0n, oem), oem, BL.octets_drop_zero(oem)) : {B.Octets.take(6n, _) == oem : B.Octets}
112  %oem6 : {B.Octets.take(_, oem) == oem : B.Octets}
113  BL.octets_take_len(oem)
114
115def ckr.hlt8(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32) -> {Nat.is_lt(8n, B.Octets.len(B.Octets.concat([P.AcpiRsdp.signature(), B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]))) == True{} : Bool}:
116  %Equal.sym(B.Octets, B.Octets.concat([P.AcpiRsdp.signature(), B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), ckr.vr(oem, oem6, rev, rsdt)) : {Nat.is_lt(8n, B.Octets.len(_)) == True{} : Bool}
117  %Equal.sym(Nat, B.Octets.len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), 20n, ckr.l20(0, oem, oem6, rev, rsdt)) : {Nat.is_lt(8n, _) == True{} : Bool}
118  {==}
119
120def ckr.ok1(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32) -> {C.AcpiChecksum.ok(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) == True{} : Bool}:
121  %ckr.fa(oem, oem6, rev, rsdt) : {C.AcpiChecksum.ok(_) == True{} : Bool}
122  CL.fix_ok(8n, B.Octets.concat([P.AcpiRsdp.signature(), B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]), ckr.hlt8(oem, oem6, rev, rsdt))
123
124# The laws
125
126def Laws.rsdp_v1_round_trip(oem, oem6, rev, rev8, rev2, rsdt):
127  %Equal.sym(B.Octets, P.rs.v1(oem, rev, rsdt), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), ckr.fa(oem, oem6, rev, rsdt)) : {P.AcpiRsdp.parse(_) == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
128  %Equal.sym(Nat, B.Octets.len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), 20n, ckr.l20(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt)) : {P.rs.p1(Nat.is_le(20n, _), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
129  %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(P.AcpiRsdp.signature()), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), P.AcpiRsdp.signature(), BL.octets_take_append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) : {P.rs.p2(B.Octets.is_eq(_, P.AcpiRsdp.signature()), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
130  %Equal.sym(Bool, B.Octets.is_eq(P.AcpiRsdp.signature(), P.AcpiRsdp.signature()), True{}, BL.octets_is_eq_refl(P.AcpiRsdp.signature())) : {P.rs.p2(_, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
131  %ckr.l20(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt) : {P.rs.p3(C.AcpiChecksum.ok(B.Octets.take(_, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
132  %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), BL.octets_take_len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))) : {P.rs.p3(C.AcpiChecksum.ok(_), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
133  %Equal.sym(Bool, C.AcpiChecksum.ok(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), True{}, ckr.ok1(oem, oem6, rev, rsdt)) : {P.rs.p3(_, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
134  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 15n), Some{rev}, ckr.at15(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, rev8)) : {P.rs.p4(U32.is_lt(Maybe.default(&2, U32, _, 0), 2), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
135  %Equal.sym(Bool, U32.is_lt(rev, 2), True{}, rev2) : {P.rs.p4(_, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
136  %Equal.sym(B.Octets, B.Octets.slice(9n, 6n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, ckr.sl9(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt)) : {Done{P.AcpiRsdp{_, F.AcpiF.u8(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 15n), F.AcpiF.u32(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 16n), None{}}} == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
137  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 15n), Some{rev}, ckr.at15(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, rev8)) : {Done{P.AcpiRsdp{oem, Maybe.default(&2, U32, _, 0), F.AcpiF.u32(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 16n), None{}}} == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
138  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 16n), Some{rsdt}, ckr.u16(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt)) : {Done{P.AcpiRsdp{oem, rev, Maybe.default(&2, U32, _, 0), None{}}} == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
139  {==}
140
141# Revision 2: the 20 bytes, then Length 36 and XsdtAddress (32 bytes),
142# then the extended checksum byte and three reserved bytes
143
144def ckr.le_by(+n: Nat, +o: B.Octets, +m: Nat, +e: {B.Octets.len(o) == m : Nat}, +h: {Nat.is_le(n, m) == True{} : Bool}) -> {Nat.is_le(n, B.Octets.len(o)) == True{} : Bool}:
145  %Equal.sym(Nat, B.Octets.len(o), m, e) : {Nat.is_le(n, _) == True{} : Bool}
146  h
147
148def ckr.lt_by(+n: Nat, +o: B.Octets, +m: Nat, +e: {B.Octets.len(o) == m : Nat}, +h: {Nat.is_lt(n, m) == True{} : Bool}) -> {Nat.is_lt(n, B.Octets.len(o)) == True{} : Bool}:
149  %Equal.sym(Nat, B.Octets.len(o), m, e) : {Nat.is_lt(n, _) == True{} : Bool}
150  h
151
152def ckr.lp(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64) -> {B.Octets.len(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)))) == 32n : Nat}:
153  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)))), Nat.add(B.Octets.len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), B.Octets.len(B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)))), BL.octets_len_append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)))) : {_ == 32n : Nat}
154  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), Nat.add(B.Octets.len(B.Octets.le32(36)), B.Octets.len(B.Octets.le64(x))), BL.octets_len_append(B.Octets.le32(36), B.Octets.le64(x))) : {Nat.add(B.Octets.len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), _) == 32n : Nat}
155  %Equal.sym(Nat, B.Octets.len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), 20n, ckr.l20(k, oem, oem6, rev, rsdt)) : {Nat.add(_, Nat.add(B.Octets.len(B.Octets.le32(36)), B.Octets.len(B.Octets.le64(x)))) == 32n : Nat}
156  %Equal.sym(Nat, B.Octets.len(B.Octets.le32(36)), 4n, BL.octets_len_le32(36)) : {Nat.add(20n, Nat.add(_, B.Octets.len(B.Octets.le64(x)))) == 32n : Nat}
157  %Equal.sym(Nat, B.Octets.len(B.Octets.le64(x)), 8n, BL.octets_len_le64(x)) : {Nat.add(20n, Nat.add(4n, _)) == 32n : Nat}
158  {==}
159
160def ckr.t8(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64, +y: B.Octets) -> {B.Octets.take(8n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y)) == P.AcpiRsdp.signature() : B.Octets}:
161  %Equal.sym(B.Octets, B.Octets.take(8n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y)), B.Octets.take(8n, B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)))), BL.octets_take_append_le(8n, B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y, ckr.le_by(8n, B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 32n, ckr.lp(k, oem, oem6, rev, rsdt, x), {==}))) : {_ == P.AcpiRsdp.signature() : B.Octets}
162  %Equal.sym(B.Octets, B.Octets.take(8n, B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)))), B.Octets.take(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), BL.octets_take_append_le(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), ckr.le_by(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 20n, ckr.l20(k, oem, oem6, rev, rsdt), {==}))) : {_ == P.AcpiRsdp.signature() : B.Octets}
163  BL.octets_take_append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))
164
165def ckr.t20(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64, +y: B.Octets) -> {B.Octets.take(20n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y)) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}:
166  %Equal.sym(B.Octets, B.Octets.take(20n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y)), B.Octets.take(20n, B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)))), BL.octets_take_append_le(20n, B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y, ckr.le_by(20n, B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 32n, ckr.lp(k, oem, oem6, rev, rsdt, x), {==}))) : {_ == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
167  %Equal.sym(B.Octets, B.Octets.take(20n, B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)))), B.Octets.take(20n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), BL.octets_take_append_le(20n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), ckr.le_by(20n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 20n, ckr.l20(k, oem, oem6, rev, rsdt), {==}))) : {_ == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
168  %ckr.l20(k, oem, oem6, rev, rsdt) : {B.Octets.take(_, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
169  BL.octets_take_len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))
170
171def ckr.a15(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64, +y: B.Octets, +rev8: {B.byte(rev) == rev : U32}) -> {B.Octets.at(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y), 15n) == Some{rev} : Maybe<&2, U32>}:
172  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y), 15n), B.Octets.at(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 15n), BL.octets_at_append_lt(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y, 15n, ckr.lt_by(15n, B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 32n, ckr.lp(k, oem, oem6, rev, rsdt, x), {==}))) : {_ == Some{rev} : Maybe<&2, U32>}
173  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 15n), B.Octets.at(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 15n), BL.octets_at_append_lt(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), 15n, ckr.lt_by(15n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 20n, ckr.l20(k, oem, oem6, rev, rsdt), {==}))) : {_ == Some{rev} : Maybe<&2, U32>}
174  ckr.at15(k, oem, oem6, rev, rsdt, rev8)
175
176def ckr.s9(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64, +y: B.Octets) -> {B.Octets.slice(9n, 6n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y)) == oem : B.Octets}:
177  %Equal.sym(B.Octets, B.Octets.slice(9n, 6n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y)), B.Octets.slice(9n, 6n, B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)))), BL.octets_slice_append_le(9n, 6n, B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y, ckr.le_by(Nat.add(9n, 6n), B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 32n, ckr.lp(k, oem, oem6, rev, rsdt, x), {==}))) : {_ == oem : B.Octets}
178  %Equal.sym(B.Octets, B.Octets.slice(9n, 6n, B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)))), B.Octets.slice(9n, 6n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), BL.octets_slice_append_le(9n, 6n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), ckr.le_by(Nat.add(9n, 6n), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 20n, ckr.l20(k, oem, oem6, rev, rsdt), {==}))) : {_ == oem : B.Octets}
179  ckr.sl9(k, oem, oem6, rev, rsdt)
180
181def ckr.w16(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64, +y: B.Octets) -> {B.Octets.le32_at(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y), 16n) == Some{rsdt} : Maybe<&2, U32>}:
182  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y), 16n), B.Octets.le32_at(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 16n), BL.octets_le32_at_append_le(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y, 16n, ckr.le_by(Nat.add(16n, 4n), B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 32n, ckr.lp(k, oem, oem6, rev, rsdt, x), {==}))) : {_ == Some{rsdt} : Maybe<&2, U32>}
183  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 16n), B.Octets.le32_at(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 16n), BL.octets_le32_at_append_le(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), 16n, ckr.le_by(Nat.add(16n, 4n), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), 20n, ckr.l20(k, oem, oem6, rev, rsdt), {==}))) : {_ == Some{rsdt} : Maybe<&2, U32>}
184  ckr.u16(k, oem, oem6, rev, rsdt)
185
186def ckr.w20(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64, +y: B.Octets) -> {B.Octets.le32_at(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y), 20n) == Some{36} : Maybe<&2, U32>}:
187  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y), 20n), B.Octets.le32_at(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 20n), BL.octets_le32_at_append_le(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y, 20n, ckr.le_by(Nat.add(20n, 4n), B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 32n, ckr.lp(k, oem, oem6, rev, rsdt, x), {==}))) : {_ == Some{36} : Maybe<&2, U32>}
188  %Equal.cong(Nat, Nat, z => Nat.add(z, 0n), B.Octets.len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), 20n, ckr.l20(k, oem, oem6, rev, rsdt)) : {B.Octets.le32_at(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), _) == Some{36} : Maybe<&2, U32>}
189  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), Nat.add(B.Octets.len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), 0n)), B.Octets.le32_at(B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), 0n), BL.octets_le32_at_append_add(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), 0n)) : {_ == Some{36} : Maybe<&2, U32>}
190  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), 0n), B.Octets.le32_at(B.Octets.le32(36), 0n), BL.octets_le32_at_append_le(B.Octets.le32(36), B.Octets.le64(x), 0n, WH.ckw.l4(36))) : {_ == Some{36} : Maybe<&2, U32>}
191  BL.octets_le32_round_trip(36)
192
193def ckr.q24(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64, +y: B.Octets) -> {B.Octets.le64_at(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y), 24n) == Some{x} : Maybe<&2, W.W64>}:
194  %Equal.sym(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y), 24n), B.Octets.le64_at(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 24n), BL.octets_le64_at_append_le(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), y, 24n, ckr.le_by(Nat.add(24n, 8n), B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 32n, ckr.lp(k, oem, oem6, rev, rsdt, x), {==}))) : {_ == Some{x} : Maybe<&2, W.W64>}
195  %Equal.cong(Nat, Nat, z => Nat.add(z, 4n), B.Octets.len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), 20n, ckr.l20(k, oem, oem6, rev, rsdt)) : {B.Octets.le64_at(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), _) == Some{x} : Maybe<&2, W.W64>}
196  %Equal.sym(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), Nat.add(B.Octets.len(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), 4n)), B.Octets.le64_at(B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), 4n), BL.octets_le64_at_append_add(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), 4n)) : {_ == Some{x} : Maybe<&2, W.W64>}
197  %Equal.cong(Nat, Nat, z => Nat.add(z, 0n), B.Octets.len(B.Octets.le32(36)), 4n, BL.octets_len_le32(36)) : {B.Octets.le64_at(B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), _) == Some{x} : Maybe<&2, W.W64>}
198  %Equal.sym(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), Nat.add(B.Octets.len(B.Octets.le32(36)), 0n)), B.Octets.le64_at(B.Octets.le64(x), 0n), BL.octets_le64_at_append_add(B.Octets.le32(36), B.Octets.le64(x), 0n)) : {_ == Some{x} : Maybe<&2, W.W64>}
199  BL.octets_le64_round_trip(x)
200
201def ckr.z4() -> {B.Octets.zeros(4n) == B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)) : B.Octets}:
202  {==}
203
204def ckr.w2r(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64) -> {B.Octets.concat([B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}:
205  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), [B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]}), B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.concat([B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)])), BL.octets_concat_cons(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), [B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)])) : {_ == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
206  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.le32(36), [B.Octets.le64(x), B.Octets.zeros(4n)]}), B.Octets.append(B.Octets.le32(36), B.Octets.concat([B.Octets.le64(x), B.Octets.zeros(4n)])), BL.octets_concat_cons(B.Octets.le32(36), [B.Octets.le64(x), B.Octets.zeros(4n)])) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), _) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
207  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.le64(x), [B.Octets.zeros(4n)]}), B.Octets.append(B.Octets.le64(x), B.Octets.concat([B.Octets.zeros(4n)])), BL.octets_concat_cons(B.Octets.le64(x), [B.Octets.zeros(4n)])) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), _)) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
208  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.zeros(4n), Nil{}}), B.Octets.append(B.Octets.zeros(4n), B.Octets.concat(Nil{})), BL.octets_concat_cons(B.Octets.zeros(4n), Nil{})) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), _))) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
209  %Equal.sym(B.Octets, B.Octets.concat(Nil{}), B.Octets.empty(), BL.octets_concat_nil()) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), B.Octets.append(B.Octets.zeros(4n), _)))) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
210  %Equal.sym(B.Octets, B.Octets.append(B.Octets.zeros(4n), B.Octets.empty()), B.Octets.zeros(4n), BL.octets_append_empty_r(B.Octets.zeros(4n))) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), _))) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
211  %Equal.sym(B.Octets, B.Octets.zeros(4n), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)), ckr.z4()) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), _))) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
212  %Equal.sym(B.Octets, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))), B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)))), BL.octets_append_assoc(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)))) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))) == _ : B.Octets}
213  %Equal.sym(B.Octets, B.Octets.append(B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)))), BL.octets_append_assoc(B.Octets.le32(36), B.Octets.le64(x), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)))) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))) == B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), _) : B.Octets}
214  {==}
215
216def ckr.len36(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64, +c: U32) -> {B.Octets.len(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([c]), B.Octets.zeros(3n)))) == 36n : Nat}:
217  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([c]), B.Octets.zeros(3n)))), Nat.add(B.Octets.len(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)))), B.Octets.len(B.Octets.append(B.Octets.of_list([c]), B.Octets.zeros(3n)))), BL.octets_len_append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([c]), B.Octets.zeros(3n)))) : {_ == 36n : Nat}
218  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.of_list([c]), B.Octets.zeros(3n))), Nat.add(B.Octets.len(B.Octets.of_list([c])), B.Octets.len(B.Octets.zeros(3n))), BL.octets_len_append(B.Octets.of_list([c]), B.Octets.zeros(3n))) : {Nat.add(B.Octets.len(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)))), _) == 36n : Nat}
219  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)))), 32n, ckr.lp(k, oem, oem6, rev, rsdt, x)) : {Nat.add(_, Nat.add(B.Octets.len(B.Octets.of_list([c])), B.Octets.len(B.Octets.zeros(3n)))) == 36n : Nat}
220  %Equal.sym(Nat, B.Octets.len(B.Octets.of_list([c])), B.len([c]), BL.octets_len_of_list([c])) : {Nat.add(32n, Nat.add(_, B.Octets.len(B.Octets.zeros(3n)))) == 36n : Nat}
221  {==}
222
223def ckr.f2(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64) -> {C.AcpiChecksum.fix(32n, B.Octets.concat([P.rs.v1(oem, rev, rsdt), B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)])) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))) : B.Octets}:
224  %Equal.sym(B.Octets, P.rs.v1(oem, rev, rsdt), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), ckr.fa(oem, oem6, rev, rsdt)) : {C.AcpiChecksum.fix(32n, B.Octets.concat([_, B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)])) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))) : B.Octets}
225  %Equal.sym(B.Octets, B.Octets.concat([B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]), B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))), ckr.w2r(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x)) : {C.AcpiChecksum.fix(32n, _) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))) : B.Octets}
226  WH.ckw.gfix(32n, B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), 0, B.Octets.zeros(3n), ckr.lp(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x))
227
228def ckr.hlt32(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64) -> {Nat.is_lt(32n, B.Octets.len(B.Octets.concat([P.rs.v1(oem, rev, rsdt), B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]))) == True{} : Bool}:
229  %Equal.sym(B.Octets, P.rs.v1(oem, rev, rsdt), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), ckr.fa(oem, oem6, rev, rsdt)) : {Nat.is_lt(32n, B.Octets.len(B.Octets.concat([_, B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]))) == True{} : Bool}
230  %Equal.sym(B.Octets, B.Octets.concat([B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]), B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))), ckr.w2r(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x)) : {Nat.is_lt(32n, B.Octets.len(_)) == True{} : Bool}
231  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)))), 36n, ckr.len36(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x, 0)) : {Nat.is_lt(32n, _) == True{} : Bool}
232  {==}
233
234def ckr.ok2(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64) -> {C.AcpiChecksum.ok(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == True{} : Bool}:
235  %ckr.f2(oem, oem6, rev, rsdt, x) : {C.AcpiChecksum.ok(_) == True{} : Bool}
236  CL.fix_ok(32n, B.Octets.concat([P.rs.v1(oem, rev, rsdt), B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]), ckr.hlt32(oem, oem6, rev, rsdt, x))
237
238def Laws.rsdp_v2_round_trip(oem, oem6, rev, rev8, rev2, rsdt, l, x):
239  %Equal.sym(B.Octets, C.AcpiChecksum.fix(32n, B.Octets.concat([P.rs.v1(oem, rev, rsdt), B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)])), B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))), ckr.f2(oem, oem6, rev, rsdt, x)) : {P.AcpiRsdp.parse(_) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
240  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))), 36n, ckr.len36(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x, C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)))))) : {P.rs.p1(Nat.is_le(20n, _), B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
241  %Equal.sym(B.Octets, B.Octets.take(8n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))), P.AcpiRsdp.signature(), ckr.t8(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) : {P.rs.p2(B.Octets.is_eq(_, P.AcpiRsdp.signature()), B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
242  %Equal.sym(Bool, B.Octets.is_eq(P.AcpiRsdp.signature(), P.AcpiRsdp.signature()), True{}, BL.octets_is_eq_refl(P.AcpiRsdp.signature())) : {P.rs.p2(_, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
243  %Equal.sym(B.Octets, B.Octets.take(20n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), ckr.t20(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) : {P.rs.p3(C.AcpiChecksum.ok(_), B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
244  %Equal.sym(Bool, C.AcpiChecksum.ok(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), True{}, ckr.ok1(oem, oem6, rev, rsdt)) : {P.rs.p3(_, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
245  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))), 15n), Some{rev}, ckr.a15(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)), rev8)) : {P.rs.p4(U32.is_lt(Maybe.default(&2, U32, _, 0), 2), B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
246  %Equal.sym(Bool, U32.is_lt(rev, 2), False{}, rev2) : {P.rs.p4(_, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
247  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))), 36n, ckr.len36(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x, C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)))))) : {P.rs.p5(Nat.is_le(36n, _), B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
248  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))), 20n), Some{36}, ckr.w20(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) : {P.rs.p6(Bool.and(Nat.is_le(36n, U32.to_nat(Maybe.default(&2, U32, _, 0))), Nat.is_le(U32.to_nat(Maybe.default(&2, U32, _, 0)), B.Octets.len(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))))), Maybe.default(&2, U32, _, 0), B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
249  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))), 36n, ckr.len36(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x, C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)))))) : {P.rs.p6(Bool.and(Nat.is_le(36n, U32.to_nat(36)), Nat.is_le(U32.to_nat(36), _)), 36, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
250  %ckr.len36(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x, C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))) : {P.rs.p7(C.AcpiChecksum.ok(B.Octets.take(_, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))))), 36, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
251  %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))), B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))), B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))), BL.octets_take_len(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))))) : {P.rs.p7(C.AcpiChecksum.ok(_), 36, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
252  %Equal.sym(Bool, C.AcpiChecksum.ok(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))), True{}, ckr.ok2(oem, oem6, rev, rsdt, x)) : {P.rs.p7(_, 36, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
253  %Equal.sym(B.Octets, B.Octets.slice(9n, 6n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))), oem, ckr.s9(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) : {Done{P.AcpiRsdp{_, F.AcpiF.u8(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))), 15n), F.AcpiF.u32(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))), 16n), Some{P.AcpiRsdpExt{36, F.AcpiF.u64(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))), 24n)}}}} == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
254  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))), 15n), Some{rev}, ckr.a15(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)), rev8)) : {Done{P.AcpiRsdp{oem, Maybe.default(&2, U32, _, 0), F.AcpiF.u32(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))), 16n), Some{P.AcpiRsdpExt{36, F.AcpiF.u64(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))), 24n)}}}} == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
255  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))), 16n), Some{rsdt}, ckr.w16(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) : {Done{P.AcpiRsdp{oem, rev, Maybe.default(&2, U32, _, 0), Some{P.AcpiRsdpExt{36, F.AcpiF.u64(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))), 24n)}}}} == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
256  %Equal.sym(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n))), 24n), Some{x}, ckr.q24(C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))), oem, oem6, rev, rsdt, x, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) : {Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, Maybe.default(&2, W.W64, _, W.W64.zero())}}}} == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
257  {==}
258
259def Laws.rsdp_round_trip_example():
260  {==}