PROOFWhole.ckw.hpfit: def of bend-osdev-acpi@0.1.2.0
Import: import bend-osdev-acpi@0.1.2.0/PROOF_whole.bend as PROOFWhole
Lines 233-238 of bend-osdev-acpi@0.1.2.0/PROOF_whole.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_whole.bend&start_line=233&end_line=238

import Base
import bend-osdev-word64@0.1.1.1/word64.bend as W
import bend-osdev-word64@0.1.1.1/LAWS.bend as WL
import bend-osdev-bytes@0.1.1.1/bytes.bend as B
import bend-osdev-acpi@0.1.2.0/header.bend as H
import bend-osdev-acpi@0.1.2.0/gas.bend as G
import bend-osdev-acpi@0.1.2.0/PROOF_tables.bend as TP

# the HPET and the BGRT are 56 bytes long
def ckw.hpfit(+l0: U32, +r0: U32, +c0: U32, +o0: B.Octets, +t0: B.Octets, +orv0: U32, +ci0: B.Octets, +cr0: U32, +oem6b: {B.Octets.len(o0) == 6n : Nat}, +tid8b: {B.Octets.len(t0) == 8n : Nat}, +cid4b: {B.Octets.len(ci0) == 4n : Nat}, +id: U32, +gs: U32, +gw: U32, +go: U32, +ga: U32, +gaddr: W.W64, +n: U32, +m: U32, +p: U32) -> {Nat.is_le(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, gaddr}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]))), U32.to_nat(56)) == True{} : Bool}:
  %ckw.blen(B.Octets.of_string("HPET"), l0, r0, c0, o0, t0, orv0, ci0, cr0, {==}, oem6b, tid8b, cid4b, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, gaddr}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])) : {Nat.is_le(_, U32.to_nat(56)) == True{} : Bool}
  %WL.parts_of(gaddr) : {Nat.is_le(Nat.add(36n, B.Octets.len(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, _}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]))), U32.to_nat(56)) == True{} : Bool}
  %TP.tb.hp_len(id, gs, gw, go, ga, W.W64.hi(gaddr), W.W64.lo(gaddr), n, m, p) : {Nat.is_le(_, U32.to_nat(56)) == True{} : Bool}
  {==}

Uses (24):
  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=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  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_tables.bend&name=tb.hp_len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_whole.bend&name=ckw.blen
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/gas.bend&name=AcpiGas
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/gas.bend&name=AcpiGas.encode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/header.bend&name=AcpiHeader
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/header.bend&name=AcpiSdt.build
  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.concat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.le16
  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.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.of_string
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.1/LAWS.bend&name=parts_of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.1/word64.bend&name=W64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.1/word64.bend&name=W64.hi
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.1/word64.bend&name=W64.lo