PROOFRsdp.ckr.ok2: def of bend-osdev-acpi@0.1.2.0
Import: import bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend as PROOFRsdp
Lines 234-236 of bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend&start_line=234&end_line=236

import Base
import bend-osdev-word64@0.1.1.1/word64.bend as W
import bend-osdev-bytes@0.1.1.1/bytes.bend as B
import bend-osdev-acpi@0.1.2.0/checksum.bend as C
import bend-osdev-acpi@0.1.2.0/rsdp.bend as P
import bend-osdev-acpi@0.1.2.0/LAWS_checksum.bend as CL

def ckr.ok2(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64) -> {C.AcpiChecksum.ok(B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(32n, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(8n, B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))))]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))]), B.Octets.zeros(3n)))) == True{} : Bool}:
  %ckr.f2(oem, oem6, rev, rsdt, x) : {C.AcpiChecksum.ok(_) == True{} : Bool}
  CL.fix_ok(32n, B.Octets.concat([P.rs.v1(oem, rev, rsdt), B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]), ckr.hlt32(oem, oem6, rev, rsdt, x))

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/LAWS_checksum.bend&name=fix_ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend&name=ckr.f2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend&name=ckr.hlt32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/checksum.bend&name=AcpiChecksum.byte_for
  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/rsdp.bend&name=AcpiRsdp.signature
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/rsdp.bend&name=rs.v1
  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.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.concat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.le32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.le64
  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-bytes@0.1.1.1/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.zeros
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.1/word64.bend&name=W64