law ks_length

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/chacha/involution.bend:107

import Base

107law ks_length:
108  for +fuel: Nat
109  for +r: Nat
110  for +kb: List<&2, U32>
111  for +c: U32
112  for +nb: List<&2, U32>
113  {Nat.is_le(fuel, List.length(&2, U32, ks(fuel, r, kb, c, nb))) == True{} : Bool}