law xor_length

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

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

69law xor_length:
70  for +xs: List<&2, U32>
71  for +ks: List<&2, U32>
72  for +h: {Nat.is_le(List.length(&2, U32, xs), List.length(&2, U32, ks)) == True{} : Bool}
73  {List.length(&2, U32, R.xor_bytes(xs, ks)) == List.length(&2, U32, xs) : Nat}