law fix_ok

bend-osdev-acpi@0.1.2.0 · LAWS_checksum.bend:8

import bend-osdev-acpi@0.1.2.0/LAWS_checksum.bend as LAWSChecksum
import Base
import bend-osdev-bytes@0.1.1.1/bytes.bend as B
import bend-osdev-acpi@0.1.2.0/checksum.bend as C

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}

Uses (14)

Used by (3)