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.
7	import Base
8	import bend-osdev-word64@0.1.1.1/word64.bend as W
9	import bend-osdev-bytes@0.1.1.1/bytes.bend as B
10	import ./error.bend as E
11	import ./rsdp.bend as P
12	
13	law 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	
22	law 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
34	law 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}