Involution.xor_length: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/involution.bend as Involution
Lines 69-73 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/involution.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/involution.bend&start_line=69&end_line=73

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

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

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend&name=xor_bytes