law hinit_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/chacha/core.bend:153

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/core.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R

153law hinit_correct:
154  for +k0: U32
155  for +k1: U32
156  for +k2: U32
157  for +k3: U32
158  for +k4: U32
159  for +k5: U32
160  for +k6: U32
161  for +k7: U32
162  for +n0: U32
163  for +n1: U32
164  for +n2: U32
165  for +n3: U32
166  {vec(C.hinit(k0, k1, k2, k3, k4, k5, k6, k7, n0, n1, n2, n3)) == R.hstate([k0, k1, k2, k3, k4, k5, k6, k7], [n0, n1, n2, n3]) : List<&2, U32>}