~/jendhub

def amen

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addc.bend:116

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend as F64addc
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/nat.bend as N
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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
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/w64sh.bend as SH
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

116# addMags, equal normal exponents e: the 54-bit sum at bit 62
117def amen(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +fa: WU.U64, +fb: WU.U64, +Fa: Nat, +Fb: Nat, +hfa: {SW.value(fa) == Fa : Nat}, +hfb: {SW.value(fb) == Fb : Nat}, +hFa: {C.fits(52n, Fa) == True{} : Bool}, +hFb: {C.fits(52n, Fb) == True{} : Bool}, +c: U32, +hc: {c == U32{WD.pw(32n, 21n)} : U32}) -> {F.round_pack(s, Nat.add(F.off(), e), X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)) == SF.round(s, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(1925n, e)) : F.F64}:
118  +eW = Equal.trans(Nat, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), Nat.add(Nat.add(C.shift(52n, one), C.shift(52n, one)), Nat.add(Fa, Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Fa, Fb)), Nat.double(C.shift(52n, one)), Nat.add(C.shift(52n, one), C.shift(52n, one)), NA.double_self(C.shift(52n, one))), Equal.trans(Nat, Nat.add(Nat.add(C.shift(52n, one), C.shift(52n, one)), Nat.add(Fa, Fb)), Nat.add(Nat.add(C.shift(52n, one), Fa), Nat.add(C.shift(52n, one), Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), swap4(C.shift(52n, one), C.shift(52n, one), Fa, Fb), Equal.trans(Nat, Nat.add(Nat.add(C.shift(52n, one), Fa), Nat.add(C.shift(52n, one), Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(C.shift(52n, one), Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(C.shift(52n, one), Fb)), Nat.add(C.shift(52n, one), Fa), Nat.add(Fa, C.shift(52n, one)), NA.add_comm(C.shift(52n, one), Fa)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Fa, C.shift(52n, one)), z), Nat.add(C.shift(52n, one), Fb), Nat.add(Fb, C.shift(52n, one)), NA.add_comm(C.shift(52n, one), Fb)))))
119  +fW = FR.fits_add1(53n, Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)), f53(one, h1, Fa, hFa), f53(one, h1, Fb, hFb))
120  +fV = L.subst(Nat, z => {C.fits(54n, z) == True{} : Bool}, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), Equal.sym(Nat, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), eW), fW)
121  +eA = Equal.trans(Nat, SW.value(X.add(WU.U64{0, c}, X.add(fa, fb))), C.low(64n, Nat.add(SW.value(WU.U64{0, c}), SW.value(X.add(fa, fb)))), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), WA.add_value(WU.U64{0, c}, X.add(fa, fb)), Equal.trans(Nat, C.low(64n, Nat.add(SW.value(WU.U64{0, c}), SW.value(X.add(fa, fb)))), C.low(64n, Nat.add(C.shift(53n, one), SW.value(X.add(fa, fb)))), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(z, SW.value(X.add(fa, fb)))), SW.value(WU.U64{0, c}), C.shift(53n, one), c53(one, h1, c, hc)), Equal.trans(Nat, C.low(64n, Nat.add(C.shift(53n, one), SW.value(X.add(fa, fb)))), C.low(64n, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb))), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(C.shift(53n, one), z)), SW.value(X.add(fa, fb)), Nat.add(Fa, Fb), addv2(fa, fb, Fa, Fb, hfa, hfb, hFa, hFb)), Equal.trans(Nat, C.low(64n, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb))), Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), WW.low_fit(64n, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), SH.fits_mono(54n, 64n, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), {==}, fV)), eW))))
122  +fA = L.subst(Nat, z => {C.fits(54n, z) == True{} : Bool}, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), SW.value(X.add(WU.U64{0, c}, X.add(fa, fb))), Equal.sym(Nat, SW.value(X.add(WU.U64{0, c}, X.add(fa, fb))), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), eA), fW)
123  +eS = Equal.trans(Nat, SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), C.shift(9n, SW.value(X.add(WU.U64{0, c}, X.add(fa, fb)))), C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), shl_v(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n, 54n, {==}, {==}, fA), Equal.cong(Nat, Nat, z => C.shift(9n, z), SW.value(X.add(WU.U64{0, c}, X.add(fa, fb))), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), eA))
124  +f63 = Equal.trans(Bool, C.fits(63n, C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))))), C.fits(54n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), True{}, RT.fits_sh(9n, 54n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), fW)
125  +h63 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), Equal.sym(Nat, SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), eS), f63)
126  +f0 = Equal.trans(Bool, C.fits(53n, C.shift(53n, one)), Nat.is_lt(C.shift(53n, one), C.shift(53n, one)), False{}, Equal.sym(Bool, Nat.is_lt(C.shift(53n, one), C.shift(53n, one)), C.fits(53n, C.shift(53n, one)), FR.lt_fit(53n, one, h1, C.shift(53n, one))), N.lt_irrefl(C.shift(53n, one)))
127  +hle = L.subst(Nat, z => {Nat.is_le(C.shift(53n, one), z) == True{} : Bool}, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), eW, N.le_add_right(C.shift(53n, one), Nat.add(Fa, Fb)))
128  +f62 = Equal.trans(Bool, C.fits(62n, C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))))), C.fits(53n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), False{}, RT.fits_sh(9n, 53n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), FR.nfit(53n, C.shift(53n, one), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), hle, f0))
129  +h62 = L.subst(Nat, z => {C.fits(62n, z) == False{} : Bool}, C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), Equal.sym(Nat, SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), eS), f62)
130  +hx = Equal.trans(Nat, Nat.add(Nat.add(e, 1916n), 2180n), Nat.add(e, 4096n), Nat.add(4096n, e), NA.add_assoc(e, 1916n, 2180n), NA.add_comm(e, 4096n))
131  +r1 = FR.round_pack(s, Nat.add(F.off(), e), X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n), Nat.add(e, 1916n), hx, h62, h63)
132  +r2 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.add(e, 1916n)), SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), eS)
133  +r3 = RT.round_shift(s, 9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(e, 1916n))
134  +ex = Equal.trans(Nat, Nat.add(Nat.add(e, 1916n), 9n), Nat.add(e, 1925n), Nat.add(1925n, e), NA.add_assoc(e, 1916n, 9n), NA.add_comm(e, 1925n))
135  +r4 = Equal.cong(Nat, F.F64, z => SF.round(s, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), z), Nat.add(Nat.add(e, 1916n), 9n), Nat.add(1925n, e), ex)
136  Equal.trans(F.F64, F.round_pack(s, Nat.add(F.off(), e), X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), SF.round(s, SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), Nat.add(e, 1916n)), SF.round(s, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(1925n, e)), r1, Equal.trans(F.F64, SF.round(s, SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), Nat.add(e, 1916n)), SF.round(s, C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), Nat.add(e, 1916n)), SF.round(s, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(1925n, e)), r2, Equal.trans(F.F64, SF.round(s, C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), Nat.add(e, 1916n)), SF.round(s, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(Nat.add(e, 1916n), 9n)), SF.round(s, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(1925n, e)), r3, r4)))

Uses (42)

Used by (1)