def ckw.hpfit

bend-osdev-acpi@0.1.2.0 · PROOF_whole.bend:233

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

233# the HPET and the BGRT are 56 bytes long
234def 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}:
235  %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}
236  %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}
237  %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}
238  {==}