def mm_bg
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mmtop.bend:41
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mmtop.bend as W64mmtop
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/src/math/u64.bend as WU
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/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend as W64D
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend as M128
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mm.bend as MM
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
41def mm_bg(+one: Nat, +h1: {one == 1n : Nat}, +pl: WU.U64, +ph: WU.U64, +pr: Nat, +em: {Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))) == pr : Nat}, +ml: U32, +mh: U32, +hsq: {Nat.is_lt(pr, Nat.mul(SW.value(WU.U64{ml, mh}), SW.value(WU.U64{ml, mh}))) == True{} : Bool}, +hz: {U32.is_zero(mh) == False{} : Bool}) -> {SW.value(X.red96(X.red96(ph, X.hi(pl), WU.U64{ml, mh}), X.lo(pl), WU.U64{ml, mh})) == Nat.mod(pr, SW.value(WU.U64{ml, mh})) : Nat}:
42 +S = C.shift(64n, one)
43 +ePH = WW.shift_mul_one(64n, one, h1, SW.value(ph))
44 +h1a = L.subst(Nat, z => {Nat.is_le(z, pr) == True{} : Bool}, C.shift(64n, SW.value(ph)), Nat.mul(SW.value(ph), S), ePH, L.subst(Nat, z => {Nat.is_le(C.shift(64n, SW.value(ph)), z) == True{} : Bool}, Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), pr, em, L.subst(Nat, z => {Nat.is_le(C.shift(64n, SW.value(ph)), z) == True{} : Bool}, Nat.add(C.shift(64n, SW.value(ph)), SW.value(pl)), Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), N.add_comm(C.shift(64n, SW.value(ph)), SW.value(pl)), N.le_add_right(C.shift(64n, SW.value(ph)), SW.value(pl)))))
45 +h2a = N.lt_le_trans(pr, Nat.mul(SW.value(WU.U64{ml, mh}), SW.value(WU.U64{ml, mh})), Nat.mul(SW.value(WU.U64{ml, mh}), S), hsq, W64M.le_mul_r(SW.value(WU.U64{ml, mh}), SW.value(WU.U64{ml, mh}), S, N.lt_le(SW.value(WU.U64{ml, mh}), S, WW.lt_one(64n, one, h1, SW.value(WU.U64{ml, mh}), M128.fit64(WU.U64{ml, mh})))))
46 +h3a = L.subst(Nat, z => {Nat.is_lt(Nat.mul(SW.value(ph), S), z) == True{} : Bool}, Nat.mul(SW.value(WU.U64{ml, mh}), S), Nat.mul(SW.value(WU.U64{ml, mh}), S), {==}, N.le_lt_trans(Nat.mul(SW.value(ph), S), pr, Nat.mul(SW.value(WU.U64{ml, mh}), S), h1a, h2a))
47 +hPH = W64D.lt_cancel_mul(SW.value(ph), SW.value(WU.U64{ml, mh}), S, h3a)
48 +er1 = MM.red_vg(one, h1, X.hi(pl), ph, ml, mh, hPH, hz)
49 +bp = Nat.sub(SW.value(WU.U64{ml, mh}), 1n)
50 +hB = Equal.sym(Nat, 1n+bp, SW.value(WU.U64{ml, mh}), N.sub_add(SW.value(WU.U64{ml, mh}), 1n, N.le_trans(1n, 1n+SW.value(ph), SW.value(WU.U64{ml, mh}), N.zero_le(SW.value(ph)), N.lt_succ_le_succ(SW.value(ph), SW.value(WU.U64{ml, mh}), hPH))))
51 +hr1 = L.subst(Nat, z => {Nat.is_lt(SW.value(X.red96(ph, X.hi(pl), WU.U64{ml, mh})), z) == True{} : Bool}, 1n+bp, SW.value(WU.U64{ml, mh}), Equal.sym(Nat, SW.value(WU.U64{ml, mh}), 1n+bp, hB), L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp), SW.value(X.red96(ph, X.hi(pl), WU.U64{ml, mh})), Equal.sym(Nat, SW.value(X.red96(ph, X.hi(pl), WU.U64{ml, mh})), Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp), Equal.trans(Nat, SW.value(X.red96(ph, X.hi(pl), WU.U64{ml, mh})), Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), SW.value(WU.U64{ml, mh})), Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp), er1, Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), z), SW.value(WU.U64{ml, mh}), 1n+bp, hB))), NR.dm_lt(bp, Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))))))
52 +er2 = MM.red_vg(one, h1, X.lo(pl), X.red96(ph, X.hi(pl), WU.U64{ml, mh}), ml, mh, hr1, hz)
53 +P = C.shift(32n, one)
54 +lo = v(X.lo(pl))
55 +f1 = Equal.trans(Nat, Nat.add(lo, C.shift(32n, Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp))), Nat.add(lo, Nat.mul(Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp), P)), Nat.add(Nat.mul(Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp), P), lo), Equal.cong(Nat, Nat, z => Nat.add(lo, z), C.shift(32n, Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp)), Nat.mul(Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp), P), WW.shift_mul_one(32n, one, h1, Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp))), N.add_comm(lo, Nat.mul(Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp), P)))
56 +f2 = Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), P), lo), Nat.add(lo, C.shift(32n, Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))))), Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), P), lo), Nat.add(lo, Nat.mul(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), P)), Nat.add(lo, C.shift(32n, Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))))), N.add_comm(Nat.mul(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), P), lo), Equal.cong(Nat, Nat, z => Nat.add(lo, z), Nat.mul(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), P), C.shift(32n, Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph)))), Equal.sym(Nat, C.shift(32n, Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph)))), Nat.mul(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), P), WW.shift_mul_one(32n, one, h1, Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))))))), Equal.trans(Nat, Nat.add(lo, C.shift(32n, Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))))), Nat.add(lo, Nat.add(C.shift(32n, v(X.hi(pl))), C.shift(32n, C.shift(32n, SW.value(ph))))), Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), Equal.cong(Nat, Nat, z => Nat.add(lo, z), C.shift(32n, Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph)))), Nat.add(C.shift(32n, v(X.hi(pl))), C.shift(32n, C.shift(32n, SW.value(ph)))), WW.shift_add(32n, v(X.hi(pl)), C.shift(32n, SW.value(ph)))), Equal.trans(Nat, Nat.add(lo, Nat.add(C.shift(32n, v(X.hi(pl))), C.shift(32n, C.shift(32n, SW.value(ph))))), Nat.add(Nat.add(lo, C.shift(32n, v(X.hi(pl)))), C.shift(32n, C.shift(32n, SW.value(ph)))), Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), Equal.sym(Nat, Nat.add(Nat.add(lo, C.shift(32n, v(X.hi(pl)))), C.shift(32n, C.shift(32n, SW.value(ph)))), Nat.add(lo, Nat.add(C.shift(32n, v(X.hi(pl))), C.shift(32n, C.shift(32n, SW.value(ph))))), NA.add_assoc(lo, C.shift(32n, v(X.hi(pl))), C.shift(32n, C.shift(32n, SW.value(ph))))), Equal.trans(Nat, Nat.add(Nat.add(lo, C.shift(32n, v(X.hi(pl)))), C.shift(32n, C.shift(32n, SW.value(ph)))), Nat.add(SW.value(pl), C.shift(32n, C.shift(32n, SW.value(ph)))), Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, C.shift(32n, SW.value(ph)))), Nat.add(lo, C.shift(32n, v(X.hi(pl)))), SW.value(pl), Equal.sym(Nat, SW.value(pl), Nat.add(lo, C.shift(32n, v(X.hi(pl)))), WA.val_eta(pl))), Equal.cong(Nat, Nat, z => Nat.add(SW.value(pl), z), C.shift(32n, C.shift(32n, SW.value(ph))), C.shift(64n, SW.value(ph)), Equal.sym(Nat, C.shift(64n, SW.value(ph)), C.shift(32n, C.shift(32n, SW.value(ph))), WW.shift_comp(32n, 32n, SW.value(ph))))))))
57 +ems = Equal.trans(Nat, Nat.mod(Nat.add(lo, C.shift(32n, Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp))), 1n+bp), Nat.mod(Nat.add(Nat.mul(Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp), P), lo), 1n+bp), Nat.mod(Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(lo, C.shift(32n, Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp))), Nat.add(Nat.mul(Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp), P), lo), f1), Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp), P), lo), 1n+bp), Nat.mod(Nat.add(Nat.mul(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), P), lo), 1n+bp), Nat.mod(Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), 1n+bp), W64D.mstep(bp, Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), P, lo), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(Nat.mul(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), P), lo), Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), f2)))
58 +er1b = Equal.trans(Nat, SW.value(X.red96(ph, X.hi(pl), WU.U64{ml, mh})), Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), SW.value(WU.U64{ml, mh})), Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp), er1, Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), z), SW.value(WU.U64{ml, mh}), 1n+bp, hB))
59 +e3 = Equal.trans(Nat, SW.value(X.red96(X.red96(ph, X.hi(pl), WU.U64{ml, mh}), X.lo(pl), WU.U64{ml, mh})), Nat.mod(Nat.add(lo, C.shift(32n, SW.value(X.red96(ph, X.hi(pl), WU.U64{ml, mh})))), SW.value(WU.U64{ml, mh})), Nat.mod(Nat.add(lo, C.shift(32n, Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp))), 1n+bp), er2, Equal.trans(Nat, Nat.mod(Nat.add(lo, C.shift(32n, SW.value(X.red96(ph, X.hi(pl), WU.U64{ml, mh})))), SW.value(WU.U64{ml, mh})), Nat.mod(Nat.add(lo, C.shift(32n, SW.value(X.red96(ph, X.hi(pl), WU.U64{ml, mh})))), 1n+bp), Nat.mod(Nat.add(lo, C.shift(32n, Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(lo, C.shift(32n, SW.value(X.red96(ph, X.hi(pl), WU.U64{ml, mh})))), z), SW.value(WU.U64{ml, mh}), 1n+bp, hB), Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(lo, C.shift(32n, z)), 1n+bp), SW.value(X.red96(ph, X.hi(pl), WU.U64{ml, mh})), Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp), er1b)))
60 Equal.trans(Nat, SW.value(X.red96(X.red96(ph, X.hi(pl), WU.U64{ml, mh}), X.lo(pl), WU.U64{ml, mh})), Nat.mod(Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), 1n+bp), Nat.mod(pr, SW.value(WU.U64{ml, mh})), Equal.trans(Nat, SW.value(X.red96(X.red96(ph, X.hi(pl), WU.U64{ml, mh}), X.lo(pl), WU.U64{ml, mh})), Nat.mod(Nat.add(lo, C.shift(32n, Nat.mod(Nat.add(v(X.hi(pl)), C.shift(32n, SW.value(ph))), 1n+bp))), 1n+bp), Nat.mod(Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), 1n+bp), e3, ems), Equal.trans(Nat, Nat.mod(Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), 1n+bp), Nat.mod(pr, 1n+bp), Nat.mod(pr, SW.value(WU.U64{ml, mh})), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), pr, em), Equal.cong(Nat, Nat, z => Nat.mod(pr, z), 1n+bp, SW.value(WU.U64{ml, mh}), Equal.sym(Nat, SW.value(WU.U64{ml, mh}), 1n+bp, hB))))