law Expand.prefix

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/kdf/laws.bend:52

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/kdf.bend as KDF

52# A shorter output is a prefix of a longer one (same key and info).
53law Expand.prefix:
54  for +prk: List<&2, U32>
55  for +info: List<&2, U32>
56  for +a: Nat
57  for +b: Nat
58  for +out: List<&2, U32>
59  for +hab: {Nat.is_le(a, b) == True{} : Bool}
60  for +h: {KDF.expand(prk, info, b) == Done{out} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
61  {KDF.expand(prk, info, a) == Done{List.take(&2, U32, out, a)} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}