~/bend-docscommunity

proofs/math/typed/w64mmtop.bend source

proofs/math/typed/w64mmtop.bend on the hub · documented module

import Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/math/w64.bend as SWimport ../../../src/math/w64.bend as Ximport ../../../src/math/u64.bend as WUimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../natural/arith.bend as NRimport ./w64mul.bend as W64Mimport ./w64div.bend as W64Dimport ./w64add.bend as WAimport ./w64m128.bend as M128import ./w64mm.bend as MMimport ./width.bend as WWimport ./u32laws.bend as LW# MulMod.value of spec/math/w64.bend.def v(+x: U32) -> Nat:  U32.to_nat(x)def val0(+x: U32) -> {SW.value(WU.U64{x, 0}) == v(x) : Nat}:  Equal.trans(Nat, Nat.add(v(x), C.shift(32n, 0n)), Nat.add(v(x), 0n), v(x), Equal.cong(Nat, Nat, z => Nat.add(v(x), z), C.shift(32n, 0n), 0n, WW.shift_zero(32n)), N.add_zero(v(x)))def vm_small(+ml: U32, +mh: U32, +hz: {U32.is_zero(mh) == True{} : Bool}) -> {SW.value(WU.U64{ml, mh}) == v(ml) : Nat}:  +e0 = N.eq_from_is_eq(v(mh), 0n, Equal.trans(Bool, Nat.is_eq(v(mh), 0n), U32.is_zero(mh), True{}, Equal.sym(Bool, U32.is_zero(mh), Nat.is_eq(v(mh), 0n), LW.zero_nat(mh)), hz))  Equal.trans(Nat, SW.value(WU.U64{ml, mh}), Nat.add(v(ml), C.shift(32n, 0n)), v(ml), Equal.cong(Nat, Nat, z => Nat.add(v(ml), C.shift(32n, z)), v(mh), 0n, e0), Equal.trans(Nat, Nat.add(v(ml), C.shift(32n, 0n)), Nat.add(v(ml), 0n), v(ml), Equal.cong(Nat, Nat, z => Nat.add(v(ml), z), C.shift(32n, 0n), 0n, WW.shift_zero(32n)), N.add_zero(v(ml))))def mm_small(+al: U32, +ah: U32, +bl: U32, +bh: U32, +ml: U32, +mh: U32, +ha: {Nat.is_lt(SW.value(WU.U64{al, ah}), SW.value(WU.U64{ml, mh})) == True{} : Bool}, +hb: {Nat.is_lt(SW.value(WU.U64{bl, bh}), SW.value(WU.U64{ml, mh})) == True{} : Bool}, +hz: {U32.is_zero(mh) == True{} : Bool}) -> {SW.value(X.mm_pick(WU.U64{al, ah}, WU.U64{bl, bh}, WU.U64{ml, mh}, True{})) == Nat.mod(Nat.mul(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), SW.value(WU.U64{ml, mh})) : Nat}:  +evm = vm_small(ml, mh, hz)  +ha1 = L.subst(Nat, z => {Nat.is_lt(SW.value(WU.U64{al, ah}), z) == True{} : Bool}, SW.value(WU.U64{ml, mh}), v(ml), evm, ha)  +hb1 = L.subst(Nat, z => {Nat.is_lt(SW.value(WU.U64{bl, bh}), z) == True{} : Bool}, SW.value(WU.U64{ml, mh}), v(ml), evm, hb)  +eva = MM.hi0(1n, {==}, al, ah, ml, ha1, v(ah), {==})  +evb = MM.hi0(1n, {==}, bl, bh, ml, hb1, v(bh), {==})  +hpos = N.le_lt_trans(0n, SW.value(WU.U64{al, ah}), v(ml), N.zero_le(SW.value(WU.U64{al, ah})), ha1)  +hd = LW.nz(ml, N.is_eq_sym_false(0n, v(ml), N.is_eq_lt(0n, v(ml), hpos)))  +p = X.mul32(al, bl)  Equal.trans(Nat, SW.value(WU.U64{X.mod32(p, ml), 0}), v(X.mod32(p, ml)), Nat.mod(Nat.mul(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), SW.value(WU.U64{ml, mh})), val0(X.mod32(p, ml)), Equal.trans(Nat, v(X.mod32(p, ml)), Nat.mod(SW.value(p), v(ml)), Nat.mod(Nat.mul(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), SW.value(WU.U64{ml, mh})), W64D.mod32_value(p, ml, hd), Equal.trans(Nat, Nat.mod(SW.value(p), v(ml)), Nat.mod(Nat.mul(v(al), v(bl)), v(ml)), Nat.mod(Nat.mul(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), SW.value(WU.U64{ml, mh})), Equal.cong(Nat, Nat, z => Nat.mod(z, v(ml)), SW.value(p), Nat.mul(v(al), v(bl)), W64M.mul32_value(al, bl)), Equal.sym(Nat, Nat.mod(Nat.mul(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), SW.value(WU.U64{ml, mh})), Nat.mod(Nat.mul(v(al), v(bl)), v(ml)), Equal.trans(Nat, Nat.mod(Nat.mul(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), SW.value(WU.U64{ml, mh})), Nat.mod(Nat.mul(v(al), SW.value(WU.U64{bl, bh})), SW.value(WU.U64{ml, mh})), Nat.mod(Nat.mul(v(al), v(bl)), v(ml)), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(z, SW.value(WU.U64{bl, bh})), SW.value(WU.U64{ml, mh})), SW.value(WU.U64{al, ah}), v(al), eva), Equal.trans(Nat, Nat.mod(Nat.mul(v(al), SW.value(WU.U64{bl, bh})), SW.value(WU.U64{ml, mh})), Nat.mod(Nat.mul(v(al), v(bl)), SW.value(WU.U64{ml, mh})), Nat.mod(Nat.mul(v(al), v(bl)), v(ml)), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(v(al), z), SW.value(WU.U64{ml, mh})), SW.value(WU.U64{bl, bh}), v(bl), evb), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(v(al), v(bl)), z), SW.value(WU.U64{ml, mh}), v(ml), evm)))))))def 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}:  +S = C.shift(64n, one)  +ePH = WW.shift_mul_one(64n, one, h1, SW.value(ph))  +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)))))  +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})))))  +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))  +hPH = W64D.lt_cancel_mul(SW.value(ph), SW.value(WU.U64{ml, mh}), S, h3a)  +er1 = MM.red_vg(one, h1, X.hi(pl), ph, ml, mh, hPH, hz)  +bp = Nat.sub(SW.value(WU.U64{ml, mh}), 1n)  +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))))  +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))))))  +er2 = MM.red_vg(one, h1, X.lo(pl), X.red96(ph, X.hi(pl), WU.U64{ml, mh}), ml, mh, hr1, hz)  +P = C.shift(32n, one)  +lo = v(X.lo(pl))  +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)))  +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))))))))  +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)))  +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))  +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)))  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))))def mm_big(+al: U32, +ah: U32, +bl: U32, +bh: U32, +ml: U32, +mh: U32, +ha: {Nat.is_lt(SW.value(WU.U64{al, ah}), SW.value(WU.U64{ml, mh})) == True{} : Bool}, +hb: {Nat.is_lt(SW.value(WU.U64{bl, bh}), SW.value(WU.U64{ml, mh})) == True{} : Bool}, +hz: {U32.is_zero(mh) == False{} : Bool}) -> {SW.value(X.red96(X.red96(X.psnd(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh})), X.hi(X.pfst(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh}))), WU.U64{ml, mh}), X.lo(X.pfst(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh}))), WU.U64{ml, mh})) == Nat.mod(Nat.mul(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), SW.value(WU.U64{ml, mh})) : Nat}:  mm_bg(1n, {==}, X.pfst(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh})), X.psnd(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh})), Nat.mul(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), M128.m128_value(al, ah, bl, bh), ml, mh, W64M.mul_lt_sq(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh}), SW.value(WU.U64{ml, mh}), ha, hb), hz)def mm_c(+al: U32, +ah: U32, +bl: U32, +bh: U32, +ml: U32, +mh: U32, +ha: {Nat.is_lt(SW.value(WU.U64{al, ah}), SW.value(WU.U64{ml, mh})) == True{} : Bool}, +hb: {Nat.is_lt(SW.value(WU.U64{bl, bh}), SW.value(WU.U64{ml, mh})) == True{} : Bool}, +z: Bool, +hz: {U32.is_zero(mh) == z : Bool}) -> {SW.value(X.mm_pick(WU.U64{al, ah}, WU.U64{bl, bh}, WU.U64{ml, mh}, z)) == Nat.mod(Nat.mul(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), SW.value(WU.U64{ml, mh})) : Nat}:  match z:    case True{}:      mm_small(al, ah, bl, bh, ml, mh, ha, hb, hz)    case False{}:      mm_big(al, ah, bl, bh, ml, mh, ha, hb, hz)def mulmod_value(+a: WU.U64, +b: WU.U64, +m: WU.U64, +ha: {Nat.is_lt(SW.value(a), SW.value(m)) == True{} : Bool}, +hb: {Nat.is_lt(SW.value(b), SW.value(m)) == True{} : Bool}) -> SW.MulMod.value(a, b, m, ha, hb):  match a b m:    case WU.U64{+al, +ah} WU.U64{+bl, +bh} WU.U64{+ml, +mh}:      mm_c(al, ah, bl, bh, ml, mh, ha, hb, U32.is_zero(mh), {==})