Float.enc: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend as Float Lines 116-140 of bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&start_line=116&end_line=140 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 # the implementation's bits are encode(False, e, q mod 2^52) for the value # q < 2^53 of the shifted significand def 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}: +ql = X.lo(Q) +qh = X.hi(Q) +lq = C.low(20n, v(qh)) +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)) +f = C.low(52n, q) +F1 = Nat.add(v(ql), C.shift(32n, lq)) +s1 = FB.low_split(32n, 20n, q) +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))) +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))) +ef1 = Equal.trans(Nat, f, Nat.add(C.low(32n, q), C.shift(32n, C.low(20n, C.high(32n, q)))), F1, s1, 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), Equal.cong(Nat, Nat, z => Nat.add(v(ql), C.shift(32n, C.low(20n, z))), C.high(32n, q), v(qh), eh))) +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))) +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))) +T = Nat.add(e, C.shift(11n, SF.b2n(False{}))) +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))) +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))) +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)) +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))) +lo_s = U32.from_nat(C.low(32n, f)) +hi_s = U32.from_nat(Nat.add(C.high(32n, f), C.shift(20n, T))) 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))) Uses (31): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=bits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=hw https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=hw_value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=value_eta https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=low_split https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend&name=rt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend&name=vb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=high_u https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_u https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=b2n https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=encode https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=hi https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=lo