law front_correct

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

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

211# One block of the stream: the XORed front is the spec's.
212law front_correct:
213  for +r: Nat
214  for +kb: List<&2, U32>
215  for +c: U32
216  for +nb: List<&2, U32>
217  for +xs: List<&2, U32>
218  {I.xor_front(I.keystream(r, I.key(kb), c, I.nonce(nb)), xs) == R.xor_bytes(R.prefix(64n, xs), R.block_rounds(r, kb, c, nb)) : List<&2, U32>}