F64mul.mc2: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mul.bend as F64mul Lines 47-65 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mul.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mul.bend&start_line=47&end_line=65 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/f64.bend as SF import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F 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/proofs/lib/logic.bend as L 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/w64add.bend as WA import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend as M128 import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulp.bend as MP # the 128-bit product jammed to 64 bits and rounded by rp62 def mc2(+s: Bool, +e: Nat, +pl: WU.U64, +ph: WU.U64, +P: Nat, +hp: {Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))) == P : Nat}, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +hx1: {Nat.is_le(1n, x) == True{} : Bool}, +h127: {C.fits(127n, P) == True{} : Bool}, +h125: {C.fits(125n, P) == False{} : Bool}) -> {F.rp62(s, e, X.or_bit(ph, F.nz(pl))) == SF.round(s, SW.jam(C.high(64n, P), C.low(64n, P)), x) : F.F64}: +fl = M128.fit64(pl) +eh = Equal.trans(Nat, C.high(64n, P), C.high(64n, Nat.add(SW.value(pl), C.shift(64n, SW.value(ph)))), SW.value(ph), Equal.cong(Nat, Nat, z => C.high(64n, z), P, Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), Equal.sym(Nat, Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), P, hp)), WW.high_u(64n, SW.value(pl), SW.value(ph), fl)) +el = Equal.trans(Nat, C.low(64n, P), C.low(64n, Nat.add(SW.value(pl), C.shift(64n, SW.value(ph)))), SW.value(pl), Equal.cong(Nat, Nat, z => C.low(64n, z), P, Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), Equal.sym(Nat, Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), P, hp)), WW.low_u(64n, SW.value(pl), SW.value(ph), fl)) +ez = Equal.cong(Bool, Nat, t => SF.b2n(Bool.not(t)), X.is_zero(pl), Nat.is_eq(SW.value(pl), 0n), WA.is_zero_value(pl)) +ev = Equal.trans(Nat, SW.value(X.or_bit(ph, F.nz(pl))), SW.jam(SW.value(ph), SF.b2n(F.nz(pl))), SW.jam(C.high(64n, P), C.low(64n, P)), MP.orv(ph, F.nz(pl)), Equal.trans(Nat, SW.jam(SW.value(ph), SF.b2n(F.nz(pl))), SW.jam(SW.value(ph), SF.b2n(Bool.not(Nat.is_eq(SW.value(pl), 0n)))), SW.jam(C.high(64n, P), C.low(64n, P)), Equal.cong(Nat, Nat, z => SW.jam(SW.value(ph), z), SF.b2n(F.nz(pl)), SF.b2n(Bool.not(Nat.is_eq(SW.value(pl), 0n))), ez), Equal.trans(Nat, SW.jam(SW.value(ph), SF.b2n(Bool.not(Nat.is_eq(SW.value(pl), 0n)))), SW.jam(SW.value(ph), SW.value(pl)), SW.jam(C.high(64n, P), C.low(64n, P)), MP.jmin(SW.value(ph), SW.value(pl)), Equal.trans(Nat, SW.jam(SW.value(ph), SW.value(pl)), SW.jam(C.high(64n, P), SW.value(pl)), SW.jam(C.high(64n, P), C.low(64n, P)), Equal.cong(Nat, Nat, z => SW.jam(z, SW.value(pl)), SW.value(ph), C.high(64n, P), Equal.sym(Nat, C.high(64n, P), SW.value(ph), eh)), Equal.cong(Nat, Nat, z => SW.jam(C.high(64n, P), z), SW.value(pl), C.low(64n, P), Equal.sym(Nat, C.low(64n, P), SW.value(pl), el)))))) +f63h = Equal.trans(Bool, C.fits(63n, C.high(64n, P)), C.fits(Nat.add(64n, 63n), P), True{}, Equal.sym(Bool, C.fits(Nat.add(64n, 63n), P), C.fits(63n, C.high(64n, P)), FR.fits_hc(64n, 63n, P)), h127) +f61h = Equal.trans(Bool, C.fits(61n, C.high(64n, P)), C.fits(Nat.add(64n, 61n), P), False{}, Equal.sym(Bool, C.fits(Nat.add(64n, 61n), P), C.fits(61n, C.high(64n, P)), FR.fits_hc(64n, 61n, P)), h125) +fJ63 = Equal.trans(Bool, C.fits(63n, SW.jam(C.high(64n, P), C.low(64n, P))), C.fits(63n, C.high(64n, P)), True{}, RT.jam_fits(62n, C.high(64n, P), C.low(64n, P)), f63h) +t = Nat.max(C.bit(C.high(64n, P)), Nat.min(C.low(64n, P), 1n)) +ejf = FR.jam_form(C.high(64n, P), C.low(64n, P)) +hhb = WW.le_add_r(C.bit(C.high(64n, P)), t, Nat.double(C.half(C.high(64n, P))), RT.max_ge_l(C.bit(C.high(64n, P)), Nat.min(C.low(64n, P), 1n))) +hhJ = L.subst(Nat, z => {Nat.is_le(z, SW.jam(C.high(64n, P), C.low(64n, P))) == True{} : Bool}, Nat.add(C.bit(C.high(64n, P)), Nat.double(C.half(C.high(64n, P)))), C.high(64n, P), Equal.sym(Nat, C.high(64n, P), Nat.add(C.bit(C.high(64n, P)), Nat.double(C.half(C.high(64n, P)))), WW.hb(C.high(64n, P))), L.subst(Nat, z => {Nat.is_le(Nat.add(C.bit(C.high(64n, P)), Nat.double(C.half(C.high(64n, P)))), z) == True{} : Bool}, Nat.add(t, Nat.double(C.half(C.high(64n, P)))), SW.jam(C.high(64n, P), C.low(64n, P)), Equal.sym(Nat, SW.jam(C.high(64n, P), C.low(64n, P)), Nat.add(t, Nat.double(C.half(C.high(64n, P)))), ejf), hhb)) +fJ61 = FR.nfit(61n, C.high(64n, P), SW.jam(C.high(64n, P), C.low(64n, P)), hhJ, f61h) +sig = X.or_bit(ph, F.nz(pl)) +h61 = L.subst(Nat, z => {C.fits(61n, z) == False{} : Bool}, SW.jam(C.high(64n, P), C.low(64n, P)), SW.value(sig), Equal.sym(Nat, SW.value(sig), SW.jam(C.high(64n, P), C.low(64n, P)), ev), fJ61) +h63 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, SW.jam(C.high(64n, P), C.low(64n, P)), SW.value(sig), Equal.sym(Nat, SW.value(sig), SW.jam(C.high(64n, P), C.low(64n, P)), ev), fJ63) Equal.trans(F.F64, F.rp62(s, e, sig), SF.round(s, SW.value(sig), x), SF.round(s, SW.jam(C.high(64n, P), C.low(64n, P)), x), MP.rp62(s, e, sig, x, hx, hx1, h61, h63), Equal.cong(Nat, F.F64, z => SF.round(s, z, x), SW.value(sig), SW.jam(C.high(64n, P), C.low(64n, P)), ev)) Uses (43): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not 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.double https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.max https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.min https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulp.bend&name=jmin https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulp.bend&name=orv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulp.bend&name=rp62 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=fits_hc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=jam_form https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=nfit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend&name=jam_fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend&name=max_ge_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=is_zero_value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend&name=fit64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=hb 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=le_add_r 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=bit 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=half 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=round https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=jam 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/f64.bend&name=nz https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=rp62 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=is_zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=or_bit