def xsplit

bend-collections-laws-math@1.0.0.0 · proofs/math/random/pcg/xor.bend:78

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/random/pcg.bend as SP
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

78# xor_bits splits at bit k when the low parts fit k bits
79def xsplit(+k: Nat, +j: Nat, +al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +ha: {C.fits(k, al) == True{} : Bool}, +hb: {C.fits(k, bl) == True{} : Bool}) -> {SP.xor_bits(Nat.add(k, j), Nat.add(al, C.shift(k, ah)), Nat.add(bl, C.shift(k, bh))) == Nat.add(SP.xor_bits(k, al, bl), C.shift(k, SP.xor_bits(j, ah, bh))) : Nat}:
80  match k:
81    case 0n:
82      %Equal.sym(Nat, al, 0n, fits0(al, ha)) : {SP.xor_bits(j, Nat.add(_, ah), Nat.add(bl, bh)) == SP.xor_bits(j, ah, bh) : Nat}
83      %Equal.sym(Nat, bl, 0n, fits0(bl, hb)) : {SP.xor_bits(j, Nat.add(0n, ah), Nat.add(_, bh)) == SP.xor_bits(j, ah, bh) : Nat}
84      {==}
85    case 1n+p:
86      +A = Nat.add(al, Nat.double(C.shift(p, ah)))
87      +B = Nat.add(bl, Nat.double(C.shift(p, bh)))
88      +X = SP.xor_bits(j, ah, bh)
89      +Y = SP.xor_bits(p, C.half(al), C.half(bl))
90      +bx = SP.b2n(Bool.not(Nat.is_eq(C.bit(al), C.bit(bl))))
91      %Equal.sym(Nat, C.bit(A), C.bit(al), WW.bit_dbl(al, C.shift(p, ah))) : {Nat.add(SP.b2n(Bool.not(Nat.is_eq(_, C.bit(B)))), Nat.double(SP.xor_bits(Nat.add(p, j), C.half(A), C.half(B)))) == Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))) : Nat}
92      %Equal.sym(Nat, C.bit(B), C.bit(bl), WW.bit_dbl(bl, C.shift(p, bh))) : {Nat.add(SP.b2n(Bool.not(Nat.is_eq(C.bit(al), _))), Nat.double(SP.xor_bits(Nat.add(p, j), C.half(A), C.half(B)))) == Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))) : Nat}
93      %Equal.sym(Nat, C.half(A), Nat.add(C.half(al), C.shift(p, ah)), WW.half_dbl(al, C.shift(p, ah))) : {Nat.add(bx, Nat.double(SP.xor_bits(Nat.add(p, j), _, C.half(B)))) == Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))) : Nat}
94      %Equal.sym(Nat, C.half(B), Nat.add(C.half(bl), C.shift(p, bh)), WW.half_dbl(bl, C.shift(p, bh))) : {Nat.add(bx, Nat.double(SP.xor_bits(Nat.add(p, j), Nat.add(C.half(al), C.shift(p, ah)), _))) == Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))) : Nat}
95      %Equal.sym(Nat, SP.xor_bits(Nat.add(p, j), Nat.add(C.half(al), C.shift(p, ah)), Nat.add(C.half(bl), C.shift(p, bh))), Nat.add(Y, C.shift(p, X)), xsplit(p, j, C.half(al), ah, C.half(bl), bh, ha, hb)) : {Nat.add(bx, Nat.double(_)) == Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))) : Nat}
96      %Equal.sym(Nat, Nat.double(Nat.add(Y, C.shift(p, X))), Nat.add(Nat.double(Y), Nat.double(C.shift(p, X))), NA.double_add(Y, C.shift(p, X))) : {Nat.add(bx, _) == Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))) : Nat}
97      Equal.sym(Nat, Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))), Nat.add(bx, Nat.add(Nat.double(Y), Nat.double(C.shift(p, X)))), NA.add_assoc(bx, Nat.double(Y), Nat.double(C.shift(p, X))))