PROOFChecksum.ckp.sumv: def of bend-osdev-acpi@0.1.2.0
Import: import bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend as PROOFChecksum
Lines 162-164 of bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend&start_line=162&end_line=164

import Base
import bend-osdev-bytes@0.1.1.1/bytes.bend as B
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-acpi@0.1.2.0/checksum.bend as C

def ckp.sumv(+o: B.Octets) -> {U32.to_nat(C.AcpiChecksum.sum(o)) == U.U32Nat.low(8n, ckp.ns(B.Octets.to_list(o))) : Nat}:
  %Equal.sym(Nat, U32.to_nat(U32.and(255, C.ck.sum.go(B.Octets.to_list(o), 0))), U.U32Nat.low(8n, U32.to_nat(C.ck.sum.go(B.Octets.to_list(o), 0))), ckp.am(C.ck.sum.go(B.Octets.to_list(o), 0))) : {_ == U.U32Nat.low(8n, ckp.ns(B.Octets.to_list(o))) : Nat}
  ckp.go(B.Octets.to_list(o), 0)

Uses (12):
  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=U32.and
  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.am
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend&name=ckp.go
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend&name=ckp.ns
  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-acpi@0.1.2.0/checksum.bend&name=ck.sum.go
  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.to_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.low