The choice of the moduli

The choice of the moduli and the cut points from the curve (Ratpoints.sievingInfo) either exits, when the curve has no points modulo a prime that it examines, or gives what the run needs (Ratpoints.IsSievingInfo): sound sieve entries with the fields that the packing reads and the tables of inverses of their factors, prime entries wherever the count of factors is zero, the reciprocals of the moduli in their order, a first decision whose cut points the run can use (Ratpoints.Sieve.DecisionWF), sound forbidden divisors and a store of the tables of rows that fits every entry, for any values of the doubles of the cost model.

The loop of the tables (Ratpoints.tablesLoop) keeps the tables of the primes looked at at their positions, prime candidates, sound forbidden divisors and the store of the rows of the primes (Ratpoints.TableLoop.WF); the rest of the choice (Ratpoints.choiceTail) offers the composite moduli, runs the stages and ends with one sieve entry for each candidate of the pool, made for its position (Ratpoints.IsChoiceEntries), whose tables of rows the store then fits.

Main definitions

• Ratpoints.Sieve.SieveEntry.IsSound: a sieve entry that lets the numerator of every point through.
• Ratpoints.Sieve.EntriesWF: sieve entries fit for the run, with the reciprocals of their moduli and a store of the tables of rows.
• Ratpoints.IsSievingInfo: what the run needs of the result of the choice.
• Ratpoints.Sieve.PrimeStore: the store of the tables of rows that the loop of the tables makes.
• Ratpoints.TableLoop.WF: the state of the loop of the tables.
• Ratpoints.IsChoiceEntries: the sieve entries of the choice, each made for its position.

Main statements

• Ratpoints.SieveOptions.numPrimes_normalize_le: the normalized options look at most Ratpoints.numPrimes primes.
• Ratpoints.IsModulusEntry.isSound: an entry of a modulus as the choice makes it is sound.
• Ratpoints.tablesLoop_spec: the loop of the tables.
• Ratpoints.isSievingInfo_choiceEnd, Ratpoints.choiceTail_spec: the end of the choice.
• Ratpoints.sievingInfo_spec: the contract of the choice.

structure Ratpoints.Sieve.SieveEntry.IsSound (c : List ℤ) (e : SieveEntry) : Prop

A sieve entry that lets the numerator of every point of the curve y ^ 2 = F(x, z) with the coefficient list c through: its modulus is positive, and its row of the denominator b admits the numerator a of every triple (a, y, b) with gcd(a, b) = 1 and y ^ 2 = F(a, b). The choice of the moduli makes only such entries (Ratpoints.sievingInfo_spec).

• pos : 0 < e.p

  The modulus is positive.

• admits_of_sq_eq {a y : ℤ} {b : ℕ} (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : e.admits b a = true

  The row of the denominator of every point admits its numerator.

structure Ratpoints.Sieve.EntriesWF (c : List ℤ) (entries : List SieveEntry) (magics : Array ℕ) (store : RowStore) : Prop

Sieve entries fit for the run of the search on the curve y ^ 2 = F(x, z) with the coefficient list c: sound (Ratpoints.Sieve.SieveEntry.IsSound), each with no factors counted a prime entry of the table (Ratpoints.Sieve.SieveEntry.IsPrimeEntry), as the third stage needs, with the tables of inverses of their factors (Ratpoints.Sieve.SieveEntry.HasInverses), the reciprocals magics of their moduli in their order, and a store of the tables of rows that fits them all (Ratpoints.Sieve.RowStore.Fits).

• isSound (e : SieveEntry) : e ∈ entries → SieveEntry.IsSound c e

  The sieve entries are sound.

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

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

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

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

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

  The factors of the sieve entries have their tables of inverses.

• fits : store.Fits entries

  The store of the tables of rows fits all the entries.

theorem Ratpoints.Sieve.EntriesWF.map_dinv {c : List ℤ} {entries : List SieveEntry} {magics : Array ℕ} {store : RowStore} (h : EntriesWF c entries magics store) (dinv : SieveEntry → Array ℕ) : EntriesWF c (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 }) entries) magics store

Sieve entries fit for the run stay so when the inverses of the strides that each records change.

theorem Ratpoints.IsModulusEntry.isSound {c : List ℤ} {m : ℕ} {s : Sieve.SieveEntry} (h : IsModulusEntry c m s) : Sieve.SieveEntry.IsSound c s

A sieve entry of a modulus as the choice makes it is sound.

structure Ratpoints.IsSievingInfo (c : List ℤ) (bHigh : ℕ) (si : SievingInfo) extends Ratpoints.Sieve.EntriesWF c si.entries si.magics si.store : Prop

What the run needs of the result si of the choice of the moduli for the curve y ^ 2 = F(x, z) with the coefficient list c and the largest denominator bHigh: sieve entries fit for the run with the reciprocals of their moduli and the store of the tables of rows, the reserve included (Ratpoints.Sieve.EntriesWF), with the fields that the packing reads (Ratpoints.Sieve.SieveEntry.Packable); the first decision, from the block 0 on, with the cut points of the parameters, well-formed for the entries (Ratpoints.Sieve.DecisionWF); the forbidden divisors among those that the loops of the tables and of the further primes may record (Ratpoints.Sieve.IsForbiddenEntry, Ratpoints.Sieve.IsForbiddenVal); and the test of the denominators only for even degree.

• isSound (e : SieveEntry) : e ∈ si.entries → SieveEntry.IsSound c e
• isPrimeEntry_of_nf (e : SieveEntry) : e ∈ si.entries → e.nf = 0 → e.IsPrimeEntry
• magics_eq : si.magics.toList = List.map (fun (e : SieveEntry) => magic e.p) si.entries
• hasInverses (e : SieveEntry) : e ∈ si.entries → e.HasInverses
• fits : si.store.Fits si.entries
• packable (e : Sieve.SieveEntry) : e ∈ si.entries → e.Packable

  The sieve entries have the fields that the packing reads.

• decisionWF : Sieve.DecisionWF si.entries si.params.sp1 { block := 0, sp2 := si.params.sp2, sp3 := si.params.sp3 }

  The first decision is well-formed.

• isForbiddenEntry (e : Sieve.ForbiddenEntry) : e ∈ si.forb → Sieve.IsForbiddenEntry c (degree c) bHigh e

  The forbidden divisors tested with words are sound.

• isForbiddenVal (e : Sieve.ForbiddenVal) : e ∈ si.forbVal → Sieve.IsForbiddenVal c (degree c) bHigh e

  The forbidden divisors tested by their valuations are sound.

• degree_mod_two_eq_zero_of_checkDenom : si.checkDenom = true → degree c % 2 = 0

  The denominators are tested only for even degree.

theorem Ratpoints.SieveOptions.numPrimes_normalize_le (s : SieveOptions) : s.normalize.numPrimes ≤ ↑Ratpoints.numPrimes

The normalized options look at most Ratpoints.numPrimes primes.

The loop of the tables

def Ratpoints.Sieve.PrimeStore (store : RowStore) : Prop

The store of the tables of rows that the loop of the tables makes holds every function R of the references and the residues (Ratpoints.Sieve.RowStore.Holds) whose rows of 0 of the primes are the patterns sieves0 (Ratpoints.Sieve.sieves0), since it holds only these rows, and every table of rows of a prime in it has its row of 0 (Ratpoints.Sieve.RowStore.PrimeZeroRows).

Equations

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

theorem Ratpoints.Sieve.primeStore_empty : PrimeStore ∅

theorem Ratpoints.Sieve.PrimeStore.insertIfNew {store : RowStore} (h : PrimeStore store) {p : ℕ} (hp : 0 < p) : PrimeStore (Std.HashMap.insertIfNew store (EntryRef.prime p) (primeRows p))

structure Ratpoints.TableLoop.WF (c : List ℤ) (bHigh : ℕ) (st : TableLoop) : Prop

The state of the loop of the tables (Ratpoints.TableLoop) for the curve with the coefficient list c and the largest denominator bHigh: at most Ratpoints.numPrimes primes to look at, the tables of the primes those of Ratpoints.Sieve.examinePrime at their positions (Ratpoints.IsExaminedPrimeSe), prime candidates (Ratpoints.ModulusCandidate.IsPrime), sound forbidden divisors and the store of the tables of rows of the primes (Ratpoints.Sieve.PrimeStore).

• pnLim_le : st.pnLim ≤ numPrimes

  At most Ratpoints.numPrimes primes to look at.

• primeSe : IsExaminedPrimeSe c st.primeSe

  The tables of the primes at their positions.

• isPrime (e : ModulusCandidate) : e ∈ st.pool → ModulusCandidate.IsPrime c e

  Prime candidates.

• ba (e : Sieve.ForbiddenEntry) : e ∈ st.ba → Sieve.IsForbiddenEntry c (degree c) bHigh e

  Sound forbidden divisors tested with words.

• val (e : Sieve.ForbiddenVal) : e ∈ st.val → Sieve.IsForbiddenVal c (degree c) bHigh e

  Sound forbidden divisors tested by their valuations.

• store : Sieve.PrimeStore st.store

  The store of the tables of rows of the primes.

theorem Ratpoints.IsExaminedPrimeSe.push_none {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} (h : IsExaminedPrimeSe c primeSe) : IsExaminedPrimeSe c (primeSe.push none)

theorem Ratpoints.IsExaminedPrimeSe.set!_push_none {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} (h : IsExaminedPrimeSe c primeSe) {pn : ℕ} (hpn : pn < numPrimes) (hs : primeSe.size = pn) (r : Float) : IsExaminedPrimeSe c ((primeSe.push none).set! pn (some (Sieve.examinePrime c (degree c) primeTable[pn]!, r)))

theorem Ratpoints.TableLoop.WF.push_ba_of_run {c : List ℤ} {bHigh : ℕ} {st : TableLoop} (h : WF c bHigh st) {pn : ℕ} (hpn : pn < numPrimes) {u : Bool} {t : Sieve.Entry} {cm : Array ℕ} {code : ℕ} {r : Float} (he : (Sieve.examinePrime? c (degree c) primeTable[pn]! u).run = some (t, cm, code, r)) {f : Sieve.ForbiddenEntry} (hf : (Sieve.forbiddenOfPrime c (degree c) primeTable[pn]! bHigh cm t.isFSquare[primeTable[pn]!]!).run = some (Sum.inl f)) : WF c bHigh { pool := st.pool, pnLim := st.pnLim, nWeak := st.nWeak, primeSe := st.primeSe, pinf := st.pinf, ba := st.ba.push f, val := st.val, store := st.store }

A forbidden divisor tested with words that the prime at the position pn < numPrimes gives from what its table hands back, recorded.

theorem Ratpoints.TableLoop.WF.push_val_of_run {c : List ℤ} {bHigh : ℕ} {st : TableLoop} (h : WF c bHigh st) {pn : ℕ} (hpn : pn < numPrimes) {u : Bool} {t : Sieve.Entry} {cm : Array ℕ} {code : ℕ} {r : Float} (he : (Sieve.examinePrime? c (degree c) primeTable[pn]! u).run = some (t, cm, code, r)) {f : Sieve.ForbiddenVal} (hf : (Sieve.forbiddenOfPrime c (degree c) primeTable[pn]! bHigh cm t.isFSquare[primeTable[pn]!]!).run = some (Sum.inr f)) : WF c bHigh { pool := st.pool, pnLim := st.pnLim, nWeak := st.nWeak, primeSe := st.primeSe, pinf := st.pinf, ba := st.ba, val := st.val.push f, store := st.store }

A forbidden divisor tested by its valuation that the prime at the position pn < numPrimes gives from what its table hands back, recorded.

theorem Ratpoints.TableLoop.WF.push_ofPrime {c : List ℤ} {bHigh : ℕ} {st : TableLoop} (h : WF c bHigh st) {pn : ℕ} (hs : st.primeSe.size = pn) (hpn : pn < numPrimes) {u : Bool} {t : Sieve.Entry} {cm : Array ℕ} {code : ℕ} {r : Float} (he : (Sieve.examinePrime? c (degree c) primeTable[pn]! u).run = some (t, cm, code, r)) (ct U D cc : Float) (atInf : Bool) (nWeak : ℕ) : WF c bHigh { pool := st.pool.push (phase1Key ct U D cc (ModulusCandidate.ofPrime pn t r code)), pnLim := st.pnLim, nWeak := nWeak, primeSe := (st.primeSe.push none).set! pn (some (t, r)), pinf := st.pinf.push atInf, ba := st.ba, val := st.val, store := Std.HashMap.insertIfNew st.store (Sieve.EntryRef.prime primeTable[pn]!) (Sieve.primeRows primeTable[pn]!) }

The state of the loop of the tables after the prime at the position pn = st.primeSe.size, which says something, with its candidate, its table and its table of rows.

theorem Ratpoints.TableLoop.WF.push_none {c : List ℤ} {bHigh : ℕ} {st : TableLoop} (h : WF c bHigh st) (atInf : Bool) : WF c bHigh { pool := st.pool, pnLim := st.pnLim, nWeak := st.nWeak, primeSe := st.primeSe.push none, pinf := st.pinf.push atInf, ba := st.ba, val := st.val, store := st.store }

The state of the loop of the tables after the prime at the position pn, which says nothing.

theorem Ratpoints.examineInLoop_spec (c : List ℤ) (u checkDenom : Bool) (maxForbidden bHigh : ℕ) (ct : Float) (est : RunEstimate) (cc : Float) (pn : ℕ) (st : TableLoop) : ⦃ TableLoop.WF c bHigh st ∧ st.primeSe.size = pn ∧ pn < numPrimes ⦄ examineInLoop c (degree c) u checkDenom maxForbidden bHigh ct est cc pn st ⦃ fun (r : Option TableLoop) => (r = none → ∀ (H : ℕ) (q : ℤ × ℤ × ℤ), ¬IsPoint c H q) ∧ ∀ (st' : TableLoop), r = some st' → TableLoop.WF c bHigh st' ∧ st'.primeSe.size = pn + 1 ∧ st'.pnLim = st.pnLim ⦄

The contract of Ratpoints.examineInLoop at the position pn = st.primeSe.size below Ratpoints.numPrimes: at none the curve has no points; otherwise the state of the loop of the tables stays one (Ratpoints.TableLoop.WF), with the table of the prime at its position.

theorem Ratpoints.raiseLimit_spec (c : List ℤ) (bHigh : ℕ) (s : SieveOptions) (bpws target : Float) (sp2e : ℕ) (st : TableLoop) : ⦃ TableLoop.WF c bHigh st ∧ st.pnLim < numPrimes ⦄ raiseLimit s bpws target sp2e st ⦃ fun (st' : TableLoop) => TableLoop.WF c bHigh st' ∧ st'.primeSe = st.primeSe ⦄

The contract of Ratpoints.raiseLimit while fewer than Ratpoints.numPrimes primes are to be looked at: the state of the loop of the tables stays one, with its tables.

theorem Ratpoints.TableLoop.wf_init (c : List ℤ) (bHigh : ℕ) {s : SieveOptions} (hs : s.numPrimes ≤ ↑numPrimes) : WF c bHigh { pnLim := s.numPrimes.toNat }

The state of the loop of the tables at its start, for the number of primes to look at of options that look at most Ratpoints.numPrimes primes.

def Ratpoints.TablesLoopInvariant (c : List ℤ) (bHigh : ℕ) : Std.WP.Invariant ℕ (Option (Except ℕ TableLoop) × TableLoop) Prop

The invariant of the loop of Ratpoints.tablesLoop over the positions of the table, whose state is the value of a return and the state of the loop: the state of the loop (Ratpoints.TableLoop.WF), with the tables of the positions looked at while the loop goes on; the value of a return an exit, at which the curve has no points.

Equations

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

theorem Ratpoints.tablesLoop_spec (c : List ℤ) (u checkDenom mayExtend : Bool) (s : SieveOptions) (bHigh : ℕ) (target ct : Float) (est : RunEstimate) (cc bpws : Float) (sp2e : ℕ) : ⦃ s.numPrimes ≤ ↑numPrimes ⦄ tablesLoop c (degree c) u checkDenom mayExtend s bHigh target ct est cc bpws sp2e ⦃ fun (r : Except ℕ TableLoop) => (∀ (p : ℕ), r = Except.error p → ∀ (H : ℕ) (q : ℤ × ℤ × ℤ), ¬IsPoint c H q) ∧ ∀ (st : TableLoop), r = Except.ok st → TableLoop.WF c bHigh st ⦄

The contract of Ratpoints.tablesLoop, for options that look at most Ratpoints.numPrimes primes and any values of the doubles: at an exit the curve has no points; otherwise the state of the loop is one (Ratpoints.TableLoop.WF).

The end of the choice

theorem Ratpoints.ChoicePoolWF.sortFrom {c : List ℤ} {sp2 : ℕ} {pool : Array ModulusCandidate} (h : ChoicePoolWF c sp2 pool) (hs : sp2 ≤ pool.size) (le : ModulusCandidate → ModulusCandidate → Bool) : ChoicePoolWF c sp2 (Ratpoints.sortFrom pool sp2 le)

theorem Ratpoints.ChoicePoolWF.exists_isChoiceEntry {c : List ℤ} {sp2 : ℕ} {pool : Array ModulusCandidate} (h : ChoicePoolWF c sp2 pool) (n : ℕ) (hn : n < pool.size) : ∃ (se : Sieve.SieveEntry), pool[n].ssp = some se ∧ IsChoiceEntry c n se ∧ (sp2 ≤ n → se.nf = 0)

Every candidate of the pool after the stages has its sieve entry, made for its position.

def Ratpoints.IsChoiceEntries (c : List ℤ) (sp2 : ℕ) (es : List Sieve.SieveEntry) : Prop

The sieve entries es of the choice, each made for its position (Ratpoints.IsChoiceEntry), those from the end sp2 of the second stage on with no factors counted.

Equations

• Ratpoints.IsChoiceEntries c sp2 es = ∀ (n : ℕ) (hn : n < es.length), Ratpoints.IsChoiceEntry c n es[n] ∧ (sp2 ≤ n → es[n].nf = 0)

theorem Ratpoints.IsChoiceEntries.exists_isChoiceEntry_of_mem {c : List ℤ} {sp2 : ℕ} {es : List Sieve.SieveEntry} (h : IsChoiceEntries c sp2 es) {e : Sieve.SieveEntry} (he : e ∈ es) : ∃ (n : ℕ), IsChoiceEntry c n e

theorem Ratpoints.IsChoiceEntries.isModulusEntry_of_mem {c : List ℤ} {sp2 : ℕ} {es : List Sieve.SieveEntry} (h : IsChoiceEntries c sp2 es) {e : Sieve.SieveEntry} (he : e ∈ es) : IsModulusEntry c e.p e

theorem Ratpoints.IsChoiceEntries.fits_foldl_addTables {c : List ℤ} {sp2 : ℕ} {es : List Sieve.SieveEntry} (h : IsChoiceEntries c sp2 es) {store : Sieve.RowStore} (hs : Sieve.PrimeStore store) : (List.foldl (fun (s : Sieve.RowStore) (e : Sieve.SieveEntry) => e.addTables s) store es).Fits es

The store of the loop of the tables with the tables of rows of the sieve entries of the choice fits them.

theorem Ratpoints.isChoiceEntries_choiceEnd {c : List ℤ} {sp2 : ℕ} {t : ThirdState} (ht : ThirdState.WF c sp2 t) (store : Sieve.RowStore) : IsChoiceEntries c sp2 (choiceEnd t sp2 store).1 ∧ (choiceEnd t sp2 store).1.length = t.pool.size

The sieve entries at the end of the choice, after the third stage that ends at t.sp3: one for each candidate of the pool, each made for its position (Ratpoints.IsChoiceEntries).

theorem Ratpoints.IsChoiceEntries.nf_eq_zero_of_mem_drop {c : List ℤ} {sp2 : ℕ} {es : List Sieve.SieveEntry} (h : IsChoiceEntries c sp2 es) {e : Sieve.SieveEntry} (he : e ∈ List.drop sp2 es) : e.nf = 0

theorem Ratpoints.isSievingInfo_choiceEnd {c : List ℤ} {bHigh sp1 sp2 : ℕ} {t : ThirdState} (ht : ThirdState.WF c sp2 t) (h12 : sp1 ≤ sp2) {store : Sieve.RowStore} (hs : Sieve.PrimeStore store) {forb : List Sieve.ForbiddenEntry} {forbVal : List Sieve.ForbiddenVal} (hforb : ∀ e ∈ forb, Sieve.IsForbiddenEntry c (degree c) bHigh e) (hval : ∀ e ∈ forbVal, Sieve.IsForbiddenVal c (degree c) bHigh e) {checkDenom : Bool} (hcd : checkDenom = true → degree c % 2 = 0) {P : Params} (h1 : P.sp1 = sp1) (h2 : P.sp2 = sp2) (h3 : P.sp3 = t.sp3) : IsSievingInfo c bHigh { params := P, entries := (choiceEnd t sp2 store).1, magics := (choiceEnd t sp2 store).2.1, forb := forb, forbVal := forbVal, store := (choiceEnd t sp2 store).2.2, checkDenom := checkDenom }

The result of the choice after its third stage (Ratpoints.choiceEnd), with the cut points of the stages, sound forbidden divisors, the store of the loop of the tables and the test of the denominators only for even degree: what the run needs (Ratpoints.IsSievingInfo).

theorem Ratpoints.thirdOf_spec (c : List ℤ) (u mayExtend : Bool) (s : SieveOptions) (checkRel : Float) (est : RunEstimate) (bpw : Float) (pool : Array ModulusCandidate) (sp2 pnLim : ℕ) : ⦃ ChoicePoolWF c sp2 pool ∧ sp2 ≤ pool.size ⦄ thirdOf c (degree c) u mayExtend s checkRel est bpw pool sp2 pnLim ⦃ fun (r : Except ℕ ThirdState) => (∀ (p : ℕ), r = Except.error p → ∀ (H : ℕ) (q : ℤ × ℤ × ℤ), ¬IsPoint c H q) ∧ ∀ (t : ThirdState), r = Except.ok t → ThirdState.WF c sp2 t ⦄

The contract of Ratpoints.thirdOf: Ratpoints.thirdStage_spec from the end sp2 of the second stage.

theorem Ratpoints.firstStages_post {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws : Array Sieve.Power} {pool₀ : Array ModulusCandidate} (h : ∀ e ∈ pool₀, ModulusCandidate.IsPrimeOrComposite c primeSe pws e) {s : SieveOptions} {target ct : Float} {est : RunEstimate} {bpws : Float} {sp2e : ℕ} {pool : Array ModulusCandidate} {sp1 sp2 : ℕ} (he : (pool, sp1, sp2) = (firstStages (sortFrom pool₀ 0 ModulusCandidate.keyLe) s target ct est bpws sp2e).run) : (∀ e ∈ pool, ModulusCandidate.IsPrimeOrComposite c primeSe pws e) ∧ NfEqZeroFrom pool sp2 ∧ sp1 ≤ sp2 ∧ sp2 ≤ pool.size

Ratpoints.firstStages_run for the candidates of the pool after the composite moduli, sorted by their keys.

theorem Ratpoints.ModulusCandidate.isPrimeOrComposite_of_mem_map_phase1Key {c : List ℤ} {pool : Array ModulusCandidate} (h : ∀ e ∈ pool, IsPrime c e) {ct U D cc : Float} {e : ModulusCandidate} (he : e ∈ Array.map (phase1Key ct U D cc) pool) (primeSe : Array (Option (Sieve.Entry × Float))) (pws : Array Sieve.Power) : IsPrimeOrComposite c primeSe pws e

The candidates of the primes, keyed for the first stage, are candidates of the pool before the stages.

theorem Ratpoints.choiceTail_spec (c : List ℤ) (u mayExtend : Bool) (s : SieveOptions) (a : ShapeArgs) (bpw checkRel : Float) (checkDenom : Bool) (forb : List Sieve.ForbiddenEntry) (forbVal : List Sieve.ForbiddenVal) (st : TableLoop) : ⦃ TableLoop.WF c a.bHigh st ∧ (∀ e ∈ forb, Sieve.IsForbiddenEntry c (degree c) a.bHigh e) ∧ (∀ e ∈ forbVal, Sieve.IsForbiddenVal c (degree c) a.bHigh e) ∧ (checkDenom = true → degree c % 2 = 0) ⦄ choiceTail c (degree c) u mayExtend s a bpw checkRel checkDenom forb forbVal st ⦃ fun (r : Except ℕ SievingInfo) => (∀ (p : ℕ), r = Except.error p → ∀ (H : ℕ) (q : ℤ × ℤ × ℤ), ¬IsPoint c H q) ∧ ∀ (si : SievingInfo), r = Except.ok si → IsSievingInfo c a.bHigh si ⦄

The contract of Ratpoints.choiceTail, after the loop of the tables, with sound forbidden divisors and the test of the denominators only for even degree: at an exit of the third stage the curve has no points; otherwise the result is what the run needs (Ratpoints.IsSievingInfo).

theorem Ratpoints.sievingInfo_spec (c : List ℤ) (u checkDenom mayExtend : Bool) (s : SieveOptions) (a : ShapeArgs) (bpw : Float) : ⦃ s.numPrimes ≤ ↑numPrimes ∧ (checkDenom = true → degree c % 2 = 0) ⦄ sievingInfo c (degree c) u checkDenom mayExtend s a bpw ⦃ fun (r : Except ℕ SievingInfo) => (∀ (p : ℕ), r = Except.error p → ∀ (H : ℕ) (q : ℤ × ℤ × ℤ), ¬IsPoint c H q) ∧ ∀ (si : SievingInfo), r = Except.ok si → IsSievingInfo c a.bHigh si ⦄

The contract of the choice of the moduli and the cut points from the curve, for options that look at most Ratpoints.numPrimes primes (normalized options, Ratpoints.SieveOptions.numPrimes_normalize_le), the test of the denominators only for even degree and any values of the doubles: at an exit, at a prime of the loop of the tables or of the third stage without points modulo it, the curve has no points; otherwise the result is what the run needs (Ratpoints.IsSievingInfo).