def enc

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

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/spec/math/f64.bend as SF
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/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
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/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

116# the implementation's bits are encode(False, e, q mod 2^52) for the value
117# q < 2^53 of the shifted significand
118def enc(+one: Nat, +h1: {one == 1n : Nat}, +Q: WU.U64, +e: Nat, +he: {Nat.is_lt(e, 2048n) == True{} : Bool}, +q: Nat, +hq: {SW.value(Q) == q : Nat}, +f53: {C.fits(53n, q) == True{} : Bool}) -> {bits(Q, e) == SF.encode(False{}, e, C.low(52n, q)) : F.F64}:
119  +ql = X.lo(Q)
120  +qh = X.hi(Q)
121  +lq = C.low(20n, v(qh))
122  +hq2 = Equal.trans(Nat, q, SW.value(Q), Nat.add(v(ql), C.shift(32n, v(qh))), Equal.sym(Nat, SW.value(Q), q, hq), value_eta(Q))
123  +f = C.low(52n, q)
124  +F1 = Nat.add(v(ql), C.shift(32n, lq))
125  +s1 = FB.low_split(32n, 20n, q)
126  +el = Equal.trans(Nat, C.low(32n, q), C.low(32n, Nat.add(v(ql), C.shift(32n, v(qh)))), v(ql), Equal.cong(Nat, Nat, z => C.low(32n, z), q, Nat.add(v(ql), C.shift(32n, v(qh))), hq2), WW.low_u(32n, v(ql), v(qh), LW.vb(ql)))
127  +eh = Equal.trans(Nat, C.high(32n, q), C.high(32n, Nat.add(v(ql), C.shift(32n, v(qh)))), v(qh), Equal.cong(Nat, Nat, z => C.high(32n, z), q, Nat.add(v(ql), C.shift(32n, v(qh))), hq2), WW.high_u(32n, v(ql), v(qh), LW.vb(ql)))
128  +ef1 = Equal.trans(Nat, f, Nat.add(C.low(32n, q), C.shift(32n, C.low(20n, C.high(32n, q)))), F1, s1,
129    Equal.trans(Nat, Nat.add(C.low(32n, q), C.shift(32n, C.low(20n, C.high(32n, q)))), Nat.add(v(ql), C.shift(32n, C.low(20n, C.high(32n, q)))), F1, Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, C.low(20n, C.high(32n, q)))), C.low(32n, q), v(ql), el),
130      Equal.cong(Nat, Nat, z => Nat.add(v(ql), C.shift(32n, C.low(20n, z))), C.high(32n, q), v(qh), eh)))
131  +elo = Equal.trans(Nat, C.low(32n, f), C.low(32n, F1), v(ql), Equal.cong(Nat, Nat, z => C.low(32n, z), f, F1, ef1), WW.low_u(32n, v(ql), lq, LW.vb(ql)))
132  +ehi0 = Equal.trans(Nat, C.high(32n, f), C.high(32n, F1), lq, Equal.cong(Nat, Nat, z => C.high(32n, z), f, F1, ef1), WW.high_u(32n, v(ql), lq, LW.vb(ql)))
133  +T = Nat.add(e, C.shift(11n, SF.b2n(False{})))
134  +ehi1 = Equal.trans(Nat, Nat.add(C.high(32n, f), C.shift(20n, T)), Nat.add(lq, C.shift(20n, T)), Nat.add(lq, C.shift(20n, e)), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(20n, T)), C.high(32n, f), lq, ehi0), Equal.cong(Nat, Nat, z => Nat.add(lq, C.shift(20n, z)), T, e, N.add_zero(e)))
135  +ehi2 = Equal.trans(Nat, Nat.add(C.high(32n, f), C.shift(20n, T)), Nat.add(lq, C.shift(20n, e)), v(hw(e, qh)), ehi1, Equal.sym(Nat, v(hw(e, qh)), Nat.add(lq, C.shift(20n, e)), hw_value(one, h1, e, qh, he)))
136  +wlo = Equal.trans(U32, U32.from_nat(C.low(32n, f)), U32.from_nat(v(ql)), ql, Equal.cong(Nat, U32, z => U32.from_nat(z), C.low(32n, f), v(ql), elo), LW.rt(ql))
137  +whi = Equal.trans(U32, U32.from_nat(Nat.add(C.high(32n, f), C.shift(20n, T))), U32.from_nat(v(hw(e, qh))), hw(e, qh), Equal.cong(Nat, U32, z => U32.from_nat(z), Nat.add(C.high(32n, f), C.shift(20n, T)), v(hw(e, qh)), ehi2), LW.rt(hw(e, qh)))
138  +lo_s = U32.from_nat(C.low(32n, f))
139  +hi_s = U32.from_nat(Nat.add(C.high(32n, f), C.shift(20n, T)))
140  Equal.sym(F.F64, F.Bits{lo_s, hi_s}, F.Bits{ql, hw(e, qh)}, Equal.trans(F.F64, F.Bits{lo_s, hi_s}, F.Bits{ql, hi_s}, F.Bits{ql, hw(e, qh)}, Equal.cong(U32, F.F64, z => F.Bits{z, hi_s}, lo_s, ql, wlo), Equal.cong(U32, F.F64, z => F.Bits{ql, z}, hi_s, hw(e, qh), whi)))