def red_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mm.bend:74

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/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend as W64E

74def red_v(+one: Nat, +h1: {one == 1n : Nat}, +x0: U32, +y0: U32, +y1: U32, +ml: U32, +mh: U32, +hx: {Nat.is_lt(SW.value(WU.U64{y0, y1}), SW.value(WU.U64{ml, mh})) == True{} : Bool}, +hz: {U32.is_zero(mh) == False{} : Bool}) -> {SW.value(X.red96(WU.U64{y0, y1}, x0, WU.U64{ml, mh})) == Nat.mod(Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), SW.value(WU.U64{ml, mh})) : Nat}:
75  L.subst(Bool, t => {SW.value(X.red96_z(WU.U64{y0, y1}, x0, WU.U64{ml, mh}, t)) == Nat.mod(Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), SW.value(WU.U64{ml, mh})) : Nat}, False{}, U32.is_zero(mh), Equal.sym(Bool, U32.is_zero(mh), False{}, hz), red_ve(one, h1, x0, y0, y1, ml, mh, X.q_est(WU.U64{x0, y0}, y1, WU.U64{ml, mh}, X.bitlen(mh)), hx, hz, W64E.est_up(one, h1, WU.U64{x0, y0}, y1, ml, mh, hz, red_hx(one, h1, x0, y0, y1, ml, mh, hx))))