def ckw.bgfit

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

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/PROOF_tables.bend as TP

247def ckw.bgfit(+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}, +v: U32, +st: U32, +it: U32, +a: W.W64, +x: U32, +y: U32) -> {Nat.is_le(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0}, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(a), B.Octets.le32(x), B.Octets.le32(y)]))), U32.to_nat(56)) == True{} : Bool}:
248  %ckw.blen(B.Octets.of_string("BGRT"), l0, r0, c0, o0, t0, orv0, ci0, cr0, {==}, oem6b, tid8b, cid4b, B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(a), B.Octets.le32(x), B.Octets.le32(y)])) : {Nat.is_le(_, U32.to_nat(56)) == True{} : Bool}
249  %WL.parts_of(a) : {Nat.is_le(Nat.add(36n, B.Octets.len(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(_), B.Octets.le32(x), B.Octets.le32(y)]))), U32.to_nat(56)) == True{} : Bool}
250  %TP.tb.bg_len(v, st, it, W.W64.hi(a), W.W64.lo(a), x, y) : {Nat.is_le(_, U32.to_nat(56)) == True{} : Bool}
251  {==}