def dig_r

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divd.bend:22

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/math/typed/w64dm.bend as DM
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mm.bend as MM

22# the remainder digit
23def dig_r(+one: Nat, +h1: {one == 1n : Nat}, +rl: U32, +rh: U32, +ml: U32, +mh: U32, +e: U32, +hx: {Nat.is_lt(SW.value(WU.U64{rl, rh}), SW.value(WU.U64{ml, mh})) == True{} : Bool}, +hz: {U32.is_zero(mh) == False{} : Bool}, +he: {Nat.is_lt(DM.X96(WU.U64{0, rl}, rh), Nat.mul(1n+v(e), SW.value(WU.U64{ml, mh}))) == True{} : Bool}) -> {SW.value(X.sub(WU.U64{0, rl}, X.fst_q(X.mul_32_64(X.q_start(WU.U64{0, rl}, rh, WU.U64{ml, mh}, e), WU.U64{ml, mh})))) == Nat.mod(C.shift(32n, SW.value(WU.U64{rl, rh})), SW.value(WU.U64{ml, mh})) : Nat}:
24  MM.red_ve(one, h1, 0, rl, rh, ml, mh, e, hx, hz, he)