law state_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/chacha/stream.bend:71

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/core.bend as K

71law state_eq:
72  for +ks: List<&2, U32>
73  for +c: U32
74  for +ns: List<&2, U32>
75  {K.vec(I.state(I.key_words(ks), c, I.nonce_words(ns))) == R.state(ks, c, ns) : List<&2, U32>}