The shapes of the loop over the denominators

The lists of the denominators of the shapes of the loop (Ratpoints.Sieve.Shape.dens) and their tests on a single denominator (Ratpoints.Sieve.Shape.keep), definitions of the proofs: the denominators of each shape in the order in which the blocks of the run visit them, the reference of the loops of the blocks (Ratpoints.Sieve.Shape.blockLoop). The square shape lists the squares of a range, in increasing order, by the exact integer square roots (Ratpoints.Sieve.ceilSqrt, Ratpoints.Sieve.floorSqrt); the divisor shape lists the products s k ^ 2 of a range, each once for distinct squarefree divisors s, since s k ^ 2 determines the squarefree s and k; and the word shape lists the denominators of a range whose class admits a numerator and which no forbidden divisor tested with words divides, in increasing order (Ratpoints.Sieve.wordsDens), since bit j of word r of the words of a prime p is clear exactly when p ∣ 64 r + j (Ratpoints.Sieve.forbiddenRow) and the walk over the set bits of a word pushes their denominators, lowest first. The tests let the denominator of every point through: the class test (Ratpoints.Sieve.getElem!_twoAdic_ne_zero), the valuation test of the divisor shape with the slopes of the divisor set-up (Ratpoints.Setup.DenInfo.excludes_eq_false_of_sq_eq), and the tests of the word shape, the forbidden divisors and both Jacobi tests (Ratpoints.Sieve.IsForbiddenEntry.not_dvd, Ratpoints.Sieve.IsForbiddenVal.excludes_eq_false, Ratpoints.Sieve.run_jacobi_eq_one_of_sq_eq, Ratpoints.Sieve.run_jacobiTest_of_sq_eq). The denominators that the C code computes as longs are at most the largest denominator, those of every shape lie between the smallest and the largest, and those that pass the tests of the shape have a class with a pattern, which the packing of the numerators needs.

Main definitions

• Ratpoints.Sieve.wordBits, Ratpoints.Sieve.wordsDens, Ratpoints.Sieve.squaresDens, Ratpoints.Sieve.squares1Dens, Ratpoints.Sieve.Shape.dens, Ratpoints.Sieve.Shape.keep: the listing of the denominators of the shapes and their tests on a single denominator.

Main statements

• Ratpoints.Sieve.squaresDens_eq_filter, Ratpoints.Sieve.mem_squaresDens_iff: the square shape lists the squares of a range, in increasing order.
• Ratpoints.Sieve.mem_squares1Dens_iff, Ratpoints.Sieve.nodup_squares1Dens: the divisor shape lists the products s k ^ 2 of a range, each once for distinct squarefree divisors; Ratpoints.Sieve.squares1Dens_one_eq_filter: from the denominator 1 it lists the products e k ^ 2 ≤ H, divisor by divisor and k = 1, 2, … for each.
• Ratpoints.Sieve.run_denInfoTest_eq_true, Ratpoints.Sieve.run_denInfoTest_of_sq_eq: the valuation test of the divisor shape passes a denominator that no entry excludes, so the denominator of every point.
• Ratpoints.Sieve.getLsbD_wordBits, Ratpoints.Sieve.wordsDens_spec, Ratpoints.Sieve.toList_run_wordsDens: the word shape lists the denominators of a range whose class admits a numerator and which no forbidden divisor tested with words divides, in increasing order.
• Ratpoints.Sieve.run_wordsTest_eq_true: the tests of the word shape pass when the Jacobi tests and the valuation entries do.
• Ratpoints.Sieve.getLsbD_denBits_and_all_of_sq_eq, Ratpoints.Sieve.run_wordsTest_of_sq_eq: the class bit, the forbidden divisors tested with words and the tests of the word shape let the denominator of every point through.
• Ratpoints.Sieve.fitsLong_of_mem_squaresDens, Ratpoints.Sieve.fitsLong_of_mem_squares1Dens, Ratpoints.Sieve.fitsLong_of_mem_wordsDens: the denominators k ^ 2, s k ^ 2 and 64 w + t of the C code are longs for a long largest denominator.
• Ratpoints.Sieve.Shape.le_and_le_of_mem_dens: the denominators of every shape lie between the smallest denominator bLow ≥ 1 and the largest.
• Ratpoints.Sieve.le_and_le_and_getLsbD_of_mem_wordsDens, Ratpoints.Sieve.Shape.bits_ne_zero_of_mem_dens: a denominator of a shape that passes its tests has a class with a pattern, when the word den_bits has the bits of the classes with a pattern.

Implementation notes

The lemmas on the longs of the C code (Ratpoints.Sieve.fitsLong_of_mem_squaresDens, Ratpoints.Sieve.fitsLong_of_mem_squares1Dens, Ratpoints.Sieve.fitsLong_of_mem_wordsDens) discharge range obligations that the Deviation paragraphs of the model state, and no proof consumes them. The contracts are proved with vcgen, with loop invariants that are named definitions; the tests read the valuation and the Jacobi tests through specifications ⦃True⦄ x ⦃fun r ↦ r = Id.run x⦄ of their values (Ratpoints.Setup.valuation_value, and private ones for the Jacobi tests), so that they do not depend on the contracts of these components.

The listing of the denominators

The denominators of each shape in the order in which the blocks of the run visit them (Ratpoints.Sieve.Shape.blockLoop), listed, and the tests of a shape on a single denominator: the reference of the loops of the blocks over the denominators, which do not list them.

def Ratpoints.Sieve.wordBits (db : UInt64) (forb : List ForbiddenEntry) (bLow bHigh w : ℕ) : UInt64

The word of the 64 denominators 64 w + j that pass the class test and the forbidden divisors tested with words: the word db of the classes that admit a numerator (Ratpoints.Sieve.denBits), and-ed with word w mod p of each entry of forb (Ratpoints.Sieve.ForbiddenEntry); in the word of bLow the bits below bLow mod 64 are cleared, and in the word of bHigh those above bHigh mod 64; the word that the loop of the word shape computes (Ratpoints.Sieve.denWord).

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Sieve.wordsDens (db : UInt64) (forb : List ForbiddenEntry) (bLow bHigh : ℕ) : Id (Array ℕ)

The denominators of the word shape that their words leave, in increasing order: for each word w from ⌊bLow / 64⌋ to ⌊bHigh / 64⌋, the set bits j of its word (Ratpoints.Sieve.wordBits), lowest first (Ratpoints.Sieve.ctz), each giving the denominator 64 w + j.

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Sieve.squaresDens (bLow bHigh : ℕ) : List ℕ

The denominators of the square shape, k ^ 2 for k from ⌈√bLow⌉ to ⌊√bHigh⌋ (Ratpoints.Sieve.ceilSqrt, Ratpoints.Sieve.floorSqrt), in increasing order; for odd degree and |c_d| = 1 the denominator of every point is a square.

Equations

• Ratpoints.Sieve.squaresDens bLow bHigh = List.map (fun (k : ℕ) => k * k) (List.range' (Ratpoints.Sieve.ceilSqrt bLow) (Ratpoints.Sieve.floorSqrt bHigh + 1 - Ratpoints.Sieve.ceilSqrt bLow))

def Ratpoints.Sieve.squares1Dens (divisors : List ℕ) (bLow bHigh : ℕ) : List ℕ

The denominators of the divisor shape: for each divisor s in turn (Ratpoints.Setup.setupUs1), s k ^ 2 for k from ⌈√(⌊(bLow - 1) / s⌋ + 1)⌉ to ⌊√⌊bHigh / s⌋⌋ (Ratpoints.Sieve.ceilSqrt, Ratpoints.Sieve.floorSqrt), that is for the k with bLow ≤ s k ^ 2 ≤ bHigh, in increasing order of k; in increasing order for each divisor, not as a whole.

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Sieve.Shape.dens (s : Shape) (db : UInt64) (bLow bHigh : ℕ) : Id (List ℕ)

The denominators of the shape s from bLow to bHigh, in the order of its loop, before its tests on a single denominator: for the squares and the divisors those of Ratpoints.Sieve.squaresDens and Ratpoints.Sieve.squares1Dens, for the words those that their words leave (Ratpoints.Sieve.wordsDens, with the class test and the forbidden divisors tested with words, for the word db of the classes that admit a numerator), and otherwise bLow, …, bHigh.

Equations

• Ratpoints.Sieve.Shape.squares.dens db bLow bHigh = pure (Ratpoints.Sieve.squaresDens bLow bHigh)
• (Ratpoints.Sieve.Shape.squares1 info divisors).dens db bLow bHigh = pure (Ratpoints.Sieve.squares1Dens divisors bLow bHigh)
• (Ratpoints.Sieve.Shape.words forb forbVal useJacobi fast lcf).dens db bLow bHigh = do let __do_lift ← Ratpoints.Sieve.wordsDens db forb bLow bHigh pure __do_lift.toList
• Ratpoints.Sieve.Shape.all.dens db bLow bHigh = pure (List.range' bLow (bHigh + 1 - bLow))

def Ratpoints.Sieve.Shape.keep (s : Shape) (cls : Vector NumClass 64) (b : ℕ) : Id Bool

The tests of the shape s on a single denominator b: the class test, that the pattern of the class of b modulo 64 among the classes cls (Ratpoints.Sieve.numClasses) is not 0, that is, that the class admits a numerator, and for the divisors then the valuation test (Ratpoints.Sieve.denInfoTest); for the words the tests of Ratpoints.Sieve.wordsTest, the class test being made by the words, with den_bits.

Equations

• Ratpoints.Sieve.Shape.squares.keep cls b = pure (cls[b % 64]!.bits != 0)
• (Ratpoints.Sieve.Shape.squares1 info divisors).keep cls b = if (cls[b % 64]!.bits != 0) = true then Ratpoints.Sieve.denInfoTest info b else pure false
• (Ratpoints.Sieve.Shape.words forb forbVal useJacobi fast lcf).keep cls b = Ratpoints.Sieve.wordsTest forbVal useJacobi fast lcf b
• Ratpoints.Sieve.Shape.all.keep cls b = pure (cls[b % 64]!.bits != 0)

The square shapes

theorem Ratpoints.Sieve.ceilSqrt_le_iff {n k : ℕ} (hn : 1 ≤ n) : ceilSqrt n ≤ k ↔ n ≤ k * k

theorem Ratpoints.Sieve.le_floorSqrt_iff {n k : ℕ} : k ≤ floorSqrt n ↔ k * k ≤ n

theorem Ratpoints.Sieve.mem_squaresDens_iff {bLow bHigh b : ℕ} (hbLow : 1 ≤ bLow) : b ∈ squaresDens bLow bHigh ↔ bLow ≤ b ∧ b ≤ bHigh ∧ ∃ (k : ℕ), b = k * k

theorem Ratpoints.Sieve.pairwise_lt_squaresDens (bLow bHigh : ℕ) : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (squaresDens bLow bHigh)

theorem Ratpoints.Sieve.squaresDens_eq_filter {bLow : ℕ} (hbLow : 1 ≤ bLow) (bHigh : ℕ) : squaresDens bLow bHigh = List.filter (fun (b : ℕ) => b.sqrt * b.sqrt == b) (List.range' bLow (bHigh + 1 - bLow))

The square shape lists the squares from bLow ≥ 1 to bHigh, in increasing order.

theorem Ratpoints.Sieve.mem_range'_ceilSqrt_iff {s bLow bHigh k : ℕ} (hs : 0 < s) (hbLow : 1 ≤ bLow) : k ∈ List.range' (ceilSqrt ((bLow - 1) / s + 1)) (floorSqrt (bHigh / s) + 1 - ceilSqrt ((bLow - 1) / s + 1)) ↔ bLow ≤ s * k * k ∧ s * k * k ≤ bHigh

The segment of the divisor s > 0 in the divisor shape: bLow ≤ s k ^ 2 ≤ bHigh exactly for the k from ⌈√(⌊(bLow - 1) / s⌋ + 1)⌉ to ⌊√⌊bHigh / s⌋⌋, for bLow ≥ 1.

theorem Ratpoints.Sieve.mem_squares1Dens_iff {divisors : List ℕ} (hpos : ∀ s ∈ divisors, 0 < s) {bLow : ℕ} (hbLow : 1 ≤ bLow) {bHigh b : ℕ} : b ∈ squares1Dens divisors bLow bHigh ↔ bLow ≤ b ∧ b ≤ bHigh ∧ ∃ s ∈ divisors, ∃ (k : ℕ), b = s * k * k

The products s k ^ 2 of the divisor shape with bLow ≤ s k ^ 2 ≤ bHigh, for positive divisors and bLow ≥ 1.

theorem Ratpoints.Sieve.squares1Dens_one_eq_filter {divisors : List ℕ} (hpos : ∀ e ∈ divisors, 0 < e) (H : ℕ) : squares1Dens divisors 1 H = List.filter (fun (x : ℕ) => decide (x ≤ H)) (List.flatMap (fun (e : ℕ) => List.map (fun (k : ℕ) => e * k ^ 2) (List.range' 1 H)) divisors)

The divisor shape from the smallest denominator 1: for each positive divisor e in turn, the products e k ^ 2 ≤ H with k = 1, 2, ….

theorem Ratpoints.Sieve.squares1Dens_eq_filter {divisors : List ℕ} {bLow : ℕ} (hbLow : 1 ≤ bLow) (bHigh : ℕ) : squares1Dens divisors bLow bHigh = List.filter (fun (x : ℕ) => decide (bLow ≤ x)) (squares1Dens divisors 1 bHigh)

The divisor shape from the smallest denominator bLow ≥ 1 is the one from 1 without the denominators below bLow (Ratpoints.Sieve.mem_range'_ceilSqrt_iff); a divisor 0 gives an empty segment in both.

theorem Ratpoints.Sieve.nodup_squares1Dens {divisors : List ℕ} (hnd : divisors.Nodup) (hsq : ∀ s ∈ divisors, Squarefree s) (bLow bHigh : ℕ) : (squares1Dens divisors bLow bHigh).Nodup

The divisor shape lists each denominator once, for distinct squarefree divisors: s k ^ 2 determines the squarefree s (Nat.eq_of_mul_sq_eq_mul_sq), and the segments start at k ≥ 1.

theorem Ratpoints.Sieve.fitsLong_of_mem_squaresDens {bLow bHigh b : ℕ} (hb : b ∈ squaresDens bLow bHigh) (hH : bHigh < 2 ^ 63) : fitsLong ↑b = true

The denominators k ^ 2 of the square shape, which the C code computes as longs (find_points.c:3922), are at most bHigh, and so longs for a long bHigh.

theorem Ratpoints.Sieve.fitsLong_of_mem_squares1Dens {divisors : List ℕ} {bLow bHigh b : ℕ} (hb : b ∈ squares1Dens divisors bLow bHigh) (hH : bHigh < 2 ^ 63) : fitsLong ↑b = true

The denominators s k ^ 2 of the divisor shape, which the C code computes as longs (find_points.c:3940), are at most bHigh, and so longs for a long bHigh, as is s k ≤ s k ^ 2 for k ≥ 1.

The valuation test of the divisor shape

theorem Ratpoints.Sieve.run_denInfoTest_eq_true {info : List Setup.DenInfo} {b : ℕ} (hinfo : ∀ e ∈ info, e.excludes b = false) : (denInfoTest info b).run = true

theorem Ratpoints.Sieve.run_denInfoTest_of_sq_eq {c : List ℤ} {bHigh : ℕ} {info : List Setup.DenInfo} {divisors : List ℕ} (hd : degree c % 2 = 1) (hs : (Setup.setupUs1 c (degree c) bHigh).run = some (info, divisors)) {a y : ℤ} {b : ℕ} (hb : b ≠ 0) (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : (denInfoTest info b).run = true

The valuation test of the divisor shape, with the slopes of the divisor set-up, lets the denominator of every point through: for v_p(b) ≥ slope the term c_d a ^ d b of F(a, b) alone has the least valuation v_p(c_d) + v_p(b), which is then even (Ratpoints.Setup.DenInfo.excludes_eq_false_of_sq_eq).

The word shape

theorem Ratpoints.Sieve.getLsbD_wordBits (db : UInt64) (forb : List ForbiddenEntry) {bLow bHigh w : ℕ} (hlo : bLow / 64 ≤ w) (hhi : w ≤ bHigh / 64) (t : ℕ) : (wordBits db forb bLow bHigh w).toBitVec.getLsbD t = ((db.toBitVec.getLsbD t && forb.all fun (e : ForbiddenEntry) => e.words[w % e.p]!.toBitVec.getLsbD t) && decide (bLow ≤ 64 * w + t) && decide (64 * w + t ≤ bHigh))

The bits of the word of Ratpoints.Sieve.wordBits for a word w of the range from ⌊bLow / 64⌋ to ⌊bHigh / 64⌋: bit t is set exactly when bit t of db and of word w mod p of every entry p are set and bLow ≤ 64 w + t ≤ bHigh.

theorem Ratpoints.Sieve.wordsDens_spec (db : UInt64) (forb : List ForbiddenEntry) (bLow bHigh : ℕ) : ⦃ True ⦄ wordsDens db forb bLow bHigh ⦃ fun (out : Array ℕ) => out.toList = List.flatMap (fun (w : ℕ) => List.map (fun (x : ℕ) => 64 * w + x) (List.filter (wordBits db forb bLow bHigh w).toBitVec.getLsbD (List.range 64))) (List.range' (bLow / 64) (bHigh / 64 + 1 - bLow / 64)) ⦄

The contract of Ratpoints.Sieve.wordsDens: for each word w of the range, the denominators 64 w + t of the set bits t of its word (Ratpoints.Sieve.wordBits), lowest first. The loops over the set bits end, since clearing the lowest set bit makes a word other than 0 smaller.

theorem Ratpoints.Sieve.toList_run_wordsDens {db : UInt64} {forb : List ForbiddenEntry} (hpos : ∀ e ∈ forb, 0 < e.p) (hwords : ∀ e ∈ forb, e.words = forbiddenRow e.p) (bLow bHigh : ℕ) : (wordsDens db forb bLow bHigh).run.toList = List.filter (fun (b : ℕ) => db.toBitVec.getLsbD (b % 64) && forb.all fun (e : ForbiddenEntry) => b % e.p != 0) (List.range' bLow (bHigh + 1 - bLow))

The word shape lists the denominators b from bLow to bHigh, in increasing order, whose class b mod 64 has its bit in db and which no forbidden divisor tested with words divides, for entries with the words of Ratpoints.Sieve.forbiddenRow: bit j of word w mod p of the entry p is clear exactly when p ∣ 64 w + j.

theorem Ratpoints.Sieve.le_and_le_and_getLsbD_of_mem_wordsDens {db : UInt64} {forb : List ForbiddenEntry} {bLow bHigh b : ℕ} (hb : b ∈ (wordsDens db forb bLow bHigh).run.toList) : bLow ≤ b ∧ b ≤ bHigh ∧ db.toBitVec.getLsbD (b % 64) = true

The word shape lists only denominators from bLow to bHigh whose class has its bit in db.

theorem Ratpoints.Sieve.fitsLong_of_mem_wordsDens {db : UInt64} {forb : List ForbiddenEntry} {bLow bHigh b : ℕ} (hb : b ∈ (wordsDens db forb bLow bHigh).run.toList) (hH : bHigh < 2 ^ 63) : fitsLong ↑b = true

The denominators 64 w + t of the word shape, which the C code computes as longs (base = w << LONG_SHIFT and b = base + RP_CTZL(b_bits), find_points.c:3991, find_points.c:4008), are at most bHigh, and so longs for a long bHigh; so is 64 w for the words w ≤ ⌊bHigh / 64⌋ (Ratpoints.Setup.fitsLong_mul_of_le_div).

The bounds of the denominators of the shapes

theorem Ratpoints.Sieve.le_and_le_of_mem_squares1Dens {divisors : List ℕ} {bLow bHigh b : ℕ} (hbLow : 1 ≤ bLow) (hb : b ∈ squares1Dens divisors bLow bHigh) : bLow ≤ b ∧ b ≤ bHigh

For any divisors, without positivity: a divisor 0 gives an empty segment.

theorem Ratpoints.Sieve.Shape.le_and_le_of_mem_dens (s : Shape) {db : UInt64} {bLow bHigh b : ℕ} (hbLow : 1 ≤ bLow) (hb : b ∈ (s.dens db bLow bHigh).run) : bLow ≤ b ∧ b ≤ bHigh

The denominators of every shape lie between bLow ≥ 1 and bHigh, as the test for common factors on the words of the C code needs (Ratpoints.Sieve.sift_spec).

theorem Ratpoints.Sieve.Shape.bits_ne_zero_of_mem_dens (s : Shape) {db : UInt64} {cls : Vector NumClass 64} (hdb : ∀ j < 64, db.toBitVec.getLsbD j = (cls[j]!.bits != 0)) {bLow bHigh b : ℕ} (hb : b ∈ (s.dens db bLow bHigh).run) (hk : (s.keep cls b).run = true) : cls[b % 64]!.bits ≠ 0

A denominator of a shape that passes its tests has a class with a pattern, when the bits of the word db are those of the classes with a pattern: the class test of the other shapes reads the pattern, and the word shape lists only denominators whose class has its bit in db (Ratpoints.Sieve.le_and_le_and_getLsbD_of_mem_wordsDens).

The tests of the word shape

theorem Ratpoints.Sieve.run_wordsTest_eq_true {forbVal : List ForbiddenVal} {useJacobi : Bool} {fast : Option JacobiInfo} {lcf : ℤ} {b : ℕ} (hfast : ∀ (ji : JacobiInfo), fast = some ji → (jacobiTest ji b).run = true) (hval : ∀ e ∈ forbVal, e.excludes b = false) (hjac : fast = none → useJacobi = true → (jacobi b lcf).run = 1) : (wordsTest forbVal useJacobi fast lcf b).run = true

The tests of the word shape on the denominator b pass when the Jacobi test by the tables fast passes, when they are given, when no forbidden divisor tested by its valuation excludes b, and when the binary algorithm gives the symbol 1, when the Jacobi test is on without tables.

The tests let the denominators of the points through

theorem Ratpoints.Sieve.getLsbD_denBits_and_all_of_sq_eq {c : List ℤ} {H : ℕ} (hd : degree c % 2 = 0) {forb : List ForbiddenEntry} (hforb : ∀ e ∈ forb, IsForbiddenEntry c (degree c) H e) {a y : ℤ} {b : ℕ} (hb : b ≠ 0) (hbH : b ≤ H) (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : ((denBits (twoAdic c (degree c)).run).toBitVec.getLsbD (b % 64) && forb.all fun (e : ForbiddenEntry) => b % e.p != 0) = true

For even degree, the class bit in Ratpoints.Sieve.denBits and forbidden divisors tested with words that the loop of the tables and the further primes may record for the largest denominator H (Ratpoints.Sieve.IsForbiddenEntry) let the denominator 1 ≤ b ≤ H of a point (a, y, b) through (Ratpoints.Sieve.classBit_twoAdic_of_sq_eq, Ratpoints.Sieve.IsForbiddenEntry.not_dvd): the filter of the list of the word shape (Ratpoints.Sieve.toList_run_wordsDens) keeps it.

theorem Ratpoints.Sieve.run_wordsTest_of_sq_eq {c : List ℤ} {H : ℕ} (hd : degree c % 2 = 0) {forbVal : List ForbiddenVal} (hval : ∀ e ∈ forbVal, IsForbiddenVal c (degree c) H e) (useJacobi : Bool) {a y : ℤ} {b : ℕ} (hb : b ≠ 0) (hbH : b ≤ H) (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : (wordsTest forbVal useJacobi (if useJacobi = true then (jacobiSetup (c.getD (degree c) 0) H).run else none) (c.getD (degree c) 0) b).run = true

For even degree, the tests of the word shape, with forbidden divisors tested by their valuations that the loop of the tables may record for the largest denominator H (Ratpoints.Sieve.IsForbiddenVal) and the tables of the Jacobi test when it is on, let the denominator 1 ≤ b ≤ H of a point (a, y, b) through (Ratpoints.Sieve.IsForbiddenVal.excludes_eq_false, Ratpoints.Sieve.run_jacobiTest_of_sq_eq, Ratpoints.Sieve.run_jacobi_eq_one_of_sq_eq).