4 The set-up
This chapter describes what a search does with its input before the sieve: it checks the coefficient list and the height bound, drops the leading zero coefficients, refuses a binary form that is not squarefree, may reverse the polynomial, delivers the points at infinity, and ends when the curve has no points modulo one of the primes it examines. The refusal theorems (Theorem 3.6) rest on it, and so do the statements on the points delivered, since after a reversal ratpoints searches another polynomial and maps its points back. The rest of the Sturm step, which begins with the remainder chain of this chapter, is in Chapter 5, the tests on the denominators that follow the set-up in Chapter 8, and the loop over the primes in which the exit fires in Chapter 6.
Throughout, \(c = [c_0, \dots , c_n]\) is the coefficient list, constant term first; \(d\) is its degree, the largest index with \(c_d \ne 0\); \(D = 2 \lceil d/2 \rceil \) and \(N = 2 \lceil n/2 \rceil \) are \(d\) and \(n\) rounded up to even numbers; \(F_c(x, z) = \sum _{i \le d} c_i x^i z^{D-i}\) is the binary form of the points (Definition 2.1), \(\Phi _c = \sum _{i \le n} c_i X^i Z^{N-i}\) the binary form of the refusals (Definition 2.3), and \(f = \sum _i c_i X^i \in \mathbb {Q}[X]\) the polynomial that the C code works with.
4.1 The order of the checks
The program refuses more than \(\mathrm{maxDegree} + 1\) coefficients with its error 3, fewer than two with error 5, and a height bound below \(1\) or one that is not a long with error 4, before it calls the library (main.c:362-380). The library refuses a degree above \(\mathrm{maxDegree}\) (find_points.c:4557-4558), and then:
- (1)
it drops the leading zero coefficients and refuses the form as not squarefree when that lowers \(\lceil n/2 \rceil \), that is when \(d + 2 \le N\), so that \(Z^2 \mid \Phi _c\) (find_points.c:4624-4632); this catches every list of two or more entries of degree \(0\), so that the refusal of a degree \(0\) as bad arguments that follows (find_points.c:4633-4633) is never met from the program; then it refuses a height bound below \(1\) (find_points.c:4658-4658);
- (2)
it turns the reversal off when the caller gives search intervals or a range of the denominators other than \(1, \dots , H\) (find_points.c:4686-4687), and runs the reversal check, which refuses the form when \(d\) is even and \(c_0 = c_1 = 0\), so that \(X^2 \mid \Phi _c\), and may reverse the polynomial (find_points.c:4732-4803);
- (3)
it takes the default interval \([-H, H]\), its ends rounded outward to doubles, when the caller gives none, and otherwise refuses as bad arguments search intervals without \(l \le u\), not increasing and strictly apart, or with a NaN end (find_points.c:4831-4855), which no command line causes;
- (4)
with the Sturm step on, it refuses the form when the remainder chain of the polynomial searched meets a zero remainder, then restricts the search intervals, and returns when nothing is left to search and there is no point at infinity (find_points.c:4857-4892);
- (5)
it sets up the tests on the denominators and chooses the moduli, each with an exit when it finds that the curve has no points (find_points.c:4954-4963, find_points.c:4996-5012);
- (6)
it delivers the points at infinity (find_points.c:5068-5105) and sieves.
The program reports the refusal as not squarefree with its error 8, and the other negative codes of the library with its error 9, but for a lack of memory, error 10 (main.c:256-261). All refusals come before the first call of the callback. Where the program and the library differ, the model follows the program: it refuses the coefficient list and the height bound before the leading zeros (so that 5 0 with \(H = 0\) is error 4, as in the program), and a height bound of \(2^{63}\) or more, which the library cannot be given, with error 4. These first checks are in the search with a callback (Definition 3.1); the rest of the set-up is one definition. Appendix A lists how else the components differ from the C code; the main deviations of the set-up are noted in the sections below.
The refusals (Definition 2.11) carry the errors 3, 5, 4, 8 and 9 of the program; an integer is a long when it lies in \([-2^{63}, 2^{63})\). The set-up of find_points_work_1, whose state is declared at find_points.c:4577-4585, for the list \(c\) of degree \(d\) and the options \(o\), normalizes the options (Ratpoints.Options.normalize), so that the reversal is allowed only when \(o\) allows it and its search region is the whole box; runs the reversal check (Definition 4.4), which may refuse or hand on a list \(c'\) of degree \(d'\); takes the search intervals of \(o\), or the default one, refusing malformed ones (Ratpoints.searchIntervals); runs the Sturm step on \(c'\) (Ratpoints.sturmRegion), which with the step on refuses the form when the remainder chain of \(c'\) is none, returns at once with nothing delivered when it keeps no interval and \(c'\) has no point at infinity, and otherwise narrows the intervals; and runs the search of \(c'\) (Ratpoints.searchPoints) with the flag of the reversal and the options of the output as the flags of the check. Whether the coefficients of \(c'\) are all longs, which the C code tests in the set-up and the model tests in the search of \(c'\), where it is used (Definition 3.2), chooses how the tables reduce them modulo a prime: by the helper mod of the C code (Ratpoints.Sieve.modLong) or by the Euclidean remainder, which agree (Chapter 7).
With the print channel that prints nothing, the search with a callback refuses, in this order, more than \(\mathrm{maxDegree} + 1\) coefficients, fewer than two, \(H = 0\) or \(H \ge 2^{63}\), \(\lceil d/2 \rceil {\lt} \lceil n/2 \rceil \) (error 8), the refusal of the reversal check with the switch of the normalized options, malformed search intervals, and the refusal of the Sturm step; otherwise it returns the outcome of the search of the list \(c'\) that the check hands on, or, when the Sturm step returns before the search, the data of the callback with the count \(0\), the flag of the reversal and no interval. The refusals do not depend on the callback. A natural number is a long exactly when it is below \(2^{63}\). The predicate \(\mathrm{IsSearchedPoly}\) collects what the refusals leave for a successful search, from which the main theorems start (Chapter 3): the reversal check of the normalized options hands on \(c'\) with its degree \(d'\); \(1 \le d' \le \mathrm{maxDegree}\); \(1 \le H {\lt} 2^{63}\); the caller’s search intervals are well formed (Definition 2.6); and with the Sturm step on, the remainder chain of \(c'\) is not none.
Unfolding the definitions gives the order; a print channel that prints nothing leaves the data as they are, and every refusing branch returns the same error for any callback. A natural number is never below \(-2^{63}\). After the refusals \(c\) has at least two entries and the leading zeros did not lower \(\lceil n/2 \rceil \), so \(d \ge 1\); the reversal check returns the degree of its list, never raises it and keeps it at least \(1\) (Lemma 4.5).
4.2 The squarefree binary form
As \(\Phi _c = Z^{N-d}\, \Phi ^0\), where \(\Phi ^0\) is the homogenization of \(f\) in degree \(d\), which \(Z\) does not divide, \(\Phi _c\) is squarefree exactly when \(N \le d + 1\) and \(f\) is squarefree (Lemma 4.3): the first condition is the test of the leading zeros, the second is what the remainder chain tests (Section 4.4). Mathlib has nothing on the squarefreeness of a homogenization; the facts that are needed are proved at Mathlib’s generality in Ratpoints/Mathlib. The search itself needs no squarefreeness: the statements on the points hold for every polynomial that the set-up hands on, also for a form that is not squarefree, which the search accepts when the Sturm step is off.
- (1)
Over a domain and for \(m \ge \deg p\), the homogenization of degree \(m\) of a polynomial \(p\) is squarefree if and only if \(p\) is squarefree and \(m \le \deg p + 1\). The homogenization of degree \(m\) of the reflection of \(p\) in degree \(m\) is that of \(p\) with the variables exchanged; so, for \(m \ge \deg p\), the homogenization of degree \(m\) of \(p\) is squarefree exactly when the reflection of \(p\) in degree \(m\) is, provided that \(m\) exceeds the degree of the reflection by at most one.
- (2)
The polynomial \(f\) of the list \(c\) has the degree \(d\) of \(c\), and \(\Phi _c\) is its homogenization of degree \(N\); so \(\Phi _c\) is squarefree if and only if \(f\) is squarefree and \(N \le d + 1\). In particular \(\Phi _c\) is not squarefree when the leading zeros lower \(\lceil n/2 \rceil \), nor when \(c_0 = c_1 = 0\), whatever the degree.
(1) The homogenization of degree \(m\) is that of degree \(\deg p\) times \(Z^{m - \deg p}\). If \(m \ge \deg p + 2\), then \(Z^2\) divides it, and if \(a^2 \mid p\), the square of the homogenization of \(a\) divides it. Conversely, if \(A^2\) divides it and \(m \le \deg p + 1\), then \(A\) is homogeneous, as a factor of a homogeneous polynomial over a semiring without zero divisors (MvPolynomial.IsHomogeneous.of_mul_left), \(Z \nmid A\), and the square of \(A(X, 1)\) divides \(p\), so \(A(X, 1)\) is a constant, and then so is \(A\). The reflection compares coefficients, and the exchange of the variables is a ring automorphism, which keeps squarefreeness. (2) The coefficient of \(X^i\) in \(f\) is \(c_i\), so \(f\) has the degree \(d \le N\); \(\Phi _c\) and the homogenization agree term by term, and (1) applies. A drop of \(\lceil n/2 \rceil \) means \(d + 2 \le N\), and \(c_0 = c_1 = 0\) gives \(X^2 \mid f\).
4.3 The reversal
When the caller allows it and the search region is the whole box, ratpoints may replace the polynomial by its reversal, in three cases in which it expects the search of the reversed polynomial to be faster. The reversal exchanges \(x\) and \(z\) in the binary form; the C code maps each point of the reversed curve back to the caller’s curve before it delivers it, so that the output holds the same points in another order, which the specification of the order follows: it names the polynomial searched, as the reversal check chooses it (Definition 2.9). The model makes a new list where the C code reverses its array in place, and writes back to the caller the flag of the reversal, not the reversed coefficients.
For the switch of the reversal and the list \(c\) of degree \(d\): if the switch is off, \(c\) itself; otherwise, for even \(d\) with \(c_0 = 0\), the refusal (not squarefree) if also \(c_1 = 0\), and else the list \(c_d, \dots , c_1, c_0\) with the degree \(d - 1\) (case 1); for even \(d\) with \(c_d\) a square and \(c_0\) not, the list \(c_d, \dots , c_0\) (case 2); for odd \(d\) with \(|c_d| \ne 1\), \(c_0 = 0\) and \(|c_1| = 1\), the list \(c_0, c_d, \dots , c_1\) (case 3); and otherwise \(c\) itself; with a flag that says whether the list is reversed (find_points.c:4744-4756, find_points.c:4759-4770, find_points.c:4775-4790). The squares are those of mpz_perfect_square_p: \(0\) and the squares of the positive integers. The map of a reversed search sends a point \((a, y, b)\) of the reversed curve to \((b, y, a)\) for \(a \ge 0\) and to \((-b, y, -a)\) for \(a {\lt} 0\); the exact check applies it to every point it finds when the flag of the reversal is set (Chapter 9), and the points at infinity use its image of the candidate \((1, 0)\) (Definition 4.9).
The check refuses exactly when its switch is on, \(d\) is even and \(c_0 = c_1 = 0\); with the switch of the normalized options, exactly when the options allow the reversal, their search region is the whole box (Definition 2.6), \(d\) is even and \(c_0 = c_1 = 0\); and it reverses only for the whole box. For \(d\) the degree of \(c\): the degree returned is that of the list returned, at most \(d\), and at least \(1\) when \(d \ge 1\). If the check reverses, the list \(c'\) it returns is the reflection of \(c\) in degree \(D\), \(c'_i = c_{D-i}\) for \(i \le D\) and \(c'_i = 0\) beyond, and \(F_{c'}(x, z) = F_c(z, x)\) for all integers \(x\) and \(z\). If the leading zeros of \(c\) do not lower \(\lceil n/2 \rceil \), then \(\Phi _c\) is squarefree if and only if the polynomial of the list handed on is, reversed or not.
By the cases of the check. In each case of a reversal the list built is the reflection, with \(c_{d+1} = 0\) in case 3; the new leading coefficient, \(c_1\), \(c_0\) or \(c_1\), is not zero, so the reversed list has the degree returned and the same \(D\), and \(F_{c'}(x, z) = \sum _i c_{D-i}\, x^i z^{D-i} = F_c(z, x)\). Without a reversal Lemma 4.3 gives the last claim; after one, the polynomial of \(c'\) is the reflection of \(f\) in degree \(D = N\), of degree \(D - 1\) or \(D\), and the reflection does not change whether the homogenization of degree \(D\) is squarefree (Lemma 4.3).
The map of a reversed search keeps the normalized pairs \((x, z)\) of height at most \(H\) (Definition 2.4) and is injective on the triples with \(z {\gt} 0\) or \((x, z) = (1, 0)\). For lists \(c\) and \(c'\) with \(F_{c'}(x, z) = F_c(z, x)\) for all \(x\) and \(z\), it sends the normalized points of height at most \(H\) of \(c'\) to points of \(c\), and the brute-force reference of \(c'\), mapped, is a permutation of that of \(c\). The reversal check hands on the polynomial and the flag of the specification of the order (Definition 2.9). The negation of an integer of absolute value below \(2^{63}\) is a long, so the map stays among the longs for \(H {\lt} 2^{63}\).
\(F_c(-b, -a) = F_c(b, a)\), since \(D\) is even. For \(a \ne 0\) the image has \(z = |a| {\gt} 0\) and \(|x| = b\); for \(a = 0\) the normalization forces \(b = 1\), and the image \((1, y, 0)\) is a point at infinity; so the box goes onto the box. On the triples with \(z {\gt} 0\) or \((x, z) = (1, 0)\) the map is its own inverse; both references list their points once (Theorem 2.15), so the mapped list is a permutation.
4.4 The remainder chain
For the coefficients \(c_0, \dots , c_d\) of \(f\), with \(d \ge 1\) and \(c_d \ne 0\), the rows of integers that sturm.c computes (sturm.c:99-163): \(s_0 = f\), \(s_1 = f'\), and for \(k = 2, \dots , d\) the row \(s_k\) from the remainder \(t\) of \(s_{k-2}\) by \(s_{k-1}\): starting from \(t = s_{k-2}\), while \(\deg t \ge \deg s_{k-1}\), \(t\) becomes \(u t - v X^{\deg t - \deg s_{k-1}} s_{k-1}\), with \(u\) and \(v\) the leading coefficients of \(s_{k-1}\) and \(t\) divided by their \(\gcd \) and signed so that \(u {\gt} 0\), and its zero leading coefficients are dropped; the result is none when \(t\) becomes zero. Otherwise \(s_k\) is \(-t\) divided by the \(\gcd \) of its coefficients, and the chain ends when \(s_k\) is constant. The contract, proved with the program logic of Lean core: the loops end, and the result is a chain (\(\mathrm{IsChain}\): rows as just described, each with a nonzero leading coefficient, their sizes decreasing from \(s_1\) on) whose last row is constant, or none, and then some chain has a last row of positive degree that reduces the row before it to zero. A chain has at most \(d + 1\) rows, the size of the table of the C code.
Three consecutive rows of a chain satisfy \(A\, s_k = Q\, s_{k+1} - g\, s_{k+2}\) with integers \(A, g {\gt} 0\) and some \(Q \in \mathbb {Q}[X]\). For \(d \ge 1\) and \(c_d \ne 0\), the chain is none if and only if \(f\) is not squarefree over \(\mathbb {Q}\). So for a list \(c\) of at least two entries whose leading zeros do not lower \(\lceil n/2 \rceil \), the chain of the list that the reversal check hands on, with the degree it returns, is none if and only if \(\Phi _c\) is not squarefree.
The relation is read off the arrays coefficient by coefficient. In a commutative ring, for units \(a\) and \(b\), \(a x = q y - b z\) makes \(y\) and \(z\) coprime exactly when \(x\) and \(y\) are; so coprimality passes down the chain from \((f, f')\) to its last two rows, which a constant last row makes coprime and a last row of positive degree that reduces the row before it to zero makes not coprime. Over \(\mathbb {Q}\), \(f\) and \(f'\) are coprime exactly when \(f\) is separable, that is squarefree. The last claim follows with Lemma 4.5: the degree handed on is at least \(1\), and \(\Phi _c\) is squarefree exactly when the polynomial handed on is.
The C code keeps the rows, not only the verdict, because the Sturm step goes on with them: the relation with positive \(A\) and \(g\) and the decreasing degrees make the rows positive multiples of the Sturm sequence of \(f\) and \(f'\), whose sign changes the step counts (Chapter 5). The model keeps each row as the array of its coefficients up to its degree, where the C code keeps a table of GMP integers with an array of degrees.
4.5 The points at infinity
The points at infinity of the polynomial searched are the triples \((1, y, 0)\) with \(y^2 = c_D\): for odd \(d\) the one point \((1 : 0 : 0)\), for even \(d\) the points \((1 : \pm \sqrt{c_d} : 0)\) when \(c_d\) is a square, and none otherwise. After a reversal they are the points \((0 : y : 1)\) of the caller’s curve.
For the callback, the list \(c\) of degree \(d\), the flags of the check and a delivery whose flag of the stop is clear: when \(d\) is odd or \(c_d\) a square, with the candidate \((a, b) = (1, 0)\), or \((0, 1)\) when the flag of the reversal is set, one call with \((a : 0 : b)\) under \(\mathrm{noCheck}\) or for odd \(d\), and otherwise the call with \((a : s : b)\) for \(s = \lfloor \sqrt{c_d} \rfloor \) and then, unless that call stopped the search or \(\mathrm{noY}\) is set, the call with \((a : -s : b)\); nothing otherwise (find_points.c:4894-4896, find_points.c:5068-5074, find_points.c:5078-5099). The contract: on a delivery whose flag is clear these calls are the delivery (Definition 2.13) of the list of \((1, 0, 0)\), or of \((1, s, 0)\) and, unless \(\mathrm{noY}\), \((1, -s, 0)\), each mapped by the map of the reversal when its flag is set, and of the empty list when there are no points at infinity; without \(\mathrm{noCheck}\) and for odd \(d\) or \(c_d \ne 0\), this list is that of the brute-force reference over the candidate \((1, 0)\), mapped after a reversal and without the point with \(y {\lt} 0\) under \(\mathrm{noY}\).
Like the C code, the model has no test \(s \ne 0\), which would matter only for even \(d\) and \(c_d = 0\) (the point \((1, 0, 0)\) twice), excluded by the refusals. The C code computes the flag lcfsq before the reversal check and clears it in case 2; the model tests \(c_d\) on the polynomial searched, which agrees for even degree, the only one that reads the flag. The search delivers the points at infinity after the choice of the moduli and returns when a call stops it there (Definition 3.2).
4.6 The exit by a prime
While it chooses the moduli (Chapter 6), ratpoints computes for each prime \(p\) it examines the table of the residues \(x\) with \(f(x)\) a square modulo \(p\), with a last entry for the points at infinity modulo \(p\) (Chapter 7). When no entry is true, examine_prime returns \(-1\) (find_points.c:1762-1762) and the search ends with no points (find_points.c:2613-2614, find_points.c:2994-2998, find_points.c:4996-5012). The model’s table with the exit, Ratpoints.Sieve.examinePrime?, is then none, and otherwise the reference table Ratpoints.Sieve.examinePrime, for every prime below \(\mathrm{maxPrimeEven} = 2^{\mathrm{maxBitsInPrime}}\), the bound of the moduli of the sieve, below which lie all the primes that the choice examines.
Let \(p\) be a prime and \(d\) the degree of \(c\). Integers \(a\) and \(y\) and a natural number \(b\) with \(\gcd (a, b) = 1\) and \(y^2 = F_c(a, b)\) make some entry of the table of \(p\) true: for \(p \nmid b\) the entry of the residue \(a b^{-1}\), and for \(p \mid b\) the entry at infinity, since then \(c_d\) is a square modulo \(p\) when \(d\) is even. So if \(p {\lt} \mathrm{maxPrimeEven}\) and the table of \(p\) with the exit is none, \(c\) has no normalized point of any height; this holds in particular for the prime at each position below \(\mathrm{numPrimes}\) of the table.
For \(p \nmid b\) the row of \(b\) admits \(a\) (Lemma 6.4), so the entry of \(a b^{-1}\) is true. For \(p \mid b\), \(b = 0\) included, \(p \nmid a\) and \(y^2 \equiv c_D a^D \bmod p\), so the entry at infinity is true: for even \(d\) because \(c_d\) is then a square modulo \(p\), for odd \(d\) always. For \(0 {\lt} p {\lt} \mathrm{maxPrimeEven}\) the table with the exit is none exactly when no entry is true (Lemma 7.1).
When the exit fires the curve has no points at all, so it changes no output. After a reversal it never fires: each case leaves the caller’s curve a point of height \(1\), \((0 : 0 : 1)\) in cases 1 and 3 and the points at infinity in case 2.