1 import Base 2 import ../../../spec/math/f64.bend as SF 3 import ../../../spec/math/w64.bend as SW 4 import ../../../src/math/f64.bend as F 5 import ../../../src/math/w64.bend as X 6 import ../../../src/math/u64.bend as WU 7 import ../../../src/math/natural.bend as M 8 import ../../lib/nat.bend as N 9 import ../../lib/logic.bend as L 10 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 11 import ./w64mul.bend as W64M 12 import ./natfuel.bend as NF 13 import ./u32laws.bend as LW 14 import ./w64clz.bend as CLZ 15 import ../../lib/u32half.bend as UH 16 import ../../lib/u32alg.bend as A 17 import ./f64cmp.bend as FC 18 import ./f64round.bend as FR 19 import ./f64rtools.bend as RT 20 import ./f64norm.bend as NM 21 22 # Mul.value of spec/math/f64.bend: SoftFloat's f64_mul multiplies the two 23 # normalized 53-bit significands (shifted by 10 and 11) into 128 bits, jams 24 # the low half into bit 0 and rounds with rp62; the spec rounds the exact 25 # product of the significands. round_jam and round_shift bridge the two. 26 27 28 # ---- exponent bookkeeping ---- 29 30 def sa_le(+ea: Nat, +fa: WU.U64) -> {Nat.is_le(NM.sa(ea, fa), 53n) == True{} : Bool}: 31 match ea: 32 case 0n: 33 +hc = L.subst(Nat, z => {Nat.is_le(z, 64n) == True{} : Bool}, Nat.sub(64n, M.bit_length(SW.value(fa))), X.clz(fa), Equal.sym(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(SW.value(fa))), CLZ.clz_value(fa)), UH.sub_le(64n, M.bit_length(SW.value(fa)))) 34 NF.sub_mono_l(X.clz(fa), 64n, 11n, hc) 35 case 1n+ +p: 36 {==} 37 38 def e_ge1(+E: Nat, +h: {Nat.is_eq(E, 0n) == False{} : Bool}) -> {Nat.is_le(1926n, Nat.add(1925n, E)) == True{} : Bool}: 39 match E: 40 case 0n: 41 Empty.absurd({Nat.is_le(1926n, Nat.add(1925n, 0n)) == True{} : Bool}, LW.true_ne_false(h)) 42 case 1n+ +p: 43 N.zero_le(p) 44 45 def xg_c(+E: Nat, +c: Bool, +hc: {Nat.is_eq(E, 0n) == c : Bool}) -> {Nat.is_le(1926n, SF.pick(Nat, c, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n))) == True{} : Bool}: 46 match c: 47 case True{}: 48 {==} 49 case False{}: 50 L.subst(Nat, z => {Nat.is_le(1926n, z) == True{} : Bool}, Nat.add(1925n, E), Nat.sub(Nat.add(E, SF.zb()), 1075n), Equal.sym(Nat, Nat.sub(Nat.add(E, SF.zb()), 1075n), Nat.add(1925n, E), FC.esub(E)), e_ge1(E, hc)) 51 52 def xexp_ge(+E: Nat) -> {Nat.is_le(1926n, SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n))) == True{} : Bool}: 53 xg_c(E, Nat.is_eq(E, 0n), {==}) 54 55 def eg(+ea: Nat, +sa: Nat, +Xx: Nat, +n2: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +hs: {Nat.is_le(sa, 53n) == True{} : Bool}, +hX: {Nat.is_le(1926n, Xx) == True{} : Bool}) -> {Nat.is_le(4044n, ea) == True{} : Bool}: 56 +h1 = L.subst(Nat, z => {Nat.is_le(4097n, z) == True{} : Bool}, Nat.add(Xx, 2171n), Nat.add(ea, sa), Equal.sym(Nat, Nat.add(ea, sa), Nat.add(Xx, 2171n), n2), Equal.trans(Bool, Nat.is_le(Nat.add(1926n, 2171n), Nat.add(Xx, 2171n)), Nat.is_le(1926n, Xx), True{}, FR.le_cancel_r(1926n, Xx, 2171n), hX)) 57 +h2 = N.le_trans(4097n, Nat.add(ea, sa), Nat.add(ea, 53n), h1, N.le_add_left(sa, 53n, ea, hs)) 58 Equal.trans(Bool, Nat.is_le(4044n, ea), Nat.is_le(Nat.add(4044n, 53n), Nat.add(ea, 53n)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(4044n, 53n), Nat.add(ea, 53n)), Nat.is_le(4044n, ea), FR.le_cancel_r(4044n, ea, 53n)), h2) 59 60 def s_ge(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.is_le(8088n, Nat.add(ea, eb)) == True{} : Bool}: 61 +ha = eg(ea, sa, Xx, n2x, hsa, hXx) 62 +hb = eg(eb, sb, Xy, n2y, hsb, hXy) 63 N.le_trans(8088n, Nat.add(4044n, eb), Nat.add(ea, eb), N.le_add_left(4044n, eb, 4044n, hb), Equal.trans(Bool, Nat.is_le(Nat.add(4044n, eb), Nat.add(ea, eb)), Nat.is_le(4044n, ea), True{}, FR.le_cancel_r(4044n, ea, eb), ha)) 64 65 def e0_ge(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.is_le(2244n, Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n))) == True{} : Bool}: 66 RT.le_sub(2244n, 5119n, Nat.add(ea, eb), N.le_trans(Nat.add(2244n, 5119n), 8088n, Nat.add(ea, eb), {==}, s_ge(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy))) 67 68 def x_eq(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n) == Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)) : Nat}: 69 +h = N.le_trans(2180n, 2244n, Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), {==}, e0_ge(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy)) 70 Equal.trans(Nat, Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n)), Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), NA.add_comm(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), N.sub_add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n, h)) 71 72 def x_ge(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.is_le(64n, Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n)) == True{} : Bool}: 73 RT.le_sub(64n, 2180n, Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), e0_ge(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy)) 74 75 def x0_eq(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n) == Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n) : Nat}: 76 Equal.trans(Nat, Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), Nat.add(64n, Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n)), Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), NA.add_comm(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), N.sub_add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n, x_ge(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy))) 77 78 # x0 + 21 + sa + sb is the spec's product exponent 79 def mexp(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(sa, sb)) == Nat.sub(Nat.add(Xx, Xy), SF.zb()) : Nat}: 80 +ex0 = x0_eq(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy) 81 +exx = x_eq(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy) 82 +eS0 = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), Nat.add(5119n, Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n))), Nat.add(ea, eb), NA.add_comm(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), N.sub_add(Nat.add(ea, eb), 5119n, N.le_trans(5119n, 8088n, Nat.add(ea, eb), {==}, s_ge(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy)))) 83 +eS = Equal.trans(Nat, Nat.add(ea, eb), Nat.add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), Nat.add(ea, eb), eS0), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), 5119n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), Equal.cong(Nat, Nat, z => Nat.add(z, 5119n), Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), exx)), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), 5119n), Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), 2180n), 5119n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(z, 2180n), 5119n), Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), ex0)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), 2180n), 5119n), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), 7299n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n) 84 +e1 = Equal.trans(Nat, Nat.add(Nat.add(ea, sa), Nat.add(eb, sb)), Nat.add(Nat.add(Xx, 2171n), Nat.add(eb, sb)), Nat.add(Nat.add(Xx, 2171n), Nat.add(Xy, 2171n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(eb, sb)), Nat.add(ea, sa), Nat.add(Xx, 2171n), n2x), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Xx, 2171n), z), Nat.add(eb, sb), Nat.add(Xy, 2171n), n2y)) 85 +e2 = W64M.add4(ea, sa, eb, sb) 86 +e3 = W64M.add4(Xx, 2171n, Xy, 2171n) 87 +T2 = Nat.add(sa, sb) 88 +W = Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), T2) 89 +e4 = Equal.trans(Nat, Nat.add(Nat.add(W, 3000n), 4342n), Nat.add(W, 7342n), Nat.add(Nat.add(Xx, Xy), 4342n), NA.add_assoc(W, 3000n, 4342n), Equal.trans(Nat, Nat.add(W, 7342n), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(T2, 7342n)), Nat.add(Nat.add(Xx, Xy), 4342n), NA.add_assoc(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), T2, 7342n), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(T2, 7342n)), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(7342n, T2)), Nat.add(Nat.add(Xx, Xy), 4342n), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), z), Nat.add(T2, 7342n), Nat.add(7342n, T2), NA.add_comm(T2, 7342n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(7342n, T2)), Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n), T2), Nat.add(Nat.add(Xx, Xy), 4342n), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n), T2), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(7342n, T2)), NA.add_assoc(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n, T2)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n), T2), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), T2), Nat.add(Nat.add(Xx, Xy), 4342n), Equal.cong(Nat, Nat, z => Nat.add(z, T2), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub( 90 +e5 = A.add_cancel_r(Nat.add(W, 3000n), Nat.add(Xx, Xy), 4342n, e4) 91 Equal.sym(Nat, Nat.sub(Nat.add(Xx, Xy), SF.zb()), W, Equal.trans(Nat, Nat.sub(Nat.add(Xx, Xy), 3000n), Nat.sub(Nat.add(W, 3000n), 3000n), W, Equal.cong(Nat, Nat, z => Nat.sub(z, 3000n), Nat.add(Xx, Xy), Nat.add(W, 3000n), Equal.sym(Nat, Nat.add(W, 3000n), Nat.add(Xx, Xy), e5)), FR.sub_add_l(W, 3000n)))