proofs/math/typed/f64norm.bend

bend-collections-laws-math@1.0.0.0 · 161 lines · 14 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/spec/math/w64.bend as SW
5import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
6import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
7import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
8import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
9import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
10import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
11import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
12import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as UH
13import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
14import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as BT
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as CLZ
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
21import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
22import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as BL
23import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC
24
25# SoftFloat's normSubnormalF64Sig and the hidden bit: a finite nonzero
26# double's significand as a 53-bit A = m * 2^sa (m the spec's mant) at the
27# offset exponent norm_e, with norm_e + sa = xexp + 2171.
28
29def v(+x: U32) -> Nat:
30  U32.to_nat(x)
31
32def sa(+ea: Nat, +fa: WU.U64) -> Nat:
33  match ea:
34    case 0n:
35      Nat.sub(X.clz(fa), 11n)
36    case _:
37      0n
38
39# the hidden bit: f + 2^52 for a fraction below 2^52
40def hid(+one: Nat, +h1: {one == 1n : Nat}, +fa: WU.U64, +hF: {C.fits(52n, SW.value(fa)) == True{} : Bool}, +c: U32, +hc: {c == U32{WD.pw(32n, 20n)} : U32}) -> {SW.value(X.add(fa, WU.U64{0, c})) == Nat.add(SW.value(fa), C.shift(52n, one)) : Nat}:
41  a1 = WA.add_value(fa, WU.U64{0, c})
42  +ec = Equal.trans(Nat, C.shift(32n, v(c)), C.shift(32n, C.shift(20n, one)), C.shift(52n, one), Equal.cong(Nat, Nat, z => C.shift(32n, z), v(c), C.shift(20n, one), FB.pwv(20n, {==}, one, h1, c, hc)), Equal.sym(Nat, C.shift(52n, one), C.shift(32n, C.shift(20n, one)), WW.shift_comp(32n, 20n, one)))
43  +f53 = WW.limbs_fit(52n, 1n, SW.value(fa), one, hF, L.subst(Nat, z => {C.fits(1n, z) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==}))
44  +f64 = SH.fits_mono(53n, 64n, Nat.add(SW.value(fa), C.shift(52n, one)), {==}, f53)
45  Equal.trans(Nat, SW.value(X.add(fa, WU.U64{0, c})), C.low(64n, Nat.add(SW.value(fa), C.shift(32n, v(c)))), Nat.add(SW.value(fa), C.shift(52n, one)), a1, Equal.trans(Nat, C.low(64n, Nat.add(SW.value(fa), C.shift(32n, v(c)))), C.low(64n, Nat.add(SW.value(fa), C.shift(52n, one))), Nat.add(SW.value(fa), C.shift(52n, one)), Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(SW.value(fa), z)), C.shift(32n, v(c)), C.shift(52n, one), ec), WW.low_fit(64n, Nat.add(SW.value(fa), C.shift(52n, one)), f64)))
46
47# ---- a subnormal fraction shifted up to bit 52 ----
48
49def clz_t(+fa: WU.U64, +Fr: Nat, +hfa: {SW.value(fa) == Fr : Nat}, +hb: {Nat.is_le(M.bit_length(Fr), 52n) == True{} : Bool}) -> {Nat.sub(X.clz(fa), 11n) == Nat.sub(53n, M.bit_length(Fr)) : Nat}:
50  +ec = Equal.trans(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(SW.value(fa))), Nat.sub(64n, M.bit_length(Fr)), CLZ.clz_value(fa), Equal.cong(Nat, Nat, z => Nat.sub(64n, M.bit_length(z)), SW.value(fa), Fr, hfa))
51  +hb53 = N.le_trans(M.bit_length(Fr), 52n, 53n, hb, {==})
52  +e1 = Equal.cong(Nat, Nat, z => Nat.sub(z, 11n), X.clz(fa), Nat.sub(64n, M.bit_length(Fr)), ec)
53  +e2 = Equal.cong(Nat, Nat, z => Nat.sub(z, 11n), Nat.sub(64n, M.bit_length(Fr)), Nat.add(11n, Nat.sub(53n, M.bit_length(Fr))), FR.sub_add_a(11n, 53n, M.bit_length(Fr), hb53))
54  Equal.trans(Nat, Nat.sub(X.clz(fa), 11n), Nat.sub(Nat.sub(64n, M.bit_length(Fr)), 11n), Nat.sub(53n, M.bit_length(Fr)), e1, Equal.trans(Nat, Nat.sub(Nat.sub(64n, M.bit_length(Fr)), 11n), Nat.sub(Nat.add(11n, Nat.sub(53n, M.bit_length(Fr))), 11n), Nat.sub(53n, M.bit_length(Fr)), e2, N.add_sub_cancel(11n, Nat.sub(53n, M.bit_length(Fr)))))
55
56def sub_fit(+fa: WU.U64, +Fr: Nat, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hz: {Nat.is_eq(Fr, 0n) == False{} : Bool}) -> {C.fits(53n, C.shift(Nat.sub(X.clz(fa), 11n), Fr)) == True{} : Bool}:
57  +hb = BL.bl_le(52n, Fr, hF, Nat.is_le(M.bit_length(Fr), 52n), {==})
58  +et = clz_t(fa, Fr, hfa, hb)
59  +k = Nat.sub(53n, M.bit_length(Fr))
60  +hb53 = N.le_trans(M.bit_length(Fr), 52n, 53n, hb, {==})
61  +ek = Equal.trans(Nat, Nat.add(k, M.bit_length(Fr)), Nat.add(M.bit_length(Fr), k), 53n, NA.add_comm(k, M.bit_length(Fr)), N.sub_add(53n, M.bit_length(Fr), hb53))
62  +hqu = L.subst(Nat, z => {Nat.is_lt(C.shift(k, Fr), z) == True{} : Bool}, C.shift(k, C.pow2(M.bit_length(Fr))), C.pow2(Nat.add(k, M.bit_length(Fr))), WW.shift_pow2(k, M.bit_length(Fr)), WW.shift_lt(k, Fr, C.pow2(M.bit_length(Fr)), BT.bit_length_lt(Fr)))
63  +f53 = L.subst(Nat, z => {C.fits(z, C.shift(k, Fr)) == True{} : Bool}, Nat.add(k, M.bit_length(Fr)), 53n, ek, WW.fits_of_lt(Nat.add(k, M.bit_length(Fr)), C.shift(k, Fr), hqu))
64  L.subst(Nat, z => {C.fits(53n, C.shift(z, Fr)) == True{} : Bool}, k, Nat.sub(X.clz(fa), 11n), Equal.sym(Nat, Nat.sub(X.clz(fa), 11n), k, et), f53)
65
66def sub_nfit(+fa: WU.U64, +Fr: Nat, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hz: {Nat.is_eq(Fr, 0n) == False{} : Bool}) -> {C.fits(52n, C.shift(Nat.sub(X.clz(fa), 11n), Fr)) == False{} : Bool}:
67  +hb = BL.bl_le(52n, Fr, hF, Nat.is_le(M.bit_length(Fr), 52n), {==})
68  +et = clz_t(fa, Fr, hfa, hb)
69  +k = Nat.sub(53n, M.bit_length(Fr))
70  +hb53 = N.le_trans(M.bit_length(Fr), 52n, 53n, hb, {==})
71  +ek = Equal.trans(Nat, Nat.add(k, M.bit_length(Fr)), Nat.add(M.bit_length(Fr), k), 53n, NA.add_comm(k, M.bit_length(Fr)), N.sub_add(53n, M.bit_length(Fr), hb53))
72  +pb = Nat.sub(M.bit_length(Fr), 1n)
73  +epb = N.sub_add(M.bit_length(Fr), 1n, BL.bl_pos(Fr, hz, M.bit_length(Fr), {==}))
74  +K2 = Nat.add(k, pb)
75  +e52 = N.succ_inj(K2, 52n, Equal.trans(Nat, 1n+K2, Nat.add(k, 1n+pb), 53n, Equal.sym(Nat, Nat.add(k, 1n+pb), 1n+K2, N.add_succ(k, pb)), Equal.trans(Nat, Nat.add(k, 1n+pb), Nat.add(k, M.bit_length(Fr)), 53n, Equal.cong(Nat, Nat, z => Nat.add(k, z), 1n+pb, M.bit_length(Fr), epb), ek)))
76  +hql = L.subst(Nat, z => {Nat.is_le(z, C.shift(k, Fr)) == True{} : Bool}, C.shift(k, C.pow2(pb)), C.pow2(K2), WW.shift_pow2(k, pb), WW.shift_mono(k, C.pow2(pb), Fr, BL.lower(Fr, hz)))
77  +nf = Equal.trans(Bool, C.fits(K2, C.pow2(K2)), Nat.is_lt(C.pow2(K2), C.pow2(K2)), False{}, WW.fits_lt(K2, C.pow2(K2)), N.lt_irrefl(C.pow2(K2)))
78  +f52 = L.subst(Nat, z => {C.fits(z, C.shift(k, Fr)) == False{} : Bool}, K2, 52n, e52, FR.nfit(K2, C.pow2(K2), C.shift(k, Fr), hql, nf))
79  L.subst(Nat, z => {C.fits(52n, C.shift(z, Fr)) == False{} : Bool}, k, Nat.sub(X.clz(fa), 11n), Equal.sym(Nat, Nat.sub(X.clz(fa), 11n), k, et), f52)
80
81def sub_val(+fa: WU.U64, +Fr: Nat, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hz: {Nat.is_eq(Fr, 0n) == False{} : Bool}) -> {SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))) == C.shift(Nat.sub(X.clz(fa), 11n), Fr) : Nat}:
82  +hb = BL.bl_le(52n, Fr, hF, Nat.is_le(M.bit_length(Fr), 52n), {==})
83  +et = clz_t(fa, Fr, hfa, hb)
84  +hk = N.le_lt_trans(Nat.sub(X.clz(fa), 11n), 53n, 64n, L.subst(Nat, z => {Nat.is_le(z, 53n) == True{} : Bool}, Nat.sub(53n, M.bit_length(Fr)), Nat.sub(X.clz(fa), 11n), Equal.sym(Nat, Nat.sub(X.clz(fa), 11n), Nat.sub(53n, M.bit_length(Fr)), et), UH.sub_le(53n, M.bit_length(Fr))), {==})
85  sv = SH.shl_value(fa, Nat.sub(X.clz(fa), 11n), hk)
86  Equal.trans(Nat, SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), C.low(64n, C.shift(Nat.sub(X.clz(fa), 11n), SW.value(fa))), C.shift(Nat.sub(X.clz(fa), 11n), Fr), sv, Equal.trans(Nat, C.low(64n, C.shift(Nat.sub(X.clz(fa), 11n), SW.value(fa))), C.low(64n, C.shift(Nat.sub(X.clz(fa), 11n), Fr)), C.shift(Nat.sub(X.clz(fa), 11n), Fr), Equal.cong(Nat, Nat, z => C.low(64n, C.shift(Nat.sub(X.clz(fa), 11n), z)), SW.value(fa), Fr, hfa), WW.low_fit(64n, C.shift(Nat.sub(X.clz(fa), 11n), Fr), SH.fits_mono(53n, 64n, C.shift(Nat.sub(X.clz(fa), 11n), Fr), {==}, sub_fit(fa, Fr, hfa, hF, hz)))))
87
88def sub_sum(+A: Nat, +t: Nat, +B: Nat, +hB: {Nat.is_le(B, t) == True{} : Bool}, +hA: {Nat.is_le(t, A) == True{} : Bool}) -> {Nat.add(Nat.sub(A, t), Nat.sub(t, B)) == Nat.sub(A, B) : Nat}:
89  +r = Nat.sub(t, B)
90  +q = Nat.sub(A, t)
91  +et = N.sub_add(t, B, hB)
92  +eA = N.sub_add(A, t, hA)
93  +e1 = Equal.trans(Nat, Nat.sub(A, B), Nat.sub(Nat.add(t, q), B), Nat.add(q, r), Equal.cong(Nat, Nat, z => Nat.sub(z, B), A, Nat.add(t, q), Equal.sym(Nat, Nat.add(t, q), A, eA)), Equal.trans(Nat, Nat.sub(Nat.add(t, q), B), Nat.sub(Nat.add(Nat.add(B, r), q), B), Nat.add(q, r), Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(z, q), B), t, Nat.add(B, r), Equal.sym(Nat, Nat.add(B, r), t, et)), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(B, r), q), B), Nat.sub(Nat.add(B, Nat.add(r, q)), B), Nat.add(q, r), Equal.cong(Nat, Nat, z => Nat.sub(z, B), Nat.add(Nat.add(B, r), q), Nat.add(B, Nat.add(r, q)), NA.add_assoc(B, r, q)), Equal.trans(Nat, Nat.sub(Nat.add(B, Nat.add(r, q)), B), Nat.add(r, q), Nat.add(q, r), N.add_sub_cancel(B, Nat.add(r, q)), NA.add_comm(r, q)))))
94  Equal.sym(Nat, Nat.sub(A, B), Nat.add(q, r), e1)
95
96def ez0(+E: Nat, +hea: {0n == E : Nat}) -> {Nat.is_eq(E, 0n) == True{} : Bool}:
97  Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), E, 0n, Equal.sym(Nat, 0n, E, hea))
98
99def ezs(+p: Nat, +E: Nat, +hea: {1n+p == E : Nat}) -> {Nat.is_eq(E, 0n) == False{} : Bool}:
100  Equal.sym(Bool, False{}, Nat.is_eq(E, 0n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), 1n+p, E, hea))
101
102# the normalized significand
103def n1(+one: Nat, +h1: {one == 1n : Nat}, +ea: Nat, +fa: WU.U64, +E: Nat, +Fr: Nat, +hea: {ea == E : Nat}, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hnz: {Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool}) -> {SW.value(F.norm_f(ea, fa)) == C.shift(sa(ea, fa), Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n)))))) : Nat}:
104  match ea:
105    case 0n:
106      +ez = ez0(E, hea)
107      +hz = L.subst(Bool, t => {Bool.and(t, Nat.is_eq(Fr, 0n)) == False{} : Bool}, Nat.is_eq(E, 0n), True{}, ez, hnz)
108      +em = Equal.trans(Nat, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Nat.add(Fr, 0n), Fr, Equal.cong(Bool, Nat, t => Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(t)))), Nat.is_eq(E, 0n), True{}, ez), N.add_zero(Fr))
109      Equal.trans(Nat, SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), C.shift(Nat.sub(X.clz(fa), 11n), Fr), C.shift(Nat.sub(X.clz(fa), 11n), Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n)))))), sub_val(fa, Fr, hfa, hF, hz), Equal.cong(Nat, Nat, z => C.shift(Nat.sub(X.clz(fa), 11n), z), Fr, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Equal.sym(Nat, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Fr, em)))
110    case 1n+ +p:
111      +ez = ezs(p, E, hea)
112      +ec = Equal.trans(Nat, SF.b2n(Bool.not(Nat.is_eq(E, 0n))), 1n, one, Equal.cong(Bool, Nat, t => SF.b2n(Bool.not(t)), Nat.is_eq(E, 0n), False{}, ez), Equal.sym(Nat, one, 1n, h1))
113      +em = Equal.cong(Nat, Nat, z => Nat.add(Fr, C.shift(52n, z)), SF.b2n(Bool.not(Nat.is_eq(E, 0n))), one, ec)
114      +hFv = L.subst(Nat, z => {C.fits(52n, z) == True{} : Bool}, Fr, SW.value(fa), Equal.sym(Nat, SW.value(fa), Fr, hfa), hF)
115      Equal.trans(Nat, SW.value(X.add(fa, WU.U64{0, 1048576})), Nat.add(SW.value(fa), C.shift(52n, one)), Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), hid(one, h1, fa, hFv, 1048576, {==}), Equal.trans(Nat, Nat.add(SW.value(fa), C.shift(52n, one)), Nat.add(Fr, C.shift(52n, one)), Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(52n, one)), SW.value(fa), Fr, hfa), Equal.sym(Nat, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Nat.add(Fr, C.shift(52n, one)), em)))
116
117# the exponent: norm_e + sa = xexp + 2171
118def n2(+ea: Nat, +fa: WU.U64, +E: Nat, +Fr: Nat, +hea: {ea == E : Nat}, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hnz: {Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool}) -> {Nat.add(F.norm_e(ea, fa), sa(ea, fa)) == Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n) : Nat}:
119  match ea:
120    case 0n:
121      +ez = ez0(E, hea)
122      +hz = L.subst(Bool, t => {Bool.and(t, Nat.is_eq(Fr, 0n)) == False{} : Bool}, Nat.is_eq(E, 0n), True{}, ez, hnz)
123      +hb = BL.bl_le(52n, Fr, hF, Nat.is_le(M.bit_length(Fr), 52n), {==})
124      +ec = Equal.trans(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(SW.value(fa))), Nat.sub(64n, M.bit_length(Fr)), CLZ.clz_value(fa), Equal.cong(Nat, Nat, z => Nat.sub(64n, M.bit_length(z)), SW.value(fa), Fr, hfa))
125      +h11 = L.subst(Nat, z => {Nat.is_le(11n, z) == True{} : Bool}, Nat.sub(64n, M.bit_length(Fr)), X.clz(fa), Equal.sym(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(Fr)), ec), RT.le_sub(11n, M.bit_length(Fr), 64n, N.le_add_left(M.bit_length(Fr), 53n, 11n, N.le_trans(M.bit_length(Fr), 52n, 53n, hb, {==}))))
126      +h4108 = L.subst(Nat, z => {Nat.is_le(z, 4108n) == True{} : Bool}, Nat.sub(64n, M.bit_length(Fr)), X.clz(fa), Equal.sym(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(Fr)), ec), N.le_trans(Nat.sub(64n, M.bit_length(Fr)), 64n, 4108n, UH.sub_le(64n, M.bit_length(Fr)), {==}))
127      +l1 = sub_sum(4108n, X.clz(fa), 11n, h11, h4108)
128      +r1 = Equal.cong(Bool, Nat, t => Nat.add(SF.pick(Nat, t, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), Nat.is_eq(E, 0n), True{}, ez)
129      Equal.trans(Nat, Nat.add(Nat.sub(4108n, X.clz(fa)), Nat.sub(X.clz(fa), 11n)), 4097n, Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), l1, Equal.sym(Nat, Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), 4097n, r1))
130    case 1n+ +p:
131      +ez = ezs(p, E, hea)
132      +r1 = Equal.cong(Bool, Nat, t => Nat.add(SF.pick(Nat, t, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), Nat.is_eq(E, 0n), False{}, ez)
133      +r2 = Equal.cong(Nat, Nat, z => Nat.add(z, 2171n), Nat.sub(Nat.add(E, SF.zb()), 1075n), Nat.add(1925n, E), FC.esub(E))
134      +r3 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(1925n, z), 2171n), E, 1n+p, Equal.sym(Nat, 1n+p, E, hea))
135      +r4 = Equal.cong(Nat, Nat, z => Nat.add(1926n, z), Nat.add(p, 2171n), Nat.add(2171n, p), NA.add_comm(p, 2171n))
136      +rr = Equal.trans(Nat, Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), Nat.add(Nat.sub(Nat.add(E, SF.zb()), 1075n), 2171n), Nat.add(4096n, 1n+p), r1, Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(E, SF.zb()), 1075n), 2171n), Nat.add(Nat.add(1925n, E), 2171n), Nat.add(4096n, 1n+p), r2, Equal.trans(Nat, Nat.add(Nat.add(1925n, E), 2171n), Nat.add(Nat.add(1925n, 1n+p), 2171n), Nat.add(4096n, 1n+p), r3, r4)))
137      Equal.trans(Nat, Nat.add(Nat.add(F.off(), 1n+p), 0n), Nat.add(4096n, 1n+p), Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), N.add_zero(Nat.add(F.off(), 1n+p)), Equal.sym(Nat, Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), Nat.add(4096n, 1n+p), rr))
138
139# the normalized significand has its top bit at 52
140def n3a(+one: Nat, +h1: {one == 1n : Nat}, +ea: Nat, +fa: WU.U64, +E: Nat, +Fr: Nat, +hea: {ea == E : Nat}, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hnz: {Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool}) -> {C.fits(53n, SW.value(F.norm_f(ea, fa))) == True{} : Bool}:
141  match ea:
142    case 0n:
143      +ez = ez0(E, hea)
144      +hz = L.subst(Bool, t => {Bool.and(t, Nat.is_eq(Fr, 0n)) == False{} : Bool}, Nat.is_eq(E, 0n), True{}, ez, hnz)
145      L.subst(Nat, z => {C.fits(53n, z) == True{} : Bool}, C.shift(Nat.sub(X.clz(fa), 11n), Fr), SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), Equal.sym(Nat, SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), C.shift(Nat.sub(X.clz(fa), 11n), Fr), sub_val(fa, Fr, hfa, hF, hz)), sub_fit(fa, Fr, hfa, hF, hz))
146    case 1n+ +p:
147      +hFv = L.subst(Nat, z => {C.fits(52n, z) == True{} : Bool}, Fr, SW.value(fa), Equal.sym(Nat, SW.value(fa), Fr, hfa), hF)
148      +f = WW.limbs_fit(52n, 1n, SW.value(fa), one, hFv, L.subst(Nat, z => {C.fits(1n, z) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==}))
149      L.subst(Nat, z => {C.fits(53n, z) == True{} : Bool}, Nat.add(SW.value(fa), C.shift(52n, one)), SW.value(X.add(fa, WU.U64{0, 1048576})), Equal.sym(Nat, SW.value(X.add(fa, WU.U64{0, 1048576})), Nat.add(SW.value(fa), C.shift(52n, one)), hid(one, h1, fa, hFv, 1048576, {==})), f)
150
151def n3b(+one: Nat, +h1: {one == 1n : Nat}, +ea: Nat, +fa: WU.U64, +E: Nat, +Fr: Nat, +hea: {ea == E : Nat}, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hnz: {Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool}) -> {C.fits(52n, SW.value(F.norm_f(ea, fa))) == False{} : Bool}:
152  match ea:
153    case 0n:
154      +ez = ez0(E, hea)
155      +hz = L.subst(Bool, t => {Bool.and(t, Nat.is_eq(Fr, 0n)) == False{} : Bool}, Nat.is_eq(E, 0n), True{}, ez, hnz)
156      L.subst(Nat, z => {C.fits(52n, z) == False{} : Bool}, C.shift(Nat.sub(X.clz(fa), 11n), Fr), SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), Equal.sym(Nat, SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), C.shift(Nat.sub(X.clz(fa), 11n), Fr), sub_val(fa, Fr, hfa, hF, hz)), sub_nfit(fa, Fr, hfa, hF, hz))
157    case 1n+ +p:
158      +hFv = L.subst(Nat, z => {C.fits(52n, z) == True{} : Bool}, Fr, SW.value(fa), Equal.sym(Nat, SW.value(fa), Fr, hfa), hF)
159      +nf = Equal.trans(Bool, C.fits(52n, C.shift(52n, one)), Nat.is_lt(C.shift(52n, one), C.shift(52n, one)), False{}, Equal.sym(Bool, Nat.is_lt(C.shift(52n, one), C.shift(52n, one)), C.fits(52n, C.shift(52n, one)), FR.lt_fit(52n, one, h1, C.shift(52n, one))), N.lt_irrefl(C.shift(52n, one)))
160      +hle = L.subst(Nat, z => {Nat.is_le(C.shift(52n, one), z) == True{} : Bool}, Nat.add(C.shift(52n, one), SW.value(fa)), Nat.add(SW.value(fa), C.shift(52n, one)), NA.add_comm(C.shift(52n, one), SW.value(fa)), N.le_add_right(C.shift(52n, one), SW.value(fa)))
161      L.subst(Nat, z => {C.fits(52n, z) == False{} : Bool}, Nat.add(SW.value(fa), C.shift(52n, one)), SW.value(X.add(fa, WU.U64{0, 1048576})), Equal.sym(Nat, SW.value(X.add(fa, WU.U64{0, 1048576})), Nat.add(SW.value(fa), C.shift(52n, one)), hid(one, h1, fa, hFv, 1048576, {==})), FR.nfit(52n, C.shift(52n, one), Nat.add(SW.value(fa), C.shift(52n, one)), hle, nf))