def dmr_b

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64dmrem.bend:52

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend as DM
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64est.bend as W64E

52def dmr_b(+one: Nat, +h1: {one == 1n : Nat}, +al: U32, +ah: U32, +bl: U32, +bh: U32, +hb: {X.is_zero(WU.U64{bl, bh}) == False{} : Bool}, +hz: {U32.is_zero(bh) == False{} : Bool}) -> {SW.value(X.psnd(X.dm_pick(WU.U64{al, ah}, WU.U64{bl, bh}, False{}))) == Nat.mod(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})) : Nat}:
53  rem_core(one, h1, al, ah, bl, bh, X.q96(WU.U64{al, ah}, 0, WU.U64{bl, bh}, X.bitlen(bh)), le_qs(one, h1, al, ah, bl, bh, X.q_est(WU.U64{al, ah}, 0, WU.U64{bl, bh}, X.bitlen(bh)), hz, W64E.est_up(one, h1, WU.U64{al, ah}, 0, bl, bh, hz, DM.dm_hx(one, h1, al, ah, bl, bh, hz))), mod_qs(one, h1, al, ah, bl, bh, X.q_est(WU.U64{al, ah}, 0, WU.U64{bl, bh}, X.bitlen(bh)), hz, W64E.est_up(one, h1, WU.U64{al, ah}, 0, bl, bh, hz, DM.dm_hx(one, h1, al, ah, bl, bh, hz))))