11 The link to the C code

Lean has no semantics of C, and no theorem of this blueprint speaks about the C code of ratpoints: the theorems speak about the model, which mirrors the C code component by component, with the same loops, tables, bit arrays of 64-bit words and index arithmetic. This chapter describes what ties the model to the C code of release 3.1.1: the record of which declaration models which lines of C, and its checks; the lines that no declaration models; the departures of the model from the C code; the differential tests of the program ratpoints-model against the C program; the builds with other values of the compile-time constants; and CI. The nodes of the chapters before this one cite the main ranges of their definitions; Appendix A, generated from the record, lists every range with its owners and their deviations, or its exclusion.

The link is not a proof. That a definition does what its lines of C do is checked by reading the two side by side; the record makes sure that every line of C is accounted for, that each claim is made for a definite text on both sides, and that a change on either side is noticed; the differential tests check the correspondence on behaviour, on finitely many inputs. Comparator certifies the statements about the model and says nothing about the C code (Section 3.8).

11.1 The record

Every line number refers to one commit of ratpoints, the pin: release 3.1.1, tag v3.1.1, commit 1a99853, named in correspondence/ratpoints.toml and, for the links of the blueprint, in the macro \ratpointscommit. The record covers find_points.c, sift.c, init.c, sturm.c, the headers rp-private.h, ratpoints.h and primes.h, the generators of tables gen_find_points_h.c and gen_init_sieve_h.c, and the program main.c. Every line of code of these files, that is, every line that holds something besides white space and comments (a line of the preprocessor counts), lies in exactly one recorded range, and no two ranges overlap.

A range is modelled when the docstring of a public declaration of the model names it, in a paragraph that begins with C:; an optional paragraph that begins with Deviation: says where the declaration departs from the C code. The docstring of Ratpoints.Sieve.squaresMod, for instance, ends with

C: `find_points.c:37`, `gen_find_points_h.c:69-88`

Deviation: a function of `p`, computed when it is called, for the row of `p` in the table
`squares` that the build generates and that `find_points.c` includes. -/

A range may have several owners (line 37 of find_points.c includes three generated tables and is a range of the three functions that compute them), and a declaration that calls another, which models a part of its C code, cites the lines around that part. A private declaration carries no record, since no node can name it. A range is excluded when a table [[excluded]] of the record gives it, with a kind and the reason (Section 11.2).

The script scripts/correspondence.py checks the record. It reads the docstrings of the model with the help of scripts/Correspondence.lean, and the C files at the pin from a clone of ratpoints, and it checks:

1. (1)

   that the pin is a commit of the clone, to which its tag points where the clone has the tag, that every range lies within the lines of a file of the record, that no line lies in two ranges, and that every exclusion has a known kind and a reason;

2. (2)

   that every range and every C link of the blueprint is locked: for every range, the lock holds the SHA-256 hash of its text at the pin and its owners (the declarations that model it, or its exclusion), and for every link the hash of the text that it shows; a range whose text or owners differ from those of the lock, and a new link, are reported until they have been compared with their counterparts by hand and locked again by scripts/correspondence.py lock, which writes the lock into correspondence/lock.json;

3. (3)

   that the appendix is the one that the record generates, and that every link inside a node of the dependency graph that names declarations with \lean is one of the ranges of the model declarations that the node names, exactly as recorded (a node need not cite all of them; prose and remarks may link to any range);

4. (4)

   with --complete, which CI passes, that every line of code lies in a range.

After a move of the pin, a range counts as locked when some locked range has its text and its owners, and a link when some locked link shows its text, wherever their lines are; so a move of the pin to another release of ratpoints makes the check report exactly the ranges whose text or owners changed and the links whose text changed (correspondence/README.md describes the procedure).

11.2 The exclusions

An excluded range has one of the kinds threads, memory, instrumentation, interface and other.

threads: the pool of threads, with which ratpoints sieves the blocks of its loop over the denominators apart (find_points.c:4129-4519), its set-up in the search, the atomic loads and stores of the fields that the threads share (rp-private.h:76-84), the fields of the arguments that hold the number of threads and the pool, and the default of one thread in main.c. The model sieves the blocks in turn. The thread lemma (Theorem 3.15) shows that blocks sifted apart and delivered in their order give the same; that the pool of the C code meets its hypotheses is read off the C code (Chapter 3).

memory: the buffers of the sieve entries, the rows, the tables, the words of the forbidden divisors and the prime powers, with their alignment and enlargement (find_points.c:181-270) and their release (find_points.c:377-416), the arrays of the run and of a worker, the copy of the caller’s intervals in the Sturm step, the GMP variables that main.c initializes and releases, and the failures for lack of memory, error 10 of the program among them. The model allocates nothing itself and cannot fail for lack of memory; such failures inside modelled ranges, such as the drop of the forbidden divisors beyond the table whose words find no memory, are deviations of their owners.

instrumentation: the output under DEBUG, the timers and counters of RP_PHASE_TIMING and RP_PHASE_COUNTS (sift.c:55-176), the report of RP_PRIME_STATS, RP_STOP_AFTER, RP_MOD_CHOICE, RP_MOD_COUNTS, the check RP_VERIFY_MODULI of the rows (init.c:299-353) and two probes for a benchmark, all compiled only on request or empty in the default build. Output under DEBUG inside a modelled block goes with the block, whose deviation says that the model prints nothing there; the report under RATPOINTS_VERBOSE (-v) is modelled (Chapter 10).

interface: what only another caller of the library meets: find_points_init (find_points.c:272-375) and its prototype, the input fields of the arguments that find_points_work saves and puts back, the checks of arrays that only such a caller can fail (find_points.c:4618-4623), the declaration of the arguments in main.c and the initialization of the fields that the model passes as values, and the prototype of the Sturm step.

other: lines without meaning for the model: the includes, those of the vector intrinsics among them, and the prototypes; the inlining attributes and the pragma that unrolls the loops of tail_leg (sift.c:466-472); FLOOR, RATPOINTS_DEFAULT_SP1 and RATPOINTS_DEFAULT_SP2, which the C code reads nowhere, and a count stored that nothing reads; the text of message 1, which main never prints (main.c:977-978); the frames of the main functions of the generators of tables; and the arm of exact_scale for a build without a 128-bit integer type (find_points.c:3239-3256), since the default build compiles the arm with unsigned __int128.

11.3 The deviations

The Deviation: paragraphs record, declaration by declaration, where the model departs from its lines of C. Most of the departures are of the following kinds. None corrects the C code: the model is that of release 3.1.1 as it is.

Integer types. The model computes with natural numbers and integers where the C code has longs, ints, unsigned longs and GMP integers, and with rational numbers for GMP rationals; where a value of the C code could leave its type, the range obligation is a lemma that the deviation names. Lean’s 64-bit words stand where the C code depends on the words themselves: in the bit arrays, the reductions by a reciprocal and the counters of the run, which wrap as unsigned longs wrap; in the test for common factors (Ratpoints.Sieve.relprime), whose step without branches acts on the two’s complement of a negative long and shifts it arithmetically, as gcc defines these operations, which the C standard leaves to the implementation; and in the bits of the numerators of an interval, the forms of the ends of the intervals and the numerators of the Sturm step, whose arithmetic wraps where that of the longs would overflow, on no path that the search takes. The 128-bit products are taken on two words, the high word from four products of 32-bit halves (Ratpoints.Sieve.mulHi). The height bound is a natural number, refused from \(2^{63}\) on with error 4, as the program refuses such a height when it reads it.

Pointers and buffers. Arrays and indices stand for pointers into arrays, an option for a pointer that may be null, and values returned, often structures, for what the C code writes through pointers or into buffers of its caller; state that the C code reaches through pointers, such as the delivery of the points, the tables of rows (Ratpoints.Sieve.RowStore) and the counters, is passed and returned. A search gives back what the program reads (Definition 2.11), not the other fields that the C code leaves in the arguments. The end of a row that is not built yet is \(p\) (Ratpoints.Sieve.setRows), where set_rows adds \(p\) to the null pointer (find_points.c:3149-3170), which the C standard leaves undefined; this happens in ordinary runs, whenever set_rows reports a row as missing, and the end is set again when the row is built, before it is read.

Generated tables. The squares, the inverses and the rows of \(0\) of the primes, which the build generates into find_points.h, are functions of the prime, computed when they are called: Ratpoints.Sieve.squaresMod, Ratpoints.Sieve.inversesMod and Ratpoints.Sieve.sieves0. The functions that the build generates into init_sieve.h, one for each prime, which build its rows, are two functions, Ratpoints.Sieve.sieveInit1 and Ratpoints.Sieve.sieveInit2, with the prime an argument; and a pointer to such a function is the kind of the builder, with a match on it (Chapter 7).

Vector code. A bit array of the default build is a vector of \(256\) bits; in the model it is \(\mathrm{rbaPack} = 4\) consecutive words of an array of UInt64, and the & of two bit arrays the & of their words (Ratpoints.Sieve.andBitArray). The registers of the chunked first stage are a vector of \(\mathrm{chunk} = 16\) bit arrays, the code that the build unrolls under #if (RATPOINTS_CHUNK >= k) is a loop over them (Ratpoints.Sieve.chunkSieve), and the conditional compilation that chooses an arm is a test on the constant (Chapter 9). The other builds differ in these constants (Section 11.5).

Doubles. The doubles of the search region are their IEEE 754 bits (Ratpoints.Double), with a function, which owns no range of C, for each operation that ratpoints applies to them, as gcc and glibc compute it with rounding to nearest; strtod and printf under %f are modelled by their values, not by glibc’s algorithms (Chapter 5). The doubles of the cost model are Lean’s Float, with the platform’s arithmetic, log and pow, and no proof reads their values; the sorts by qsort are a stable merge sort (Ratpoints.sortFrom), which gives the order of glibc’s qsort, a stable merge sort whenever it can allocate its buffer, since no key is a NaN (Chapter 6). Where the C code computes in double what the model computes exactly (the comparison of \(2pH\) with the limit of the third stage, the integer square roots of the shapes), the deviation shows that the outcome is the same.

Structure and the program. The model has one function, Ratpoints.findPointsVerbose, for find_points, find_points_work and the start of find_points_work_1, whose rest is Ratpoints.findPointsWork; parts of long functions and bodies of loops are functions of their own; arrays that the C code fills once per denominator under a flag are thunks; and the report under RATPOINTS_VERBOSE goes through a print channel of the search. The program writes its output once, at the end, where main.c prints after every point; it differs from ratpoints on a closed pipe and on format words that are not UTF-8, where the runtime of Lean acts otherwise than that of C (Chapter 10).

Inputs that ratpoints never meets. Where the C code would overflow or divide by zero on an input that it is never given, the model takes a defined value, and the contract excludes the input or the proofs show that it does not occur: the negation of \(-2^{63}\) in the test for common factors wraps, and the integer square root rounded up gives \(1\) at \(0\). The loop that counts the trailing zeros does not end on \(0\), as in the C code (Ratpoints.Sieve.ctz), and the masks of the forbidden valuations drop the bound \(m {\lt} 63\) of the C code, which never binds for a height that is a long (Chapter 8).

11.4 The differential tests

The script scripts/difftest.py runs ratpoints-model, the model compiled by Lean (Chapter 10), on the test suites of ratpoints and on further command lines, and compares it with the outputs that the suites record and with the C program at the pin on the same command line; the C program must be the default build, without the machine-dependent tuning that make tune writes. Every list of points is compared in its order. Under -q the points are compared with a recorded output and byte for byte with the output of the C program, and so are the outputs with the options and formats of the output and the reports, with messages 3, 4 and 8 on the search region, the moduli used and the search intervals, the banner exchanged for that of the C program, also under -v, where the report of the library comes between the points. The outputs that test4.sh filters are compared after the filter and as a whole; those that test3.sh filters, as a whole, before the filter. Under -x, where the program prints the pairs that survive the sieve, the pairs are compared byte for byte with the C program, since the model chooses and corrects its moduli as ratpoints does, and, without a format and without -v, they also pass a check that does not depend on the moduli: normalized coprime pairs in the range of the height and in the search region, none repeated, and the points among them the same, in the same order, in both outputs. Exit statuses and messages are compared exactly, but for the banner and the usage; ratpoints-model must write nothing to its standard error (a panic of the Lean runtime ends it); and failed writes are compared too.

The default suites search up to the height \(30000\), and above it in narrow search regions. Since the choice of the moduli computes with the log and pow of the platform’s C library, which glibc does not round correctly and chooses by the processor, the comparisons that depend on it (the pairs under -x, message 4 and the report under -v) are made with both programs on one machine; CI runs both on its runner. On the state of the project that this blueprint describes, the suites make these comparisons, none of which fails:

The last two suites are not run by default, nor the comparison of a build of the C program with a fixed length of the blocks (-DRP_BLOCK_LEN=3) with ratpoints-model built with the same length (Ratpoints.blockLen), which tests the boundaries of the blocks. The #guard examples of the model, which every build runs, compare components with values taken from the C program, gcc and glibc, none of which depends on the log or pow of the platform.

11.5 Other values of the constants

The file Ratpoints/Model/Constants.lean holds the constants that the C code fixes when it is compiled, each a definition with the value of the default build and a docstring that names its macro: among them the bound on the degree (Ratpoints.maxDegree), the number of bits of the moduli, the width of a bit array (Ratpoints.rbaPack), the chunk of the first stage (Ratpoints.chunk), the default depth of the Sturm step, the limits of the reductions by a reciprocal, the doubles that tune the cost model and the constants of the blocks (Ratpoints.adaptLag, Ratpoints.blockLen). No proof depends on their values beyond a few facts that the file decides: that the width, the chunk and the array sizes are positive, that the limits of the reductions are at most \(2^{32}\), that a bit array has \(2^{\mathrm{rbaShift}}\) bits with \(\mathrm{rbaShift} {\lt} 32\), that \(\mathrm{maxBitsInPrime} \le 10\), that the bound on the degree is positive and below \(2^{57}\), that a fixed length of the blocks is positive, and a few more of that kind.

The script scripts/constants_check.py checks this by building copies of the committed project, with all its proofs and without the #guard examples of the model, which test the default values, for eleven other sets of values, each of which builds: two that change every constant, one to small values (among them bit arrays of \(64\) bits, the chunk \(1\), the lag \(0\) and blocks of length \(1\)) and one to large values (bit arrays of \(512\) bits, the chunk \(17\), which compiles the other arm of the first stage, the lag \(1000\)); four that change the chunk alone, to \(2\), \(3\), \(5\) and \(12\); three that pair the chunked first stage with the widths of the other builds, \(512\), \(128\) and \(64\) bits; one with the lag \(1\) and blocks of length \(3\); and one with one block wanted. So the proofs hold for the models of the configurations of the C code that differ in these constants, the widths of the bit arrays of all its builds among them. The script builds the copies one after the other, with the built packages of the repository, and runs on demand, outside CI; the sets of values are a table in it, and --variant gives others.

11.6 Continuous integration

The workflow .github/workflows/build-project.yml runs on every push to the main branch and on every pull request. It checks the layout (scripts/check_layout.py: the imports of each part; no partial, unsafe, implemented_by, extern or experimental option in the model, which would let the executable run code that the proofs do not see; and nowhere a tactic that adds an axiom, such as native_decide), the style of the Lean code and the length of its lines, and the listing Ratpoints.lean of the modules; builds, with every warning a failure, the model, the specification and the proofs, ratpoints-model and the solution of comparator, and then the challenge, whose sorrys warn by design; runs the tests of the scripts; checks the record with --complete against ratpoints at the pin; and builds the C program at the pin and runs the default suites of the differential tests against it. The build fails if a main theorem depends on an axiom beyond propext, Classical.choice and Quot.sound, by the guards #print axioms under #guard_msgs. Comparator (Section 3.8), the suites test4high and adapt, the pair with a fixed length of the blocks and the builds with other values of the constants (scripts/constants_check.py) run outside CI.