def tb.hp
bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:170
import bend-osdev-acpi@0.1.1.0/PROOF_tables.bend as PROOFTables
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
170def 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>}:
171 %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>}
172 %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>}
173 %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>}
174 %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>}
175 %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>}
176 %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>}
177 %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>}
178 tb.hp_vals(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, id, gs, gw, go, ga, ah, al, n, m, p)