LAWSChecksum.fix_ok: law of bend-osdev-acpi@0.1.2.0
Import: import bend-osdev-acpi@0.1.2.0/LAWS_checksum.bend as LAWSChecksum
Lines 8-12 of bend-osdev-acpi@0.1.2.0/LAWS_checksum.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/LAWS_checksum.bend&start_line=8&end_line=12

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

law fix_ok:
  for +i: Nat
  for +o: B.Octets
  for +h: {Nat.is_lt(i, B.Octets.len(o)) == True{} : Bool}
  {C.AcpiChecksum.ok(C.AcpiChecksum.fix(i, o)) == True{} : Bool}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend&name=ckp.fixzero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/checksum.bend&name=AcpiChecksum.fix
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/checksum.bend&name=AcpiChecksum.ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/checksum.bend&name=AcpiChecksum.sum
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_eq_value