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

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/PROOF_whole.bend as WH

def ckr.f2(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64) -> {C.AcpiChecksum.fix(32n, B.Octets.concat([P.rs.v1(oem, rev, 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([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))) : B.Octets}:
  %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)) : {C.AcpiChecksum.fix(32n, B.Octets.concat([_, 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([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))) : B.Octets}
  %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)) : {C.AcpiChecksum.fix(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([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))) : B.Octets}
  WH.ckw.gfix(32n, 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))), 0, B.Octets.zeros(3n), ckr.lp(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))

Uses (21):
  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=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.lp
  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/PROOF_whole.bend&name=ckw.gfix
  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.fix
  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