Xor.xor64_value: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/xor.bend as Xor
Lines 99-105 of bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/xor.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/xor.bend&start_line=99&end_line=105

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/spec/math/random/pcg.bend as SP
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/random/pcg.bend as P
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH

# THEOREM: the value of xor64 is xor_bits(64) of the values
def xor64_value(+a: WU.U64, +b: WU.U64) -> {SW.value(P.xor64(a, b)) == SP.xor_bits(64n, SW.value(a), SW.value(b)) : Nat}:
  match a b:
    case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
      %Equal.sym(Nat, v(U32.xor(al, bl)), SP.xor_bits(32n, v(al), v(bl)), xor32(al, bl)) : {Nat.add(_, C.shift(32n, v(U32.xor(ah, bh)))) == SP.xor_bits(64n, Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))) : Nat}
      %Equal.sym(Nat, v(U32.xor(ah, bh)), SP.xor_bits(32n, v(ah), v(bh)), xor32(ah, bh)) : {Nat.add(SP.xor_bits(32n, v(al), v(bl)), C.shift(32n, _)) == SP.xor_bits(64n, Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))) : Nat}
      Equal.sym(Nat, SP.xor_bits(Nat.add(32n, 32n), Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(SP.xor_bits(32n, v(al), v(bl)), C.shift(32n, SP.xor_bits(32n, v(ah), v(bh)))), xsplit(32n, 32n, v(al), v(ah), v(bl), v(bh), SH.vb(al), SH.vb(bl)))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/xor.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/xor.bend&name=xor32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/xor.bend&name=xsplit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=vb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/pcg.bend&name=xor_bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/pcg.bend&name=xor64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64