1 import Base 2 import ../../lib/nat.bend as N 3 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 4 import ../natural/arith.bend as NR 5 6 # Exponent bookkeeping for Sqrt.value: with the spec exponent made even 7 # (XX = 2q + cs) and the implementation's made odd (EN = Ep + ci, 8 # 2p + 1075 = Ep + 4096), the root's rounding cut j (2j + 72 + sa + ci = 9 # 200 + cs) lines the spec's ulp up with roundPackToF64's. 10 11 def sqexp(+q: Nat, +p: Nat, +j: Nat, +x: Nat, +XX: Nat, +EN: Nat, +Ep: Nat, +sa: Nat, +ci: Nat, +cs: Nat, +hq: {Nat.add(Nat.add(q, q), cs) == XX : Nat}, +hp: {Nat.add(Nat.add(p, p), 1075n) == Nat.add(Ep, 4096n) : Nat}, +hE: {Nat.add(Ep, ci) == EN : Nat}, +hEN: {Nat.add(EN, sa) == Nat.add(XX, 2171n) : Nat}, +hj: {Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))) == Nat.add(200n, cs) : Nat}, +hx: {Nat.add(x, 2180n) == Nat.add(p, 1048n) : Nat}) -> {Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)) == x : Nat}: 12 +A = Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(XX, Nat.add(Nat.add(200n, cs), 2800n)), Nat.add(cs, Nat.add(XX, 3000n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(XX, Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Nat.add(XX, Nat.add(Nat.add(200n, cs), 2800n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(Nat.add(Nat.add(q, q), cs), Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Nat.add(XX, Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(Nat.add(Nat.add(q, q), cs), Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, 13 +A2 = NR.add_cancel(cs, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(XX, 3000n), Equal.trans(Nat, Nat.add(cs, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(cs, Nat.add(XX, 3000n)), Equal.trans(Nat, Nat.add(cs, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Equal.trans(Nat, Nat.add(cs, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(cs, 0n), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(cs, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(cs, 0n), Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(cs, 0n), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n)))), cs, Nat.add(cs, 0n), Equal.sym(Nat, Nat.add(cs, 0n), cs, N.add_zero(cs))), E 14 +B = Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(XX, 2171n), 6192n), Nat.add(5363n, Nat.add(XX, 3000n)), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(EN, sa), 6192n), Nat.add(Nat.add(XX, 2171n), 6192n), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(Nat.add(Ep, ci), sa), 6192n), Nat.add(Nat.add(EN, sa), 6192n), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(Nat.add(Ep, 4096n), Nat.add(ci, sa)), 2096n), Nat.add(Nat.add(Nat.add(Ep, ci), sa), 6192n), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(Nat.add(Nat.add(p, p), 1075n), Nat.add(ci, sa)), 2096n), Nat.add(Nat.add(Nat.add(Ep, 4096n), Nat.add(ci, sa)), 2096n), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Nat.add(1075n, Nat.add(ci, sa))), Nat.add(Nat.add(Nat.add(Nat.add(p, p), 1075n), Nat.add(ci, sa)), 2096n), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Nat.add(1075n, Nat.add(ci, sa))), Nat.add(Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Nat.add(1075n, Nat.add(ci, sa))), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 5435n)))), Nat.add(Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Nat.add(1075n, Nat.add(ci, sa))), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(5363n, Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n))))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 5435n)))), Equal.cong(Nat, Nat, z => Nat.add(5363n, z), Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(ci, Nat.add(sa, 15 +B2 = NR.add_cancel(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(XX, 3000n), B) 16 +C1 = NR.add_cancel(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(x, x), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)))), Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(x, x)), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n))), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)))), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)))), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)))), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)))), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add( 17 N.double_inj(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), x, Equal.trans(Nat, Nat.double(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.double(x), NA.double_self(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(x, x), Nat.double(x), C1, Equal.sym(Nat, Nat.double(x), Nat.add(x, x), NA.double_self(x)))))