PROOFTables.tb.hp: def of bend-osdev-acpi@0.1.1.0
Import: import bend-osdev-acpi@0.1.1.0/PROOF_tables.bend as PROOFTables
Lines 170-178 of bend-osdev-acpi@0.1.1.0/PROOF_tables.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&start_line=170&end_line=178

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-acpi@0.1.1.0/error.bend as E
import bend-osdev-acpi@0.1.1.0/header.bend as H
import bend-osdev-acpi@0.1.1.0/fields.bend as F
import bend-osdev-acpi@0.1.1.0/gas.bend as G
import bend-osdev-acpi@0.1.1.0/hpet.bend as Hp

def tb.hp(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +id: U32, +gs: U32, +gw: U32, +go: U32, +ga: U32, +ah: U32, +al: U32, +n: U32, +m: U32, +p: U32) -> {Hp.AcpiHpet.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])}) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}:
  %tb.lenchk(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])) : {Hp.hpet.read(Nat.is_le(56n, _), H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]))) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
  %tb.hp_len(id, gs, gw, go, ga, ah, al, n, m, p) : {Hp.hpet.read(Nat.is_le(56n, _), H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]))) == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
  %tb.r32(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 0n) : {Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, _, G.AcpiGas.at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 40n), F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 52n), F.AcpiF.u16(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 53n), F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 55n)}} == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
  %tb.rgas(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 4n) : {Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u32(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 0n), _, F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 52n), F.AcpiF.u16(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 53n), F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 55n)}} == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
  %tb.r8(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 16n) : {Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u32(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 0n), G.AcpiGas.at(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 4n), _, F.AcpiF.u16(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 53n), F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 55n)}} == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
  %tb.r16(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 17n) : {Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u32(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 0n), G.AcpiGas.at(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 4n), F.AcpiF.u8(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 16n), _, F.AcpiF.u8(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])])), 55n)}} == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
  %tb.r8(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 19n) : {Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u32(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 0n), G.AcpiGas.at(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 4n), F.AcpiF.u8(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 16n), F.AcpiF.u16(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]), 17n), _}} == Done{Hp.AcpiHpet{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, G.AcpiGas{B.byte(gs), B.byte(gw), B.byte(go), B.byte(ga), W.W64.from_parts(ah, al)}, B.byte(n), B.low16(m), B.byte(p)}} : Result<&2, &2, E.AcpiError, Hp.AcpiHpet>}
  tb.hp_vals(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, gs, gw, go, ga, ah, al, n, m, p)

Uses (35):
  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_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.hp_len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.hp_vals
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.lenchk
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.r16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.r32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.r8
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.rgas
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/error.bend&name=AcpiError
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/fields.bend&name=AcpiF.u16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/fields.bend&name=AcpiF.u32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/fields.bend&name=AcpiF.u8
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/gas.bend&name=AcpiGas
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/gas.bend&name=AcpiGas.at
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/gas.bend&name=AcpiGas.encode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=AcpiHeader
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=AcpiHeader.encode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=AcpiSdt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/hpet.bend&name=AcpiHpet
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/hpet.bend&name=AcpiHpet.of_sdt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/hpet.bend&name=hpet.read
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.concat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.le16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.le32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=byte
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=low16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.from_parts