The contracts of the stages of the sieve

The test for common factors on the 64-bit words of the C code (Ratpoints.Sieve.relprime) decides whether a numerator is prime to the denominator, and none of its operations leaves the range of a long. For a numerator a prime to the denominator b with |a| ≤ H, the third stage (Ratpoints.Sieve.stage3) with the sieve entries of primes 1 < p ≤ 2 ^ 32 with their tables and reciprocals (Ratpoints.Sieve.SieveEntry.IsPrimeEntry) is the test of the rows of these entries: it reads the table of each prime at a b⁻¹ mod p, in both branches of the bias, and a prime that divides b admits every numerator prime to b; the values that the C code holds in longs stay in range. The exact check (Ratpoints.Sieve.checkPoint) and the points at infinity (Ratpoints.Sieve.pointsAtInfinity), on a delivery whose flag of the stop is clear, are the reference of the delivery (Ratpoints.Delivery.deliver) of the lists of the points they deliver for the flags of the search: the points of the check of the reference, without the point with y < 0 under RATPOINTS_NO_Y, or the one survivor with y = 0 under RATPOINTS_NO_CHECK, mapped back after a reversal. So the test of a candidate (Ratpoints.Sieve.accepted), for |a| < 2 ^ 63 and 0 < b < 2 ^ 63, followed by the exact check, delivers the points of the check with the flags (Ratpoints.Sieve.checkNumWith), which is the check of the reference (Ratpoints.Sieve.checkNum) with the flags of the output clear, for the numerators that survive these entries. The second stage on a bit array (Ratpoints.Sieve.secondStage), or on one of its words (Ratpoints.Sieve.secondStageWord), with moduli in the range of the packing and their reciprocals and the test small of the piece, gives its words and-ed with the rows of all its moduli at their offsets (Ratpoints.Sieve.andWords), although it stops when the bit array or the word is zero. The contracts of the loops are @[spec] theorems proved with vcgen, the program logic of Lean core, with loop invariants that are named definitions.

Main definitions

• Ratpoints.Sieve.RelprimeOddInvariant: the invariant of the loop of the binary algorithm.
• Ratpoints.Sieve.CheckSpec.admits, Ratpoints.Sieve.Stage3Invariant: whether the third stage lets a numerator through one of its primes, and the invariant of its loop.
• Ratpoints.Sieve.SieveEntry.IsPrimeEntry: the shape of the sieve entries of the third stage.
• Ratpoints.Sieve.checkPointList, Ratpoints.Sieve.checkNumWith: the points that the exact check delivers for a numerator with the flags of the search, and the same when the numerator is prime to the denominator, the check of the reference with the flags.
• Ratpoints.Sieve.acceptedPoints: the points that the extraction delivers for a numerator, those of the exact check when the numerator passes the test of a candidate, the test for common factors and the third stage.
• Ratpoints.Sieve.pointsAtInfinityList: the points at infinity that the search delivers with the flags of the search.
• Ratpoints.Sieve.testedCounts: the counts of the tests of a candidate of a list of numerators, the closed form of what the components of the sieve add to the counters (Ratpoints.Sieve.Counters, added field by field).
• Ratpoints.Sieve.SecondStageInvariant, Ratpoints.Sieve.SecondStageWordInvariant: the invariants of the loops of the second stage on a bit array and on a word, over the moduli with their reciprocals.

Main statements

• Ratpoints.Sieve.relprimeOdd_spec, Ratpoints.Sieve.relprime_spec: the binary algorithm decides whether gcd(m, n) = 1 for odd positive words m and n, and for words m > -2 ^ 63 and n ≥ 1.
• Ratpoints.Sieve.stage3_spec: the third stage is whether all its primes admit the numerator.
• Ratpoints.Sieve.CheckSpec.index_eq: the residue at which it reads the table of a prime is (a mod p) binv mod p, with the bias and without it.
• Ratpoints.Sieve.SieveEntry.IsPrimeEntry.admits_checkOf, Ratpoints.Sieve.all_admits_fillChecks: for a numerator prime to b with |a| ≤ H, a prime entry admits it in the third stage exactly when its row of b does, and the third stage is the survivor test of its entries.
• Ratpoints.Sieve.accepted_spec: the test of a candidate is the test of gcd(a, b) = 1 followed by the third stage; Ratpoints.Sieve.acceptedPoints_eq_ite: for a numerator a with |a| ≤ H < 2 ^ 63 and a denominator 0 < b < 2 ^ 63, the test with the exact check gives the points of the check with the flags (Ratpoints.Sieve.checkNumWith) when a survives the entries of the third stage, and none otherwise.
• Ratpoints.Sieve.snd_run_accepted: the test of a candidate with the count of the numerator before it adds the counts of Ratpoints.Sieve.testedCounts to the counters.
• Ratpoints.Sieve.checkPoint_eq_deliver, Ratpoints.Sieve.pointsAtInfinity_eq_deliver: the exact check and the points at infinity deliver their lists to the callback, the second call left out after a call that stops the search.
• Ratpoints.Sieve.checkNumWith_of_noCheck_eq_false, Ratpoints.Sieve.checkNumWith_of_noCheck_eq_true, Ratpoints.Sieve.flatMap_checkNumWith_of_noCheck_eq_false, Ratpoints.Sieve.pointsAtInfinityList_of_noCheck_eq_false, Ratpoints.Sieve.pointsAtInfinityList_of_noCheck_eq_true: the lists with the flags of the output, in terms of the brute-force reference without RATPOINTS_NO_CHECK, and the survivors with it.
• Ratpoints.Sieve.checkNumWith_eq_map, Ratpoints.Sieve.pointsAtInfinityList_eq_map: the lists with the flag of the reversal are those without it, mapped; Ratpoints.Sieve.map_checkNumWith_sublist, Ratpoints.Sieve.map_pointsAtInfinityList: without RATPOINTS_NO_CHECK and with RATPOINTS_NO_Y, with y replaced by 0, they are sublists of those under RATPOINTS_NO_CHECK.
• Ratpoints.Sieve.snd_snd_eq_zero_of_mem_pointsAtInfinityList, Ratpoints.Sieve.fst_eq_and_snd_snd_eq_of_mem_checkNumWith: without the flag of the reversal, the points at infinity have z = 0, and the points of a numerator a over b are (a, y, b).
• Ratpoints.Sieve.secondStage_spec, Ratpoints.Sieve.secondStageWord_spec: the second stage on a bit array, or on one of its words, gives its words and-ed with the rows of all its moduli.

Implementation notes

The file uses Lean core and Std only, as Ratpoints.Proof.Delivery and Ratpoints.Proof.Words do; the second stage builds on the words of the rows of the latter (Ratpoints.Sieve.SieveSpec.wordAt, Ratpoints.Sieve.andWords) and on its reading of the reciprocals in step with the moduli (Ratpoints.Sieve.eq_magic_and_of_next?_eq_some, Ratpoints.Sieve.next?_ne_none_of_lt). The proofs use only the facts on the constants that decide checks next to them, that Ratpoints.mulModLimit < 2 ^ 32 and Ratpoints.stage3Limit ≤ 2 ^ 32, never their values. The words of the test for common factors are read as natural numbers by Int64.toNatClampNeg, which is faithful on the non-negative words that the binary algorithm keeps; the facts on words that are not about the model are in Ratpoints.Proof.Bits.

The test for common factors

def Ratpoints.Sieve.RelprimeOddInvariant (g : Nat) : Std.WP.WhileInvariant (Int64 × Int64) Prop

The invariant of the loop of Ratpoints.Sieve.relprimeOdd, whose state is (m, n): both words are odd as natural numbers (Int64.toNatClampNeg), and so positive, they have the gcd g of the operands, and m = n at the exit.

Equations

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

theorem Ratpoints.Sieve.relprimeOddInvariant_self {m n : Int64} (h : m.toNatClampNeg % 2 = 1 ∧ n.toNatClampNeg % 2 = 1) : RelprimeOddInvariant (m.toNatClampNeg.gcd n.toNatClampNeg) false (m, n)

theorem Ratpoints.Sieve.RelprimeOddInvariant.toUInt64_ne_zero {g k : Nat} {m n : Int64} (hmn : (n != m) = true) (h : m.toNatClampNeg + n.toNatClampNeg = k ∧ RelprimeOddInvariant g false (m, n)) : ¬((m - n ^^^ (m - n) >>> 63) - (m - n) >>> 63).toUInt64 = 0

In the loop of Ratpoints.Sieve.relprimeOdd, from m ≠ n, the absolute value of the difference is a word other than 0, whose lowest set bit RP_CTZL may look for.

theorem Ratpoints.Sieve.RelprimeOddInvariant.shiftRight_min {g k t : Nat} {m n d : Int64} (hmn : (n != m) = true) (h : m.toNatClampNeg + n.toNatClampNeg = k ∧ RelprimeOddInvariant g false (m, n)) (hd : d = (m - n ^^^ (m - n) >>> 63) - (m - n) >>> 63) (ht : t = d.toUInt64.toBitVec.ctz.toNat) : (d >>> Int64.ofNat t).toNatClampNeg + (n + (m - n &&& (m - n) >>> 63)).toNatClampNeg < k ∧ RelprimeOddInvariant g false (d >>> Int64.ofNat t, n + (m - n &&& (m - n) >>> 63))

A step of the loop of Ratpoints.Sieve.relprimeOdd from m ≠ n, in the shape of the verification condition: n becomes the smaller of the two and m the odd part of their distance d, which keep what the loop keeps, and their sum, the measure, decreases.

theorem Ratpoints.Sieve.RelprimeOddInvariant.exit {g k : Nat} {m n : Int64} (hmn : ¬(n != m) = true) (h : m.toNatClampNeg + n.toNatClampNeg = k ∧ RelprimeOddInvariant g false (m, n)) : RelprimeOddInvariant g true (m, n)

theorem Ratpoints.Sieve.RelprimeOddInvariant.post {g : Nat} {m n : Int64} (h : RelprimeOddInvariant g true (m, n)) : (m == 1) = decide (g = 1)

At the exit of the loop of Ratpoints.Sieve.relprimeOdd, m = n is the gcd g.

theorem Ratpoints.Sieve.relprimeOdd_spec (m n : Int64) : ⦃ m.toNatClampNeg % 2 = 1 ∧ n.toNatClampNeg % 2 = 1 ⦄ relprimeOdd m n ⦃ fun (r : Bool) => r = decide (m.toNatClampNeg.gcd n.toNatClampNeg = 1) ⦄

The loop ends, since the sum of the two values decreases, and it ends at m = n = gcd(m, n); no operation leaves the range of a long, since the values stay positive.

theorem Ratpoints.Sieve.relprime_spec (m n : Int64) : ⦃ Int64.minValue < m ∧ 0 < n ⦄ relprime m n ⦃ fun (r : Bool) => r = decide (m.toInt.gcd n.toInt = 1) ⦄

The binary algorithm decides whether the numerator m is prime to the denominator n ≥ 1, for m other than -2 ^ 63, whose negation would leave the range of a long; no operation leaves it.

The third stage

def Ratpoints.Sieve.CheckSpec.admits (cs : CheckSpec) (a : Int) : Bool

Whether the third stage lets the numerator a through the prime of cs: when the prime divides the denominator (binv = 0), or when its table marks the residue at which the stage reads it (Ratpoints.Sieve.CheckSpec.index).

Equations

• cs.admits a = (cs.binv == 0 || cs.isFSquare[cs.index a]!)

theorem Ratpoints.Sieve.CheckSpec.admits_of_binv_eq_zero {cs : CheckSpec} (a : Int) (h : cs.binv = 0) : cs.admits a = true

theorem Ratpoints.Sieve.CheckSpec.admits_of_not_not {cs : CheckSpec} {a : Int} (h : ¬(!cs.isFSquare[cs.index a]!) = true) : cs.admits a = true

theorem Ratpoints.Sieve.CheckSpec.admits_eq_false {cs : CheckSpec} {a : Int} (h0 : ¬cs.binv = 0) (h : (!cs.isFSquare[cs.index a]!) = true) : cs.admits a = false

def Ratpoints.Sieve.Stage3Invariant (a : Int) (checks pref suff : List CheckSpec) (st : Option Bool × PUnit) : Prop

The invariant of the loop of Ratpoints.Sieve.stage3 over checks, after the checks pref with the checks suff still to come, on the result of an early return: without one, the checks so far let a through; with one, at the end, the result is whether all the checks do.

Equations

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

theorem Ratpoints.Sieve.stage3Invariant_nil (a : Int) (checks : List CheckSpec) : Stage3Invariant a checks [] checks (none, PUnit.unit)

theorem Ratpoints.Sieve.Stage3Invariant.push {a : Int} {checks pref suff : List CheckSpec} {cur : CheckSpec} {o : Option Bool} {u : PUnit} (h : Stage3Invariant a checks pref (cur :: suff) (o, u)) (hc : cur.admits a = true) : Stage3Invariant a checks (pref ++ [cur]) suff (none, PUnit.unit)

theorem Ratpoints.Sieve.stage3Invariant_some_false {a : Int} {checks pref suff : List CheckSpec} {cur : CheckSpec} (hl : checks = pref ++ cur :: suff) (hc : cur.admits a = false) : Stage3Invariant a checks checks [] (some false, PUnit.unit)

theorem Ratpoints.Sieve.Stage3Invariant.eq_all_of_some {a : Int} {checks : List CheckSpec} {o : Option Bool} {u : PUnit} {r : Bool} (h : Stage3Invariant a checks checks [] (o, u)) (ho : (o, u).fst = some r) : r = checks.all fun (x : CheckSpec) => x.admits a

theorem Ratpoints.Sieve.Stage3Invariant.true_eq_all_of_none {a : Int} {checks : List CheckSpec} {o : Option Bool} {u : PUnit} (h : Stage3Invariant a checks checks [] (o, u)) (ho : (o, u).fst = none) : true = checks.all fun (x : CheckSpec) => x.admits a

theorem Ratpoints.Sieve.stage3_spec (a : Int) (checks : List CheckSpec) : ⦃ True ⦄ stage3 a checks ⦃ fun (r : Bool) => r = checks.all fun (x : CheckSpec) => x.admits a ⦄

The third stage stops at the first prime that rejects the numerator, which is what all its primes say then.

@[simp]

theorem Ratpoints.Sieve.p_checkOf (b H : Nat) (e : SieveEntry) (mg : Nat) : (checkOf b H e mg).p = e.p

@[simp]

theorem Ratpoints.Sieve.magic_checkOf (b H : Nat) (e : SieveEntry) (mg : Nat) : (checkOf b H e mg).magic = e.magic

theorem Ratpoints.Sieve.bias_checkOf (b H : Nat) {e : SieveEntry} {t : Entry} (he : e.factors = [Factor.prime t]) (mg : Nat) : (checkOf b H e mg).bias = if 2 * e.p * H < stage3Limit then e.p * H else 0

theorem Ratpoints.Sieve.isFSquare_checkOf (b H : Nat) {e : SieveEntry} {t : Entry} (he : e.factors = [Factor.prime t]) (mg : Nat) : (checkOf b H e mg).isFSquare = t.isFSquare

theorem Ratpoints.Sieve.binv_checkOf {b : Nat} (H : Nat) {e : SieveEntry} {t : Entry} (he : e.factors = [Factor.prime t]) (hp : 0 < e.p) (hp32 : e.p ≤ 2 ^ 32) : (checkOf b H e (magic e.p)).binv = if b % e.p = 0 then 0 else t.inverses[b % e.p]!

The inverse of the denominator b that Ratpoints.Sieve.checkOf takes from the table t of the single factor of the sieve entry e of a modulus 0 < p ≤ 2 ^ 32, with the reciprocal of p: 0 when p divides b, and otherwise the entry of t at b mod p, which the reduction by the reciprocal gives for b ≤ Ratpoints.mulModLimit.

theorem Ratpoints.Sieve.le_mul_add_natCast_mul {a : Int} {p binv H : Nat} (ha : a.natAbs ≤ H) (hb : binv < p) : ↑H ≤ a * ↑binv + ↑(p * H)

The value a binv + p H that the third stage reduces with the bias p H, for |a| ≤ H and binv < p, is at least H (sift.c:303): a natural number.

theorem Ratpoints.Sieve.mul_add_natCast_mul_le_two_mul_mul_sub {a : Int} {p binv H : Nat} (ha : a.natAbs ≤ H) (hb : binv < p) : a * ↑binv + ↑(p * H) ≤ 2 * ↑p * ↑H - ↑H

The value a binv + p H that the third stage reduces with the bias p H, for |a| ≤ H and binv < p, is at most 2 p H - H (sift.c:303), below the bound 2 p H < Ratpoints.stage3Limit of the bias, and so a long.

theorem Ratpoints.Sieve.toNat_emod_mul_lt_sq (a : Int) {p binv : Nat} (hb : binv < p) : (a % ↑p).toNat * binv < p ^ 2

The product am binv that the third stage reduces without the bias, of the residue am of the numerator modulo p and the inverse binv < p, is below p ^ 2 (sift.c:307), a long for the moduli below 2 ^ 31.

theorem Ratpoints.Sieve.mulMod_toNat_mul_add_mul_magic {a : Int} {p binv H : Nat} (ha : a.natAbs ≤ H) (hb : binv < p) (hH : 2 * p * H < 2 ^ 32) : mulMod (a * ↑binv + ↑(p * H)).toNat p (magic p) = (a % ↑p).toNat * binv % p

With the bias p H, for |a| ≤ H, binv < p and 2 p H < 2 ^ 32, the value a binv + p H reduced by the reciprocal of p is the residue of (a mod p) binv: the value is below 2 ^ 32, and so is p unless a = H = 0.

theorem Ratpoints.Sieve.CheckSpec.index_eq {cs : CheckSpec} {a : Int} {H : Nat} (hb : cs.binv < cs.p) (ha : a.natAbs ≤ H) (hbias : cs.bias ≠ 0 → cs.bias = cs.p * H ∧ 2 * cs.p * H < 2 ^ 32 ∧ cs.magic = Sieve.magic cs.p) : cs.index a = (a % ↑cs.p).toNat * cs.binv % cs.p

The residue at which the third stage reads the table of the prime p of cs for the numerator a with |a| ≤ H is (a mod p) binv mod p, for binv < p, in both branches: with the bias p H, for 2 p H < 2 ^ 32 and the reciprocal of p, and without it.

theorem Ratpoints.Sieve.bias_checkOf_eq_and_of_ne_zero {b H : Nat} {e : SieveEntry} {t : Entry} (hf : e.factors = [Factor.prime t]) (hm : e.magic = magic e.p) {mg : Nat} (h0 : (checkOf b H e mg).bias ≠ 0) : (checkOf b H e mg).bias = (checkOf b H e mg).p * H ∧ 2 * (checkOf b H e mg).p * H < 2 ^ 32 ∧ (checkOf b H e mg).magic = magic (checkOf b H e mg).p

The bias of what the third stage needs of the entry e of a prime, when it is not 0, is p H with 2 p H < 2 ^ 32, and its reciprocal, that of the entry, is that of p when the entry's is.

def Ratpoints.Sieve.SieveEntry.IsPrimeEntry (e : SieveEntry) : Prop

The sieve entry e is that of a modulus 1 < p ≤ 2 ^ 32 whose single factor is a table t of p with inverses of the residues 0 < r < p that are residues 0 < t.inverses[r]! < p, and whose reciprocal is that of p (Ratpoints.Sieve.magic): the shape that the third stage needs of its entries (Ratpoints.Sieve.checkOf), whose rows it then tests (Ratpoints.Sieve.all_admits_fillChecks); the fields of the packing (the bias, the inverses of Ratpoints.rbaLength and of the strides) do not matter. The entry of a prime with the table of the reference has it (Ratpoints.Sieve.isPrimeEntry_examinePrime).

Equations

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

theorem Ratpoints.Sieve.SieveEntry.IsPrimeEntry.admits_checkOf {e : SieveEntry} (he : e.IsPrimeEntry) {b H : Nat} {a : Int} (hab : a.gcd ↑b = 1) (ha : a.natAbs ≤ H) : (checkOf b H e (Sieve.magic e.p)).admits a = e.admits b a

The third stage with the entry of a prime 1 < p ≤ 2 ^ 32 whose single factor is its table, of the shape of Ratpoints.Sieve.SieveEntry.IsPrimeEntry, lets a numerator a prime to b with |a| ≤ H through exactly when the row of b in the entry admits it: when p divides b, since then p ∤ a, and otherwise since the stage reads the table at (a mod p) b⁻¹ mod p (Ratpoints.Sieve.CheckSpec.index_eq).

theorem Ratpoints.Sieve.all_admits_fillChecks {es : List SieveEntry} (hes : ∀ (e : SieveEntry), e ∈ es → e.IsPrimeEntry) {a : Int} {b H : Nat} (hab : a.gcd ↑b = 1) (ha : a.natAbs ≤ H) : ((fillChecks b H es (List.map (fun (e : SieveEntry) => magic e.p) es)).all fun (x : CheckSpec) => x.admits a) = survives es b a

For a numerator a prime to b with |a| ≤ H, what the third stage needs of the sieve entries es of the shape of Ratpoints.Sieve.SieveEntry.IsPrimeEntry, with the reciprocals of their moduli, lets a through exactly when a survives these entries.

The test of a candidate

theorem Ratpoints.Sieve.accepted_spec (a : Int) (b : Nat) (checks : Thunk (List CheckSpec)) (cnt : Counters) : ⦃ 0 < b ∧ a.natAbs < 2 ^ 63 ∧ b < 2 ^ 63 ⦄ accepted a b checks cnt ⦃ fun (r : Bool × Counters) => r.fst = (decide (a.gcd ↑b = 1) && checks.get.all fun (x : CheckSpec) => x.admits a) ⦄

The test for common factors on the words of the numerator |a| < 2 ^ 63 and the denominator 0 < b < 2 ^ 63 is the test on the integers, and the thunk of the third stage is forced only when the numerator is prime to b.

theorem Ratpoints.Sieve.accepted_value (a : Int) (b : Nat) (checks : Thunk (List CheckSpec)) (cnt : Counters) : ⦃ True ⦄ accepted a b checks cnt ⦃ fun (r : Bool × Counters) => r = (accepted a b checks cnt).run ⦄

The test of a candidate as its value: the walks through the set bits of a word read it so, and their contracts need none of the hypotheses of Ratpoints.Sieve.accepted_spec.

theorem Ratpoints.Sieve.fst_run_accepted_congr (a : Int) (b : Nat) (checks : Thunk (List CheckSpec)) (cnt cnt' : Counters) : (accepted a b checks cnt).run.fst = (accepted a b checks cnt').run.fst

Whether a numerator passes the test of a candidate does not depend on the counters.

theorem Ratpoints.Sieve.fst_run_accepted_eq {es : List SieveEntry} (hes : ∀ (e : SieveEntry), e ∈ es → e.IsPrimeEntry) {a : Int} {b H : Nat} {checks : Thunk (List CheckSpec)} (cnt : Counters) (hc : checks.get = fillChecks b H es (List.map (fun (e : SieveEntry) => magic e.p) es)) (hb : 0 < b) (hb63 : b < 2 ^ 63) (ha : a.natAbs ≤ H) (hH : H < 2 ^ 63) : (accepted a b checks cnt).run.fst = (decide (a.gcd ↑b = 1) && survives es b a)

For |a| ≤ H < 2 ^ 63, a denominator 0 < b < 2 ^ 63 and the thunk of what the third stage needs of the sieve entries es of the shape of Ratpoints.Sieve.SieveEntry.IsPrimeEntry, with the reciprocals of their moduli, for b and H, a numerator goes on to the exact check when it is prime to b and survives these entries.

The counters

@[instance_reducible]

instance Ratpoints.Sieve.instAddCounters : Add Counters

The counters c and k (Ratpoints.Sieve.Counters) added field by field, wrapping as the UInt64s do: the counts of two pieces of work of the sieve, one after the other, as Ratpoints.Sieve.RunCounts.fold adds those of a block to those of the run.

Equations

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

theorem Ratpoints.Sieve.Counters.ext {x y : Counters} (words : x.words = y.words) (arrays : x.arrays = y.arrays) (bits : x.bits = y.bits) (coprime : x.coprime = y.coprime) (checks : x.checks = y.checks) (sifts : x.sifts = y.sifts) : x = y

theorem Ratpoints.Sieve.Counters.ext_iff {x y : Counters} : x = y ↔ x.words = y.words ∧ x.arrays = y.arrays ∧ x.bits = y.bits ∧ x.coprime = y.coprime ∧ x.checks = y.checks ∧ x.sifts = y.sifts

@[simp]

theorem Ratpoints.Sieve.Counters.words_add (c k : Counters) : (c + k).words = c.words + k.words

@[simp]

theorem Ratpoints.Sieve.Counters.arrays_add (c k : Counters) : (c + k).arrays = c.arrays + k.arrays

@[simp]

theorem Ratpoints.Sieve.Counters.bits_add (c k : Counters) : (c + k).bits = c.bits + k.bits

@[simp]

theorem Ratpoints.Sieve.Counters.coprime_add (c k : Counters) : (c + k).coprime = c.coprime + k.coprime

@[simp]

theorem Ratpoints.Sieve.Counters.checks_add (c k : Counters) : (c + k).checks = c.checks + k.checks

@[simp]

theorem Ratpoints.Sieve.Counters.sifts_add (c k : Counters) : (c + k).sifts = c.sifts + k.sifts

theorem Ratpoints.Sieve.Counters.add_assoc (a b c : Counters) : a + b + c = a + (b + c)

theorem Ratpoints.Sieve.Counters.add_comm (a b : Counters) : a + b = b + a

instance Ratpoints.Sieve.instAssociativeCountersHAdd : Std.Associative fun (x1 x2 : Counters) => x1 + x2

instance Ratpoints.Sieve.instCommutativeCountersHAdd : Std.Commutative fun (x1 x2 : Counters) => x1 + x2

@[simp]

theorem Ratpoints.Sieve.Counters.add_empty (c : Counters) : c + { } = c

theorem Ratpoints.Sieve.Counters.arrays_add_one (c : Counters) : { words := c.words, arrays := c.arrays + 1, bits := c.bits, coprime := c.coprime, checks := c.checks, sifts := c.sifts } = c + { arrays := 1 }

theorem Ratpoints.Sieve.Counters.words_add_eq (c : Counters) (x : UInt64) : { words := c.words + x, arrays := c.arrays, bits := c.bits, coprime := c.coprime, checks := c.checks, sifts := c.sifts } = c + { words := x }

theorem Ratpoints.Sieve.Counters.words_mk_add (x y : UInt64) : { words := x + y } = { words := x } + { words := y }

theorem Ratpoints.Sieve.Counters.arrays_mk_add (x y : UInt64) : { arrays := x + y } = { arrays := x } + { arrays := y }

def Ratpoints.Sieve.testedCounts (b : Nat) (checks : Thunk (List CheckSpec)) (as : List Int) : Counters

The counts of the tests of a candidate (Ratpoints.Sieve.accepted) of the numerators as over the denominator b, with the thunk checks of the third stage, each numerator counted in bits before its test, as the walk through the set bits of a word counts them (Ratpoints.Sieve.walkWord): bits the number of the numerators, coprime the number of those prime to b on the words of the C code (Ratpoints.Sieve.relprime), and checks the number of those that pass the third stage too, each as a UInt64, wrapping.

Equations

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

@[simp]

theorem Ratpoints.Sieve.testedCounts_nil (b : Nat) (checks : Thunk (List CheckSpec)) : testedCounts b checks [] = { }

theorem Ratpoints.Sieve.testedCounts_append (b : Nat) (checks : Thunk (List CheckSpec)) (as bs : List Int) : testedCounts b checks (as ++ bs) = testedCounts b checks as + testedCounts b checks bs

theorem Ratpoints.Sieve.snd_run_accepted (a : Int) (b : Nat) (checks : Thunk (List CheckSpec)) (cnt : Counters) : (accepted a b checks { words := cnt.words, arrays := cnt.arrays, bits := cnt.bits + 1, coprime := cnt.coprime, checks := cnt.checks, sifts := cnt.sifts }).run.snd = cnt + testedCounts b checks [a]

The counts of the test of a candidate, with the count of the numerator in bits before it as the walk through the set bits of a word counts it (Ratpoints.Sieve.walkWord).

theorem Ratpoints.Sieve.eq_add_testedCounts_of_eq_run_accepted {a : Int} {b : Nat} {checks : Thunk (List CheckSpec)} {ok : Bool} {c c' : Counters} (h : (ok, c') = (accepted a b checks { words := c.words, arrays := c.arrays, bits := c.bits + 1, coprime := c.coprime, checks := c.checks, sifts := c.sifts }).run) : c' = c + testedCounts b checks [a]

The counters c' after the test of a candidate of a, with its count in bits before it, in the shape of the verification conditions of the walk through the set bits of a word.

The exact check

@[simp]

theorem Ratpoints.Sieve.fst_snd_swapPoint (p : Int × Int × Int) : (swapPoint p).snd.fst = p.snd.fst

The map of the reversal keeps the y-coordinate.

theorem Ratpoints.Sieve.filter_map_swapPoint (rev noY : Bool) (L : List (Int × Int × Int)) : List.filter (fun (p : Int × Int × Int) => !noY || decide (0 ≤ p.snd.fst)) (List.map (if rev = true then swapPoint else id) L) = List.map (if rev = true then swapPoint else id) (List.filter (fun (p : Int × Int × Int) => !noY || decide (0 ≤ p.snd.fst)) L)

The map of the reversal and the test of RATPOINTS_NO_Y commute, since the map keeps the y-coordinate.

theorem Ratpoints.Sieve.swapPoint_fst_zero_snd (q : Int × Int × Int) : swapPoint (q.fst, 0, q.snd.snd) = ((swapPoint q).fst, 0, (swapPoint q).snd.snd)

The map of the reversal commutes with the replacement of y by 0, since it moves only x and z.

theorem Ratpoints.Delivery.callMapped_eq_deliver {σ : Type} (process : Int → Int → Int → σ → Answer σ) {r : Delivery σ} (hr : r.quit = false) (rev : Bool) (a b y : Int) : callMapped process r rev a b y = deliver process r [(if rev = true then Sieve.swapPoint else id) (a, y, b)]

One call of the callback with the point (a : y : b), mapped back after a reversal, on a delivery whose flag is clear, is the delivery of that point mapped by Ratpoints.Sieve.swapPoint when rev is set.

def Ratpoints.Sieve.checkPointList (w : List Int) (f b : Int) (fl : CheckFlags) (a : Int) : List (Int × Int × Int)

The points that the exact check (Ratpoints.Sieve.checkPoint) of the numerator a over the denominator b delivers to a callback that does not stop the search, for the products w, the factor f and the flags fl: unless fl.noCheck, the points (a, y, b) and, for y ≠ 0, (a, -y, b) when the value v of Horner's rule in a on w, times f, is y ^ 2 with y ≥ 0 (Ratpoints.BruteForce.pointsAbove), the point with y < 0 left out when fl.noY is set; with fl.noCheck, the one survivor (a, 0, b); each mapped by Ratpoints.Sieve.swapPoint when the flag fl.reversed of the reversal is set.

Equations

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

theorem Ratpoints.Sieve.checkPoint_eq_deliver {σ : Type} (process : Int → Int → Int → σ → Answer σ) (w : Thunk (List Int)) (d : Nat) (b : Int) (fl : CheckFlags) (a : Int) {r : Delivery σ} (hr : r.quit = false) : checkPoint process w d b fl a r = Delivery.deliver process r (checkPointList w.get (if d % 2 = 1 then b else 1) b fl a)

The exact check on a delivery whose flag is clear delivers the points of Ratpoints.Sieve.checkPointList, the call with -y left out after a call that stops the search.

def Ratpoints.Sieve.checkNumWith (w : List Int) (f b : Int) (fl : CheckFlags) (a : Int) : List (Int × Int × Int)

The check of the numerator a over the denominator b with the flags fl: the points of Ratpoints.Sieve.checkPointList when a is prime to b, and none otherwise. With the flags RATPOINTS_NO_CHECK and RATPOINTS_NO_Y clear, it is the check of the reference (Ratpoints.Sieve.checkNumWith_of_noCheck_eq_false).

Equations

• Ratpoints.Sieve.checkNumWith w f b fl a = if a.gcd b = 1 then Ratpoints.Sieve.checkPointList w f b fl a else []

theorem Ratpoints.Sieve.checkNumWith_of_noCheck_eq_false {fl : CheckFlags} (hc : fl.noCheck = false) (w : List Int) (f b a : Int) : checkNumWith w f b fl a = List.filter (fun (p : Int × Int × Int) => !fl.noY || decide (0 ≤ p.snd.fst)) (checkNum w f b fl.reversed a)

Without RATPOINTS_NO_CHECK, the check with the flags is the check of the reference with the flag of the reversal, without the points with y < 0 under RATPOINTS_NO_Y.

theorem Ratpoints.Sieve.checkNumWith_of_noCheck_eq_true {fl : CheckFlags} (hc : fl.noCheck = true) (w : List Int) (f b a : Int) : checkNumWith w f b fl a = if a.gcd b = 1 then [(if fl.reversed = true then swapPoint else id) (a, 0, b)] else []

Under RATPOINTS_NO_CHECK, the check with the flags gives the survivor (a, 0, b) of a numerator prime to b, mapped after a reversal.

theorem Ratpoints.Sieve.checkNumWith_eq_map (w : List Int) (f b : Int) (fl : CheckFlags) (a : Int) : checkNumWith w f b fl a = List.map (if fl.reversed = true then swapPoint else id) (checkNumWith w f b { noCheck := fl.noCheck, noY := fl.noY } a)

The check with the flags gives the points of the check without the flag of the reversal, mapped by Ratpoints.Sieve.swapPoint when it is set.

theorem Ratpoints.Sieve.mem_checkNumWith_of_noCheck {fl : CheckFlags} (hc : fl.noCheck = true) {w : List Int} {f b a : Int} {q : Int × Int × Int} : q ∈ checkNumWith w f b fl a ↔ a.gcd b = 1 ∧ q = (if fl.reversed = true then swapPoint else id) (a, 0, b)

theorem Ratpoints.Sieve.fst_eq_and_snd_snd_eq_of_mem_checkNumWith {w : List Int} {f b : Int} {fl : CheckFlags} (hr : fl.reversed = false) {a : Int} {q : Int × Int × Int} (hq : q ∈ checkNumWith w f b fl a) : q.fst = a ∧ q.snd.snd = b

Without the flag of the reversal, the points of the check with the flags of the numerator a over b are (a, y, b).

theorem Ratpoints.Sieve.map_checkNumWith_sublist (w : List Int) (f b : Int) (rev noY : Bool) (a : Int) : (List.map (fun (q : Int × Int × Int) => (q.fst, 0, q.snd.snd)) (checkNumWith w f b { reversed := rev, noY := true } a)).Sublist (checkNumWith w f b { reversed := rev, noCheck := true, noY := noY } a)

Without RATPOINTS_NO_CHECK and with RATPOINTS_NO_Y, the check of a numerator a over b gives at most one point, the one with y ≥ 0; with y replaced by 0 it is the survivor that the check gives under RATPOINTS_NO_CHECK.

def Ratpoints.Sieve.acceptedPoints (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) (checks : Thunk (List CheckSpec)) (a : Int) : List (Int × Int × Int)

The points that the extraction delivers for the numerator a over the denominator b: those of the exact check (Ratpoints.Sieve.checkPointList, with the thunk w of the products, the degree d and the flags fl) when a passes the test of a candidate (Ratpoints.Sieve.accepted, with the thunk checks of the third stage), and none otherwise.

Equations

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

theorem Ratpoints.Sieve.acceptedPoints_eq_ite {es : List SieveEntry} (hes : ∀ (e : SieveEntry), e ∈ es → e.IsPrimeEntry) {a : Int} {b H : Nat} {checks : Thunk (List CheckSpec)} (hc : checks.get = fillChecks b H es (List.map (fun (e : SieveEntry) => magic e.p) es)) (w : Thunk (List Int)) (d : Nat) (fl : CheckFlags) (hb : 0 < b) (hb63 : b < 2 ^ 63) (ha : a.natAbs ≤ H) (hH : H < 2 ^ 63) : acceptedPoints w d b fl checks a = if survives es b a = true then checkNumWith w.get (if d % 2 = 1 then ↑b else 1) (↑b) fl a else []

The points of Ratpoints.Sieve.acceptedPoints, the test of Ratpoints.Sieve.accepted followed by the exact check, are those of the check with the flags Ratpoints.Sieve.checkNumWith for a numerator a with |a| ≤ H < 2 ^ 63 that survives the sieve entries es of the third stage, of the shape of Ratpoints.Sieve.SieveEntry.IsPrimeEntry, and none for the others, for a denominator 0 < b < 2 ^ 63.

theorem Ratpoints.Sieve.checkPoint_eq_deliver_acceptedPoints {σ : Type} (process : Int → Int → Int → σ → Answer σ) (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) {checks : Thunk (List CheckSpec)} {a : Int} {cnt : Counters} (h : (accepted a b checks cnt).run.fst = true) {r : Delivery σ} (hr : r.quit = false) : checkPoint process w d (↑b) fl a r = Delivery.deliver process r (acceptedPoints w d b fl checks a)

The exact check of a numerator that passes the test of a candidate, on a delivery whose flag is clear, delivers the points of Ratpoints.Sieve.acceptedPoints.

theorem Ratpoints.Sieve.deliver_acceptedPoints_of_not_accepted {σ : Type} (process : Int → Int → Int → σ → Answer σ) (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) {checks : Thunk (List CheckSpec)} {a : Int} {cnt : Counters} (h : ¬(accepted a b checks cnt).run.fst = true) (r : Delivery σ) : Delivery.deliver process r (acceptedPoints w d b fl checks a) = r

A numerator that does not pass the test of a candidate has no points to deliver.

theorem Ratpoints.Sieve.flatMap_checkNumWith_of_noCheck_eq_false {fl : CheckFlags} (hc : fl.noCheck = false) (c : List Int) (d : Nat) (b : Int) (xs : List Int) : List.flatMap (checkNumWith (BruteForce.scaledCoeffs c d b) (if d % 2 = 1 then b else 1) b fl) xs = List.filter (fun (p : Int × Int × Int) => !fl.noY || decide (0 ≤ p.snd.fst)) (List.map (if fl.reversed = true then swapPoint else id) (BruteForce.pointsOfDen c d b xs))

Without RATPOINTS_NO_CHECK, the checks with the flags of the numerators xs over b give the points of the brute-force reference, mapped by Ratpoints.Sieve.swapPoint after a reversal, without those with y < 0 under RATPOINTS_NO_Y.

The points at infinity

def Ratpoints.Sieve.pointsAtInfinityList (c : List Int) (d : Nat) (fl : CheckFlags) : List (Int × Int × Int)

The points that Ratpoints.Sieve.pointsAtInfinity delivers to a callback that does not stop the search, for the polynomial of degree d with the coefficient list c and the flags fl: when there are points at infinity, for odd d or c_d a square (Ratpoints.Setup.isSquare), with fl.noCheck or odd d the point (1, 0, 0), and otherwise (1, s, 0) for s = √c_d followed, unless fl.noY, by (1, -s, 0); each mapped by Ratpoints.Sieve.swapPoint to (0, y, 1) when the flag fl.reversed of the reversal is set.

Equations

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

theorem Ratpoints.Sieve.pointsAtInfinity_eq_deliver {σ : Type} (process : Int → Int → Int → σ → Answer σ) (c : List Int) (d : Nat) (fl : CheckFlags) {r : Delivery σ} (hr : r.quit = false) : pointsAtInfinity process c d fl r = Delivery.deliver process r (pointsAtInfinityList c d fl)

The points at infinity on a delivery whose flag is clear deliver the points of Ratpoints.Sieve.pointsAtInfinityList, the call with -√c_d left out after a call that stops the search.

theorem Ratpoints.Sieve.pointsAtInfinityList_of_noCheck_eq_false {fl : CheckFlags} (hc : fl.noCheck = false) {c : List Int} {d : Nat} (h : d % 2 = 1 ∨ c.getD d 0 ≠ 0) : pointsAtInfinityList c d fl = List.filter (fun (p : Int × Int × Int) => !fl.noY || decide (0 ≤ p.snd.fst)) (List.map (if fl.reversed = true then swapPoint else id) (BruteForce.pointsAbove 1 0 (c.getD d 0 * if d % 2 = 1 then 0 else 1)))

Without RATPOINTS_NO_CHECK, for odd d or c_d ≠ 0, the points at infinity delivered are those of the candidate (1, 0) with the value F(1, 0), which is c_d for even d and 0 for odd d, without the point with y < 0 under RATPOINTS_NO_Y, and mapped after a reversal. (For even d and c_d = 0, which the search refuses before, the point (1 : 0 : 0) is delivered twice, once under RATPOINTS_NO_Y.)

theorem Ratpoints.Sieve.pointsAtInfinityList_of_noCheck_eq_true {fl : CheckFlags} (hc : fl.noCheck = true) (c : List Int) (d : Nat) : pointsAtInfinityList c d fl = if d % 2 = 1 ∨ Setup.isSquare (c.getD d 0) = true then [(if fl.reversed = true then swapPoint else id) (1, 0, 0)] else []

Under RATPOINTS_NO_CHECK, the points at infinity delivered are the one survivor (1, 0, 0), mapped after a reversal, when there are points at infinity.

theorem Ratpoints.Sieve.pointsAtInfinityList_eq_map (c : List Int) (d : Nat) (fl : CheckFlags) : pointsAtInfinityList c d fl = List.map (if fl.reversed = true then swapPoint else id) (pointsAtInfinityList c d { noCheck := fl.noCheck, noY := fl.noY })

The points at infinity are those without the flag of the reversal, mapped by Ratpoints.Sieve.swapPoint when it is set.

theorem Ratpoints.Sieve.eq_of_mem_pointsAtInfinityList_of_noCheck {fl : CheckFlags} (hc : fl.noCheck = true) {c : List Int} {d : Nat} {q : Int × Int × Int} (hq : q ∈ pointsAtInfinityList c d fl) : q = (if fl.reversed = true then swapPoint else id) (1, 0, 0)

theorem Ratpoints.Sieve.snd_snd_eq_zero_of_mem_pointsAtInfinityList {c : List Int} {d : Nat} {fl : CheckFlags} (hr : fl.reversed = false) {q : Int × Int × Int} (hq : q ∈ pointsAtInfinityList c d fl) : q.snd.snd = 0

Without the flag of the reversal, the points at infinity that the search delivers have z = 0.

theorem Ratpoints.Sieve.map_pointsAtInfinityList (c : List Int) (d : Nat) (rev noY : Bool) : List.map (fun (q : Int × Int × Int) => (q.fst, 0, q.snd.snd)) (pointsAtInfinityList c d { reversed := rev, noY := true }) = pointsAtInfinityList c d { reversed := rev, noCheck := true, noY := noY }

Without RATPOINTS_NO_CHECK and with RATPOINTS_NO_Y, the points at infinity, with y replaced by 0, are those under RATPOINTS_NO_CHECK.

The second stage

def Ratpoints.Sieve.SecondStageInvariant (nums : Vector UInt64 rbaPack) (i : Int) (specs : List SieveSpec) (mgs : List Nat) (pref : List SieveSpec) (st : Vector UInt64 rbaPack × List Nat) : Prop

The invariant of the loop of Ratpoints.Sieve.secondStage over the moduli specs and their reciprocals mgs on the bit array nums with the word number i, after the moduli pref, whose state is the bit array and the reciprocals still to come: before the loop has gone through all the moduli, these are the reciprocals after the first pref.length; and word κ of the bit array is word κ of nums and-ed with the row words of the moduli of pref.

Equations

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

theorem Ratpoints.Sieve.SecondStageInvariant.next?_ne_none {nums v : Vector UInt64 rbaPack} {i : Int} {small : Bool} {specs pref suff : List SieveSpec} {s : SieveSpec} {mgs rest : List Nat} (pre : StageFits specs mgs small i (i + 1)) (hs : specs = pref ++ s :: suff) (h : SecondStageInvariant nums i specs mgs pref (v, rest)) : Std.Stream.next? rest ≠ none

theorem Ratpoints.Sieve.secondStageInvariant_nil (nums : Vector UInt64 rbaPack) (i : Int) (specs : List SieveSpec) (mgs : List Nat) : SecondStageInvariant nums i specs mgs [] (nums, Std.toStream mgs)

theorem Ratpoints.Sieve.SecondStageInvariant.getElem!_eq {nums : Vector UInt64 rbaPack} {i : Int} {specs : List SieveSpec} {mgs : List Nat} {st : Vector UInt64 rbaPack × List Nat} (h : SecondStageInvariant nums i specs mgs specs st) {κ : Nat} (hκ : κ < rbaPack) : st.fst[κ]! = andWords specs nums[κ]! i κ

theorem Ratpoints.Sieve.SecondStageInvariant.of_isZeroAt {nums v : Vector UInt64 rbaPack} {i : Int} {specs pref suff : List SieveSpec} {cur : SieveSpec} {mgs rest rest' : List Nat} (hs : specs = pref ++ cur :: suff) (h : SecondStageInvariant nums i specs mgs pref (v, rest)) (hz : isZeroAt v 0 = true) : SecondStageInvariant nums i specs mgs specs (v, rest')

At the stop the bit array is zero, and so is its and with the rows of the other moduli.

theorem Ratpoints.Sieve.SecondStageInvariant.andBitArray {nums v : Vector UInt64 rbaPack} {i : Int} {small : Bool} {specs pref suff : List SieveSpec} {s : SieveSpec} {mgs rest rest' : List Nat} {mg : Nat} (pre : StageFits specs mgs small i (i + 1)) (hs : specs = pref ++ s :: suff) (h : SecondStageInvariant nums i specs mgs pref (v, rest)) (hnext : Std.Stream.next? rest = some (mg, rest')) : SecondStageInvariant nums i specs mgs (pref ++ [s]) (Sieve.andBitArray v 0 s.row (if small = true then mulMod (i + ↑s.offset).toNat s.p mg else (modLong (i + ↑s.offset) ↑s.p).toNat), rest')

A step of the loop of Ratpoints.Sieve.secondStage: the bit array and-ed with bit array (i + offset) mod p of the row of the next modulus s, the index that the reduction by the reciprocal of the cursor gives under the test small (Ratpoints.Sieve.SieveSpec.Fits.ite_mulMod_modLong_eq_toNat_emod).

theorem Ratpoints.Sieve.secondStage_spec (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (i : Int) (nums : Vector UInt64 rbaPack) : ⦃ StageFits specs mgs small i (i + 1) ⦄ secondStage specs mgs small i nums ⦃ fun (r : Vector UInt64 rbaPack) => ∀ (κ : Nat), κ < rbaPack → r[κ]! = andWords specs nums[κ]! i κ ⦄

The stop when the bit array is zero loses nothing, since a zero bit array stays zero; the reciprocals run in step with the moduli and do not run out before them.

def Ratpoints.Sieve.SecondStageWordInvariant (x0 : UInt64) (i : Int) (κ : Nat) (specs : List SieveSpec) (mgs : List Nat) (pref : List SieveSpec) (st : UInt64 × List Nat) : Prop

The invariant of the loop of Ratpoints.Sieve.secondStageWord over the moduli specs and their reciprocals mgs on word κ of the bit array with the word number i, from the word x0 on, after the moduli pref, whose state is the word and the reciprocals still to come: before the loop has gone through all the moduli, these are the reciprocals after the first pref.length; and the word is x0 and-ed with the row words of the moduli of pref.

Equations

• Ratpoints.Sieve.SecondStageWordInvariant x0 i κ specs mgs pref st = ((pref.length < specs.length → st.snd = List.drop pref.length mgs) ∧ st.fst = Ratpoints.Sieve.andWords pref x0 i κ)

theorem Ratpoints.Sieve.SecondStageWordInvariant.and {x0 x : UInt64} {i : Int} {κ : Nat} (hκ : κ < rbaPack) {small : Bool} {specs pref suff : List SieveSpec} {s : SieveSpec} {mgs rest rest' : List Nat} {mg : Nat} (pre : StageFits specs mgs small i (i + 1)) (hs : specs = pref ++ s :: suff) (h : SecondStageWordInvariant x0 i κ specs mgs pref (x, rest)) (hnext : Std.Stream.next? rest = some (mg, rest')) : SecondStageWordInvariant x0 i κ specs mgs (pref ++ [s]) (x &&& s.row[(rbaPack * if small = true then mulMod (i + ↑s.offset).toNat s.p mg else (modLong (i + ↑s.offset) ↑s.p).toNat) + κ]!, rest')

A step of the loop of Ratpoints.Sieve.secondStageWord, as for Ratpoints.Sieve.SecondStageInvariant.andBitArray.

theorem Ratpoints.Sieve.SecondStageWordInvariant.next?_ne_none {x0 x : UInt64} {i : Int} {κ : Nat} {small : Bool} {specs pref suff : List SieveSpec} {s : SieveSpec} {mgs rest : List Nat} (pre : StageFits specs mgs small i (i + 1)) (hs : specs = pref ++ s :: suff) (h : SecondStageWordInvariant x0 i κ specs mgs pref (x, rest)) : Std.Stream.next? rest ≠ none

theorem Ratpoints.Sieve.secondStageWordInvariant_nil (x0 : UInt64) (i : Int) (κ : Nat) (specs : List SieveSpec) (mgs : List Nat) : SecondStageWordInvariant x0 i κ specs mgs [] (x0, Std.toStream mgs)

theorem Ratpoints.Sieve.SecondStageWordInvariant.eq {x0 : UInt64} {i : Int} {κ : Nat} {specs : List SieveSpec} {mgs : List Nat} {st : UInt64 × List Nat} (h : SecondStageWordInvariant x0 i κ specs mgs specs st) : st.fst = andWords specs x0 i κ

theorem Ratpoints.Sieve.SecondStageWordInvariant.of_eq_zero {x0 x : UInt64} {i : Int} {κ : Nat} {specs pref suff : List SieveSpec} {cur : SieveSpec} {mgs rest rest' : List Nat} (hs : specs = pref ++ cur :: suff) (h : SecondStageWordInvariant x0 i κ specs mgs pref (x, rest)) (hz : (x == 0) = true) : SecondStageWordInvariant x0 i κ specs mgs specs (x, rest')

At the stop the word is zero, and so is its and with the rows of the other moduli.

theorem Ratpoints.Sieve.secondStageWord_spec (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (i : Int) {κ : Nat} (hκ : κ < rbaPack) (x : UInt64) : ⦃ StageFits specs mgs small i (i + 1) ⦄ secondStageWord specs mgs small i κ x ⦃ fun (r : UInt64) => r = andWords specs x i κ ⦄

The stop when the word is zero loses nothing, since a zero word stays zero; the reciprocals run in step with the moduli and do not run out before them.