PROOFRsdp.ckr.hlt32: def of bend-osdev-acpi@0.1.2.0
Import: import bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend as PROOFRsdp
Lines 228-232 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=228&end_line=232

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

def ckr.hlt32(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64) -> {Nat.is_lt(32n, B.Octets.len(B.Octets.concat([P.rs.v1(oem, rev, rsdt), B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]))) == True{} : Bool}:
  %Equal.sym(B.Octets, P.rs.v1(oem, rev, rsdt), 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))))), ckr.fa(oem, oem6, rev, rsdt)) : {Nat.is_lt(32n, B.Octets.len(B.Octets.concat([_, B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]))) == True{} : Bool}
  %Equal.sym(B.Octets, B.Octets.concat([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.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]), 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))), ckr.w2r(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)))))), oem, oem6, rev, rsdt, x)) : {Nat.is_lt(32n, B.Octets.len(_)) == True{} : Bool}
  %Equal.sym(Nat, B.Octets.len(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)))), 36n, ckr.len36(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)))))), oem, oem6, rev, rsdt, x, 0)) : {Nat.is_lt(32n, _) == True{} : Bool}
  {==}

Uses (21):
  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=List
  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_lt
  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/PROOF_rsdp.bend&name=ckr.fa
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend&name=ckr.len36
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend&name=ckr.w2r
  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/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