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.
4	import Base
5	import bend-osdev-bytes@0.1.1.1/bytes.bend as B
6	import ./checksum.bend as C
7	
8	law 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
15	law 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}