law init_correct

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

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

135law init_correct:
136  for +k0: U32
137  for +k1: U32
138  for +k2: U32
139  for +k3: U32
140  for +k4: U32
141  for +k5: U32
142  for +k6: U32
143  for +k7: U32
144  for +c: U32
145  for +n0: U32
146  for +n1: U32
147  for +n2: U32
148  {vec(C.init(k0, k1, k2, k3, k4, k5, k6, k7, c, n0, n1, n2)) == R.state([k0, k1, k2, k3, k4, k5, k6, k7], c, [n0, n1, n2]) : List<&2, U32>}