law add_correct

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

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

105law add_correct:
106  for +a: C.State
107  for +b: C.State
108  {vec(C.add(a, b)) == R.add_words(vec(a), vec(b)) : List<&2, U32>}