def assemble

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mul.bend:165

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

165# the value equation of the product: low word, carries and high digits
166def assemble(+al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +m: Nat, +k: Nat, +mlo: Nat, +mhi: Nat, +vl: Nat, +c2: Nat, +e3: {Nat.add(m, WD.sc(32n, k)) == Nat.add(Nat.mul(al, bh), Nat.mul(ah, bl)) : Nat}, +e5: {m == Nat.add(mlo, WD.sc(16n, mhi)) : Nat}, +e8: {Nat.add(vl, WD.sc(32n, c2)) == Nat.add(Nat.mul(al, bl), WD.sc(16n, mlo)) : Nat}) -> {Nat.add(vl, WD.sc(32n, Nat.add(Nat.add(Nat.mul(ah, bh), Nat.add(mhi, WD.sc(16n, k))), c2))) == Nat.mul(Nat.add(al, WD.sc(16n, ah)), Nat.add(bl, WD.sc(16n, bh))) : Nat}:
167  +ll = Nat.mul(al, bl)
168  +lh = Nat.mul(al, bh)
169  +hl = Nat.mul(ah, bl)
170  +hh = Nat.mul(ah, bh)
171  +q = Nat.add(hh, Nat.add(mhi, WD.sc(16n, k)))
172  +r = Nat.add(WD.sc(32n, mhi), WD.sc(48n, k))
173  +sq = Nat.add(WD.sc(32n, hh), r)
174  +eq = Equal.trans(Nat, WD.sc(32n, q), Nat.add(WD.sc(32n, hh), WD.sc(32n, Nat.add(mhi, WD.sc(16n, k)))), sq, sc_add2(32n, hh, Nat.add(mhi, WD.sc(16n, k))), cong_r(WD.sc(32n, hh), WD.sc(32n, Nat.add(mhi, WD.sc(16n, k))), r, Equal.trans(Nat, WD.sc(32n, Nat.add(mhi, WD.sc(16n, k))), Nat.add(WD.sc(32n, mhi), WD.sc(32n, WD.sc(16n, k))), r, sc_add2(32n, mhi, WD.sc(16n, k)), cong_r(WD.sc(32n, mhi), WD.sc(32n, WD.sc(16n, k)), WD.sc(48n, k), sc_sc(32n, 16n, k)))))
175  +t1 = Nat.add(vl, Nat.add(WD.sc(32n, q), WD.sc(32n, c2)))
176  +t2 = Nat.add(Nat.add(vl, WD.sc(32n, c2)), WD.sc(32n, q))
177  +t3 = Nat.add(Nat.add(ll, WD.sc(16n, mlo)), sq)
178  +t4 = Nat.add(Nat.add(ll, WD.sc(32n, hh)), Nat.add(WD.sc(16n, mlo), r))
179  +t5 = Nat.add(Nat.add(ll, WD.sc(32n, hh)), Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)))
180  +t6 = Nat.add(Nat.add(ll, WD.sc(16n, lh)), Nat.add(WD.sc(32n, hh), WD.sc(16n, hl)))
181  +rr = Nat.add(Nat.add(ll, WD.sc(16n, lh)), Nat.add(WD.sc(16n, hl), WD.sc(32n, hh)))
182  +swp = Equal.trans(Nat, Nat.add(vl, Nat.add(WD.sc(32n, q), WD.sc(32n, c2))), Nat.add(WD.sc(32n, q), Nat.add(vl, WD.sc(32n, c2))), t2, NA.add_swap(vl, WD.sc(32n, q), WD.sc(32n, c2)), NA.add_comm(WD.sc(32n, q), Nat.add(vl, WD.sc(32n, c2))))
183  +chain = Equal.trans(Nat, Nat.add(vl, WD.sc(32n, Nat.add(q, c2))), t1, rr, cong_r(vl, WD.sc(32n, Nat.add(q, c2)), Nat.add(WD.sc(32n, q), WD.sc(32n, c2)), sc_add2(32n, q, c2)),
184    Equal.trans(Nat, t1, t2, rr, swp,
185      Equal.trans(Nat, t2, Nat.add(Nat.add(ll, WD.sc(16n, mlo)), WD.sc(32n, q)), rr, cong_l(Nat.add(vl, WD.sc(32n, c2)), Nat.add(ll, WD.sc(16n, mlo)), WD.sc(32n, q), e8),
186        Equal.trans(Nat, Nat.add(Nat.add(ll, WD.sc(16n, mlo)), WD.sc(32n, q)), t3, rr, cong_r(Nat.add(ll, WD.sc(16n, mlo)), WD.sc(32n, q), sq, eq),
187          Equal.trans(Nat, t3, t4, rr, add4(ll, WD.sc(16n, mlo), WD.sc(32n, hh), r),
188            Equal.trans(Nat, t4, t5, rr, cong_r(Nat.add(ll, WD.sc(32n, hh)), Nat.add(WD.sc(16n, mlo), r), Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)), mid_eq(m, k, mlo, mhi, lh, hl, e3, e5)),
189              Equal.trans(Nat, t5, t6, rr, add4(ll, WD.sc(32n, hh), WD.sc(16n, lh), WD.sc(16n, hl)),
190                cong_r(Nat.add(ll, WD.sc(16n, lh)), Nat.add(WD.sc(32n, hh), WD.sc(16n, hl)), Nat.add(WD.sc(16n, hl), WD.sc(32n, hh)), NA.add_comm(WD.sc(32n, hh), WD.sc(16n, hl))))))))))
191  Equal.trans(Nat, Nat.add(vl, WD.sc(32n, Nat.add(q, c2))), rr, Nat.mul(Nat.add(al, WD.sc(16n, ah)), Nat.add(bl, WD.sc(16n, bh))), chain, Equal.sym(Nat, Nat.mul(Nat.add(al, WD.sc(16n, ah)), Nat.add(bl, WD.sc(16n, bh))), rr, expand16(al, ah, bl, bh)))