The contract of the sieve of one denominator

The contract of the sieve of one denominator in the packing of its class (Ratpoints.Sieve.sift), over the search intervals in pieces, as an @[spec] theorem proved with vcgen, the program logic of Lean core, with loop invariants that are named definitions, on the contracts of the pieces and of the bits of one interval (Ratpoints.Proof.SiftBits). The sieve hands the points it finds to the callback of the caller on a delivery (Ratpoints.Delivery), whose flag of the stop is clear at the start, and returns as soon as a call sets it; its contract says that the delivery it returns is the reference of the delivery (Ratpoints.Delivery.deliver) of the list of the points it finds, which passes over the points after the stop, and that, when the callback does not stop the search, the counters it returns are those it is given plus a closed form that depends neither on the callback, the delivery and the flags of the output nor on the store of the tables of rows (Ratpoints.Sieve.siftCounts). The numerators come in with the bits of the numerators -H, …, H of one denominator; the points of a numerator are those that the exact check delivers with the flags of the search.

Main definitions

• Ratpoints.Sieve.packedReads: the closed forms of the rows of the sieve entries for a denominator in the packing of a class, with the tests of the bits that they read.
• Ratpoints.Sieve.SiftIntervalsInvariant, Ratpoints.Sieve.SiftIntervalsLoopInvariant: the invariant of the loop of Ratpoints.Sieve.sift over the search intervals, range after range.
• Ratpoints.Sieve.IsSiftArgs: what the contract of Ratpoints.Sieve.sift on the ranges of the numerators needs of its arguments.
• Ratpoints.Sieve.intervalCounts, Ratpoints.Sieve.siftCounts: the counts of one search interval and of the sieve of one denominator; Ratpoints.Sieve.SiftIntervalsCounts: the invariant of the counters of the loop over the search intervals.

Main statements

• Ratpoints.Sieve.eq_map_fst_packedReads_of_eq_run_buildRows, Ratpoints.Sieve.reads_of_mem_packedReads: the rows that Ratpoints.Sieve.setRows and Ratpoints.Sieve.buildRows give for the residues b dinv[k] mod p, the closed forms of the rows of the entries, at the offsets of the class read whether the rows of b admit the numerators of the bits (Ratpoints.Sieve.SieveEntry.reads_closedRow).
• Ratpoints.Sieve.flatMap_filter_bits_eq: the bits of numerators_to_bits of the height in the packing of the class of a class word w give the numerators -H, …, H that pass w; Ratpoints.Sieve.flatMap_filter_intervalBits_eq: the bits of a search interval that Ratpoints.Sieve.intervalBits gives, neither of the codes 1 and 2, give the numerators -H, …, H of its range that pass w.
• Ratpoints.Sieve.sift_spec: the pieces of a denominator 0 < b < 2 ^ 63 in the packing of a class cl of the class word w, for H < 2 ^ 63, entries of the first two stages with their tables of inverses and the row offsets of the packing of cl, a store of the tables of rows that fits them (Ratpoints.Sieve.RowStore.Fits), and entries of the third stage of the shape of Ratpoints.Sieve.SieveEntry.IsPrimeEntry with the reciprocals of their moduli, deliver, for the ranges of the numerators that the bounds of the search intervals give (Ratpoints.Sieve.RangesFor), the points of the check with the flags (Ratpoints.Sieve.checkNumWith) of the numerators -H, …, H in one of the ranges that pass w and survive the sieve entries of all three stages, and, when the callback does not stop the search, they add the counts of Ratpoints.Sieve.siftCounts to the counters; Ratpoints.Sieve.run_sift_eq_deliver_checkDen: without RATPOINTS_NO_CHECK, these are the points that the plain sieve of b with all the entries gives whose numerators lie in the ranges and pass w, mapped by Ratpoints.Sieve.swapPoint after a reversal, without those with y < 0 under RATPOINTS_NO_Y.
• Ratpoints.Sieve.RowStore.Fits.fits_run_sift: the sieve of one denominator with the first entries of a run as those of its first two stages keeps a store that fits all the entries of the run, since it only adds rows.

Implementation notes

The file uses Lean core and Std only, as Ratpoints.Proof.SiftBits, Ratpoints.Proof.Stages, Ratpoints.Proof.Packing, Ratpoints.Proof.BitRange, Ratpoints.Proof.RowStore and Ratpoints.Proof.Delivery do, whose contracts of the bits of one interval and of the rows built into the tables of rows of the run and whose lemmas on classes, the bits of an interval and the delivery it builds on. The hypotheses of the test on the words of the C code, 0 < b < 2 ^ 63 and |a| ≤ H < 2 ^ 63, come in with the numerators -H, …, H of one denominator (Ratpoints.Sieve.acceptedPoints_eq_ite). The loop of Ratpoints.Sieve.sift over the search intervals returns at the first interval above H and at a stop: its invariant holds the delivery of the points of the ranges done, range after range, which are those of the numerators in one of the ranges, the ranges being increasing and strictly apart (List.flatMap_filter_eq_filter_any); the sieve specs, made at the first interval that is neither below -H nor above H, are those of Ratpoints.Sieve.packedReads from then on, and the store of the tables of rows fits the entries in both branches. The counters have a contract of their own, on the contract of the bits of one interval (Ratpoints.Sieve.siftBits_spec, which states the delivery and the counters), which needs neither the class word nor the ranges, and Ratpoints.Sieve.sift_spec states the two; the store frame is a contract of its own (Ratpoints.Sieve.RowStore.Fits.fits_run_sift), without the class word and the ranges. The contracts of one block and of the run over the blocks, which call Ratpoints.Sieve.sift with the class of each denominator, are in Ratpoints.Proof.Blocks and Ratpoints.Proof.Correction.

One denominator

def Ratpoints.Sieve.packedReads (es : List SieveEntry) (b : Nat) (cl : NumClass) (offsets : Array Nat) (pos : Nat) : List (SieveSpec × (Int → Bool))

The rows of the sieve entries es for the denominator b in the packing of the class cl, with the row offsets from position pos of offsets on, as Ratpoints.Sieve.setRows and Ratpoints.Sieve.buildRows make them: the closed forms of the rows of the residues b dinv[k] mod p (Ratpoints.Sieve.closedRow), with the start 0 and the end p, each with the test of the bits that it reads (Ratpoints.Sieve.SieveSpec.Reads): whether the row of b admits the numerator of the bit (Ratpoints.Sieve.SieveEntry.reads_closedRow).

Equations

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

theorem Ratpoints.Sieve.mapIdx_eq_map_fst_packedReads (es : List SieveEntry) (b : Nat) {cl : NumClass} {pos : Nat} (hpos : cl.offset = some pos) (offsets : Array Nat) : List.mapIdx (fun (n : Nat) (e : SieveEntry) => { p := e.p, offset := offsets[cl.offset.getD 0 + n]!, row := closedRow e.admits e.p (b * e.dinv[cl.k]! % e.p), start := 0, stop := e.p }) es = List.map Prod.fst (packedReads es b cl offsets pos)

The sieve specs that Ratpoints.Sieve.buildRows completes for the residues b dinv[k] mod p of the entries (Ratpoints.Sieve.buildRows_setRows_map_spec), the residues that Ratpoints.Sieve.fillBpList gives (Ratpoints.Sieve.fillBpList_eq_map), at the offsets of the class from its position pos on, are those of Ratpoints.Sieve.packedReads.

theorem Ratpoints.Sieve.reads_of_mem_packedReads {es : List SieveEntry} {b : Nat} {cl : NumClass} {offsets : Array Nat} {pos : Nat} (hinv : ∀ (e : SieveEntry), e ∈ es → e.HasInverses) (hoff : ∀ (n : Nat) (h : n < es.length), es[n].PackedFor cl offsets[pos + n]!) (sf : SieveSpec × (Int → Bool)) : sf ∈ packedReads es b cl offsets pos → sf.fst.Reads sf.snd

The rows of Ratpoints.Sieve.packedReads read their tests, for entries whose factors have their tables of inverses and whose offsets are those of the packing of the class.

theorem Ratpoints.Sieve.flatMap_acceptedPoints_eq_flatMap_checkNumWith {c : List Int} {d b : Nat} {fl : CheckFlags} {p : Int → Bool} {entries es3 : List SieveEntry} (hes : ∀ (e : SieveEntry), e ∈ es3 → e.IsPrimeEntry) {H : Nat} (hb : 0 < b) (hb63 : b < 2 ^ 63) (hH : H < 2 ^ 63) : List.flatMap (acceptedPoints { fn := fun (x : Unit) => BruteForce.scaledCoeffs c d ↑b } d b fl { fn := fun (x : Unit) => fillChecks b H es3 (List.map (fun (x : SieveEntry) => magic x.p) es3) }) (List.filter (fun (a : Int) => p a && survives entries b a) (BruteForce.numerators H)) = List.flatMap (checkNumWith (BruteForce.scaledCoeffs c d ↑b) (if d % 2 = 1 then ↑b else 1) (↑b) fl) (List.filter (fun (a : Int) => p a && survives (entries ++ es3) b a) (BruteForce.numerators H))

For the points of Ratpoints.Sieve.acceptedPoints with the thunks of the products and of what the third stage needs of the entries es3 of the shape of Ratpoints.Sieve.SieveEntry.IsPrimeEntry, with the reciprocals of their moduli, for a denominator 0 < b < 2 ^ 63, H < 2 ^ 63 and the flags fl, the numerators -H, …, H that pass a test p and survive the entries of the first two stages give the points of the check with the flags (Ratpoints.Sieve.checkNumWith) of the numerators that pass p and survive the entries of all three stages (Ratpoints.Sieve.acceptedPoints_eq_ite).

theorem Ratpoints.Sieve.flatMap_filter_bits_eq {cl : NumClass} {w : UInt64} (hcl : cl.Packs w) {H : Nat} {lo hi : Int} (hlo : lo = -((↑cl.a0 + ↑H) / 2 ^ cl.k)) (hhi : hi = (↑H - ↑cl.a0) / 2 ^ cl.k) {test t : Int → Bool} (htest : ∀ (j : Int), test j = t (cl.numerator j)) (g : Int → List (Int × Int × Int)) : List.flatMap (fun (j : Int) => g (cl.numerator j)) (List.filter (fun (j : Int) => classBit cl.bits j && test j) (List.map (fun (k : Nat) => lo + ↑k) (List.range (hi + 1 - lo).toNat))) = List.flatMap g (List.filter (fun (a : Int) => classBit w a && t a) (BruteForce.numerators H))

The bits from ⌈(-H - a₀) / 2 ^ k⌉ to ⌊(H - a₀) / 2 ^ k⌋ of the packing of a class cl of the class word w (Ratpoints.Sieve.NumClass.Packs) that pass a test of the numerators of the bits give the points of the numerators -H, …, H that pass w and the test: the numerators of the bits are those of the class among -H, …, H (Ratpoints.Sieve.NumClass.WF.map_range_numerator_eq_filter_numerators), the pattern of the class lets the numerator of a bit through exactly when w does (Ratpoints.Sieve.NumClass.Packs.classBit_bits), and w lets nothing off the class through.

theorem Ratpoints.Sieve.eq_map_fst_packedReads_of_eq_run_buildRows {store store' : RowStore} {es : List SieveEntry} (hs : store.Fits es) {b : Nat} {cl : NumClass} {pos : Nat} (hpos : cl.offset = some pos) {offsets : Array Nat} {specs : List SieveSpec} (hr : (specs, store') = (buildRows (setRows store es (List.map (fun (e : SieveEntry) => b * e.dinv[cl.k]! % e.p) es) cl offsets).snd es (List.map (fun (e : SieveEntry) => b * e.dinv[cl.k]! % e.p) es) (setRows store es (List.map (fun (e : SieveEntry) => b * e.dinv[cl.k]! % e.p) es) cl offsets).fst store).run) : specs = List.map Prod.fst (packedReads es b cl offsets pos)

The sieve specs of the denominator b that Ratpoints.Sieve.setRows makes and Ratpoints.Sieve.buildRows completes, for the residues b dinv[k] mod p of the entries, the class cl with its row offsets from position pos on and a store that fits the entries (Ratpoints.Sieve.RowStore.Fits), are those of Ratpoints.Sieve.packedReads.

theorem Ratpoints.Sieve.flatMap_filter_intervalBits_eq {c : List Int} {d b H : Nat} {fl : CheckFlags} {es es3 : List SieveEntry} (hes : ∀ (e : SieveEntry), e ∈ es3 → e.IsPrimeEntry) {w : UInt64} {cl : NumClass} (hcl : cl.Packs w) {offsets : Array Nat} {pos : Nat} {bd : IntervalBounds} {lo hi : Int} (hrep : bd.Represents b H lo hi) (h1 : (intervalBits b.toInt64 bd H.toInt64 cl).fst ≠ 1) (h2 : (intervalBits b.toInt64 bd H.toInt64 cl).fst ≠ 2) (hb : 0 < b) (hb63 : b < 2 ^ 63) (hH : H < 2 ^ 63) : List.flatMap (fun (j : Int) => acceptedPoints { fn := fun (x : Unit) => BruteForce.scaledCoeffs c d ↑b } d b fl { fn := fun (x : Unit) => fillChecks b H es3 (List.map (fun (x : SieveEntry) => magic x.p) es3) } (cl.numerator j)) (List.filter (fun (j : Int) => classBit cl.bits j && (packedReads es b cl offsets pos).all fun (x : SieveSpec × (Int → Bool)) => x.snd j) (List.map (fun (k : Nat) => (intervalBits b.toInt64 bd H.toInt64 cl).snd.fst.toInt + ↑k) (List.range ((intervalBits b.toInt64 bd H.toInt64 cl).snd.snd.toInt + 1 - (intervalBits b.toInt64 bd H.toInt64 cl).snd.fst.toInt).toNat))) = List.flatMap (checkNumWith (BruteForce.scaledCoeffs c d ↑b) (if d % 2 = 1 then ↑b else 1) (↑b) fl) (List.filter (fun (a : Int) => decide (lo ≤ a ∧ a ≤ hi) && (classBit w a && survives (es ++ es3) b a)) (BruteForce.numerators H))

The bits of a search interval with the bounds bd, which give the range lo, …, hi of the numerators (Ratpoints.Sieve.IntervalBounds.Represents), when Ratpoints.Sieve.intervalBits gives neither the code 1 nor the code 2, in the packing of a class cl of the class word w, with the tests that the rows of Ratpoints.Sieve.packedReads read and the points of the check of Ratpoints.Sieve.acceptedPoints, give the points of the check with the flags (Ratpoints.Sieve.checkNumWith) of the numerators -H, …, H in lo, …, hi that pass w and survive the entries of all three stages.

structure Ratpoints.Sieve.SiftIntervalsInvariant {σ : Type} (process : Int → Int → Int → σ → Answer σ) (l : List Int) (q : Int → Bool) (g : Int → List (Int × Int × Int)) (es : List SieveEntry) (specs0 : List SieveSpec) (rs : List (Int × Int)) (r0 : Delivery σ) (k : Nat) (r : Delivery σ) (store : RowStore) (doSetup : Bool) (specs : List SieveSpec) : Prop

The invariant of the loop of Ratpoints.Sieve.sift over the bounds of the search intervals, from the delivery r0, after the first k intervals, for the ranges rs of the numerators that they give, the increasing list l of the numerators, their test q and their points g: the callback has not stopped the search, the store of the tables of rows fits the sieve entries es, the sieve specs are specs0 once they are made (doSetup false), and the delivery is that of the points of the numerators of l that pass q, range after range, for the first k ranges.

• quit_eq_false : r.quit = false

  The callback has not stopped the search.

• fits : store.Fits es

  The store fits the sieve entries of the first two stages.

• specs_eq : doSetup = false → specs = specs0

  The sieve specs, once made.

• eq_deliver : r = Delivery.deliver process r0 (List.flatMap (fun (rg : Int × Int) => List.flatMap g (List.filter (fun (a : Int) => decide (rg.fst ≤ a ∧ a ≤ rg.snd) && q a) l)) (List.take k rs))

  The delivery is that of the points of the first k ranges.

def Ratpoints.Sieve.SiftIntervalsLoopInvariant {σ : Type} (process : Int → Int → Int → σ → Answer σ) (c : List Int) (d H b : Nat) (fl : CheckFlags) (es es3 : List SieveEntry) (w : UInt64) (cl : NumClass) (offsets : Array Nat) (pos : Nat) (rs : List (Int × Int)) (r0 : Delivery σ) : Std.WP.Invariant IntervalBounds (Option (Delivery σ × RowStore × Counters) × Delivery σ × RowStore × Counters × Bool × List SieveSpec) Prop

The invariant of the loop of Ratpoints.Sieve.sift over the bounds of the search intervals of the denominator b, with the class word w, the sieve entries es and es3, the specs of Ratpoints.Sieve.packedReads with the row offsets from position pos of offsets on, and the ranges rs of the numerators, whose state is the value of a return, the delivery, the store of the tables of rows, the flag of the set-up and the sieve specs: before a return, Ratpoints.Sieve.SiftIntervalsInvariant after the intervals done, for the numerators -H, …, H, their test by w and the entries, and the points of the check with the flags fl; after the return at a stop or at an interval above the height bound, the delivery returned is that of the points of all the ranges.

Equations

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

theorem Ratpoints.Sieve.siftIntervalsInvariant_zero {σ : Type} {process : Int → Int → Int → σ → Answer σ} {l : List Int} {q : Int → Bool} {g : Int → List (Int × Int × Int)} {es : List SieveEntry} {specs0 : List SieveSpec} {rs : List (Int × Int)} {r0 : Delivery σ} {store : RowStore} (hr : r0.quit = false) (hs : store.Fits es) (specs : List SieveSpec) : SiftIntervalsInvariant process l q g es specs0 rs r0 0 r0 store true specs

theorem Ratpoints.Sieve.SiftIntervalsInvariant.post_of_length_le {σ : Type} {process : Int → Int → Int → σ → Answer σ} {l : List Int} {q : Int → Bool} {g : Int → List (Int × Int × Int)} {es : List SieveEntry} {specs0 : List SieveSpec} {rs : List (Int × Int)} {r0 r : Delivery σ} {store : RowStore} {doSetup : Bool} {specs : List SieveSpec} {k : Nat} (h : SiftIntervalsInvariant process l q g es specs0 rs r0 k r store doSetup specs) (hk : rs.length ≤ k) : r = Delivery.deliver process r0 (List.flatMap (fun (rg : Int × Int) => List.flatMap g (List.filter (fun (a : Int) => decide (rg.fst ≤ a ∧ a ≤ rg.snd) && q a) l)) rs)

After the last range, the delivery is that of the points of all the ranges.

theorem Ratpoints.Sieve.SiftIntervalsInvariant.post_of_forall_mem_drop {σ : Type} {process : Int → Int → Int → σ → Answer σ} {l : List Int} {q : Int → Bool} {g : Int → List (Int × Int × Int)} {es : List SieveEntry} {specs0 : List SieveSpec} {rs : List (Int × Int)} {r0 r : Delivery σ} {store : RowStore} {doSetup : Bool} {specs : List SieveSpec} {k : Nat} (h : SiftIntervalsInvariant process l q g es specs0 rs r0 k r store doSetup specs) (hnil : ∀ (rg : Int × Int), rg ∈ List.drop k rs → List.filter (fun (a : Int) => decide (rg.fst ≤ a ∧ a ≤ rg.snd) && q a) l = []) : r = Delivery.deliver process r0 (List.flatMap (fun (rg : Int × Int) => List.flatMap g (List.filter (fun (a : Int) => decide (rg.fst ≤ a ∧ a ≤ rg.snd) && q a) l)) rs)

When the ranges from the k-th on hold no element of l that passes q, the delivery after the first k ranges is that of the points of all of them.

theorem Ratpoints.Sieve.SiftIntervalsInvariant.append_of_forall_mem {σ : Type} {process : Int → Int → Int → σ → Answer σ} {l : List Int} {q : Int → Bool} {g : Int → List (Int × Int × Int)} {es : List SieveEntry} {specs0 : List SieveSpec} {rs : List (Int × Int)} {r0 r : Delivery σ} {store : RowStore} {doSetup : Bool} {specs : List SieveSpec} {pref : List IntervalBounds} {cur : IntervalBounds} {o : Option (Delivery σ × RowStore × Counters)} (h : o = none ∧ SiftIntervalsInvariant process l q g es specs0 rs r0 pref.length r store doSetup specs) (hnil : ∀ (rg : Int × Int), rg ∈ rs[pref.length]? → List.filter (fun (a : Int) => decide (rg.fst ≤ a ∧ a ≤ rg.snd) && q a) l = []) : SiftIntervalsInvariant process l q g es specs0 rs r0 (pref ++ [cur]).length r store doSetup specs

A range that holds no element of l that passes q, or none at all, delivers nothing.

theorem Ratpoints.Sieve.SiftIntervalsInvariant.append_of_eq_deliver {σ : Type} {process : Int → Int → Int → σ → Answer σ} {l : List Int} {q : Int → Bool} {g : Int → List (Int × Int × Int)} {es : List SieveEntry} {specs0 : List SieveSpec} {rs : List (Int × Int)} {r0 r r' : Delivery σ} {store st : RowStore} {doSetup : Bool} {specs specs' : List SieveSpec} {pref : List IntervalBounds} {cur : IntervalBounds} {o : Option (Delivery σ × RowStore × Counters)} (h : o = none ∧ SiftIntervalsInvariant process l q g es specs0 rs r0 pref.length r store doSetup specs) (hr : r' = Delivery.deliver process r (List.flatMap (fun (rg : Int × Int) => List.flatMap g (List.filter (fun (a : Int) => decide (rg.fst ≤ a ∧ a ≤ rg.snd) && q a) l)) rs[pref.length]?.toList)) (hq : ¬r'.quit = true) (hs : st.Fits es) (hsp : specs' = specs0) (ds : Bool) : SiftIntervalsInvariant process l q g es specs0 rs r0 (pref ++ [cur]).length r' st ds specs'

A range whose points the delivery r' adds, after which the callback has not stopped the search, with the store st that fits the entries and the sieve specs made, keeps the invariant.

theorem Ratpoints.Sieve.SiftIntervalsInvariant.post_of_quit {σ : Type} {process : Int → Int → Int → σ → Answer σ} {l : List Int} {q : Int → Bool} {g : Int → List (Int × Int × Int)} {es : List SieveEntry} {specs0 : List SieveSpec} {rs : List (Int × Int)} {r0 r r' : Delivery σ} {store : RowStore} {doSetup : Bool} {specs : List SieveSpec} {pref : List IntervalBounds} {o : Option (Delivery σ × RowStore × Counters)} (h : o = none ∧ SiftIntervalsInvariant process l q g es specs0 rs r0 pref.length r store doSetup specs) (hr : r' = Delivery.deliver process r (List.flatMap (fun (rg : Int × Int) => List.flatMap g (List.filter (fun (a : Int) => decide (rg.fst ≤ a ∧ a ≤ rg.snd) && q a) l)) rs[pref.length]?.toList)) (hq : r'.quit = true) : r' = Delivery.deliver process r0 (List.flatMap (fun (rg : Int × Int) => List.flatMap g (List.filter (fun (a : Int) => decide (rg.fst ≤ a ∧ a ≤ rg.snd) && q a) l)) rs)

A range whose points the delivery r' adds, after which the callback has stopped the search: the delivery is that of the points of all the ranges (Ratpoints.Delivery.deliver_flatMap_eq_of_prefix).

theorem Ratpoints.Sieve.SiftIntervalsInvariant.specs_eq_and_fits_of_not {σ : Type} {process : Int → Int → Int → σ → Answer σ} {l : List Int} {q : Int → Bool} {g : Int → List (Int × Int × Int)} {es : List SieveEntry} {specs0 : List SieveSpec} {rs : List (Int × Int)} {r0 r : Delivery σ} {store : RowStore} {doSetup : Bool} {specs : List SieveSpec} {o : Option (Delivery σ × RowStore × Counters)} {k : Nat} (h : o = none ∧ SiftIntervalsInvariant process l q g es specs0 rs r0 k r store doSetup specs) (hd : ¬doSetup = true) : specs = specs0 ∧ store.Fits es

Once the sieve specs are made, they are specs0, and the store fits the entries.

theorem Ratpoints.Sieve.filter_numerators_eq_nil_of_lt_neg {H : Nat} {lo hi : Int} (h : hi < -↑H) (q : Int → Bool) : List.filter (fun (a : Int) => decide (lo ≤ a ∧ a ≤ hi) && q a) (BruteForce.numerators H) = []

theorem Ratpoints.Sieve.filter_numerators_eq_nil_of_natCast_lt {H : Nat} {lo hi : Int} (h : ↑H < lo) (q : Int → Bool) : List.filter (fun (a : Int) => decide (lo ≤ a ∧ a ≤ hi) && q a) (BruteForce.numerators H) = []

structure Ratpoints.Sieve.IsSiftArgs (es es3 : List SieveEntry) (w : UInt64) (cl : NumClass) (offsets : Array Nat) (pos : Nat) (iv : Array IntervalBounds) (b H : Nat) (rs : List (Int × Int)) : Prop

What the contract of Ratpoints.Sieve.sift on the ranges rs of the numerators that the bounds iv of the search intervals give (Ratpoints.Sieve.RangesFor) needs of its arguments: a denominator 0 < b < 2 ^ 63 and H < 2 ^ 63, the sieve entries es3 of the third stage of the shape that it needs, the class cl that packs the class word w with its row offsets from position pos of offsets on, and the sieve entries es of the first two stages with their tables of inverses and the offsets of the packing of cl.

• b_pos : 0 < b

  The denominator is positive.

• b_lt : b < 2 ^ 63

  The denominator is below 2 ^ 63.

• H_lt : H < 2 ^ 63

  The height bound is below 2 ^ 63.

• isPrimeEntry (e : SieveEntry) : e ∈ es3 → e.IsPrimeEntry

  The entries of the third stage have the shape that it needs.

• packs : cl.Packs w

  The class packs the class word.

• offset_eq : cl.offset = some pos

  The row offsets of the class start at pos.

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

  The entries of the first two stages have their tables of inverses.

• packedFor (n : Nat) (h : n < es.length) : es[n].PackedFor cl offsets[pos + n]!

  The entries of the first two stages have the offsets of the packing of the class.

• rangesFor : RangesFor iv b H rs

  The bounds of the search intervals give the ranges.

theorem Ratpoints.Sieve.IsSiftArgs.post_of_length {σ : Type} {process : Int → Int → Int → σ → Answer σ} {b H : Nat} {es es3 : List SieveEntry} {w : UInt64} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {iv : Array IntervalBounds} {rs : List (Int × Int)} {q : Int → Bool} {g : Int → List (Int × Int × Int)} {specs0 : List SieveSpec} {r0 r : Delivery σ} {store : RowStore} {doSetup : Bool} {specs : List SieveSpec} (ha : IsSiftArgs es es3 w cl offsets pos iv b H rs) (h : SiftIntervalsInvariant process (BruteForce.numerators H) q g es specs0 rs r0 (ForIn.toList iv).length r store doSetup specs) : r = Delivery.deliver process r0 (List.flatMap (fun (rg : Int × Int) => List.flatMap g (List.filter (fun (a : Int) => decide (rg.fst ≤ a ∧ a ≤ rg.snd) && q a) (BruteForce.numerators H))) rs)

After the last interval, the delivery is that of the points of all the ranges.

theorem Ratpoints.Sieve.IsSiftArgs.post_of_two {σ : Type} {process : Int → Int → Int → σ → Answer σ} {b H : Nat} {es es3 : List SieveEntry} {w : UInt64} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {iv : Array IntervalBounds} {rs : List (Int × Int)} {q : Int → Bool} {g : Int → List (Int × Int × Int)} {specs0 : List SieveSpec} {r0 r : Delivery σ} {store : RowStore} {doSetup : Bool} {specs : List SieveSpec} {pref suff : List IntervalBounds} {cur : IntervalBounds} {o : Option (Delivery σ × RowStore × Counters)} (ha : IsSiftArgs es es3 w cl offsets pos iv b H rs) (hl : ForIn.toList iv = pref ++ cur :: suff) (h : o = none ∧ SiftIntervalsInvariant process (BruteForce.numerators H) q g es specs0 rs r0 pref.length r store doSetup specs) (h2 : (intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).fst = 2) : r = Delivery.deliver process r0 (List.flatMap (fun (rg : Int × Int) => List.flatMap g (List.filter (fun (a : Int) => decide (rg.fst ≤ a ∧ a ≤ rg.snd) && q a) (BruteForce.numerators H))) rs)

At an interval with the code 2, above the height bound, the delivery is that of the points of all the ranges: the ranges from that interval on lie above H.

theorem Ratpoints.Sieve.IsSiftArgs.append_of_one {σ : Type} {process : Int → Int → Int → σ → Answer σ} {b H : Nat} {es es3 : List SieveEntry} {w : UInt64} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {iv : Array IntervalBounds} {rs : List (Int × Int)} {q : Int → Bool} {g : Int → List (Int × Int × Int)} {specs0 : List SieveSpec} {r0 r : Delivery σ} {store : RowStore} {doSetup : Bool} {specs : List SieveSpec} {pref suff : List IntervalBounds} {cur : IntervalBounds} {o : Option (Delivery σ × RowStore × Counters)} (ha : IsSiftArgs es es3 w cl offsets pos iv b H rs) (hl : ForIn.toList iv = pref ++ cur :: suff) (h : o = none ∧ SiftIntervalsInvariant process (BruteForce.numerators H) q g es specs0 rs r0 pref.length r store doSetup specs) (h1 : (intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).fst = 1) : SiftIntervalsInvariant process (BruteForce.numerators H) q g es specs0 rs r0 (pref ++ [cur]).length r store doSetup specs

An interval with the code 1, below -H, keeps the invariant.

theorem Ratpoints.Sieve.IsSiftArgs.specs_eq_and_fits_of_eq_run_buildRows {σ : Type} {process : Int → Int → Int → σ → Answer σ} {b H : Nat} {es es3 : List SieveEntry} {w : UInt64} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {iv : Array IntervalBounds} {rs : List (Int × Int)} {q : Int → Bool} {g : Int → List (Int × Int × Int)} {specs0 : List SieveSpec} {r0 r : Delivery σ} {store st : RowStore} {doSetup : Bool} {specs specs' : List SieveSpec} {o : Option (Delivery σ × RowStore × Counters)} (ha : IsSiftArgs es es3 w cl offsets pos iv b H rs) {k : Nat} (h : o = none ∧ SiftIntervalsInvariant process (BruteForce.numerators H) q g es specs0 rs r0 k r store doSetup specs) (hr : (specs', st) = (buildRows (setRows store es (List.map (fun (e : SieveEntry) => b * e.dinv[cl.k]! % e.p) es) cl offsets).snd es (List.map (fun (e : SieveEntry) => b * e.dinv[cl.k]! % e.p) es) (setRows store es (List.map (fun (e : SieveEntry) => b * e.dinv[cl.k]! % e.p) es) cl offsets).fst store).run) : specs' = List.map Prod.fst (packedReads es b cl offsets pos) ∧ st.Fits es

The sieve specs that Ratpoints.Sieve.setRows and Ratpoints.Sieve.buildRows make at the first interval that asks for them are those of Ratpoints.Sieve.packedReads, and the store after them fits the entries (Ratpoints.Sieve.eq_map_fst_packedReads_of_eq_run_buildRows).

theorem Ratpoints.Sieve.IsSiftArgs.eq_deliver_getElem? {σ : Type} {process : Int → Int → Int → σ → Answer σ} {c : List Int} {d b H : Nat} {fl : CheckFlags} {es es3 : List SieveEntry} {w : UInt64} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {iv : Array IntervalBounds} {rs : List (Int × Int)} {r r' : Delivery σ} {specs : List SieveSpec} {pref suff : List IntervalBounds} {cur : IntervalBounds} (ha : IsSiftArgs es es3 w cl offsets pos iv b H rs) (hl : ForIn.toList iv = pref ++ cur :: suff) (h2 : ¬(intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).fst = 2) (h1 : ¬(intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).fst = 1) (hsp : specs = List.map Prod.fst (packedReads es b cl offsets pos)) {P : List (SieveSpec × (Int → Bool)) → Prop} (hsb : ∀ (sfs : List (SieveSpec × (Int → Bool))), specs = List.map Prod.fst sfs → (∀ (sf : SieveSpec × (Int → Bool)), sf ∈ sfs → sf.fst.Reads sf.snd) → r' = Delivery.deliver process r (List.flatMap (fun (j : Int) => acceptedPoints { fn := fun (x : Unit) => BruteForce.scaledCoeffs c d ↑b } d b fl { fn := fun (x : Unit) => fillChecks b H es3 (List.map (fun (x : SieveEntry) => magic x.p) es3) } (cl.numerator j)) (List.filter (fun (j : Int) => classBit cl.bits j && sfs.all fun (x : SieveSpec × (Int → Bool)) => x.snd j) (List.map (fun (k : Nat) => (intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).snd.fst.toInt + ↑k) (List.range ((intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).snd.snd.toInt + 1 - (intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).snd.fst.toInt).toNat)))) ∧ P sfs) : r' = Delivery.deliver process r (List.flatMap (fun (rg : Int × Int) => List.flatMap (checkNumWith (BruteForce.scaledCoeffs c d ↑b) (if d % 2 = 1 then ↑b else 1) (↑b) fl) (List.filter (fun (a : Int) => decide (rg.fst ≤ a ∧ a ≤ rg.snd) && (classBit w a && survives (es ++ es3) b a)) (BruteForce.numerators H))) rs[pref.length]?.toList)

The delivery after Ratpoints.Sieve.siftBits on the bits that Ratpoints.Sieve.intervalBits gives for the interval at the position pref.length, neither of the codes 1 and 2, with the sieve specs of Ratpoints.Sieve.packedReads, adds the points of the range of the numerators of that interval (Ratpoints.Sieve.flatMap_filter_intervalBits_eq).

theorem Ratpoints.Sieve.RowStore.Fits.fits_run_sift {σ : Type} (process : Int → Int → Int → σ → Answer σ) (c : List Int) (d H A : Nat) {b : Nat} (fl : CheckFlags) (sp1 : Nat) {L : List SieveEntry} {k : Nat} (mgs : List Nat) {bp : List Nat} {cl : NumClass} (offsets : Array Nat) (es3 : List SieveEntry) (mgs3 : List Nat) (iv : Array IntervalBounds) {store : RowStore} (r : Delivery σ) (cnt : Counters) (hs : store.Fits L) (hbp : bp = List.map (fun (e : SieveEntry) => b * e.dinv[cl.k]! % e.p) (List.take k L)) : (sift process c d H A b fl sp1 (List.take k L) mgs bp cl offsets es3 mgs3 iv store r cnt).run.snd.fst.Fits L

The sieve of one denominator with the first k entries of the run L as those of its first two stages only adds rows to the store of the tables of rows, rows of the references of these entries: a store that fits L still fits L after it.

The counters of one denominator

def Ratpoints.Sieve.intervalCounts (b H sp1 : Nat) (es es3 : List SieveEntry) (mgs3 : List Nat) (cl : NumClass) (bd : IntervalBounds) : Counters

The counts that the search interval with the bounds bd adds to the counters in the sieve of the denominator b (Ratpoints.Sieve.sift), for the height H, the class cl of b, the sieve entries es of the first two stages, the first stage ending after sp1 of them, and the entries es3 of the third stage with the reciprocals mgs3 of their moduli: none for an interval with the code 1 of Ratpoints.Sieve.intervalBits, and otherwise those of its bits (Ratpoints.Sieve.bitsCounts), with the tests of the rows the survivor tests of the entries.

Equations

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

def Ratpoints.Sieve.siftCounts (b H sp1 : Nat) (es es3 : List SieveEntry) (mgs3 : List Nat) (cl : NumClass) (iv : Array IntervalBounds) : Counters

The counts that the sieve of the denominator b adds to the counters (Ratpoints.Sieve.sift), for the height H, the class cl of b, the sieve entries es of the first two stages, the first stage ending after sp1 of them, the entries es3 of the third stage with the reciprocals mgs3 of their moduli and the bounds iv of the search intervals: one denominator, in sifts, and the counts of the search intervals (Ratpoints.Sieve.intervalCounts) before the first with the code 2 of Ratpoints.Sieve.intervalBits, at which the sieve returns.

Equations

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

structure Ratpoints.Sieve.SiftIntervalsCounts {σ : Type} (b H sp1 : Nat) (es es3 : List SieveEntry) (mgs3 : List Nat) (cl : NumClass) (offsets : Array Nat) (pos : Nat) (cnt0 : Counters) (pref : List IntervalBounds) (r : Delivery σ) (store : RowStore) (doSetup : Bool) (specs : List SieveSpec) (c : Counters) : Prop

The invariant of the counters of the loop of Ratpoints.Sieve.sift over the bounds of the search intervals of the denominator b, after the intervals pref, for the sieve entries es with the row offsets of the class cl from position pos of offsets on: the callback has not stopped the search on the delivery r, the store of the tables of rows fits es, the sieve specs are those of Ratpoints.Sieve.packedReads once they are made (doSetup false), none of the intervals of pref has the code 2, and the counters are cnt0 plus one denominator and the counts of the intervals of pref (Ratpoints.Sieve.intervalCounts).

• quit_eq_false : r.quit = false

  The callback has not stopped the search.

• fits : store.Fits es

  The store fits the sieve entries of the first two stages.

• specs_eq : doSetup = false → specs = List.map Prod.fst (packedReads es b cl offsets pos)

  The sieve specs, once made.

• ne_two (bd : IntervalBounds) : bd ∈ pref → (intervalBits (Int64.ofNat b) bd (Int64.ofNat H) cl).fst ≠ 2

  No interval done has the code 2.

• eq_counts : c = cnt0 + List.foldl (fun (x1 x2 : Counters) => x1 + x2) { sifts := 1 } (List.map (intervalCounts b H sp1 es es3 mgs3 cl) pref)

  The counters of the intervals done.

def Ratpoints.Sieve.SiftIntervalsCountsLoopInvariant {σ : Type} (b H sp1 : Nat) (es es3 : List SieveEntry) (mgs3 : List Nat) (cl : NumClass) (offsets : Array Nat) (pos : Nat) (iv : Array IntervalBounds) (cnt0 : Counters) : Std.WP.Invariant IntervalBounds (Option (Delivery σ × RowStore × Counters) × Delivery σ × RowStore × Counters × Bool × List SieveSpec) Prop

Ratpoints.Sieve.SiftIntervalsCounts as the invariant of the counters of the loop of Ratpoints.Sieve.sift over the bounds of the search intervals, whose state is the value of a return, the delivery, the store of the tables of rows, the counters, the flag of the set-up and the sieve specs; after a return without a stop, at an interval with the code 2, the counters returned are those of Ratpoints.Sieve.siftCounts.

Equations

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

theorem Ratpoints.Sieve.take_packedReads (es : List SieveEntry) (b : Nat) (cl : NumClass) (offsets : Array Nat) (pos k : Nat) : List.take k (packedReads es b cl offsets pos) = packedReads (List.take k es) b cl offsets pos

The rows of Ratpoints.Sieve.packedReads of the first k sieve entries are its first k.

theorem Ratpoints.Sieve.bitsCounts_packedReads_eq_intervalCounts {H sp1 : Nat} {es es3 : List SieveEntry} {mgs3 : List Nat} {b : Nat} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {bd : IntervalBounds} (h1 : ¬(intervalBits (Int64.ofNat b) bd (Int64.ofNat H) cl).fst = 1) : bitsCounts b { fn := fun (x : Unit) => fillChecks b H es3 mgs3 } cl (fun (j : Int) => (List.take sp1 (packedReads es b cl offsets pos)).all fun (x : SieveSpec × (Int → Bool)) => x.snd j) (fun (j : Int) => (packedReads es b cl offsets pos).all fun (x : SieveSpec × (Int → Bool)) => x.snd j) (intervalBits (Int64.ofNat b) bd (Int64.ofNat H) cl).snd.fst.toInt (intervalBits (Int64.ofNat b) bd (Int64.ofNat H) cl).snd.snd.toInt = intervalCounts b H sp1 es es3 mgs3 cl bd

The counts of the bits of a search interval with the tests that the rows of Ratpoints.Sieve.packedReads read are those of Ratpoints.Sieve.intervalCounts, for an interval without the code 1.

theorem Ratpoints.Sieve.siftIntervalsCounts_zero {σ : Type} {b H sp1 : Nat} {es es3 : List SieveEntry} {mgs3 : List Nat} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {cnt0 : Counters} {r : Delivery σ} {store : RowStore} (hr : r.quit = false) (hs : store.Fits es) (specs : List SieveSpec) : SiftIntervalsCounts b H sp1 es es3 mgs3 cl offsets pos cnt0 [] r store true specs { words := cnt0.words, arrays := cnt0.arrays, bits := cnt0.bits, coprime := cnt0.coprime, checks := cnt0.checks, sifts := cnt0.sifts + 1 }

theorem Ratpoints.Sieve.SiftIntervalsCounts.eq_siftCounts {σ : Type} {b H sp1 : Nat} {es es3 : List SieveEntry} {mgs3 : List Nat} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {iv : Array IntervalBounds} {cnt0 c : Counters} {r : Delivery σ} {store : RowStore} {doSetup : Bool} {specs : List SieveSpec} (h : SiftIntervalsCounts b H sp1 es es3 mgs3 cl offsets pos cnt0 (ForIn.toList iv) r store doSetup specs c) : c = cnt0 + siftCounts b H sp1 es es3 mgs3 cl iv

After all the search intervals, none with the code 2, the counters are those of Ratpoints.Sieve.siftCounts.

theorem Ratpoints.Sieve.SiftIntervalsCounts.post_of_two {σ : Type} {b H sp1 : Nat} {es es3 : List SieveEntry} {mgs3 : List Nat} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {iv : Array IntervalBounds} {cnt0 c : Counters} {pref suff : List IntervalBounds} {cur : IntervalBounds} {r : Delivery σ} {store : RowStore} {doSetup : Bool} {specs : List SieveSpec} {o : Option (Delivery σ × RowStore × Counters)} (hl : ForIn.toList iv = pref ++ cur :: suff) (h2 : (intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).fst = 2) (h : o = none ∧ SiftIntervalsCounts b H sp1 es es3 mgs3 cl offsets pos cnt0 pref r store doSetup specs c) : r.quit = false → c = cnt0 + siftCounts b H sp1 es es3 mgs3 cl iv

At an interval with the code 2, the counters are those of Ratpoints.Sieve.siftCounts: the intervals before it are those that Ratpoints.Sieve.siftCounts counts.

theorem Ratpoints.Sieve.SiftIntervalsCounts.eq_counts_append {σ : Type} {b H sp1 : Nat} {es es3 : List SieveEntry} {mgs3 : List Nat} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {cnt0 c c' : Counters} {pref : List IntervalBounds} {cur : IntervalBounds} {r : Delivery σ} {store : RowStore} {doSetup : Bool} {specs : List SieveSpec} (h : SiftIntervalsCounts b H sp1 es es3 mgs3 cl offsets pos cnt0 pref r store doSetup specs c) (hc : c' = c + intervalCounts b H sp1 es es3 mgs3 cl cur) : c' = cnt0 + List.foldl (fun (x1 x2 : Counters) => x1 + x2) { sifts := 1 } (List.map (intervalCounts b H sp1 es es3 mgs3 cl) (pref ++ [cur]))

The counters after one more interval with the counts k, not with the code 2.

theorem Ratpoints.Sieve.SiftIntervalsCounts.append_of_one {σ : Type} {b H sp1 : Nat} {es es3 : List SieveEntry} {mgs3 : List Nat} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {cnt0 c : Counters} {pref : List IntervalBounds} {cur : IntervalBounds} {r : Delivery σ} {store : RowStore} {doSetup : Bool} {specs : List SieveSpec} {o : Option (Delivery σ × RowStore × Counters)} (h2 : ¬(intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).fst = 2) (h1 : (intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).fst = 1) (h : o = none ∧ SiftIntervalsCounts b H sp1 es es3 mgs3 cl offsets pos cnt0 pref r store doSetup specs c) : SiftIntervalsCounts b H sp1 es es3 mgs3 cl offsets pos cnt0 (pref ++ [cur]) r store doSetup specs c

An interval with the code 1, below -H, counts nothing.

theorem Ratpoints.Sieve.SiftIntervalsCounts.specs_eq_and_fits_of_eq_run_buildRows {σ : Type} {b H sp1 : Nat} {es es3 : List SieveEntry} {mgs3 : List Nat} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {cnt0 c : Counters} {pref : List IntervalBounds} {r : Delivery σ} {store st : RowStore} {doSetup : Bool} {specs specs' : List SieveSpec} {o : Option (Delivery σ × RowStore × Counters)} (hpos : cl.offset = some pos) (h : o = none ∧ SiftIntervalsCounts b H sp1 es es3 mgs3 cl offsets pos cnt0 pref r store doSetup specs c) (hr : (specs', st) = (buildRows (setRows store es (List.map (fun (e : SieveEntry) => b * e.dinv[cl.k]! % e.p) es) cl offsets).snd es (List.map (fun (e : SieveEntry) => b * e.dinv[cl.k]! % e.p) es) (setRows store es (List.map (fun (e : SieveEntry) => b * e.dinv[cl.k]! % e.p) es) cl offsets).fst store).run) : specs' = List.map Prod.fst (packedReads es b cl offsets pos) ∧ st.Fits es

The sieve specs that Ratpoints.Sieve.setRows and Ratpoints.Sieve.buildRows make at the first interval that asks for them are those of Ratpoints.Sieve.packedReads, and the store after them fits the entries (Ratpoints.Sieve.eq_map_fst_packedReads_of_eq_run_buildRows).

theorem Ratpoints.Sieve.SiftIntervalsCounts.specs_eq_and_fits_of_not_doSetup {σ : Type} {b H sp1 : Nat} {es es3 : List SieveEntry} {mgs3 : List Nat} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {cnt0 c : Counters} {pref : List IntervalBounds} {r : Delivery σ} {store : RowStore} {doSetup : Bool} {specs : List SieveSpec} {o : Option (Delivery σ × RowStore × Counters)} (h : o = none ∧ SiftIntervalsCounts b H sp1 es es3 mgs3 cl offsets pos cnt0 pref r store doSetup specs c) (hd : ¬doSetup = true) : specs = List.map Prod.fst (packedReads es b cl offsets pos) ∧ store.Fits es

Once the sieve specs are made, they are those of Ratpoints.Sieve.packedReads, and the store fits the entries.

theorem Ratpoints.Sieve.SiftIntervalsCounts.append_of_siftBits {σ : Type} {b H sp1 : Nat} {es es3 : List SieveEntry} {mgs3 : List Nat} {cl : NumClass} {offsets : Array Nat} {pos : Nat} {cnt0 c c' : Counters} {pref : List IntervalBounds} {cur : IntervalBounds} {r r' : Delivery σ} {store st : RowStore} {doSetup : Bool} {specs specs' : List SieveSpec} {o : Option (Delivery σ × RowStore × Counters)} {P : List (SieveSpec × (Int → Bool)) → Prop} (h : o = none ∧ SiftIntervalsCounts b H sp1 es es3 mgs3 cl offsets pos cnt0 pref r store doSetup specs c) (h2 : ¬(intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).fst = 2) (h1 : ¬(intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).fst = 1) (hsf : specs' = List.map Prod.fst (packedReads es b cl offsets pos) ∧ st.Fits es) (hinv : ∀ (e : SieveEntry), e ∈ es → e.HasInverses) (hoff : ∀ (n : Nat) (h : n < es.length), es[n].PackedFor cl offsets[pos + n]!) (hc : ∀ (sfs : List (SieveSpec × (Int → Bool))), specs' = List.map Prod.fst sfs → (∀ (sf : SieveSpec × (Int → Bool)), sf ∈ sfs → sf.fst.Reads sf.snd) → P sfs ∧ (r'.quit = false → c' = c + bitsCounts b { fn := fun (x : Unit) => fillChecks b H es3 mgs3 } cl (fun (j : Int) => (List.take sp1 sfs).all fun (x : SieveSpec × (Int → Bool)) => x.snd j) (fun (j : Int) => sfs.all fun (x : SieveSpec × (Int → Bool)) => x.snd j) (intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).snd.fst.toInt (intervalBits (Int64.ofNat b) cur (Int64.ofNat H) cl).snd.snd.toInt)) (hq : ¬r'.quit = true) (ds : Bool) : SiftIntervalsCounts b H sp1 es es3 mgs3 cl offsets pos cnt0 (pref ++ [cur]) r' st ds specs' c'

An interval whose bits Ratpoints.Sieve.siftBits sifts with the sieve specs of Ratpoints.Sieve.packedReads, after which the callback has not stopped the search, adds its counts (Ratpoints.Sieve.bitsCounts_packedReads_eq_intervalCounts).

theorem Ratpoints.Sieve.sift_spec {σ : Type} (process : Int → Int → Int → σ → Answer σ) (c : List Int) (d H A b : Nat) (fl : CheckFlags) (sp1 : Nat) (es : List SieveEntry) (mgs bp : List Nat) (cl : NumClass) (offsets : Array Nat) (es3 : List SieveEntry) (mgs3 : List Nat) (iv : Array IntervalBounds) (store : RowStore) (r : Delivery σ) (cnt : Counters) : ⦃ r.quit = false ∧ 1 ≤ A ∧ 0 < b ∧ b < 2 ^ 63 ∧ H < 2 ^ 63 ∧ (∀ (e : SieveEntry), e ∈ es3 → e.IsPrimeEntry) ∧ mgs3 = List.map (fun (x : SieveEntry) => magic x.p) es3 ∧ mgs = List.map (fun (x : SieveEntry) => magic x.p) es ∧ bp = List.map (fun (e : SieveEntry) => b * e.dinv[cl.k]! % e.p) es ∧ (∀ (e : SieveEntry), e ∈ es → e.HasInverses) ∧ store.Fits es ⦄ sift process c d H A b fl sp1 es mgs bp cl offsets es3 mgs3 iv store r cnt ⦃ fun (r' : Delivery σ × RowStore × Counters) => (∀ (w : UInt64) (pos : Nat) (rs : List (Int × Int)), cl.Packs w → cl.offset = some pos → (∀ (n : Nat) (h : n < es.length), es[n].PackedFor cl offsets[pos + n]!) → RangesFor iv b H rs → r'.fst = Delivery.deliver process r (List.flatMap (checkNumWith (BruteForce.scaledCoeffs c d ↑b) (if d % 2 = 1 then ↑b else 1) (↑b) fl) (List.filter (fun (a : Int) => inRanges rs a && classBit w a && survives (es ++ es3) b a) (BruteForce.numerators H)))) ∧ ∀ (pos : Nat), cl.offset = some pos → (∀ (n : Nat) (h : n < es.length), es[n].PackedFor cl offsets[pos + n]!) → r'.fst.quit = false → r'.snd.snd = cnt + siftCounts b H sp1 es es3 mgs3 cl iv ⦄

The sieve of one denominator b delivers, for every class word w that the class cl packs, the position pos of the row offsets of cl and the ranges rs of the numerators that the bounds iv of the search intervals give (Ratpoints.Sieve.RangesFor), quantified in the postcondition since the program does not mention them, the points of the check with the flags fl (Ratpoints.Sieve.checkNumWith) of the numerators -H, …, H in one of the ranges that pass w and survive the sieve entries of all three stages; when the callback does not stop the search, it adds the counts of Ratpoints.Sieve.siftCounts to the counters. The bounds 0 < b < 2 ^ 63 and H < 2 ^ 63 are those of the test for common factors on the words of the C code (Ratpoints.Sieve.accepted_spec); the rows built for b at the first interval that asks for them (the lazy set-up) are read at the offsets of the packing of cl (Ratpoints.Sieve.SieveEntry.PackedFor), from a store that fits the entries of the first two stages (Ratpoints.Sieve.RowStore.Fits), with the residues b dinv[k] mod p of Ratpoints.Sieve.fillBpList_eq_map.

theorem Ratpoints.Sieve.run_sift_eq_deliver_checkDen {σ : Type} (process : Int → Int → Int → σ → Answer σ) (c : List Int) (d H b : Nat) {fl : CheckFlags} (hc : fl.noCheck = false) (sp1 : Nat) {A : Nat} (hA : 1 ≤ A) (hb : 0 < b) (hb63 : b < 2 ^ 63) (hH : H < 2 ^ 63) {es es3 : List SieveEntry} {w : UInt64} {cl : NumClass} {pos : Nat} (offsets : Array Nat) {iv : Array IntervalBounds} {rs : List (Int × Int)} {store : RowStore} (hes : ∀ (e : SieveEntry), e ∈ es3 → e.IsPrimeEntry) (hcl : cl.Packs w) (hpos : cl.offset = some pos) (hinv : ∀ (e : SieveEntry), e ∈ es → e.HasInverses) (hoff : ∀ (n : Nat) (h : n < es.length), es[n].PackedFor cl offsets[pos + n]!) (hiv : RangesFor iv b H rs) (hs : store.Fits es) {r : Delivery σ} (hr : r.quit = false) (cnt : Counters) : (sift process c d H A b fl sp1 es (List.map (fun (x : SieveEntry) => magic x.p) es) (List.map (fun (e : SieveEntry) => b * e.dinv[cl.k]! % e.p) es) cl offsets es3 (List.map (fun (x : SieveEntry) => magic x.p) es3) iv store r cnt).run.fst = Delivery.deliver process r (List.filter (fun (p : Int × Int × Int) => !fl.noY || decide (0 ≤ p.snd.fst)) (List.map (if fl.reversed = true then swapPoint else id) (List.filter (fun (q : Int × Int × Int) => inRanges rs q.fst && classBit w q.fst) (checkDen c d H b (sieveDen H b (es ++ es3)).run).run.toList)))

Without RATPOINTS_NO_CHECK, the points that the sieve of one denominator delivers are those of the plain sieve of b with all the entries and its check, the reference of the bit arrays of words, whose numerators lie in one of the ranges rs and pass the class word w (Ratpoints.Sieve.classBit), mapped by Ratpoints.Sieve.swapPoint after a reversal, without those with y < 0 under RATPOINTS_NO_Y: both give the points of the brute-force reference over b and the numerators that survive the entries (Ratpoints.Sieve.sift_spec, Ratpoints.Sieve.sieveDen_spec, Ratpoints.Sieve.checkDen_spec, Ratpoints.BruteForce.pointsOfDen_filter).