law pbkdf2_length

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

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

494# PBKDF2 over any MAC (pbkdf2.bend), for every MAC, password, salt,
495# iteration count and length: a derivation that succeeds gives exactly the
496# length asked for (the KDF interface's length law); the unchecked stream
497# has that length, and a shorter stream is a prefix of a longer (the KDF
498# interface's prefix law)
499law pbkdf2_length:
500  for ~K: Data
501  for ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>
502  for ~compute: K -> B.Octets -> B.Octets
503  for ~hlen: Nat
504  for +p: B.Octets
505  for +salt: B.Octets
506  for +c: U32
507  for +n: Nat
508  {Result.map(&2, &2, Cr.CrError, B.Octets, Nat, o => B.Octets.len(o), Pb.CrPbkdf2.pbkdf2(~K, ~key, ~compute, ~hlen, p, salt, c, n)) == Result.map(&2, &2, Cr.CrError, B.Octets, Nat, o => n, Pb.CrPbkdf2.pbkdf2(~K, ~key, ~compute, ~hlen, p, salt, c, n)) : Result<&2, &2, Cr.CrError, Nat>}