~/jendhub

def rpv

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:281

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as F64round
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/f64.bend as SF
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/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A

281# the rounded significand of roundPackToF64 is rne(sig, 10)
282def rpv(+l: U32, +h: U32, +hS: {C.fits(63n, SW.value(WU.U64{l, h})) == True{} : Bool}) -> {SW.value(X.clear0(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n), U32.is_eq(U32.and(l, 1023), 512))) == SF.rne(SW.value(WU.U64{l, h}), 10n) : Nat}:
283  a1 = WA.add_value(WU.U64{l, h}, WU.U64{512, 0})
284  +ev1 = Equal.trans(Nat, SW.value(X.add(WU.U64{l, h}, WU.U64{512, 0})), C.low(64n, Nat.add(SW.value(WU.U64{l, h}), 512n)), Nat.add(SW.value(WU.U64{l, h}), 512n), a1, WW.low_fit(64n, Nat.add(SW.value(WU.U64{l, h}), 512n), fits_add1(63n, SW.value(WU.U64{l, h}), 512n, hS, {==})))
285  s1 = SH.shr_value(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)
286  +ev2 = Equal.trans(Nat, SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), C.high(10n, SW.value(X.add(WU.U64{l, h}, WU.U64{512, 0}))), C.high(10n, Nat.add(SW.value(WU.U64{l, h}), 512n)), s1, Equal.cong(Nat, Nat, z => C.high(10n, z), SW.value(X.add(WU.U64{l, h}, WU.U64{512, 0})), Nat.add(SW.value(WU.U64{l, h}), 512n), ev1))
287  +sp = Equal.trans(Nat, C.high(10n, Nat.add(SW.value(WU.U64{l, h}), 512n)), C.high(10n, Nat.add(Nat.add(C.low(10n, SW.value(WU.U64{l, h})), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h})))), 512n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), Equal.cong(Nat, Nat, z => C.high(10n, Nat.add(z, 512n)), SW.value(WU.U64{l, h}), Nat.add(C.low(10n, SW.value(WU.U64{l, h})), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h})))), WW.low_high(10n, SW.value(WU.U64{l, h}))), Equal.trans(Nat, C.high(10n, Nat.add(Nat.add(C.low(10n, SW.value(WU.U64{l, h})), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h})))), 512n)), C.high(10n, Nat.add(Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h}))))), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), Equal.cong(Nat, Nat, z => C.high(10n, z), Nat.add(Nat.add(C.low(10n, SW.value(WU.U64{l, h})), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h})))), 512n), Nat.add(Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h})))), A.add_rot(C.low(10n, SW.value(WU.U64{l, h})), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h}))), 512n)), Equal.trans(Nat, C.high(10n, Nat.add(Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h}))))), Nat.add(C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n)), C.high(10n, SW.value(WU.U64{l, h}))), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), WW.high_add_shift(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n), C.high(10n, SW.value(WU.U64{l, h}))), NA.add_comm(C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n)), C.high(10n, SW.value(WU.U64{l, h}))))))
288  +ev3 = Equal.trans(Nat, SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), C.high(10n, Nat.add(SW.value(WU.U64{l, h}), 512n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), ev2, sp)
289  +ec = cv(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n), U32.is_eq(U32.and(l, 1023), 512))
290  +e4 = Equal.cong(Nat, Nat, z => SF.pick(Nat, U32.is_eq(U32.and(l, 1023), 512), Nat.sub(z, Nat.mod(z, 2n)), z), SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), ev3)
291  +e5 = Equal.cong(Bool, Nat, t => SF.pick(Nat, t, Nat.sub(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), Nat.mod(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), 2n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n)))), U32.is_eq(U32.and(l, 1023), 512), Nat.is_eq(C.low(10n, SW.value(WU.U64{l, h})), 512n), tie_v(l, h))
292  Equal.trans(Nat, SW.value(X.clear0(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n), U32.is_eq(U32.and(l, 1023), 512))), SF.pick(Nat, U32.is_eq(U32.and(l, 1023), 512), Nat.sub(SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), Nat.mod(SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), 2n)), SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n))), SF.rne_up(C.high(10n, SW.value(WU.U64{l, h})), C.low(10n, SW.value(WU.U64{l, h})), 512n), ec, Equal.trans(Nat, SF.pick(Nat, U32.is_eq(U32.and(l, 1023), 512), Nat.sub(SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), Nat.mod(SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), 2n)), SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n))), SF.pick(Nat, U32.is_eq(U32.and(l, 1023), 512), Nat.sub(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), Nat.mod(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), 2n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n)))), SF.rne_up(C.high(10n, SW.value(WU.U64{l, h})), C.low(10n, SW.value(WU.U64{l, h})), 512n), e4, Equal.trans(Nat, SF.pick(Nat, U32.is_eq(U32.and(l, 1023), 512), Nat.sub(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), Nat.mod(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), 2n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n)))), SF.pick(Nat, Nat.is_eq(C.low(10n, SW.value(WU.U64{l, h})), 512n), Nat.sub(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), Nat.mod(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), 2n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n)))), SF.rne_up(C.high(10n, SW.value(WU.U64{l, h})), C.low(10n, SW.value(WU.U64{l, h})), 512n), e5, rp_c(C.high(10n, SW.value(WU.U64{l, h})), C.low(10n, SW.value(WU.U64{l, h})), WW.low_fits(10n, SW.value(WU.U64{l, h})), Nat.cmp(C.low(10n, SW.value(WU.U64{l, h})), 512n), {==}))))

Uses (36)

Used by (1)