The forbidden divisors #
For a polynomial of even degree d, a point (a, y, b) with m = v_p(b) ≥ 1 has the terms
c_{d-j} a ^ (d - j) b ^ j of F(a, b) of the valuations w_j + j m at p, where
w_j = v_p(c_{d-j}); when one of them alone has the least valuation, that valuation is even, and
for even j the unit part of c_{d-j} is a square modulo p
(Ratpoints.even_and_isSquare_of_sq_eq_binaryForm_of_even), the Newton polygon of the comment of
forbidden_valuations. So the valuations that Ratpoints.Sieve.forbiddenAt excludes, with the unit
parts of the coefficients (Ratpoints.Sieve.unitParts), are those of no denominator of a point, and
so are the bits of the mask of Ratpoints.Sieve.forbiddenValuations, the unit parts read from the
coefficients reduced modulo p that the table of p hands back. The forbidden divisors are
therefore sound, those that the loop of the tables records prime by prime from what each table hands
back (Ratpoints.tablesLoop), the coefficients modulo p and the entry at infinity, and those of
the further primes (Ratpoints.Sieve.forbidden): a prime tested with words divides no denominator
b ≤ bHigh of a point, since the mask holds every valuation that such a denominator can have
(Ratpoints.Sieve.allValuations) or there are no points at infinity modulo p, that is c_d is
not a square modulo p, and its words are those of Ratpoints.Sieve.forbiddenRow, bit j of word
r clear exactly when p ∣ 64 r + j (Ratpoints.Sieve.getLsbD_getElem!_forbiddenRow); a prime
tested by its valuation excludes no denominator of a point. The words of a forbidden divisor that is
one of the first Ratpoints.numPrimes primes of the table are the first p words of its row of
0, the pattern sieves0, which are those of Ratpoints.Sieve.forbiddenRow
(Ratpoints.Sieve.extract_sieves0). A forbidden divisor tested with words holds the reciprocal of
its prime (Ratpoints.Sieve.IsForbiddenEntry.magic_eq), with which the C code reduces the word
number of the first word of a block. The masks, which the C code keeps in an unsigned long, have
no bit from 40 on for an odd prime and a long b_high, so that its cap on the valuations never
binds (Ratpoints.Sieve.lt_forty_of_pow_le); the products pm p of its loops of the valuations and
the square p p of a prime of the table that its loop over the further primes compares with
b_high are longs (Ratpoints.Setup.fitsLong_mul_of_le_div,
Ratpoints.Setup.mul_self_lt_of_mem_primeTable). Ratpoints.Sieve.lt_forty_of_pow_le and
Ratpoints.Setup.fitsLong_mul_of_le_div discharge range obligations that the Deviation paragraphs
of the model state, and no proof consumes them.
Main definitions #
Ratpoints.Sieve.IsUnitPart: what an entry ofRatpoints.Sieve.unitPartssays of a coefficient.Ratpoints.Sieve.ExcludesByTerm: the terms ofF(a, b)exclude a valuation at a prime.Ratpoints.Sieve.IsForbiddenEntry,Ratpoints.Sieve.IsForbiddenVal: the forbidden divisors of the primes ofRatpoints.primeTablethat the loop of the tables may record, tested with words or by their valuations, and those tested with words thatRatpoints.Sieve.forbiddenmay add.Ratpoints.Sieve.ForbiddenVal.excludes: whether a forbidden divisor tested by its valuation excludes a denominator.
Main statements #
Ratpoints.even_and_isSquare_of_sq_eq_binaryForm_of_even: the Newton polygon at a prime.Ratpoints.Sieve.unitParts_spec,Ratpoints.Sieve.forbiddenAt_spec,Ratpoints.Sieve.forbiddenValuations_spec,Ratpoints.Sieve.allValuations_spec,Ratpoints.Sieve.forbidden_spec: the contracts of the forbidden divisors.Ratpoints.Sieve.run_forbiddenAt_eq_false_of_sq_eq,Ratpoints.Sieve.testBit_run_forbiddenValuations_eq_false_of_sq_eq: no denominator of a point has a forbidden valuation.Ratpoints.Sieve.isForbiddenEntry_of_run_examinePrime?_eq_some,Ratpoints.Sieve.isForbiddenVal_of_run_examinePrime?_eq_some: the forbidden divisor that a prime gives from what its table hands back is one that the loop of the tables may record.Ratpoints.Sieve.IsForbiddenEntry.prime,Ratpoints.Sieve.IsForbiddenEntry.words_eq,Ratpoints.Sieve.IsForbiddenEntry.magic_eq: the forbidden divisors tested with words are primes with the words ofRatpoints.Sieve.forbiddenRowand their reciprocals.Ratpoints.Sieve.IsForbiddenEntry.not_dvd,Ratpoints.Sieve.IsForbiddenVal.excludes_eq_false: the forbidden divisors let the denominator of every point through.Ratpoints.Sieve.lt_forty_of_pow_le: the cap of the loops of the valuations never binds, and the masks fit anunsigned long.
Implementation notes #
The contracts are proved with vcgen, the program logic of Lean core, with loop invariants that are
named definitions, in a file with Mathlib, since they speak of primes, their valuations and the
squares modulo a prime. A contract that needs the exact value of a component that its loop calls
takes a specification ⦃True⦄ x ⦃fun r ↦ r = Id.run x⦄ of it (Ratpoints.Setup.valuation_value
for the valuation, private ones for the components of this file), since the registered contract
would give only what it says of the value.
The Newton polygon at a prime #
The Newton polygon at a prime p (even degree): for a point (a, y, b) with
m = v_p(b) ≥ 1, whose term c_{d-j} a ^ (d - j) b ^ j of F(a, b) alone has the least
valuation w + j m, where c_{d-j} = p ^ w u with p ∤ u and p ^ (w + j m + 1) divides
c_{d-i} p ^ (i m) for every other i ≤ d, the valuation w + j m is even, and for even j the
unit part u is a square modulo p, since a ^ (d - j) and (b / p ^ m) ^ j then are.
The unit parts of the coefficients #
What an entry o of Ratpoints.Sieve.unitParts says of the coefficient x at the prime p:
none for x = 0, and otherwise the pair (w, r) with x = p ^ w u, p ∤ u, and r < p the
residue of the unit part u modulo p.
Equations
Instances For
The residue r ≠ 0 of the coefficient x modulo p, as the table of p hands it back
(Ratpoints.Sieve.examinePrime?), describes x at p with the valuation 0.
The valuation of a nonzero coefficient x with the residue r of |x| / p ^ w modulo p
(Ratpoints.Setup.valuation), and p - r for x < 0, describes x at p: the unit part of x
carries its sign.
The invariant of the loop of Ratpoints.Sieve.unitParts after k coefficients: the entries
describe the coefficients c_d, …, c_{d-k+1}.
Equations
Instances For
The contract of Ratpoints.Sieve.unitParts: for p > 1 and the coefficients cm reduced
modulo p, as the table of p hands them back (Ratpoints.Sieve.examinePrime?), its entries
describe the coefficients c_d, …, c_0 at p (Ratpoints.Sieve.IsUnitPart).
The valuations that the terms exclude #
The terms of F(a, b) exclude the valuation m at a prime, with the entries us of the
coefficients at the prime (Ratpoints.Sieve.IsUnitPart) and the table sq of the squares modulo
it: the term of some j₀, 0 or a coefficient present, has a valuation w_{j₀} + j₀ m less than
those of the other terms (the term of j = 0 counted as present), which is odd, or j₀ is even
and the residue of its unit part is not marked in sq; by the Newton polygon at the prime, no
denominator of a point then has the valuation m.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The invariant of the loop of Ratpoints.Sieve.forbiddenAt over the coefficients j ≤ k, on
the index jmin, the least valuation vmin and the flag tie: jmin is 0 or a coefficient
present, vmin is the valuation w_jmin + jmin m of its term, at most that of every term j ≤ k
(the term of j = 0 counted as present), and less than those of the others unless tie.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The step of Ratpoints.Sieve.forbiddenAt at a coefficient whose term has a valuation less than
vmin: it becomes the least one, with no tie.
The step of Ratpoints.Sieve.forbiddenAt at a coefficient whose term has the valuation vmin:
a tie.
The step of Ratpoints.Sieve.forbiddenAt at a coefficient absent or whose term has a valuation
greater than vmin: nothing changes.
The contract of Ratpoints.Sieve.forbiddenAt: it excludes the valuation m only when the
terms exclude it (Ratpoints.Sieve.ExcludesByTerm).
Ratpoints.Sieve.forbiddenAt_spec as a plain statement.
A coefficient x with the entry o at p makes x p ^ (i m) divisible by p ^ (V + 1) when
V < w + i m for the valuation w of o; for o = none, x = 0.
For a point (a, y, b) of a curve of even degree with v_p(b) = m ≥ 1, a coefficient
c_{d-j₀}, with the entry (w, r) at p, whose term has a valuation w + j₀ m less than those of
the other terms present has an even w + j₀ m, and for even j₀ a unit part whose residue r is
marked as a square modulo p (Ratpoints.even_and_isSquare_of_sq_eq_binaryForm_of_even); cm are
the coefficients reduced modulo p.
The forbidden valuations are sound. No denominator b of a point of a curve of even degree
has a valuation v_p(b) ≥ 1 at a prime p that Ratpoints.Sieve.forbiddenAt excludes, with the
unit parts of the coefficients at p (Ratpoints.Sieve.unitParts) and the squares modulo p: the
term of the least valuation would make F(a, b) a non-square
(Ratpoints.Sieve.even_and_getElem!_squaresMod_of_sq_eq), and for c_d = 0 the term of j = 0,
of the valuation 0 and the unit part 0, a square, is the least one; cm are the coefficients
reduced modulo p.
The masks of the valuations #
The invariant of the loops of Ratpoints.Sieve.forbiddenValuations and
Ratpoints.Sieve.allValuations on the mask, the valuation m and pm, for the test f of the
valuations: before the exit, pm = p ^ m with m ≥ 1, p ^ t ≤ bHigh for 1 ≤ t < m, and the
mask holds the t with 1 ≤ t < m that pass f; at the exit, the mask holds the t ≥ 1 with
p ^ t ≤ bHigh that pass f.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The step of the valuation m of the loops of Ratpoints.Sieve.forbiddenValuations and
Ratpoints.Sieve.allValuations that ends them, p ^ (m + 1) > bHigh, with the bit of m set when
m passes f.
The step of the valuation m of the loops of Ratpoints.Sieve.forbiddenValuations and
Ratpoints.Sieve.allValuations that goes on, with the bit of m set when m passes f.
The exit of the loops of Ratpoints.Sieve.forbiddenValuations and
Ratpoints.Sieve.allValuations at p ^ m > bHigh.
The measure of the loops of Ratpoints.Sieve.forbiddenValuations and
Ratpoints.Sieve.allValuations drops with each step that goes on: pm p ≤ bHigh, and pm p > pm
since pm = p ^ m ≥ 1 and p > 1.
The step of the loops of Ratpoints.Sieve.forbiddenValuations and
Ratpoints.Sieve.allValuations that goes on, with the measure.
The contract of Ratpoints.Sieve.forbiddenValuations: bit m of the mask is set exactly for
the m ≥ 1 with p ^ m ≤ bHigh that Ratpoints.Sieve.forbiddenAt excludes. The loop ends for
p > 1, since pm = p ^ m grows and stays at most bHigh while it goes on.
The mask of the forbidden valuations at a prime p, with the coefficients cm reduced modulo
p, has no bit v_p(b) for the denominator b of a point of a curve of even degree
(Ratpoints.Sieve.run_forbiddenAt_eq_false_of_sq_eq); its bit 0 is never set.
The forbidden divisors #
A forbidden divisor tested with words that Ratpoints.Sieve.forbiddenOfPrime gives for p
from the coefficients cm and the entry atInf at infinity is p with its words, for cm[d] = 0
and a mask of the forbidden valuations that holds every valuation a denominator can have, or for
atInf = false: for the coefficients reduced modulo p and the entry at infinity of the table of
p, when p ∣ c_d, or when there are no points at infinity modulo p.
A forbidden divisor tested by its valuation that Ratpoints.Sieve.forbiddenOfPrime gives for
p from the coefficients cm is p with the mask of the forbidden valuations of cm
(Ratpoints.Sieve.forbiddenValuations).
A forbidden divisor tested with words that an examined prime gives is sound, from the
coefficients cm reduced modulo p and the entry atInf at infinity of the table of p, as the
table hands them back: for a point (a, y, b) of a curve of even degree with b ≤ bHigh, the prime
would divide b with a valuation that the mask holds, if it holds every valuation a denominator can
have, or c_d would be a square modulo p, so that there are points at infinity modulo p.
Whether the forbidden divisor e tested by its valuation excludes the denominator b: bit
v_p(b) of its mask, for the valuation v_p(b) of Ratpoints.Setup.valuation, the test that the
tests of the word shape make with e (Ratpoints.Sieve.wordsTest).
Instances For
A forbidden divisor tested by its valuation that an examined prime p gives, from the
coefficients cm reduced modulo p, excludes no denominator of a point of a curve of even degree:
the valuations of its mask are excluded by the terms of F(a, b)
(Ratpoints.Sieve.forbiddenValuations).
A forbidden divisor tested with words that the loop of the tables (Ratpoints.tablesLoop) and
Ratpoints.Sieve.forbidden may record: the one that Ratpoints.Sieve.forbiddenOfPrime gives for a
prime p of Ratpoints.primeTable from the coefficients reduced modulo p and the entry at
infinity of the table of the reference (Ratpoints.Sieve.examinePrime), what
Ratpoints.Sieve.examinePrime? hands back for the primes the loop of the tables examines, or a
prime of the table with its words (Ratpoints.Sieve.forbiddenRow) and its reciprocal at which
c_d is not a square modulo it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A forbidden divisor tested by its valuation that the loop of the tables may record: the one
that Ratpoints.Sieve.forbiddenOfPrime gives for a prime p of Ratpoints.primeTable from the
coefficients reduced modulo p and the entry at infinity of the table of the reference
(Ratpoints.Sieve.examinePrime).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A forbidden divisor tested with words holds the reciprocal of its prime, with which the C code reduces the word number of the first word of a block.
A forbidden divisor tested with words divides no denominator b ≤ bHigh of a point of a curve
of even degree: either every valuation that such a denominator can have at p is excluded by the
terms of F(a, b) (Ratpoints.Sieve.forbiddenValuations), or c_d is not a square modulo p
while F(a, b) ≡ c_d a ^ d (mod p) for p ∣ b.
A forbidden divisor tested by its valuation excludes no denominator of a point of a curve of
even degree (Ratpoints.Sieve.ForbiddenVal.excludes_eq_false_of_run_forbiddenOfPrime_eq_inr).
The loop of the tables #
The forbidden divisor that the prime at the position k < Ratpoints.numPrimes of the table
gives from what its table hands back (Ratpoints.Sieve.examinePrime?) is that of the coefficients
reduced modulo the prime and the entry at infinity of the table of the reference.
A forbidden divisor tested with words that the prime at the position k < Ratpoints.numPrimes
gives from what its table hands back is one that the loop of the tables may record.
A forbidden divisor tested by its valuation that the prime at the position
k < Ratpoints.numPrimes gives from what its table hands back is one that the loop of the tables
may record.
The further primes #
The step of the loop of Ratpoints.Sieve.forbidden over the further primes that records a
prime of the table at which c_d is not a square modulo it, with its words: the forbidden divisors
stay of the kind that Ratpoints.Sieve.IsForbiddenEntry describes.
The contract of Ratpoints.Sieve.forbidden: from forbidden divisors ba and val of the
kinds that Ratpoints.Sieve.IsForbiddenEntry and Ratpoints.Sieve.IsForbiddenVal describe, such
as the loop of the tables records, it returns forbidden divisors of the same kinds, since the
further primes add only primes of the table with their words at which c_d is not a square modulo
the prime, and val passes through.
The longs of the C code #
The valuations m with p ^ m ≤ bHigh for p ≥ 3, as for an odd prime, and a long bHigh
are below 40, since 3 ^ 40 > 2 ^ 63: the cap m < LONG_LENGTH - 1 of the loops of
forbidden_valuations and of the valuations that a denominator can have (find_points.c:2217,
find_points.c:2636-2637), which the model drops, never binds, and the bits 1UL << m that they
set are defined, so that the masks fit an unsigned long (find_points.c:2229,
find_points.c:2638). The values pm * p of these loops, computed only for pm ≤ ⌊b_high / p⌋,
are longs too (Ratpoints.Setup.fitsLong_mul_of_le_div).