proofs/math/typed/f64misc.bend
bend-collections-laws-math@1.0.0.0 · 94 lines · 11 definitions
1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
4import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
5import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
6import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
7import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
9import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
10import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T
13
14
15
16
17
18
19
20
21def v(+x: U32) -> Nat:
22 U32.to_nat(x)
23
24
25
26def of_u64_value(+w: WU.U64) -> SF.OfU64.value(w):
27 T.rw_value(False{}, 3000n, w, {==})
28
29def of_u32_value(+u: U32) -> SF.OfU32.value(u):
30 +e1 = T.rw_value(False{}, 3000n, WU.U64{u, 0}, {==})
31 +e2 = Equal.cong(Nat, F.F64, t => SF.round(False{}, t, 3000n), Nat.add(v(u), 0n), v(u), N.add_zero(v(u)))
32 Equal.trans(F.F64, F.of_u32(u), SF.round(False{}, Nat.add(v(u), 0n), 3000n), SF.round(False{}, v(u), SF.zb()), e1, e2)
33
34
35
36def ulp_c(+x: F.F64, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {F.ulp_cls(x, t) == SF.pick(F.F64, Bool.and(t, Bool.not(z)), SF.qnan(), SF.pick(F.F64, Bool.and(t, z), SF.inf(False{}), SF.round(False{}, 1n, SF.xexp(x)))) : F.F64}:
37 match t z:
38 case True{} True{}:
39 Equal.cong(Bool, F.F64, b => F.nan_or(F.inf(False{}), Bool.not(b)), X.is_zero(F.frac(x)), True{}, hz)
40 case True{} False{}:
41 Equal.cong(Bool, F.F64, b => F.nan_or(F.inf(False{}), Bool.not(b)), X.is_zero(F.frac(x)), False{}, hz)
42 case False{} _:
43 +e1 = T.rw_value(False{}, F.dexp(x), WU.U64{1, 0}, T.dexp_ge(x))
44 +e2 = Equal.cong(Nat, F.F64, t => SF.round(False{}, 1n, t), F.dexp(x), SF.xexp(x), T.dexp_value(x))
45 Equal.trans(F.F64, F.round_w(False{}, F.dexp(x), WU.U64{1, 0}), SF.round(False{}, 1n, F.dexp(x)), SF.round(False{}, 1n, SF.xexp(x)), e1, e2)
46
47def ulp_value(+x: F.F64) -> SF.Ulp.value(x):
48 +e1 = Equal.cong(Nat, F.F64, t => F.ulp_cls(x, Nat.is_eq(t, 2047n)), F.exp_field(x), SF.efield(x), T.ea(x))
49 Equal.trans(F.F64, F.ulp(x), F.ulp_cls(x, Nat.is_eq(SF.efield(x), 2047n)), SF.pick(F.F64, SF.is_nan(x), SF.qnan(), SF.pick(F.F64, SF.is_inf(x), SF.inf(False{}), SF.round(False{}, 1n, SF.xexp(x)))), e1, ulp_c(x, Nat.is_eq(SF.efield(x), 2047n), Nat.is_eq(SF.frac(x), 0n), T.fz(x)))
50
51
52
53def is_normal_value(+x: F.F64) -> SF.IsNormal.value(x):
54 Equal.cong(Nat, Bool, t => Bool.and(Bool.not(Nat.is_eq(t, 0n)), Nat.is_lt(t, 2047n)), F.exp_field(x), SF.efield(x), T.ea(x))
55
56def is_subnormal_value(+x: F.F64) -> SF.IsSubnormal.value(x):
57 +e1 = Equal.cong(Nat, Bool, t => Bool.and(Nat.is_eq(t, 0n), Bool.not(X.is_zero(F.frac(x)))), F.exp_field(x), SF.efield(x), T.ea(x))
58 +e2 = Equal.cong(Bool, Bool, b => Bool.and(Nat.is_eq(SF.efield(x), 0n), Bool.not(b)), X.is_zero(F.frac(x)), Nat.is_eq(SF.frac(x), 0n), T.fz(x))
59 Equal.trans(Bool, F.is_subnormal(x), Bool.and(Nat.is_eq(SF.efield(x), 0n), Bool.not(X.is_zero(F.frac(x)))), Bool.and(Nat.is_eq(SF.efield(x), 0n), Bool.not(Nat.is_eq(SF.frac(x), 0n))), e1, e2)
60
61
62
63def bits_g(+l: U32, +h: U32) -> {Nat.add(v(l), C.shift(32n, v(h))) == Nat.add(SF.pat(F.Bits{l, h}), C.shift(63n, SF.b2n(SF.sign(F.Bits{l, h})))) : Nat}:
64 +H = v(h)
65 +Lo = C.low(31n, H)
66 +Hh = C.high(31n, H)
67 +e1 = Equal.cong(Nat, Nat, t => Nat.add(v(l), C.shift(32n, t)), H, Nat.add(Lo, C.shift(31n, Hh)), WW.low_high(31n, H))
68 +e2 = Equal.cong(Nat, Nat, t => Nat.add(v(l), t), C.shift(32n, Nat.add(Lo, C.shift(31n, Hh))), Nat.add(C.shift(32n, Lo), C.shift(32n, C.shift(31n, Hh))), WW.shift_add(32n, Lo, C.shift(31n, Hh)))
69 +e3 = Equal.cong(Nat, Nat, t => Nat.add(v(l), Nat.add(C.shift(32n, Lo), t)), C.shift(32n, C.shift(31n, Hh)), C.shift(63n, Hh), Equal.sym(Nat, C.shift(63n, Hh), C.shift(32n, C.shift(31n, Hh)), WW.shift_comp(32n, 31n, Hh)))
70 +e4 = Equal.sym(Nat, Nat.add(Nat.add(v(l), C.shift(32n, Lo)), C.shift(63n, Hh)), Nat.add(v(l), Nat.add(C.shift(32n, Lo), C.shift(63n, Hh))), NA.add_assoc(v(l), C.shift(32n, Lo), C.shift(63n, Hh)))
71 +e5 = Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(63n, Hh)), Nat.add(v(l), C.shift(32n, Lo)), SF.pat(F.Bits{l, h}), FC.magQ(l, h))
72 +e6 = Equal.cong(Nat, Nat, t => Nat.add(SF.pat(F.Bits{l, h}), C.shift(63n, t)), Hh, SF.b2n(SF.sign(F.Bits{l, h})), FB.bit_c(Hh, FB.half0(h)))
73 +a1 = Nat.add(v(l), C.shift(32n, Nat.add(Lo, C.shift(31n, Hh))))
74 +a2 = Nat.add(v(l), Nat.add(C.shift(32n, Lo), C.shift(32n, C.shift(31n, Hh))))
75 +a3 = Nat.add(v(l), Nat.add(C.shift(32n, Lo), C.shift(63n, Hh)))
76 +a4 = Nat.add(Nat.add(v(l), C.shift(32n, Lo)), C.shift(63n, Hh))
77 +a5 = Nat.add(SF.pat(F.Bits{l, h}), C.shift(63n, Hh))
78 +a6 = Nat.add(SF.pat(F.Bits{l, h}), C.shift(63n, SF.b2n(SF.sign(F.Bits{l, h}))))
79 Equal.trans(Nat, Nat.add(v(l), C.shift(32n, H)), a1, a6, e1, Equal.trans(Nat, a1, a2, a6, e2, Equal.trans(Nat, a2, a3, a6, e3, Equal.trans(Nat, a3, a4, a6, e4, Equal.trans(Nat, a4, a5, a6, e5, e6)))))
80
81def bits_value(+x: F.F64) -> SF.Bits.value(x):
82 match x:
83 case F.Bits{+l, +h}:
84 bits_g(l, h)
85
86def bits_roundtrip(+x: F.F64) -> SF.Bits.roundtrip(x):
87 match x:
88 case F.Bits{+l, +h}:
89 {==}
90
91def bits_inverse(+w: WU.U64) -> SF.Bits.inverse(w):
92 match w:
93 case WU.U64{+l, +h}:
94 {==}