The correction of the moduli and the run

The run sifts its blocks in order (Ratpoints.Sieve.sieveRun), each with the cut points of the decision for it (Ratpoints.Sieve.findDecision), and folds the counters of each block into the state of the correction (Ratpoints.Sieve.runFold), which may push a decision for the blocks from Ratpoints.adaptLag + 1 blocks later on (Ratpoints.Sieve.adaptPrimes). The counters are counted before the exact check, so that the decisions depend neither on the callback nor on the flags of the output: while the callback does not stop the search, the state of the correction is a fold of the reports of the blocks in closed form (Ratpoints.Sieve.correctionAfter), and a stop of the callback in a block ends the run before any decision that the fold of that block pushes is read. So the run delivers the points of its blocks in order, each with the decision of the block (Ratpoints.Sieve.blockDecision), and, over the denominators of its shape in the order of its loops, the points of the numerators that pass the class word and survive the entries of the first three stages of the decision of the block of the denominator, a decision that is a function of the denominator alone. The correction keeps the decisions well-formed (Ratpoints.Sieve.DecisionWF) for any values of the doubles of its cost model, and the decision of a block reads only the folds of the blocks at least Ratpoints.adaptLag + 1 blocks before it.

Main definitions

• Ratpoints.Sieve.Correction.WF: a well-formed state of the correction.
• Ratpoints.Sieve.correctionAfter, Ratpoints.Sieve.blockDecision: the state of the correction after the folds of the first blocks with their reports in closed form (Ratpoints.Sieve.blockReport), and the decision of a block, both free of the callback and the flags.
• Ratpoints.Sieve.blockPoints: the points that a block delivers.
• Ratpoints.Sieve.deliverSlots: the calling thread of a run with threads, which delivers the slots of the blocks in their order.

Main statements

• Ratpoints.Sieve.adaptPrimes_spec, Ratpoints.Sieve.runFold_spec, Ratpoints.Sieve.wf_correctionAfter: the correction keeps the decisions well-formed.
• Ratpoints.Sieve.getElem!_findDecision_correctionAfter: the lag of the correction, the decision in force for block i is the same after the folds of any k ≥ i - adaptLag blocks.
• Ratpoints.Sieve.sieveRun_spec, Ratpoints.Sieve.fst_run_sieveRun: the block lemma, the run delivers the points of its blocks in order, each with its decision.
• Ratpoints.Sieve.exists_run_sieveRun_eq_deliver: the contract of the run per denominator.
• Ratpoints.Sieve.run_deliverSlots_eq_fst_run_sieveRun: the property that the threads, which the model leaves out, preserve: the blocks sifted apart into slots with the decisions after enough folds, each with a store of its own, and delivered in their order give the output of the run.

Implementation notes

The contracts of the loops of the correction state only what the natural numbers of the C code do: no proof reads a value of the doubles, so every statement holds for whatever values the cost model computes. The run's invariant (Ratpoints.Sieve.SieveRunLoopInvariant) states the delivery for every choice of the words of the classes and the ranges of the numerators (Ratpoints.Sieve.RunWords), as the contract of one block does (Ratpoints.Sieve.runBlock_spec).

The correction keeps the decisions well-formed

def Ratpoints.Sieve.AdaptUpInvariant (start : ℕ) : Std.WP.Invariant ℕ (ℕ × Float × Float) Prop

The invariant of the loop of Ratpoints.Sieve.adaptUp over the entries from start on, on the new end of the second stage: at least start, and at most start plus the entries passed.

Equations

• Ratpoints.Sieve.AdaptUpInvariant start pref x✝ st = (start ≤ st.1 ∧ st.1 ≤ start + pref.length)

theorem Ratpoints.Sieve.AdaptUpInvariant.push {start want cur : ℕ} {pref : List ℕ} (h : start ≤ want ∧ want ≤ start + pref.length) : start ≤ want + 1 ∧ want + 1 ≤ start + (pref ++ [cur]).length

theorem Ratpoints.Sieve.AdaptUpInvariant.done {start want m cur : ℕ} {pref suff : List ℕ} (hl : ForIn.toList [start:m] = pref ++ cur :: suff) (h : start ≤ want ∧ want ≤ start + pref.length) : start ≤ want ∧ want ≤ start + (ForIn.toList [start:m]).length

theorem Ratpoints.Sieve.adaptUp_spec (es : Array SieveEntry) (start : ℕ) (level chance rate s costSurv ct U D : Float) : ⦃ True ⦄ adaptUp es start level chance rate s costSurv ct U D ⦃ fun (r : ℕ × Float × Float) => start ≤ r.1 ∧ r.1 ≤ start + (es.size - start) ⦄

The walk of the correction up from the end start of the second stage takes some of the entries from start on: for any values of the doubles, the new end is at least start and at most the number of the entries, if start is.

def Ratpoints.Sieve.AdaptDownInvariant (es : Array SieveEntry) (sp1 sp2 : ℕ) : Std.WP.WhileInvariant (ℕ × Float × Float × ℕ) Prop

The invariant of the loop of Ratpoints.Sieve.adaptDown on the new end want of the second stage and the position n of the next entry, from the end sp2: want at most sp2 and at least sp1 if sp2 is, the entries from want to sp2 primes of the table, and n the position just below want while it is not 0.

Equations

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

theorem Ratpoints.Sieve.adaptDownInvariant_init (es : Array SieveEntry) (sp1 sp2 : ℕ) : sp2 ≤ sp2 ∧ (sp1 ≤ sp2 → sp1 ≤ sp2) ∧ (∀ (k : ℕ), sp2 ≤ k → k < sp2 → es[k]!.nf = 0) ∧ (sp2 - 1 = 0 ∨ sp2 = sp2 - 1 + 1)

theorem Ratpoints.Sieve.AdaptDownInvariant.sub_one {es : Array SieveEntry} {sp1 sp2 want n : ℕ} (h : want ≤ sp2 ∧ (sp1 ≤ sp2 → sp1 ≤ want) ∧ (∀ (k : ℕ), want ≤ k → k < sp2 → es[k]!.nf = 0) ∧ (n = 0 ∨ want = n + 1)) (hc : (decide (sp1 < n) && es[n]!.nf == 0) = true) : n - 1 < n ∧ want - 1 ≤ sp2 ∧ (sp1 ≤ sp2 → sp1 ≤ want - 1) ∧ (∀ (k : ℕ), want - 1 ≤ k → k < sp2 → es[k]!.nf = 0) ∧ (n - 1 = 0 ∨ want - 1 = n - 1 + 1)

theorem Ratpoints.Sieve.adaptDown_spec (es : Array SieveEntry) (sp1 sp2 : ℕ) (level chance rate s costSurv ct U D : Float) : ⦃ True ⦄ adaptDown es sp1 sp2 level chance rate s costSurv ct U D ⦃ fun (r : ℕ × Float) => r.1 ≤ sp2 ∧ (sp1 ≤ sp2 → sp1 ≤ r.1) ∧ ∀ (k : ℕ), r.1 ≤ k → k < sp2 → es[k]!.nf = 0 ⦄

The walk of the correction down from the end sp2 of the second stage drops some of the entries below sp2, only primes of the table and never below sp1: for any values of the doubles, the new end is at most sp2, at least sp1 if sp2 is, and the entries from it to sp2 count no factors.

def Ratpoints.Sieve.AdaptThirdInvariant (es : Array SieveEntry) (sp2 : ℕ) : Std.WP.WhileInvariant (Float × ℕ) Prop

The invariant of the loop of Ratpoints.Sieve.adaptThird on the end sp3 of the third stage, from the end sp2 of the second: at least sp2 and at most sp2 and the number of the entries.

Equations

• Ratpoints.Sieve.AdaptThirdInvariant es sp2 = Std.WP.WhileInvariant.mk fun (x : Bool) (st : Float × ℕ) => sp2 ≤ st.2 ∧ st.2 ≤ sp2 + (es.size - sp2)

theorem Ratpoints.Sieve.adaptThird_spec (es : Array SieveEntry) (c : RunCounts) (sp2 : ℕ) (q checkRel level chance r2 s : Float) : ⦃ True ⦄ adaptThird es c sp2 q checkRel level chance r2 s ⦃ fun (r : ℕ) => sp2 ≤ r ∧ r ≤ sp2 + (es.size - sp2) ⦄

The correction of the third stage takes some of the entries from the end sp2 of the second stage on: for any values of the doubles, the end of the third stage is at least sp2 and at most the number of the entries, if sp2 is.

theorem Ratpoints.Sieve.adaptSecond_spec (es : Array SieveEntry) (c : RunCounts) (sp1 : ℕ) (level chance r2 checkRel ct U D : Float) : ⦃ DecisionWF es.toList sp1 { block := 0, sp2 := c.sp2, sp3 := c.sp2 } ⦄ adaptSecond es c sp1 level chance r2 checkRel ct U D ⦃ fun (r : ℕ × Float) => DecisionWF es.toList sp1 { block := 0, sp2 := r.1, sp3 := r.1 } ⦄

The correction of the end of the second stage keeps it well-formed.

theorem Ratpoints.Sieve.adaptPrimes_spec (s : SieveOptions) (P : Params) (es : Array SieveEntry) (c : RunCounts) (sp2 sp3 : ℕ) : ⦃ DecisionWF es.toList P.sp1 { block := 0, sp2 := sp2, sp3 := sp3 } ∧ DecisionWF es.toList P.sp1 { block := 0, sp2 := c.sp2, sp3 := c.sp2 } ⦄ adaptPrimes s P es c sp2 sp3 ⦃ fun (r : ℕ × ℕ × UInt64) => DecisionWF es.toList P.sp1 { block := 0, sp2 := r.1, sp3 := r.2.1 } ⦄

The correction of the choice of the moduli keeps the decision well-formed.

The fold of a block

@[simp]

theorem Ratpoints.Sieve.RunCounts.sp2_fold (c : RunCounts) (sp2 : ℕ) (k : Counters) : (c.fold sp2 k).sp2 = sp2

The counters of the second stage on, after a fold, are counted under the end of the second stage of the block folded.

structure Ratpoints.Sieve.Correction.WF (es : List SieveEntry) (sp1 : ℕ) (corr : Correction) : Prop

The state of the correction of the moduli is well-formed for the sieve entries es and the end sp1 of the first stage: its decisions, the first for block 0, well-formed (Ratpoints.Sieve.DecisionWF), as are the latest decision and the end of the second stage that the counters of the run were counted under.

• size_pos : 0 < corr.decisions.size

  There is a decision.

• block_zero : corr.decisions[0]!.block = 0

  The first decision is for block 0.

• decisionWF (d : Decision) : d ∈ corr.decisions → DecisionWF es sp1 d

  Every decision is well-formed.

• latest : DecisionWF es sp1 { block := 0, sp2 := corr.sp2, sp3 := corr.sp3 }

  The latest decision is well-formed.

• counted : DecisionWF es sp1 { block := 0, sp2 := corr.cnt.sp2, sp3 := corr.cnt.sp2 }

  The end of the second stage of the counters is one of a well-formed decision.

theorem Ratpoints.Sieve.Correction.wf_start {es : List SieveEntry} {sp1 sp2 sp3 : ℕ} (adaptAt : UInt64) (h : DecisionWF es sp1 { block := 0, sp2 := sp2, sp3 := sp3 }) : WF es sp1 (start sp2 sp3 adaptAt)

theorem Ratpoints.Sieve.Correction.WF.inForce {es : List SieveEntry} {sp1 : ℕ} {corr : Correction} (h : WF es sp1 corr) (i : ℕ) : Decision.InForce corr.decisions i (findDecision corr.decisions i).run

The decision in force for block i among the decisions of a well-formed state of the correction (Ratpoints.Sieve.findDecision_spec).

theorem Ratpoints.Sieve.Correction.WF.decisionWF_findDecision {es : List SieveEntry} {sp1 : ℕ} {corr : Correction} (h : WF es sp1 corr) (i : ℕ) : DecisionWF es sp1 corr.decisions[(findDecision corr.decisions i).run]!

The decision in force for a block among the decisions of a well-formed state of the correction is well-formed.

theorem Ratpoints.Sieve.runFold_spec (s : SieveOptions) (P : Params) (es : List SieveEntry) (st : Correction) (b : BlockStat) : ⦃ Correction.WF es P.sp1 st ∧ b.dec < st.decisions.size ⦄ runFold s P es.toArray st b ⦃ fun (st' : Correction) => Correction.WF es P.sp1 st' ⦄

The fold of a block reported with one of the decisions keeps the correction well-formed: the counters are then counted under the end of the second stage of that decision, and the decision that the correction may push is well-formed (Ratpoints.Sieve.adaptPrimes_spec).

theorem Ratpoints.Sieve.runFold_decisions_spec (s : SieveOptions) (P : Params) (es : Array SieveEntry) (st : Correction) (b : BlockStat) : ⦃ True ⦄ runFold s P es st b ⦃ fun (st' : Correction) => st'.folded = st.folded + 1 ∧ ∃ (L : List Decision), st'.decisions.toList = st.decisions.toList ++ L ∧ ∀ d ∈ L, d.block = st.folded + adaptLag + 1 ⦄

The fold of a block counts one more block folded and pushes at most a decision, for the blocks from Ratpoints.adaptLag + 1 blocks later on.

The correction of the run in closed form

def Ratpoints.Sieve.correctionAfter (H : ℕ) (s : SieveOptions) (P : Params) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh : ℕ) : ℕ → Correction

The state of the correction of the moduli after the folds of the first k blocks of the run (Ratpoints.Sieve.runFold), each with its report in closed form (Ratpoints.Sieve.blockReport), from the choice (Ratpoints.Sieve.Correction.start, with the ends P.sp2 and P.sp3 and the words P.adaptAt): what the run keeps while the callback does not stop the search, a function of the arguments of the run that depends neither on the callback nor on the flags of the output, for the height H, the options s, the result P of the choice, 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.
• Ratpoints.Sieve.correctionAfter H s P entries magics cls db shape iv bLow bHigh 0 = Ratpoints.Sieve.Correction.start P.sp2 P.sp3 P.adaptAt

def Ratpoints.Sieve.blockDecision (H : ℕ) (s : SieveOptions) (P : Params) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh i : ℕ) : Decision

The decision of the correction of the moduli in force for block i of the run (Ratpoints.Sieve.findDecision), among the decisions after the folds of the blocks before it (Ratpoints.Sieve.correctionAfter), which depends neither on the callback nor on the flags of the output.

Equations

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

theorem Ratpoints.Sieve.folded_correctionAfter {H : ℕ} {s : SieveOptions} {P : Params} {entries : List SieveEntry} {magics : Array ℕ} {cls : Vector NumClass 64} {db : UInt64} {shape : Shape} {iv : Array IntervalBounds} {bLow bHigh : ℕ} (k : ℕ) : (correctionAfter H s P entries magics cls db shape iv bLow bHigh k).folded = k

The blocks folded so far.

theorem Ratpoints.Sieve.exists_toList_decisions_correctionAfter (H : ℕ) (s : SieveOptions) (P : Params) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh : ℕ) {m k : ℕ} (hmk : m ≤ k) : ∃ (L : List Decision), (correctionAfter H s P entries magics cls db shape iv bLow bHigh k).decisions.toList = (correctionAfter H s P entries magics cls db shape iv bLow bHigh m).decisions.toList ++ L ∧ ∀ d ∈ L, m + adaptLag + 1 ≤ d.block

The decisions after the folds of the first k blocks are those after the first m ≤ k followed by decisions for the blocks from m + Ratpoints.adaptLag + 1 on.

theorem Ratpoints.Sieve.size_pos_and_block_zero_correctionAfter {H : ℕ} {s : SieveOptions} {P : Params} {entries : List SieveEntry} {magics : Array ℕ} {cls : Vector NumClass 64} {db : UInt64} {shape : Shape} {iv : Array IntervalBounds} {bLow bHigh : ℕ} (k : ℕ) : 0 < (correctionAfter H s P entries magics cls db shape iv bLow bHigh k).decisions.size ∧ (correctionAfter H s P entries magics cls db shape iv bLow bHigh k).decisions[0]!.block = 0

There is a decision, and the first is for block 0.

theorem Ratpoints.Sieve.wf_correctionAfter {H : ℕ} {s : SieveOptions} {P : Params} {entries : List SieveEntry} {magics : Array ℕ} {cls : Vector NumClass 64} {db : UInt64} {shape : Shape} {iv : Array IntervalBounds} {bLow bHigh : ℕ} (hdec : DecisionWF entries P.sp1 { block := 0, sp2 := P.sp2, sp3 := P.sp3 }) (k : ℕ) : Correction.WF entries P.sp1 (correctionAfter H s P entries magics cls db shape iv bLow bHigh k)

The state of the correction of the moduli after the folds of the first k blocks of the run is well-formed, for a well-formed decision of the choice.

The decision in force for a block: the lag

theorem Ratpoints.Sieve.Decision.InForce.unique {decs : Array Decision} {i dd dd' : ℕ} (h : InForce decs i dd) (h' : InForce decs i dd') : dd = dd'

The decision in force for block i is unique: the last whose first block is at most i.

theorem Ratpoints.Sieve.findDecision_eq_of_toList_eq_append {decs decs' : Array Decision} {L : List Decision} {i : ℕ} (h0 : 0 < decs.size) (hb : decs[0]!.block = 0) (h : decs'.toList = decs.toList ++ L) (hL : ∀ d ∈ L, i < d.block) : (findDecision decs' i).run = (findDecision decs i).run

The index of the decision in force for block i among decisions of which the first is for block 0 is also that among these decisions followed by decisions for blocks after block i: the decision in force is unique (Ratpoints.Sieve.Decision.InForce.unique).

theorem Ratpoints.Sieve.getElem!_findDecision_eq_of_toList_eq_append {decs decs' : Array Decision} {L : List Decision} {i : ℕ} (h0 : 0 < decs.size) (hb : decs[0]!.block = 0) (h : decs'.toList = decs.toList ++ L) (hL : ∀ d ∈ L, i < d.block) : decs'[(findDecision decs' i).run]! = decs[(findDecision decs i).run]!

The decision in force for block i among decisions of which the first is for block 0 is also that among these decisions followed by decisions for blocks after block i.

theorem Ratpoints.Sieve.getElem!_findDecision_correctionAfter {H : ℕ} {s : SieveOptions} {P : Params} {entries : List SieveEntry} {magics : Array ℕ} {cls : Vector NumClass 64} {db : UInt64} {shape : Shape} {iv : Array IntervalBounds} {bLow bHigh i k : ℕ} (hk : i - adaptLag ≤ k) : (correctionAfter H s P entries magics cls db shape iv bLow bHigh k).decisions[(findDecision (correctionAfter H s P entries magics cls db shape iv bLow bHigh k).decisions i).run]! = blockDecision H s P entries magics cls db shape iv bLow bHigh i

The lag of the correction of the moduli: the decision in force for block i among the decisions after the folds of the first k blocks is the decision of block i (Ratpoints.Sieve.blockDecision) for every k ≥ i - Ratpoints.adaptLag, since a decision made at the fold of block j is for the blocks from j + Ratpoints.adaptLag + 1 on: block i reads only the decisions made at the folds of the blocks before block i - Ratpoints.adaptLag.

The run

def Ratpoints.Sieve.blockPoints (c : List ℤ) (d H : ℕ) (fl : CheckFlags) (s : SieveOptions) (P : Params) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh : ℕ) (x : Vector UInt64 64 × (ℕ → List (ℤ × ℤ))) (i : ℕ) : List (ℤ × ℤ × ℤ)

The points that block i of the run delivers, for the polynomial of degree d with the coefficient list c, the height H, the flags fl and the words x.1 of the classes and the ranges x.2 of the numerators of Ratpoints.Sieve.RunWords: those of its denominators (Ratpoints.Sieve.blockDens) that pass the tests of the shape, in order, each with the first sp3 sieve entries of the decision of the block (Ratpoints.Sieve.blockDecision, Ratpoints.Sieve.denPoints).

Equations

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

def Ratpoints.Sieve.SieveRunLoopInvariant {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (c : List ℤ) (d H : ℕ) (fl : CheckFlags) (s : SieveOptions) (P : Params) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh : ℕ) (r0 : Delivery σ) : Std.WP.Invariant ℕ (Correction × Delivery σ × RowStore) Prop

The invariant of the loop of Ratpoints.Sieve.sieveRun over the blocks, whose state is the correction, the delivery and the store of the tables of rows, from the delivery r0: the delivery is that of the points of the blocks done (Ratpoints.Sieve.blockPoints), for every choice of the words of the classes and the ranges of the numerators of Ratpoints.Sieve.RunWords; while the callback has not stopped the search, the correction is that after the folds of the blocks done in closed form (Ratpoints.Sieve.correctionAfter) and the store fits all the entries; and the callback has not stopped the search before the loop is done.

Equations

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

theorem Ratpoints.Sieve.sieveRunLoopInvariant_nil {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {c : List ℤ} {d H : ℕ} {fl : CheckFlags} {s : SieveOptions} {P : Params} {entries : List SieveEntry} {magics : Array ℕ} {cls : Vector NumClass 64} {db : UInt64} {shape : Shape} {iv : Array IntervalBounds} {bLow bHigh : ℕ} {r0 : Delivery σ} {st : RowStore} (hr : r0.quit = false) (hs : st.Fits entries) (l : List ℕ) : SieveRunLoopInvariant process c d H fl s P entries magics cls db shape iv bLow bHigh r0 [] l (Correction.start P.sp2 P.sp3 P.adaptAt, r0, st)

theorem Ratpoints.Sieve.SieveRunLoopInvariant.pre {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {c : List ℤ} {d H : ℕ} {fl : CheckFlags} {s : SieveOptions} {P : Params} {entries : List SieveEntry} {magics : Array ℕ} {cls : Vector NumClass 64} {db : UInt64} {shape : Shape} {iv : Array IntervalBounds} {bLow bHigh : ℕ} {r0 r1 : Delivery σ} {corr : Correction} {st : RowStore} {pref suff : List ℕ} {cur : ℕ} (hdec : DecisionWF entries P.sp1 { block := 0, sp2 := P.sp2, sp3 := P.sp3 }) (h : SieveRunLoopInvariant process c d H fl s P entries magics cls db shape iv bLow bHigh r0 pref (cur :: suff) (corr, r1, st)) : r1.quit = false ∧ DecisionWF entries P.sp1 corr.decisions[(findDecision corr.decisions cur).run]! ∧ st.Fits entries

What the block at the cursor cur needs.

theorem Ratpoints.Sieve.SieveRunLoopInvariant.quit {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {c : List ℤ} {d H : ℕ} {fl : CheckFlags} {s : SieveOptions} {P : Params} {entries : List SieveEntry} {magics : Array ℕ} {cls : Vector NumClass 64} {db : UInt64} {shape : Shape} {iv : Array IntervalBounds} {bLow bHigh : ℕ} {r0 r1 r' : Delivery σ} {corr corr' : Correction} {st st' : RowStore} {pref suff : List ℕ} {cur n : ℕ} (hl : ForIn.toList [:n] = pref ++ cur :: suff) (h : SieveRunLoopInvariant process c d H fl s P entries magics cls db shape iv bLow bHigh r0 pref (cur :: suff) (corr, r1, st)) (hb : ∀ (x : Vector UInt64 64 × (ℕ → List (ℤ × ℤ))), RunWords cls iv H bLow bHigh x → r' = Delivery.deliver process r1 (List.flatMap (denPoints c d H fl (List.take corr.decisions[(findDecision corr.decisions cur).run]!.sp3 entries) x) (List.filter (fun (b : ℕ) => (shape.keep cls b).run) (blockDens shape db (shape.blockPlan bLow bHigh).run bLow bHigh cur)))) (hq : r'.quit = true) : SieveRunLoopInvariant process c d H fl s P entries magics cls db shape iv bLow bHigh r0 (ForIn.toList [:n]) [] (corr', r', st')

The block at the cursor cur after which the callback stops the search.

theorem Ratpoints.Sieve.SieveRunLoopInvariant.append {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {c : List ℤ} {d H : ℕ} {fl : CheckFlags} {s : SieveOptions} {P : Params} {entries : List SieveEntry} {magics : Array ℕ} {cls : Vector NumClass 64} {db : UInt64} {shape : Shape} {iv : Array IntervalBounds} {bLow bHigh : ℕ} {r0 r1 r' : Delivery σ} {corr corr' : Correction} {st st' : RowStore} {pref suff : List ℕ} {cur n : ℕ} {b : BlockStat} (hl : ForIn.toList [:n] = pref ++ cur :: suff) (h : SieveRunLoopInvariant process c d H fl s P entries magics cls db shape iv bLow bHigh r0 pref (cur :: suff) (corr, r1, st)) (hs : st'.Fits entries) (hb : ∀ (x : Vector UInt64 64 × (ℕ → List (ℤ × ℤ))), RunWords cls iv H bLow bHigh x → r' = Delivery.deliver process r1 (List.flatMap (denPoints c d H fl (List.take corr.decisions[(findDecision corr.decisions cur).run]!.sp3 entries) x) (List.filter (fun (b : ℕ) => (shape.keep cls b).run) (blockDens shape db (shape.blockPlan bLow bHigh).run bLow bHigh cur)))) (hc : r'.quit = false → b = blockReport H P.sp1 entries magics cls db shape iv bLow bHigh corr.decisions cur) (hcorr : corr' = (runFold s P entries.toArray corr b).run) (hq : ¬r'.quit = true) : SieveRunLoopInvariant process c d H fl s P entries magics cls db shape iv bLow bHigh r0 (pref ++ [cur]) suff (corr', r', st')

The block at the cursor cur after which the callback has not stopped the search.

theorem Ratpoints.Sieve.SieveRunLoopInvariant.post {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {c : List ℤ} {d H : ℕ} {fl : CheckFlags} {s : SieveOptions} {P : Params} {entries : List SieveEntry} {magics : Array ℕ} {cls : Vector NumClass 64} {db : UInt64} {shape : Shape} {iv : Array IntervalBounds} {bLow bHigh : ℕ} {r0 : Delivery σ} {n : ℕ} {stt : Correction × Delivery σ × RowStore} (h : SieveRunLoopInvariant process c d H fl s P entries magics cls db shape iv bLow bHigh r0 (ForIn.toList [:n]) [] stt) (x : Vector UInt64 64 × (ℕ → List (ℤ × ℤ))) (hx : RunWords cls iv H bLow bHigh x) : stt.2.1 = Delivery.deliver process r0 (List.flatMap (blockPoints c d H fl s P entries magics cls db shape iv bLow bHigh x) (List.range n))

At the end of the loop, the points of all the blocks.

theorem Ratpoints.Sieve.sieveRun_spec {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (c : List ℤ) (d H A : ℕ) (fl : CheckFlags) (s : SieveOptions) (P : Params) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (offsets : Array ℕ) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh : ℕ) (store : RowStore) (r : Delivery σ) (hA : 1 ≤ A) (hw : IsRunEntries entries magics cls offsets) (hdb : ∀ j < 64, db.toBitVec.getLsbD j = (cls[j]!.bits != 0)) (hdec : DecisionWF entries P.sp1 { block := 0, sp2 := P.sp2, sp3 := P.sp3 }) (hforb : shape.ForbFits) (hbLow : 1 ≤ bLow) (hbHigh : bHigh < 2 ^ 63) (hH : H < 2 ^ 63) : ⦃ r.quit = false ∧ store.Fits entries ⦄ sieveRun process c d H A fl s P entries magics cls offsets db shape iv bLow bHigh store r ⦃ fun (res : Delivery σ × ℕ × ℕ) => ∀ (x : Vector UInt64 64 × (ℕ → List (ℤ × ℤ))), RunWords cls iv H bLow bHigh x → res.1 = Delivery.deliver process r (List.flatMap (blockPoints c d H fl s P entries magics cls db shape iv bLow bHigh x) (List.range (shape.blockPlan bLow bHigh).run.nblocks)) ⦄

The contract of the run over the blocks with the correction of the moduli, the block lemma: for sieve entries with what the run needs of them (Ratpoints.Sieve.IsRunEntries), the word db whose bits mark the classes cls with a pattern, a well-formed decision of the choice (Ratpoints.Sieve.DecisionWF), forbidden divisors of the word shape that have what its loop needs, pieces of at least one bit array, the denominators from bLow ≥ 1 to bHigh < 2 ^ 63 and the height below 2 ^ 63, the run, with a delivery whose flag of the stop is clear and a store of the tables of rows that fits all the entries, delivers the points of its blocks in order (Ratpoints.Sieve.blockPoints), each a function of the block and of its decision (Ratpoints.Sieve.blockDecision), which depends neither on the callback nor on the flags of the output, for every choice of the words of the classes and the ranges of the numerators of Ratpoints.Sieve.RunWords.

theorem Ratpoints.Sieve.fst_run_sieveRun {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (c : List ℤ) (d H A : ℕ) (fl : CheckFlags) (s : SieveOptions) (P : Params) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (offsets : Array ℕ) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh : ℕ) (store : RowStore) {r : Delivery σ} (hA : 1 ≤ A) (hw : IsRunEntries entries magics cls offsets) (hdb : ∀ j < 64, db.toBitVec.getLsbD j = (cls[j]!.bits != 0)) (hdec : DecisionWF entries P.sp1 { block := 0, sp2 := P.sp2, sp3 := P.sp3 }) (hforb : shape.ForbFits) (hbLow : 1 ≤ bLow) (hbHigh : bHigh < 2 ^ 63) (hH : H < 2 ^ 63) (hr : r.quit = false) (hs : store.Fits entries) {x : Vector UInt64 64 × (ℕ → List (ℤ × ℤ))} (hx : RunWords cls iv H bLow bHigh x) : (sieveRun process c d H A fl s P entries magics cls offsets db shape iv bLow bHigh store r).run.1 = Delivery.deliver process r (List.flatMap (blockPoints c d H fl s P entries magics cls db shape iv bLow bHigh x) (List.range (shape.blockPlan bLow bHigh).run.nblocks))

Ratpoints.Sieve.sieveRun_spec as a plain statement.

theorem Ratpoints.Sieve.exists_run_sieveRun_eq_deliver (c : List ℤ) (d H A : ℕ) (s : SieveOptions) (P : Params) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (offsets : Array ℕ) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh : ℕ) (store : RowStore) (hA : 1 ≤ A) (hw : IsRunEntries entries magics cls offsets) (hdb : ∀ j < 64, db.toBitVec.getLsbD j = (cls[j]!.bits != 0)) (hdec : DecisionWF entries P.sp1 { block := 0, sp2 := P.sp2, sp3 := P.sp3 }) (hforb : shape.ForbFits) (hnd : (shape.dens db bLow bHigh).run.Nodup) (hbLow : 1 ≤ bLow) (hbHigh : bHigh < 2 ^ 63) (hH : H < 2 ^ 63) (hs : store.Fits entries) : ∃ (sp3At : ℕ → ℕ), ∀ {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (fl : CheckFlags) (r : Delivery σ), r.quit = false → ∀ (nb : Vector UInt64 64) (rs : ℕ → List (ℤ × ℤ)), (∀ b < 64, cls[b]!.Packs nb[b]!) → (∀ (b : ℕ), bLow ≤ b → b ≤ bHigh → RangesFor iv b H (rs b)) → (sieveRun process c d H A fl s P entries magics cls offsets db shape iv bLow bHigh store r).run.1 = Delivery.deliver process r (List.flatMap (fun (b : ℕ) => List.flatMap (checkNumWith (BruteForce.scaledCoeffs c d ↑b) (if d % 2 = 1 then ↑b else 1) (↑b) fl) (List.filter (fun (a : ℤ) => inRanges (rs b) a && classBit nb[b % 64]! a && survives (List.take (sp3At b) entries) b a) (BruteForce.numerators H))) (List.filter (fun (b : ℕ) => (shape.keep cls b).run) (shape.dens db bLow bHigh).run))

The contract of the run over the blocks with the correction of the moduli, per denominator: for sieve entries with what the run needs of them (Ratpoints.Sieve.IsRunEntries), the word db whose bits mark the classes cls with a pattern, a store of the tables of rows that fits all the entries, a first decision of the parameters that is well-formed (Ratpoints.Sieve.DecisionWF), forbidden divisors of the word shape that have what its loop needs (Ratpoints.Sieve.Shape.ForbFits), a listing of the shape with no denominator twice, so that each lies in one block (Ratpoints.Sieve.Shape.eq_of_mem_blockDens), pieces of at least one bit array, the denominators from bLow ≥ 1 to bHigh < 2 ^ 63 and the height below 2 ^ 63, there is a number sp3At b of the entries of the first three stages for each denominator b, the end of the third stage of the decision of its block (Ratpoints.Sieve.blockDecision), which depends neither on the callback nor on the flags of the output, such that the run, with any callback, flags and delivery whose flag of the stop is clear, delivers for each denominator b of the listing of the shape that passes its tests (Ratpoints.Sieve.Shape.dens, Ratpoints.Sieve.Shape.keep), in order, the points of the check with the flags of the numerators -H, …, H in one of the ranges rs b that the bounds of the search intervals give for b (Ratpoints.Sieve.RangesFor), that pass the class word nb[b mod 64] for words nb that the classes pack, and survive the first sp3At b entries: the blocks in order (Ratpoints.Sieve.sieveRun_spec) visit the denominators of the listing in its order (Ratpoints.Sieve.Shape.flatMap_filter_blockDens).

The threads

def Ratpoints.Sieve.deliverSlots {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (slot : ℕ → Array (ℤ × ℤ × ℤ)) (n : ℕ) (r : Delivery σ) : Id (Delivery σ)

The calling thread of a run whose blocks are sifted by threads, which the model leaves out with the threads: the slots slot i of the blocks i < n, the points that each block delivered to the appending callback (Ratpoints.appendPoint), delivered to the callback process on the delivery r in the order of the blocks, the loop ending when the callback has stopped the search.

Equations

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

def Ratpoints.Sieve.DeliverSlotsInvariant {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (slot : ℕ → Array (ℤ × ℤ × ℤ)) (r0 : Delivery σ) : Std.WP.Invariant ℕ (Delivery σ) Prop

The invariant of the loop of Ratpoints.Sieve.deliverSlots, whose state is the delivery, from the delivery r0: that of the points of the slots done, and the callback has not stopped the search before the loop is done.

Equations

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

theorem Ratpoints.Sieve.DeliverSlotsInvariant.quit {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {slot : ℕ → Array (ℤ × ℤ × ℤ)} {r0 r : Delivery σ} {n cur : ℕ} {pref suff : List ℕ} (hl : ForIn.toList [:n] = pref ++ cur :: suff) (h : r = Delivery.deliver process r0 (List.flatMap (fun (i : ℕ) => (slot i).toList) pref) ∧ (cur :: suff = [] ∨ r.quit = false)) (hq : (Delivery.deliver process r (slot cur).toList).quit = true) : Delivery.deliver process r (slot cur).toList = Delivery.deliver process r0 (List.flatMap (fun (i : ℕ) => (slot i).toList) (ForIn.toList [:n])) ∧ (True ∨ (Delivery.deliver process r (slot cur).toList).quit = false)

The slot at the cursor cur after which the callback stops the search.

theorem Ratpoints.Sieve.DeliverSlotsInvariant.append {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {slot : ℕ → Array (ℤ × ℤ × ℤ)} {r0 r : Delivery σ} {cur : ℕ} {pref suff : List ℕ} (h : r = Delivery.deliver process r0 (List.flatMap (fun (i : ℕ) => (slot i).toList) pref) ∧ (cur :: suff = [] ∨ r.quit = false)) (hq : ¬(Delivery.deliver process r (slot cur).toList).quit = true) : Delivery.deliver process r (slot cur).toList = Delivery.deliver process r0 (List.flatMap (fun (i : ℕ) => (slot i).toList) (pref ++ [cur])) ∧ (suff = [] ∨ (Delivery.deliver process r (slot cur).toList).quit = false)

The slot at the cursor cur after which the callback has not stopped the search.

theorem Ratpoints.Sieve.deliverSlots_spec {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (slot : ℕ → Array (ℤ × ℤ × ℤ)) (n : ℕ) (r : Delivery σ) : ⦃ r.quit = false ⦄ deliverSlots process slot n r ⦃ fun (r' : Delivery σ) => r' = Delivery.deliver process r (List.flatMap (fun (i : ℕ) => (slot i).toList) (List.range n)) ⦄

The calling thread delivers the points of the slots in the order of the blocks.

theorem Ratpoints.Sieve.toList_info_run_runBlock_appendPoint (c : List ℤ) (d H A : ℕ) (fl : CheckFlags) (s : SieveOptions) (P : Params) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (offsets : Array ℕ) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh : ℕ) {i k : ℕ} {store : RowStore} (hA : 1 ≤ A) (hw : IsRunEntries entries magics cls offsets) (hdb : ∀ j < 64, db.toBitVec.getLsbD j = (cls[j]!.bits != 0)) (hdec : DecisionWF entries P.sp1 { block := 0, sp2 := P.sp2, sp3 := P.sp3 }) (hforb : shape.ForbFits) (hbLow : 1 ≤ bLow) (hbHigh : bHigh < 2 ^ 63) (hH : H < 2 ^ 63) (hk : i - adaptLag ≤ k) (hi : i < (shape.blockPlan bLow bHigh).run.nblocks) (hs : store.Fits entries) {x : Vector UInt64 64 × (ℕ → List (ℤ × ℤ))} (hx : RunWords cls iv H bLow bHigh x) : (runBlock appendPoint c d H A fl P.sp1 entries magics cls offsets db shape iv bLow bHigh (shape.blockPlan bLow bHigh).run (correctionAfter H s P entries magics cls db shape iv bLow bHigh k).decisions i store { info := #[], total := 0, quit := false }).run.1.info.toList = blockPoints c d H fl s P entries magics cls db shape iv bLow bHigh x i

Block i of the run, sifted with the decisions after the folds of the first k blocks, for k ≥ i - Ratpoints.adaptLag, with a store of its own that fits all the entries, delivers to the appending callback (Ratpoints.appendPoint) from an empty array the points of the block with its decision (Ratpoints.Sieve.blockPoints): the contract of one block (Ratpoints.Sieve.runBlock_spec) and the lag of the correction (Ratpoints.Sieve.getElem!_findDecision_correctionAfter); the step of Ratpoints.Sieve.run_deliverSlots_eq_fst_run_sieveRun.

theorem Ratpoints.Sieve.run_deliverSlots_eq_fst_run_sieveRun {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (c : List ℤ) (d H A : ℕ) (fl : CheckFlags) (s : SieveOptions) (P : Params) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (offsets : Array ℕ) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh : ℕ) {store : RowStore} {r : Delivery σ} {k : ℕ → ℕ} {stores : ℕ → RowStore} (hA : 1 ≤ A) (hw : IsRunEntries entries magics cls offsets) (hdb : ∀ j < 64, db.toBitVec.getLsbD j = (cls[j]!.bits != 0)) (hdec : DecisionWF entries P.sp1 { block := 0, sp2 := P.sp2, sp3 := P.sp3 }) (hforb : shape.ForbFits) (hbLow : 1 ≤ bLow) (hbHigh : bHigh < 2 ^ 63) (hH : H < 2 ^ 63) (hk : ∀ (i : ℕ), i - adaptLag ≤ k i) (hst : ∀ (i : ℕ), (stores i).Fits entries) (hr : r.quit = false) (hs : store.Fits entries) {x : Vector UInt64 64 × (ℕ → List (ℤ × ℤ))} (hx : RunWords cls iv H bLow bHigh x) : (deliverSlots process (fun (i : ℕ) => (runBlock appendPoint c d H A fl P.sp1 entries magics cls offsets db shape iv bLow bHigh (shape.blockPlan bLow bHigh).run (correctionAfter H s P entries magics cls db shape iv bLow bHigh (k i)).decisions i (stores i) { info := #[], total := 0, quit := false }).run.1.info) (shape.blockPlan bLow bHigh).run.nblocks r).run = (sieveRun process c d H A fl s P entries magics cls offsets db shape iv bLow bHigh store r).run.1

The threads preserve the output of the run: the blocks of the run, each sifted with the decisions after the folds of the first k i ≥ i - Ratpoints.adaptLag blocks and a store of its own that fits all the entries, into a slot by the appending callback, their slots delivered in the order of the blocks by the calling thread (Ratpoints.Sieve.deliverSlots), give what the run on the calling thread gives (Ratpoints.Sieve.sieveRun), for the hypotheses of Ratpoints.Sieve.sieveRun_spec and words of the classes and ranges of the numerators of Ratpoints.Sieve.RunWords. The pool of threads of the C code meets these hypotheses: a thread starts block i only once the blocks before block i - RP_ADAPT_LAG are folded (find_points.c:4292-4296), and the tables of rows that the threads share only gain complete rows, published once built (init.c:180, init.c:241, init.c:391, init.c:443), so that they fit all the entries whenever a thread reads them (find_points.c:3160, find_points.c:3533-3535).