def round_q

bend-collections-laws-math@1.0.0.0 · proofs/math/random/float.bend:193

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/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

193# round(q, X) for 2^52 <= q < 2^53 at the scale X = j + 2895 is pack(q, X)
194def round_q(+q: Nat, +j: Nat, +bq: {M.bit_length(q) == 53n : Nat}, +hz: {Nat.is_eq(q, 0n) == False{} : Bool}) -> {SF.round(False{}, q, Nat.add(j, 2895n)) == SF.pack(False{}, q, Nat.add(j, 2895n)) : F.F64}:
195  +X = Nat.add(j, 2895n)
196  +U = Nat.max(Nat.sub(Nat.add(X, M.bit_length(q)), 53n), Nat.sub(SF.zb(), 1074n))
197  +hle = Equal.trans(Bool, Nat.is_le(1926n, X), Nat.is_le(1926n, Nat.add(2895n, j)), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(1926n, z), X, Nat.add(2895n, j), N.add_comm(j, 2895n)), {==})
198  +eU = Equal.trans(Nat, U, Nat.max(Nat.sub(Nat.add(X, 53n), 53n), 1926n), X, Equal.cong(Nat, Nat, z => Nat.max(Nat.sub(Nat.add(X, z), 53n), Nat.sub(SF.zb(), 1074n)), M.bit_length(q), 53n, bq),
199    Equal.trans(Nat, Nat.max(Nat.sub(Nat.add(X, 53n), 53n), 1926n), Nat.max(X, 1926n), X, Equal.cong(Nat, Nat, z => Nat.max(z, 1926n), Nat.sub(Nat.add(X, 53n), 53n), X, sub_add53(X)), max_l(X, 1926n, hle)))
200  +r1 = Equal.cong(Bool, F.F64, c => SF.pick(F.F64, c, SF.zero(False{}), SF.round_u(False{}, q, X, U)), Nat.is_eq(q, 0n), False{}, hz)
201  +r2 = Equal.cong(Nat, F.F64, z => SF.round_u(False{}, q, X, z), U, X, eU)
202  +r3 = Equal.cong(Bool, F.F64, c => SF.pack(False{}, SF.pick(Nat, c, SF.rne(q, Nat.sub(X, X)), C.shift(Nat.sub(X, X), q)), X), Nat.is_le(X, X), True{}, N.le_refl(X))
203  +r4 = Equal.cong(Nat, F.F64, z => SF.pack(False{}, SF.rne(q, z), X), Nat.sub(X, X), 0n, N.sub_self(X))
204  Equal.trans(F.F64, SF.round(False{}, q, X), SF.round_u(False{}, q, X, U), SF.pack(False{}, q, X), r1,
205    Equal.trans(F.F64, SF.round_u(False{}, q, X, U), SF.round_u(False{}, q, X, X), SF.pack(False{}, q, X), r2,
206      Equal.trans(F.F64, SF.round_u(False{}, q, X, X), SF.pack(False{}, SF.rne(q, Nat.sub(X, X)), X), SF.pack(False{}, q, X), r3, r4)))