def ok

lawful-bytes@0.1.1.0 · defs.bend:37

import Base
import lawful-arrays@0.1.0.0/defs.bend as A

37# b is well formed with a block of depth d: a perfect block of 2^d words,
38# d <= 29, and len within the block. A buffer holds at most 2^31 bytes (2 GiB),
39# so every index and length fits in a U32; the laws' hypotheses keep sums of
40# lengths in range too. Larger files are read in pieces.
41def ok(b: Bytes, +d: Nat) -> Bool:
42  Bytes{len, buf} = b
43  A.full(U32, buf, d) && (Nat.is_le(d, 29n) && Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))))