def cr.hkdf.ok

bend-osdev-crypto@0.1.0.0 · hkdf.bend:49

import Base

49def cr.hkdf.ok(pos: Bool, +len: Nat, +dsize: Nat) -> Bool:
50  match pos:
51    case True{}:
52      Nat.is_le(len, Nat.mul(255n, dsize))
53    case False{}:
54      False{}