1 import Base 2 import ./f64light.bend as FL 3 import ../../../spec/lib/common.bend as C 4 import ../../../spec/math/f64.bend as SF 5 import ../../../spec/math/w64.bend as SW 6 import ../../../src/math/f64.bend as F 7 import ../../../src/math/w64.bend as X 8 import ../../../src/math/u64.bend as WU 9 import ../../lib/nat.bend as N 10 import ../../lib/logic.bend as L 11 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 12 import ../../lib/word.bend as WD 13 import ../natural/arith.bend as NR 14 import ./width.bend as WW 15 import ./w64add.bend as WA 16 import ./w64sh.bend as SH 17 import ./f64bits.bend as FB 18 import ./f64round.bend as FR 19 import ./f64rtools.bend as RT 20 21 # Pieces of SoftFloat's f64_mul and roundPackToF64 used by the arithmetic 22 # proofs: the sticky OR into bit 0, the one-bit renormalization of rp62, and 23 # exact products of 53-bit significands. 24 25 def v(+x: U32) -> Nat: 26 U32.to_nat(x) 27 28 # or_bit(a, b) is jam(a, b) 29 def orv_c(+l: U32, +h: U32, +b: Bool) -> {SW.value(X.or_bit(WU.U64{l, h}, b)) == SW.jam(SW.value(WU.U64{l, h}), SF.b2n(b)) : Nat}: 30 FL.orv_c(l, h, b) 31 32 def orv(+a: WU.U64, +b: Bool) -> {SW.value(X.or_bit(a, b)) == SW.jam(SW.value(a), SF.b2n(b)) : Nat}: 33 FL.orv(a, b) 34 35 def minz(+r: Nat) -> {Nat.min(r, 0n) == 0n : Nat}: 36 FL.minz(r) 37 38 # jam reads only whether r is zero 39 def jmin(+q: Nat, +r: Nat) -> {SW.jam(q, SF.b2n(Bool.not(Nat.is_eq(r, 0n)))) == SW.jam(q, r) : Nat}: 40 FL.jmin(q, r) 41 42 # ---- rp62: a significand in [2^61, 2^63) renormalized to bit 62 ---- 43 44 def lt62(+one: Nat, +h1: {one == 1n : Nat}, +sig: WU.U64, +c: U32, +hc: {c == U32{WD.pw(32n, 30n)} : U32}) -> {X.lt(sig, WU.U64{0, c}) == C.fits(62n, SW.value(sig)) : Bool}: 45 l1 = WA.lt_value(sig, WU.U64{0, c}) 46 +ec = Equal.trans(Nat, C.shift(32n, v(c)), C.shift(32n, C.shift(30n, one)), C.shift(62n, one), Equal.cong(Nat, Nat, z => C.shift(32n, z), v(c), C.shift(30n, one), FB.pwv(30n, {==}, one, h1, c, hc)), Equal.sym(Nat, C.shift(62n, one), C.shift(32n, C.shift(30n, one)), WW.shift_comp(32n, 30n, one))) 47 Equal.trans(Bool, X.lt(sig, WU.U64{0, c}), Nat.is_lt(SW.value(sig), C.shift(32n, v(c))), C.fits(62n, SW.value(sig)), l1, Equal.trans(Bool, Nat.is_lt(SW.value(sig), C.shift(32n, v(c))), Nat.is_lt(SW.value(sig), C.shift(62n, one)), C.fits(62n, SW.value(sig)), Equal.cong(Nat, Bool, z => Nat.is_lt(SW.value(sig), z), C.shift(32n, v(c)), C.shift(62n, one), ec), FR.lt_fit(62n, one, h1, SW.value(sig)))) 48 49 def rp62_c(+s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +hx1: {Nat.is_le(1n, x) == True{} : Bool}, +h61: {C.fits(61n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +f: Bool, +hf: {C.fits(62n, SW.value(sig)) == f : Bool}) -> {F.rp62_pick(s, e, sig, f) == SF.round(s, SW.value(sig), x) : F.F64}: 50 match f: 51 case True{}: 52 +Vs = SW.value(sig) 53 +d = X.add(sig, sig) 54 a1 = WA.add_value(sig, sig) 55 +f63 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, Nat.add(0n, C.shift(1n, Vs)), Nat.double(Vs), {==}, WW.limbs_fit(1n, 62n, 0n, Vs, FR.fz(1n), hf)) 56 +eVV = Equal.sym(Nat, Nat.double(Vs), Nat.add(Vs, Vs), NA.double_self(Vs)) 57 +ed = Equal.trans(Nat, SW.value(d), C.low(64n, Nat.add(Vs, Vs)), Nat.double(Vs), a1, Equal.trans(Nat, C.low(64n, Nat.add(Vs, Vs)), C.low(64n, Nat.double(Vs)), Nat.double(Vs), Equal.cong(Nat, Nat, z => C.low(64n, z), Nat.add(Vs, Vs), Nat.double(Vs), eVV), WW.low_fit(64n, Nat.double(Vs), SH.fits_mono(63n, 64n, Nat.double(Vs), {==}, f63)))) 58 +f62 = Equal.trans(Bool, C.fits(62n, Nat.double(Vs)), C.fits(61n, Vs), False{}, RT.fit_td(61n, 0n, Vs, {==}), h61) 59 +h62d = L.subst(Nat, z => {C.fits(62n, z) == False{} : Bool}, Nat.double(Vs), SW.value(d), Equal.sym(Nat, SW.value(d), Nat.double(Vs), ed), f62) 60 +h63d = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, Nat.double(Vs), SW.value(d), Equal.sym(Nat, SW.value(d), Nat.double(Vs), ed), f63) 61 +ex = Equal.trans(Nat, Nat.add(Nat.sub(x, 1n), 2180n), Nat.sub(Nat.add(x, 2180n), 1n), Nat.sub(e, 1n), Equal.sym(Nat, Nat.sub(Nat.add(x, 2180n), 1n), Nat.add(Nat.sub(x, 1n), 2180n), FR.sub_add_r(x, 2180n, 1n, hx1)), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), Nat.add(x, 2180n), e, hx)) 62 +r1 = FR.round_pack(s, Nat.sub(e, 1n), d, Nat.sub(x, 1n), ex, h62d, h63d) 63 +r2 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.sub(x, 1n)), SW.value(d), C.shift(1n, Vs), ed) 64 +r3 = RT.round_shift(s, 1n, Vs, Nat.sub(x, 1n)) 65 +r4 = Equal.cong(Nat, F.F64, z => SF.round(s, Vs, z), Nat.add(Nat.sub(x, 1n), 1n), x, Equal.trans(Nat, Nat.add(Nat.sub(x, 1n), 1n), Nat.add(1n, Nat.sub(x, 1n)), x, NA.add_comm(Nat.sub(x, 1n), 1n), N.sub_add(x, 1n, hx1))) 66 Equal.trans(F.F64, F.round_pack(s, Nat.sub(e, 1n), d), SF.round(s, SW.value(d), Nat.sub(x, 1n)), SF.round(s, Vs, x), r1, Equal.trans(F.F64, SF.round(s, SW.value(d), Nat.sub(x, 1n)), SF.round(s, C.shift(1n, Vs), Nat.sub(x, 1n)), SF.round(s, Vs, x), r2, Equal.trans(F.F64, SF.round(s, C.shift(1n, Vs), Nat.sub(x, 1n)), SF.round(s, Vs, Nat.add(Nat.sub(x, 1n), 1n)), SF.round(s, Vs, x), r3, r4))) 67 case False{}: 68 FR.round_pack(s, e, sig, x, hx, hf, h63) 69 70 def rp62_g(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +hx1: {Nat.is_le(1n, x) == True{} : Bool}, +h61: {C.fits(61n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +c: U32, +hc: {c == U32{WD.pw(32n, 30n)} : U32}) -> {F.rp62_pick(s, e, sig, X.lt(sig, WU.U64{0, c})) == SF.round(s, SW.value(sig), x) : F.F64}: 71 +el = lt62(one, h1, sig, c, hc) 72 Equal.trans(F.F64, F.rp62_pick(s, e, sig, X.lt(sig, WU.U64{0, c})), F.rp62_pick(s, e, sig, C.fits(62n, SW.value(sig))), SF.round(s, SW.value(sig), x), Equal.cong(Bool, F.F64, t => F.rp62_pick(s, e, sig, t), X.lt(sig, WU.U64{0, c}), C.fits(62n, SW.value(sig)), el), rp62_c(s, e, sig, x, hx, hx1, h61, h63, C.fits(62n, SW.value(sig)), {==})) 73 74 # SoftFloat's rp62(s, e, sig) for sig in [2^61, 2^63) is round(s, sig, e - 2180) 75 def rp62(+s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +hx1: {Nat.is_le(1n, x) == True{} : Bool}, +h61: {C.fits(61n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}) -> {F.rp62(s, e, sig) == SF.round(s, SW.value(sig), x) : F.F64}: 76 rp62_g(1n, {==}, s, e, sig, x, hx, hx1, h61, h63, 1073741824, {==})