def tb.bg

bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:190
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/bgrt.bend as Bg

190def tb.bg(+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}, +v: U32, +st: U32, +it: U32, +ah: U32, +al: U32, +x: U32, +y: U32) -> {Bg.AcpiBgrt.of_sdt(H.AcpiSdt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])}) == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}:
191  %tb.lenchk(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])) : {Bg.bgrt.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.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]))) == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
192  %tb.bg_len(v, st, it, ah, al, x, y) : {Bg.bgrt.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.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]))) == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
193  %tb.r16(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 0n) : {Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, _, 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.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 38n), 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.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 39n), F.AcpiF.u64(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 40n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 48n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 52n)}} == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
194  %tb.r8(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 2n) : {Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u16(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 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.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 39n), F.AcpiF.u64(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 40n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 48n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 52n)}} == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
195  %tb.r8(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 3n) : {Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u16(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 0n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 2n), _, F.AcpiF.u64(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 40n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 48n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 52n)}} == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
196  %tb.r64(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 4n) : {Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u16(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 0n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 2n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 3n), _, F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 48n), F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 52n)}} == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
197  %tb.r32(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 12n) : {Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u16(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 0n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 2n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 3n), F.AcpiF.u64(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 4n), _, F.AcpiF.u32(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)])), 52n)}} == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
198  %tb.r32(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 16n) : {Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, F.AcpiF.u16(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 0n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 2n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 3n), F.AcpiF.u64(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 4n), F.AcpiF.u32(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 12n), _}} == Done{Bg.AcpiBgrt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}
199  tb.bg_vals(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, v, st, it, ah, al, x, y)
Uses (34)

Used by (1)

bend-osdev-acpi@0.1.1.0/LAWS_tables:bgrt_round_trip