The contracts of the bit arrays of words

The lemmas on the operations on the bit arrays of 64-bit words of the model, on its rows as words, on the rows under a unit, on the check of a numerator and on the array of a walk through the set bits of a word, and the contract of the first stage over a piece, as @[spec] theorems proved with vcgen, the program logic of Lean core, with loop invariants that are named definitions.

Main definitions

• Ratpoints.Sieve.Factor.HasInverses, Ratpoints.Sieve.SieveEntry.HasInverses: what the scaling of the rows by a unit needs of a factor of a modulus, its modulus dividing the modulus and its table of inverses inverting its units, and of a sieve entry, all its factors having it.
• Ratpoints.Sieve.SieveSpec.wordAt, Ratpoints.Sieve.andWords: the row word that the first stage ands into a word of a piece, at the offset of the row, and the words of a piece after it.
• Ratpoints.Sieve.SieveSpec.Reads: the rows of a modulus read a test of the bits.
• Ratpoints.Sieve.AndRowsFillInvariant, Ratpoints.Sieve.AndRowsLoopInvariant, Ratpoints.Sieve.AndRowsStartInvariant: the invariants of the loop of the first stage one row at a time that sets the bit arrays to the class word, from the last, of its loop over the moduli with their reciprocals, and of its loops over the bit arrays of a modulus.
• Ratpoints.Sieve.WalkWordInvariant: the invariant of the array that a walk through the set bits of a word, lowest first, appends to.

Main statements

• Ratpoints.Sieve.getElem!_andBitArray, Ratpoints.Sieve.getElem!_loadBitArray, Ratpoints.Sieve.getElem!_storeBitArray, Ratpoints.Sieve.getElem!_fillBitArray: the operations on bit arrays of the first stage set the words of one bit array and leave the other words as they are; Ratpoints.Sieve.getElem!_andBitArray_mul_add, Ratpoints.Sieve.getElem!_loadBitArray_mul_add: the same at word κ of bit array j.
• Ratpoints.Sieve.getLsbD_clearLowBits, Ratpoints.Sieve.getLsbD_clearHighBits: which bits the masks at the two ends of the numerator range keep.
• Ratpoints.Sieve.isZeroAt_eq_true_iff: a bit array is zero when all its words are.
• Ratpoints.Sieve.Entry.admits_mod_of_dvd, Ratpoints.Sieve.Power.admits_mod_of_dvd, Ratpoints.Sieve.Factor.admits_mod_of_dvd: the row of a prime, a prime power or a factor reads the residues modulo a multiple of its modulus as those of the numbers.
• Ratpoints.Sieve.Factor.admits_congr, Ratpoints.Sieve.Factor.admits_mod_left: the row of a factor reads the residues of the denominator and the numerator modulo its modulus.
• Ratpoints.Sieve.SieveEntry.admits_eq_all: the row of a sieve entry whose factors have moduli dividing its modulus is the and of the rows of its factors; Ratpoints.Sieve.SieveEntry.admits_eq_of_factors_eq: that of an entry with one factor of its modulus is the row of the factor.
• Ratpoints.Sieve.SieveEntry.admits_mul: the row of a sieve entry whose factors have their tables of inverses is unchanged when the denominator and the numerator are scaled by a unit.
• Ratpoints.Sieve.SieveEntry.reads_closedRow: the closed form of the row of b / 2 ^ k (Ratpoints.Sieve.closedRow) at the offset of the class a₀ mod 2 ^ k reads at bit j whether the row of b admits the numerator a₀ + 2 ^ k j.
• Ratpoints.Sieve.getLsbD_andWords: the words of rows that read tests of the bits, and-ed into a word, have the bits of the word that pass all the tests.
• Ratpoints.Sieve.andWords_append: and-ing the rows of two lists of moduli one after the other is and-ing those of their concatenation.
• Ratpoints.Sieve.andRows_spec: after the first stage over a piece from the class word cw, with moduli in the range of the packing and their reciprocals (Ratpoints.Sieve.SieveSpec.Fits) and the test small of the piece (Ratpoints.Sieve.SmallFits), each word of the piece is cw and-ed with its row words (Ratpoints.Sieve.andWords).
• Ratpoints.BruteForce.pointsOfDen_eq_flatMap_checkNum: the points that the brute-force reference finds over a denominator are those of Ratpoints.Sieve.checkNum for its numerators, one after the other, with the flag of the reversal clear.
• Ratpoints.Sieve.checkNum_eq_map, Ratpoints.Sieve.flatMap_checkNum: with the flag of the reversal set, the check of a numerator gives the points of the check with the flag clear, mapped by Ratpoints.Sieve.swapPoint, and so do the checks of a list of numerators, one after the other.

Implementation notes

The file uses Lean core and Std only, as Ratpoints.Proof.Sieve does; the lemmas on words that are not about the model are in Ratpoints.Proof.Bits. The proofs use only that Ratpoints.rbaPack and Ratpoints.chunk are positive, never their values.

The width of the bit arrays

theorem Ratpoints.rbaLength_mul (j : Nat) : rbaLength * j = 64 * (rbaPack * j)

theorem Ratpoints.lt_rbaLength_mul_of_lt {n y t : Nat} (hy : y < n * rbaPack) (ht : t < 64) : 64 * y + t < rbaLength * n

Operations on bit arrays

theorem Ratpoints.Sieve.rbaPack_mul_le_and_lt_iff {y j : Nat} : rbaPack * j ≤ y ∧ y < rbaPack * j + rbaPack ↔ y / rbaPack = j

Word y lies in bit array j exactly when y / rbaPack = j.

theorem Ratpoints.Sieve.getElem!_andBitArray {m : Nat} (v : Vector UInt64 m) (j : Nat) (row : Array UInt64) (x : Nat) {y : Nat} (hy : y < m) : (andBitArray v j row x)[y]! = if y / rbaPack = j then v[y]! &&& row[rbaPack * x + y % rbaPack]! else v[y]!

theorem Ratpoints.Sieve.getElem!_loadBitArray {m : Nat} (v : Vector UInt64 m) (j : Nat) (cw : UInt64) (row : Array UInt64) (x : Nat) {y : Nat} (hy : y < m) : (loadBitArray v j cw row x)[y]! = if y / rbaPack = j then cw &&& row[rbaPack * x + y % rbaPack]! else v[y]!

theorem Ratpoints.Sieve.getElem!_andBitArray_mul_add {m : Nat} (v : Vector UInt64 m) (cur : Nat) (row : Array UInt64) (x : Nat) {j κ : Nat} (hκ : κ < rbaPack) (hy : rbaPack * j + κ < m) : (andBitArray v cur row x)[rbaPack * j + κ]! = if j = cur then v[rbaPack * j + κ]! &&& row[rbaPack * x + κ]! else v[rbaPack * j + κ]!

Ratpoints.Sieve.getElem!_andBitArray at word κ of bit array j.

theorem Ratpoints.Sieve.getElem!_loadBitArray_mul_add {m : Nat} (v : Vector UInt64 m) (cur : Nat) (cw : UInt64) (row : Array UInt64) (x : Nat) {j κ : Nat} (hκ : κ < rbaPack) (hy : rbaPack * j + κ < m) : (loadBitArray v cur cw row x)[rbaPack * j + κ]! = if j = cur then cw &&& row[rbaPack * x + κ]! else v[rbaPack * j + κ]!

Ratpoints.Sieve.getElem!_loadBitArray at word κ of bit array j.

theorem Ratpoints.Sieve.getElem!_storeBitArray {m k : Nat} (v : Vector UInt64 m) (y' : Nat) (regs : Vector UInt64 k) (j : Nat) {y : Nat} (hy : y < m) : (storeBitArray v y' regs j)[y]! = if y / rbaPack = y' then regs[rbaPack * j + y % rbaPack]! else v[y]!

theorem Ratpoints.Sieve.getElem!_fillBitArray {m : Nat} (v : Vector UInt64 m) (y' : Nat) (cw : UInt64) {y : Nat} (hy : y < m) : (fillBitArray v y' cw)[y]! = if y / rbaPack = y' then cw else v[y]!

theorem Ratpoints.Sieve.getLsbD_clearLowBits {m : Nat} (v : Vector UInt64 m) (s : Nat) {y : Nat} (hy : y < m) (t : Nat) : (clearLowBits v s)[y]!.toBitVec.getLsbD t = (v[y]!.toBitVec.getLsbD t && decide (s ≤ 64 * y + t))

theorem Ratpoints.Sieve.getLsbD_clearHighBits {m : Nat} (v : Vector UInt64 m) (j : Nat) {s : Nat} (hs : s < rbaLength) {y : Nat} (hy : y < m) (hyj : y < rbaPack * (j + 1)) (t : Nat) : (clearHighBits v j s)[y]!.toBitVec.getLsbD t = (v[y]!.toBitVec.getLsbD t && decide (64 * y + t + s < rbaLength * (j + 1)))

theorem Ratpoints.Sieve.isZeroAt_eq_true_iff {m : Nat} (v : Vector UInt64 m) (pos : Nat) : isZeroAt v pos = true ↔ ∀ (κ : Nat), κ < rbaPack → v[rbaPack * pos + κ]! = 0

The rows as words

theorem Ratpoints.Sieve.SieveEntry.admits_congr (e : SieveEntry) (b : Nat) {a a' : Int} (h : a % ↑e.p = a' % ↑e.p) : e.admits b a = e.admits b a'

theorem Ratpoints.Sieve.SieveEntry.admits_mod (e : SieveEntry) (b : Nat) : e.admits (b % e.p) = e.admits b

The rows under a unit

theorem Ratpoints.Sieve.Entry.admits_mod_of_dvd (e : Entry) {m : Nat} (h : e.p ∣ m) (b : Nat) (a : Int) : e.admits (b % m) (a % ↑m) = e.admits b a

theorem Ratpoints.Sieve.Power.admits_mod_of_dvd (pw : Power) {m : Nat} (h : pw.m ∣ m) (b : Nat) (a : Int) : pw.admits (b % m) (a % ↑m) = pw.admits b a

theorem Ratpoints.Sieve.Factor.admits_mod_of_dvd (f : Factor) {m : Nat} (h : f.modulus ∣ m) (b : Nat) (a : Int) : f.admits (b % m) (a % ↑m) = f.admits b a

theorem Ratpoints.Sieve.Factor.admits_congr {f : Factor} (b : Nat) {a a' : Int} (h : a % ↑f.modulus = a' % ↑f.modulus) : f.admits b a = f.admits b a'

theorem Ratpoints.Sieve.Factor.admits_mod_left (f : Factor) (b : Nat) (a : Int) : f.admits (b % f.modulus) a = f.admits b a

theorem Ratpoints.Sieve.SieveEntry.admits_eq_all {e : SieveEntry} (h : ∀ (f : Factor), f ∈ e.factors → f.modulus ∣ e.p) (b : Nat) (a : Int) : e.admits b a = e.factors.all fun (x : Factor) => x.admits b a

The row of a sieve entry whose factors have moduli dividing its modulus admits a numerator when each factor does, the factors reading the residues modulo their own moduli.

theorem Ratpoints.Sieve.SieveEntry.admits_eq_of_factors_eq {e : SieveEntry} {f : Factor} (he : e.factors = [f]) (hp : e.p = f.modulus) : e.admits = f.admits

A sieve entry whose one factor f has the modulus of the entry, as a prime or a prime power is its own factor (Ratpoints.makeModulus), has the row of the factor.

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

What the scaling of the rows by a unit needs of a factor of the modulus P of a sieve entry: the modulus of the factor divides P, and its table of inverses inverts the residues at which its row reads it, the nonzero residues of a prime and the units of a prime power p ^ e, whose prime divides it (Ratpoints.Sieve.SieveEntry.admits_mul).

Equations

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

theorem Ratpoints.Sieve.Factor.HasInverses.modulus_dvd {f : Factor} {P : Nat} (hf : f.HasInverses P) : f.modulus ∣ P

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

The factors of a sieve entry have their tables of inverses for its modulus (Ratpoints.Sieve.Factor.HasInverses): what the scaling of its row by a unit needs (Ratpoints.Sieve.SieveEntry.admits_mul).

Equations

• e.HasInverses = ∀ (f : Ratpoints.Sieve.Factor), f ∈ e.factors → f.HasInverses e.p

theorem Ratpoints.Sieve.Entry.admits_mul {t : Entry} (hq : 0 < t.p) (hinv : ∀ (r : Nat), r < t.p → r ≠ 0 → t.inverses[r]! * r % t.p = 1) {u v : Nat} (huv : v * u % t.p = 1 % t.p) (b : Nat) (a : Int) : t.admits (u * b) (↑u * a) = t.admits b a

The row of a prime q > 0 whose table inverts the nonzero residues is unchanged when the denominator and the numerator are scaled by a unit u modulo q.

theorem Ratpoints.Sieve.Power.admits_mul {pw : Power} (hm : 0 < pw.m) (hpm : pw.p ∣ pw.m) (hinv : ∀ (x : Nat), x < pw.m → x % pw.p ≠ 0 → pw.inv[x]! * x % pw.m = 1) {u v : Nat} (huv : v * u % pw.m = 1 % pw.m) (b : Nat) (a : Int) : pw.admits (u * b) (↑u * a) = pw.admits b a

The row of a prime power p ^ e with p ∣ p ^ e, whose table inverts its units, is unchanged when the denominator and the numerator are scaled by a unit u modulo p ^ e.

theorem Ratpoints.Sieve.Factor.HasInverses.admits_mul {f : Factor} {P : Nat} (hf : f.HasInverses P) (hP : 0 < P) {u v : Nat} (huv : v * u % P = 1) (b : Nat) (a : Int) : f.admits (u * b) (↑u * a) = f.admits b a

The row of a factor of a modulus P > 0 with its tables of inverses is unchanged when the denominator and the numerator are scaled by a unit u modulo P.

theorem Ratpoints.Sieve.SieveEntry.admits_mul {e : SieveEntry} (he : e.HasInverses) {u v : Nat} (huv : v * u % e.p = 1) (b : Nat) (a : Int) : e.admits (u * b) (↑u * a) = e.admits b a

The row of a sieve entry whose factors have their tables of inverses is unchanged when the denominator and the numerator are scaled by a unit u modulo the modulus, with an inverse v.

One piece

def Ratpoints.Sieve.SieveSpec.wordAt (s : SieveSpec) (w0 : Int) (y : Nat) : UInt64

The word of the row of s that the first stage ands into word y of the piece from the word number w0 on: word y % rbaPack of bit array (w0 + offset + y / rbaPack) mod p of the row, for the number rbaPack of words of a bit array (Ratpoints.rbaPack).

Equations

• s.wordAt w0 y = s.row[Ratpoints.rbaPack * ((w0 + ↑s.offset + ↑(y / Ratpoints.rbaPack)) % ↑s.p).toNat + y % Ratpoints.rbaPack]!

theorem Ratpoints.Sieve.SieveSpec.wordAt_of_lt (s : SieveSpec) (i : Int) {κ : Nat} (hκ : κ < rbaPack) : s.wordAt i κ = s.row[rbaPack * ((i + ↑s.offset) % ↑s.p).toNat + κ]!

Word κ < Ratpoints.rbaPack of the row of s for the word number i is word κ of bit array (i + offset) mod p.

theorem Ratpoints.Sieve.SieveSpec.wordAt_rbaPack_mul_add (s : SieveSpec) (w0 : Int) (pos : Nat) {κ : Nat} (hκ : κ < rbaPack) : s.wordAt w0 (rbaPack * pos + κ) = s.wordAt (w0 + ↑pos) κ

The row word of word κ of bit array pos of a piece from the word number w0 on is the row word of word κ of the bit array with the word number w0 + pos.

theorem Ratpoints.Sieve.SieveSpec.getLsbD_wordAt_mk {e : SieveEntry} (b : Nat) (hp : 0 < e.p) (off st stop : Nat) (w0 : Int) (y t : Nat) : ({ p := e.p, offset := off, row := closedRow e.admits e.p b, start := st, stop := stop }.wordAt w0 y).toBitVec.getLsbD t = (decide (t < 64) && e.admits b (↑rbaLength * (w0 + ↑off) + 64 * ↑y + ↑t))

Bit t of the row word of word y of a piece from the word number w0 on, in the closed form of the row of the denominator b with the offset off and any start and end, is the bit of the numerator rbaLength (w0 + off) + 64 y + t in the row of b.

def Ratpoints.Sieve.SieveSpec.Reads (s : SieveSpec) (f : Int → Bool) : Prop

The rows of the sieve spec s read the test f of the bits: bit t of the row word of word y of a piece from the word number i on is f at the bit rbaLength i + 64 y + t.

Equations

• s.Reads f = ∀ (i : Int) (y t : Nat), (s.wordAt i y).toBitVec.getLsbD t = (decide (t < 64) && f (↑Ratpoints.rbaLength * i + 64 * ↑y + ↑t))

theorem Ratpoints.Sieve.SieveEntry.reads_closedRow {e : SieveEntry} (he : e.HasInverses) (hp : 0 < e.p) {k a0 off bp b v st stop : Nat} (hv : v * 2 ^ k % e.p = 1) (hoff : off * (2 ^ k * rbaLength) % e.p = a0 % e.p) (hbp : 2 ^ k * bp % e.p = b % e.p) : { p := e.p, offset := off, row := closedRow e.admits e.p bp, start := st, stop := stop }.Reads fun (j : Int) => e.admits b (↑a0 + 2 ^ k * j)

The closed form of the row of the residue bp of the denominator b divided by the stride 2 ^ k (2 ^ k bp ≡ b), with any start and end, read at the offset off of the class a₀ mod 2 ^ k (off 2 ^ k Ratpoints.rbaLength ≡ a₀), reads at bit j whether the row of b admits the numerator a₀ + 2 ^ k j, when 2 ^ k has an inverse v modulo p and the factors of the entry have their tables of inverses: the rows are unchanged when the denominator and the numerator are scaled by the unit 2 ^ k (Ratpoints.Sieve.SieveEntry.admits_mul).

theorem Ratpoints.Sieve.classBit_rbaLength_mul_add (cw : UInt64) (w0 : Int) (y : Nat) {t : Nat} (ht : t < 64) : classBit cw (↑rbaLength * w0 + 64 * ↑y + ↑t) = cw.toBitVec.getLsbD t

def Ratpoints.Sieve.andWords (specs : List SieveSpec) (cw : UInt64) (w0 : Int) (y : Nat) : UInt64

The word cw and-ed in turn with the words of the rows specs at word y of a piece from the word number w0 on (Ratpoints.Sieve.SieveSpec.wordAt): word y of the piece after the first stage from the class word cw, or, with w0 the word number of a bit array and y one of its words, that word after the second stage from its word cw in a copy of the bit array.

Equations

• Ratpoints.Sieve.andWords specs cw w0 y = List.foldl (fun (acc : UInt64) (s : Ratpoints.Sieve.SieveSpec) => acc &&& s.wordAt w0 y) cw specs

theorem Ratpoints.Sieve.andWords_append (l₁ l₂ : List SieveSpec) (cw : UInt64) (w0 : Int) (y : Nat) : andWords (l₁ ++ l₂) cw w0 y = andWords l₂ (andWords l₁ cw w0 y) w0 y

@[simp]

theorem Ratpoints.Sieve.andWords_zero (l : List SieveSpec) (w0 : Int) (y : Nat) : andWords l 0 w0 y = 0

theorem Ratpoints.Sieve.andWords_concat (l : List SieveSpec) (s : SieveSpec) (cw : UInt64) (w0 : Int) (y : Nat) : andWords (l ++ [s]) cw w0 y = andWords l cw w0 y &&& s.wordAt w0 y

theorem Ratpoints.Sieve.andWords_rbaPack_mul_add (specs : List SieveSpec) (x : UInt64) (w0 : Int) (pos : Nat) {κ : Nat} (hκ : κ < rbaPack) : andWords specs x w0 (rbaPack * pos + κ) = andWords specs x (w0 + ↑pos) κ

theorem Ratpoints.Sieve.getLsbD_andWords {sfs : List (SieveSpec × (Int → Bool))} (h : ∀ (sf : SieveSpec × (Int → Bool)), sf ∈ sfs → sf.fst.Reads sf.snd) (cw : UInt64) (w0 : Int) (y t : Nat) : (andWords (List.map Prod.fst sfs) cw w0 y).toBitVec.getLsbD t = (cw.toBitVec.getLsbD t && sfs.all fun (x : SieveSpec × (Int → Bool)) => x.snd (↑rbaLength * w0 + 64 * ↑y + ↑t))

The words of rows that read the tests sf.2 of the bits (Ratpoints.Sieve.SieveSpec.Reads), and-ed into the word cw, have bit t set when cw has it and all the tests pass at the bit rbaLength w0 + 64 y + t.

theorem Ratpoints.Sieve.eq_magic_and_of_next?_eq_some {specs pref suff : List SieveSpec} {s : SieveSpec} {mgs rest rest' : List Nat} {mg : Nat} (hmg : mgs = List.map (fun (x : SieveSpec) => magic x.p) specs) (hs : specs = pref ++ s :: suff) (hrest : pref.length < specs.length → rest = List.drop pref.length mgs) (hnext : Std.Stream.next? rest = some (mg, rest')) : mg = magic s.p ∧ rest' = List.drop (pref ++ [s]).length mgs

The reciprocals of the moduli specs that a loop over the moduli and their reciprocals in step has still to read after the moduli pref, before it has gone through all of them, are those after the first pref.length: the next is that of the next modulus, and the cursor moves on.

theorem Ratpoints.Sieve.next?_ne_none_of_lt {specs pref suff : List SieveSpec} {s : SieveSpec} {mgs rest : List Nat} (hmg : mgs = List.map (fun (x : SieveSpec) => magic x.p) specs) (hs : specs = pref ++ s :: suff) (hrest : pref.length < specs.length → rest = List.drop pref.length mgs) : Std.Stream.next? rest ≠ none

The reciprocals of a loop over the moduli and their reciprocals in step do not run out before the moduli.

def Ratpoints.Sieve.AndRowsLoopInvariant {m : Nat} (cw : UInt64) (w0 : Int) (n : Nat) (mgs : List Nat) (pref : List SieveSpec) (st : Vector UInt64 m × List Nat) : Prop

The invariant of the loop of Ratpoints.Sieve.andRows over the moduli and, in step with them, their reciprocals mgs, whose state is the piece and the reciprocals still to come: after the moduli pref, the reciprocals still to come are those after the first pref.length, and the words of the n bit arrays of the piece are the class word cw and-ed with their row words (Ratpoints.Sieve.andWords).

Equations

• Ratpoints.Sieve.AndRowsLoopInvariant cw w0 n mgs pref st = (st.snd = List.drop pref.length mgs ∧ ∀ (y : Nat), y < n * Ratpoints.rbaPack → st.fst[y]! = Ratpoints.Sieve.andWords pref cw w0 y)

def Ratpoints.Sieve.AndRowsRowInvariant {m : Nat} (cw : UInt64) (w0 : Int) (n : Nat) (pref : List SieveSpec) (s : SieveSpec) (c : Nat) (surv : Vector UInt64 m) : Prop

The invariant of the loops of Ratpoints.Sieve.andRows over the bit arrays for the modulus s after the moduli pref: the words of the bit arrays below c are and-ed with the row of s as well, the others not yet.

Equations

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

@[reducible, inline]

abbrev Ratpoints.Sieve.andRowsStart (small : Bool) (w0 : Int) (s : SieveSpec) (mg : Nat) : Nat

The residue r of -w0 - offset modulo p that Ratpoints.Sieve.andRows computes with the reciprocal mg of the cursor, by Ratpoints.Sieve.modMul under the test small and by Ratpoints.Sieve.modLong otherwise: the first stage ands bit array p - r + j of the row of s into bit array j of a piece from the word number w0 on, for j < r.

Equations

• Ratpoints.Sieve.andRowsStart small w0 s mg = (if small = true then Ratpoints.Sieve.modMul (-w0 - ↑s.offset) s.p mg else Ratpoints.Sieve.modLong (-w0 - ↑s.offset) ↑s.p).toNat

def Ratpoints.Sieve.AndRowsStartInvariant {m : Nat} (cw : UInt64) (w0 : Int) (n : Nat) (pref : List SieveSpec) (s : SieveSpec) (r c : Nat) (surv : Vector UInt64 m) : Prop

Ratpoints.Sieve.AndRowsRowInvariant for the modulus s with the bit arrays below c done, and r, the index that the loops over the bit arrays use, is the residue of -(w0 + offset) modulo p > 0: the invariant of each loop over the bit arrays, with the c of that loop.

Equations

• Ratpoints.Sieve.AndRowsStartInvariant cw w0 n pref s r c surv = ((0 < s.p ∧ r = (-(w0 + ↑s.offset) % ↑s.p).toNat) ∧ Ratpoints.Sieve.AndRowsRowInvariant cw w0 n pref s c surv)

@[reducible, inline]

abbrev Ratpoints.Sieve.AndRowsHeadInvariant {m : Nat} (small : Bool) (cw : UInt64) (w0 : Int) (n : Nat) (pref : List SieveSpec) (s : SieveSpec) (mg : Nat) (done : List Nat) (surv : Vector UInt64 m) : Prop

The invariant of the loops of Ratpoints.Sieve.andRows over the bit arrays before the first whole period of the row of s, with the reciprocal mg of the cursor: the bit arrays done are done.

Equations

• Ratpoints.Sieve.AndRowsHeadInvariant small cw w0 n pref s mg done surv = Ratpoints.Sieve.AndRowsStartInvariant cw w0 n pref s (Ratpoints.Sieve.andRowsStart small w0 s mg) done.length surv

@[reducible, inline]

abbrev Ratpoints.Sieve.AndRowsPeriodInvariant {m : Nat} (small : Bool) (cw : UInt64) (w0 : Int) (n : Nat) (pref : List SieveSpec) (s : SieveSpec) (mg : Nat) (done : List Nat) (surv : Vector UInt64 m) : Prop

The invariant of the loop of Ratpoints.Sieve.andRows over the whole periods of the row of s, with the reciprocal mg of the cursor: the bit arrays before the first whole period and the periods done are done.

Equations

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

@[reducible, inline]

abbrev Ratpoints.Sieve.AndRowsPacketInvariant {m : Nat} (small : Bool) (cw : UInt64) (w0 : Int) (n : Nat) (pref : List SieveSpec) (s : SieveSpec) (mg : Nat) (periods done : List Nat) (surv : Vector UInt64 m) : Prop

The invariant of the loop of Ratpoints.Sieve.andRows over one whole period of the row of s, with the reciprocal mg of the cursor, after the periods periods: the bit arrays done of the current period are done too.

Equations

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

@[reducible, inline]

abbrev Ratpoints.Sieve.AndRowsTailInvariant {m : Nat} (small : Bool) (cw : UInt64) (w0 : Int) (n : Nat) (pref : List SieveSpec) (s : SieveSpec) (mg : Nat) (done : List Nat) (surv : Vector UInt64 m) : Prop

The invariant of the loop of Ratpoints.Sieve.andRows over the bit arrays after the last whole period of the row of s, with the reciprocal mg of the cursor: the bit arrays before them and the bit arrays done are done.

Equations

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

def Ratpoints.Sieve.AndRowsFillInvariant {m : Nat} (cw : UInt64) (n c : Nat) (surv : Vector UInt64 m) : Prop

The invariant of the loop of Ratpoints.Sieve.andRows that sets the bit arrays of the piece to the class word cw, from the last: after c steps, the words of the last c of the n bit arrays are cw.

Equations

• Ratpoints.Sieve.AndRowsFillInvariant cw n c surv = ∀ (y : Nat), y < n * Ratpoints.rbaPack → n - c ≤ y / Ratpoints.rbaPack → surv[y]! = cw

theorem Ratpoints.Sieve.andRowsFillInvariant_zero {m : Nat} (cw : UInt64) (n : Nat) (surv : Vector UInt64 m) : AndRowsFillInvariant cw n [].length surv

theorem Ratpoints.Sieve.AndRowsFillInvariant.append_fillBitArray {n cur : Nat} {cw : UInt64} {done suff : List Nat} {surv : Vector UInt64 ((n + 1) * rbaPack)} (h : AndRowsFillInvariant cw n done.length surv) (hl : ForIn.toList [:n] = done ++ cur :: suff) : AndRowsFillInvariant cw n (done ++ [cur]).length (fillBitArray surv (n - 1 - cur) cw)

A step of the loop of Ratpoints.Sieve.andRows that sets the bit arrays to the class word: bit array n - 1 - cur set.

theorem Ratpoints.Sieve.AndRowsFillInvariant.andRowsLoopInvariant {m n : Nat} {cw : UInt64} {w0 : Int} {mgs : List Nat} {surv : Vector UInt64 m} (h : AndRowsFillInvariant cw n (ForIn.toList [:n]).length surv) : AndRowsLoopInvariant cw w0 n mgs [] (surv, Std.toStream mgs)

After the bit arrays are all set to the class word, the loop over the moduli starts with no moduli.

theorem Ratpoints.Sieve.AndRowsLoopInvariant.getElem!_eq {m n : Nat} {cw : UInt64} {w0 : Int} {mgs : List Nat} {pref : List SieveSpec} {st : Vector UInt64 m × List Nat} (h : AndRowsLoopInvariant cw w0 n mgs pref st) {y : Nat} (hy : y < n * rbaPack) : st.fst[y]! = andWords pref cw w0 y

theorem Ratpoints.Sieve.AndRowsLoopInvariant.next?_ne_none {m k n : Nat} {cw : UInt64} {w0 : Int} {small : Bool} {specs pref suff : List SieveSpec} {s : SieveSpec} {mgs rest : List Nat} {surv : Vector UInt64 m} (pre : StageFits specs mgs small w0 (w0 + ↑n)) (hs : specs = pref ++ s :: suff) (h : AndRowsLoopInvariant cw w0 k mgs pref (surv, rest)) : Std.Stream.next? rest ≠ none

The reciprocals do not run out before the moduli.

theorem Ratpoints.Sieve.AndRowsLoopInvariant.andRowsHeadInvariant {m n : Nat} {cw : UInt64} {w0 : Int} {small : Bool} {specs pref suff : List SieveSpec} {s : SieveSpec} {mgs rest rest' : List Nat} {mg : Nat} {surv : Vector UInt64 m} (pre : StageFits specs mgs small w0 (w0 + ↑n)) (hs : specs = pref ++ s :: suff) (h : AndRowsLoopInvariant cw w0 n mgs pref (surv, rest)) (hnext : Std.Stream.next? rest = some (mg, rest')) : AndRowsHeadInvariant small cw w0 n pref s mg [] surv

The index of the first row of the first stage, as Ratpoints.Sieve.andRows computes it with the reciprocal mg of the cursor, is the residue of -(w0 + offset) (Ratpoints.Sieve.SieveSpec.Fits.ite_modMul_modLong_eq_emod), since mg is the reciprocal of the modulus.

theorem Ratpoints.Sieve.AndRowsLoopInvariant.push {m n c : Nat} {cw : UInt64} {w0 : Int} {small : Bool} {specs pref suff : List SieveSpec} {s : SieveSpec} {mgs rest rest' : List Nat} {r mg : Nat} {surv surv' : Vector UInt64 m} (pre : StageFits specs mgs small w0 (w0 + ↑n)) (hs : specs = pref ++ s :: suff) (h : AndRowsLoopInvariant cw w0 n mgs pref (surv, rest)) (hnext : Std.Stream.next? rest = some (mg, rest')) (h' : AndRowsStartInvariant cw w0 n pref s r c surv') (hc : n ≤ c) : AndRowsLoopInvariant cw w0 n mgs (pref ++ [s]) (surv', rest')

After the bit arrays of the modulus s are all done, the cursor moves on.

theorem Ratpoints.Sieve.AndRowsStartInvariant.of_eq {m n : Nat} {cw : UInt64} {w0 : Int} {pref : List SieveSpec} {s : SieveSpec} {r c c' : Nat} {surv : Vector UInt64 m} (h : AndRowsStartInvariant cw w0 n pref s r c surv) (hc : c = c') : AndRowsStartInvariant cw w0 n pref s r c' surv

theorem Ratpoints.Sieve.AndRowsRowInvariant.add_one_andBitArray {n : Nat} {cw : UInt64} {w0 : Int} {pref : List SieveSpec} {s : SieveSpec} {c x : Nat} {surv : Vector UInt64 ((n + 1) * rbaPack)} (h : AndRowsRowInvariant cw w0 n pref s c surv) (hx : ((w0 + ↑s.offset + ↑c) % ↑s.p).toNat = x) : AndRowsRowInvariant cw w0 n pref s (c + 1) (andBitArray surv c s.row x)

One step of the loops of Ratpoints.Sieve.andRows for the modulus s: bit array c and-ed with bit array (w0 + offset + c) mod p of the row.

theorem Ratpoints.Sieve.AndRowsStartInvariant.add_append_andBitArray {n m : Nat} {cw : UInt64} {w0 : Int} {pref : List SieveSpec} {s : SieveSpec} {r c0 x : Nat} {done suff : List Nat} {cur : Nat} {surv : Vector UInt64 ((n + 1) * rbaPack)} (h : AndRowsStartInvariant cw w0 n pref s r (c0 + done.length) surv) (hl : ForIn.toList [:m] = done ++ cur :: suff) (hx : ((w0 + ↑s.offset + ↑(c0 + cur)) % ↑s.p).toNat = x) : AndRowsStartInvariant cw w0 n pref s r (c0 + (done ++ [cur]).length) (andBitArray surv (c0 + cur) s.row x)

theorem Ratpoints.Sieve.AndRowsStartInvariant.append_andBitArray_sub {n m : Nat} {cw : UInt64} {w0 : Int} {pref : List SieveSpec} {s : SieveSpec} {r : Nat} {done suff : List Nat} {cur : Nat} {surv : Vector UInt64 ((n + 1) * rbaPack)} (h : AndRowsStartInvariant cw w0 n pref s r done.length surv) (hl : ForIn.toList [:m] = done ++ cur :: suff) (hm : m ≤ r) : AndRowsStartInvariant cw w0 n pref s r (done ++ [cur]).length (andBitArray surv cur s.row (s.p - r + cur))

The loops of Ratpoints.Sieve.andRows before the first whole period: bit array cur is and-ed with bit array p - r + cur of the row, for r = -(w0 + offset) mod p.

theorem Ratpoints.Sieve.AndRowsStartInvariant.append_andBitArray_period {n mk : Nat} {cw : UInt64} {w0 : Int} {pref : List SieveSpec} {s : SieveSpec} {r : Nat} {periods suffK done suff : List Nat} {k i : Nat} {surv : Vector UInt64 ((n + 1) * rbaPack)} (h : AndRowsStartInvariant cw w0 n pref s r (r + periods.length * s.p + done.length) surv) (hlk : ForIn.toList [:mk] = periods ++ k :: suffK) (hl : ForIn.toList [:s.p] = done ++ i :: suff) : AndRowsStartInvariant cw w0 n pref s r (r + periods.length * s.p + (done ++ [i]).length) (andBitArray surv (r + k * s.p + i) s.row i)

The loop of Ratpoints.Sieve.andRows over one whole period: bit array r + k p + i is and-ed with bit array i of the row, for r = -(w0 + offset) mod p.

theorem Ratpoints.Sieve.AndRowsStartInvariant.append_andBitArray_tail {n : Nat} {cw : UInt64} {w0 : Int} {pref : List SieveSpec} {s : SieveSpec} {r : Nat} {done suff : List Nat} {i : Nat} {surv : Vector UInt64 ((n + 1) * rbaPack)} (h : AndRowsStartInvariant cw w0 n pref s r (r + (n - r) / s.p * s.p + done.length) surv) (hl : ForIn.toList [:(n - r) % s.p] = done ++ i :: suff) : AndRowsStartInvariant cw w0 n pref s r (r + (n - r) / s.p * s.p + (done ++ [i]).length) (andBitArray surv (r + (n - r) / s.p * s.p + i) s.row i)

The loop of Ratpoints.Sieve.andRows after the last whole period: bit array r + ⌊(n - r) / p⌋ p + i is and-ed with bit array i of the row, for r = -(w0 + offset) mod p.

theorem Ratpoints.Sieve.andRows_spec (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (cw : UInt64) (w0 : Int) (n : Nat) (surv : Vector UInt64 ((n + 1) * rbaPack)) : ⦃ StageFits specs mgs small w0 (w0 + ↑n) ⦄ andRows specs mgs small cw w0 n surv ⦃ fun (surv' : Vector UInt64 ((n + 1) * rbaPack)) => ∀ (y : Nat), y < n * rbaPack → surv'[y]! = andWords specs cw w0 y ⦄

Each modulus s has its row read at the offset of s (Ratpoints.Sieve.SieveSpec.wordAt): the loops over the bit arrays start at the index r of the residue of -(w0 + offset), which the reduction by the reciprocal of the cursor gives under the test small (Ratpoints.Sieve.SieveSpec.Fits.ite_modMul_modLong_eq_emod); the reciprocals run in step with the moduli and do not run out before them.

The check of a numerator and the set bits of a word

theorem Ratpoints.BruteForce.pointsOfDen_eq_flatMap_checkNum (c : List Int) (d : Nat) (b : Int) (xs : List Int) : pointsOfDen c d b xs = List.flatMap (Sieve.checkNum (scaledCoeffs c d b) (if d % 2 = 1 then b else 1) b false) xs

theorem Ratpoints.Sieve.checkNum_eq_map (w : List Int) (f b : Int) (rev : Bool) (a : Int) : checkNum w f b rev a = List.map (if rev = true then swapPoint else id) (checkNum w f b false a)

theorem Ratpoints.Sieve.flatMap_checkNum (w : List Int) (f b : Int) (rev : Bool) (xs : List Int) : List.flatMap (checkNum w f b rev) xs = List.map (if rev = true then swapPoint else id) (List.flatMap (checkNum w f b false) xs)

def Ratpoints.Sieve.WalkWordInvariant {β : Type u} (g : Nat → List β) (x0 : UInt64) (out0 : Array β) (k : Nat) (out : Array β) : Prop

The property of the array out of a walk through the set bits of the word x0, lowest first, that appends the list g t of each set bit t to the array out0, after the set bits below k: out is out0 followed by the lists of the set bits t < k of x0, in increasing order. In Ratpoints.Sieve.wordsDens, g t is the list of the denominator of bit t alone; the walk of the sieve, which delivers its points to a callback (Ratpoints.Sieve.walkWord), has an invariant of its own (Ratpoints.Sieve.WalkDeliveryInvariant).

Equations

• Ratpoints.Sieve.WalkWordInvariant g x0 out0 k out = (out.toList = out0.toList ++ List.flatMap g (List.filter (fun (x : Nat) => x0.toBitVec.getLsbD x) (List.range k)))

theorem Ratpoints.Sieve.walkWordInvariant_zero {β : Type u} (g : Nat → List β) (x0 : UInt64) (out0 : Array β) : WalkWordInvariant g x0 out0 0 out0

theorem Ratpoints.Sieve.WalkWordInvariant.append_ctz {β : Type u} {g : Nat → List β} {x0 x : UInt64} {out0 out : Array β} {k : Nat} (h : WalkWordInvariant g x0 out0 k out) (hx : ClearedBelow x0 k x) (hx0 : x ≠ 0) : WalkWordInvariant g x0 out0 (x.toBitVec.ctz.toNat + 1) (out ++ (g x.toBitVec.ctz.toNat).toArray)

theorem Ratpoints.Sieve.WalkWordInvariant.toList_eq {β : Type u} {g : Nat → List β} {x0 x : UInt64} {out0 out : Array β} (h : WalkWhileInvariant x0 (WalkWordInvariant g x0 out0) true (out, x)) : out.toList = out0.toList ++ List.flatMap g (List.filter (fun (x : Nat) => x0.toBitVec.getLsbD x) (List.range 64))