The closed form of the rows

The closed form of a row of words (Ratpoints.Sieve.closedRow): for an admission test adm, a modulus m and a residue r, the (m + chunk - 1) Ratpoints.rbaPack words whose word j has bit t set exactly when adm r admits the numerator 64 j + t. Every builder of the rows of init.c and of the generators of the headers of the build computes the closed form of its admission test (Ratpoints.Proof.PrimeRows, Ratpoints.Proof.CompositeRows), and the tables of rows of a run hold closed forms (Ratpoints.Proof.RowStore). For a test of period m the closed form repeats its first m bit arrays in the Ratpoints.chunk - 1 after them (Ratpoints.Sieve.getElem!_closedRow_mod), the copies that the chunked first stage reads (Ratpoints.Sieve.SieveSpec.Wraps). The words of a forbidden divisor (Ratpoints.Sieve.forbiddenRow) have bit t of word r clear exactly when p ∣ 64 r + t, and the row of 0 of a prime of the table (Ratpoints.Sieve.sieves0) is the closed form of the row of 0 of every table of the prime, the first p of its words those of the forbidden divisor p.

The words of a pattern in the shape in which the builders compute them: a word holding a stretch of bits of a pattern of period m (Ratpoints.Sieve.PatternBits), and the words of a row that are the windows of 64 bits of the pattern (Ratpoints.Sieve.RowWords), which give the closed form (Ratpoints.Sieve.RowWords.toArray_eq_closedRow); a word of a stretch, or-ed with another shifted left (Ratpoints.Sieve.PatternBits.or_shiftLeft), or shifted right (Ratpoints.Sieve.PatternBits.shiftRight), holds a stretch of the pattern again. The bits of a bit array of words that the C code reads with a shift and a mask (Ratpoints.Sieve.bitAt) are the bits of its words (Ratpoints.Sieve.bitAt_eq_getLsbD), set one at a time (Ratpoints.Sieve.bitAt_setBitAt).

Main definitions

• Ratpoints.Sieve.wordOfBits: the word of the bits c t, t < 64.
• Ratpoints.Sieve.closedRow: the closed form of a row.
• Ratpoints.Sieve.PatternBits, Ratpoints.Sieve.RowWords: a word holding a stretch of a periodic pattern, and the words of a row that are windows of it.

Main statements

• Ratpoints.Sieve.getLsbD_closedRow: bit t of word j of the closed form says whether the test admits 64 j + t.
• Ratpoints.Sieve.getElem!_closedRow_mod, Ratpoints.Sieve.wraps_closedRow, Ratpoints.Sieve.SieveEntry.wraps_closedRow: the closed form of a test of period m repeats its first m bit arrays.
• Ratpoints.Sieve.PatternBits.or_shiftLeft, Ratpoints.Sieve.PatternBits.shiftRight: the stretches of a pattern under an or with a shifted word and under a shift right.
• Ratpoints.Sieve.RowWords.toArray_eq_closedRow: words of a row that are the windows of a pattern are the closed form of a test that reads the pattern.
• Ratpoints.Sieve.bitAt_eq_getLsbD, Ratpoints.Sieve.bitAt_setBitAt: the bit of a bit array of words that the C code reads, and the bits after one is set.
• Ratpoints.Sieve.getLsbD_getElem!_forbiddenRow: the bits of the words of a forbidden divisor.
• Ratpoints.Sieve.sieves0_eq_closedRow, Ratpoints.Sieve.extract_sieves0: the row of 0 of a prime is the closed form of the row of 0 of its table, and its first p words are those of the forbidden divisor p.

Implementation notes

The file uses Lean core and Std only, as the contracts of the sieve do; the proofs use only that Ratpoints.rbaPack and Ratpoints.chunk are positive, never their values.

theorem Ratpoints.le_add_chunk_sub_one_mul_rbaPack (p : Nat) : p ≤ (p + chunk - 1) * rbaPack

A row of p + Ratpoints.chunk - 1 bit arrays of Ratpoints.rbaPack words has at least p words.

The closed form

def Ratpoints.Sieve.wordOfBits (c : Nat → Bool) : UInt64

The word whose bit t is c t for t < 64.

Equations

• Ratpoints.Sieve.wordOfBits c = Nat.fold 64 (fun (t : Nat) (x : t < 64) (w : UInt64) => if c t = true then w ||| 1 <<< t.toUInt64 else w) 0

theorem Ratpoints.Sieve.getLsbD_wordOfBits (c : Nat → Bool) (t : Nat) : (wordOfBits c).toBitVec.getLsbD t = (decide (t < 64) && c t)

def Ratpoints.Sieve.closedRow (adm : Nat → Int → Bool) (m r : Nat) : Array UInt64

The closed form of the row of the residue r for the admission test adm of the modulus m: m + chunk - 1 bit arrays of Ratpoints.rbaPack words, for the chunk Ratpoints.chunk, word j with bit t set exactly when adm r admits the numerator 64 j + t. With the test Ratpoints.Sieve.SieveEntry.admits of a sieve entry, or Ratpoints.Sieve.Factor.admits of a factor, this is the row that ratpoints builds for the residue, m bit arrays and the copies of the first chunk - 1 of them (Ratpoints.Sieve.getElem!_closedRow_mod).

Equations

• Ratpoints.Sieve.closedRow adm m r = Array.map (fun (j : Nat) => Ratpoints.Sieve.wordOfBits fun (t : Nat) => adm r (64 * ↑j + ↑t)) (Array.range ((m + Ratpoints.chunk - 1) * Ratpoints.rbaPack))

@[simp]

theorem Ratpoints.Sieve.size_closedRow (adm : Nat → Int → Bool) (m r : Nat) : (closedRow adm m r).size = (m + chunk - 1) * rbaPack

theorem Ratpoints.Sieve.getLsbD_closedRow (adm : Nat → Int → Bool) (m r : Nat) {j : Nat} (hj : j < (m + chunk - 1) * rbaPack) (t : Nat) : (closedRow adm m r)[j]!.toBitVec.getLsbD t = (decide (t < 64) && adm r (64 * ↑j + ↑t))

theorem Ratpoints.Sieve.eq_closedRow {adm : Nat → Int → Bool} {m r : Nat} {row : Array UInt64} (hs : row.size = (m + chunk - 1) * rbaPack) (h : ∀ (j : Nat), j < (m + chunk - 1) * rbaPack → ∀ (t : Nat), row[j]!.toBitVec.getLsbD t = (decide (t < 64) && adm r (64 * ↑j + ↑t))) : row = closedRow adm m r

An array of (m + chunk - 1) rbaPack words whose word j has bit t set exactly when adm r admits 64 j + t is the closed form.

theorem Ratpoints.Sieve.getElem!_closedRow_mod {adm : Nat → Int → Bool} {m r : Nat} (hm : 0 < m) (hadm : ∀ (a k : Int), adm r (a + ↑m * k) = adm r a) {j : Nat} (hj : j < (m + chunk - 1) * rbaPack) : (closedRow adm m r)[j]! = (closedRow adm m r)[j % (m * rbaPack)]!

The closed form of a test of period m > 0 repeats its first m bit arrays: word j is word j mod m rbaPack.

theorem Ratpoints.Sieve.wraps_closedRow {adm : Nat → Int → Bool} {s : SieveSpec} {r : Nat} (hp : 0 < s.p) (hadm : ∀ (a k : Int), adm r (a + ↑s.p * k) = adm r a) (hrow : s.row = closedRow adm s.p r) : s.Wraps

The row of a sieve spec that is the closed form of a test of period p > 0 repeats its first p bit arrays where the chunked first stage reads it.

theorem Ratpoints.Sieve.SieveEntry.wraps_closedRow (e : SieveEntry) (hp : 0 < e.p) (off st stop r : Nat) : { p := e.p, offset := off, row := closedRow e.admits e.p r, start := st, stop := stop }.Wraps

The sieve spec of the closed form of a row of the sieve entry e, of a modulus p > 0, with any offset, start and end, repeats its first bit arrays where the chunked first stage reads it.

Words of a periodic pattern

def Ratpoints.Sieve.PatternBits (g : Nat → Bool) (m s n : Nat) (x : UInt64) : Prop

The word x holds n ≤ 64 bits of the pattern g of period m from the position s on: bit t < n of x is the bit of the pattern at s + t, and the bits from n on are clear.

Equations

• Ratpoints.Sieve.PatternBits g m s n x = ∀ (t : Nat), x.toBitVec.getLsbD t = (decide (t < n) && g ((s + t) % m))

theorem Ratpoints.Sieve.PatternBits.congr_left {g : Nat → Bool} {m s s' n : Nat} {x : UInt64} (h : PatternBits g m s n x) (hs : s % m = s' % m) : PatternBits g m s' n x

theorem Ratpoints.Sieve.PatternBits.or_shiftLeft {g : Nat → Bool} {m s k n : Nat} {x y : UInt64} (hx : PatternBits g m s k x) (hy : PatternBits g m (s + k) n y) (hk : k < 64) : PatternBits g m s (min (k + n) 64) (x ||| y <<< UInt64.ofNat k)

The k < 64 bits of the pattern from s on in x, or-ed with the n bits from s + k on in y shifted left by k: the min (k + n) 64 bits from s on.

theorem Ratpoints.Sieve.PatternBits.shiftRight {g : Nat → Bool} {m s n k : Nat} {x : UInt64} (h : PatternBits g m s n x) (hk : k < 64) : PatternBits g m (s + k) (n - k) (x >>> UInt64.ofNat k)

The n bits of the pattern from s on in x, shifted right by k < 64: the n - k bits from s + k on.

def Ratpoints.Sieve.RowWords (g : Nat → Bool) (m L : Nat) {n : Nat} (si : Vector UInt64 n) : Prop

The words 0, …, L - 1 of si are the windows of the pattern g of period m: word j the 64 bits from the position 64 j on.

Equations

• Ratpoints.Sieve.RowWords g m L si = ∀ (j : Nat), j < L → Ratpoints.Sieve.PatternBits g m (64 * j) 64 si[j]!

theorem Ratpoints.Sieve.RowWords.set!_self {g : Nat → Bool} {m L n : Nat} {si : Vector UInt64 n} (h : RowWords g m L si) (hL : L < n) {x : UInt64} (hx : PatternBits g m (64 * L) 64 x) : RowWords g m (L + 1) (si.set! L x)

Setting word L < n to the window at 64 L makes one more of the words windows.

theorem Ratpoints.Sieve.RowWords.of_mod {g : Nat → Bool} {p n L : Nat} {si si' : Vector UInt64 n} (hp : 0 < p) (h : RowWords g p p si) (h' : ∀ (j : Nat), j < L → si'[j]! = si[j % p]!) : RowWords g p L si'

Words that repeat the first p words of a row, whose word j < p is the window of the pattern at 64 j, are windows of the pattern, since 64 j ≡ 64 (j mod p) (mod p).

theorem Ratpoints.Sieve.RowWords.toArray_eq_closedRow {g : Nat → Bool} {adm : Nat → Int → Bool} {m r : Nat} {si : Vector UInt64 ((m + chunk - 1) * rbaPack)} (h : RowWords g m ((m + chunk - 1) * rbaPack) si) (hg : ∀ (N : Nat), g (N % m) = adm r ↑N) : si.toArray = closedRow adm m r

Words of a row of (m + chunk - 1) rbaPack words that are the windows of the pattern g of period m are the closed form of a test adm r that reads the pattern at the residues of the numerators.

The bits of a bit array of words

theorem Ratpoints.Sieve.bitAt_eq_getLsbD (ws : Array UInt64) (x : Nat) : bitAt ws x = ws[x / 64]!.toBitVec.getLsbD (x % 64)

Bit x of a bit array of words, read with the shift and the mask of the C code, is bit x mod 64 of word ⌊x / 64⌋.

theorem Ratpoints.Sieve.size_setBitAt (ws : Array UInt64) (x : Nat) : (setBitAt ws x).size = ws.size

theorem Ratpoints.Sieve.bitAt_setBitAt {ws : Array UInt64} {x : Nat} (hx : x / 64 < ws.size) (y : Nat) : bitAt (setBitAt ws x) y = (bitAt ws y || decide (y = x))

Setting bit x of a bit array of words, x within the words, sets bit x.

The words of a forbidden divisor

theorem Ratpoints.Sieve.size_forbiddenRow (p : Nat) : (forbiddenRow p).size = p

theorem Ratpoints.Sieve.getLsbD_getElem!_forbiddenRow {p r : Nat} (hr : r < p) (t : Nat) : (forbiddenRow p)[r]!.toBitVec.getLsbD t = (decide (t < 64) && (64 * r + t) % p != 0)

Bit t of word r < p of the words of the forbidden divisor p is clear exactly when p ∣ 64 r + t, the multiples p i of p with i < 64 being cleared.

The row of 0 of a prime

theorem Ratpoints.Sieve.size_sieves0 (p : Nat) : (sieves0 p).size = (p + chunk - 1) * rbaPack

theorem Ratpoints.Sieve.getElem!_sieves0 {p x : Nat} (hx : x < (p + chunk - 1) * rbaPack) : (sieves0 p)[x]! = (forbiddenRow p)[x % p]!

Word x of the row of 0 of the prime p is word x mod p of the words of the forbidden divisor p.

theorem Ratpoints.Sieve.sieves0_eq_closedRow (e : Entry) (hp : 0 < e.p) : sieves0 e.p = closedRow e.admits e.p 0

The row of 0 of the prime p = e.p > 0 of the table is the closed form of the row of 0 of the table e of the prime, whatever its entries: bit t of word x set exactly when p ∤ 64 x + t.

theorem Ratpoints.Sieve.extract_sieves0 (p : Nat) : (sieves0 p).extract 0 p = forbiddenRow p

The first p words of the row of 0 of the prime p are the words of the forbidden divisor p.