1
Overview
▶
1.1
What
ratpoints
computes
1.2
The four parts
1.3
The specification
1.4
The main theorems
1.5
How the proofs go
1.6
What one has to trust
1.7
What is not verified
1.8
How to read this blueprint
2
The specification
▶
2.1
The binary form
2.2
The points
2.3
The search region
2.4
The order of
ratpoints
2.5
The options, the refusals and the outcome of a search
2.6
The reference of the delivery
2.7
The brute-force reference
3
The main theorems
▶
3.1
The search
3.2
The points that a search finds
3.3
The refusals
3.4
The delivery and the options of the output
3.5
What the program prints
3.6
The search as a filter of the reference
3.7
The blocks, the lag and the threads
3.8
What comparator certifies
4
The set-up
▶
4.1
The order of the checks
4.2
The squarefree binary form
4.3
The reversal
4.4
The remainder chain
4.5
The points at infinity
4.6
The exit by a prime
5
The search region and the Sturm step
▶
5.1
The doubles
5.2
The search intervals
5.3
The bounds of the numerators
5.4
The Sturm step
5.5
Sturm’s theorem and the coverage
5.6
The region that the search uses
5.7
Deviations
6
The choice of the moduli and the blocks
▶
6.1
The table of a prime and the loop of the tables
6.2
Prime powers and products
6.3
The cost model
6.4
The choice of the moduli and of the cut points
6.5
The blocks of the run
6.6
The correction of the moduli
6.7
Why the choice does not change the output
7
Tables and rows
▶
7.1
The tables as
ratpoints
computes them
7.2
The closed form of a row
7.3
The tables of rows and the builders
7.4
The rows of a run
7.5
Where the model differs from the C code
8
The denominators
▶
8.1
The 2-adic information
8.2
Odd degree: squares and divisors
8.3
Even degree: the forbidden divisors
8.4
The Jacobi test
8.5
The shapes of the loop
8.6
The order of the denominators
8.7
Where the model differs from the C code
9
The sieve of one denominator
▶
9.1
The sieve in the C code and in the model
9.2
Bit arrays of words
9.3
Reductions by a reciprocal
9.4
The packing of the numerators
9.5
The first stage
9.6
The second stage and the extraction
9.7
The test of a candidate and the exact check
9.8
One denominator
9.9
The stages compute the plain sieve
9.10
Where the model differs from the C code
10
Delivery and the program
▶
10.1
The callback and the delivery
10.2
The stops
10.3
The options of the output
10.4
What a search gives back
10.5
The report of the library
10.6
The program
11
The link to the C code
▶
11.1
The record
11.2
The exclusions
11.3
The deviations
11.4
The differential tests
11.5
Other values of the constants
11.6
Continuous integration
A
The correspondence with the C code
▶
find_points.c
sift.c
init.c
sturm.c
rp-private.h
ratpoints.h
primes.h
gen_find_points_h.c
gen_init_sieve_h.c
main.c
Dependency graph
Verifying ratpoints in Lean: a blueprint
Michael Stoll
1
Overview
1.1
What
ratpoints
computes
1.2
The four parts
1.3
The specification
1.4
The main theorems
1.5
How the proofs go
1.6
What one has to trust
1.7
What is not verified
1.8
How to read this blueprint
2
The specification
2.1
The binary form
2.2
The points
2.3
The search region
2.4
The order of
ratpoints
2.5
The options, the refusals and the outcome of a search
2.6
The reference of the delivery
2.7
The brute-force reference
3
The main theorems
3.1
The search
3.2
The points that a search finds
3.3
The refusals
3.4
The delivery and the options of the output
3.5
What the program prints
3.6
The search as a filter of the reference
3.7
The blocks, the lag and the threads
3.8
What comparator certifies
4
The set-up
4.1
The order of the checks
4.2
The squarefree binary form
4.3
The reversal
4.4
The remainder chain
4.5
The points at infinity
4.6
The exit by a prime
5
The search region and the Sturm step
5.1
The doubles
5.2
The search intervals
5.3
The bounds of the numerators
5.4
The Sturm step
5.5
Sturm’s theorem and the coverage
5.6
The region that the search uses
5.7
Deviations
6
The choice of the moduli and the blocks
6.1
The table of a prime and the loop of the tables
6.2
Prime powers and products
6.3
The cost model
6.4
The choice of the moduli and of the cut points
6.5
The blocks of the run
6.6
The correction of the moduli
6.7
Why the choice does not change the output
7
Tables and rows
7.1
The tables as
ratpoints
computes them
7.2
The closed form of a row
7.3
The tables of rows and the builders
7.4
The rows of a run
7.5
Where the model differs from the C code
8
The denominators
8.1
The 2-adic information
8.2
Odd degree: squares and divisors
8.3
Even degree: the forbidden divisors
8.4
The Jacobi test
8.5
The shapes of the loop
8.6
The order of the denominators
8.7
Where the model differs from the C code
9
The sieve of one denominator
9.1
The sieve in the C code and in the model
9.2
Bit arrays of words
9.3
Reductions by a reciprocal
9.4
The packing of the numerators
9.5
The first stage
9.6
The second stage and the extraction
9.7
The test of a candidate and the exact check
9.8
One denominator
9.9
The stages compute the plain sieve
9.10
Where the model differs from the C code
10
Delivery and the program
10.1
The callback and the delivery
10.2
The stops
10.3
The options of the output
10.4
What a search gives back
10.5
The report of the library
10.6
The program
11
The link to the C code
11.1
The record
11.2
The exclusions
11.3
The deviations
11.4
The differential tests
11.5
Other values of the constants
11.6
Continuous integration
A
The correspondence with the C code
find_points.c
sift.c
init.c
sturm.c
rp-private.h
ratpoints.h
primes.h
gen_find_points_h.c
gen_init_sieve_h.c
main.c