Dependencies

The degree \(d\) of \(c\) is the length of \(c\) with its trailing zeros (the leading zero coefficients of the polynomial) dropped, less one (\(0\) for a list of zeros). For integers \(x\) and \(z\),

the binary form of even degree \(D\) of the polynomial \(f = \sum _i c_i X^i\).

the polynomial made homogeneous of the even degree \(N\) that the length of its coefficient list allows. When \(\lceil n/2 \rceil \le \lceil d/2 \rceil \), the two degrees agree, \(D = N\), and \(\Phi _c(x, z) = F_c(x, z)\) for all integers \(x\) and \(z\).

A bit array has \(\mathrm{rbaPack} = 4\) words, \(\mathrm{rbaLength} = 256\) bits, as in the default build (rp-private.h:172-172, rp-private.h:174-175); bit \(t\) of bit array \(j\) is bit \(t \bmod 64\) of word \(\mathrm{rbaPack} \cdot j + \lfloor t/64 \rfloor \). The operations: bit array \(j\) of an array of words and-ed with bit array \(x\) of a row, word by word (AND, rp-private.h:176-176); the lowest \(s\) bits of bit array \(0\), or the highest \(s\) bits of bit array \(j\), cleared for \(s {\lt} \mathrm{rbaLength}\) (MASKL, MASKU, rp-private.h:206-213, rp-private.h:214-221), so that the low mask keeps bit \(t\) of word \(y\) exactly when \(s \le 64 y + t\) and the high mask keeps it in a word \(y {\lt} \mathrm{rbaPack}\, (j + 1)\) exactly when \(64 y + t + s {\lt} \mathrm{rbaLength}\, (j + 1)\); and whether bit array \(j\) is zero (TEST, TESTZ, rp-private.h:179-202). The lowest set bit of a word \(x \ne 0\) comes from the loop of RP_CTZL for a compiler without the builtin, which shifts \(x\) right while its lowest bit is clear (rp-private.h:429-444); its contract: the count is the number of trailing zeros of \(x\).

The steps of a shape form segments (find_points.c:3812-3837): the \(k\) of the squares \(k^2\), for each divisor \(s\) of the divisor shape the \(k\) of \(s k^2\), both within \([b_{\mathrm{low}}, b_{\mathrm{high}}]\), or the words of \(64\) denominators, or the denominators. The blocks have length \(\lfloor \mathrm{steps}/1024 \rfloor + 1\), at least \(16\), or the length that the build fixes (find_points.c:3838-3842), and cut each segment into consecutive pieces (find_points.c:3843-3850). A decision of the correction is the first block that it is for, with the ends \(s_2\) and \(s_3\) from that block on; the decision in force for block \(i\) is the last whose first block is at most \(i\) (find_points.c:3908-3910). Block \(i\) (find_points.c:3889-3898) hands each denominator of its steps that passes the tests of the shape to the sieve of one denominator, with the sieve entries cut by the decision in force into the first two stages, the first ending at \(s_1\), and the third; it returns when the callback stops the search, and reports its counters with its decision.

The list, computed in the model, of the triples found by testing, in this order, the candidate \((1, 0)\) if \(H \ge 1\), and then the pairs \((x, z)\) with \(1 \le z \le H\), \(-H \le x \le H\) and \(\gcd (x, z) = 1\), with \(z\) increasing and, for each \(z\), \(x\) increasing. For each candidate, \(v = F_c(x, z)\) is computed by Horner’s rule in \(x\) on the products \(c_k z^{d-k}\), computed once for each \(z\), times \(z\) when \(d\) is odd; if \(v \ge 0\) and \(v = y^2\) for \(y = \lfloor \sqrt{v} \rfloor \), the triple \((x, y, z)\) is listed, followed by \((x, -y, z)\) if \(y \ne 0\). The part of the list over one denominator \(z \ge 1\), or over the candidate \((1, 0)\) for \(z = 0\), is a function of its own, with which the proofs compare a search denominator by denominator.

The flags of the check, which decide what the exact check and the points at infinity deliver: the bits RATPOINTS_REVERSED (ratpoints.h:414-414), RATPOINTS_NO_CHECK and RATPOINTS_NO_Y of the word of flags, as three Booleans, clear by default. One call (Definition 2.13) with a point \((a : y : b)\) of the polynomial searched, mapped back to the caller’s curve when the flag of the reversal is set: with \((b : y : a)\) for \(a \ge 0\) and \((-b : y : -a)\) for \(a {\lt} 0\), and with \((a : y : b)\) otherwise, the three branches that the exact check of the C code writes at each of its calls. The callback of the model that appends each point \((x, y, z)\) to an array, with the weight \(1\), and never stops the search; with it the data of a search is the list of the points that it delivers, in their order. And a text printed through the print channel of a search: the data as the channel leaves it, the count and the flag as they are (Section 10.5).

The test for common factors on signed 64-bit words (sift.c:318-327): for \(m = 0\), whether \(n = 1\); otherwise \(m\) replaced by \(-m\) when it is negative, false when \(m\) and \(n\) are both even, and else the binary algorithm on their odd parts: while \(n \ne m\), with \(d = m - n\) and the mask \(d \gg 63\), \(n\) becomes \(n + (d \mathbin {\& } \mathrm{mask})\) and \(m\) becomes \((d \oplus \mathrm{mask}) - \mathrm{mask}\) shifted right by its trailing zeros; the result is whether \(m\) ends as \(1\) (sift.c:328-342). What the third stage needs of the entry of a prime \(p\) for \(b\) (sift.c:414-428): the entry of its table of inverses at \(b \bmod p\), or \(0\) when \(p \mid b\); the bias \(p H\) when \(2 p H {\lt} 2^{32}\), else \(0\); the reciprocal and the table of \(p\); for the entries of the stage, a thunk made once per denominator (sift.c:405-413). The third stage for \(a\): each prime whose inverse is not \(0\) rejects \(a\) when its table says that \(f\) is not a square modulo \(p\) at the residue of \(a\, b^{-1}\), reduced with the reciprocal after adding the bias if there is one, and by division otherwise (sift.c:291-301). The test of a candidate: \(a\) is prime to \(b\) and passes the third stage (sift.c:438-446). The exact check (find_points.c:5250-5338): unless \(\mathrm{noCheck}\), for the value \(v\) of Horner’s rule at \(a\) on the products \(c_k b^{d - k}\) (a thunk made once per denominator), times \(b\) for odd \(d\), so that \(v = F_c(a, b)\) (Definition 2.1), and \(y = \lfloor \sqrt{v} \rfloor \): when \(v = y^2\), the call with \((a : y : b)\) and then, unless that call stopped the search, \(y = 0\) or \(\mathrm{noY}\), the call with \((a : -y : b)\); under \(\mathrm{noCheck}\) one call with \((a : 0 : b)\); the points mapped back to the caller’s curve after a reversal.

The points that the exact check of the numerator \(a\) over the denominator \(b\) delivers, for the products \(w\) of the coefficients with the powers of \(b\), the factor \(e\) (\(b\) for odd degree, \(1\) for even degree) and the flags: under \(\mathrm{noCheck}\) the survivor \((a, 0, b)\); otherwise, when the value of Horner’s rule in \(a\) on \(w\), times \(e\), is \(y^2\) with \(y \ge 0\), the point \((a, y, b)\) and, for \(y \ne 0\), the point \((a, -y, b)\), which is left out under \(\mathrm{noY}\), and none when that value is no square; each mapped to the caller’s curve when the flag of the reversal is set, \((a, y, b)\) to \((b, y, a)\) for \(a \ge 0\) and to \((-b, y, -a)\) for \(a {\lt} 0\). The points of a numerator with the flags: these when \(\gcd (a, b) = 1\), and none otherwise.

The choice for the curve, with the options of the sieve as the search normalizes them (Definition 2.11), takes these steps:

1. (1)

   the tuning, from -r, -R, -U and -C or the defaults (find_points.c:2569-2575);

2. (2)

   the first estimate, the loop of the tables with its exit, which returns the prime, and the further forbidden divisors (find_points.c:2522-2532);

3. (3)

   the estimate and the keys again, the composite moduli with their entries (add_moduli, Section 6.2) and the sort (find_points.c:2808-2812, find_points.c:2816-2823, find_points.c:2826-2826);

4. (4)

   the first stage, the value of -n or as many as its rule wants, and the second, the value of -N or the offset, each taking candidates in their order (find_points.c:2490-2508, find_points.c:2843-2846, find_points.c:2864-2871);

5. (5)

   the third stage, up to the value of -P more or while each prime pays for itself, looking at further primes, with the exit, when no prime left pays (find_points.c:2973-2975, find_points.c:3009-3016);

6. (6)

   the end: the third stage and the reserve sorted by density from \(s_2\) on, the entries of all the candidates, their reciprocals and the store with the tables of rows of every entry (find_points.c:3024-3034).

The result holds the cut points \(s_1 \le s_2 \le s_3\), the ends of the three stages, the number of primes looked at and the estimates of the run (ratpoints.h:395-397), with the sieve entries of all the moduli, the reserve included, their reciprocals, the forbidden divisors, the store of the tables of rows and the switch of the checked loop.

The coefficient list, the height bound, the options of the sieve, the options of the search and the settings of the output that a command line gives, or its first failure, in the order of main.c. Fewer than two arguments fail with error 2 (main.c:210-214). The first argument gives the coefficients, constant term first, integers separated by white space: a word that is not an integer fails with error 11 wherever it stands, then more than \(\mathrm{maxDegree} + 1\) integers fail with error 3 and fewer than two with error 5. The second gives the height bound, a C long of at least \(1\), or error 4. The options are read from left to right, the last setting of each kind winning. An unknown option, an argument among the options that does not begin with -, a missing or malformed argument of an option (but for -l and -u) and -f or -d followed by another character fail with error 6 (main.c:393-400, main.c:437-532, main.c:533-577, main.c:638-649, main.c:650-668); -l and -u read the ends of the search intervals (Definition 10.7), with error 7 for ends that are missing, no numbers, not alternating, too many or not ordered. Then a pending interval is completed, the format is (%x : %z)\n under -x or -y and (%x : %y : %z)\n otherwise, unless -f gave one, and -q cancels -v (main.c:688-688). A failure prints the message of the function error of main.c, for errors 2 and 6 with the banner and the usage (main.c:1036-1048).

The readers of the numbers, on the words of an argument, its maximal runs of characters other than C white space: an integer of the coefficient list as scan_mpz reads it, with an optional sign and of any size; a C long as scan_long reads it, from \(-2^{63}\) to \(2^{63} - 1\), with only white space around it (main.c:733-740); and a real number as scan_double reads it, the double that strtod of glibc reads in the C locale, none for a NaN (main.c:746-752): \(\pm \infty \) for an infinity, and otherwise the double nearest to the exact value \(\pm m\, 10^{e - k}\) of the word, or \(\pm m\, 2^{e - 4k}\) for a hexadecimal word, with ties to even. An end of a search interval as scan_end reads it: the number that the argument denotes, or an infinity, also for a number beyond the range of the doubles, and \(\pm 2^{-1075}\) for a nonzero number that strtod reads as \(0\), which lies between \(0\) and every other \(x\) of the search as the number does; with the double that the library is given for it, the double of strtod moved outward to the largest double at most a lower end, or the smallest double at least an upper end (main.c:798-806). The reading of the intervals of -l and -u into the doubles and the exact ends of at most \(\mathrm{maxDegree}\) intervals (main.c:66-66, main.c:73-73), a missing first lower end or last upper end standing for \(\mp \infty \) with the double \(\mp h\) of the height bound, or \(\mp \infty \) when that double would turn the interval round. The test whether \(a/b\) lies in one of these intervals, by the binary search of in_region over their exact ends (main.c:126-137). And the intervals that the library is given, those of the command line joined where their doubles meet or overlap (main.c:891-905).

The data that main.c passes to its callback process (main.c:110-113): whether a point was printed, the settings of the output that process reads, the search intervals of the command line, before they are joined, with their exact ends, and the text printed so far. The callback on \((x, z, y)\) (main.c:139-142, main.c:150-156) passes over, with the weight \(0\) and the flag clear, a point at infinity under -i and an affine point whose \(x/z\) lies in none of the search intervals of the command line, when it gives some (the library searches them with the doubles outward of the exact ends); every other point is one that it keeps. It gives such a point the weight \(1\), stops the search at it under -1, and prints it in the format unless -z, after the string before the points if it is the first point printed and after the string between them otherwise. The format prints %x, %y and %z as the coordinates in decimal (%y as itself under -x or -y), \t, \n, \\ and \% as a tab, a line feed, a backslash and a percent sign, and every other character as itself (main.c:157-177, main.c:178-182, main.c:183-186); a string prints in the same way, its percent signs not special (main.c:952-960).

The messages of the report of main.c (main.c:979-1033), among them the search region of the command line (message 3), the numbers of the moduli used (message 4), what the search did, from the bits written back (message 7), the search intervals as the search leaves them (message 8), and the count of the points, or of the point pairs under -x or -y (message 2). The program on a command line (main.c:195-198): on a failure of the command line, the message and the status of the failure. Otherwise, unless -q, the head of the report: the banner, the curve, the height bound unless -v (main.c:215-220), and message 3 when the command line gives intervals (main.c:224-224); then the search with a print channel (Definition 3.1), with the options of the sieve of the command line and the array size that main.c sets (main.c:221-222), the options of the search on the joined intervals (main.c:248-248), the callback of the program on its data and, under -v, the print channel that appends to the text of the data (main.c:251-252). On a refusal it prints what the library printed and the message of the error that main.c gives for it (Ratpoints.Cli.Failure.ofRefusal: error 8 for a binary form that is not squarefree), and exits with that status. Otherwise it prints what the callback and the library printed, the string before the points if no point was printed (main.c:265-265), the string after them (main.c:267-267) and, unless -q, the end of the report: two line feeds and messages 4, 7 and 8 unless -v, then message 2 (main.c:268-276); its status is \(0\) (main.c:284-285).

The bisection, the nested function iterate of gcc (sturm.c:197-208, sturm.c:228-233, sturm.c:261-267), works on intervals whose ends are \(n/2^e\), with longs \(n\) and \(e\), or \(\mp \infty \), written \(\mp \mathrm{LONG\_ MAX}\) with the exponent \(0\). It evaluates the rows of the chain at \(n/2^e\) by Horner’s rule in integers, which computes \(2^{e \deg s}\) times the value of the row \(s\), and counts their sign changes, zeros skipped. An interval with the counts \(c_l\), \(c_r\) at its ends and the signs \(\sigma _l\), \(\sigma _r\) of \(f\) just inside them is dropped when \(c_l = c_r\) and \(\sigma _l {\lt} 0\); it is kept when \(c_l = c_r\) and \(\sigma _l {\gt} 0\), or at the depth of the step, its ends converted to doubles, \(\mathrm{ldexp}((\mathrm{double})\, n, -e)\), and appended to the intervals kept, or joined to the last of them when that ends at its lower end (== of doubles); and otherwise it is split at its midpoint \(m\), the left half bisected first, both halves with the count and the sign of \(f\) at \(m\), except that at a root \(m\) the left half gets the count plus \(1\) and \(-\mathrm{sign}\, f'(m)\), the right half \(\mathrm{sign}\, f'(m)\). The midpoint is \(0\) for \([-\infty , +\infty ]\); \(-1\) or \(2 n_r\) for \([-\infty , n_r]\) and \(1\) or \(2 n_l\) for \([n_l, +\infty ]\), as the finite end is \(0\) or not; and otherwise half the sum of the ends over the larger denominator. An interval is well formed at the depth \(\delta \) when it has one of the four shapes that the bisection meets (the whole line; an infinite interval whose finite end, of exponent \(0\), is \(0\) or on its side of \(0\); two finite ends, equal exponents being \(0\)), its exponents lie between \(0\) and \(\delta \), its finite numerators over the larger exponent are at most \(2^{\delta }/4\) in absolute value from the depth \(1\) on, and its ends increase.

The intersection with the caller’s intervals goes by two cursors: of the two current intervals, compared as doubles, the one that begins first is skipped when it ends before the other begins; otherwise their intersection is noted and the cursor of the one that ends first moves on (sturm.c:289-322). The Sturm step on \(f\) of degree \(d \ge 1\) with \(c_d \ne 0\) (sturm.c:86-97, sturm.c:177-190, sturm.c:269-273): none when the remainder chain is none; no interval when the counts at \(\mp \infty \) agree, so that \(f\) has no real root, and \(c_0 {\lt} 0\); otherwise the intervals that the bisection keeps from \([-\infty , +\infty ]\), started with the counts and the signs of \(f\) at \(\mp \infty \), intersected with the caller’s intervals. The Sturm step of the search, on the polynomial that the reversal check hands on, at the normalized depth (find_points.c:4879-4892): with the step off, the intervals as they are; the refusal \(\mathrm{notSquarefree}\) when the chain is none; the intervals left, when there are some; and when there are none, none for an even \(d\) whose leading coefficient is not a square, so that the search returns at once, there being no point at infinity either, and otherwise no intervals with the flag sturm_empty, by which the search delivers the points at infinity only.

The counters of the run, the sums of the counters of the blocks folded (Definition 9.1), those from the extracted numerators on restarted when a block sifted with another \(s_2\) is folded (find_points.c:1363-1367). The correction (find_points.c:1383-1388), when the run has swept enough words, sets the next one at twice the words swept and computes the rates, the walk of \(s_2\) under -A 2 or more and the end of the third stage, every double in the order of the C code. The fold of block \(j\) (find_points.c:4114-4127) adds its counters to the state of the correction and appends a decision for the blocks from \(j + \mathrm{adaptLag} + 1\) on when the correction changes an end. The run starts from the decision of the choice for block \(0\), sifts each block with the decisions made before it and folds its report, returns after the block in which the callback stopped the search, and gives the ends \(s_2\) and \(s_3\) of the last block folded, the moduli used (find_points.c:5152-5160).

A candidate modulus carries its density, key and cost, its mask of primes, its sieve entry and the codes of its factors (find_points.c:147-149). Its cost per word swept, in units of an and of the first stage, is a part for every word, the cost of its entry in the list of the moduli of a denominator and, in the first two stages, the costs of its set-up and, for a positive cost of a row, of its table of rows, spread over the \(U\) words and the \(V\) denominators of the run (find_points.c:1220-1235); its key is that cost over \(-\log r\) (find_points.c:1241-1247), with a variant for the first stage (find_points.c:1256-1270). The rule of the first stage always takes the first candidate and then the next while the survivors per word that it removes, weighted by what a surviving word costs further on, exceed a target times its cost (find_points.c:1583-1589); the second stage adds as many moduli as an offset, \(11\) by default, scaled by \(1/(1 + u_0/U)\) (find_points.c:1619-1626). The run is estimated from \(64\) samples of each segment of the loop over the denominators (find_points.c:1939-1944), and the cost of an exact check from the bit lengths of the coefficients and of \(H\) (find_points.c:1285-1318). Every expression is computed in Float, in the order of the operations of the C code; there is no contract.

The six counters that the sieve keeps for the correction of the moduli (Chapter 6), \(64\)-bit words that wrap (rp-private.h:579-581): the words that the first stage sweeps, the bit arrays that survive it, the numerators extracted, those prime to the denominator, those that pass the third stage, and the calls of the sieve.

The callback is a function of \(x\), \(z\), \(y\) and the data, in the order of the C code, that returns what the call gives: the weight that it returns, an integer, whether it set *quit, and the data after the call (ratpoints.h:436-437, ratpoints.h:441-442). A delivery is the data of the callback, the count, the sum of the weights so far, and the flag of the stop; one call on a delivery adds the weight to the count and takes the flag and the data that the call leaves. The delivery of a list \(L\) of points to the callback, from a delivery \(r\): for each point \((x, y, z)\) of \(L\) in turn, while the flag is clear, the call with \((x, z, y)\); the points after a call that sets the flag, and all of them when it is set at the start, are passed over.

A C double by its \(64\) bits of IEEE 754 binary64, in a structure with no equality of its own (equality of the bits is not ==); and the operations that ratpoints applies to doubles, as gcc and glibc compute them with rounding to nearest, ties to even: the comparisons, false when either side is a NaN and otherwise the order of a key (the bits without the sign bit, negated when it is set); negation and fabs; the exact value of a finite double; the double nearest to \(\pm m\, 2^k\) and to \(\pm n/d\); the conversions from and to long, and to unsigned long; and frexp, ldexp and nextafter towards \(\pm \)HUGE_VAL, which pass a signalling NaN on as it is, where glibc quiets it (ratpoints passes them no NaN). These functions model the platform and hold no C range.

1. (1)

   An end \(x\) (find_points.c:3264-3271, find_points.c:3272-3291, find_points.c:3292-3299): its sign, \(x {\lt} 0\) as in C, so that \(-0.0\) is not negative; for \(|x| {\lt} 2^{63}\), \(|x| = m\, 2^{-s}\) with \(m\) odd or \(s = 0\), except that \(s\) is capped at \(127\), where \(m\, 2^{-s} \ne |x|\) but \(b\, m\, 2^{-s}\) and \(b|x|\) both lie strictly between \(0\) and \(1\) for \(1 \le b {\lt} 2^{63}\); otherwise \(m = 2^{63}\) and \(s = 0\); and the rounding \(r = 2^s - 1\) when the end wants \(b|x|\) rounded up (a lower end with \(x \ge 0\), an upper end with \(x {\lt} 0\)), else \(r = 0\). Its scaled value at \(b\), \(\min (2^{64} - 1, \lfloor (b m + r)/2^s \rfloor )\), is computed on two words (find_points.c:3231-3238).

2. (2)

   The form \((M, C, \mathit{sh})\) of an end (find_points.c:3304-3318), for which \((b M + C) \gg \mathit{sh}\) fits a long for every \(b \le b_{\mathrm{high}}\): \((0, \mp H, 0)\) for an end at or beyond the height bound on its side (\(x \le -H\) at a lower end, \(x \ge H\) at an upper end); \((\pm m, C, s)\), with \(C = 2^s - 1\) at a lower end and \(0\) at an upper end, when \(s {\lt} 64\) and \(m \le \lfloor (2^{63} - 1 - C)/b_{\mathrm{high}} \rfloor \); and none otherwise.

3. (3)

   The bounds of the search intervals (find_points.c:3323-3340): the two ends of each interval, which is taken inline, with the forms of its ends, when \(H \le 2^{63} - 65\) and both ends have a form, and otherwise gets the forms of an empty interval.

4. (4)

   The bits of an interval at \(b\) for a class of the numerators (find_points.c:3410-3434): \(\mathit{lo} = \lceil b l \rceil \) and \(\mathit{hi} = \lfloor b u \rfloor \) from the forms; the code \(2\) for \(\mathit{lo} {\gt} H\); for \(\mathit{hi} {\lt} -H\) the code \(1\) if the interval is taken inline, and otherwise what interval_bits_exact computes from the scaled ends (find_points.c:3381-3406); and otherwise the code \(0\) with the bits of the first and the last numerator of the class in \(\max (\mathit{lo}, -H), \dots , \min (\mathit{hi}, H)\).

5. (5)

   The bounds of an interval represent a range \(\mathit{lo}, \dots , \mathit{hi}\) at \(b\) when, for every class of a packing (Chapter 9: stride \(2^k\) with \(k {\lt} \mathrm{numStrides}\) and \(k \le 6\), residue \(a_0 {\lt} 2^k\)), their bits have the code \(2\) only for a range above \(H\), the code \(1\) only for one below \(-H\), and otherwise the bits of the numerators of the class in \(\max (\mathit{lo}, -H), \dots , \min (\mathit{hi}, H)\). The bounds of a run give a list of ranges at \(b\) when there is one for each interval, represented by its bounds, each with \(\mathit{lo} \le \mathit{hi} + 1\), increasing and strictly apart.

The second stage on a copy of the bit array with the word number \(i\): for each of its moduli in turn, while the copy is nonzero, the copy is and-ed with bit array \((i + \mathrm{offset}) \bmod p\) of the row, the index reduced as in the first stage (sift.c:1175-1202). The walk through a word \(x\) whose bit \(t\) stands for \(a_0 + s t\): while \(x \ne 0\), the numerator of the lowest set bit goes to the test of a candidate and, if it passes, to the exact check (Definition 9.9), the walk returning if the callback has stopped the search; then \(x\) becomes \(x \mathbin {\& } (x - 1)\) (sift.c:262-264, sift.c:1227-1255). A bit array (sift.c:1213-1226, sift.c:1257-1264): the second stage on the copy and, if the copy is still nonzero, the walk through each of its words, bit \(t\) of word \(\kappa \) standing for \(a_0 + 2^k(\mathrm{rbaLength}\, i + 64\kappa + t)\). The scan of a piece (sift.c:1061-1082): a sentinel of ones just past the piece; the zero bit arrays are stepped over, the scan stops at the sentinel, and each other bit array is sifted as above. The contracts, for specs that fit, the reciprocals of their moduli and the bounds of small, from a delivery whose flag is clear: the copy after the second stage is the copy and-ed with the rows of all the moduli of the stage; the walk, and a bit array in either arm, deliver in increasing order the points of the numerators of the set bits (of \(x\), and of the words and-ed with the rows of the second stage) that pass the test of a candidate; and if, for a test \(\varphi \) of the bits, bit \(t\) of word \(y\) of the piece and-ed with the rows of the second stage is \(t {\lt} 64 \wedge \varphi (\mathrm{rbaLength}\, w_0 + 64 y + t)\), the scan delivers in the same way the points of the numerators \(a_0 + 2^k j\) of the bits \(j\) of the piece that pass \(\varphi \) and the test of a candidate.

The search with a callback and a print channel models the library function find_points, the function find_points_work that it calls and the start of find_points_work_1 (ratpoints.h:436-437, find_points.c:4523-4528, find_points.c:4624-4633, among others). It makes the refusals of the program in its order (Lemma 4.2), first those of the coefficient list, the height bound and the leading zeros (errors 3, 5, 4 and 8), then those of the set-up (Definition 4.1), which may also return at once after the Sturm step with nothing delivered; otherwise it runs the search of the polynomial that the set-up hands on (Definition 3.2). A refusal comes with the data of the callback as the report has left it; otherwise the search returns its outcome (Definition 2.11). The print channel prints the report of the library under -v into the data of the callback (Definition 10.5). The search with a callback is this search with the data dropped from a refusal and, by default, the print channel that prints nothing; \(\mathrm{findPoints}(c, H, s, o)\) is the list of the array that it gives for the callback that appends each point and never stops (Ratpoints.appendPoint), from the empty array, or its refusal.

The chunk is \(16\), as in the default build (rp-private.h:222-224). A sieve spec (rp-private.h:378-379) holds a modulus \(p\), its row for the denominator at hand (\(p + \mathrm{chunk} - 1\) bit arrays), the offset of the row, and a start and an end for the chunked arm. It fits when \(0 {\lt} p \le \mathrm{maxPrimeEven}\), \(\mathrm{rowBias} \le \mathrm{offset} {\lt} \mathrm{rowBias} + 2p\), its end is \(p\), and bit array \(x {\lt} p + \mathrm{chunk} - 1\) of its row is bit array \(x \bmod p\). The test small says whether the word numbers of the piece lie between \(-\mathrm{rowBias}\) and \(\mathrm{rowBias} - 2\, \mathrm{maxPrimeEven}\); then the sums of a word number and an offset are reduced with the reciprocal, and otherwise by mod. The arm one row at a time (sift.c:943-1022) sets every bit array to the class pattern and then, for each modulus, and-s bit array \(j\) with bit array \((w_0 + \mathrm{offset} + j) \bmod p\) of the row. The chunked arm sets the start of each row to \((w_0 + \mathrm{offset}) \bmod p\) (sift.c:596-606); with no modulus in the stage (\(s_1 = 0\)) it writes the class pattern into every bit array, and otherwise it finds where the whole chunks end (sift.c:608-620). A whole chunk is loaded into registers as the class pattern and-ed with the first row from its start on, and-ed with the other rows and stored, each start moving on by the chunk modulo \(p\); the \(t {\lt} \mathrm{chunk}\) bit arrays after the whole chunks go in legs of \(8\), \(4\), \(2\) and \(1\) registers, one for each set bit of \(t\) (sift.c:915-940). The contract of each arm (of the chunked one under \(\mathrm{chunk} \le 16\)): for specs that fit, the reciprocals of their moduli and the bounds of small, word \(y {\lt} n\, \mathrm{rbaPack}\) of the piece is the class pattern and-ed, for each spec, with word \(y \bmod \mathrm{rbaPack}\) of bit array \((w_0 + \mathrm{offset} + \lfloor y/\mathrm{rbaPack} \rfloor ) \bmod p\) of its row.

Let \(d\) be even. The test of a valuation \(m\) at a prime \(p\) is true when, for the valuations \(w_j\) and the unit parts \(r_j\) modulo \(p\), signs included, of the nonzero \(c_{d-j}\), the least \(w_j + j m\) is taken at one \(j_0\) only and is odd, or \(j_0\) is even and \(r_{j_0}\) is not a square modulo \(p\) (find_points.c:2218-2228); the mask of the forbidden valuations at \(p\), a natural number, has bit \(m\) set for the \(m \ge 1\) with \(p^m \le b_{\mathrm{high}}\) that the test excludes (find_points.c:2229-2234). The forbidden divisor of an examined prime \(p\) (find_points.c:2642-2676): for \(p \mid c_d\) and a nonzero mask, \(p\) with its words when the mask holds every \(m \ge 1\) with \(p^m \le b_{\mathrm{high}}\), and \(p\) with its mask otherwise; for \(p \nmid c_d\), \(p\) with its words when \(c_d\) is not a square modulo \(p\), as the entry at infinity of its table says. Then, unless \(c_d\) is a square, the further primes \(p\) of the table, from the first one not examined, with \(p^2 \le b_{\mathrm{high}}\) and \(c_d\) not a square modulo \(p\), with their words, while fewer than \(\mathrm{maxForbidden}\) forbidden divisors are found (find_points.c:2709-2772). The contracts: a true test means that one term of least valuation excludes \(m\), and the mask is as described. A forbidden divisor is admissible when it is the forbidden divisor of a prime of the table, made from the residues of the coefficients and the entry at infinity of its table, or, with words, a prime of the table with its words and its reciprocal at which \(c_d\) is not a square; from admissible entries the further primes add only admissible ones, whatever the cap.

A pair \((x, z)\) of integers is normalized and of height at most \(H\) if

A triple \((x, y, z)\) of integers is a normalized point of height at most \(H\) on \(y^2 = F_c(x, z)\) if \(y^2 = F_c(x, z)\) and \((x, z)\) is normalized and of height at most \(H\). These points form a finite set \(\mathrm{points}(c, H)\): \(|x| \le H\), \(0 \le z \le H\), and \(|y| \le y^2 = F_c(x, z)\).

The binary algorithm (find_points.c:498-566, find_points.c:568-641) for \(b \ge 1\) and an integer \(\ell \): subtraction and halving on \(\ell \bmod b\) and \(b\), with the signs of \(J(2 \mid m)\) and of the reciprocity, the gcd divided out of \(b\) when it is not \(1\). Its contract: the result is \(J(\ell \mid b^*)\), where \(b^*\) is the largest divisor of \(b\) prime to \(2\ell \). The tables (find_points.c:683-708), for \(\ell = \pm 2^v \prod _i q_i^{e_i}\) and \(b_{\mathrm{high}} \le \mathrm{mulModLimit} = 2^{32} - 1\): the odd primes \(q_i\), at most \(\mathrm{jacobiPrimes} = 16\), each with its reciprocal and, for odd \(e_i\), the table of the non-squares modulo \(q_i\), at most \(\mathrm{jacobiTable} = 8192\) entries in all; and the sign for each \(b^* \bmod 8\), the product of \(J(-1 \mid b^*)\) for negative \(\ell \), \(J(2 \mid b^*)^v\) and the signs of the reciprocity of the \(q_i \equiv 3 \bmod 4\) with odd \(e_i\); none when a prime of \(\ell \) lies beyond the table or a bound is passed. The test of \(b\) (find_points.c:734-759) divides \(2\) and the \(q_i\) out of \(b\) with the reciprocals and passes when the sign of the result times its entries modulo the \(q_i\) of odd exponent is \(1\). The contracts: tables exist only for \(b_{\mathrm{high}} \le \mathrm{mulModLimit}\) and \(\ell \ne 0\), and then describe \(\ell \) as above, with primes of the table and their reciprocals; for such tables and \(1 \le b {\lt} 2^{64}\) with \(b q {\lt} 2^{64}\) for every prime \(q\) of the tables, the test is the negated exclusive or of the sign and the entries at the part of \(b\) free of \(2\) and of these primes.

The texts of the report, each as printf prints it from the data that the C code prints, with %ld, %3ld, and %.pf for the doubles and the values of Float as glibc prints them, the exact value rounded to \(p\) places with ties to even: the arguments of the search as it normalizes them (find_points.c:4691-4725); the outcome of the reversal check (find_points.c:4740-4743, find_points.c:4757-4758, find_points.c:4771-4774, find_points.c:4791-4801, find_points.c:4804-4807); the Sturm step (find_points.c:4864-4878); the points at infinity and the tests on the denominators (find_points.c:4897-4898, find_points.c:4915-4918, find_points.c:4921-4926, find_points.c:4928-4941, find_points.c:4946-4947); the packing of the classes of the numerators (find_points.c:4969-4985); the choice of the moduli (find_points.c:3089-3095), the moduli of the three stages with the cost of an exact check (find_points.c:5027-5042) and the forbidden divisors (find_points.c:5043-5048); and the lines before the sieve (find_points.c:5111-5113).

\(\mathrm{maxDegree} = 100\), the largest degree of a polynomial that ratpoints accepts, the value of RATPOINTS_MAX_DEGREE (ratpoints.h:33-33): a list of coefficients has at most \(\mathrm{maxDegree} + 1 = 101\) entries. \(\mathrm{maxDivisors} = 512\), the value of MAX_DIVISORS (find_points.c:121-121): the loop over the denominators of a polynomial of odd degree runs over the divisors of its leading coefficient times squares only when there are fewer than this many divisors up to the largest denominator. An integer is a C long when it lies in \([-2^{63}, 2^{63})\) (rp-private.h:41-43): ratpoints needs a long of \(64\) bits, and the height bound is one.

The options of a search are those of the library that change the refusals, the order of the output or what is delivered, with the defaults of a run of the program without options: whether the set-up may reverse the polynomial, that is, whether the bit RATPOINTS_NO_REVERSE is clear (true by default); the depth args->sturm of the Sturm step, an integer, negative for none, by default \(\mathrm{defaultSturm} = 10\) (RATPOINTS_DEFAULT_STURM); the two options of the output \(\mathrm{noCheck}\) and \(\mathrm{noY}\), false by default, the bits RATPOINTS_NO_CHECK, under which every numerator that passes the sieve is delivered with \(y = 0\) without the exact check, and RATPOINTS_NO_Y, under which only the point with \(y \ge 0\) of a pair is delivered; and the search region: the search intervals, a list of pairs of doubles for the array domain with its length num_inter, empty by default, and the least and the largest denominator, integers for the longs b_low and b_high, by default \(1\) and \(0\) (main.c:348-348, main.c:352-352, ratpoints.h:403-405); the program sets b_high to \(H\), and the library takes a value below \(1\) as \(H\), so that the two defaults give the same search. The statements read the search intervals by the values of their ends, \(\mathrm{domainValues}\), and by their bits, \(\mathrm{domainBits}\).

The options of the sieve are the values of the options of the program that tune the sieve, which change neither the points nor their order: the number of primes examined (-p), the cut points of the stages (-n, -N), the parameters of the choice of the moduli and of its correction (-r -R -U -C -A -P -Q -W), the number of forbidden divisors (-F), the array size, and whether the Jacobi test runs (-j, -J), as the program reads them into ratpoints_args, \(-1\) for an absent option that takes a number (main.c:337-347, main.c:349-350, ratpoints.h:365-367).

The refusals are five, each with the error of the program: more than \(\mathrm{maxDegree} + 1\) coefficients (error 3), fewer than two (error 5), the height bound \(0\) or one of \(2^{63}\) or more, which is not a C long (error 4), a binary form that is not squarefree (error 8), and search intervals that are not well formed (error 9).

The outcome of a search that is not refused is what the library gives back to its caller: the data of the callback, the count, the three bits of the flags that the program reads after the search, RATPOINTS_REVERSED, RATPOINTS_USE_SQUARES and RATPOINTS_USE_SQUARES1, the search intervals as the search leaves them, and the numbers of the moduli used in the stages (ratpoints.h:377-383, ratpoints.h:414-414, ratpoints.h:416-417).

For the switch \(r\) of the reversal and the coefficient list \(c\) of degree \(d\), the polynomial that ratpoints searches and whether it is the reversed one, \(\mathrm{searchedPoly}(r, c)\), is the first of the following that applies:

1. (1)

   \(((c_d, c_{d-1}, \dots , c_0), \mathrm{true})\) if \(r\) is true, \(d\) is even and \(c_0 = 0\);

2. (2)

   \(((c_d, c_{d-1}, \dots , c_0), \mathrm{true})\) if \(r\) is true, \(d\) is even, \(c_d\) is a square and \(c_0\) is not a square;

3. (3)

   \(((0, c_d, c_{d-1}, \dots , c_1), \mathrm{true})\) if \(r\) is true, \(d\) is odd, \(|c_d| \ne 1\), \(c_0 = 0\) and \(|c_1| = 1\);

4. (4)

   \((c, \mathrm{false})\) otherwise.

A natural number \(n\) is factored by trial division when the product of its prime factors from \(1021\) on, with multiplicity, is below \(1021^2\), or none of its prime factors exceeds \(1021\). The squarefree divisors of \(n\) at most \(B\) in the order of binary counting: for the distinct prime factors \(p_1 {\lt} p_2 {\lt} \cdots \) of \(n\), the products of the sublists of \((p_1, p_2, \dots )\) in the order of List.sublists, \(1, p_1, p_2, p_1 p_2, p_3, p_1 p_3, \dots \), with \(p_1\) the lowest bit, those at most \(B\). The denominators of the search of \(c\) up to \(B\), for a bound \(m\) of the number of divisors: when \(d\) is odd, \(|c_d| \ne 1\), \(|c_d|\) is factored by trial division and has fewer than \(m\) squarefree divisors at most \(B\), the numbers \(e k^2 \le B\), divisor \(e\) by divisor in the order of binary counting and \(k = 1, 2, \dots \) for each; otherwise \(1, \dots , B\). The points with the denominator \(z\): for \(x = -H, \dots , H\) in turn, with \(y = \lfloor \sqrt{F_c(x, z)} \rfloor \) (\(0\) when \(F_c(x, z) {\lt} 0\)), those among \((x, y, z)\) and \((x, -y, z)\) that are normalized points of height at most \(H\), in this order, one triple when \(y = 0\); the denominator \(0\) gives the points at infinity. The points in the order of ratpoints, \(\mathrm{orderedPoints}(m, r, c, H, B)\): for \((c', \mathrm{rev}) = \mathrm{searchedPoly}(r, c)\), the points of \(c'\) with the denominator \(0\) and then with the denominators of the search of \(c'\) up to \(B\), in turn, each \((a, y, b)\) mapped to \((b, y, a)\) for \(a \ge 0\) and to \((-b, y, -a)\) for \(a {\lt} 0\) when \(\mathrm{rev}\) is set.

A class (rp-private.h:494-495) has a pattern, a stride exponent \(k\), a residue \(a_0\) and the position of its row of offsets. The class of a word \(w\) of the 2-adic information (find_points.c:1064-1081): for \(w = 0\) the stride \(1\) and the pattern \(0\); otherwise, for the lowest set bit \(a\) of \(w\), the largest \(k \le 6\) below \(\mathrm{numStrides}\) such that every set bit of \(w\) is \(\equiv a \bmod 2^k\), \(a_0 = a \bmod 2^k\), and the pattern whose bit \(t\) is bit \((a_0 + 2^k t) \bmod 64\) of \(w\) (find_points.c:1082-1094); with the classes the word den_bits of the classes whose word is not \(0\). The offsets (find_points.c:1142-1158): for each entry of an odd modulus \(p\) the inverses \(\mathrm{dinv}[k] = 2^{-k} \bmod p\) and \((2^k\, \mathrm{rbaLength})^{-1} \bmod p\), by halvings, and for each packing \((k, a_0)\) of a class with a nonzero pattern a row with the offset \(a_0\, (2^k\, \mathrm{rbaLength})^{-1} \bmod p\) plus the bias of \(p\), the least multiple of \(p\) from \(\mathrm{rowBias} = 2^{31}\) on (find_points.c:1164-1182). The residues \(b\, \mathrm{dinv}[k] \bmod p\) of a denominator for the moduli of the first two stages, in three branches by the size of \(b\) (find_points.c:3639-3679). The bits \(\lceil (\mathrm{low} - a_0)/2^k \rceil \) to \(\lfloor (\mathrm{high} - a_0)/2^k \rfloor \) of an interval of numerators, by arithmetic shifts of signed 64-bit words, in a plain form and in a form that splits each end into its multiple of \(2^k\) and its rest, which cannot overflow (find_points.c:3355-3370).

For a denominator \(b\), the height bound \(H\) and a list of sieve entries (Chapter 6): an array of \(2H + 1\) Booleans, entry \(i\) for the numerator \(a = i - H\), all true at the start, each and-ed in turn with the row of \(b\) in every entry at \(a\). Its contract: entry \(i\) is the survivor test Ratpoints.Sieve.survives at \(i - H\), the conjunction of the rows. The check of such an array takes the numerators whose entry is true, in increasing order, and tests and checks each as the brute-force reference does. Its contract: if entry \(i\) is \(\varphi (i - H)\) for a test \(\varphi \) of the numerators, the result is what the brute-force reference (Definition 2.14) finds over \(b\) and the numerators \(-H, \dots , H\) that pass \(\varphi \).

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}\).

The reciprocal of \(p\) is \(\mathrm{magic}(p) = \lfloor (2^{64} - 1)/p \rfloor + 1\). The high half \(\mathrm{mulHi}(a, b)\) of the 128-bit product of two words, which the C code takes from gcc’s __uint128_t (rp-private.h:404-408, rp-private.h:409-410), comes in the model from the four products of their 32-bit halves, no partial sum leaving a word. The remainder by the reciprocal \(m\), RP_MULMOD, is \(\mathrm{mulHi}(m u \bmod 2^{64}, p)\), and the quotient, RP_MULDIV, is \(\mathrm{mulHi}(u, m)\), the arguments cast to words as the macros cast them; the builds that compile no 128-bit product (no such type, or RP_MULMOD_DIVIDE or RP_NO_INT128 set) divide instead (rp-private.h:413-414, rp-private.h:415-416), with the same results wherever the multiplication is exact. The remainder of an integer \(a\), mod_mul, is the remainder \(r\) of \(|a|\), and \(p - r\) for negative \(a\) with \(r \ne 0\) (sift.c:243-247).

For the bits \(w {\lt} 2^{64}\) of an IEEE binary64 double, with the exponent field \(e = \lfloor w / 2^{52} \rfloor \bmod 2^{11}\), the fraction \(t = w \bmod 2^{52}\) and the sign \(\sigma = -1\) for \(w \ge 2^{63}\) and \(\sigma = 1\) otherwise: \(w\) is a NaN when \(e = 2047\) and \(t \ne 0\), and the value of the double is

so that both zeros have the value \(0\). The intervals of a list over the values are search intervals when each \([l, u]\) has \(l \le u\) and each upper end lies below the lower end of the next interval; a list of pairs of doubles, each given by its bits \(w\), is well formed when no end is a NaN and the values of the ends are search intervals. A rational number \(r\) lies in a list \(D\) of intervals over the values when \(l \le r \le u\) for some \([l, u] \in D\). A triple \((x, y, z)\) lies in the search region of the intervals \(D\) (over the values) and the range from \(b_{\mathrm{low}}\) to \(b_{\mathrm{high}}\) when

a point at infinity lies in every region, and \(x/z\) may lie anywhere when there are no intervals. The search region is the whole box of the height bound \(H\) when there are no intervals, \(b_{\mathrm{low}} \le 1\), and \(b_{\mathrm{high}} {\lt} 1\) or \(H \le b_{\mathrm{high}}\). The largest denominator of the search is \(b_{\mathrm{high}}\) when \(1 \le b_{\mathrm{high}} \le H\), and \(H\) otherwise.

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.

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).

A reference to an entry, for a pointer to it: a prime by itself, a prime power by its prime and its exponent, a product by the position of its modulus among the moduli. The store maps each reference to its table of rows, \(m\) rows for the modulus \(m\), each present or absent; publishing a row puts it into the table of a reference and leaves a store without that table as it is. The kinds of builder, for the pointer init (rp-private.h:497-498): the function of a prime below \(64\) from CODE_INIT_SIEVE1 and that of a prime above \(64\) from CODE_INIT_SIEVE2, which the primes of the table have (gen_init_sieve_h.c:48-62), and the builders of a prime power and of a product. A sieve entry holds the reference to its table of rows and the kind of its builder: for a prime or a prime power those of its one factor, for a product its own (Ratpoints.Sieve.SieveEntry.refInit).

The table of rows of a prime \(p\): its row of \(0\) that of Lemma 7.5, the other \(p - 1\) rows absent (find_points.c:1820-1821). The tables of rows of a sieve entry, each made only when its reference is absent: that of each factor, and for a product its own (find_points.c:2427-2427, find_points.c:2471-2471). The row of a residue \(b\) of a sieve entry read or built: the row in its table when it is there, and otherwise the row that its builder builds into it. The sieve specs of a denominator, as set_rows makes them (find_points.c:3149-3170): for each entry of the first two stages its modulus, the offset of the row of the class and its row at its residue of \(b\), absent when it is not built, with the end \(p\). The missing rows of a denominator: each sieve spec of the first two stages without a row gets the row read or built of its entry at its residue (find_points.c:3522-3554).

For the options of a search (Definition 2.11) and the height bound \(H \ge 1\), the normalized options: the least denominator \(1\) for one below \(1\); the largest denominator \(H\) for one below \(1\) or above \(H\); the depth of the Sturm step capped at \(\mathrm{DBL\_ MANT\_ DIG} + 2 = 55\), beyond which the ends of the intervals of the step would not all be doubles; and the switch of the reversal turned off, for the private bit RATPOINTS_NO_REVERSE_AUTO, when the caller gives search intervals or the normalized range is not \(1, \dots , H\) (find_points.c:4659-4661, find_points.c:4678-4689). The search intervals of a search: for none given, the default interval \([-h, h]\), where \(h\) is the double of \(H\), moved up to the next double when \(h {\lt} 2^{63}\) and the long of \(h\) is below \(H\); otherwise the caller’s intervals, or none, for RATPOINTS_BAD_ARGS, when an interval has not \(l \le u\) or does not begin above the end of the one before it, compared as doubles, so that a NaN end is refused too (find_points.c:4831-4855).

For the coefficient list \(c\) of its degree, \(H\), the denominators from \(b_{\mathrm{low}}\) to \(b_{\mathrm{high}}\), intervals \(D\) of values, a test \(S(b, a)\) of the numerators \(a\) over the denominators \(b\), and the flags of the check: the points at infinity with the flags (Definition 4.9), followed, for the denominators \(b\) of the search from \(b_{\mathrm{low}}\) to \(b_{\mathrm{high}}\) in the order of its loop (Definition 8.10), by the points with the flags (Definition 10.3) of the numerators \(a = -H, \dots , H\) with \(a/b\) in one of the intervals of \(D\) and \(S(b, a)\). The test is sound when, over each denominator \(b\) of the search, it holds for every numerator \(a \in [-H, H]\) over which the brute-force reference finds a point \((a, y, b)\).

For the polynomial that the set-up hands on, with the flags of the check (the flag of the reversal and the two options of the output), the range of the denominators and the intervals that the Sturm step leaves, with its flag sturm_empty, the search sets up the tests on the denominators (find_points.c:4900-4914) and the 2-adic information, and returns with nothing delivered when no class modulo \(64\) admits a numerator and there is no point at infinity (find_points.c:4954-4959); it tests whether the coefficients are all longs, (Definition 2.12; find_points.c:4814-4823), which chooses how the tables reduce them modulo a prime; it chooses the moduli (Definition 6.7), with nothing delivered when the curve has no points modulo a prime (find_points.c:4996-5006); it delivers the points at infinity (Definition 4.9) and returns when the callback has stopped the search or the Sturm step has left no interval (find_points.c:5100-5103, find_points.c:5105-5106); otherwise it runs over the blocks of the denominators of the shape of the loop (Definition 8.10) with the correction of the moduli (Definition 6.11, find_points.c:5137-5139). Each point is mapped back to the caller’s curve when the flag of the reversal is set (Definition 4.4). The outcome has the bits of the flags, the search intervals that the Sturm step leaves (those that this search is given), and the numbers of the moduli of the last block that the run sifts (find_points.c:5210-5213), \(0\) after a return before the sieve.

A definition of the proofs, not of the model: for the polynomial \(c\) of degree \(d\) that the reversal check hands on, \(H\) and the options, none when the search intervals are none or the Sturm step of the search refuses or returns at once; no interval when it sets sturm_empty; and otherwise the values of the intervals that it leaves. For well-formed intervals of the caller:

1. (1)

   every \(x\) in the region lies in the caller’s intervals, or the caller gives none;

2. (2)

   if the chain does not fail when the step is on, the region is none only for an even \(d\) whose leading coefficient is not a square;

3. (3)

   assuming Sturm’s theorem when the step is on, for \(0 {\lt} d {\lt} 2^{57}\) the degree of \(c\), \(1 \le H {\lt} 2^{63}\) and a chain that does not fail when the step is on: every \(a/b\) with \(b {\gt} 0\), \(|a| \le H\) and \(F(a, b) \ge 0\) in the caller’s intervals, or anywhere when there are none, lies in the region, which is not none.

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).

For odd \(d\) and \(|c_d| \ne 1\), as setup_us1 computes them: the factorization of \(|c_d|\) by trial division over the primes of the table, a cofactor below the square of the next prime taken as a prime (find_points.c:777-860); the squarefree divisors at most \(b_{\mathrm{high}}\) by a doubling loop, at most \(\mathrm{maxDivisors} = 512\) of them (find_points.c:864-880); and for each prime \(p\) of \(c_d\) a record of \(p\), \(v_p(c_d)\) and the slope, the least \(n \ge 1\) with \((d - k)\, n {\gt} v_p(c_d) - v_p(c_k)\) for all \(k {\lt} d\) (find_points.c:894-912). The records and the divisors are returned exactly when the factorization ends with the cofactor \(1\) and there are fewer than \(\mathrm{maxDivisors}\) divisors (find_points.c:914-935). The contracts say so, and: for \(c_d \ne 0\) the factorization ends with the cofactor \(1\) exactly when ratpoints factors \(|c_d|\) completely in the sense of the specification (\(\mathrm{FactorsByTrialDivision}\), Definition 2.9), and then lists the primes of \(|c_d|\) in increasing order with their valuations; the slope satisfies \(n \ge 1\) and \(1 + v_p(c_d) - v_p(c_k) \le (d - k)\, n\) for all \(k {\lt} d\), where \(v_p(0) = \mathrm{veryBig}\); for \(c_d \ne 0\) and \(b_{\mathrm{high}} \ge 1\) the set-up returns divisors exactly when \(|c_d|\) is factored completely and has fewer than \(\mathrm{maxDivisors}\) squarefree divisors at most \(b_{\mathrm{high}}\), and these are then \(\mathrm{binaryDivisors}(|c_d|, b_{\mathrm{high}})\), in its order.

The four shapes with their data (find_points.c:3725-3728, find_points.c:3736-3749), which run_setup chooses from the flags and returns with the bounds of the search intervals (find_points.c:3778-3806), and their denominators from \(b_{\mathrm{low}}\) to \(b_{\mathrm{high}}\) in the order of the loop, each with its test of a single denominator:

1. (1)

   under the flag of the squares, the squares \(k^2\) for \(\lceil \sqrt{b_{\mathrm{low}}}\, \rceil \le k \le \lfloor \sqrt{b_{\mathrm{high}}}\, \rfloor \), with the class test;

2. (2)

   otherwise, when the set-up has returned the records and the divisors of Definition 8.4, the divisors times squares: for each divisor \(s\) in turn, the \(s k^2\) of the range in increasing order of \(k\), with the class test and the valuation test, which \(b\) fails when the record of a prime excludes it (find_points.c:3944-3953);

3. (3)

   otherwise, under the flag of the checked loop, the words, with the forbidden divisors, the switch of the Jacobi test, its tables when the test is on and they exist, and \(c_d\): word by word, the \(64 w + j\) of the range for the set bits \(j\), lowest first, of \(\mathrm{den\_ bits}\) and-ed with word \(w \bmod p\) of each forbidden divisor \(p\) with words, tested by the tables, then by the forbidden divisors with masks, and, with the Jacobi test on and no tables, by the binary algorithm (find_points.c:4013-4041);

4. (4)

   otherwise every denominator, \(b_{\mathrm{low}}, \dots , b_{\mathrm{high}}\), with the class test.

The class test is that the pattern of the class of \(b \bmod 64\) is not \(0\). The lists of the denominators of the shapes (Ratpoints.Sieve.Shape.dens) and the choice of the test of a single denominator (Ratpoints.Sieve.Shape.keep) are definitions of the proofs, the reference of the loops over the blocks, which test and sift each denominator as they reach it, as run_block does; the tests themselves model the C code. The denominators of the search (Ratpoints.searchDens) are those of the divisors times squares when \(d\) is odd, \(|c_d| \ne 1\) and the set-up for \(b_{\mathrm{high}}\) returns divisors, and \(b_{\mathrm{low}}, \dots , b_{\mathrm{high}}\) otherwise.

The tables of a prime power \(q = p^e\) are the bit arrays fsq, bit \(x {\lt} q\) set when \(f(x)\) is a square modulo \(q\), and gsq, bit \(t\) set when \(p \mid t\) and \(\tilde f(t)\) is a square modulo \(q\), with the inverses of the units (rp-private.h:531-534). Its row of \(b\) admits \(a\), for \(r = b \bmod q\) and \(x = a \bmod q\), when bit \(x r^{-1}\) of fsq is set if \(p \nmid r\), and when \(p \nmid x\) and bit \(r x^{-1}\) of gsq is set if \(p \mid r\). A factor is a prime with its table or a prime power with its tables. The sieve entry of a modulus \(m\) holds its factors, the reciprocal of \(m\), with which the sieve reduces, the fields of the packing (Chapter 9), the reference to its table of rows and the kind of its builder (Chapter 7), its density, and the count of its factors, \(0\) for a prime, \(1\) for a prime power and their number for a product (rp-private.h:542-555). Its row of \(b\) admits \(a\) when the row of every factor admits \(a \bmod m\) at \(b \bmod m\); a numerator survives a list of entries for \(b\) when the row of \(b\) of every entry admits it, the interface between the sieve and the check.

One piece (sift.c:498-531): the test small, a fresh array with room for the sentinel, the first stage with the first \(s_1\) moduli in the arm that \(1 {\lt} \mathrm{chunk} \le 16\) chooses, the masks of the ends (sift.c:1030-1041) and the scan with the moduli of the second stage. The bits from \(\mathrm{low}\) to \(\mathrm{high}\) of an interval (find_points.c:3563-3612): the word numbers from \(\lfloor \mathrm{low}/\mathrm{rbaLength} \rfloor \) to \(\lfloor \mathrm{high}/\mathrm{rbaLength} \rfloor \) in pieces of at most \(A\) bit arrays, the first and the last masked. One denominator (find_points.c:3442-3488): for each search interval the bits of its numerators within the height bound (Chapter 5); at the first interval that the height bound does not rule out (also one without numerators) the sieve specs (Definition 7.8), the modulus, the offset of the row of the class and the row of the residue of \(b\) for the stride of each entry of the first two stages, the missing rows built into their tables (Chapter 7); then the bits of the interval in pieces. Each returns when the callback stops the search. The contract of one denominator: for \(A \ge 1\), \(0 {\lt} b {\lt} 2^{63}\), \(H {\lt} 2^{63}\), prime entries in the third stage, the reciprocals of all the entries, the residues \(b\, \mathrm{dinv}[k] \bmod p\) of the entries of the first two stages, whose tables of inverses invert, tables of rows that fit them, and a delivery whose flag is clear: for every word \(w\) that the class packs, a row of offsets packed for the class, and the ranges of the numerators that the bounds of the search intervals give at \(b\), the delivery is that of the points of the check with the flags of the numerators \(-H, \dots , H\) that lie in a range, pass \(w\) and survive the entries of all three stages, in increasing order; when the callback does not stop the search, the counters of the sieve grow by a closed form that depends neither on the callback and the flags nor on the tables of rows; and the tables of rows afterwards fit the entries again.

The proposition that for every squarefree real polynomial \(p\) and all reals \(a \le b\)

where \(V_p(t)\) is the number of sign changes (List.signVariations) of the values at \(t\) of the Sturm sequence of \(p\) and its derivative (Polynomial.sturmSeq p (derivative p)), and the number of roots is Set.ncard.

The primes of the sieve are the odd primes below \(1024\) in increasing order (primes.h:29-40), which decide checks; ratpoints chooses its moduli among the \(\mathrm{numPrimes}\) of them below \(2^{\mathrm{maxBitsInPrime}}\), the \(53\) primes up to \(251\) for the \(8\) bits of the default build, whose Makefile passes PRIME_SIZE \(= 8\) in place of the header’s own default \(7\) (rp-private.h:321-323, rp-private.h:325-361). The table of a prime \(p\) has \(p + 1\) entries: entry \(x {\lt} p\) says whether \(f(x)\) is a square modulo \(p\), and entry \(p\) whether there are points at infinity modulo \(p\), that is, whether \(d\) is odd or \(c_d\) is a square modulo \(p\); it is kept with \(p\) and the inverses modulo \(p\) (rp-private.h:542-555). The row of the denominator \(b\) admits the numerator \(a\) when, for \(r = b \bmod p\) and \(x = a \bmod p\), the entry at \(x r^{-1} \bmod p\) is true if \(r \ne 0\), and \(x \ne 0\) if \(r = 0\). This admission test is what the bit of \(a\) in the row of \(r\) says in ratpoints.

The loop of sieving_info over the primes of the table while fewer than the number to look at, the normalized value of -p, have been looked at (find_points.c:2601-2605). The examination of a prime (find_points.c:2606-2626) gives its table, the coefficients modulo \(p\), its density (the share of the numerators that its rows let through) and a code: \(-1\), the exit, when the curve has no points modulo \(p\) (Chapter 4); \(0\) when the prime says nothing; \(2\) when it says only that numerator and denominator are coprime; \(1\) otherwise. A prime that says something becomes a candidate with its key for the first stage, and its table of rows goes into the store; while fewer than their bound have been found, the coefficients modulo \(p\) give the forbidden divisor of \(p\) (Chapter 8). When the caller left the number of primes to the library, the loop looks at one more prime, at most \(\mathrm{numPrimes}\) in all, while the first two stages would be short of candidates that say more than coprimality (find_points.c:2694-2705).

The contract: for options that look at no more than \(\mathrm{numPrimes}\) primes, an exit means that the curve has no points of any height; otherwise at most \(\mathrm{numPrimes}\) primes are to be looked at, each table that the loop keeps, that of a prime that says something, is that of Definition 6.1 for one of the first \(\mathrm{numPrimes}\) primes, every candidate is a prime of the table with the sieve entry of its table, the forbidden divisors are sound, and the store holds the tables of rows of the primes.

The words \(\mathrm{fsq}\) and \(\mathrm{gsq}\), by Horner’s rule on \(64\)-bit words (find_points.c:1006-1014, find_points.c:1015-1021): bit \(k\) of \(\mathrm{fsq}\) is set exactly when \(k {\lt} 64\) and \(\sum _{i \le d} c_i k^i\) is a square in \(\mathbb {Z}/64\), bit \(t\) of \(\mathrm{gsq}\) exactly when \(t {\lt} 64\) is even and \(\sum _{i \le d} c_i t^{D - i}\) is a square in \(\mathbb {Z}/64\). The words \(\mathrm{nb}[b]\) for \(b {\lt} 64\), scattered from these (find_points.c:983-994, find_points.c:1023-1050): bit \(a\) of \(\mathrm{nb}[b]\) is set exactly when \(b\) is odd and \(a = k b \bmod 64\) for a set bit \(k\) of \(\mathrm{fsq}\), or \(a {\lt} 64\) is odd and \(b = t a \bmod 64\) for a set bit \(t\) of \(\mathrm{gsq}\). And \(\mathrm{den\_ bits}\), with bit \(b\) set exactly when \(\mathrm{nb}[b] \ne 0\). These descriptions are the contracts.

The valuation \(v\) of an integer \(n \ne 0\) at \(p\) with the unit part \((|n| / p^v) \bmod p\), by repeated division with remainder, and \((\mathrm{veryBig}, 0)\) for \(n = 0\), with \(\mathrm{veryBig} = 1000\) (find_points.c:422-422): one function for valuation on GMP integers and valuation1 on longs (find_points.c:424-454). The contract: for \(p {\gt} 1\) the loop ends, and for \(n \ne 0\), \(v\) is the \(p\)-adic valuation of \(|n|\) and the unit part is not \(0\).

The plan of the blocks is well formed, with blocks of at least one step, and the denominators of the blocks, concatenated in order, are those of the shape from \(b_{\mathrm{low}}\) to \(b_{\mathrm{high}}\) in the order of its loop. When the first decision is for block \(0\), the decision found for block \(i\) is the one in force. Let the callback not have stopped the search, the pieces have at least one bit array, the sieve entries be fit for the run (of the shape that the third stage needs where they count no factor, with the tables of inverses of their factors, their reciprocals in order and the row offsets of the classes; soundness is not needed here), the word of the classes have bit \(j\) set exactly when class \(j\) admits a numerator, the decision in force be well formed, the forbidden divisors be as the shape of the words needs them, \(i\) be below the number of the blocks, \(1 \le b_{\mathrm{low}}\), \(b_{\mathrm{high}} {\lt} 2^{63}\), \(H {\lt} 2^{63}\), and the store fit all the entries. Then block \(i\) keeps the store so and delivers, in order, over the denominators of its steps that pass the tests of the shape, the points that the exact check finds among the numerators that survive the first \(s_3\) entries of its decision, for every choice of the words of the classes and the ranges of the numerators that the packing and the bounds give; and when the callback has not stopped the search within it, its report is a closed form in the arguments of the run, which reads neither the callback nor the flags of the output.

For words \(m {\gt} -2^{63}\) and \(n {\gt} 0\) the test for common factors gives whether \(\gcd (m, n) = 1\). A prime entry is a sieve entry whose single factor is a table of the kind of a prime, of a modulus \(1 {\lt} p \le 2^{32}\) (\(p\) need not be prime), whose table of inverses holds a value in \([1, p - 1]\) at each nonzero residue below \(p\) (that these are inverses is not needed), and whose modulus and reciprocal are those of \(p\). For prime entries, \(\gcd (a, b) = 1\) and \(|a| \le H\), the third stage lets \(a\) through exactly when the rows of \(b\) in all the entries admit \(a\). For \(0 {\lt} b {\lt} 2^{63}\) and \(|a| {\lt} 2^{63}\) the test of a candidate is \(\gcd (a, b) = 1\) followed by the third stage. So for prime entries in the third stage with their reciprocals, \(0 {\lt} b {\lt} 2^{63}\) and \(|a| \le H {\lt} 2^{63}\), the points that the extraction delivers for \(a\) are those of the check with the flags (Ratpoints.Sieve.checkNumWith, the points of the exact check if \(\gcd (a, b) = 1\)) when the rows of the third stage admit \(a\), and none otherwise.

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.

On a delivery whose flag is clear, the exact check of a numerator delivers its list of Definition 10.3, as the points at infinity deliver theirs (Definition 4.9): the second call of a pair, left out after a first call that stops the search, is the part of the delivery that a set flag passes over. Without \(\mathrm{noCheck}\), the points of a numerator with the flags are those of the check of the reference (Ratpoints.Sieve.checkNum), which tests \(\gcd (a, b) = 1\) and the square as the brute-force reference does, mapped after a reversal, without those with \(y {\lt} 0\) under \(\mathrm{noY}\); under \(\mathrm{noCheck}\) they are the survivor \((a, 0, b)\), mapped after a reversal, when \(\gcd (a, b) = 1\), and nothing otherwise. With the exact check on and \(\mathrm{noY}\) set, the points of a numerator with \(y\) replaced by \(0\) form a sublist of its points under \(\mathrm{noCheck}\), with the same flag of the reversal and either setting of \(\mathrm{noY}\), and the points at infinity with \(y\) replaced by \(0\) are those under \(\mathrm{noCheck}\).

For options that look at no more than \(\mathrm{numPrimes}\) primes, the checked loop only for even degree, and any values of the doubles: an exit of the choice means that the curve has no points of any height; otherwise the result is what the run needs:

1. (1)

   every sieve entry is sound (Lemma 6.4), with the tables of inverses of its factors and the fields that the packing reads;

2. (2)

   every entry that counts no factor has a single factor, a table of its modulus \(1 {\lt} p \le 2^{32}\) whose table of inverses gives every nonzero residue below \(p\) a nonzero residue below \(p\), and the reciprocal of \(p\): the shape that the third stage of the sieve needs;

3. (3)

   the reciprocals are those of the moduli of the entries, in their order, and the store fits all the entries, the reserve included;

4. (4)

   the first decision, the ends \(s_2\) and \(s_3\) from block \(0\) on, is well formed: \(s_1 \le s_2 \le s_3 \le \) the number of the entries, and every entry from \(s_2\) on counts no factor;

5. (5)

   the forbidden divisors are sound (Chapter 8), and the checked loop is on only for even degree.

strtod never gives a NaN, and when it gives a finite double other than zero for a word that is not an infinity, the exact value of the word lies below the next double above it: half of a faithful rounding, the half that the lower ends need. outward moves a double to the side of the end that its direction asks, and onto the largest double at most a lower end when it starts from a double whose next double lies above the end; so for an argument of fewer than \(2^{56}\) characters the double that scan_end gives for a lower end is the largest double at most the end (for an upper end the proofs show only that it is at least the end). The binary search of in_region decides whether \(a/b\) lies in increasing and disjoint exact intervals. For intervals without a NaN, join_intervals gives no interval exactly when it is given none, and intervals without a NaN that hold every number that the given ones hold; when moreover each lower end is at most its upper end and the lower ends increase from the second on, its intervals are increasing and strictly apart, search intervals in the sense of the specification (Definition 2.6).

The closed form of the row of a residue \(r\) modulo \(m\), for an admission test \(\mathrm{adm}\), which says whether the row of \(r\) admits a number \(N\), is the array of \((m + \mathrm{chunk} - 1)\, \mathrm{rbaPack}\) words whose word \(j\) has bit \(t\) set exactly when \(t {\lt} 64\) and \(\mathrm{adm}(r)\) admits \(64 j + t\). With the admission test of a sieve entry, of the table of a prime or of the tables of a prime power, it is the row that ratpoints builds; it has no C code of its own. Then:

1. (1)

   bit \(t\) of word \(j {\lt} (m + \mathrm{chunk} - 1)\, \mathrm{rbaPack}\) is \(t {\lt} 64\) and \(\mathrm{adm}(r)(64 j + t)\);

2. (2)

   for \(m {\gt} 0\) and a test that does not change when a multiple of \(m\) is added to the number, word \(j\) is word \(j \bmod m\, \mathrm{rbaPack}\), so that the closed form of a row of a sieve entry of positive modulus repeats its first \(m\) bit arrays after them;

3. (3)

   a word holds \(n \le 64\) bits of a pattern \(g\) of period \(m\) from \(s\) on when its bit \(t {\lt} n\) is \(g((s + t) \bmod m)\) and its other bits are clear; if \(g(N \bmod m) = \mathrm{adm}(r)(N)\) for every \(N\), an array of \((m + \mathrm{chunk} - 1)\, \mathrm{rbaPack}\) words whose word \(j\) holds the 64 bits of \(g\) from \(64 j\) on is the closed form; the contracts of the builders conclude by this.

For any values of the doubles: when the latest decision and the decision with \(s_3 = s_2\) for the end \(s_2\) under which the counters of the run were counted are well formed, so is the decision that the correction makes. A state of the correction is well formed when its first decision is for block \(0\) and its decisions, the latest one and the one for the end of the counters are well formed; the fold of a block whose decision is one of the state keeps it so, adds one block folded and appends decisions only for the blocks from \(\mathrm{folded} + \mathrm{adaptLag} + 1\) on. The state after the folds of the first \(k\) blocks, each with its report in closed form (Lemma 6.10), and the decision of each block are functions of the arguments of the run that read neither the callback nor the flags of the output, well formed when the decision of the choice is.

The delivery of \(L_1 \mathbin {+\! \! +} L_2\) is the delivery of \(L_2\) after that of \(L_1\). A delivery whose flag is set stays as it is, whatever the list; so if the delivery of a prefix \(M\) of \(L\) sets the flag, the delivery of \(L\) is that of \(M\), and a test of the flag after the delivery of \(L_1\), followed by the delivery of \(L_2\) when the flag is clear, is the delivery of \(L_1 \mathbin {+\! \! +} L_2\). With the appending callback, from a delivery whose flag is clear, the array grows by \(L\) and the count by the length of \(L\). For every list \(L\) there is a prefix \(M\) of \(L\) whose delivery is that of \(L\), such that the flag is clear before each point of \(M\), so that each of them gets its call, and the delivery of \(M\) sets the flag unless \(M = L\).

Write \(v(x)\) for the value of the bits of a double \(x\) (Definition 2.6).

1. (1)

   On doubles that are not NaNs, <, <= and == are the order and the equality of the values; the value of a finite double is its exact value.

2. (2)

   The double nearest to \(\pm m\, 2^k\) is exact for \(0 {\lt} m {\lt} 2^{53}\), \(k \ge -1074\) and \(m\, 2^k {\lt} 2^{1024}\), and (double)n for \(|n| \le 2^{53}\); for a finite \(x \ne 0\), frexp writes \(x\) as \(g\, 2^e\) with \(1/2 \le |g| {\lt} 1\), and ldexp(x, n) is \(x\, 2^n\) when \(2^{-1022} \le |x|\, 2^n {\lt} 2^{1023}\); and a double \(0 \le x {\lt} 2^{63}\) converts to the long \(\lfloor x \rfloor \), one \(0 \le x {\lt} 2^{64}\) to the unsigned long \(\lfloor x \rfloor \).

3. (3)

   The next double above \(x\), not a NaN or \(+\infty \), is at most every double above \(x\); dually below.

4. (4)

   The roundings of \(\pm n/d\) and of \(\pm m\, 2^k\) are never a NaN, and for \(n, m \ne 0\) a finite result is a faithful rounding: the value lies strictly between the values of its two neighbours.

5. (5)

   For \(1 \le H {\lt} 2^{63}\), the double \(h\) of \(H\), moved up to the next double when \(h {\lt} 2^{63}\) and the long of \(h\) is below \(H\), is finite and \(H \le v(h)\).

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.

Let \(\mathrm{findPoints}(c, H, s, o)\) return the list \(L\), let \(c'\) and \(\mathrm{rev}\) be the list and the flag that the reversal check of the normalized options hands on, and let the normalized range of the denominators run from \(b'_{\mathrm{low}}\) to \(b'_{\mathrm{high}}\).

1. (1)

   The predicate Ratpoints.IsSearchedPoly of what a successful search guarantees after its refusals (Lemma 4.2) holds for \(c'\) and \(\mathrm{rev}\), and there is a sound test \(S\) over that range such that \(L\) is the list of the search of \(c'\) for \(S\) and the region that the search uses (Definition 5.11), with the flag \(\mathrm{rev}\) and the options of the output of \(o\), or the empty list when that region is none; for every choice of the two options of the output, with the other options unchanged, \(\mathrm{findPoints}\) returns the list for the same \(S\) and region with that choice.

2. (2)

   With the exact check on, \(L\) is what the brute-force reference of \(c'\) finds over the candidate \((1, 0)\) and over the denominators of its search from \(b'_{\mathrm{low}}\) to \(b'_{\mathrm{high}}\) with the numerators in the region that the search uses, mapped back after a reversal, without the points with \(y {\lt} 0\) under \(\mathrm{noY}\).

3. (3)

   If moreover \(h_S\) holds, \(L\) is what the reference of \(c'\) finds over the candidate \((1, 0)\) and over the denominators of its search from \(1\) to \(b'_{\mathrm{high}}\) with all the numerators \(-H, \dots , H\), mapped back after a reversal, without the points with \(y {\lt} 0\) under \(\mathrm{noY}\) and those outside the search region of \(o\).

Let \(d\) be even, \(a\) and \(y\) integers and \(b\) a natural number with \(\gcd (a, b) = 1\) and \(y^2 = F(a, b)\). For every prime \(p\) and every \(b_{\mathrm{high}}\), bit \(v_p(b)\) of the mask of the forbidden valuations at \(p\) is clear. An admissible forbidden divisor with words has the words of Ratpoints.Sieve.forbiddenRow, and for \(1 \le b \le b_{\mathrm{high}}\) its prime does not divide \(b\); and for \(b \ge 1\) no admissible forbidden divisor with a mask excludes \(b\).

Barrett’s reduction of \(u\) modulo \(p\) with the reciprocal \(m\) is \(r = u - \lfloor u m / 2^{64} \rfloor \, p\), and \(r - p\) when \(r \ge p\) (find_points.c:1639-1650); the value of \(f\) at \(a\) modulo \(p\) is Horner’s rule from \(c_d\) on the coefficients reduced modulo \(p\), with Barrett’s reduction at the end and, for \(d {\gt} \mathrm{hornerSteps}\), after every \(\mathrm{hornerSteps}\) steps (find_points.c:1726-1731, find_points.c:1737-1744); the table is made of these values and handed back with the coefficients modulo \(p\), or none, the exit, when no entry of it is true (find_points.c:1683-1697). Then:

1. (1)

   for \(p {\gt} 0\) and \(u {\lt} 2^{64}\), Barrett’s reduction with \(m = \lfloor (2^{64} - 1)/p \rfloor \) gives \(u \bmod p\);

2. (2)

   for \(p {\lt} \mathrm{maxPrimeEven}\), \(a {\lt} p\) and coefficients below \(p\), the schedule gives \(f(a) \bmod p\), and the accumulator stays below \(p^{\mathrm{hornerSteps} + 1} {\lt} 2^{64}\);

3. (3)

   for \(0 {\lt} p {\lt} \mathrm{maxPrimeEven}\) the computed entry, the prime with its table and its inverses, is that of Definition 6.1, with the coefficients modulo \(p\), or none exactly when no entry of that table is true.

When the tables of \(\ell \) for \(b_{\mathrm{high}}\) exist, the test by tables passes \(1 \le b \le b_{\mathrm{high}}\) exactly when \(J(\ell \mid b^*) = 1\). Let \(d\) be even, \(a\) and \(y\) integers and \(b\) a natural number with \(\gcd (a, b) = 1\) and \(y^2 = F(a, b)\). Then \(J(c_d \mid b^*) = 1\) for the largest divisor \(b^*\) of \(b\) prime to \(2 c_d\); so for \(b \ge 1\) the binary algorithm gives \(1\) on \(b\) and \(c_d\), and the test by tables of \(c_d\) for \(b_{\mathrm{high}} \ge b\), when they exist, passes \(b\).

The tables of \(m = p^e\) as examine_power makes them from the coefficients reduced modulo \(m\) (find_points.c:2267-2282), in bit arrays of \(\mathrm{modWords} = \lceil \mathrm{maxPrimeEven}/64 \rceil \) words, bit \(x\) in bit \(x \bmod 64\) of word \(\lfloor x/64 \rfloor \) (rp-private.h:523-523): the bits of the squares \(x^2 \bmod m\), \(x {\lt} m\), set in a bit array sq (find_points.c:2283-2284); the bits of fsq and gsq set where the values of \(f\) and of the reversed polynomial, by Horner’s rule, are marked in sq; and the inverses by the extended Euclidean algorithm modinv (find_points.c:2241-2252), \(0\) for the residues divisible by \(p\) (find_points.c:2302-2303). Then:

1. (1)

   for \(1 {\lt} m\) and \(x\) prime to \(m\), modinv gives the inverse of \(x\) modulo \(m\) in \([0, m)\); for a prime \(p\) and \(e \ge 1\), every entry of the inverses is below \(p^e\), and the entry of a unit \(x {\lt} p^e\) is its inverse;

2. (2)

   \(\mathrm{maxPrimeEven} \le 64\, \mathrm{modWords}\), and for \(m \le 64\, \mathrm{modWords}\) a bit array of \(\mathrm{modWords}\) words gets the bit of every square modulo \(m\) set;

3. (3)

   for a prime \(p\), \(e \ge 1\) and \(p^e \le 64\, \mathrm{modWords}\), the tables of \(p^e\) have these inverses, bit \(x {\lt} p^e\) of fsq set whenever \(f(x)\) is a square modulo \(p^e\), and bit \(t {\lt} p^e\) of gsq, for \(p \mid t\), set whenever the reversed polynomial of the even degree \(D = 2 \lceil d/2 \rceil \) takes a square value at \(t\); only this direction is needed, since a further bit loses no point.

The range of the numerators of \(b\) in an interval \([l, u]\) over the values runs from \(\lceil b l \rceil \), clamped to \(-H, \dots , H + 1\), to \(\lfloor b u \rfloor \), clamped to \(-H - 1, \dots , H\), an infinite end going to the end of its clamp.

1. (1)

   For \(b {\gt} 0\) and \(|a| \le H\), \(a\) lies in one of the ranges of the intervals of \(D\) exactly when \(a/b\) lies in one of the intervals. For intervals with \(l \le u\) each range has \(\mathit{lo} \le \mathit{hi} + 1\), and for search intervals (Definition 2.6) each range ends below the start of the next.

2. (2)

   For a double \(x\) that is not a NaN, \(1 \le b {\lt} 2^{63}\) and \(H {\lt} 2^{63}\), the end made of \(x\), at either side, gives the same clamped numerators as \(x\); and for \(H {\lt} 2^{63}\) and \(1 \le b \le b_{\mathrm{high}} \le H\) the bounds of an interval represent the range of the ends made of its doubles, on both paths of interval_bits.

3. (3)

   So, for well-formed intervals, \(H {\lt} 2^{63}\), \(b_{\mathrm{high}} \le H\) and \(0 {\lt} b \le b_{\mathrm{high}}\), the bounds of the run give at \(b\) the ranges of the values of the intervals (Definition 5.5).

Let \(d\) be odd, \(a\) and \(y\) integers and \(b\) a natural number with \(\gcd (a, b) = 1\) and \(y^2 = F(a, b)\).

1. (1)

   If \(|c_d| = 1\), then \(b\) is a square.

2. (2)

   \(b = s k^2\) for a squarefree \(s\) that divides \(c_d\).

3. (3)

   If \(p\) is a prime with \(v_p(b) \ge 1\) and \(v_p(c_d) + 1 \le v_p(c_k) + (d - k)\, v_p(b)\) for every \(k {\lt} d\) with \(c_k \ne 0\), then \(v_p(c_d) + v_p(b)\) is even. So for \(b \ge 1\) the record of any prime \(p\) with its slope does not exclude \(b\), where a record excludes \(b\) when \(v_p(b)\) is at least the slope and \(v_p(b) + v_p(c_d)\) is odd.

When the set-up returns divisors, for \(c_d \ne 0\) and \(b_{\mathrm{high}} \ge 1\), they are the squarefree divisors of \(c_d\) at most \(b_{\mathrm{high}}\), each once.

1. (1)

   The class of \(w\) packs \(w\): it is well formed (\(k \le 6\), \(k {\lt} \mathrm{numStrides}\), \(a_0 {\lt} 2^k\)), every set bit of \(w\) is \(\equiv a_0 \bmod 2^k\), and bit \(t\) of its pattern is bit \((a_0 + 2^k t) \bmod 64\) of \(w\); bit \(j\) of den_bits is set exactly when \(j {\lt} 64\) and the word of \(j\) is not \(0\).

2. (2)

   For entries of odd moduli \(1 {\lt} p \le \mathrm{maxPrimeEven}\) with their reciprocals, the inverse of \(\mathrm{rbaLength}\) and a bias in \(p\mathbb {Z}\cap [\mathrm{rowBias}, \mathrm{rowBias} + p)\), well-formed classes and an array large enough, every class with a nonzero pattern gets a row whose offset \(o\) for each entry is packed for it: \(\mathrm{rowBias} \le o {\lt} \mathrm{rowBias} + 2p\), \(o\, 2^k\, \mathrm{rbaLength} \equiv a_0 \bmod p\) and \(\mathrm{dinv}[k]\, 2^k \equiv 1 \bmod p\) with \(\mathrm{dinv}[k] {\lt} p\); nothing else changes.

3. (3)

   For entries with \(0 {\lt} p \le \mathrm{maxPrimeEven}\), their reciprocals and \(\mathrm{dinv}[k] {\lt} p\), the residues of a denominator are \(b\, \mathrm{dinv}[k] \bmod p\).

4. (4)

   For a well-formed class the split form gives the bits \(-\lfloor (a_0 - \mathrm{low})/2^k \rfloor \) and \(\lfloor (\mathrm{high} - a_0)/2^k \rfloor \), and so does the plain form when \(a_0 - \mathrm{low} {\lt} 2^{63}\) and \(\mathrm{high} - a_0 \ge -2^{63}\).

5. (5)

   If the tables of inverses of the factors of an entry invert their units and \(v u \equiv 1 \bmod p\), the row of \(u b\) admits \(u a\) exactly when the row of \(b\) admits \(a\); so the closed form of the row of \(b'\) with \(2^k b' \equiv b\) (Chapter 7), read at an offset \(o\) with \(o\, 2^k\, \mathrm{rbaLength} \equiv a_0\), has at bit \(j\) the admission of \(a_0 + 2^k j\) by the row of \(b\).

The layout of a pattern of period \(m\): word \(x {\lt} m\, \mathrm{rbaPack}\) of the row the 64 bits from the offset \(64 x \bmod m\) on of the pattern repeated through \(w = \lfloor (m + 127)/64 \rfloor \) words, then the copies (init.c:259-267, init.c:280-297). The row of the residue \(b\) of a prime power \(m\), from its tables, the reference and the store: for a unit \(b\), bit \(x\) of the pattern set when bit \(x b^{-1} \bmod m\) of fsq is (init.c:369-375), and for \(p \mid b\), bit \(x\) of a unit \(x\) set when bit \(b x^{-1} \bmod m\) of gsq is (init.c:378-385); the pattern laid out, and the row published in the table of the reference (init.c:391-393). Then:

1. (1)

   for \(0 {\lt} m \le 64\, \mathrm{modWords}\) and a pattern whose bits \(x\) with \(m \le x {\lt} 64 \lceil m/64 \rceil \) are clear, word \(j\) of the row holds the 64 bits of the pattern, read with period \(m\), from \(64 j\) on;

2. (2)

   for \(b {\lt} m \le 64\, \mathrm{modWords}\) whose entry in the table of inverses is below \(m\), the builder returns the closed form of the row of \(b\), and the store with it published in the table of the reference.

The row of \(0\) of a prime \(p\): the \(p\) words of the forbidden divisor \(p\), whose word \(r\) has bit \(t\) clear exactly when \(p \mid 64 r + t\) (Ratpoints.Sieve.forbiddenRow), written \(\mathrm{rbaPack}\) times and followed by the copies (gen_find_points_h.c:122-134). The other rows by one function for the primes below \(64\) and one for those above, from the table of the prime, the reference, the residue \(b\) and the store: bit \(a {\lt} p\) of the pattern the entry of the table at \(a d \bmod p\) for the inverse \(d\) of \(b\), by a loop that steps four residues by \(4 d \bmod p\) (init.c:72-83), rotated into the first \(p\) words, the copies (init.c:99-111), and the row published in the table of the reference (init.c:178-183, init.c:239-244). Then:

1. (1)

   for \(p {\gt} 0\) the row of \(0\) is the closed form of the row of \(0\) of every table of \(p\), and its first \(p\) words are those that the forbidden divisors read (Chapter 8);

2. (2)

   for the table of a prime \(p {\lt} 64\) and \(0 {\lt} b {\lt} p\) whose inverse in the table is below \(p\), the function from CODE_INIT_SIEVE1 returns the closed form of the row of \(b\), and the store with it published in the table of the reference; the same holds for \(p \ge 64\) with \(p \bmod 64 \ne 0\) and the function from CODE_INIT_SIEVE2.

The builders need no primality and nothing of the table of squares.

The row of the residue \(b\) of a product: the rows of its factors at \(b\) modulo their moduli, read from their tables or built into them through the pointer of the entry of each factor (init.c:407-414); the first laid down in blocks of its length (init.c:419-423), the others and-ed in (init.c:424-429), the copies (init.c:430-430), and the row published (init.c:443-445). A factor is buildable when its builder has what it needs: a prime \(p {\gt} 0\) with its inverses below \(p\) and \(p \bmod 64 \ne 0\) for \(p \ge 64\), or a prime power \(0 {\lt} m \le 64\, \mathrm{modWords}\) with its inverses below \(m\); it may be called below its modulus, for a prime not at \(0\). Then:

1. (1)

   a buildable factor called where it may be called returns the closed form of its row and publishes it in the table given;

2. (2)

   if the product has a positive modulus \(m\) and a factor, the moduli of its factors divide \(m\), its factors are buildable, the rows present in their tables are closed forms, a row absent below the modulus of a factor is one where its builder may be called, and two factors with one reference have the same closed forms, then the builder returns the closed form of the row of \(b\), and the store has grown by rows of the factors (the tables keep their sizes, no row is replaced, every new row is the closed form of a factor whose table it is in), with the row of the product published.

For all words, \(\mathrm{mulHi}(a, b) = \lfloor a b / 2^{64} \rfloor \). For \(0 {\lt} p\) and \(u p {\lt} 2^{64}\) the remainder with the reciprocal of \(p\) is \(u \bmod p\); for \(1 {\lt} p\) and \(u p {\lt} 2^{64}\) the quotient is \(\lfloor u/p \rfloor \); for \(0 {\lt} p\) and \(|a|\, p {\lt} 2^{64}\), mod_mul gives the Euclidean remainder \(a \bmod p\).

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.

The row of \(b\) of a sound entry admits \(a\) for every triple \((a, y, b)\) with \(\gcd (a, b) = 1\) and \(y^2 = F(a, b)\), and the numerator of every point with the denominator \(b\) that the brute-force reference lists (Ratpoints.BruteForce.pointsOfDen) survives every list of sound entries for \(b\).

A store holds a function \(R\) of the references and the residues for a list of entries when every row present in the table of a reference \(\rho \) at \(r\) is \(R(\rho , r)\) and the table of every prime factor of the entries has its row of \(0\). An entry at the position \(n\) fits \(R\) when it has the reference and the kind of builder of that position (and, with one factor, the modulus of that factor), a positive modulus, a factor, moduli of the factors dividing its modulus and buildable factors, and \(R\) at its reference and at those of its factors is the closed form of their rows; a store fits a list of entries when it holds some \(R\) for them that every entry fits. The rows of the references of a run are the closed forms of the rows of the table of a prime, of the tables of a prime power and of the entry of a product at its position; a store is made for a list of entries when it holds the rows of the references of every run whose entries begin with the list, and every table of rows of a prime in it, or of a prime factor of the entries, has its row of \(0\). Then:

1. (1)

   if the row present in the table of an entry at \(b\) is the closed form, and the builder has what it needs when the row is absent, the row read or built is the closed form of the row of \(b\), and the store is the same or has grown by rows of the factors, with the row published;

2. (2)

   the store of the loop of the tables, which holds the rows of \(0\) of the primes and no others, is made for no entries; adding the tables of rows of further entries, each with the reference and the kind of builder of its position and with positive primes, gives a store made for the longer list; a store made for the entries of a run holds the rows of their references for them; and an entry of a modulus as the choice makes it (Chapter 6) fits the rows of the references of the run at its position;

3. (3)

   for a store that holds \(R\) for a list \(L\), entries of \(L\) that fit \(R\) at their positions and residues below their moduli, the sieve specs that set_rows makes and the missing rows complete have the closed forms of the rows of their entries at their residues, the offsets of the class, the start \(0\) and the end \(p\), and the store after them holds \(R\) for \(L\); so a store that fits the entries of a run fits them after each denominator.

For \(b_{\mathrm{high}} \ge 1\) the denominators of the search of \(c\) of its degree from \(1\) to \(b_{\mathrm{high}}\) are \(\mathrm{searchDenominators}(\mathrm{maxDivisors}, c, b_{\mathrm{high}})\) (Definition 2.9), and those from \(b_{\mathrm{low}} \ge 1\) are those from \(1\) that are at least \(b_{\mathrm{low}}\). For \(1 \le b_{\mathrm{low}}\) and \(1 \le b_{\mathrm{high}} \le H\), the points that the brute-force reference finds over \((1, 0)\), the points at infinity, followed by those over the denominators of the search with the numerators \(-H, \dots , H\), are a permutation of the points of \(\mathrm{bruteForce}(c, H)\) with \(z = 0\) or \(b_{\mathrm{low}} \le z \le b_{\mathrm{high}}\).

1. (1)

   The normalized switch of the reversal is the switch and the whole box (Definition 2.6); the normalized largest denominator is \(\mathrm{denominatorBound}(b_{\mathrm{high}}, H)\); a denominator \(1 \le z \le H\) lies in the normalized range exactly when \(b_{\mathrm{low}} \le z\) and (\(b_{\mathrm{high}} {\lt} 1\) or \(z \le b_{\mathrm{high}}\)), as in the search region; the normalized depth is at most \(55\) and negative exactly when the depth is.

2. (2)

   The search intervals are none exactly when the caller’s intervals are not well formed; they are the caller’s intervals when these are well formed and not empty; and for \(1 \le H {\lt} 2^{63}\) they are well formed and, when the caller gives none, hold \(a/b\) for every \(b {\gt} 0\) and \(|a| \le H\).

For the list of a search of \(c\) with the denominators from \(b_{\mathrm{low}}\) to \(b_{\mathrm{high}}\), intervals \(D\), a test \(S\) and the flags of the check:

1. (1)

   Let \(1 \le H {\lt} 2^{63}\), \(1 \le b_{\mathrm{low}}\), \(b_{\mathrm{high}} \le H\), and let the search intervals be well formed. For the normalized options of the sieve and either value of sturm_empty there is a sound test \(S\) such that the search of \(c\) of its degree (Definition 3.2), with the print channel that prints nothing, gives, for every callback, every setting of the flags of the check and every delivery whose flag of the stop is clear, the data and the count of the delivery of the list of the search for \(S\), the values of the search intervals (none when sturm_empty is set) and these flags. So the search with any callback gives the data and the count of the delivery of the list that the search with the appending callback gives. The run over the blocks has the corresponding contract, for sound arguments (Ratpoints.Sieve.IsSoundRun), a well-formed first decision of the choice and the bounds of well-formed search intervals.

2. (2)

   If \(S\) is sound, \(d \ge 1\) and the exact check is on, the list is what the brute-force reference finds over the candidate \((1, 0)\), followed by what it finds over the denominators of the search and the numerators \(a \in [-H, H]\) with \(a/b\) in \(D\), each point mapped back when the flag of the reversal is set, without those with \(y {\lt} 0\) under \(\mathrm{noY}\).

3. (3)

   With the exact check off, \(1 \le H\), \(1 \le b_{\mathrm{low}}\) and \(b_{\mathrm{high}} \le H\), whatever \(D\) and \(S\), every element is \((x, 0, z)\) with \((x, z)\) normalized and of height at most \(H\), and the list has no duplicates.

4. (4)

   Without the flag of the reversal and for \(1 \le b_{\mathrm{low}}\), every element has \(z = 0\), or \(b_{\mathrm{low}} \le z \le b_{\mathrm{high}}\) and \(x/z\) in \(D\).

5. (5)

   For the same \(D\), \(S\) and flag of the reversal, the list with the exact check on and \(\mathrm{noY}\) set, each \(y\) replaced by \(0\), is a sublist of the list with the exact check off, for either value of \(\mathrm{noY}\).

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.

Let \(1 \le b_{\mathrm{low}}\). The denominators of every shape lie in the range: the squares are its squares in increasing order; for positive divisors, the divisors times squares are its \(s k^2\) with \(s\) a divisor, without duplicates for distinct squarefree divisors; for forbidden divisors with positive primes and the words of Ratpoints.Sieve.forbiddenRow, the words give, in increasing order, the denominators of the range with their bit in \(\mathrm{den\_ bits}\) set that none of these primes divides. Let \(a\) and \(y\) be integers and \(1 \le b \le H\) with \(\gcd (a, b) = 1\) and \(y^2 = F(a, b)\). For odd \(d\), \(b\) passes the valuation test with the records of Definition 8.4; for even \(d\) and admissible forbidden divisors for \(b_{\mathrm{high}} = H\), the bit of \(b \bmod 64\) in \(\mathrm{den\_ bits}\) is set, no forbidden divisor with words divides \(b\), and \(b\) passes the tests of the words, with the tables for \(H\) when the Jacobi test is on. When bit \(j\) of \(\mathrm{den\_ bits}\) says whether the pattern of class \(j\) is not \(0\), a denominator of a shape that passes its test has a nonzero pattern.

Let \(b\) be a natural number and \(a\), \(y\) integers with \(\gcd (a, b) = 1\) and \(y^2 = F(a, b)\).

1. (1)

   For a prime \(p\), the row of \(b\) in the table of \(p\) admits \(a\).

2. (2)

   For a prime \(p\) and \(e \ge 1\) with \(p^e\) within the words of the bit arrays, the row of \(b\) in the tables of \(p^e\) admits \(a\).

3. (3)

   A factor is sound for \(m\) when its row of \(b \bmod m\) admits \(a \bmod m\) for every such \((a, y, b)\), its inverses serve the scaling of the rows by a unit modulo \(m\), its builder has what it needs, and its tables are those of Definition 6.1 or of examine_power. A prime of the sieve that divides \(m\) is a sound factor for \(m\), and so is a power \(p^e \mid m\) of one, for \(e \ge 1\) and \(0 {\lt} m {\lt} 2^{\mathrm{maxBitsInPrime}}\).

4. (4)

   A sieve entry is sound when its modulus is positive and its row of \(b\) admits \(a\) for every such \((a, y, b)\). An entry of an odd modulus \(1 {\lt} m {\lt} 2^{\mathrm{maxBitsInPrime}}\) with sound factors whose moduli multiply to \(m\), the reciprocal and the bias of \(m\) and an inverse \(x {\lt} m\) of \(\mathrm{rbaLength}\) modulo \(m\) is an entry of \(m\) as the choice makes it (\(\mathrm{IsModulusEntry}\)), whatever its density, count, reference and builder; such an entry is sound.

1. (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. (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.

Let \(f\) have degree \(1 \le d {\lt} 2^{57}\) with \(c_d \ne 0\), and the depth be at most \(55\). When the chain does not fail, \(f\) is squarefree. Assuming Sturm’s theorem:

1. (1)

   The invariant of the bisection is a well-formed interval whose counts and signs are those of \(f\) at its ends (Lemma 5.9). The bisection of an interval with the invariant keeps what the intervals kept before it hold and every \(x \in \mathbb {Q}\) with \(f(x) \ge 0\) between the values of the doubles of its ends, at a finite end only when \(f\) is positive just inside it.

2. (2)

   For well-formed intervals of the caller, the step leaves intervals that hold every \(x \in \mathbb {Q}\) of the caller’s intervals with \(|x| \le 2^{63}\) and \(f(x) \ge 0\). So the Sturm step of the search, for \(d\) the degree of \(c\) and when it does not refuse, puts every \(a/b\) of the given intervals with \(b {\gt} 0\), \(|a| \le 2^{63}\) and \(F(a, b) \ge 0\) into an interval that it leaves, sturm_empty clear; this needs Sturm’s theorem only when the step is on.

3. (3)

   The bisection keeps at most \(1 + \lfloor d/2 \rfloor \) intervals, the size of the array ivlocal of the C code, and the step leaves at most \(\lfloor d/2 \rfloor \) intervals more than the caller gives, within the room for \(1 + \lfloor d/2 \rfloor \) more that sturm.c asks of the caller’s array.

For a real polynomial \(p\) let \(V_p(t)\) be the number of sign changes at \(t\) of the Sturm sequence of \(p\) and \(p'\), \(V_p(+\infty )\) that of the leading coefficients of its entries, and \(V_p(-\infty )\) that of the leading coefficients each times \((-1)^{\deg q}\) for the entry \(q\). For an interval with ends \(l {\lt} r\) in \(\mathbb {R} \cup \{ \pm \infty \} \), the count at \(l\) is \(V_p(l)\), and at \(r\) it is \(V_p(r)\), plus \(1\) at a root; the sign at a finite \(l\) is that of \(p(l)\), or of \(p'(l)\) when \(p(l) = 0\), at a finite \(r\) that of \(p(r)\), or of \(-p'(r)\) when \(p(r) = 0\), and at \(\pm \infty \) that of the leading coefficient of \(p\), times \((-1)^{\deg p}\) at \(-\infty \); for a squarefree \(p\) these are the signs of \(p\) just inside the ends. Assuming Sturm’s theorem, for a squarefree \(p\):

1. (1)

   the counts at the ends agree exactly when \(p\) has no root strictly between them;

2. (2)

   when they agree and \(p\) is negative just inside \(l\), \(p\) is negative on \((l, r)\) and just inside \(r\);

3. (3)

   when they differ, or \(p\) is positive just inside \(l\), \(p\) is positive somewhere in \((l, r)\);

4. (4)

   when \(V_p(-\infty ) = V_p(+\infty )\) and \(p(0) {\lt} 0\), \(p\) is negative everywhere.

1. (1)

   Over an ordered field, a list of nonzero polynomials whose last entry is a unit and whose entries from the third on are positive multiples (\(c\, p\) with \(c {\gt} 0\)) of the negated remainders of the two before is, entry by entry, a list of positive multiples of the Sturm sequence of its first two entries; so the rows of a chain that ends with a constant are, over \(\mathbb {R}\), positive multiples of the Sturm sequence of \(f\) and \(f'\).

2. (2)

   Horner’s rule gives the sign of the value of a row at \(n/2^e\) when \(e \ge 0\) and \(e\) times the size of the row is below \(2^{63}\). For a chain that ends with a constant, the counts of the step at \(\pm \infty \) are those of the Sturm sequence of \(f\) and \(f'\); if also \(d {\lt} 2^{57}\) and \(f\) is squarefree, the signs and the count of the step at \(n/2^e\), \(0 \le e \le 55\), are the signs of \(f\) and \(f'\) and the count \(V_f(n/2^e)\) of Sturm’s theorem (Definition 2.8).

3. (3)

   The whole line is well formed at the depth \(0\), and the halves of a well-formed interval at a depth below \(55\) are well formed at the next depth, without overflow of the longs; the doubles of the ends have the values \(n\, 2^{-e}\), and \(\pm 2^{63}\) for \(\pm \mathrm{LONG\_ MAX}\). So the bisection to a depth of at most \(55\) keeps intervals with \(l \le u\), increasing and strictly apart.

4. (4)

   The step is none exactly when the chain is none. The intersection of two well-formed lists holds every value that lies in both. At a depth of at most \(55\), for well-formed intervals of the caller, the step and the Sturm step of the search leave well-formed intervals inside the given ones, none when sturm_empty is set; the Sturm step of the search refuses exactly when it is on and the chain is none.

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}\).

Let \(a\) and \(y\) be integers and \(b\) a natural number with \(\gcd (a, b) = 1\) and \(y^2 = F(a, b)\). Then bit \(a \bmod 64\) of \(\mathrm{nb}[b \bmod 64]\) is set. So the word of the class of a denominator over which the brute-force reference finds a point is not \(0\); and if \(\mathrm{den\_ bits} = 0\), the curve has no point of any height, the points at infinity included.

Let the run satisfy the hypotheses of Lemma 6.10 other than those on block \(i\) and its decision, the sieve entries having what Ratpoints.Sieve.IsRunEntries asks (their tables of inverses, the reciprocals of their moduli in their order, the row offsets of the classes with a pattern for all of them, and prime entries where they count no factor; they need not be sound), let the word of the classes mark those with a nonzero pattern, and let the decision of the choice be well formed. Then the run delivers the points of its blocks in order, block \(i\) those of its denominators that pass the tests of the shape, each with the first \(s_3\) entries of the decision of block \(i\), which depends neither on the callback nor on the flags of the output. So, when the loop of the shape visits no denominator twice, there is for each denominator \(b\) a number \(s_3(b)\), independent of the callback and the flags, such that the run delivers, over the denominators of the loop that pass its tests and in its order, the points with the flags of the numerators in the ranges of \(b\) that pass the class word of \(b\) and survive the first \(s_3(b)\) entries.

For every list \(c\) and every \(H\): a triple lies in \(\mathrm{bruteForce}(c, H)\) if and only if it is a normalized point of height at most \(H\) on \(y^2 = F_c(x, z)\); the list has no duplicates; and its set of elements is \(\mathrm{points}(c, H)\).

Let the program read a command line as above, and call the points of a list that the callback of the program keeps (Definition 10.9), under -1 only the first of them, its counted points (Ratpoints.Cli.countedPoints).

1. (1)

   Without -v: if \(\mathrm{findPoints}(c, H, s', o')\) returns the list \(L\) and the search with the callback of the program the outcome \(r\), the program prints the head of its report, the string before the points, the counted points of \(L\) (none under -z) in the format, separated by the string between the points, the string after the points and the end of the report for \(r\), with the status \(0\); the count of \(r\) is the number of the counted points of \(L\).

2. (2)

   Under -q, which clears -v, the program prints, whenever \(\mathrm{findPoints}(c, H, s', o')\) returns \(L\), the same without the head and the end of the report; under -q -1 without -z the one point printed is the first point of \(L\) that the callback keeps.

3. (3)

   The callback keeps a point unless it lies at infinity under -i, or \(z \ne 0\), the command line gives search intervals and \(x/z\) does not lie in their exact intervals. When every argument of the command line has fewer than \(2^{56}\) characters, the joined intervals are well formed (Definition 2.6), so that the library does not refuse them.

4. (4)

   Assume \(h_S\) and that the exact check is on. If \(\mathrm{findPoints}(c, H, s', o')\) returns \(L\), a triple lies in \(L\) and is kept by the callback exactly when it is a normalized point \((x, y, z)\) of height at most \(H\) (Definition 2.4) with \(y \ge 0\) under -y and \(z \ne 0\) under -i, and, for \(z \ne 0\), with \(z\) in the range of the denominators of -dl and -du and \(x/z\) in the exact intervals of the command line when there are such intervals.

For the arguments of a run and every block \(i\), the decision in force for block \(i\) among the decisions after the folds of the first \(k\) blocks is the decision of block \(i\) for every \(k \ge i - \mathrm{adaptLag}\): block \(i\) reads only decisions made at the folds of blocks at least \(\mathrm{adaptLag} + 1\) before it.

Assume \(h_S\) and that the exact check is on, \(o.\mathrm{noCheck} = \mathrm{false}\), and let \(\mathrm{findPoints}(c, H, s, o)\) return the list \(L\). A triple \(p = (x, y, z)\) lies in \(L\) if and only if \(p\) is a normalized point of height at most \(H\) on \(y^2 = F_c(x, z)\) (Definition 2.4), \(y \ge 0\) if \(o.\mathrm{noY}\) is set, and \(p\) lies in the search region of \(o\). Indeed \(L\) is a permutation of the brute-force reference \(\mathrm{bruteForce}(c, H)\) filtered by the last two conditions; and when neither option of the output is set, the set of the elements of \(L\) is \(\mathrm{points}(c, H)\) filtered by the search region of \(o\).

Let the exact check be off, \(o.\mathrm{noCheck} = \mathrm{true}\), and let the search \(\mathrm{findPoints}(c, H, s, o)\) return the list \(L\).

1. (1)

   Every element \((x, y, z)\) of \(L\) has \(y = 0\) and the pair \((x, z)\) normalized and of height at most \(H\) (Definition 2.4), and lies in the search region of \(o\).

2. (2)

   Assume \(h_S\). For every normalized point \((x, y, z)\) of height at most \(H\) in the search region of \(o\), the triple \((x, 0, z)\) lies in \(L\).

3. (3)

   If the search with the same \(s\) and \(o\) with \(\mathrm{noCheck}\) cleared and \(\mathrm{noY}\) set returns the list \(L'\), then \(L'\) with each \(y\) replaced by \(0\) is a sublist of \(L\).

For all \(c\), \(H\), \(s\) and \(o\), if \(\mathrm{findPoints}(c, H, s, o)\) returns the list \(L\), then \(L\) has no duplicates.

Assume \(h_S\) and that the exact check is on, \(o.\mathrm{noCheck} = \mathrm{false}\). Let \(\mathrm{findPoints}(c, H, s, o)\) return the list \(L\), let \(r\) be true when \(o\) allows the reversal and its search region is the whole box of \(H\), and \(B\) the largest denominator of the search, \(o.\mathrm{bHigh}\) if \(1 \le o.\mathrm{bHigh} \le H\) and \(H\) otherwise (Definition 2.6). Then \(L\) is

(Definition 2.9) with the points left out that have \(y {\lt} 0\) when \(o.\mathrm{noY}\) is set or do not lie in the search region of \(o\). Moreover, the search with the Sturm step off and the other options as in \(o\) returns \(L\) too.

For all \(c\), \(H\), \(s\) and \(o\), every callback and its data: the search with the callback, with the print channel that prints nothing, refuses exactly when \(\mathrm{findPoints}(c, H, s, o)\) refuses, with the same refusal; and when \(\mathrm{findPoints}(c, H, s, o)\) returns the list \(L\), the search with the callback returns an outcome whose data and count are those of the delivery of \(L\) to the callback from its data, the count \(0\) and the flag of the stop clear. So the calls of the callback are those for the points of \(L\), in their order, up to and including the first call that stops the search, and the count is the sum of the weights that these calls return.

Let \(n + 1\) be the length of \(c\) and \(N = 2 \lceil n/2 \rceil \). With the Sturm step on (\(0 \le o.\mathrm{sturm}\)), \(\mathrm{findPoints}(c, H, s, o)\) refuses if and only if

1. (1)

   \(c\) has fewer than two or more than \(\mathrm{maxDegree} + 1\) entries,

2. (2)

   \(H = 0\) or \(H \ge 2^{63}\),

3. (3)

   the binary form \(\Phi _c\) (Definition 2.3) is not squarefree, or

4. (4)

   the search intervals of \(o\) are not well formed (Definition 2.6).

With the Sturm step off (\(o.\mathrm{sturm} {\lt} 0\)), it refuses if and only if (1), (2) or (4) holds, or \(d + 2 \le N\), or \(o\) allows the reversal, its search region is the whole box of \(H\), \(d\) is even and \(c_0 = c_1 = 0\).

Let \(A \ge 1\), \(0 {\lt} b {\lt} 2^{63}\) and \(H {\lt} 2^{63}\); let the class pack a word \(w\) and have a row of offsets packed for it, the entries of the first two stages have tables of inverses that invert and tables of rows that fit them, the entries of the third stage be prime entries, and the bounds of the search intervals give the ranges of the numerators at \(b\). Then, with the exact check on, from a delivery whose flag is clear, sift on \(b\), with the reciprocals of the entries and the residues of \(b\) for the stride, delivers the points that the check of the plain sieve with the entries of all three stages finds, restricted to the numerators that lie in a range and pass \(w\), mapped back after a reversal, and without those with \(y {\lt} 0\) under \(\mathrm{noY}\).

Under the hypotheses of Theorem 3.13, let each block \(i\) be sifted alone with the appending callback into a slot, from the empty array, with the decisions after the folds of any \(k_i \ge i - \mathrm{adaptLag}\) blocks and a store of its own that fits all the entries. Then delivering the slots in the order of the blocks to a callback whose flag is clear, with a return after the slot in which a call stops the search, gives what the run delivers.