def mulval

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

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/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
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/arith.bend as AR
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/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P64

274# the value of the generalised product, constants symbolic
275def mulval(+one: Nat, +h1: {one == 1n : Nat}, +a: U32, +b: U32, +c: U32, +pc: {c == U32{WD.pw(32n, 16n)} : U32}, +m: U32, +pm: {m == U32{WD.mask(32n, 16n)} : U32}) -> {SW.value(mul32g(a, b, c, m)) == Nat.mul(v(a), v(b)) : Nat}:
276  +al = U32.and(a, m)
277  +ah = U32.div(a, c)
278  +bl = U32.and(b, m)
279  +bh = U32.div(b, c)
280  +xal = v(al)
281  +xah = v(ah)
282  +xbl = v(bl)
283  +xbh = v(bh)
284  +bal = lo16_lt(one, h1, a, m, pm)
285  +bah = hi16_lt(one, h1, a, c, pc)
286  +bbl = lo16_lt(one, h1, b, m, pm)
287  +bbh = hi16_lt(one, h1, b, c, pc)
288  +ll = U32.mul(al, bl)
289  +lh = U32.mul(al, bh)
290  +hl = U32.mul(ah, bl)
291  +hh = U32.mul(ah, bh)
292  +pll = PD.mul32(one, h1, al, bl, prod_lt(one, h1, xal, xbl, bal, bbl))
293  +plh = PD.mul32(one, h1, al, bh, prod_lt(one, h1, xal, xbh, bal, bbh))
294  +phl = PD.mul32(one, h1, ah, bl, prod_lt(one, h1, xah, xbl, bah, bbl))
295  +phh = PD.mul32(one, h1, ah, bh, prod_lt(one, h1, xah, xbh, bah, bbh))
296  # the middle sum and its carry
297  +mid = U32.add(lh, hl)
298  +cm = P64.carry32(lh, hl)
299  +kk = S.bit_value(cm)
300  +mlo = lo16(mid, m)
301  +mhi = hi16(mid, c)
302  +e3a = P64.add_cons(lh, hl)
303  +e3 = Equal.trans(Nat, Nat.add(v(mid), WD.sc(32n, kk)), Nat.add(v(lh), v(hl)), Nat.add(Nat.mul(xal, xbh), Nat.mul(xah, xbl)), e3a, Equal.trans(Nat, Nat.add(v(lh), v(hl)), Nat.add(Nat.mul(xal, xbh), v(hl)), Nat.add(Nat.mul(xal, xbh), Nat.mul(xah, xbl)), cong_l(v(lh), Nat.mul(xal, xbh), v(hl), plh), cong_r(Nat.mul(xal, xbh), v(hl), Nat.mul(xah, xbl), phl)))
304  +e5 = split16(one, h1, mid, c, pc, m, pm)
305  # the wrapped middle shift keeps the low half
306  +mm = U32.mul(mid, c)
307  +emc = mul_cons(mid, c)
308  +e6a = Equal.trans(Nat, Nat.mul(v(mid), v(c)), WD.sc(16n, v(mid)), Nat.add(WD.sc(16n, mlo), WD.sc(32n, mhi)), PD.mul_pow(one, h1, 16n, v(mid), v(c), h16(one, h1, c, pc)), Equal.trans(Nat, WD.sc(16n, v(mid)), WD.sc(16n, Nat.add(mlo, WD.sc(16n, mhi))), Nat.add(WD.sc(16n, mlo), WD.sc(32n, mhi)), cong_sc(16n, v(mid), Nat.add(mlo, WD.sc(16n, mhi)), e5), Equal.trans(Nat, WD.sc(16n, Nat.add(mlo, WD.sc(16n, mhi))), Nat.add(WD.sc(16n, mlo), WD.sc(16n, WD.sc(16n, mhi))), Nat.add(WD.sc(16n, mlo), WD.sc(32n, mhi)), sc_add2(16n, mlo, WD.sc(16n, mhi)), cong_r(WD.sc(16n, mlo), WD.sc(16n, WD.sc(16n, mhi)), WD.sc(32n, mhi), sc_sc(16n, 16n, mhi)))))
309  +e6 = Equal.trans(Nat, Nat.add(v(mm), WD.sc(32n, mex(mid, c))), Nat.mul(v(mid), v(c)), Nat.add(WD.sc(16n, mlo), WD.sc(32n, mhi)), emc, e6a)
310  +e7 = WD.uniq(32n, one, h1, v(mm), WD.sc(16n, mlo), mex(mid, c), mhi, e6, UD.vb(one, h1, mm), sc16_lt(one, mlo, lo16_lt(one, h1, mid, m, pm)))
311  # the low word
312  +lo = U32.add(ll, mm)
313  +c2 = P64.carry32(ll, mm)
314  +e8a = P64.add_cons(ll, mm)
315  +e8 = Equal.trans(Nat, Nat.add(v(lo), WD.sc(32n, S.bit_value(c2))), Nat.add(v(ll), v(mm)), Nat.add(Nat.mul(xal, xbl), WD.sc(16n, mlo)), e8a, Equal.trans(Nat, Nat.add(v(ll), v(mm)), Nat.add(Nat.mul(xal, xbl), v(mm)), Nat.add(Nat.mul(xal, xbl), WD.sc(16n, mlo)), cong_l(v(ll), Nat.mul(xal, xbl), v(mm), pll), cong_r(Nat.mul(xal, xbl), v(mm), WD.sc(16n, mlo), e7)))
316  # the total, as numbers
317  +q = Nat.add(Nat.add(Nat.mul(xah, xbh), Nat.add(mhi, WD.sc(16n, kk))), S.bit_value(c2))
318  +tot = assemble(xal, xah, xbl, xbh, v(mid), kk, mlo, mhi, v(lo), S.bit_value(c2), e3, e5, e8)
319  +ea = split16(one, h1, a, c, pc, m, pm)
320  +eb = split16(one, h1, b, c, pc, m, pm)
321  +eab = Equal.trans(Nat, Nat.mul(Nat.add(xal, WD.sc(16n, xah)), Nat.add(xbl, WD.sc(16n, xbh))), Nat.mul(v(a), Nat.add(xbl, WD.sc(16n, xbh))), Nat.mul(v(a), v(b)), Equal.cong(Nat, Nat, t => Nat.mul(t, Nat.add(xbl, WD.sc(16n, xbh))), Nat.add(xal, WD.sc(16n, xah)), v(a), Equal.sym(Nat, v(a), Nat.add(xal, WD.sc(16n, xah)), ea)), Equal.cong(Nat, Nat, t => Nat.mul(v(a), t), Nat.add(xbl, WD.sc(16n, xbh)), v(b), Equal.sym(Nat, v(b), Nat.add(xbl, WD.sc(16n, xbh)), eb)))
322  +etot = Equal.trans(Nat, Nat.add(v(lo), WD.sc(32n, q)), Nat.mul(Nat.add(xal, WD.sc(16n, xah)), Nat.add(xbl, WD.sc(16n, xbh))), Nat.mul(v(a), v(b)), tot, eab)
323  # the high word does not wrap: 2^32 q <= a b < 2^64
324  +pab = L.subst(Nat, z => {Nat.is_lt(Nat.mul(v(a), v(b)), z) == True{} : Bool}, Nat.mul(WD.sc(32n, one), WD.sc(32n, one)), WD.sc(64n, one), sq_sc(32n, one, h1), mul_lt_sq(v(a), v(b), WD.sc(32n, one), UD.vb(one, h1, a), UD.vb(one, h1, b)))
325  +lq = L.subst(Nat, z => {Nat.is_le(WD.sc(32n, q), z) == True{} : Bool}, Nat.add(WD.sc(32n, q), v(lo)), Nat.mul(v(a), v(b)), Equal.trans(Nat, Nat.add(WD.sc(32n, q), v(lo)), Nat.add(v(lo), WD.sc(32n, q)), Nat.mul(v(a), v(b)), NA.add_comm(WD.sc(32n, q), v(lo)), etot), N.le_add_right(WD.sc(32n, q), v(lo)))
326  +bq = AR.sc_lt_cancel(32n, q, WD.sc(32n, one), L.subst(Nat, z => {Nat.is_lt(WD.sc(32n, q), z) == True{} : Bool}, WD.sc(64n, one), WD.sc(32n, WD.sc(32n, one)), AR.sc_idx(32n, 32n, one), N.le_lt_trans(WD.sc(32n, q), Nat.mul(v(a), v(b)), WD.sc(64n, one), lq, pab)))
327  # the high word's value is q
328  +mc = U32.is_lt(mid, lh)
329  +emc2 = P64.add_lt(lh, hl)
330  +tb = U32.mul(X.b32(mc), c)
331  +vb32 = Equal.trans(Nat, v(X.b32(mc)), S.bit_value(mc), kk, b32_v(mc), Equal.cong(Bool, Nat, t => S.bit_value(t), mc, cm, emc2))
332  +btb = L.subst(Nat, z => {Nat.is_lt(WD.sc(16n, z), WD.sc(32n, one)) == True{} : Bool}, S.bit_value(mc), v(X.b32(mc)), Equal.sym(Nat, v(X.b32(mc)), S.bit_value(mc), b32_v(mc)), sc16_lt(one, S.bit_value(mc), bit_lt16(one, h1, mc)))
333  +ptb = Equal.trans(Nat, v(tb), WD.sc(16n, v(X.b32(mc))), WD.sc(16n, kk), PD.mulp32(one, h1, 16n, X.b32(mc), c, h16(one, h1, c, pc), btb), cong_sc(16n, v(X.b32(mc)), kk, vb32))
334  +bt = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, Nat.add(WD.sc(16n, kk), mhi), Nat.add(mhi, WD.sc(16n, kk)), NA.add_comm(WD.sc(16n, kk), mhi), L.subst(Nat, z => {Nat.is_lt(Nat.add(WD.sc(16n, kk), mhi), z) == True{} : Bool}, WD.sc(16n, WD.sc(16n, one)), WD.sc(32n, one), sc_sc(16n, 16n, one), AR.digit_lt(16n, one, h1, mhi, kk, WD.sc(16n, one), hi16_lt(one, h1, mid, c, pc), bit_lt16(one, h1, cm))))
335  +t = U32.add(U32.div(mid, c), tb)
336  +pt = PD.addv32(one, h1, U32.div(mid, c), tb, mhi, WD.sc(16n, kk), {==}, ptb, bt)
337  +q1 = Nat.add(Nat.mul(xah, xbh), Nat.add(mhi, WD.sc(16n, kk)))
338  +bq1 = N.le_lt_trans(q1, q, WD.sc(32n, one), N.le_add_right(q1, S.bit_value(c2)), bq)
339  +h1v = PD.addv32(one, h1, hh, t, Nat.mul(xah, xbh), Nat.add(mhi, WD.sc(16n, kk)), phh, pt, bq1)
340  +ec2 = Equal.trans(Nat, v(X.b32(U32.is_lt(lo, ll))), S.bit_value(U32.is_lt(lo, ll)), S.bit_value(c2), b32_v(U32.is_lt(lo, ll)), Equal.cong(Bool, Nat, t2 => S.bit_value(t2), U32.is_lt(lo, ll), c2, P64.add_lt(ll, mm)))
341  +hv = PD.addv32(one, h1, U32.add(hh, t), X.b32(U32.is_lt(lo, ll)), q1, S.bit_value(c2), h1v, ec2, bq)
342  # the value of the pair
343  +hi = U32.add(U32.add(hh, t), X.b32(U32.is_lt(lo, ll)))
344  +ev = Equal.trans(Nat, Nat.add(v(lo), C.shift(32n, v(hi))), Nat.add(v(lo), WD.sc(32n, v(hi))), Nat.add(v(lo), WD.sc(32n, q)), cong_r(v(lo), C.shift(32n, v(hi)), WD.sc(32n, v(hi)), shift_sc(32n, v(hi))), cong_r(v(lo), WD.sc(32n, v(hi)), WD.sc(32n, q), cong_sc(32n, v(hi), q, hv)))
345  Equal.trans(Nat, Nat.add(v(lo), C.shift(32n, v(hi))), Nat.add(v(lo), WD.sc(32n, q)), Nat.mul(v(a), v(b)), ev, etot)