law encrypt_xor
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/chacha/involution.bend:177
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/involution.bend as Involution
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R
177law encrypt_xor:
178 for +r: Nat
179 for +kb: List<&2, U32>
180 for +c: U32
181 for +nb: List<&2, U32>
182 for +pt: List<&2, U32>
183 {R.encrypt_rounds(r, kb, c, nb, pt) == R.xor_bytes(pt, ks(List.length(&2, U32, pt), r, kb, c, nb)) : List<&2, U32>}