LAWS_rsdp.bend

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

1# The RSDP's whole round trip (5.2.5.3), for every input: what
2# AcpiRsdp.build writes, AcpiRsdp.parse reads back, both checksums passing
3# (LAWS_checksum.bend). A revision 0 or 1 RSDP is the first 20 bytes; a
4# revision 2 or later one adds the extended fields, its Length being the 36
5# that build writes. The OEMID must be 6 bytes (build fits it to 6) and the
6# revision a byte.
7import Base
8import bend-osdev-word64@0.1.1.1/word64.bend as W
9import bend-osdev-bytes@0.1.1.1/bytes.bend as B
10import bend-osdev-acpi@0.1.2.0/error.bend as E
11import bend-osdev-acpi@0.1.2.0/rsdp.bend as P
12
13law rsdp_v1_round_trip:
14  for +oem: B.Octets
15  for +oem6: {B.Octets.len(oem) == 6n : Nat}
16  for +rev: U32
17  for +rev8: {B.byte(rev) == rev : U32}
18  for +rev2: {U32.is_lt(rev, 2) == True{} : Bool}
19  for +rsdt: U32
20  {P.AcpiRsdp.parse(P.AcpiRsdp.build(P.AcpiRsdp{oem, rev, rsdt, None{}})) == Done{P.AcpiRsdp{oem, rev, rsdt, None{}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
21
22law rsdp_v2_round_trip:
23  for +oem: B.Octets
24  for +oem6: {B.Octets.len(oem) == 6n : Nat}
25  for +rev: U32
26  for +rev8: {B.byte(rev) == rev : U32}
27  for +rev2: {U32.is_lt(rev, 2) == False{} : Bool}
28  for +rsdt: U32
29  for +l: U32
30  for +x: W.W64
31  {P.AcpiRsdp.parse(P.AcpiRsdp.build(P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{l, x}}})) == Done{P.AcpiRsdp{oem, rev, rsdt, Some{P.AcpiRsdpExt{36, x}}}} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}
32
33# the hypotheses hold at an example: a 6-byte OEMID, revisions 1 and 2
34law rsdp_round_trip_example:
35  {(B.Octets.len(B.Octets.of_string("BENDOS")), B.byte(2), U32.is_lt(1, 2), U32.is_lt(2, 2)) == (6n, 2, True{}, False{}) : Nat & U32 & Bool & Bool}