law kbkdf_feedback_stream_prefix

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

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/kbkdf.bend as Kb

583law kbkdf_feedback_stream_prefix:
584  for ~K: Data
585  for ~compute: K -> B.Octets -> B.Octets
586  for ~rlen: Nat
587  for +k: K
588  for +iv: B.Octets
589  for +fixed: B.Octets
590  for +n: Nat
591  for +j: Nat
592  {B.Octets.take(n, Kb.CrKbkdf.feedback_stream(~K, ~compute, ~rlen, k, iv, fixed, Nat.add(n, j))) == Kb.CrKbkdf.feedback_stream(~K, ~compute, ~rlen, k, iv, fixed, n) : B.Octets}