law enc_ks

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/chacha/involution.bend:141

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R

141law enc_ks:
142  for +fuel: Nat
143  for +xs: List<&2, U32>
144  for +r: Nat
145  for +kb: List<&2, U32>
146  for +c: U32
147  for +nb: List<&2, U32>
148  {R.encrypt_blocks(R.blocks(fuel, xs), r, kb, c, nb) == R.xor_bytes(xs, ks(fuel, r, kb, c, nb)) : List<&2, U32>}