The blocks of the run

The run sifts the denominators of its shape in blocks (Ratpoints.Sieve.Shape.blockPlan, Ratpoints.Sieve.BlockPlan.steps), each with the cut points of the decision in force for it (Ratpoints.Sieve.findDecision, Ratpoints.Sieve.runBlock), the loop of the shape over the steps of the block (Ratpoints.Sieve.Shape.blockLoop) handing each denominator that passes the tests of the shape to the sieve of one denominator (Ratpoints.Sieve.siftDen). The blocks of the run, in order, visit the denominators of the listing of the shape (Ratpoints.Sieve.Shape.dens) in its order (Ratpoints.Sieve.Shape.flatMap_blockDens), and a block delivers the points of its denominators (Ratpoints.Sieve.blockDens) that pass the tests of the shape, each with the entries of the first three stages of its decision (Ratpoints.Sieve.denPoints), keeps a store of the tables of rows that fits all the entries, and, when the callback does not stop the search, reports the sum of the counts of its denominators (Ratpoints.Sieve.denCounts) with its decision, a closed form (Ratpoints.Sieve.blockReport) that depends neither on the callback nor on the flags of the output (Ratpoints.Sieve.runBlock_spec).

Main definitions

• Ratpoints.Sieve.RunWords, Ratpoints.Sieve.denPoints, Ratpoints.Sieve.denCounts: the words of the classes and the ranges of the numerators that the deliveries are stated for, the points of a denominator, and the counts of its sieve.
• Ratpoints.Sieve.IsRunEntries: what the run needs of its sieve entries.
• Ratpoints.Sieve.blockDens: the denominators of a block, before the tests of the shape.
• Ratpoints.Sieve.blockReport: the report of a block in closed form.

Main statements

• Ratpoints.Sieve.siftDen_spec: the contract of the step of the blocks, the sieve of one denominator with the entries cut by a decision.
• Ratpoints.Sieve.Shape.flatMap_blockDens: the blocks of the run visit the denominators of the listing of the shape in its order; Ratpoints.Sieve.Shape.flatMap_filter_blockDens: so lists of the denominators made block by block are lists over the listing; Ratpoints.Sieve.Shape.eq_of_mem_blockDens: when the listing has no denominator twice, a denominator lies in one block at most.
• Ratpoints.Sieve.forbFits_of_forall_isForbiddenEntry, Ratpoints.Sieve.forbFits_fst_run_runSetup: the forbidden divisors of the loop of the tables have what the loop of the word shape needs, and so has the shape that Ratpoints.Sieve.runSetup chooses with them.
• Ratpoints.Sieve.runBlock_spec: the contract of one block.

Implementation notes

The store frame of the sieve of one denominator (Ratpoints.Sieve.RowStore.Fits.fits_run_sift) is in Ratpoints.Proof.Sift, the loops of the shapes in Ratpoints.Proof.BlockLoops, the plan of the blocks and the well-formed decisions (Ratpoints.Sieve.DecisionWF) in Ratpoints.Proof.BlockPlan, and the listing of the shape, a definition of the proofs, in Ratpoints.Proof.Shapes; the contract of the run over the blocks with the correction of the moduli is in Ratpoints.Proof.Correction.

One denominator of a block

def Ratpoints.Sieve.RunWords (cls : Vector NumClass 64) (iv : Array IntervalBounds) (H bLow bHigh : ℕ) (x : Vector UInt64 64 × (ℕ → List (ℤ × ℤ))) : Prop

The words x.1 of the classes modulo 64 that the classes cls pack, and the ranges x.2 b of the numerators that the bounds iv of the search intervals give for the denominators b from bLow to bHigh (Ratpoints.Sieve.RangesFor), for the height H: what the deliveries of the run are stated for, since the program does not mention them.

Equations

• Ratpoints.Sieve.RunWords cls iv H bLow bHigh x = ((∀ b < 64, cls[b]!.Packs x.1[b]!) ∧ ∀ (b : ℕ), bLow ≤ b → b ≤ bHigh → Ratpoints.Sieve.RangesFor iv b H (x.2 b))

def Ratpoints.Sieve.denPoints (c : List ℤ) (d H : ℕ) (fl : CheckFlags) (es : List SieveEntry) (x : Vector UInt64 64 × (ℕ → List (ℤ × ℤ))) (b : ℕ) : List (ℤ × ℤ × ℤ)

The points that the run delivers for the denominator b, for the polynomial of degree d with the coefficient list c, the height H, the flags fl and the sieve entries es of the first three stages, with the words x.1 of the classes and the ranges x.2 b of the numerators of Ratpoints.Sieve.RunWords: the points of the check with the flags (Ratpoints.Sieve.checkNumWith) of the numerators -H, …, H in one of the ranges that pass the word of the class of b (Ratpoints.Sieve.classBit) and survive the entries.

Equations

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

structure Ratpoints.Sieve.IsRunEntries (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (offsets : Array ℕ) : Prop

What the run needs of its sieve entries entries, the reciprocals magics of their moduli and the row offsets offsets of the packings of the classes cls: prime entries wherever no factor is counted, as the third stage needs, the tables of inverses of the factors, the reciprocals in the order of the entries, and the offsets of the classes with a pattern for all the entries, since a correction may move the cut points.

• isPrimeEntry_of_nf (e : SieveEntry) : e ∈ entries → e.nf = 0 → e.IsPrimeEntry

  An entry with no factors counted is a prime entry of the table.

• hasInverses (e : SieveEntry) : e ∈ entries → e.HasInverses

  The factors of the entries have their tables of inverses.

• magics_eq : magics.toList = List.map (fun (e : SieveEntry) => magic e.p) entries

  The reciprocals of the moduli, in the order of the entries.

• offsetsFor : OffsetsFor cls entries offsets

  The classes with a pattern have their row offsets for all the entries.

def Ratpoints.Sieve.denCounts (H sp1 : ℕ) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (iv : Array IntervalBounds) (sp2 sp3 b : ℕ) : Counters

The counts that the sieve of the denominator b adds to the counters of its block (Ratpoints.Sieve.siftCounts), for the height H, the end sp1 of the first stage, the first sp2 sieve entries of entries in the first two stages and those up to sp3 in the third, with the reciprocals magics of their moduli, the classes cls and the bounds iv of the search intervals.

Equations

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

theorem Ratpoints.Sieve.siftDen_spec {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (c : List ℤ) (d H A : ℕ) (fl : CheckFlags) (sp1 : ℕ) (entries : List SieveEntry) (magics : Array ℕ) (sp2 sp3 : ℕ) (cls : Vector NumClass 64) (offsets : Array ℕ) (iv : Array IntervalBounds) (bLow bHigh : ℕ) (hA : 1 ≤ A) (hw : IsRunEntries entries magics cls offsets) (h23 : sp2 ≤ sp3) (hnf : ∀ e ∈ List.drop sp2 entries, e.nf = 0) (hbLow : 1 ≤ bLow) (hbHigh : bHigh < 2 ^ 63) (hH : H < 2 ^ 63) (b : ℕ) (st : BlockState σ) : ⦃ (bLow ≤ b ∧ b ≤ bHigh ∧ cls[b % 64]!.bits ≠ 0) ∧ st.1.quit = false ∧ st.2.1.Fits entries ⦄ siftDen process c d H A fl sp1 (List.take sp2 entries) (List.take sp2 magics.toList) (List.take (sp3 - sp2) (List.drop sp2 entries)) (List.take (sp3 - sp2) (List.drop sp2 magics.toList)) cls offsets iv b st ⦃ fun (st' : BlockState σ) => BlockPost process (RunWords cls iv H bLow bHigh) (denPoints c d H fl (List.take sp3 entries)) (denCounts H sp1 entries magics cls iv sp2 sp3) (fun (x : RowStore) => x.Fits entries) [b] st st' ⦄

One denominator b of a block, with the first sp2 sieve entries in the first two stages and those up to sp3 in the third, delivers the points of Ratpoints.Sieve.denPoints with the first sp3 entries, for every choice of the words of the classes and the ranges of the numerators of Ratpoints.Sieve.RunWords, keeps a store of the tables of rows that fits all the entries, and adds the counts of Ratpoints.Sieve.siftCounts to the counters, for a denominator between bLow ≥ 1 and bHigh < 2 ^ 63 whose class has a pattern, entries with what the run needs of them (Ratpoints.Sieve.IsRunEntries) that count no factors from sp2 on.

The denominators of a block

def Ratpoints.Sieve.blockDens (shape : Shape) (db : UInt64) (plan : BlockPlan) (bLow bHigh i : ℕ) : List ℕ

The denominators of block i of the blocks plan of the shape shape for the denominators bLow, …, bHigh, before the tests of the shape on a single denominator: those of its steps in order (Ratpoints.Sieve.Shape.stepDens, Ratpoints.Sieve.BlockPlan.blockSteps).

Equations

• Ratpoints.Sieve.blockDens shape db plan bLow bHigh i = List.flatMap (shape.stepDens db bLow bHigh (plan.blockSeg i)) (plan.blockSteps i)

theorem Ratpoints.Sieve.Shape.flatMap_range_numSegs (shape : Shape) (db : UInt64) (bLow bHigh : ℕ) : List.flatMap (fun (seg : ℕ) => List.flatMap (shape.stepDens db bLow bHigh seg) (List.range' (shape.segment bLow bHigh seg).1 ((shape.segment bLow bHigh seg).2 + 1 - (shape.segment bLow bHigh seg).1))) (List.range shape.numSegs) = (shape.dens db bLow bHigh).run

The steps of the segments of a shape, in order, with the denominators of each step, are the denominators of the listing of the shape (Ratpoints.Sieve.Shape.dens): the squares, the divisors one after the other, the words with their denominators, and every denominator.

theorem Ratpoints.Sieve.Shape.flatMap_blockDens (shape : Shape) (db : UInt64) (bLow bHigh : ℕ) : List.flatMap (blockDens shape db (shape.blockPlan bLow bHigh).run bLow bHigh) (List.range (shape.blockPlan bLow bHigh).run.nblocks) = (shape.dens db bLow bHigh).run

The blocks of the run of a shape, in order, visit the denominators of the listing of the shape (Ratpoints.Sieve.Shape.dens) in its order: the blocks of each segment cover its steps in order (Ratpoints.Sieve.BlockPlan.WF.flatMap_blockSteps), and the steps of the segments are those of the listing (Ratpoints.Sieve.Shape.flatMap_range_numSegs).

theorem Ratpoints.Sieve.Shape.mem_dens_of_mem_blockDens {shape : Shape} {db : UInt64} {bLow bHigh i b : ℕ} (hi : i < (shape.blockPlan bLow bHigh).run.nblocks) (hb : b ∈ blockDens shape db (shape.blockPlan bLow bHigh).run bLow bHigh i) : b ∈ (shape.dens db bLow bHigh).run

A denominator of a block of the run of a shape is one of the listing of the shape.

theorem Ratpoints.Sieve.Shape.flatMap_filter_blockDens {β : Type} (shape : Shape) (db : UInt64) (cls : Vector NumClass 64) (bLow bHigh : ℕ) {F : ℕ → ℕ → List β} {G : ℕ → List β} (hF : ∀ i < (shape.blockPlan bLow bHigh).run.nblocks, ∀ b ∈ blockDens shape db (shape.blockPlan bLow bHigh).run bLow bHigh i, F i b = G b) : List.flatMap (fun (i : ℕ) => List.flatMap (F i) (List.filter (fun (b : ℕ) => (shape.keep cls b).run) (blockDens shape db (shape.blockPlan bLow bHigh).run bLow bHigh i))) (List.range (shape.blockPlan bLow bHigh).run.nblocks) = List.flatMap G (List.filter (fun (b : ℕ) => (shape.keep cls b).run) (shape.dens db bLow bHigh).run)

The blocks of the run of a shape, each delivering for its denominators that pass the tests of the shape the lists F i b, which agree with the lists G b of the denominators, deliver the lists G b of the denominators of the listing of the shape that pass its tests, in order.

theorem Ratpoints.Sieve.Shape.eq_of_mem_blockDens {shape : Shape} {db : UInt64} {bLow bHigh i j b : ℕ} (hnd : (shape.dens db bLow bHigh).run.Nodup) (hi : i < (shape.blockPlan bLow bHigh).run.nblocks) (hj : j < (shape.blockPlan bLow bHigh).run.nblocks) (hbi : b ∈ blockDens shape db (shape.blockPlan bLow bHigh).run bLow bHigh i) (hbj : b ∈ blockDens shape db (shape.blockPlan bLow bHigh).run bLow bHigh j) : i = j

When the listing of the shape has no denominator twice, a denominator lies in one block of the run at most.

theorem Ratpoints.Sieve.IsForbiddenEntry.mem_primeTable {c : List ℤ} {d bHigh : ℕ} {e : ForbiddenEntry} (h : IsForbiddenEntry c d bHigh e) : e.p ∈ primeTable

A forbidden divisor tested with words that the loop of the tables may record is a prime of the table, with the words of Ratpoints.Sieve.forbiddenRow.

theorem Ratpoints.Sieve.forbFits_of_forall_isForbiddenEntry {c : List ℤ} {d bHigh : ℕ} {forb : List ForbiddenEntry} (h : ∀ e ∈ forb, IsForbiddenEntry c d bHigh e) : ForbFits forb

Forbidden divisors tested with words that the loop of the tables may record have what the loop of a block of the word shape needs: positive primes of the table, below 2 ^ 32, with their reciprocals (Ratpoints.Sieve.IsForbiddenEntry.magic_eq).

theorem Ratpoints.Sieve.forbFits_fst_run_runSetup {c : List ℤ} {d bHigh' : ℕ} (useSquares : Bool) (us1 : Option (List Setup.DenInfo × List ℕ)) (checkDenom useJacobi : Bool) {forb : List ForbiddenEntry} (forbVal : List ForbiddenVal) (lcf : ℤ) (H bHigh : ℕ) (domain : List (Double × Double)) (h : ∀ e ∈ forb, IsForbiddenEntry c d bHigh' e) : (runSetup useSquares us1 checkDenom useJacobi forb forbVal lcf H bHigh domain).run.1.ForbFits

The shape that Ratpoints.Sieve.runSetup chooses with forbidden divisors tested with words that the loop of the tables may record has what its loops need.

One block

theorem Ratpoints.Sieve.Shape.loopFits_run_blockPlan {shape : Shape} (hf : shape.ForbFits) (bLow bHigh : ℕ) : LoopFits (shape.blockPlan bLow bHigh).run bLow bHigh shape

The blocks of the run of a shape have what its loops need, for the word shape with forbidden divisors that have what the loop needs: the first segment from the word of bLow to that of bHigh.

def Ratpoints.Sieve.blockReport (H sp1 : ℕ) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh : ℕ) (decs : Array Decision) (i : ℕ) : BlockStat

The report of block i of the run with the decisions decs, in closed form: the counts of the sieve of its denominators that pass the tests of the shape (Ratpoints.Sieve.denCounts), with the ends of the second and the third stage of the decision in force for it (Ratpoints.Sieve.findDecision), the index of that decision and its ends; what Ratpoints.Sieve.runBlock reports when the callback does not stop the search (Ratpoints.Sieve.runBlock_spec), for the height H, the end sp1 of the first stage, the sieve entries entries with the reciprocals magics of their moduli, the classes cls, the word db of the classes that admit a numerator, the shape shape, the bounds iv of the search intervals and the denominators from bLow to bHigh.

Equations

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

theorem Ratpoints.Sieve.runBlock_spec {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (c : List ℤ) (d H A : ℕ) (fl : CheckFlags) (sp1 : ℕ) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (offsets : Array ℕ) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh : ℕ) (plan : BlockPlan) (decs : Array Decision) (i : ℕ) (store : RowStore) (r : Delivery σ) : ⦃ r.quit = false ∧ 1 ≤ A ∧ IsRunEntries entries magics cls offsets ∧ (∀ j < 64, db.toBitVec.getLsbD j = (cls[j]!.bits != 0)) ∧ DecisionWF entries sp1 decs[(findDecision decs i).run]! ∧ plan = (shape.blockPlan bLow bHigh).run ∧ shape.ForbFits ∧ i < plan.nblocks ∧ 1 ≤ bLow ∧ bHigh < 2 ^ 63 ∧ H < 2 ^ 63 ∧ store.Fits entries ⦄ runBlock process c d H A fl sp1 entries magics cls offsets db shape iv bLow bHigh plan decs i store r ⦃ fun (res : Delivery σ × RowStore × BlockStat) => res.2.1.Fits entries ∧ (∀ (x : Vector UInt64 64 × (ℕ → List (ℤ × ℤ))), RunWords cls iv H bLow bHigh x → res.1 = Delivery.deliver process r (List.flatMap (denPoints c d H fl (List.take decs[(findDecision decs i).run]!.sp3 entries) x) (List.filter (fun (b : ℕ) => (shape.keep cls b).run) (blockDens shape db plan bLow bHigh i)))) ∧ (res.1.quit = false → res.2.2 = blockReport H sp1 entries magics cls db shape iv bLow bHigh decs i) ⦄

Block i of the run of a shape, with the decision in force for it, delivers the points of the denominators of the block (Ratpoints.Sieve.blockDens) that pass the tests of the shape, in order, each with the first sp3 entries of the decision (Ratpoints.Sieve.denPoints), for every choice of the words of the classes and the ranges of the numerators of Ratpoints.Sieve.RunWords; it keeps a store of the tables of rows that fits all the entries and, when the callback does not stop the search, reports the sum of the counts of these denominators (Ratpoints.Sieve.denCounts) with the decision, its report in closed form (Ratpoints.Sieve.blockReport). The block needs a well-formed decision (Ratpoints.Sieve.DecisionWF), entries with what the run needs of them (Ratpoints.Sieve.IsRunEntries), the word db whose bits mark the classes with a pattern, the blocks of the shape (Ratpoints.Sieve.Shape.blockPlan) with i one of them, forbidden divisors of the word shape that have what its loop needs (Ratpoints.Sieve.Shape.ForbFits), the denominators from bLow ≥ 1 to bHigh < 2 ^ 63 and the height below 2 ^ 63.