def and_join

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/bits.bend:98

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WI

98# THEOREM: and on two limbs, (a1 + 2^k b1) & (a2 + 2^k b2) = a1 & a2 + 2^k (b1 & b2)
99def and_join(+k: Nat, +j: Nat, +a1: Nat, +b1: Nat, +a2: Nat, +b2: Nat, +h1: {C.fits(k, a1) == True{} : Bool}, +h2: {C.fits(k, a2) == True{} : Bool}) -> {SR.and_bits(Nat.add(k, j), Nat.add(a1, C.shift(k, b1)), Nat.add(a2, C.shift(k, b2))) == Nat.add(SR.and_bits(k, a1, a2), C.shift(k, SR.and_bits(j, b1, b2))) : Nat}:
100  match k:
101    case 0n:
102      %Equal.sym(Nat, a1, 0n, N.eq_from_is_eq(a1, 0n, h1)) : {SR.and_bits(j, Nat.add(_, b1), Nat.add(a2, b2)) == Nat.add(SR.and_bits(0n, _, a2), SR.and_bits(j, b1, b2)) : Nat}
103      %Equal.sym(Nat, a2, 0n, N.eq_from_is_eq(a2, 0n, h2)) : {SR.and_bits(j, b1, Nat.add(_, b2)) == Nat.add(SR.and_bits(0n, 0n, _), SR.and_bits(j, b1, b2)) : Nat}
104      {==}
105    case 1n+p:
106      +S1 = C.shift(p, b1)
107      +S2 = C.shift(p, b2)
108      +X = SR.and_bits(j, b1, b2)
109      +B = Nat.mul(C.bit(a1), C.bit(a2))
110      +Ih = and_join(p, j, C.half(a1), b1, C.half(a2), b2, h1, h2)
111      %Equal.sym(Nat, C.bit(Nat.add(a1, Nat.double(S1))), C.bit(a1), WI.bit_dbl(a1, S1)) : {Nat.add(Nat.mul(_, C.bit(Nat.add(a2, Nat.double(S2)))), Nat.double(SR.and_bits(Nat.add(p, j), C.half(Nat.add(a1, Nat.double(S1))), C.half(Nat.add(a2, Nat.double(S2)))))) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
112      %Equal.sym(Nat, C.bit(Nat.add(a2, Nat.double(S2))), C.bit(a2), WI.bit_dbl(a2, S2)) : {Nat.add(Nat.mul(C.bit(a1), _), Nat.double(SR.and_bits(Nat.add(p, j), C.half(Nat.add(a1, Nat.double(S1))), C.half(Nat.add(a2, Nat.double(S2)))))) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
113      %Equal.sym(Nat, C.half(Nat.add(a1, Nat.double(S1))), Nat.add(C.half(a1), S1), WI.half_dbl(a1, S1)) : {Nat.add(B, Nat.double(SR.and_bits(Nat.add(p, j), _, C.half(Nat.add(a2, Nat.double(S2)))))) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
114      %Equal.sym(Nat, C.half(Nat.add(a2, Nat.double(S2))), Nat.add(C.half(a2), S2), WI.half_dbl(a2, S2)) : {Nat.add(B, Nat.double(SR.and_bits(Nat.add(p, j), Nat.add(C.half(a1), S1), _))) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
115      %Equal.sym(Nat, SR.and_bits(Nat.add(p, j), Nat.add(C.half(a1), S1), Nat.add(C.half(a2), S2)), Nat.add(SR.and_bits(p, C.half(a1), C.half(a2)), C.shift(p, X)), Ih) : {Nat.add(B, Nat.double(_)) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
116      %N.add_double(SR.and_bits(p, C.half(a1), C.half(a2)), C.shift(p, X)) : {Nat.add(B, _) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
117      Equal.sym(Nat, Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))), Nat.add(B, Nat.add(Nat.double(SR.and_bits(p, C.half(a1), C.half(a2))), Nat.double(C.shift(p, X)))), N.add_assoc(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2))), Nat.double(C.shift(p, X))))