def mm_big

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mmtop.bend:62

import Base
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/math/typed/w64mul.bend as W64M
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend as M128

62def 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}:
63  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)