The pool of the candidate moduli

The contracts of the stages of the choice of the moduli on the pool of the candidates (Ratpoints.ModulusCandidate), for every property of the candidates that the stages keep: the stages drop candidates (Ratpoints.dropUsed, Ratpoints.takeEntries, Ratpoints.dropComposites), sort them (Ratpoints.sortFrom) and key them again (Ratpoints.rankSecond), and leave the cut points within the pool, with only primes that say more than coprimality from the end of the second stage on (Ratpoints.NfEqZeroFrom); for any values of the doubles of the cost model, which no contract reads.

Main definitions

• Ratpoints.NfEqZeroFrom: the candidates from a position on count no factors.

Main statements

• Ratpoints.takeEntries_spec, Ratpoints.dropComposites_spec, Ratpoints.bestByR_spec: the contracts of the loops on the pool.
• Ratpoints.firstStages_spec, Ratpoints.firstStages_run: the first two stages.
• Ratpoints.mem_of_mem_sortFrom, Ratpoints.forall_mem_mapIdx_key, Ratpoints.forall_mem_rankSecond: the sort keeps the candidates, and keying again keeps every property of them that reads no key.

The pool

def Ratpoints.DropUsedInvariant (Q : ModulusCandidate → Prop) (start : Nat) : Std.WP.WhileInvariant (Array ModulusCandidate × Nat) Prop

The invariant of the loop of Ratpoints.dropUsed.

Equations

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

theorem Ratpoints.dropUsed_spec (Q : ModulusCandidate → Prop) (pool : Array ModulusCandidate) (start : Nat) (used : UInt64) : ⦃ (∀ (e : ModulusCandidate), e ∈ pool → Q e) ∧ start ≤ pool.size ⦄ dropUsed pool start used ⦃ fun (r : Array ModulusCandidate) => (∀ (e : ModulusCandidate), e ∈ r → Q e) ∧ start ≤ r.size ⦄

The contract of Ratpoints.dropUsed: it keeps a property Q of the candidates and the position start within the pool, since it only drops candidates from start on.

def Ratpoints.TakeEntriesInvariant (Q : ModulusCandidate → Prop) (start : Nat) : Std.WP.WhileInvariant (Array ModulusCandidate × UInt64 × Float × Nat × Nat) Prop

The invariant of the loop of Ratpoints.takeEntries.

Equations

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

theorem Ratpoints.takeEntries_spec (Q : ModulusCandidate → Prop) (pool : Array ModulusCandidate) (start : Nat) (used : UInt64) (want : Int) (rate bpw target : Float) (extra : Nat) : ⦃ (∀ (e : ModulusCandidate), e ∈ pool → Q e) ∧ start ≤ pool.size ⦄ takeEntries pool start used want rate bpw target extra ⦃ fun (r : Array ModulusCandidate × UInt64 × Float × Nat) => (∀ (e : ModulusCandidate), e ∈ r.fst → Q e) ∧ start + r.snd.snd.snd ≤ r.fst.size ⦄

The contract of Ratpoints.takeEntries, for any values of the doubles and any rule of the first stage: it keeps a property Q of the candidates, since it only drops candidates, and the candidates taken from start on lie within the pool.

def Ratpoints.NfEqZeroFrom (pool : Array ModulusCandidate) (s : Nat) : Prop

The candidates of the pool pool from the position s on have no factors counted: primes that say more than coprimality.

Equations

• Ratpoints.NfEqZeroFrom pool s = ∀ (i : Nat) (h : i < pool.size), s ≤ i → pool[i].nf = 0

def Ratpoints.DropCompositesInvariant (Q : ModulusCandidate → Prop) (start : Nat) : Std.WP.WhileInvariant (Array ModulusCandidate × Nat) Prop

The invariant of the loop of Ratpoints.dropComposites.

Equations

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

theorem Ratpoints.dropComposites_spec (Q : ModulusCandidate → Prop) (pool : Array ModulusCandidate) (start : Nat) : ⦃ (∀ (e : ModulusCandidate), e ∈ pool → Q e) ∧ start ≤ pool.size ⦄ dropComposites pool start ⦃ fun (r : Array ModulusCandidate) => (∀ (e : ModulusCandidate), e ∈ r → Q e) ∧ start ≤ r.size ∧ NfEqZeroFrom r start ⦄

The contract of Ratpoints.dropComposites: it keeps a property Q of the candidates and the position start within the pool, and the candidates from start on count no factors (Ratpoints.NfEqZeroFrom).

theorem Ratpoints.bestByR_spec (pool : Array ModulusCandidate) (sp3 : Nat) : ⦃ True ⦄ bestByR pool sp3 ⦃ fun (r : Option Nat) => ∀ (b : Nat), r = some b → sp3 ≤ b ∧ b < pool.size ⦄

The contract of Ratpoints.bestByR: the position it returns is that of a candidate from sp3 on.

theorem Ratpoints.mem_of_mem_sortFrom {pool : Array ModulusCandidate} {s : Nat} {le : ModulusCandidate → ModulusCandidate → Bool} {e : ModulusCandidate} (he : e ∈ sortFrom pool s le) : e ∈ pool

theorem Ratpoints.size_sortFrom {pool : Array ModulusCandidate} {s : Nat} (hs : s ≤ pool.size) (le : ModulusCandidate → ModulusCandidate → Bool) : (sortFrom pool s le).size = pool.size

theorem Ratpoints.forall_mem_mapIdx_key {Q : ModulusCandidate → Prop} (hQ : ∀ (e : ModulusCandidate), Q e → ∀ (k : Float), Q { r := e.r, key := k, cost := e.cost, p := e.p, mask := e.mask, ssp := e.ssp, nf := e.nf, fac := e.fac }) {pool : Array ModulusCandidate} (h : ∀ (e : ModulusCandidate), e ∈ pool → Q e) (key : Nat → ModulusCandidate → Float) (s : Nat) (e : ModulusCandidate) : e ∈ Array.mapIdx (fun (n : Nat) (e : ModulusCandidate) => if s ≤ n then { r := e.r, key := key n e, cost := e.cost, p := e.p, mask := e.mask, ssp := e.ssp, nf := e.nf, fac := e.fac } else e) pool → Q e

theorem Ratpoints.forall_mem_rankSecond {Q : ModulusCandidate → Prop} (hQ : ∀ (e : ModulusCandidate), Q e → ∀ (k : Float), Q { r := e.r, key := k, cost := e.cost, p := e.p, mask := e.mask, ssp := e.ssp, nf := e.nf, fac := e.fac }) {pool : Array ModulusCandidate} (h : ∀ (e : ModulusCandidate), e ∈ pool → Q e) (sp1 : Nat) (rate bpws ct U D : Float) (e : ModulusCandidate) : e ∈ (rankSecond pool sp1 rate bpws ct U D).fst → Q e

theorem Ratpoints.size_rankSecond (pool : Array ModulusCandidate) (sp1 : Nat) (rate bpws ct U D : Float) : (rankSecond pool sp1 rate bpws ct U D).fst.size = pool.size

theorem Ratpoints.firstStages_spec (Q : ModulusCandidate → Prop) (hQ : ∀ (e : ModulusCandidate), Q e → ∀ (k : Float), Q { r := e.r, key := k, cost := e.cost, p := e.p, mask := e.mask, ssp := e.ssp, nf := e.nf, fac := e.fac }) (pool : Array ModulusCandidate) (s : SieveOptions) (target ct : Float) (est : RunEstimate) (bpws : Float) (sp2e : Nat) : ⦃ ∀ (e : ModulusCandidate), e ∈ pool → Q e ⦄ firstStages pool s target ct est bpws sp2e ⦃ fun (r : Array ModulusCandidate × Nat × Nat) => (∀ (e : ModulusCandidate), e ∈ r.fst → Q e) ∧ NfEqZeroFrom r.fst r.snd.snd ∧ r.snd.fst ≤ r.snd.snd ∧ r.snd.snd ≤ r.fst.size ⦄

The first two stages keep the property Q of the candidates, which reads no key, and leave the cut points sp1 ≤ sp2 within the pool, with only primes that say more than coprimality from sp2 on.

theorem Ratpoints.getElem_sortFrom_of_lt {pool : Array ModulusCandidate} {s : Nat} (hs : s ≤ pool.size) (le : ModulusCandidate → ModulusCandidate → Bool) {n : Nat} (hn : n < s) : (sortFrom pool s le)[n] = pool[n]

theorem Ratpoints.exists_getElem_sortFrom_eq {pool : Array ModulusCandidate} {s : Nat} (le : ModulusCandidate → ModulusCandidate → Bool) {n : Nat} (hsn : s ≤ n) (hn : n < (sortFrom pool s le).size) : ∃ (k : Nat), ∃ (hk : k < pool.size), s ≤ k ∧ (sortFrom pool s le)[n] = pool[k]

theorem Ratpoints.firstStages_run {Q : ModulusCandidate → Prop} (hQ : ∀ (e : ModulusCandidate), Q e → ∀ (k : Float), Q { r := e.r, key := k, cost := e.cost, p := e.p, mask := e.mask, ssp := e.ssp, nf := e.nf, fac := e.fac }) {pool : Array ModulusCandidate} (h : ∀ (e : ModulusCandidate), e ∈ pool → Q e) {s : SieveOptions} {target ct : Float} {est : RunEstimate} {bpws : Float} {sp2e : Nat} {pool' : Array ModulusCandidate} {sp1 sp2 : Nat} (he : (pool', sp1, sp2) = (firstStages pool s target ct est bpws sp2e).run) : (∀ (e : ModulusCandidate), e ∈ pool' → Q e) ∧ NfEqZeroFrom pool' sp2 ∧ sp1 ≤ sp2 ∧ sp2 ≤ pool'.size

Ratpoints.firstStages_spec for a result (pool', sp1, sp2) of the first two stages.

theorem Ratpoints.length_filterMap_ssp_and_forall {pool : Array ModulusCandidate} {P : Nat → Sieve.SieveEntry → Prop} (h : ∀ (n : Nat) (hn : n < pool.size), ∃ (se : Sieve.SieveEntry), pool[n].ssp = some se ∧ P n se) : (List.filterMap (fun (x : ModulusCandidate) => x.ssp) pool.toList).length = pool.size ∧ ∀ (n : Nat) (hn : n < (List.filterMap (fun (x : ModulusCandidate) => x.ssp) pool.toList).length), P n (List.filterMap (fun (x : ModulusCandidate) => x.ssp) pool.toList)[n]

The sieve entries of an array of candidates each with its sieve entry ((·.ssp)) with a property at its position: one for each candidate, each with the property at its position.