def cr.kb.fits

bend-osdev-crypto@0.1.0.0 · kbkdf.bend:94

import Base

94# whether n bytes need at most max blocks of hlen bytes, and L = 8 n fits
95# llen bytes (and 32 bits)
96def cr.kb.fits(+hlen: Nat, +llen: Nat, +n: Nat, +max: Nat) -> Bool:
97  Bool.and(Bool.and(Nat.is_lt(0n, hlen), Nat.is_le(Nat.div(Nat.add(n, Nat.sub(hlen, 1n)), hlen), max)), Nat.is_lt(Nat.mul(8n, n), Nat.pow(2n, Nat.mul(8n, Nat.min(llen, 4n)))))