LAWS_checksum.bend

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

1# The checksum (5.2.6), for every input: AcpiChecksum.fix(i, o), which
2# writes the checksum byte at offset i, makes the bytes sum to zero modulo
3# 256 whenever o has a byte i, whatever the other bytes are.
4import Base
5import bend-osdev-bytes@0.1.1.1/bytes.bend as B
6import bend-osdev-acpi@0.1.2.0/checksum.bend as C
7
8law fix_ok:
9  for +i: Nat
10  for +o: B.Octets
11  for +h: {Nat.is_lt(i, B.Octets.len(o)) == True{} : Bool}
12  {C.AcpiChecksum.ok(C.AcpiChecksum.fix(i, o)) == True{} : Bool}
13
14# the hypothesis holds, and the law with it, at an example
15law fix_example:
16  {(Nat.is_lt(1n, B.Octets.len(B.Octets.of_list([7, 200, 99]))), C.AcpiChecksum.ok(C.AcpiChecksum.fix(1n, B.Octets.of_list([7, 200, 99])))) == (True{}, True{}) : Bool & Bool}