def tb.clen_g

bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:445

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-word64@0.1.1.0/LAWS.bend as WL

445def tb.clen_g(+b: W.W64, +s: U32, +lo: U32, +hi: U32) -> {16n == B.Octets.len(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)])) : Nat}:
446  %WL.parts_of(b) : {16n == B.Octets.len(B.Octets.concat([B.Octets.le64(_), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)])) : Nat}
447  tb.clen(W.W64.hi(b), W.W64.lo(b), s, lo, hi)