import Base
import ./f64light.bend as FL
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../spec/math/w64.bend as SW
import ../../../src/math/f64.bend as F
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ./width.bend as WW
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64sqa.bend as AQ

# The spec's root 2 * isqrt(N * 4^j) + [inexact], cut at bit 1 + j, is
# SoftFloat's floor(sqrt(N)) with its sticky bit (Flocq's sqrt with a
# sticky remainder bit, round_NE once).

def hb2n(+c: Bool) -> {C.half(SF.b2n(c)) == 0n : Nat}:
  match c:
    case True{}:
      {==}
    case False{}:
      {==}

def bb2n(+c: Bool) -> {C.bit(SF.b2n(c)) == SF.b2n(c) : Nat}:
  match c:
    case True{}:
      {==}
    case False{}:
      {==}

def eb2n(+c: Bool) -> {Nat.is_eq(SF.b2n(Bool.not(c)), 0n) == c : Bool}:
  match c:
    case True{}:
      {==}
    case False{}:
      {==}

def mform(+n: Nat, +j: Nat) -> {Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))) == Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))) : Nat}:
  Equal.trans(Nat, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), Equal.cong(Nat, Nat, z => Nat.add(z, SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), Equal.sym(Nat, Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), NA.double_mul(M.isqrt(C.shift(j, C.shift(j, n)))))), NA.add_comm(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))

def s_high(+n: Nat, +j: Nat) -> {C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))) == M.isqrt(n) : Nat}:
  +e1 = Equal.cong(Nat, Nat, z => C.high(1n+j, z), Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), mform(n, j))
  +e2 = Equal.cong(Nat, Nat, z => C.high(j, z), C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), M.isqrt(C.shift(j, C.shift(j, n))), Equal.trans(Nat, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), Nat.add(C.half(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), M.isqrt(C.shift(j, C.shift(j, n)))), M.isqrt(C.shift(j, C.shift(j, n))), WW.half_dbl(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), M.isqrt(C.shift(j, C.shift(j, n)))), Equal.cong(Nat, Nat, z => Nat.add(z, M.isqrt(C.shift(j, C.shift(j, n)))), C.half(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), 0n, hb2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))))
  Equal.trans(Nat, C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), C.high(j, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))))), M.isqrt(n), Equal.trans(Nat, C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), C.high(1n+j, Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), C.high(j, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))))), e1, {==}), Equal.trans(Nat, C.high(j, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))))), C.high(j, M.isqrt(C.shift(j, C.shift(j, n)))), M.isqrt(n), e2, AQ.sc_high(n, j)))

def s_low(+n: Nat, +j: Nat) -> {C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))) == Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))) : Nat}:
  +e1 = Equal.cong(Nat, Nat, z => C.low(1n+j, z), Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), mform(n, j))
  +eh = Equal.trans(Nat, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), Nat.add(C.half(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), M.isqrt(C.shift(j, C.shift(j, n)))), M.isqrt(C.shift(j, C.shift(j, n))), WW.half_dbl(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), M.isqrt(C.shift(j, C.shift(j, n)))), Equal.cong(Nat, Nat, z => Nat.add(z, M.isqrt(C.shift(j, C.shift(j, n)))), C.half(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), 0n, hb2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))
  +eb = Equal.trans(Nat, C.bit(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), C.bit(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), WW.bit_dbl(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), M.isqrt(C.shift(j, C.shift(j, n)))), bb2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))
  +e2 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.double(C.low(j, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))))))), C.bit(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), eb)
  +e3 = Equal.cong(Nat, Nat, z => Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(C.low(j, z))), C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), M.isqrt(C.shift(j, C.shift(j, n))), eh)
  +e4 = Equal.cong(Nat, Nat, z => Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(z)), C.low(j, M.isqrt(C.shift(j, C.shift(j, n)))), Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), AQ.sc_low(n, j))
  Equal.trans(Nat, C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), C.low(1n+j, Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), e1, Equal.trans(Nat, C.low(1n+j, Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(C.low(j, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), e2, Equal.trans(Nat, Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(C.low(j, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(C.low(j, M.isqrt(C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), e3, e4)))

def s_st(+n: Nat, +j: Nat) -> {Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)) == Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)) : Bool}:
  +z1 = FL.add_eq0(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))
  +z2 = Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))), 0n)), Nat.is_eq(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), 0n), Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))), eb2n(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))
  +z3 = Equal.cong(Bool, Bool, t => Bool.and(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))), t), Nat.is_eq(Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))), 0n), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n), WW.dbl_eq0(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))
  +z4 = Equal.cong(Nat, Bool, w => Bool.and(Nat.is_eq(w, C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), AQ.sqm(M.isqrt(C.shift(j, C.shift(j, n)))))
  +zz = Equal.trans(Bool, Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n), Bool.and(Nat.is_eq(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), 0n), Nat.is_eq(Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))), 0n)), Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), z1, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), 0n), Nat.is_eq(Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))), 0n)), Bool.and(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))), 0n)), Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), z2, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))), 0n)), Bool.and(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), z3, z4)))
  +n1 = Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n), Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), zz)
  +n2 = Equal.sym(Bool, Bool.or(Bool.not(Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))))), Bool.not(Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n))), FL.dm2(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)))
  Equal.trans(Bool, Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)), Bool.not(Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n))), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)), n1, Equal.trans(Bool, Bool.not(Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n))), Bool.or(Bool.not(Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))))), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)), n2, AQ.sc_x(n, j)))

def s_bl(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +j: Nat, +h62: {Nat.is_le(C.shift(62n, one), M.isqrt(n)) == True{} : Bool}) -> {Nat.is_le(Nat.add(1n+j, 55n), M.bit_length(Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))) == True{} : Bool}:
  +l1 = N.le_trans(C.shift(1n+j, M.isqrt(n)), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), N.double_le(C.shift(j, M.isqrt(n)), M.isqrt(C.shift(j, C.shift(j, n))), AQ.sc_lo(n, j)), L.subst(Nat, z => {Nat.is_le(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), z) == True{} : Bool}, Nat.add(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), NA.add_comm(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), N.le_add_right(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))))
  +l2 = L.subst(Nat, z => {Nat.is_le(C.shift(1n+j, M.isqrt(n)), z) == True{} : Bool}, Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Equal.sym(Nat, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), mform(n, j)), l1)
  +f62 = Equal.trans(Bool, C.fits(62n, M.isqrt(n)), Nat.is_lt(M.isqrt(n), C.shift(62n, one)), False{}, Equal.sym(Bool, Nat.is_lt(M.isqrt(n), C.shift(62n, one)), C.fits(62n, M.isqrt(n)), FR.lt_fit(62n, one, h1, M.isqrt(n))), N.le_not_lt(M.isqrt(n), C.shift(62n, one), h62))
  +f54 = FL.nfit_mono(54n, 62n, M.isqrt(n), {==}, f62)
  +fS = Equal.trans(Bool, C.fits(Nat.add(1n+j, 54n), C.shift(1n+j, M.isqrt(n))), C.fits(54n, M.isqrt(n)), False{}, RT.fits_sh(1n+j, 54n, M.isqrt(n)), f54)
  +fM = FR.nfit(Nat.add(1n+j, 54n), C.shift(1n+j, M.isqrt(n)), Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), l2, fS)
  +b1 = FL.nfit_bl(Nat.add(1n+j, 54n), Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), fM)
  L.subst(Nat, z => {Nat.is_le(1n+z, M.bit_length(Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))) == True{} : Bool}, 1n+Nat.add(j, 54n), Nat.add(j, 55n), Equal.sym(Nat, Nat.add(j, 55n), 1n+Nat.add(j, 54n), N.add_succ(j, 54n)), b1)

# the spec's rounded root equals roundPackToF64 of the sticky floor root
def sq_spec(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +j: Nat, +h62: {Nat.is_le(C.shift(62n, one), M.isqrt(n)) == True{} : Bool}, +Es: Nat, +x: Nat, +hEx: {Nat.add(Es, 1n+j) == x : Nat}) -> {SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Es) == SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x) : F.F64}:
  +r1 = RT.round_jam(False{}, 1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Es, s_bl(one, h1, n, j, h62))
  +r2 = Equal.cong(Nat, F.F64, z => SF.round(False{}, SW.jam(z, C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), M.isqrt(n), s_high(n, j))
  +r3 = Equal.cong(Nat, F.F64, z => SF.round(False{}, SW.jam(M.isqrt(n), z), Nat.add(Es, 1n+j)), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), s_low(n, j))
  +r4 = Equal.cong(Nat, F.F64, z => SF.round(False{}, z, Nat.add(Es, 1n+j)), SW.jam(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))), SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)))), Equal.sym(Nat, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)))), SW.jam(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))), FL.jmin(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))))))
  +r5 = Equal.cong(Bool, F.F64, t => SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(t)), Nat.add(Es, 1n+j)), Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)), s_st(n, j))
  +r6 = Equal.cong(Nat, F.F64, z => SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), z), Nat.add(Es, 1n+j), x, hEx)
  Equal.trans(F.F64, SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Es), SF.round(False{}, SW.jam(C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r1, Equal.trans(F.F64, SF.round(False{}, SW.jam(C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r2, Equal.trans(F.F64, SF.round(False{}, SW.jam(M.isqrt(n), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r3, Equal.trans(F.F64, SF.round(False{}, SW.jam(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r4, Equal.trans(F.F64, SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r5, r6)))))