def dq_round

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divq.bend:65

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/f64.bend as F
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/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT

65# roundPackToF64 of the quotient significand is the spec's round of its value
66def dq_round(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +d1: U32, +d2: U32, +r2w: WU.U64, +c: U32, +hc: {c == U32{WD.pw(32n, 30n)} : U32}) -> {F.round_pack(s, e, X.or_bit(X.add(WU.U64{0, c}, X.shr(WU.U64{d2, d1}, 2n)), Bool.or(F.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3)))))) == SF.round(s, SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n))))), x) : F.F64}:
67  +ev = sig_v(one, h1, d1, d2, r2w, c, hc)
68  +J = SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n)))))
69  +h63 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n))))), SW.value(X.or_bit(X.add(WU.U64{0, c}, X.shr(WU.U64{d2, d1}, 2n)), Bool.or(F.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3)))))), Equal.sym(Nat, SW.value(X.or_bit(X.add(WU.U64{0, c}, X.shr(WU.U64{d2, d1}, 2n)), Bool.or(F.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3)))))), SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n))))), ev), Equal.trans(Bool, C.fits(63n, SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n)))))), C.fits(63n, Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1})))), True{}, RT.jam_fits(62n, Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n))))), t63(one, h1, d1, d2)))
70  +h62 = L.subst(Nat, z => {C.fits(62n, z) == False{} : Bool}, SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n))))), SW.value(X.or_bit(X.add(WU.U64{0, c}, X.shr(WU.U64{d2, d1}, 2n)), Bool.or(F.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3)))))), Equal.sym(Nat, SW.value(X.or_bit(X.add(WU.U64{0, c}, X.shr(WU.U64{d2, d1}, 2n)), Bool.or(F.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3)))))), SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n))))), ev), Equal.trans(Bool, C.fits(62n, SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n)))))), C.fits(62n, Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1})))), False{}, RT.jam_fits(61n, Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n))))), t62(one, h1, d1, d2)))
71  +r1 = FR.round_pack(s, e, X.or_bit(X.add(WU.U64{0, c}, X.shr(WU.U64{d2, d1}, 2n)), Bool.or(F.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3))))), x, hx, h62, h63)
72  Equal.trans(F.F64, F.round_pack(s, e, X.or_bit(X.add(WU.U64{0, c}, X.shr(WU.U64{d2, d1}, 2n)), Bool.or(F.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3)))))), SF.round(s, SW.value(X.or_bit(X.add(WU.U64{0, c}, X.shr(WU.U64{d2, d1}, 2n)), Bool.or(F.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3)))))), x), SF.round(s, SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n))))), x), r1, Equal.cong(Nat, F.F64, z => SF.round(s, z, x), SW.value(X.or_bit(X.add(WU.U64{0, c}, X.shr(WU.U64{d2, d1}, 2n)), Bool.or(F.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3)))))), SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{d2, d1}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n))))), ev))