def dmr_s

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

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

30def dmr_s(+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) == True{} : Bool}) -> {SW.value(X.psnd(X.dm_pick(WU.U64{al, ah}, WU.U64{bl, bh}, True{}))) == Nat.mod(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})) : Nat}:
31  Equal.trans(Nat, SW.value(WU.U64{X.snd_r(X.div32(WU.U64{al, ah}, bl)), 0}), DM.v(X.snd_r(X.div32(WU.U64{al, ah}, bl))), Nat.mod(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), DM.u32_0(X.snd_r(X.div32(WU.U64{al, ah}, bl))), Equal.trans(Nat, DM.v(X.snd_r(X.div32(WU.U64{al, ah}, bl))), Nat.mod(SW.value(WU.U64{al, ah}), DM.v(bl)), Nat.mod(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), W64D.div32_rem(WU.U64{al, ah}, bl, hd_small(bl, bh, hb, hz)), Equal.cong(Nat, Nat, t => Nat.mod(SW.value(WU.U64{al, ah}), t), DM.v(bl), SW.value(WU.U64{bl, bh}), Equal.sym(Nat, SW.value(WU.U64{bl, bh}), DM.v(bl), vb_small(bl, bh, hz)))))