10 Delivery and the program
The library function find_points of ratpoints returns no list of points: it hands each point that it finds to a function of its caller, the callback, which may count it, print it or stop the search. This chapter describes how the model does the same, with the callback, its weights and its stop, the options of the output RATPOINTS_NO_CHECK and RATPOINTS_NO_Y, what a search writes back and the report of the library under RATPOINTS_VERBOSE; and the program ratpoints-model, which reads the command line of ratpoints and prints what ratpoints prints, but for its banner. The reference of the delivery, with which the statements compare a search, belongs to the specification (Definition 2.13); the theorems on what a search delivers and what the program prints are in Chapter 3; the components of the sieve that pass the delivery on are those of Chapter 9.
10.1 The callback and the delivery
The header of the library declares the callback of find_points and find_points_work (ratpoints.h:436-437, ratpoints.h:441-442) as int proc(long, long, const mpz_t, void*, int*); the manual names its parameters x, z, y, info and quit. The library adds the value that each call returns to a count total, which it returns, or one of the negative codes of an error (ratpoints.h:427-430); a call stops the search by setting *quit, which the library clears before the search and tests after the steps that may have made calls (Section 10.2), so that it is clear at every call. Every refusal of the input comes before the first call; only RATPOINTS_NO_MEMORY can come after calls, when an allocation fails, and the model has no allocation that can fail. The callback of the model and the delivery that a search threads through its components are those of Definition 2.13; the delivery stands for the pointer info, for the counts total of the functions of the search as one running count, and for the flags of the stop of the points at infinity and of the sieve (find_points.c:4570-4571, find_points.c:3129-3129).
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).
Apart from the flags of the check, which stand for bits of args->flags, these definitions model no C code of their own; the appending callback is that of \(\mathrm{findPoints}\), of which the statements speak (Definition 3.1).
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\).
By induction on the list, from the fold, in Lean core only, so that the contracts of the sieve, which are proved without Mathlib, can state what they deliver.
10.2 The stops
In the C code on one thread only a call of the callback sets the flag (with threads a worker also sets it when the search has been stopped, find_points.c:3610-3610), and each function tests it after each step that may have made calls, returning its count at once when it is set: _ratpoints_sift0 after the check of a numerator (sift.c:1250-1251, sift.c:1287-1288, and sift.c:1168-1169 in the arm of USE_LONG_IN_PHASE_2); sift after each call of _ratpoints_sift0 (find_points.c:3611-3611); run_block after each denominator, in each shape of the loop (find_points.c:3928-3928, find_points.c:3957-3957, find_points.c:4044-4044, find_points.c:4068-4068); the loop over the blocks after each block (find_points.c:5158-5158); and find_points_work_1 after the points at infinity, before it sieves (find_points.c:5100-5103). So the calls made are those of the search that no call stops, up to and including the first call that sets the flag, and the count is the sum of their weights. With threads the calling thread of the C code delivers the points of the blocks in their order; that blocks sifted apart and delivered in this way make the calls of the run on one thread is the thread lemma (Theorem 3.15), and that the pool of ratpoints meets its hypotheses is read off the C code, not proved.
The model tests the flag at the same places, with one difference of form: where the C code returns from _ratpoints_sift0 from within the walk through the set bits of a word, the walk of the model returns, and its callers test the flag after each walk, and the scan of a piece after each bit array, and return in turn; this makes no call that the C code does not make and skips none. Every component of the sieve from the walk up to the run over the blocks takes the callback, the flags and a delivery and hands them on (Chapter 9); its contract has the precondition that the flag is clear and concludes that the delivery after it is the delivery (Definition 2.13) of a list, the points of the component in their order. Each loop that may return early keeps an invariant with a case for the return at a stop, closed by Lemma 10.2 (the invariants Ratpoints.Sieve.WalkDeliveryInvariant of the walk and Ratpoints.Sieve.SieveRunLoopInvariant of the run over the blocks). So the search with any callback delivers the list of the search with the appending callback, up to and including the first call that stops it: the protocol of the delivery (Theorem 3.7).
10.3 The options of the output
Two bits of the flags of the caller change which points the library delivers (ratpoints.h:403-404): under RATPOINTS_NO_Y only the point with \(y \ge 0\) of a pair \((x : \pm y : z)\) goes to the callback, and under RATPOINTS_NO_CHECK every numerator that passes the sieve goes to it with \(y = 0\), without the exact check, whether or not it gives a point. The C code reads them only in the exact check (find_points.c:5250-5338), at the points at infinity (find_points.c:5068-5099), and RATPOINTS_NO_CHECK also in a line of the report; the reversal, the Sturm step, the exits, the tests on the denominators and the sieve run as without them. Conversely, what RATPOINTS_NO_CHECK delivers depends on everything that decides which numerators pass the sieve: the moduli, the Jacobi test, the reversal and the region of the Sturm step.
In the model the two options are the fields \(\mathrm{noCheck}\) and \(\mathrm{noY}\) of the options of a search, false by default (Definition 2.11), which the search copies, with the flag of the reversal, into the flags of the check (Definition 10.1). What the points at infinity deliver with these flags is the list of Definition 4.9; what the exact check (Chapter 9) delivers for one numerator to a callback that does not stop the search is the following list, a definition of the proofs that holds no C code.
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.
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}\).
Each call is the delivery of a list of one point, and the test of the flag between the two calls of a pair is the delivery of their concatenation (Lemma 10.2). The rest by the cases of the flags: over one numerator the reference finds \((a, y, b)\) and \((a, -y, b)\), or \((a, 0, b)\), or nothing, so that the point with \(y \ge 0\), with \(y\) replaced by \(0\), is the survivor, and the map of the reversal keeps \(y\).
The contracts of the sieve carry these lists upwards: the search delivers the points at infinity with the flags followed by the points with the flags of the numerators that pass the test of the sieve, a test that depends neither on the callback nor on the flags. So the output under RATPOINTS_NO_CHECK holds, as a sublist and so in the same order, the survivors \((x, 0, z)\) of the points \((x, y, z)\) that the same search delivers with the exact check on and RATPOINTS_NO_Y set, and each of its elements has \(y = 0\) and a normalized pair \((x, z)\) of height at most \(H\) in the search region (Theorem 3.8).
10.4 What a search gives back
Besides the count, find_points writes back what the program reads after the search: three bits of args->flags (ratpoints.h:414-417), RATPOINTS_REVERSED, set by the reversal check, and RATPOINTS_USE_SQUARES and RATPOINTS_USE_SQUARES1, set for odd degree when the leading coefficient is \(\pm 1\) and, otherwise, when the set-up of its divisors succeeds (find_points.c:4910-4943), for message 7; the search intervals as the Sturm step leaves them, for message 8; and the numbers of the moduli used in the stages (ratpoints.h:378-378), for message 4. The outcome of a search in the model holds exactly these, with the data of the callback and the count (Definition 2.11). The search sets the bits before its exits and before the points at infinity, and it returns after the Sturm step only for even degree, where the two bits of the squares are clear; so the bits and the intervals are written back on every path that does not refuse the input, whatever the callback does. The numbers of the moduli are zeroed on entry and set after the sieve from the moduli of the last block sifted, so that they depend on where the callback stops the search (Chapter 3). Nothing else is written back: the reversed coefficients and the private fields that the choice of the moduli writes are not, and the bits of the input come back as the caller set them (find_points.c:4606-4606).
10.5 The report of the library
Under the bit RATPOINTS_VERBOSE of the flags (ratpoints.h:407-407), which the option -v of the program sets, the library prints a report of the search on the standard output, between the points that the callback of the program prints there. The model has no standard output: the search takes a print channel, a function that prints a text into the data of the callback, which holds the standard output of the caller (Definition 10.1). The search with a print channel is \(\mathrm{findPointsVerbose}\), and \(\mathrm{findPointsWith}\) takes by default the channel that prints nothing (Definition 3.1).
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).
Four texts complete the report: the two exits on the way (Ratpoints.Report.noClasses, Ratpoints.Report.noPoints), the line before the points at infinity (Ratpoints.Report.atInfinity) and the forbidden valuations (Ratpoints.Report.excludedValuations). Each text is printed where the C code prints it, or once from the result of a check where the C code prints in its course. The report is compared byte for byte with that of the C program (Chapter 11) and not proved: with the print channel that prints nothing every text vanishes (Ratpoints.findPointsWith_eq), and the theorems speak about that channel.
10.6 The program
The executable ratpoints-model has the command line of ratpoints: the coefficients \(c_0, \dots , c_n\) of \(y^2 = c_n x^n + \dots + c_0\) as one argument, the height bound and the options. It reads them as main.c does, with its checks, messages and exit statuses in its order, runs the search with the callback of main.c, and prints what ratpoints prints, but for the banner and the usage, which name ratpoints-lean (the earlier name of the program), so that the test scripts of the C repository can run it in place of ratpoints. Its root ModelMain.lean imports only the model, so that the program depends neither on Mathlib nor on the proofs. It acts on every option of ratpoints but -t, the number of threads, which it checks and ignores: the model sifts the blocks of the run in turn, and the thread lemma (Theorem 3.15) shows that blocks sifted apart under hypotheses that the pool of ratpoints meets by its code, and delivered in their order, give the same output.
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).
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 parts of a word give its exact value, and the exponent that scan_end accumulates, which stops at LONG_MAX / 20, is the exact one for arguments of fewer than \(2^{56}\) characters whose double is finite and not zero; the rounding of strtod is that of the doubles (Chapter 5). The loops of outward, in_region and join_intervals are proved by named invariants with the program logic of Lean core.
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 delivery of a list to this callback prints, unless -z, the points of the list that it keeps, under -1 only the first of them, and its count is their number (Ratpoints.Cli.deliver_process); the theorem on what the program prints (Theorem 3.9) rests on this and on the protocol of the delivery.
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 exit statuses are thus those of main.c: \(0\) after a search, \(2\) to \(7\) and \(11\) for the command line, \(8\) for a binary form that is not squarefree, and \(9\) for search intervals that the library refuses (main.c gives \(9\) for every code of the library but those of errors 8 and 10); by Theorem 3.9 no command line whose arguments are shorter than \(2^{56}\) characters leads to error \(9\). Error \(10\), for lack of memory, has no counterpart. When the reader of its output is gone, SIGPIPE ends ratpoints and the shell reports the status \(141 = 128 + 13\); the Lean runtime ignores that signal, and ratpoints-model exits quietly with the status \(141\) when its write fails.
Besides the deviations stated above, the program keeps the data of main.c as a value with the text printed so far, for the pointer info and the standard output, and writes its output once, at the end, where main.c prints and flushes after each point. It reads the formats and the strings as Lean strings, decoded from the command line as UTF-8, where main.c copies the bytes; since every escape of main.c is ASCII and no byte of a multibyte character of UTF-8 is, both print the same bytes for every format and string in UTF-8. The lines of main.c without a counterpart, such as the includes and the initialization of the GMP integers, are excluded in the record (Chapter 11).