law hstate_eq
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/chacha/stream.bend:84
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/stream.bend as Stream
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
84law hstate_eq:
85 for +ks: List<&2, U32>
86 for +ns: List<&2, U32>
87 {K.vec(I.hstate(I.key_words(ks), ns)) == R.hstate(ks, ns) : List<&2, U32>}