law pbkdf2_stream_length

bend-osdev-crypto@0.1.0.0 · LAWS.bend:510

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/pbkdf2.bend as Pb

510law pbkdf2_stream_length:
511  for ~K: Data
512  for ~compute: K -> B.Octets -> B.Octets
513  for +k: K
514  for +salt: B.Octets
515  for +c: U32
516  for +n: Nat
517  {B.Octets.len(Pb.CrPbkdf2.stream(~K, ~compute, k, salt, c, n)) == n : Nat}