The tables of a prime, the soundness of the rows and the exit

The tables of the sieve compute what they claim: the squares, the inverses and Horner's rule modulo p. With them, the row of a denominator b in the table of a prime p lets the numerator a of every point (a, y, b) through (Ratpoints.Sieve.admits_examinePrime_of_sq_eq): for p ∤ b, since F(a, b) ≡ b ^ D f(a / b) (mod p) with D even, so that f(a / b) is a square modulo p (Ratpoints.Sieve.isSquare_sum_mul_div_pow_of_sq_eq_binaryForm), which the table of the prime marks (Ratpoints.Sieve.getElem!_isFSquare_examinePrime_of_isSquare); for p ∣ b, since gcd(a, b) = 1, so that p ∤ a (Int.toNat_emod_ne_zero_of_gcd_eq_one). The model computes modulo p in ℕ; the proofs go through ZMod p.

The table of a prime with the exit (Ratpoints.Sieve.examinePrime?) reduces the coefficients on two paths with the same result, since the helper mod of the C code is the Euclidean % (Ratpoints.Sieve.modLong_eq_emod), and computes the values of f by Horner's rule with Barrett's reduction on a fixed schedule (Ratpoints.Sieve.hornerBarrett): Barrett's reduction gives the remainder of every u < 2 ^ 64 (Ratpoints.Sieve.barrett_eq), and for p < maxPrimeEven the accumulator stays below p ^ (hornerSteps + 1) < 2 ^ 64 between two reductions (Ratpoints.Sieve.HornerInvariant.lt_two_pow_64). So for 0 < p < maxPrimeEven the table that its loop over the residues gives is that of the reference Ratpoints.Sieve.examinePrime, handed back with the coefficients reduced modulo p, and when it gives none for a prime p, the curve has no points (Ratpoints.Sieve.not_isPoint_of_run_examinePrime?_eq_none): a point (a, y, b) gives a residue that the table marks for p ∤ b, and for p ∣ b a point at infinity modulo p, the last entry of the table, since c_d is then a square modulo p for even d (Ratpoints.Sieve.isSquare_getD_degree_of_sq_eq_binaryForm). The values of the C code that could leave the range of a long stay in it: those of mod for moduli below 2 ^ 59, whose inputs are longs by the flag of the longs, the negations of the map of a reversed search, and the negation of a negative leading coefficient in jacobi1, with LONG_MIN replaced by its quarter; these lemmas discharge the range obligations that the Deviation paragraphs and the docstrings of the model state, and no proof consumes them.

Main definitions

• Ratpoints.Sieve.HornerInvariant, Ratpoints.Sieve.ExaminePrimeInvariant: the invariants of the loop of Horner's rule in Ratpoints.Sieve.hornerBarrett and of the loop over the residues in Ratpoints.Sieve.examinePrime?.

Main statements

• Ratpoints.sum_mul_pow_mul_pow_sub_of_eq_mul, Ratpoints.sum_mul_pow_mul_pow_sub_of_eq_mul_right: the binary form of degree D at a = k b is f(k) b ^ D, and at b = t a the value at t of the reversed polynomial times a ^ D, in any commutative semiring.
• Ratpoints.isSquare_sum_mul_pow_of_sq_eq_binaryForm, Ratpoints.isSquare_sum_mul_pow_sub_of_sq_eq_binaryForm: a point whose denominator, or numerator, is a unit of a commutative ring makes f, or the reversed polynomial, take a square value there.
• Ratpoints.Sieve.getElem!_squaresMod_mul_self_mod, Ratpoints.Sieve.getElem!_squaresMod_of_isSquare, Ratpoints.Sieve.getElem!_inversesMod_mul_mod, Ratpoints.Sieve.natCast_evalMod, Ratpoints.Sieve.natCast_evalMod_reverse: the tables compute their definitions.
• Ratpoints.Sieve.getElem!_isFSquare_examinePrime_of_isSquare: the table of a prime marks every residue at which f takes a square value.
• Ratpoints.Sieve.getElem!_isFSquare_examinePrime_self: the entry of the table of a prime at p says whether there are points at infinity modulo p.
• Ratpoints.Sieve.admits_examinePrime_of_sq_eq: the rows let every point through.
• Ratpoints.Sieve.isPrimeEntry_examinePrime: a sieve entry of a prime p ≤ 2 ^ 32 whose single factor is its table, with its reciprocal, has the shape that the third stage needs.
• Ratpoints.Sieve.barrett_eq: Barrett's reduction computes the remainder of every u < 2 ^ 64.
• Ratpoints.Sieve.HornerInvariant.lt_two_pow_64: the accumulator of Horner's rule in the table of p < maxPrimeEven stays below 2 ^ 64 (Ratpoints.pow_hornerSteps_add_one_lt).
• Ratpoints.Sieve.hornerBarrett_spec: Horner's rule with Barrett's reduction on its schedule computes the value modulo p (Ratpoints.Sieve.evalMod).
• Ratpoints.Sieve.examinePrime?_eq_examinePrime?_false, Ratpoints.Sieve.examinePrime?_spec, with its plain forms Ratpoints.Sieve.run_examinePrime?, Ratpoints.Sieve.eq_examinePrime_of_run_examinePrime?_eq_some, Ratpoints.Sieve.eq_map_range_of_run_examinePrime?_eq_some and Ratpoints.Sieve.run_examinePrime?_eq_none_iff: the two paths of the table with the exit give the same result, which is the table of the reference with the coefficients reduced modulo p for 0 < p < maxPrimeEven, and when it gives none; Ratpoints.Sieve.eq_examinePrime_of_lt_numPrimes_of_run_examinePrime?_eq_some: so for the prime at a position below Ratpoints.numPrimes of the table.
• Ratpoints.Sieve.any_isFSquare_examinePrime_of_sq_eq, Ratpoints.Sieve.not_isPoint_of_run_examinePrime?_eq_none, Ratpoints.Sieve.not_isPoint_of_lt_numPrimes_of_run_examinePrime?_eq_none: a point makes an entry of the table of a prime true, so a curve without points modulo a prime has no points.
• Ratpoints.fitsLong_natCast: a natural number is a long exactly when it is below 2 ^ 63.
• Ratpoints.fitsLong_sixteen_mul, Ratpoints.fitsLong_add_sixteen_mul, Ratpoints.fitsLong_neg, Ratpoints.fitsLong_neg_ite_div_four: the values of the C code that could leave the range of a long stay in it.
• Ratpoints.Setup.fitsLong_getD_of_useCLong: the inputs of mod are longs.

Notation

Local to the file: reducedCoeffs c d p and reducedCoeffArray c d p, the list and the array of the coefficients c₀, …, c_d reduced modulo p.

theorem Ratpoints.sum_mul_pow_mul_pow_sub_of_eq_mul {R : Type u_1} [CommSemiring R] {d D : ℕ} (hd : d ≤ D) (f : ℕ → R) {a b k : R} (h : a = k * b) : ∑ i ∈ Finset.range (d + 1), f i * a ^ i * b ^ (D - i) = (∑ i ∈ Finset.range (d + 1), f i * k ^ i) * b ^ D

The binary form ∑ fᵢ aⁱ b^(D - i) of degree D ≥ d at a = k b is f(k) b ^ D, in any commutative semiring; over a field, k = a / b for b ≠ 0, as Polynomial.eval_homogenize says for polynomials.

theorem Ratpoints.sum_mul_pow_mul_pow_sub_of_eq_mul_right {R : Type u_1} [CommSemiring R] {d D : ℕ} (hd : d ≤ D) (f : ℕ → R) {a b t : R} (h : b = t * a) : ∑ i ∈ Finset.range (d + 1), f i * a ^ i * b ^ (D - i) = (∑ i ∈ Finset.range (d + 1), f i * t ^ (D - i)) * a ^ D

The binary form ∑ fᵢ aⁱ b^(D - i) of degree D ≥ d at b = t a is the value ∑ fᵢ t^(D - i) of the reversed polynomial times a ^ D, in any commutative semiring.

theorem Ratpoints.isSquare_sum_mul_pow_of_sq_eq_binaryForm {R : Type u_1} [CommRing R] {c : List ℤ} {a y : ℤ} {b : ℕ} {k : R} (hb : IsUnit ↑b) (hk : ↑a = k * ↑b) (hy : y ^ 2 = binaryForm c a ↑b) : IsSquare (∑ i ∈ Finset.range (degree c + 1), ↑(c.getD i 0) * k ^ i)

A point (a, y, b) whose denominator b is a unit of the commutative ring R makes f take a square value at the k with a = k b in R: F(a, b) = f(k) b ^ D with D even.

theorem Ratpoints.isSquare_sum_mul_pow_sub_of_sq_eq_binaryForm {R : Type u_1} [CommRing R] {c : List ℤ} {a y : ℤ} {b : ℕ} {t : R} (ha : IsUnit ↑a) (ht : ↑b = t * ↑a) (hy : y ^ 2 = binaryForm c a ↑b) : IsSquare (∑ i ∈ Finset.range (degree c + 1), ↑(c.getD i 0) * t ^ (degree c + degree c % 2 - i))

A point (a, y, b) whose numerator a is a unit of the commutative ring R makes the reversed polynomial take a square value ∑ cᵢ t^(D - i) at the t with b = t a in R: F(a, b) = a ^ D ∑ cᵢ t^(D - i) with D even.

The squares, the inverses and Horner's rule modulo p

theorem Ratpoints.Sieve.exists_odd_mul_self_mod_eq {p s : ℕ} (hp : Nat.Prime p) (hs : s < p) (hs0 : s ≠ 0) : ∃ i < p, Odd i ∧ i * i % p = s * s % p

Modulo a prime p, the square of a residue s ≠ 0 below p is the square of an odd residue, of s or of p - s: the squares that the generator of the tables of ratpoints marks.

theorem Ratpoints.Sieve.getElem!_squaresMod_mul_self_mod {p s : ℕ} (hp : Nat.Prime p) (hs : s < p) : (squaresMod p)[s * s % p]! = true

theorem Ratpoints.Sieve.getElem!_squaresMod_zero {p : ℕ} (hp : Nat.Prime p) : (squaresMod p)[0]! = true

theorem Ratpoints.Sieve.getElem!_squaresMod_of_isSquare {p t : ℕ} (hp : Nat.Prime p) (ht : t < p) (h : IsSquare ↑t) : (squaresMod p)[t]! = true

theorem Ratpoints.Sieve.exists_mem_range'_mul_mod_eq_one {p r : ℕ} (hp : Nat.Prime p) (hr : r < p) (hr0 : r ≠ 0) : ∃ i ∈ List.range' 1 (p - 1), i * r % p = 1

Modulo a prime p, a residue 0 < r < p has an inverse among 1, …, p - 1, so that the trial of Ratpoints.Sieve.inversesMod finds one.

theorem Ratpoints.Sieve.getElem!_inversesMod_mul_mod {p r : ℕ} (hp : Nat.Prime p) (hr : r < p) (hr0 : r ≠ 0) : (inversesMod p)[r]! * r % p = 1

theorem Ratpoints.Sieve.getElem!_inversesMod_lt {p r : ℕ} (hr : r < p) : (inversesMod p)[r]! < p

theorem Ratpoints.Sieve.natCast_mul_getElem!_inversesMod_mod {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℕ) {r : ℕ} (hr : r < p) (hr0 : r ≠ 0) : ↑(x * (inversesMod p)[r]! % p) = ↑x / ↑r

@[simp]

theorem Ratpoints.Sieve.evalMod_nil (p x : ℕ) : evalMod [] p x = 0

@[simp]

theorem Ratpoints.Sieve.evalMod_cons (a : ℕ) (cs : List ℕ) (p x : ℕ) : evalMod (a :: cs) p x = (a + x * evalMod cs p x) % p

theorem Ratpoints.Sieve.evalMod_lt (cs : List ℕ) {p : ℕ} (hp : 0 < p) (x : ℕ) : evalMod cs p x < p

theorem Ratpoints.Sieve.natCast_evalMod (cs : List ℕ) (p x : ℕ) : ↑(evalMod cs p x) = ∑ k ∈ Finset.range cs.length, ↑(cs.getD k 0) * ↑x ^ k

theorem Ratpoints.Sieve.natCast_getD_map_range_toNat_emod (c : List ℤ) {d m : ℕ} [NeZero m] {k : ℕ} (hk : k < d + 1) : ↑((List.map (fun (n : ℕ) => (c.getD n 0 % ↑m).toNat) (List.range (d + 1))).getD k 0) = ↑(c.getD k 0)

Entry k ≤ d of the coefficients c₀, …, c_d reduced modulo m is c_k in ZMod m.

theorem Ratpoints.Sieve.natCast_evalMod_map_range (c : List ℤ) (d : ℕ) {p : ℕ} [NeZero p] (t : ℕ) : ↑(evalMod (List.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (List.range (d + 1))) p t) = ∑ k ∈ Finset.range (d + 1), ↑(c.getD k 0) * ↑t ^ k

theorem Ratpoints.Sieve.natCast_evalMod_reverse (cs : List ℕ) (m x : ℕ) : ↑(evalMod cs.reverse m x) = ∑ k ∈ Finset.range cs.length, ↑(cs.getD k 0) * ↑x ^ (cs.length - 1 - k)

Horner's rule modulo m on the reversed list of coefficients: the value at x of the polynomial whose coefficient of x ^ (n - 1 - k) is entry k of the list of length n.

theorem Ratpoints.Sieve.evalMod_cons_zero (a : ℕ) (cs : List ℕ) (p : ℕ) : evalMod (a :: cs) p 0 = a % p

Barrett's reduction and the schedule of Horner's rule

theorem Ratpoints.Sieve.barrett_eq {u p : ℕ} (hp : 0 < p) (hu : u < 2 ^ 64) : barrett u p ((2 ^ 64 - 1) / p) = u % p

Barrett's reduction with the reciprocal ⌊(2 ^ 64 - 1) / p⌋ computes u mod p for every u < 2 ^ 64: the estimate of the quotient is ⌊u / p⌋ or one less (Nat.mul_sub_one_div_div_mul_le, Nat.lt_mul_sub_one_div_div_add_two_mul), so that one conditional subtraction finishes.

def Ratpoints.Sieve.HornerInvariant (cm : Array ℕ) (d p a i k s : ℕ) : Prop

The invariant of the loops of Horner's rule of Ratpoints.Sieve.hornerBarrett after i steps, the last reduction k steps back: the accumulator s is congruent modulo p to the value at a of the polynomial with the coefficients cm[d - i], …, cm[d], and below p ^ (k + 1).

Equations

• Ratpoints.Sieve.HornerInvariant cm d p a i k s = (s % p = Ratpoints.Sieve.evalMod (List.drop (d - i) cm.toList) p a ∧ s < p ^ (k + 1))

theorem Ratpoints.Sieve.hornerInvariant_zero {cm : Array ℕ} {d p : ℕ} (hsize : cm.size = d + 1) (a : ℕ) (hd : cm[d]! < p) : HornerInvariant cm d p a 0 0 cm[d]!

theorem Ratpoints.Sieve.HornerInvariant.pos {cm : Array ℕ} {d p a i k s : ℕ} (h : HornerInvariant cm d p a i k s) : 0 < p

theorem Ratpoints.Sieve.HornerInvariant.lt_two_pow_64 {cm : Array ℕ} {d p a i k s : ℕ} (h : HornerInvariant cm d p a i k s) (hp : p < maxPrimeEven) (hk : k ≤ hornerSteps) : s < 2 ^ 64

The range obligation of the accumulator of Horner's rule in examine_prime: for p < maxPrimeEven, the values s a + c of the steps (find_points.c:1729, find_points.c:1741) and the values that Barrett's reduction takes (find_points.c:1731, find_points.c:1742, find_points.c:1744) are below p ^ (k + 1) with k ≤ hornerSteps, so below 2 ^ 64: the unsigned long does not wrap.

theorem Ratpoints.Sieve.HornerInvariant.add_one {cm : Array ℕ} {d p a i k s : ℕ} (h : HornerInvariant cm d p a i k s) (hsize : cm.size = d + 1) (hi : i < d) (ha : a < p) (hc : cm[d - 1 - i]! < p) : HornerInvariant cm d p a (i + 1) (k + 1) (s * a + cm[d - 1 - i]!)

theorem Ratpoints.Sieve.HornerInvariant.barrett_zero {cm : Array ℕ} {d p a i k s : ℕ} (h : HornerInvariant cm d p a i k s) (hp : p < maxPrimeEven) (hk : k ≤ hornerSteps) : HornerInvariant cm d p a i 0 (barrett s p ((2 ^ 64 - 1) / p))

The reduction by Barrett's method in the loop of Horner's rule keeps the invariant and restarts the bound.

theorem Ratpoints.Sieve.HornerInvariant.barrett_eq_evalMod {cm : Array ℕ} {d p a k s : ℕ} (h : HornerInvariant cm d p a d k s) (hp : p < maxPrimeEven) (hk : k ≤ hornerSteps) : barrett s p ((2 ^ 64 - 1) / p) = evalMod cm.toList p a

theorem Ratpoints.Sieve.HornerInvariant.push {cm : Array ℕ} {d p a k s : ℕ} {pref suff : List ℕ} {cur : ℕ} (h : HornerInvariant cm d p a pref.length k s) (hl : ForIn.toList [:d] = pref ++ cur :: suff) (hsize : cm.size = d + 1) (ha : a < p) (hcm : ∀ (i : ℕ), cm[i]! < p) : HornerInvariant cm d p a (pref ++ [cur]).length (k + 1) (s * a + cm[d - 1 - cur]!)

theorem Ratpoints.Sieve.HornerInvariant.push_self {cm : Array ℕ} {d p a s : ℕ} {pref suff : List ℕ} {cur : ℕ} (h : HornerInvariant cm d p a pref.length pref.length s) (hl : ForIn.toList [:d] = pref ++ cur :: suff) (hsize : cm.size = d + 1) (ha : a < p) (hcm : ∀ (i : ℕ), cm[i]! < p) : HornerInvariant cm d p a (pref ++ [cur]).length (pref ++ [cur]).length (s * a + cm[d - 1 - cur]!)

The step of the loop of Horner's rule of Ratpoints.Sieve.hornerBarrett without reductions, for d ≤ hornerSteps.

theorem Ratpoints.Sieve.HornerInvariant.push_barrett {cm : Array ℕ} {d p a k s : ℕ} {pref suff : List ℕ} {cur : ℕ} (h : HornerInvariant cm d p a pref.length k s ∧ k < hornerSteps) (hl : ForIn.toList [:d] = pref ++ cur :: suff) (hk : k + 1 = hornerSteps) (hsize : cm.size = d + 1) (hp : p < maxPrimeEven) (ha : a < p) (hcm : ∀ (i : ℕ), cm[i]! < p) : HornerInvariant cm d p a (pref ++ [cur]).length 0 (barrett (s * a + cm[d - 1 - cur]!) p ((2 ^ 64 - 1) / p)) ∧ 0 < hornerSteps

The step of the loop of Horner's rule of Ratpoints.Sieve.hornerBarrett with reductions, for d > hornerSteps, that reduces.

theorem Ratpoints.Sieve.HornerInvariant.push_lt {cm : Array ℕ} {d p a k s : ℕ} {pref suff : List ℕ} {cur : ℕ} (h : HornerInvariant cm d p a pref.length k s ∧ k < hornerSteps) (hl : ForIn.toList [:d] = pref ++ cur :: suff) (hk : ¬k + 1 = hornerSteps) (hsize : cm.size = d + 1) (ha : a < p) (hcm : ∀ (i : ℕ), cm[i]! < p) : HornerInvariant cm d p a (pref ++ [cur]).length (k + 1) (s * a + cm[d - 1 - cur]!) ∧ k + 1 < hornerSteps

The step of the loop of Horner's rule of Ratpoints.Sieve.hornerBarrett with reductions, for d > hornerSteps, that does not reduce.

theorem Ratpoints.Sieve.HornerInvariant.barrett_eq_evalMod_of_le {cm : Array ℕ} {d p a s : ℕ} (h : HornerInvariant cm d p a (ForIn.toList [:d]).length (ForIn.toList [:d]).length s) (hp : p < maxPrimeEven) (hd : d ≤ hornerSteps) : barrett s p ((2 ^ 64 - 1) / p) = evalMod cm.toList p a

The exit of the loop of Horner's rule of Ratpoints.Sieve.hornerBarrett without reductions, for d ≤ hornerSteps, with the reduction at the end.

theorem Ratpoints.Sieve.HornerInvariant.barrett_eq_evalMod_of_lt {cm : Array ℕ} {d p a k s : ℕ} (h : HornerInvariant cm d p a (ForIn.toList [:d]).length k s ∧ k < hornerSteps) (hp : p < maxPrimeEven) : barrett s p ((2 ^ 64 - 1) / p) = evalMod cm.toList p a

The exit of the loop of Horner's rule of Ratpoints.Sieve.hornerBarrett with reductions, for d > hornerSteps, with the reduction at the end.

theorem Ratpoints.Sieve.hornerBarrett_spec (cm : Array ℕ) (d p a : ℕ) : ⦃ cm.size = d + 1 ∧ p < maxPrimeEven ∧ a < p ∧ ∀ (i : ℕ), cm[i]! < p ⦄ hornerBarrett cm d p ((2 ^ 64 - 1) / p) a ⦃ fun (r : ℕ) => r = evalMod cm.toList p a ⦄

The contract of Ratpoints.Sieve.hornerBarrett: for a modulus p < maxPrimeEven, a residue a < p and d + 1 coefficients below p, Horner's rule with Barrett's reduction on its schedule computes the value modulo p at a (Ratpoints.Sieve.evalMod); the accumulator stays below 2 ^ 64 (Ratpoints.Sieve.HornerInvariant.lt_two_pow_64).

The table of a prime

@[simp]

theorem Ratpoints.Sieve.p_examinePrime (c : List ℤ) (d p : ℕ) : (examinePrime c d p).p = p

@[simp]

theorem Ratpoints.Sieve.inverses_examinePrime (c : List ℤ) (d p : ℕ) : (examinePrime c d p).inverses = inversesMod p

theorem Ratpoints.Sieve.isPrimeEntry_examinePrime (c : List ℤ) (d : ℕ) {p : ℕ} (hp : Nat.Prime p) (hp32 : p ≤ 2 ^ 32) {e : SieveEntry} (hf : e.factors = [Factor.prime (examinePrime c d p)]) (hep : e.p = p) (hm : e.magic = magic p) : e.IsPrimeEntry

The sieve entry of a prime p ≤ 2 ^ 32 whose single factor is the table of the reference, with the reciprocal of p, has the shape that the third stage needs (Ratpoints.Sieve.SieveEntry.IsPrimeEntry), whatever its fields of the packing: the inverses of the nonzero residues are residues, and nonzero, since they are inverses.

theorem Ratpoints.Sieve.getElem!_isFSquare_examinePrime (c : List ℤ) (d : ℕ) {p t : ℕ} (ht : t < p) : (examinePrime c d p).isFSquare[t]! = (squaresMod p)[evalMod (List.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (List.range (d + 1))) p t]!

@[simp]

theorem Ratpoints.Sieve.getElem!_isFSquare_examinePrime_self (c : List ℤ) (d p : ℕ) : (examinePrime c d p).isFSquare[p]! = (d % 2 == 1 || (squaresMod p)[(c.getD d 0 % ↑p).toNat]!)

The rows let every point through

theorem Ratpoints.Sieve.getElem!_isFSquare_examinePrime_of_isSquare {c : List ℤ} {d p t : ℕ} (hp : Nat.Prime p) (ht : t < p) (h : IsSquare (∑ k ∈ Finset.range (d + 1), ↑(c.getD k 0) * ↑t ^ k)) : (examinePrime c d p).isFSquare[t]! = true

The table of the prime p marks every residue t at which f = ∑ cₖ Xᵏ takes a square value modulo p.

theorem Ratpoints.Sieve.isSquare_sum_mul_div_pow_of_sq_eq_binaryForm {c : List ℤ} {p : ℕ} [Fact (Nat.Prime p)] {a y : ℤ} {b : ℕ} (hb : b % p ≠ 0) (hy : y ^ 2 = binaryForm c a ↑b) : IsSquare (∑ k ∈ Finset.range (degree c + 1), ↑(c.getD k 0) * (↑a / ↑b) ^ k)

theorem Ratpoints.Sieve.admits_examinePrime_of_sq_eq {c : List ℤ} {p : ℕ} (hp : Nat.Prime p) {a y : ℤ} {b : ℕ} (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : (examinePrime c (BruteForce.degree c) p).admits b a = true

The row of the denominator b in the table of the prime p admits the numerator a of every point (a, y, b) with gcd(a, b) = 1; neither b ≥ 1 nor an odd p is needed.

The table of a prime with the exit

theorem Ratpoints.Sieve.examinePrime?_eq_examinePrime?_false (c : List ℤ) (d p : ℕ) (u : Bool) : examinePrime? c d p u = examinePrime? c d p false

The path through longs, with the helper mod of the C code, and the path through GMP integers give the same table, whatever the coefficients: the flag of the longs changes nothing.

def Ratpoints.Sieve.ExaminePrimeInvariant (c : List ℤ) (d p k : ℕ) (t : Array Bool) : Prop

The invariant of the loop of Ratpoints.Sieve.examinePrime? over the residues 1, …, k, on the table t: entry 0 and the entries of these residues, each whether the value modulo p of Horner's rule (Ratpoints.Sieve.evalMod) on the coefficients reduced modulo p is a square modulo p.

Equations

• One or more equations did not get rendered due to their size.

theorem Ratpoints.Sieve.examinePrimeInvariant_zero (c : List ℤ) (d : ℕ) {p : ℕ} (hp : 0 < p) : ExaminePrimeInvariant c d p 0 #[(squaresMod p)[(Array.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (Array.range (d + 1)))[0]!]!]

theorem Ratpoints.Sieve.ExaminePrimeInvariant.push {c : List ℤ} {d p cur s : ℕ} {pref suff : List ℕ} {t : Array Bool} (hl : ForIn.toList [1:p] = pref ++ cur :: suff) (h : ExaminePrimeInvariant c d p pref.length t) (hs : s = evalMod (Array.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (Array.range (d + 1))).toList p cur) : ExaminePrimeInvariant c d p (pref ++ [cur]).length (t.push (squaresMod p)[s]!)

The step of the loop of Ratpoints.Sieve.examinePrime? at the residue cur, the value s of Horner's rule with Barrett's reduction being that of Horner's rule reduced at every step.

theorem Ratpoints.Sieve.ExaminePrimeInvariant.push_eq {c : List ℤ} {d p : ℕ} {t : Array Bool} (h : ExaminePrimeInvariant c d p (ForIn.toList [1:p]).length t) (hp : 0 < p) : t.push (d % 2 == 1 || (squaresMod p)[(Array.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (Array.range (d + 1)))[d]!]!) = (examinePrime c d p).isFSquare

At the end of the loop of Ratpoints.Sieve.examinePrime? over the residues, for p > 0, the table with the entry at infinity is that of the reference.

theorem Ratpoints.Sieve.ExaminePrimeInvariant.none_eq {c : List ℤ} {d p np : ℕ} {t : Array Bool} {α : Type} (f : Entry × Array ℕ × α → Entry × Array ℕ) (h : ExaminePrimeInvariant c d p (ForIn.toList [1:p]).length t ∧ np = List.count true t.toList) (hp : 0 < p) (hn : (np == 0 && !(d % 2 == 1 || (squaresMod p)[(Array.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (Array.range (d + 1)))[d]!]!)) = true) : Option.map f none = if (examinePrime c d p).isFSquare.any id = true then some (examinePrime c d p, Array.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (Array.range (d + 1))) else none

The exit of Ratpoints.Sieve.examinePrime?: no entry of the table is true.

theorem Ratpoints.Sieve.ExaminePrimeInvariant.some_eq {c : List ℤ} {d p np : ℕ} {t : Array Bool} {α : Type} (h : ExaminePrimeInvariant c d p (ForIn.toList [1:p]).length t ∧ np = List.count true t.toList) (hp : 0 < p) (hn : ¬(np == 0 && !(d % 2 == 1 || (squaresMod p)[(Array.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (Array.range (d + 1)))[d]!]!)) = true) (x : α) : Option.map (fun (x : Entry × Array ℕ × α) => (x.1, x.2.1)) (some ({ p := p, isFSquare := t.push (d % 2 == 1 || (squaresMod p)[(Array.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (Array.range (d + 1)))[d]!]!), inverses := inversesMod p }, Array.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (Array.range (d + 1)), x)) = if (examinePrime c d p).isFSquare.any id = true then some (examinePrime c d p, Array.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (Array.range (d + 1))) else none

The entry that Ratpoints.Sieve.examinePrime? returns when an entry of the table is true.

theorem Ratpoints.Sieve.examinePrime?_spec (c : List ℤ) (d p : ℕ) (u : Bool) : ⦃ 0 < p ∧ p < maxPrimeEven ⦄ examinePrime? c d p u ⦃ fun (r : Option (Entry × Array ℕ × ℕ × Float)) => Option.map (fun (x : Entry × Array ℕ × ℕ × Float) => (x.1, x.2.1)) r = if (examinePrime c d p).isFSquare.any id = true then some (examinePrime c d p, Array.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (Array.range (d + 1))) else none ⦄

The contract of Ratpoints.Sieve.examinePrime?: for 0 < p < maxPrimeEven, on both paths of the reduction of the coefficients, the table with the exit is that of Ratpoints.Sieve.examinePrime, handed back with the d + 1 coefficients reduced modulo p (the code and the density of the prime projected away: no contract reads them), when one of its entries is true, and none otherwise. Horner's rule with Barrett's reduction on its schedule gives the values of Horner's rule reduced at every step (Ratpoints.Sieve.hornerBarrett_spec).

theorem Ratpoints.Sieve.run_examinePrime? {c : List ℤ} {d p : ℕ} (u : Bool) (hp0 : 0 < p) (hp : p < maxPrimeEven) : Option.map (fun (x : Entry × Array ℕ × ℕ × Float) => (x.1, x.2.1)) (examinePrime? c d p u).run = if (examinePrime c d p).isFSquare.any id = true then some (examinePrime c d p, Array.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (Array.range (d + 1))) else none

theorem Ratpoints.Sieve.eq_examinePrime_of_run_examinePrime?_eq_some {c : List ℤ} {d p : ℕ} {u : Bool} {e : Entry} {cm : Array ℕ} {k : ℕ} {r : Float} (h : (examinePrime? c d p u).run = some (e, cm, k, r)) (hp0 : 0 < p) (hp : p < maxPrimeEven) : e = examinePrime c d p

theorem Ratpoints.Sieve.eq_examinePrime_of_lt_numPrimes_of_run_examinePrime?_eq_some {c : List ℤ} {d k : ℕ} {u : Bool} {e : Entry} {cm : Array ℕ} {code : ℕ} {r : Float} (hk : k < numPrimes) (h : (examinePrime? c d primeTable[k]! u).run = some (e, cm, code, r)) : e = examinePrime c d primeTable[k]!

theorem Ratpoints.Sieve.eq_map_range_of_run_examinePrime?_eq_some {c : List ℤ} {d p : ℕ} {u : Bool} {e : Entry} {cm : Array ℕ} {k : ℕ} {r : Float} (h : (examinePrime? c d p u).run = some (e, cm, k, r)) : cm = Array.map (fun (n : ℕ) => (c.getD n 0 % ↑p).toNat) (Array.range (d + 1))

The coefficients that the table hands back are those of f reduced modulo p.

theorem Ratpoints.Sieve.run_examinePrime?_eq_none_iff {c : List ℤ} {d p : ℕ} {u : Bool} (hp0 : 0 < p) (hp : p < maxPrimeEven) : (examinePrime? c d p u).run = none ↔ (examinePrime c d p).isFSquare.any id = false

The exit of examine_prime, for 0 < p < maxPrimeEven: no entry of the table of the reference is true.

The exit

theorem Ratpoints.Sieve.isSquare_getD_degree_of_sq_eq_binaryForm {c : List ℤ} {p : ℕ} [Fact (Nat.Prime p)] {a y : ℤ} {b : ℕ} (hab : a.gcd ↑b = 1) (hb : b % p = 0) (hd : degree c % 2 = 0) (hy : y ^ 2 = binaryForm c a ↑b) : IsSquare ↑(c.getD (degree c) 0)

A point (a, y, b) with p ∣ b, among them the points at infinity, makes the leading coefficient c_d a square modulo p for even d: since gcd(a, b) = 1, p ∤ a, and y ^ 2 ≡ c_d a ^ d (mod p).

theorem Ratpoints.Sieve.getElem!_squaresMod_of_sq_eq {c : List ℤ} (hd : degree c % 2 = 0) {p : ℕ} (hp : Nat.Prime p) {a y : ℤ} {b : ℕ} (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) (hpb : p ∣ b) : (squaresMod p)[(c.getD (degree c) 0 % ↑p).toNat]! = true

For a point (a, y, b) of a curve of even degree and a prime p ∣ b, the residue of c_d modulo p is marked as a square (Ratpoints.Sieve.isSquare_getD_degree_of_sq_eq_binaryForm).

theorem Ratpoints.Sieve.any_isFSquare_examinePrime_of_sq_eq {c : List ℤ} {p : ℕ} (hp : Nat.Prime p) {a y : ℤ} {b : ℕ} (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : (examinePrime c (degree c) p).isFSquare.any id = true

A point (a, y, b) makes an entry of the table of the prime p true: the residue a / b for p ∤ b, and the entry p at infinity for p ∣ b, since the degree is odd or c_d is a square modulo p (Ratpoints.Sieve.getElem!_squaresMod_of_sq_eq).

theorem Ratpoints.Sieve.not_isPoint_of_run_examinePrime?_eq_none {c : List ℤ} {p : ℕ} {u : Bool} (h : (examinePrime? c (degree c) p u).run = none) (hp : Nat.Prime p) (hpp : p < maxPrimeEven) (H : ℕ) (q : ℤ × ℤ × ℤ) : ¬IsPoint c H q

When the table of the prime p < maxPrimeEven is none, where examine_prime returns -1 and the search ends, the curve has no points of any height.

theorem Ratpoints.Sieve.not_isPoint_of_lt_numPrimes_of_run_examinePrime?_eq_none {c : List ℤ} {k : ℕ} {u : Bool} (hk : k < numPrimes) (h : (examinePrime? c (degree c) primeTable[k]! u).run = none) (H : ℕ) (q : ℤ × ℤ × ℤ) : ¬IsPoint c H q

The coefficients as longs

theorem Ratpoints.fitsLong_natCast (n : ℕ) : fitsLong ↑n = decide (n < 2 ^ 63)

A natural number is a long exactly when it is below 2 ^ 63: the height bounds that Ratpoints.findPoints does not refuse are those from 1 to 2 ^ 63 - 1.

theorem Ratpoints.fitsLong_sixteen_mul {b : ℤ} (hb0 : 0 ≤ b) (hb : b < 2 ^ 59) : fitsLong (16 * b) = true

The value b1 = 16 b that the helper mod of the C code (Ratpoints.Sieve.modLong) computes first is a long for 0 ≤ b < 2 ^ 59, and so is its negation (Ratpoints.fitsLong_neg), which mod compares with a.

theorem Ratpoints.fitsLong_add_sixteen_mul {a b : ℤ} (hb : b < 2 ^ 59) (ha0 : -(16 * b) ≤ a) (ha : a < 0) : fitsLong (a + 16 * b) = true

The value a + 16 b that the helper mod of the C code (Ratpoints.Sieve.modLong) computes for -16 b ≤ a < 0 is a long for b < 2 ^ 59. The other values that mod computes, but for 16 b and its negation (Ratpoints.fitsLong_sixteen_mul, Ratpoints.fitsLong_neg), lie between -b and 16 b.

theorem Ratpoints.fitsLong_neg {a : ℤ} (ha : |a| < 2 ^ 63) : fitsLong (-a) = true

The negation of an integer of absolute value below 2 ^ 63 is a long: so is the negation -16 b that the helper mod of the C code (Ratpoints.Sieve.modLong) computes for 0 ≤ b < 2 ^ 59, and so are the negations -b and -a of the map of a reversed search (Ratpoints.Sieve.swapPoint) for a point (a, y, b) with |a| ≤ H and 1 ≤ b ≤ H, since the height bound H is a long.

theorem Ratpoints.fitsLong_neg_ite_div_four {f : ℤ} (hf : fitsLong f = true) : fitsLong (-if f = -2 ^ 63 then f / 4 else f) = true

The value -f that jacobi1 forms from a negative long leading coefficient f, after it replaces LONG_MIN by LONG_MIN / 4 (find_points.c:579-584), is a long. The helper mod that jacobi1 then calls for b < 2 ^ 59 (find_points.c:585) keeps its values in the range of a long (Ratpoints.fitsLong_sixteen_mul, Ratpoints.fitsLong_neg, Ratpoints.fitsLong_add_sixteen_mul), and the other values of jacobi1 and jacobi lie between 0 and the larger of b and |f|.

theorem Ratpoints.Setup.fitsLong_getD_of_useCLong {c : List ℤ} {d n : ℕ} (h : useCLong c d = true) (hn : n ≤ d) : fitsLong (c.getD n 0) = true

The inputs of the helper mod of the C code on the path through longs of the table of a prime, the coefficients c₀, …, c_d, are longs: use_c_long holds only when each of them is.