The rows built into the tables of a run

The tables of rows of a run (Ratpoints.Sieve.RowStore) as the builders change them: the table of an entry after a row is stored into it (Ratpoints.Sieve.RowStore.getD_publish), which keeps the size of every table (Ratpoints.Sieve.RowStore.size_getD_publish), and the rows of the store after it, the row at its place and the others as they were (Ratpoints.Sieve.RowStore.row?_publish); a store that grows by rows satisfying a predicate, keeping its tables of rows with their sizes and its rows (Ratpoints.Sieve.RowStore.Grows); and the contracts of the calls of the builders through the tables of rows, as @[spec] theorems: the call through the function pointer of the entry of a factor (Ratpoints.Sieve.initFactorRow_spec), the rows of the factors of a product read from the tables of rows of their entries or built into them (Ratpoints.Sieve.factorRows_spec), the rows of a product (Ratpoints.Sieve.sieveInitProduct_spec), the row of a sieve entry built by its builder (Ratpoints.Sieve.SieveEntry.initRow_spec) and read from its table of rows or built into it (Ratpoints.Sieve.SieveEntry.fetchRow_spec). Every row that they return or store is a closed form (Ratpoints.Sieve.closedRow), and no row is replaced.

The invariant of the store of a run: its rows are those of a function R of the reference and the residue (Ratpoints.Sieve.RowStore.Holds), and the table of rows of every prime factor of the sieve entries has its row of 0 (Ratpoints.Sieve.StoreHolds), at which the builders of a prime are wrong; the entries fit R at their positions when their references and the kinds of their builders are those that Ratpoints.makeModulus sets and the closed forms of the rows of the entries and their factors are the rows of their references (Ratpoints.Sieve.SieveEntry.RowsFit), and the store fits the entries when it holds rows that they fit (Ratpoints.Sieve.RowStore.Fits). Every row fetched keeps the invariant (Ratpoints.Sieve.StoreHolds.of_fetchRow), and the sieve specs that Ratpoints.Sieve.setRows makes and Ratpoints.Sieve.buildRows completes have the closed forms of the rows of their entries (Ratpoints.Sieve.buildRows_setRows_map_spec), so that below the set-up of a denominator nothing reads the store; the store still holds the rows for every list of entries that contains those whose rows are built. The tables of rows made by the loop of the tables and with the sieve entries (Ratpoints.Sieve.primeRows, Ratpoints.Sieve.SieveEntry.addTables) keep the invariant (Ratpoints.Sieve.RowStore.Holds.addTables) and the rows of 0 of the primes (Ratpoints.Sieve.RowStore.PrimeZeroRows.row?_addTables_ne_none). For a run, R is the function of the closed forms of the rows of the table of each prime and the tables of each prime power as Ratpoints.Sieve.examinePrime and Ratpoints.Sieve.examinePower compute them, and of the entries of the products at their positions (Ratpoints.Sieve.runRows), which every sieve entry made by Ratpoints.makeModulus fits (Ratpoints.Sieve.SieveEntry.rowsFit_runRows), and which the store that the loop over the moduli of Ratpoints.sievingInfo makes holds (Ratpoints.Sieve.RowStore.MadeFor).

Main definitions

• Ratpoints.Sieve.RowStore.Grows: a store grown from another by rows satisfying a predicate.
• Ratpoints.Sieve.Factor.Buildable, Ratpoints.Sieve.Factor.Builds: what the builder of the rows of a factor needs of its tables, and the residues at which it is called.
• Ratpoints.Sieve.FactorRow, Ratpoints.Sieve.FactorRowsPre, Ratpoints.Sieve.ProductRowsPre, Ratpoints.Sieve.InitRowPre: the rows that building the rows of the factors of a product adds, and what building the rows of the factors, of a product and of an entry needs.
• Ratpoints.Sieve.RowStore.Holds, Ratpoints.Sieve.StoreHolds, Ratpoints.Sieve.RowStore.PrimeZeroRows: the rows of a store are those of a function of the reference and the residue, the invariant of the store of a run, and the rows of 0 of the tables of rows of the primes.
• Ratpoints.Sieve.SieveEntry.RefFits, Ratpoints.Sieve.SieveEntry.RowsFit: the reference and the kind of the builder of a sieve entry at its position, and what building its rows needs of it.
• Ratpoints.Sieve.BuildRowsPre, Ratpoints.Sieve.BuildRowsInvariant: what the loop of Ratpoints.Sieve.buildRows needs, and its invariant.
• Ratpoints.Sieve.runRows, Ratpoints.Sieve.RowStore.MadeFor: the rows of the references of a run, and the store as the loop of the tables and the tables of rows of the first entries of a run make it.
• Ratpoints.Sieve.RowStore.Fits: the store fits the sieve entries, holding rows that they fit at their positions, as the store of a run fits the entries of its first two stages before and after each denominator.

Main statements

• Ratpoints.Sieve.RowStore.getD_publish, Ratpoints.Sieve.RowStore.size_getD_publish: the table of an entry after a row is stored, and its size.
• Ratpoints.Sieve.RowStore.row?_publish: the rows of the store after a row is stored.
• Ratpoints.Sieve.initFactorRow_spec, Ratpoints.Sieve.factorRows_spec, Ratpoints.Sieve.sieveInitProduct_spec, Ratpoints.Sieve.SieveEntry.initRow_spec, Ratpoints.Sieve.SieveEntry.fetchRow_spec: the rows built through the tables of rows are closed forms.
• Ratpoints.Sieve.StoreHolds.fetchRow_pre, Ratpoints.Sieve.StoreHolds.of_fetchRow: a row of an entry that fits can be fetched, and the store still holds after it.
• Ratpoints.Sieve.buildRows_spec, Ratpoints.Sieve.buildRows_setRows_map_spec: the sieve specs of a denominator have the closed forms of the rows of their entries, and the store still holds the rows for every list of entries that contains them.
• Ratpoints.Sieve.RowStore.Holds.addTables, Ratpoints.Sieve.RowStore.PrimeZeroRows.addTables: the tables of rows of a sieve entry keep the invariant of the store.
• Ratpoints.Sieve.SieveEntry.rowsFit_runRows: a sieve entry as Ratpoints.makeModulus makes it fits the rows of the references of the run.
• Ratpoints.Sieve.RowStore.madeFor_nil, Ratpoints.Sieve.RowStore.MadeFor.addTables, Ratpoints.Sieve.RowStore.MadeFor.foldl_addTables, Ratpoints.Sieve.RowStore.MadeFor.storeHolds: the store of the loop over the moduli of Ratpoints.sievingInfo holds the rows of the references of the run.
• Ratpoints.Sieve.StoreHolds.of_factors, Ratpoints.Sieve.SieveEntry.RowsFit.of_eq, Ratpoints.Sieve.rowsFit_take, Ratpoints.Sieve.RowStore.Fits.take, Ratpoints.Sieve.RowStore.Fits.map_dinv: the invariant and the fit carry over to the first entries, those of the first two stages, and to the entries with the inverses of the strides.
• Ratpoints.Sieve.RowStore.Fits.buildRows_setRows: the sieve specs of a denominator have the closed forms of the rows of their entries, and the store after them still fits the entries.
• Ratpoints.Sieve.StoreHolds.buildRows_setRows_take: a store that holds the rows for all the entries of a run still holds them after the rows of the first entries are built.

Implementation notes

The file uses Lean core and Std only, as the contracts of the sieve do.

The tables of rows

theorem Ratpoints.Sieve.RowStore.getD_publish (s : RowStore) (ref ref' : EntryRef) (r : Nat) (row : Array UInt64) : Std.HashMap.getD (s.publish ref r row) ref' #[] = if ref = ref' then (Std.HashMap.getD s ref #[]).set! r (some row) else Std.HashMap.getD s ref' #[]

theorem Ratpoints.Sieve.RowStore.size_getD_publish (s : RowStore) (ref ref' : EntryRef) (r : Nat) (row : Array UInt64) : (Std.HashMap.getD (s.publish ref r row) ref' #[]).size = (Std.HashMap.getD s ref' #[]).size

theorem Ratpoints.Sieve.RowStore.row?_publish (s : RowStore) (ref ref' : EntryRef) (r r' : Nat) (row : Array UInt64) : (s.publish ref r row).row? ref' r' = if ref = ref' ∧ r = r' ∧ r < (Std.HashMap.getD s ref #[]).size then some row else s.row? ref' r'

The rows of the store after a row is stored: the row at its place, when the table has that place, and the others as they were.

structure Ratpoints.Sieve.RowStore.Grows (s s' : RowStore) (P : EntryRef → Nat → Array UInt64 → Prop) : Prop

The store s' keeps the tables of rows of s with their sizes and their rows, and its other rows, the row row at the residue r of the table of rows ref, satisfy P ref r row: what building rows into the tables of rows does to the store.

• size_eq (ref : EntryRef) : (Std.HashMap.getD s' ref #[]).size = (Std.HashMap.getD s ref #[]).size

  The tables of rows keep their sizes.

• row?_of_row? (ref : EntryRef) (r : Nat) (row : Array UInt64) : s.row? ref r = some row → s'.row? ref r = some row

  The rows are kept.

• row?_or (ref : EntryRef) (r : Nat) (row : Array UInt64) : s'.row? ref r = some row → s.row? ref r = some row ∨ P ref r row

  The other rows satisfy P.

theorem Ratpoints.Sieve.RowStore.Grows.refl (s : RowStore) (P : EntryRef → Nat → Array UInt64 → Prop) : s.Grows s P

theorem Ratpoints.Sieve.RowStore.Grows.trans {s1 s2 s3 : RowStore} {P : EntryRef → Nat → Array UInt64 → Prop} (h1 : s1.Grows s2 P) (h2 : s2.Grows s3 P) : s1.Grows s3 P

theorem Ratpoints.Sieve.RowStore.grows_publish {s : RowStore} {P : EntryRef → Nat → Array UInt64 → Prop} {ref : EntryRef} {r : Nat} {row : Array UInt64} (h : s.row? ref r = none) (hP : P ref r row) : s.Grows (s.publish ref r row) P

A row stored at a place where the store has no row.

The builder of the entry of a factor

def Ratpoints.Sieve.Factor.Buildable : Factor → Prop

What the builder of the rows of a factor needs of its tables: a positive modulus; for a prime p the inverses of its residues below p, and p mod 64 ≠ 0 for a prime of at least 64, whose builder CODE_INIT_SIEVE2 shifts by p mod 64; for a prime power m at most 64 Ratpoints.modWords and its inverses below m.

Equations

• (Ratpoints.Sieve.Factor.prime t).Buildable = (0 < t.p ∧ (64 ≤ t.p → t.p % 64 ≠ 0) ∧ ∀ (r : Nat), r < t.p → t.inverses[r]! < t.p)
• (Ratpoints.Sieve.Factor.power pw).Buildable = (0 < pw.m ∧ pw.m ≤ 64 * Ratpoints.modWords ∧ ∀ (x : Nat), x < pw.m → pw.inv[x]! < pw.m)

def Ratpoints.Sieve.Factor.Builds : Factor → Nat → Prop

The residues at which the builder of the rows of a factor is called: below the modulus, and other than 0 for a prime, whose row of 0 is in its table of rows from the start (Ratpoints.Sieve.primeRows), the builders of a prime being wrong at 0.

Equations

• (Ratpoints.Sieve.Factor.prime t).Builds x✝ = (0 < x✝ ∧ x✝ < t.p)
• (Ratpoints.Sieve.Factor.power pw).Builds x✝ = (x✝ < pw.m)

theorem Ratpoints.Sieve.Factor.Buildable.modulus_pos {f : Factor} (h : f.Buildable) : 0 < f.modulus

@[simp]

theorem Ratpoints.Sieve.Factor.init_prime (t : Entry) : (prime t).init = sieveInit t.p

@[simp]

theorem Ratpoints.Sieve.Factor.init_power (pw : Power) : (power pw).init = RowInit.power

theorem Ratpoints.Sieve.sieveInit_of_lt {p : Nat} (h : p < 64) : sieveInit p = RowInit.sieve1

theorem Ratpoints.Sieve.sieveInit_of_not_lt {p : Nat} (h : ¬p < 64) : sieveInit p = RowInit.sieve2

theorem Ratpoints.Sieve.initFactorRow_pre_sieve1 {t : Entry} {b : Nat} (hp : t.p < 64) (pre : (Factor.prime t).Buildable ∧ (Factor.prime t).Builds b) : 0 < b ∧ b < t.p ∧ t.p < 64 ∧ t.inverses[b]! < t.p

theorem Ratpoints.Sieve.initFactorRow_pre_sieve2 {t : Entry} {b : Nat} (hp : ¬t.p < 64) (pre : (Factor.prime t).Buildable ∧ (Factor.prime t).Builds b) : 0 < b ∧ b < t.p ∧ 64 ≤ t.p ∧ t.p % 64 ≠ 0 ∧ t.inverses[b]! < t.p

theorem Ratpoints.Sieve.initFactorRow_pre_power {pw : Power} {b : Nat} (pre : (Factor.power pw).Buildable ∧ (Factor.power pw).Builds b) : b < pw.m ∧ pw.m ≤ 64 * modWords ∧ pw.inv[b]! < pw.m

theorem Ratpoints.Sieve.initFactorRow_spec (f : Factor) (ref : EntryRef) (b : Nat) (store : RowStore) : ⦃ f.Buildable ∧ f.Builds b ⦄ initFactorRow f.init ref f b store ⦃ fun (r : Array UInt64 × RowStore) => r.fst = closedRow f.admits f.modulus b ∧ r.snd = store.publish ref b (closedRow f.admits f.modulus b) ⦄

The row of the residue b built by the builder of the kind of the factor f, the call through the function pointer of the entry of the factor, is the closed form of the row of b of the factor, for the residues at which it is called (Ratpoints.Sieve.Factor.Builds), and the builder stores it into the table of rows ref.

The rows of the factors of a product

def Ratpoints.Sieve.FactorRow (e : SieveEntry) (ref : EntryRef) (r : Nat) (row : Array UInt64) : Prop

A row that building the rows of the factors of e adds to the store: at the residue r of the table of rows ref, the closed form of the row of r of a factor of e whose entry is ref.

Equations

• Ratpoints.Sieve.FactorRow e ref r row = ∃ (f : Ratpoints.Sieve.Factor), f ∈ e.factors ∧ f.ref = ref ∧ row = Ratpoints.Sieve.closedRow f.admits f.modulus r

structure Ratpoints.Sieve.FactorRowsPre (e : SieveEntry) (store : RowStore) : Prop

What building the rows of the factors of e needs of them and of the store: their builders have what they need, the rows in the tables of rows of their entries are closed forms, a row that is absent below the modulus is one at which the builder of the factor may be called (for a prime, its row of 0 is in its table of rows), and two factors with one entry have the same closed forms of their rows.

• buildable (f : Factor) : f ∈ e.factors → f.Buildable

  The builders of the factors have what they need.

• rows (f : Factor) : f ∈ e.factors → ∀ (r : Nat) (row : Array UInt64), store.row? f.ref r = some row → row = closedRow f.admits f.modulus r

  The rows in the tables of rows of the entries of the factors are closed forms.

• builds (f : Factor) : f ∈ e.factors → ∀ (r : Nat), r < f.modulus → store.row? f.ref r = none → f.Builds r

  A row absent below the modulus is one that the builder of the factor may build.

• coherent (f : Factor) : f ∈ e.factors → ∀ (f' : Factor), f' ∈ e.factors → f.ref = f'.ref → closedRow f.admits f.modulus = closedRow f'.admits f'.modulus

  Two factors with one entry have the same closed forms of their rows.

def Ratpoints.Sieve.FactorRowsInvariant (e : SieveEntry) (b : Nat) (store : RowStore) (pref : List Factor) (st : RowStore × Array (Array UInt64)) : Prop

The invariant of the loop of Ratpoints.Sieve.factorRows over the factors pref done, on the store and the rows: the rows of those factors in closed form at the residues of b, and the store grown by rows of factors.

Equations

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

theorem Ratpoints.Sieve.factorRowsInvariant_nil (e : SieveEntry) (b : Nat) (store : RowStore) : FactorRowsInvariant e b store [] (store, #[])

theorem Ratpoints.Sieve.FactorRowsPre.eq_closedRow {e : SieveEntry} {store s : RowStore} (pre : FactorRowsPre e store) (hs : store.Grows s (FactorRow e)) {f : Factor} (hf : f ∈ e.factors) {r : Nat} {row : Array UInt64} (h : s.row? f.ref r = some row) : row = closedRow f.admits f.modulus r

A row of a factor of e present in a store grown from one where they were closed forms is the closed form of the factor: rows are never replaced, and two factors with one entry have the same closed forms of their rows.

theorem Ratpoints.Sieve.FactorRowsInvariant.push_some {e : SieveEntry} {b : Nat} {store : RowStore} {pref suff : List Factor} {f : Factor} {st : RowStore × Array (Array UInt64)} {fr : Array UInt64} (pre : FactorRowsPre e store) (hl : e.factors = pref ++ f :: suff) (h : FactorRowsInvariant e b store pref st) (hr : st.fst.row? f.ref (b % f.modulus) = some fr) : FactorRowsInvariant e b store (pref ++ [f]) (st.fst, st.snd.push fr)

A factor whose row is in the store.

theorem Ratpoints.Sieve.FactorRowsInvariant.push_none {e : SieveEntry} {b : Nat} {store : RowStore} {pref suff : List Factor} {f : Factor} {st : RowStore × Array (Array UInt64)} {r : Array UInt64 × RowStore} (hl : e.factors = pref ++ f :: suff) (h : FactorRowsInvariant e b store pref st) (hr : st.fst.row? f.ref (b % f.modulus) = none) (hb : r.fst = closedRow f.admits f.modulus (b % f.modulus) ∧ r.snd = st.fst.publish f.ref (b % f.modulus) (closedRow f.admits f.modulus (b % f.modulus))) : FactorRowsInvariant e b store (pref ++ [f]) (r.snd, st.snd.push r.fst)

A factor whose row the builder of its entry builds into the store.

theorem Ratpoints.Sieve.FactorRowsInvariant.pre_none {e : SieveEntry} {b : Nat} {store : RowStore} {pref suff : List Factor} {f : Factor} {st : RowStore × Array (Array UInt64)} (pre : FactorRowsPre e store) (hl : e.factors = pref ++ f :: suff) (h : FactorRowsInvariant e b store pref st) (hr : st.fst.row? f.ref (b % f.modulus) = none) : f.Buildable ∧ f.Builds (b % f.modulus)

The builder of the entry of a factor is called at a residue at which it may be.

theorem Ratpoints.Sieve.FactorRowsInvariant.post {e : SieveEntry} {b : Nat} {store : RowStore} {st : RowStore × Array (Array UInt64)} (h : FactorRowsInvariant e b store e.factors st) : st.snd.toList = List.map (fun (f : Factor) => closedRow f.admits f.modulus (b % f.modulus)) e.factors ∧ store.Grows st.fst (FactorRow e)

theorem Ratpoints.Sieve.factorRows_spec (e : SieveEntry) (b : Nat) (store : RowStore) : ⦃ FactorRowsPre e store ⦄ factorRows e b store ⦃ fun (r : Array (Array UInt64) × RowStore) => r.fst.toList = List.map (fun (f : Factor) => closedRow f.admits f.modulus (b % f.modulus)) e.factors ∧ store.Grows r.snd (FactorRow e) ⦄

The rows of the factors of e at the residues of b modulo their moduli, read from the tables of rows of their entries or built into them, are their closed forms, and the store grows by rows of factors (Ratpoints.Sieve.FactorRow), never replacing one.

The rows of a product

structure Ratpoints.Sieve.ProductRowsPre (e : SieveEntry) (store : RowStore) : Prop

What building the row of a product e needs: what building the rows of its factors needs (Ratpoints.Sieve.FactorRowsPre), a positive modulus, at least one factor, and the moduli of the factors dividing the modulus.

• factorRows : FactorRowsPre e store

  What building the rows of the factors needs.

• pos : 0 < e.p

  The modulus is positive.

• one_le_length : 1 ≤ e.factors.length

  The product has a factor.

• dvd (f : Factor) : f ∈ e.factors → f.modulus ∣ e.p

  The moduli of the factors divide the modulus.

theorem Ratpoints.Sieve.ProductRowsPre.pos_and_dvd {e : SieveEntry} {store : RowStore} (pre : ProductRowsPre e store) {i : Nat} (hi : i < e.factors.length) : 0 < e.factors[i]!.modulus ∧ e.factors[i]!.modulus ∣ e.p

theorem Ratpoints.Sieve.sieveInitProduct_pre_copy {e : SieveEntry} {store : RowStore} (pre : ProductRowsPre e store) : 0 < e.factors[0]!.modulus ∧ e.factors[0]!.modulus ∣ e.p ∧ e.p * rbaPack ≤ (e.p + chunk - 1) * rbaPack

theorem Ratpoints.Sieve.sieveInitProduct_pre_and {e : SieveEntry} {store : RowStore} {frows : Array (Array UInt64)} {row : Vector UInt64 ((e.p + chunk - 1) * rbaPack)} (pre : ProductRowsPre e store) (h : ∀ (y : Nat), y < e.p * rbaPack → row[y]! = factorWord e frows 0 y) : (∀ (i : Nat), i < e.factors.length → 0 < e.factors[i]!.modulus ∧ e.factors[i]!.modulus ∣ e.p) ∧ e.p * rbaPack ≤ (e.p + chunk - 1) * rbaPack ∧ ∀ (y : Nat), y < e.p * rbaPack → row[y]! = factorWord e frows 0 y

theorem Ratpoints.Sieve.productCopies_init {e : SieveEntry} {frows : Array (Array UInt64)} {n : Nat} {row : Vector UInt64 n} (h : ∀ (y : Nat), y < e.p * rbaPack → row[y]! = productWord e frows e.factors.length y) {y : Nat} (hy : y < (e.p + [].length) * rbaPack) : row[y]! = productWord e frows e.factors.length (y % (e.p * rbaPack))

theorem Ratpoints.Sieve.productCopies_storeBitArray {e : SieveEntry} {frows : Array (Array UInt64)} {cur : Nat} {pref suff : List Nat} {row : Vector UInt64 ((e.p + chunk - 1) * rbaPack)} {store : RowStore} (pre : ProductRowsPre e store) (hl : ForIn.toList [:chunk - 1] = pref ++ cur :: suff) (h : ∀ (y : Nat), y < (e.p + pref.length) * rbaPack → row[y]! = productWord e frows e.factors.length (y % (e.p * rbaPack))) (y : Nat) : y < (e.p + (pref ++ [cur]).length) * rbaPack → (storeBitArray row (e.p + cur) row cur)[y]! = productWord e frows e.factors.length (y % (e.p * rbaPack))

A copy of bit array cur of the row of a product after its first m bit arrays.

theorem Ratpoints.Sieve.productCopies_post {e : SieveEntry} {frows : Array (Array UInt64)} {row : Vector UInt64 ((e.p + chunk - 1) * rbaPack)} (h : ∀ (y : Nat), y < (e.p + (ForIn.toList [:chunk - 1]).length) * rbaPack → row[y]! = productWord e frows e.factors.length (y % (e.p * rbaPack))) {y : Nat} (hy : y < (e.p + chunk - 1) * rbaPack) : row[y]! = productWord e frows e.factors.length (y % (e.p * rbaPack))

theorem Ratpoints.Sieve.sieveInitProduct_post {e : SieveEntry} {b : Nat} {store store' : RowStore} {frows : Array (Array UInt64)} {row : Vector UInt64 ((e.p + chunk - 1) * rbaPack)} (pre : ProductRowsPre e store) (hf : frows.toList = List.map (fun (f : Factor) => closedRow f.admits f.modulus (b % f.modulus)) e.factors ∧ store.Grows store' (FactorRow e)) (hrow : ∀ (y : Nat), y < (e.p + (ForIn.toList [:chunk - 1]).length) * rbaPack → row[y]! = productWord e frows e.factors.length (y % (e.p * rbaPack))) : (row, store'.publish e.ref b row.toArray).fst.toArray = closedRow e.admits e.p b ∧ ∃ (s : RowStore), store.Grows s (FactorRow e) ∧ (row, store'.publish e.ref b row.toArray).snd = s.publish e.ref b (closedRow e.admits e.p b)

The row of the product built from the closed forms of the rows of its factors is the closed form of its row, and so is what the builder stores, into the store grown by the rows of the factors.

theorem Ratpoints.Sieve.sieveInitProduct_spec (e : SieveEntry) (b : Nat) (store : RowStore) : ⦃ ProductRowsPre e store ⦄ sieveInitProduct e b store ⦃ fun (r : Vector UInt64 ((e.p + chunk - 1) * rbaPack) × RowStore) => r.fst.toArray = closedRow e.admits e.p b ∧ ∃ (s : RowStore), store.Grows s (FactorRow e) ∧ r.snd = s.publish e.ref b (closedRow e.admits e.p b) ⦄

The row of the residue b of the product e, of a modulus m > 0 that the positive moduli of its factors divide, as _ratpoints_sieve_init_product builds it, is the closed form of the row of b of the product, and the builder stores it into the table of rows of the entry of the product, in the store grown by the rows of the factors that it builds into their tables of rows first (Ratpoints.Sieve.factorRows_spec).

The rows of the entries of a run

def Ratpoints.Sieve.InitRowPre (e : SieveEntry) (b : Nat) (store : RowStore) : Prop

What building the row of the residue b of the sieve entry e by its builder needs: for a product, what building its row needs (Ratpoints.Sieve.ProductRowsPre); for a prime or a prime power, its one factor f, whose modulus, entry and kind are those of e, with a builder that has what it needs, called at a residue at which it may be.

Equations

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

theorem Ratpoints.Sieve.Factor.init_ne_product (f : Factor) : f.init ≠ RowInit.product

theorem Ratpoints.Sieve.SieveEntry.initRow_spec (e : SieveEntry) (b : Nat) (store : RowStore) : ⦃ InitRowPre e b store ⦄ e.initRow b store ⦃ fun (r : Array UInt64 × RowStore) => r.fst = closedRow e.admits e.p b ∧ ∃ (s : RowStore), store.Grows s (FactorRow e) ∧ r.snd = s.publish e.ref b (closedRow e.admits e.p b) ⦄

The row of the residue b of the sieve entry e built by its builder is the closed form of the row of b of the entry, stored into the table of rows of the entry, in the store grown by the rows of the factors of a product.

theorem Ratpoints.Sieve.SieveEntry.fetchRow_spec (e : SieveEntry) (b : Nat) (store : RowStore) : ⦃ (∀ (row : Array UInt64), store.row? e.ref b = some row → row = closedRow e.admits e.p b) ∧ (store.row? e.ref b = none → InitRowPre e b store) ⦄ e.fetchRow b store ⦃ fun (r : Array UInt64 × RowStore) => r.fst = closedRow e.admits e.p b ∧ (r.snd = store ∨ ∃ (s : RowStore), store.Grows s (FactorRow e) ∧ r.snd = s.publish e.ref b (closedRow e.admits e.p b)) ⦄

The row of the residue b of the sieve entry e from the table of rows of its entry, read there when it is present, a closed form, or built by the builder of the entry: the closed form of the row of b of the entry, and the store as it was or grown by the rows of the factors of a product with the row stored into the table of rows of the entry.

The tables of rows of a run

def Ratpoints.Sieve.RowStore.Holds (R : EntryRef → Nat → Array UInt64) (s : RowStore) : Prop

The rows of the store s are those of R, a row for each reference and residue: every row present at the residue r of the table of rows of ref is R ref r.

Equations

• Ratpoints.Sieve.RowStore.Holds R s = ∀ (ref : Ratpoints.Sieve.EntryRef) (r : Nat) (row : Array UInt64), s.row? ref r = some row → row = R ref r

theorem Ratpoints.Sieve.RowStore.Holds.publish {R : EntryRef → Nat → Array UInt64} {s : RowStore} (h : Holds R s) {ref : EntryRef} {r : Nat} {row : Array UInt64} (hrow : row = R ref r) : Holds R (s.publish ref r row)

theorem Ratpoints.Sieve.RowStore.Holds.of_grows {R : EntryRef → Nat → Array UInt64} {s s' : RowStore} {P : EntryRef → Nat → Array UInt64 → Prop} (h : Holds R s) (hs : s.Grows s' P) (hP : ∀ (ref : EntryRef) (r : Nat) (row : Array UInt64), P ref r row → row = R ref r) : Holds R s'

theorem Ratpoints.Sieve.RowStore.Grows.row?_ne_none {s s' : RowStore} {P : EntryRef → Nat → Array UInt64 → Prop} (hs : s.Grows s' P) {ref : EntryRef} {r : Nat} (h : s.row? ref r ≠ none) : s'.row? ref r ≠ none

theorem Ratpoints.Sieve.RowStore.row?_publish_ne_none {s : RowStore} {ref ref' : EntryRef} {r r' : Nat} {row : Array UInt64} (h : s.row? ref' r' ≠ none) : (s.publish ref r row).row? ref' r' ≠ none

structure Ratpoints.Sieve.StoreHolds (R : EntryRef → Nat → Array UInt64) (es : List SieveEntry) (s : RowStore) : Prop

The store s of a run holds the rows R of the references (Ratpoints.Sieve.RowStore.Holds), and the table of rows of every prime factor of the sieve entries es has its row of 0 (Ratpoints.Sieve.primeRows), at which the builders of a prime are wrong: what building the rows of the entries needs of the store, beside what it needs of each entry (Ratpoints.Sieve.SieveEntry.RowsFit).

• holds : RowStore.Holds R s

  The rows of the store are those of R.

• zero (e : SieveEntry) : e ∈ es → ∀ (t : Entry), Factor.prime t ∈ e.factors → s.row? (EntryRef.prime t.p) 0 ≠ none

  The table of rows of every prime factor has its row of 0.

def Ratpoints.Sieve.SieveEntry.RefFits (e : SieveEntry) (n : Nat) : Prop

The sieve entry e at the position n of the moduli holds the reference to its table of rows and the kind of its builder as Ratpoints.makeModulus sets them (Ratpoints.Sieve.SieveEntry.refInit): for one factor, the modulus, the reference and the kind of the factor; otherwise the product's own table of rows, by its position, and the builder of the rows of a product.

Equations

• e.RefFits n = match e.factors with | [f] => e.p = f.modulus ∧ e.ref = f.ref ∧ e.init = f.init | x => e.ref = Ratpoints.Sieve.EntryRef.product n ∧ e.init = Ratpoints.Sieve.RowInit.product

theorem Ratpoints.Sieve.SieveEntry.refFits_of_refInit_eq {e : SieveEntry} {n : Nat} (h : (e.ref, e.init) = refInit n e.factors) (hp : ∀ (f : Factor), e.factors = [f] → e.p = f.modulus) : e.RefFits n

A sieve entry whose reference and kind of builder are those that Ratpoints.Sieve.SieveEntry.refInit gives at the position n, as Ratpoints.makeModulus sets them, and whose modulus is that of its factor when it has one, fits them.

structure Ratpoints.Sieve.SieveEntry.RowsFit (e : SieveEntry) (R : EntryRef → Nat → Array UInt64) (n : Nat) : Prop

What building the rows of the sieve entry e at the position n of the moduli needs of it, for the rows R of the references (Ratpoints.Sieve.RowStore.Holds): its reference and kind (Ratpoints.Sieve.SieveEntry.RefFits), a positive modulus, at least one factor, the moduli of the factors dividing the modulus, builders of the factors that have what they need (Ratpoints.Sieve.Factor.Buildable), and the rows of its reference and of the references of its factors the closed forms of their rows (Ratpoints.Sieve.closedRow).

• refFits : e.RefFits n

  The reference and the kind of the builder are those that Ratpoints.makeModulus sets.

• pos : 0 < e.p

  The modulus is positive.

• factors_ne_nil : e.factors ≠ []

  The entry has a factor.

• dvd (f : Factor) : f ∈ e.factors → f.modulus ∣ e.p

  The moduli of the factors divide the modulus.

• buildable (f : Factor) : f ∈ e.factors → f.Buildable

  The builders of the factors have what they need.

• ref_rows : R e.ref = closedRow e.admits e.p

  The rows of the reference are the closed forms of the rows of the entry.

• factor_rows (f : Factor) : f ∈ e.factors → R f.ref = closedRow f.admits f.modulus

  The rows of the reference of each factor are the closed forms of the rows of the factor.

theorem Ratpoints.Sieve.StoreHolds.builds {R : EntryRef → Nat → Array UInt64} {es : List SieveEntry} {s : RowStore} (hs : StoreHolds R es s) {e : SieveEntry} (he : e ∈ es) {f : Factor} (hf : f ∈ e.factors) {r : Nat} (hr : r < f.modulus) (h : s.row? f.ref r = none) : f.Builds r

A row absent below the modulus of a factor of an entry is one at which the builder of the factor may be called (Ratpoints.Sieve.Factor.Builds): for a prime, its row of 0 is present.

theorem Ratpoints.Sieve.SieveEntry.RowsFit.factorRowsPre {e : SieveEntry} {R : EntryRef → Nat → Array UInt64} {n : Nat} (hfit : e.RowsFit R n) {es : List SieveEntry} {s : RowStore} (hs : StoreHolds R es s) (he : e ∈ es) : FactorRowsPre e s

What building the rows of the factors of an entry needs (Ratpoints.Sieve.FactorRowsPre).

theorem Ratpoints.Sieve.StoreHolds.initRowPre {R : EntryRef → Nat → Array UInt64} {es : List SieveEntry} {s : RowStore} (hs : StoreHolds R es s) {e : SieveEntry} (he : e ∈ es) {n : Nat} (hfit : e.RowsFit R n) {b : Nat} (hb : b < e.p) (hr : s.row? e.ref b = none) : InitRowPre e b s

What building the row of the residue b < p of an entry needs (Ratpoints.Sieve.InitRowPre), when the row is absent: for a prime, b ≠ 0, since its row of 0 is present.

theorem Ratpoints.Sieve.StoreHolds.fetchRow_pre {R : EntryRef → Nat → Array UInt64} {es : List SieveEntry} {s : RowStore} (hs : StoreHolds R es s) {e : SieveEntry} (he : e ∈ es) {n : Nat} (hfit : e.RowsFit R n) {b : Nat} (hb : b < e.p) : (∀ (row : Array UInt64), s.row? e.ref b = some row → row = closedRow e.admits e.p b) ∧ (s.row? e.ref b = none → InitRowPre e b s)

The precondition of Ratpoints.Sieve.SieveEntry.fetchRow_spec for the residue b < p of an entry.

theorem Ratpoints.Sieve.StoreHolds.of_fetchRow {R : EntryRef → Nat → Array UInt64} {es : List SieveEntry} {s s' : RowStore} (hs : StoreHolds R es s) {e : SieveEntry} {n : Nat} (hfit : e.RowsFit R n) {b : Nat} (h : s' = s ∨ ∃ (s'' : RowStore), s.Grows s'' (FactorRow e) ∧ s' = s''.publish e.ref b (closedRow e.admits e.p b)) : StoreHolds R es s'

The store after a row of an entry is fetched (Ratpoints.Sieve.SieveEntry.fetchRow_spec) still holds.

The making of the tables of rows

theorem Ratpoints.Sieve.RowStore.row?_insertIfNew (s : RowStore) (k ref : EntryRef) (v : Array (Option (Array UInt64))) (r : Nat) : row? (Std.HashMap.insertIfNew s k v) ref r = if k = ref ∧ ¬k ∈ s then v.getD r none else s.row? ref r

theorem Ratpoints.Sieve.RowStore.row?_eq_none_of_not_mem {s : RowStore} {ref : EntryRef} (h : ¬ref ∈ s) (r : Nat) : s.row? ref r = none

theorem Ratpoints.Sieve.RowStore.row?_insertIfNew_of_ne_none {s : RowStore} {ref : EntryRef} {r : Nat} (h : s.row? ref r ≠ none) (k : EntryRef) (v : Array (Option (Array UInt64))) : row? (Std.HashMap.insertIfNew s k v) ref r = s.row? ref r

A table of rows made where none was keeps the rows of the store.

theorem Ratpoints.Sieve.RowStore.Holds.insertIfNew {R : EntryRef → Nat → Array UInt64} {s : RowStore} (h : Holds R s) {k : EntryRef} {v : Array (Option (Array UInt64))} (hv : ∀ (r : Nat) (row : Array UInt64), v.getD r none = some row → row = R k r) : Holds R (Std.HashMap.insertIfNew s k v)

def Ratpoints.Sieve.RowStore.PrimeZeroRows (s : RowStore) : Prop

Every table of rows of a prime in the store has its row of 0, as the loop of the tables and the sieve entries make the tables of rows of the primes (Ratpoints.Sieve.primeRows).

Equations

• s.PrimeZeroRows = ∀ (p : Nat), Ratpoints.Sieve.EntryRef.prime p ∈ s → s.row? (Ratpoints.Sieve.EntryRef.prime p) 0 ≠ none

theorem Ratpoints.Sieve.RowStore.PrimeZeroRows.insertIfNew {s : RowStore} (h : s.PrimeZeroRows) {k : EntryRef} {v : Array (Option (Array UInt64))} (hv : ∀ (p : Nat), k = EntryRef.prime p → v.getD 0 none ≠ none) : PrimeZeroRows (Std.HashMap.insertIfNew s k v)

theorem Ratpoints.Sieve.getD_primeRows (p r : Nat) : (primeRows p).getD r none = if r = 0 then some (sieves0 p) else none

theorem Ratpoints.Sieve.RowStore.holds_empty (R : EntryRef → Nat → Array UInt64) : Holds R ∅

theorem Ratpoints.Sieve.RowStore.primeZeroRows_empty : ∅.PrimeZeroRows

theorem Ratpoints.Sieve.RowStore.Holds.insertIfNew_primeRows {R : EntryRef → Nat → Array UInt64} {s : RowStore} (h : Holds R s) {p : Nat} (hR : R (EntryRef.prime p) 0 = sieves0 p) : Holds R (Std.HashMap.insertIfNew s (EntryRef.prime p) (primeRows p))

The table of rows of the prime p with its row of 0 (Ratpoints.Sieve.primeRows) keeps the rows of the store those of R when the row of 0 of p is that of R.

theorem Ratpoints.Sieve.RowStore.PrimeZeroRows.insertIfNew_primeRows {s : RowStore} (h : s.PrimeZeroRows) (p : Nat) : PrimeZeroRows (Std.HashMap.insertIfNew s (EntryRef.prime p) (primeRows p))

theorem Ratpoints.Sieve.RowStore.Holds.insertIfNew_replicate_none {R : EntryRef → Nat → Array UInt64} {s : RowStore} (h : Holds R s) (k : EntryRef) (n : Nat) : Holds R (Std.HashMap.insertIfNew s k (Array.replicate n none))

theorem Ratpoints.Sieve.RowStore.PrimeZeroRows.insertIfNew_newRows {s : RowStore} (h : s.PrimeZeroRows) (f : Factor) : PrimeZeroRows (Std.HashMap.insertIfNew s f.ref f.newRows)

theorem Ratpoints.Sieve.RowStore.Holds.insertIfNew_newRows {R : EntryRef → Nat → Array UInt64} {s : RowStore} (h : Holds R s) {f : Factor} (hR : ∀ (t : Entry), f = Factor.prime t → R (EntryRef.prime t.p) 0 = sieves0 t.p) : Holds R (Std.HashMap.insertIfNew s f.ref f.newRows)

theorem Ratpoints.Sieve.SieveEntry.RefFits.ref_eq_of_init_eq {e : SieveEntry} {n : Nat} (h : e.RefFits n) (hinit : e.init = RowInit.product) : e.ref = EntryRef.product n

A sieve entry whose builder is that of a product has the product's own table of rows.

theorem Ratpoints.Sieve.RowStore.Holds.addTables {R : EntryRef → Nat → Array UInt64} {s : RowStore} (h : Holds R s) {e : SieveEntry} (hR : ∀ (t : Entry), Factor.prime t ∈ e.factors → R (EntryRef.prime t.p) 0 = sieves0 t.p) : Holds R (e.addTables s)

The store with the tables of rows of a sieve entry holds the rows R of the references when the store does and the rows of 0 of the primes of the entry are those of R.

theorem Ratpoints.Sieve.RowStore.PrimeZeroRows.addTables {s : RowStore} (h : s.PrimeZeroRows) {e : SieveEntry} {n : Nat} (he : e.RefFits n) : (e.addTables s).PrimeZeroRows

theorem Ratpoints.Sieve.SieveEntry.row?_addTables_of_ne_none {s : RowStore} {ref : EntryRef} {r : Nat} (h : s.row? ref r ≠ none) (e : SieveEntry) : (e.addTables s).row? ref r = s.row? ref r

theorem Ratpoints.Sieve.SieveEntry.mem_addTables (e : SieveEntry) (s : RowStore) {f : Factor} (hf : f ∈ e.factors) : f.ref ∈ e.addTables s

theorem Ratpoints.Sieve.RowStore.PrimeZeroRows.row?_addTables_ne_none {s : RowStore} (h : s.PrimeZeroRows) {e : SieveEntry} {n : Nat} (he : e.RefFits n) {t : Entry} (ht : Factor.prime t ∈ e.factors) : (e.addTables s).row? (EntryRef.prime t.p) 0 ≠ none

The table of rows of a prime factor of a sieve entry has its row of 0 once the tables of rows of the entry are made, when every table of rows of a prime has it.

The rows of the sieve specs of a denominator

structure Ratpoints.Sieve.BuildRowsPre (R : EntryRef → Nat → Array UInt64) (L : List SieveEntry) (missing : Bool) (es : List SieveEntry) (bp : List Nat) (specs : List SieveSpec) (store : RowStore) : Prop

What building the rows of the sieve specs specs of the entries es at the residues bp (Ratpoints.Sieve.buildRows) needs: the store holds the rows R for a list L of entries that contains es, the entries fit them at their positions, the residues are below the moduli, and each spec has the end p and its row, or none yet, all rows when missing says none is missing.

• holds : StoreHolds R L store

  The store holds the rows R for the entries L.

• subset : es ⊆ L

  The entries are among L.

• fit (n : Nat) (h : n < es.length) : es[n].RowsFit R n

  The entries fit the rows R at their positions.

• lt (n : Nat) (h : n < es.length) : bp[n]! < es[n].p

  The residues are below the moduli.

• length_eq : specs.length = es.length

  A spec for each entry.

• stop_eq (n : Nat) : n < specs.length → specs[n]!.stop = es[n]!.p

  The specs have the end p.

• row_eq (n : Nat) : n < specs.length → specs[n]!.row = #[] ∨ specs[n]!.row = closedRow es[n]!.admits es[n]!.p bp[n]!

  The specs have their rows or none yet.

• row_eq_of_missing : missing = false → ∀ (n : Nat), n < specs.length → specs[n]!.row = closedRow es[n]!.admits es[n]!.p bp[n]!

  The specs have their rows when none is missing.

def Ratpoints.Sieve.BuildRowsInvariant (R : EntryRef → Nat → Array UInt64) (L es : List SieveEntry) (bp : List Nat) (specs : List SieveSpec) (k : Nat) (st : List SieveSpec × RowStore) : Prop

The invariant of the loop of Ratpoints.Sieve.buildRows after the specs below k, on the specs and the store: the store holds the rows R for the entries L, and each spec has its row and the end p, or for k ≤ i none yet.

Equations

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

theorem Ratpoints.Sieve.BuildRowsPre.buildRowsInvariant {R : EntryRef → Nat → Array UInt64} {L : List SieveEntry} {missing : Bool} {es : List SieveEntry} {bp : List Nat} {specs : List SieveSpec} {store : RowStore} (pre : BuildRowsPre R L missing es bp specs store) : BuildRowsInvariant R L es bp specs [].length (specs, store)

theorem Ratpoints.Sieve.BuildRowsPre.post_of_missing_false {R : EntryRef → Nat → Array UInt64} {L : List SieveEntry} {missing : Bool} {es : List SieveEntry} {bp : List Nat} {specs : List SieveSpec} {store : RowStore} (pre : BuildRowsPre R L missing es bp specs store) (h : ¬missing = true) : specs = List.mapIdx (fun (i : Nat) (s : SieveSpec) => { p := s.p, offset := s.offset, row := closedRow es[i]!.admits es[i]!.p bp[i]!, start := s.start, stop := es[i]!.p }) specs ∧ StoreHolds R L (specs, store).snd

theorem Ratpoints.Sieve.BuildRowsInvariant.post {R : EntryRef → Nat → Array UInt64} {L es : List SieveEntry} {bp : List Nat} {specs specs' : List SieveSpec} {st : RowStore} (h : BuildRowsInvariant R L es bp specs (ForIn.toList [:specs.length]).length (specs', st)) : specs' = List.mapIdx (fun (i : Nat) (s : SieveSpec) => { p := s.p, offset := s.offset, row := closedRow es[i]!.admits es[i]!.p bp[i]!, start := s.start, stop := es[i]!.p }) specs ∧ StoreHolds R L ((specs', st).fst, (specs', st).snd).snd

theorem Ratpoints.Sieve.BuildRowsInvariant.fetchRow_pre {R : EntryRef → Nat → Array UInt64} {L : List SieveEntry} {missing : Bool} {es : List SieveEntry} {bp : List Nat} {specs : List SieveSpec} {store : RowStore} (pre : BuildRowsPre R L missing es bp specs store) {pref suff : List Nat} {cur : Nat} (hl : ForIn.toList [:specs.length] = pref ++ cur :: suff) {st : List SieveSpec × RowStore} (h : BuildRowsInvariant R L es bp specs pref.length st) : (∀ (row : Array UInt64), st.snd.row? es[cur]!.ref bp[cur]! = some row → row = closedRow es[cur]!.admits es[cur]!.p bp[cur]!) ∧ (st.snd.row? es[cur]!.ref bp[cur]! = none → InitRowPre es[cur]! bp[cur]! st.snd)

theorem Ratpoints.Sieve.BuildRowsInvariant.set {R : EntryRef → Nat → Array UInt64} {L : List SieveEntry} {missing : Bool} {es : List SieveEntry} {bp : List Nat} {specs : List SieveSpec} {store : RowStore} (pre : BuildRowsPre R L missing es bp specs store) {pref suff : List Nat} {cur : Nat} (hl : ForIn.toList [:specs.length] = pref ++ cur :: suff) {st : List SieveSpec × RowStore} (h : BuildRowsInvariant R L es bp specs pref.length st) {row : Array UInt64} {st' : RowStore} (hr : (row, st').fst = closedRow es[cur]!.admits es[cur]!.p bp[cur]! ∧ ((row, st').snd = st.snd ∨ ∃ (s : RowStore), st.snd.Grows s (FactorRow es[cur]!) ∧ (row, st').snd = s.publish es[cur]!.ref bp[cur]! (closedRow es[cur]!.admits es[cur]!.p bp[cur]!))) : BuildRowsInvariant R L es bp specs (pref ++ [cur]).length (st.fst.set cur (have __src := st.fst[cur]!; { p := __src.p, offset := __src.offset, row := row, start := __src.start, stop := es[cur]!.p }), st')

theorem Ratpoints.Sieve.BuildRowsInvariant.skip {R : EntryRef → Nat → Array UInt64} {L es : List SieveEntry} {bp : List Nat} {specs : List SieveSpec} {pref suff : List Nat} {cur : Nat} (hl : ForIn.toList [:specs.length] = pref ++ cur :: suff) {st : List SieveSpec × RowStore} (h : BuildRowsInvariant R L es bp specs pref.length st) (hne : ¬st.fst[cur]!.row.isEmpty = true) : BuildRowsInvariant R L es bp specs (pref ++ [cur]).length (st.fst, st.snd)

theorem Ratpoints.Sieve.buildRows_spec (R : EntryRef → Nat → Array UInt64) (L : List SieveEntry) (missing : Bool) (es : List SieveEntry) (bp : List Nat) (specs : List SieveSpec) (store : RowStore) : ⦃ BuildRowsPre R L missing es bp specs store ⦄ buildRows missing es bp specs store ⦃ fun (r : List SieveSpec × RowStore) => r.fst = List.mapIdx (fun (i : Nat) (s : SieveSpec) => { p := s.p, offset := s.offset, row := closedRow es[i]!.admits es[i]!.p bp[i]!, start := s.start, stop := es[i]!.p }) specs ∧ StoreHolds R L r.snd ⦄

The rows that Ratpoints.Sieve.buildRows builds into the sieve specs of the entries es at the residues bp, read from the tables of rows or built into them, are the closed forms of the rows of the entries (Ratpoints.Sieve.closedRow), each with the end p, and the store still holds the rows R for every list L of entries that contains es and for which it held them.

theorem Ratpoints.Sieve.length_setRows (store : RowStore) {es : List SieveEntry} {bp : List Nat} (cl : NumClass) (offsets : Array Nat) (hbp : bp.length = es.length) : (setRows store es bp cl offsets).fst.length = es.length

theorem Ratpoints.Sieve.getElem!_setRows (store : RowStore) {es : List SieveEntry} {bp : List Nat} (cl : NumClass) (offsets : Array Nat) (hbp : bp.length = es.length) {n : Nat} (hn : n < es.length) : (setRows store es bp cl offsets).fst[n]! = { p := es[n].p, offset := offsets[cl.offset.getD 0 + n]!, row := (store.row? es[n].ref bp[n]!).getD #[], start := 0, stop := es[n].p }

theorem Ratpoints.Sieve.row?_ne_none_of_setRows {store : RowStore} {es : List SieveEntry} {bp : List Nat} {cl : NumClass} {offsets : Array Nat} (hbp : bp.length = es.length) (h : (setRows store es bp cl offsets).snd = false) {n : Nat} (hn : n < es.length) : store.row? es[n].ref bp[n]! ≠ none

theorem Ratpoints.Sieve.buildRowsPre_setRows {R : EntryRef → Nat → Array UInt64} {L : List SieveEntry} {store : RowStore} {es : List SieveEntry} {bp : List Nat} (cl : NumClass) (offsets : Array Nat) (hs : StoreHolds R L store) (hsub : es ⊆ L) (hfit : ∀ (n : Nat) (h : n < es.length), es[n].RowsFit R n) (hbp : bp.length = es.length) (hlt : ∀ (n : Nat) (h : n < es.length), bp[n]! < es[n].p) : BuildRowsPre R L (setRows store es bp cl offsets).snd es bp (setRows store es bp cl offsets).fst store

What building the rows of the sieve specs that Ratpoints.Sieve.setRows makes needs (Ratpoints.Sieve.BuildRowsPre), for a store that holds the rows R for a list of entries that contains es, entries that fit them at their positions and residues below the moduli: a row present in the store is the closed form of the row of its entry.

theorem Ratpoints.Sieve.mapIdx_setRows (store : RowStore) {es : List SieveEntry} {bp : List Nat} (cl : NumClass) (offsets : Array Nat) (hbp : bp.length = es.length) : List.mapIdx (fun (i : Nat) (s : SieveSpec) => { p := s.p, offset := s.offset, row := closedRow es[i]!.admits es[i]!.p bp[i]!, start := s.start, stop := es[i]!.p }) (setRows store es bp cl offsets).fst = List.mapIdx (fun (n : Nat) (eb : SieveEntry × Nat) => { p := eb.fst.p, offset := offsets[cl.offset.getD 0 + n]!, row := closedRow eb.fst.admits eb.fst.p eb.snd, start := 0, stop := eb.fst.p }) (es.zip bp)

theorem Ratpoints.Sieve.buildRows_setRows_map_spec (R : EntryRef → Nat → Array UInt64) (L : List SieveEntry) (store : RowStore) (es : List SieveEntry) (g : SieveEntry → Nat) (cl : NumClass) (offsets : Array Nat) : ⦃ StoreHolds R L store ∧ es ⊆ L ∧ (∀ (n : Nat) (h : n < es.length), es[n].RowsFit R n) ∧ ∀ (e : SieveEntry), e ∈ es → g e < e.p ⦄ buildRows (setRows store es (List.map g es) cl offsets).snd es (List.map g es) (setRows store es (List.map g es) cl offsets).fst store ⦃ fun (r : List SieveSpec × RowStore) => r.fst = List.mapIdx (fun (n : Nat) (e : SieveEntry) => { p := e.p, offset := offsets[cl.offset.getD 0 + n]!, row := closedRow e.admits e.p (g e), start := 0, stop := e.p }) es ∧ StoreHolds R L r.snd ⦄

The sieve specs of the first two stages that Ratpoints.Sieve.setRows makes and Ratpoints.Sieve.buildRows completes for the residues g e < p of the entries, as the run computes them (Ratpoints.Sieve.fillBpList_eq_map), have the closed forms of the rows of their entries at their residues (Ratpoints.Sieve.closedRow), the offsets of the class, the start 0 and the end p, and the store still holds the rows R for the entries L, for a store that holds them, entries among L that fit them at their positions and residues below the moduli.

The rows of the references of a run

@[simp]

theorem Ratpoints.Sieve.p_run_examinePower (c : List Int) (d p e : Nat) (u pinf : Bool) : (examinePower c d p e u pinf).run.p = p

@[simp]

theorem Ratpoints.Sieve.m_run_examinePower (c : List Int) (d p e : Nat) (u pinf : Bool) : (examinePower c d p e u pinf).run.m = p ^ e

theorem Ratpoints.Sieve.admits_run_examinePower (c : List Int) (d p e : Nat) (u pinf : Bool) : (examinePower c d p e u pinf).run.admits = (examinePower c d p e u false).run.admits

The rows of a prime power do not depend on the flag pinf, which only the density reads.

def Ratpoints.Sieve.runRows (c : List Int) (d : Nat) (es : List SieveEntry) : EntryRef → Nat → Array UInt64

The rows of the references of a run for the polynomial of degree d with the coefficient list c and the sieve entries es of the moduli in their order: for a prime p, the closed forms of the rows of its table (Ratpoints.Sieve.examinePrime); for a prime power p ^ e, those of its tables (Ratpoints.Sieve.examinePower); for a product, those of the entry at its position.

Equations

• Ratpoints.Sieve.runRows c d es (Ratpoints.Sieve.EntryRef.prime p) = Ratpoints.Sieve.closedRow (Ratpoints.Sieve.examinePrime c d p).admits p
• Ratpoints.Sieve.runRows c d es (Ratpoints.Sieve.EntryRef.power p e) = Ratpoints.Sieve.closedRow (Ratpoints.Sieve.examinePower c d p e false false).run.admits (p ^ e)
• Ratpoints.Sieve.runRows c d es (Ratpoints.Sieve.EntryRef.product n) = Ratpoints.Sieve.closedRow es[n]!.admits es[n]!.p

theorem Ratpoints.Sieve.runRows_prime_zero (c : List Int) (d : Nat) (es : List SieveEntry) {p : Nat} (hp : 0 < p) : runRows c d es (EntryRef.prime p) 0 = sieves0 p

theorem Ratpoints.Sieve.runRows_ref (c : List Int) (d : Nat) (es : List SieveEntry) {f : Factor} (hprime : ∀ (t : Entry), f = Factor.prime t → t = examinePrime c d t.p) (hpower : ∀ (pw : Power), f = Factor.power pw → ∃ (pinf : Bool), pw = (examinePower c d pw.p pw.e false pinf).run) : runRows c d es f.ref = closedRow f.admits f.modulus

The rows of the reference of a factor of a run whose table or tables are those that Ratpoints.Sieve.examinePrime and Ratpoints.Sieve.examinePower compute are the closed forms of the rows of the factor.

theorem Ratpoints.Sieve.SieveEntry.rowsFit_runRows {c : List Int} {d : Nat} {es : List SieveEntry} {n : Nat} {e : SieveEntry} (hn : es[n]? = some e) (hrf : e.RefFits n) (hpos : 0 < e.p) (hne : e.factors ≠ []) (hdvd : ∀ (f : Factor), f ∈ e.factors → f.modulus ∣ e.p) (hb : ∀ (f : Factor), f ∈ e.factors → f.Buildable) (hprime : ∀ (t : Entry), Factor.prime t ∈ e.factors → t = examinePrime c d t.p) (hpower : ∀ (pw : Power), Factor.power pw ∈ e.factors → ∃ (pinf : Bool), pw = (examinePower c d pw.p pw.e false pinf).run) : e.RowsFit (runRows c d es) n

A sieve entry at the position n of the entries es of a run, with the reference and the kind that Ratpoints.makeModulus sets, a positive modulus, at least one factor, the moduli of the factors dividing the modulus, builders that have what they need and the tables that Ratpoints.Sieve.examinePrime and Ratpoints.Sieve.examinePower compute, fits the rows of the references of the run (Ratpoints.Sieve.runRows).

The store of a run and its entries

structure Ratpoints.Sieve.RowStore.MadeFor (s : RowStore) (c : List Int) (d : Nat) (es : List SieveEntry) : Prop

The store s as the loop of the tables and the tables of the sieve entries es of the first moduli of a run make it (Ratpoints.choiceEnd): it holds the rows of the references of every run whose entries begin with es (Ratpoints.Sieve.runRows), every table of rows of a prime in it has its row of 0, and so has the table of rows of every prime factor of es.

• holds (es' : List SieveEntry) : es <+: es' → Holds (runRows c d es') s

  The store holds the rows of the references of every run whose entries begin with es.

• primeZeroRows : s.PrimeZeroRows

  Every table of rows of a prime has its row of 0.

• zero (e : SieveEntry) : e ∈ es → ∀ (t : Entry), Factor.prime t ∈ e.factors → s.row? (EntryRef.prime t.p) 0 ≠ none

  The table of rows of every prime factor of es has its row of 0.

theorem Ratpoints.Sieve.RowStore.madeFor_nil {s : RowStore} (c : List Int) (d : Nat) (h : ∀ (R : EntryRef → Nat → Array UInt64), (∀ (p : Nat), 0 < p → R (EntryRef.prime p) 0 = sieves0 p) → Holds R s) (hz : s.PrimeZeroRows) : s.MadeFor c d []

The store of the loop of the tables, which holds the rows of 0 of the primes and no others (Ratpoints.Sieve.PrimeStore), is made for no entries.

theorem Ratpoints.Sieve.RowStore.MadeFor.addTables {s : RowStore} {c : List Int} {d : Nat} {es : List SieveEntry} (h : s.MadeFor c d es) {e : SieveEntry} {n : Nat} (he : e.RefFits n) (hp : ∀ (t : Entry), Factor.prime t ∈ e.factors → 0 < t.p) : (e.addTables s).MadeFor c d (es ++ [e])

The tables of rows of the next sieve entry e, with the reference and the kind of builder of its position and positive primes: the store is made for the entries with e.

theorem Ratpoints.Sieve.RowStore.MadeFor.foldl_addTables {s : RowStore} {c : List Int} {d : Nat} {es : List SieveEntry} (h : s.MadeFor c d es) (l : List SieveEntry) (hfit : ∀ (n : Nat) (hn : n < l.length), l[n].RefFits (es.length + n)) (hp : ∀ (e : SieveEntry), e ∈ l → ∀ (t : Entry), Factor.prime t ∈ e.factors → 0 < t.p) : (List.foldl (fun (s : RowStore) (e : SieveEntry) => e.addTables s) s l).MadeFor c d (es ++ l)

The tables of rows of the sieve entries l added in turn, each with the reference and the kind of builder of its position after es and positive primes: the store is made for es ++ l.

theorem Ratpoints.Sieve.RowStore.MadeFor.storeHolds {s : RowStore} {c : List Int} {d : Nat} {es : List SieveEntry} (h : s.MadeFor c d es) : StoreHolds (runRows c d es) es s

The store made for the entries es of a run holds the rows of the references of the run for them (Ratpoints.Sieve.StoreHolds).

theorem Ratpoints.Sieve.StoreHolds.of_factors {R : EntryRef → Nat → Array UInt64} {es es' : List SieveEntry} {s : RowStore} (h : StoreHolds R es s) (h' : ∀ (e' : SieveEntry), e' ∈ es' → ∃ (e : SieveEntry), e ∈ es ∧ e'.factors = e.factors) : StoreHolds R es' s

The invariant of the store holds for entries with the factors of those for which it holds, such as the entries with the inverses of the strides (Ratpoints.Sieve.classOffsets) and those of the first two stages.

theorem Ratpoints.Sieve.SieveEntry.RowsFit.of_eq {e e' : SieveEntry} {R : EntryRef → Nat → Array UInt64} {n : Nat} (h : e.RowsFit R n) (hp : e'.p = e.p) (hf : e'.factors = e.factors) (hr : e'.ref = e.ref) (hi : e'.init = e.init) : e'.RowsFit R n

An entry with the modulus, the factors, the reference and the kind of builder of an entry that fits the rows R at its position fits them too, such as the entry with the inverses of the strides (Ratpoints.Sieve.classOffsets).

A store that fits the sieve entries

def Ratpoints.Sieve.RowStore.Fits (s : RowStore) (es : List SieveEntry) : Prop

The store s fits the sieve entries es: it holds rows R of the references (Ratpoints.Sieve.StoreHolds) that every entry fits at its position (Ratpoints.Sieve.SieveEntry.RowsFit), which is what building the rows of the entries needs.

Equations

• s.Fits es = ∃ (R : Ratpoints.Sieve.EntryRef → Nat → Array UInt64), Ratpoints.Sieve.StoreHolds R es s ∧ ∀ (n : Nat) (h : n < es.length), es[n].RowsFit R n

theorem Ratpoints.Sieve.pos_of_rowsFit_of_mem {R : EntryRef → Nat → Array UInt64} {L : List SieveEntry} (hfit : ∀ (n : Nat) (h : n < L.length), L[n].RowsFit R n) {e : SieveEntry} (he : e ∈ L) : 0 < e.p

theorem Ratpoints.Sieve.rowsFit_take {R : EntryRef → Nat → Array UInt64} {L : List SieveEntry} (hfit : ∀ (n : Nat) (h : n < L.length), L[n].RowsFit R n) (k n : Nat) (h : n < (List.take k L).length) : (List.take k L)[n].RowsFit R n

theorem Ratpoints.Sieve.RowStore.Fits.pos {s : RowStore} {es : List SieveEntry} (h : s.Fits es) (e : SieveEntry) : e ∈ es → 0 < e.p

theorem Ratpoints.Sieve.RowStore.Fits.take {s : RowStore} {es : List SieveEntry} (h : s.Fits es) (k : Nat) : s.Fits (List.take k es)

The store of the sieve entries of a run fits their first k, those of the first two stages.

theorem Ratpoints.Sieve.RowStore.Fits.map_dinv {s : RowStore} {es : List SieveEntry} (h : s.Fits es) (dinv : SieveEntry → Array Nat) : s.Fits (List.map (fun (e : SieveEntry) => { p := e.p, factors := e.factors, magic := e.magic, bias := e.bias, rbainv := e.rbainv, dinv := dinv e, ref := e.ref, init := e.init, r := e.r, nf := e.nf }) es)

The store of the sieve entries of a run fits them with the inverses of the strides that Ratpoints.Sieve.classOffsets sets.

theorem Ratpoints.Sieve.RowStore.Fits.buildRows_setRows {store store' : RowStore} {es : List SieveEntry} (h : store.Fits es) {g : SieveEntry → Nat} (hg : ∀ (e : SieveEntry), e ∈ es → g e < e.p) {cl : NumClass} {offsets : Array Nat} {specs : List SieveSpec} (hr : (specs, store') = (buildRows (setRows store es (List.map g es) cl offsets).snd es (List.map g es) (setRows store es (List.map g es) cl offsets).fst store).run) : specs = List.mapIdx (fun (n : Nat) (e : SieveEntry) => { p := e.p, offset := offsets[cl.offset.getD 0 + n]!, row := closedRow e.admits e.p (g e), start := 0, stop := e.p }) es ∧ store'.Fits es

The sieve specs of a denominator that Ratpoints.Sieve.setRows makes and Ratpoints.Sieve.buildRows completes for the residues g e < p of the entries, as the run computes them (Ratpoints.Sieve.buildRows_setRows_map_spec): the closed forms of the rows of the entries at their residues, with the offsets of the class, the start 0 and the end p; and the store after them still fits the entries.

theorem Ratpoints.Sieve.StoreHolds.buildRows_setRows_take {R : EntryRef → Nat → Array UInt64} {L : List SieveEntry} {store store' : RowStore} (h : StoreHolds R L store) (hfit : ∀ (n : Nat) (h : n < L.length), L[n].RowsFit R n) {k : Nat} {g : SieveEntry → Nat} (hg : ∀ (e : SieveEntry), e ∈ List.take k L → g e < e.p) {cl : NumClass} {offsets : Array Nat} {specs : List SieveSpec} (hr : (specs, store') = (buildRows (setRows store (List.take k L) (List.map g (List.take k L)) cl offsets).snd (List.take k L) (List.map g (List.take k L)) (setRows store (List.take k L) (List.map g (List.take k L)) cl offsets).fst store).run) : StoreHolds R L store'

The sieve specs of the first k sieve entries of L that Ratpoints.Sieve.setRows makes and Ratpoints.Sieve.buildRows completes for their residues g e < p, from a store that holds the rows R for all of L (Ratpoints.Sieve.StoreHolds), whose entries fit them: the store after them still holds the rows for all of L (Ratpoints.Sieve.buildRows_setRows_map_spec).