The contracts of the builders of the rows of a prime

The contracts of the functions that the build of ratpoints generates for the primes of the table from CODE_INIT_SIEVE1 (Ratpoints.Sieve.sieveInit1, a prime below 64) and CODE_INIT_SIEVE2 (Ratpoints.Sieve.sieveInit2, a prime above 64), and of their pieces and macros, as @[spec] theorems proved with vcgen, the program logic of Lean core, with loop invariants that are named definitions: the row of the residue 0 < b < p of a prime p is the closed form of the row of b of its table (Ratpoints.Sieve.closedRow of Ratpoints.Sieve.Entry.admits), and the builder stores it into the table of rows of its entry (Ratpoints.Sieve.RowStore.publish).

The pattern of a row is computed four bits at a time by four lanes, whose residues step through the residues x d mod p for the inverse d of b (Ratpoints.Sieve.LanesAt, Ratpoints.Sieve.lanePattern); CODE_INIT_SIEVE1 doubles the pattern of p bits up to a word and rotates it through the first p words, CODE_INIT_SIEVE2 keeps it in a ring of ⌊p / 64⌋ + 1 words (Ratpoints.Sieve.RingState); both end with the copies of RP_INIT_REPLICATE.

Main definitions

• Ratpoints.Sieve.lanePattern, Ratpoints.Sieve.LanesAt: the pattern of the lanes and the lanes at a bit of it.
• Ratpoints.Sieve.RingState: the ring of the words of CODE_INIT_SIEVE2.

Main statements

• Ratpoints.Sieve.initFourDecl_lanes, Ratpoints.Sieve.initFourLoop_spec: the four lanes and the bits that they compute.
• Ratpoints.Sieve.initReplicate_spec: the copies of RP_INIT_REPLICATE.
• Ratpoints.Sieve.sieveInit1_spec, Ratpoints.Sieve.sieveInit2_spec: the rows of a prime below and above 64 are the closed forms of the rows of their tables, stored into the tables of rows of their entries.

Notation

Local to the file: diffShift p, the diff_shift of CODE_INIT_SIEVE1; wordLen p k, the number of the bits of word k of the pattern in CODE_INIT_SIEVE2; lanePatternOf t b, the pattern of the lanes of the row of the residue b of the table t.

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; every shift that the builders execute is shown to be by an amount below 64, where Lean's shifts and the C code's agree. The builders need of the prime only the inverse of b below p, and for CODE_INIT_SIEVE2 that p mod 64 ≠ 0: no primality and nothing of the table of squares.

The four lanes

def Ratpoints.Sieve.lanePattern (isfs : Array Bool) (p ab0 d N : Nat) : Bool

The pattern of the lanes from the residue ab₀ on, stepping by d modulo p: bit N is the entry of isfs at ab₀ + N d mod p. It has the period p (Ratpoints.Sieve.lanePattern_mod).

Equations

• Ratpoints.Sieve.lanePattern isfs p ab0 d N = isfs[(ab0 + N * d) % p]!

theorem Ratpoints.Sieve.lanePattern_mod (isfs : Array Bool) (p ab0 d N : Nat) : lanePattern isfs p ab0 d (N % p) = lanePattern isfs p ab0 d N

def Ratpoints.Sieve.LanesAt (p d ab0 x ab ab1 ab2 ab3 : Nat) : Prop

The four lanes at the bit x of the pattern from ab₀ on: the residues of ab₀ + (x + k) d modulo p, k < 4.

Equations

• Ratpoints.Sieve.LanesAt p d ab0 x ab ab1 ab2 ab3 = (ab = (ab0 + x * d) % p ∧ ab1 = (ab0 + (x + 1) * d) % p ∧ ab2 = (ab0 + (x + 2) * d) % p ∧ ab3 = (ab0 + (x + 3) * d) % p)

theorem Ratpoints.Sieve.ite_add_mod_eq_add_four_mul_mod {p d ab0 x : Nat} : (if p ≤ (ab0 + x * d) % p + 4 * d % p then (ab0 + x * d) % p + 4 * d % p - p else (ab0 + x * d) % p + 4 * d % p) = (ab0 + (x + 4) * d) % p

A lane stepped by d4 = 4 d mod p.

theorem Ratpoints.Sieve.initFourDecl_lanes {p d : Nat} (hd : d < p) : (initFourDecl p d).snd.snd.snd = 4 * d % p ∧ LanesAt p d 0 0 0 (initFourDecl p d).fst (initFourDecl p d).snd.fst (initFourDecl p d).snd.snd.fst

RP_INIT_FOUR_DECL puts the lanes at the bits 0, 1, 2, 3 of the pattern from 0 on, for d < p, and their step at 4 d mod p.

theorem Ratpoints.Sieve.PatternBits.or_four {isfs : Array Bool} {p d ab0 i : Nat} {w : UInt64} (h : PatternBits (lanePattern isfs p ab0 d) p 0 i w) (hi : i + 4 ≤ 64) : PatternBits (lanePattern isfs p ab0 d) p 0 (i + 4) (w ||| (isfs[(ab0 + i * d) % p]!.toUInt64 <<< UInt64.ofNat i ||| isfs[(ab0 + (i + 1) * d) % p]!.toUInt64 <<< UInt64.ofNat (i + 1) ||| isfs[(ab0 + (i + 2) * d) % p]!.toUInt64 <<< UInt64.ofNat (i + 2) ||| isfs[(ab0 + (i + 3) * d) % p]!.toUInt64 <<< UInt64.ofNat (i + 3)))

The bits i, …, i + 3 of the four lanes, or-ed into the word of the bits below i.

def Ratpoints.Sieve.FourLanes (isfs : Array Bool) (p d ab0 : Nat) (w : UInt64) (ab ab1 ab2 ab3 i : Nat) : Prop

The lanes and the word of the loop of four lanes at the bit i, for the step d of the lanes from the residue ab₀ on.

Equations

• Ratpoints.Sieve.FourLanes isfs p d ab0 w ab ab1 ab2 ab3 i = (Ratpoints.Sieve.LanesAt p d ab0 i ab ab1 ab2 ab3 ∧ Ratpoints.Sieve.PatternBits (Ratpoints.Sieve.lanePattern isfs p ab0 d) p 0 i w)

def Ratpoints.Sieve.FourInvariant (isfs : Array Bool) (p d4 ab0 ab10 ab20 ab30 hi : Nat) : Std.WP.WhileInvariant (UInt64 × Nat × Nat × Nat × Nat × Nat) Prop

The invariant of the loop of Ratpoints.Sieve.initFourLoop from the bit 0 and the word 0 on, with the lanes ab₀, ab1₀, ab2₀, ab3₀ at the start: the bit i a multiple of 4 up to hi, and for every step d of the lanes with d4 = 4 d mod p, the lanes at i and the bits below i of the pattern of the lanes in the word.

Equations

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

theorem Ratpoints.Sieve.fourInvariant_zero (isfs : Array Bool) {p d4 hi ab ab1 ab2 ab3 : Nat} {w : UInt64} {lo : Nat} (pre : w = 0 ∧ lo = 0 ∧ 0 < p ∧ hi ≤ 64) : FourInvariant isfs p d4 ab ab1 ab2 ab3 hi false (w, ab, ab1, ab2, ab3, lo)

theorem Ratpoints.Sieve.FourInvariant.add_four {isfs : Array Bool} {p d4 ab0 ab10 ab20 ab30 hi mb : Nat} {w : UInt64} {lo : Nat} {w' : UInt64} {ab ab1 ab2 ab3 i : Nat} (pre : w' = 0 ∧ lo = 0 ∧ 0 < p ∧ hi ≤ 64) (h : hi - i = mb ∧ FourInvariant isfs p d4 ab0 ab10 ab20 ab30 hi false (w, ab, ab1, ab2, ab3, i)) (hi4 : i + 4 ≤ hi) : hi - (i + 4) < mb ∧ FourInvariant isfs p d4 ab0 ab10 ab20 ab30 hi false (w ||| (isfs[ab]!.toUInt64 <<< UInt64.ofNat i ||| isfs[ab1]!.toUInt64 <<< UInt64.ofNat (i + 1) ||| isfs[ab2]!.toUInt64 <<< UInt64.ofNat (i + 2) ||| isfs[ab3]!.toUInt64 <<< UInt64.ofNat (i + 3)), if p ≤ ab + d4 then ab + d4 - p else ab + d4, if p ≤ ab1 + d4 then ab1 + d4 - p else ab1 + d4, if p ≤ ab2 + d4 then ab2 + d4 - p else ab2 + d4, if p ≤ ab3 + d4 then ab3 + d4 - p else ab3 + d4, i + 4)

A step of the loop of four lanes.

theorem Ratpoints.Sieve.FourInvariant.exit {isfs : Array Bool} {p d4 ab0 ab10 ab20 ab30 hi mb : Nat} {w : UInt64} {ab ab1 ab2 ab3 i : Nat} (h : hi - i = mb ∧ FourInvariant isfs p d4 ab0 ab10 ab20 ab30 hi false (w, ab, ab1, ab2, ab3, i)) (hi4 : ¬i + 4 ≤ hi) : FourInvariant isfs p d4 ab0 ab10 ab20 ab30 hi true (w, ab, ab1, ab2, ab3, i)

theorem Ratpoints.Sieve.FourInvariant.post {isfs : Array Bool} {p d4 ab0 ab10 ab20 ab30 hi : Nat} {w : UInt64} {ab ab1 ab2 ab3 i : Nat} (h : FourInvariant isfs p d4 ab0 ab10 ab20 ab30 hi true (w, ab, ab1, ab2, ab3, i)) : i = 4 * (hi / 4) ∧ ∀ (d : Nat), d < p → d4 = 4 * d % p → LanesAt p d ab0 0 ab0 ab10 ab20 ab30 → FourLanes isfs p d ab0 w ab ab1 ab2 ab3 (4 * (hi / 4))

theorem Ratpoints.Sieve.initFourLoop_spec (isfs : Array Bool) (p d4 : Nat) (w : UInt64) (lo hi ab ab1 ab2 ab3 : Nat) : ⦃ w = 0 ∧ lo = 0 ∧ 0 < p ∧ hi ≤ 64 ⦄ initFourLoop isfs p d4 w lo hi ab ab1 ab2 ab3 ⦃ fun (r : UInt64 × Nat × Nat × Nat × Nat × Nat) => r.snd.fst = 4 * (hi / 4) ∧ ∀ (d : Nat), d < p → d4 = 4 * d % p → LanesAt p d ab 0 ab ab1 ab2 ab3 → FourLanes isfs p d ab r.fst r.snd.snd.fst r.snd.snd.snd.fst r.snd.snd.snd.snd.fst r.snd.snd.snd.snd.snd (4 * (hi / 4)) ⦄

The loop of four lanes from the bit 0 and the word 0 on, as its callers start it, ends at the bit 4 ⌊hi / 4⌋ with the bits below it of the pattern of the lanes in the word and the lanes at that bit, for every step d < p of the lanes with d4 = 4 d mod p.

The bits left over

def Ratpoints.Sieve.RestInvariant (isfs : Array Bool) (p d ab0 lo c : Nat) (st : UInt64 × Nat) : Prop

The state of a loop that sets the bits from lo on one at a time from the first lane, after c of them: the word holds the bits of the pattern of the lanes from ab₀ on below lo + c, and the lane is at the bit lo + c.

Equations

• Ratpoints.Sieve.RestInvariant isfs p d ab0 lo c st = (Ratpoints.Sieve.PatternBits (Ratpoints.Sieve.lanePattern isfs p ab0 d) p 0 (lo + c) st.fst ∧ st.snd = (ab0 + (lo + c) * d) % p)

theorem Ratpoints.Sieve.RestInvariant.append_initBit {isfs : Array Bool} {p d ab0 lo hi cur : Nat} {pref suff : List Nat} {w : UInt64} {ab : Nat} (pre : 0 < p ∧ hi ≤ 64 ∧ d < p) (hl : ForIn.toList [lo:hi] = pref ++ cur :: suff) (h : RestInvariant isfs p d ab0 lo pref.length (w, ab)) : RestInvariant isfs p d ab0 lo (pref ++ [cur]).length (initBit w isfs[ab]! cur, if p ≤ ab + d then ab + d - p else ab + d)

A bit set from the first lane, RP_INIT_BIT, and the lane stepped by d.

theorem Ratpoints.Sieve.RestInvariant.post {isfs : Array Bool} {p d ab0 lo hi : Nat} {st : UInt64 × Nat} (hlo : lo ≤ hi) (h : RestInvariant isfs p d ab0 lo (ForIn.toList [lo:hi]).length st) : PatternBits (lanePattern isfs p ab0 d) p 0 hi st.fst ∧ st.snd = (ab0 + hi * d) % p

The loop of the bits left over from lo ≤ hi on ends with the bits below hi.

theorem Ratpoints.Sieve.restInvariant_init {isfs : Array Bool} {p d ab0 i : Nat} {w : UInt64} {ab ab1 ab2 ab3 : Nat} (h : FourLanes isfs p d ab0 w ab ab1 ab2 ab3 i) : RestInvariant isfs p d ab0 i [].length (w, ab)

The start of the loop of the bits left over, after the loop of four lanes.

The rows of a prime below 64

theorem Ratpoints.Sieve.sieve1Pattern_rest_init {t : Entry} {b : Nat} {r : UInt64 × Nat × Nat × Nat × Nat × Nat} (pre : 0 < t.p ∧ t.p ≤ 64 ∧ t.inverses[b]! < t.p) (h : r.snd.fst = 4 * (t.p / 4) ∧ ∀ (d : Nat), d < t.p → (initFourDecl t.p t.inverses[b]!).snd.snd.snd = 4 * d % t.p → LanesAt t.p d 0 0 0 (initFourDecl t.p t.inverses[b]!).fst (initFourDecl t.p t.inverses[b]!).snd.fst (initFourDecl t.p t.inverses[b]!).snd.snd.fst → FourLanes t.isFSquare t.p d 0 r.fst r.snd.snd.fst r.snd.snd.snd.fst r.snd.snd.snd.snd.fst r.snd.snd.snd.snd.snd (4 * (t.p / 4))) : RestInvariant t.isFSquare t.p t.inverses[b]! 0 r.snd.fst [].length (r.fst, r.snd.snd.fst)

theorem Ratpoints.Sieve.sieve1Pattern_rest_post {t : Entry} {b : Nat} {r : UInt64 × Nat × Nat × Nat × Nat × Nat} {st : UInt64 × Nat} (hr : r.snd.fst = 4 * (t.p / 4) ∧ ∀ (d : Nat), d < t.p → (initFourDecl t.p t.inverses[b]!).snd.snd.snd = 4 * d % t.p → LanesAt t.p d 0 0 0 (initFourDecl t.p t.inverses[b]!).fst (initFourDecl t.p t.inverses[b]!).snd.fst (initFourDecl t.p t.inverses[b]!).snd.snd.fst → FourLanes t.isFSquare t.p d 0 r.fst r.snd.snd.fst r.snd.snd.snd.fst r.snd.snd.snd.snd.fst r.snd.snd.snd.snd.snd (4 * (t.p / 4))) (h : RestInvariant t.isFSquare t.p t.inverses[b]! 0 r.snd.fst (ForIn.toList [r.snd.fst:t.p]).length st) : PatternBits (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p 0 t.p st.fst

theorem Ratpoints.Sieve.sieve1Pattern_spec (t : Entry) (b : Nat) : ⦃ 0 < t.p ∧ t.p ≤ 64 ∧ t.inverses[b]! < t.p ⦄ sieve1Pattern t b ⦃ fun (w : UInt64) => PatternBits (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p 0 t.p w ⦄

The pattern of the row of the residue b of the prime p = t.p ≤ 64 with the inverse d < p of b: bit a < p is the entry of the table at a d mod p, the higher bits clear.

The copies of RP_INIT_REPLICATE

def Ratpoints.Sieve.RepInvariant {n : Nat} (p : Nat) (si : Vector UInt64 n) (a c : Nat) (si' : Vector UInt64 n) : Prop

The invariant of the loops of the copies of Ratpoints.Sieve.initReplicate through the first p bit arrays, with the residues below a done and of residue a the copies up to a + c p: the words below p and those done are the words of si below p that they repeat.

Equations

• Ratpoints.Sieve.RepInvariant p si a c si' = ∀ (j : Nat), j < p * Ratpoints.rbaPack → j < p ∨ j % p < a ∨ j % p = a ∧ j / p ≤ c → si'[j]! = si[j % p]!

def Ratpoints.Sieve.CopyInvariant {n : Nat} (p : Nat) (si : Vector UInt64 n) (c : Nat) (si' : Vector UInt64 n) : Prop

The invariant of the loop of the copies of the first bit arrays after the first p, after c of them: the words below p rbaPack + c repeat the words of si below p.

Equations

• Ratpoints.Sieve.CopyInvariant p si c si' = ∀ (j : Nat), j < p * Ratpoints.rbaPack + c → si'[j]! = si[j % p]!

theorem Ratpoints.Sieve.repInvariant_zero {n : Nat} (p : Nat) (si : Vector UInt64 n) : RepInvariant p si [].length 0 si

theorem Ratpoints.Sieve.RepInvariant.of_eq {n p a c a' c' : Nat} {si si' : Vector UInt64 n} (h : RepInvariant p si a c si') (ha : a = a') (hc : c = c') : RepInvariant p si a' c' si'

theorem Ratpoints.Sieve.RepInvariant.next {n p a : Nat} {si si' : Vector UInt64 n} (h : RepInvariant p si a (ForIn.toList [1:rbaPack]).length si') : RepInvariant p si (a + 1) 0 si'

The copies of residue a all done: the residues below a + 1 are done.

theorem Ratpoints.Sieve.RepInvariant.set! {n p a c : Nat} {si si' : Vector UInt64 n} (ha : a < p) (hn : p * rbaPack ≤ n) (h : RepInvariant p si a c si') (hk : c + 1 < rbaPack) : RepInvariant p si a (c + 1) (si'.set! (a + (c + 1) * p) si'[a]!)

A copy of word a to word a + k p, 1 ≤ k < rbaPack, after the copies up to a + (k - 1) p.

theorem Ratpoints.Sieve.RepInvariant.append {p n a cur : Nat} {pref' suff' pref suff : List Nat} {si si' : Vector UInt64 n} (pre : 0 < p ∧ n = (p + chunk - 1) * rbaPack) (hl' : ForIn.toList [:p] = pref' ++ a :: suff') (hl : ForIn.toList [1:rbaPack] = pref ++ cur :: suff) (h : RepInvariant p si a pref.length si') : RepInvariant p si a (pref ++ [cur]).length (si'.set! (a + cur * p) si'[a]!)

The step of the loop of the copies of a residue, in the shape of the verification condition.

theorem Ratpoints.Sieve.RepInvariant.append_of_next {n p cur : Nat} {pref suff : List Nat} {si si' : Vector UInt64 n} (hl : ForIn.toList [:p] = pref ++ cur :: suff) (h : RepInvariant p si cur (ForIn.toList [1:rbaPack]).length si') : RepInvariant p si (pref ++ [cur]).length 0 si'

theorem Ratpoints.Sieve.RepInvariant.copyInvariant {n p : Nat} {si si' : Vector UInt64 n} (pre : 0 < p ∧ n = (p + chunk - 1) * rbaPack) (h : RepInvariant p si (ForIn.toList [:p]).length 0 si') : CopyInvariant p si 0 si'

theorem Ratpoints.Sieve.CopyInvariant.append {p n cur : Nat} {pref suff : List Nat} {si si' : Vector UInt64 n} (pre : 0 < p ∧ n = (p + chunk - 1) * rbaPack) (hl : ForIn.toList [:(chunk - 1) * rbaPack] = pref ++ cur :: suff) (h : CopyInvariant p si pref.length si') : CopyInvariant p si (pref ++ [cur]).length (si'.set! (p * rbaPack + cur) si'[cur]!)

A copy of word k to word p rbaPack + k, in the shape of the verification condition.

theorem Ratpoints.Sieve.CopyInvariant.post {p n : Nat} {si si' : Vector UInt64 n} (pre : 0 < p ∧ n = (p + chunk - 1) * rbaPack) (h : CopyInvariant p si (ForIn.toList [:(chunk - 1) * rbaPack]).length si') {j : Nat} (hj : j < n) : si'[j]! = si[j % p]!

theorem Ratpoints.Sieve.initReplicate_spec {n : Nat} (p : Nat) (si : Vector UInt64 n) : ⦃ 0 < p ∧ n = (p + chunk - 1) * rbaPack ⦄ initReplicate p si ⦃ fun (si' : Vector UInt64 n) => ∀ (j : Nat), j < n → si'[j]! = si[j % p]! ⦄

After the copies, word j of the row is word j mod p of the row before, for every j below the size (p + chunk - 1) rbaPack of the row.

CODE_INIT_SIEVE1

theorem Ratpoints.Sieve.sieve1_shifts (p : Nat) : p < 64 → 0 < p → 64 + (64 / p + 1) * p % 64 = (64 / p + 1) * p ∧ (64 / p + 1) * p % 64 + 64 % p = p ∧ 0 < (64 / p + 1) * p % 64 ∧ (64 / p + 1) * p % 64 < 64

The shifts of CODE_INIT_SIEVE1 for 0 < p < 64: diff_shift = (⌊64 / p⌋ + 1) p mod 64 and 64 mod p add up to p, 64 + diff_shift is the multiple (⌊64 / p⌋ + 1) p of p, and 0 < diff_shift < 64, so that every shift of the rotation is by an amount below 64.

theorem Ratpoints.Sieve.PatternBits.rotate {g : Nat → Bool} {p s ds k : Nat} {x0 x1 : UInt64} (hk : 64 + ds = k * p) (hds0 : 0 < ds) (hds : ds < 64) (h0 : PatternBits g p s 64 x0) (h1 : PatternBits g p (s + 64) ds x1) : PatternBits g p (s + 64) 64 (x1 ||| x0 <<< UInt64.ofNat ds) ∧ PatternBits g p (s + 64 + 64) ds (x0 >>> UInt64.ofNat (64 - ds))

The rotation of CODE_INIT_SIEVE1: from the window at s in x0 and the next ds bits in x1, for 64 + ds ≡ 0 (mod p), the window at s + 64 and the ds bits after it.

def Ratpoints.Sieve.RotInvariant (g : Nat → Bool) (p ds c : Nat) {n : Nat} (st : UInt64 × UInt64 × Vector UInt64 n) : Prop

The invariant of the loop of the rotation of Ratpoints.Sieve.sieve1Rows after the words below c + 1: help0 the window at 64 c, help1 the next ds bits, and the words below c + 1 the windows of the pattern.

Equations

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

theorem Ratpoints.Sieve.rotInvariant_init {p : Nat} {help0 help1 : UInt64} (pre : 0 < p ∧ p < 64) (g : Nat → Bool) (h0 : PatternBits g p 0 64 help0) (h1 : PatternBits g p 64 ((64 / p + 1) * p % 64) help1) : RotInvariant g p ((64 / p + 1) * p % 64) [].length (help0, help1, (Vector.replicate ((p + chunk - 1) * rbaPack) 0).set! 0 help0)

theorem Ratpoints.Sieve.RotInvariant.append {p cur : Nat} {pref suff : List Nat} {help0 help1 x0 x1 : UInt64} {si : Vector UInt64 ((p + chunk - 1) * rbaPack)} (pre : 0 < p ∧ p < 64) (hl : ForIn.toList [1:p] = pref ++ cur :: suff) (h : ∀ (g : Nat → Bool), PatternBits g p 0 64 help0 → PatternBits g p 64 ((64 / p + 1) * p % 64) help1 → RotInvariant g p ((64 / p + 1) * p % 64) pref.length (x0, x1, si)) (g : Nat → Bool) : PatternBits g p 0 64 help0 → PatternBits g p 64 ((64 / p + 1) * p % 64) help1 → RotInvariant g p ((64 / p + 1) * p % 64) (pref ++ [cur]).length (x1 ||| x0 <<< UInt64.ofNat ((64 / p + 1) * p % 64), x0 >>> UInt64.ofNat (64 - (64 / p + 1) * p % 64), si.set! cur (x1 ||| x0 <<< UInt64.ofNat ((64 / p + 1) * p % 64)))

A step of the rotation: word c + 1 of the row the window at 64 (c + 1).

theorem Ratpoints.Sieve.RotInvariant.post {p : Nat} {help0 help1 : UInt64} {st : UInt64 × UInt64 × Vector UInt64 ((p + chunk - 1) * rbaPack)} (pre : 0 < p ∧ p < 64) (h : ∀ (g : Nat → Bool), PatternBits g p 0 64 help0 → PatternBits g p 64 ((64 / p + 1) * p % 64) help1 → RotInvariant g p ((64 / p + 1) * p % 64) (ForIn.toList [1:p]).length st) (g : Nat → Bool) (h0 : PatternBits g p 0 64 help0) (h1 : PatternBits g p 64 ((64 / p + 1) * p % 64) help1) : RowWords g p p st.snd.snd

theorem Ratpoints.Sieve.sieve1Rows_spec (p : Nat) (help0 help1 : UInt64) : ⦃ 0 < p ∧ p < 64 ⦄ sieve1Rows p help0 help1 ⦃ fun (si : Vector UInt64 ((p + chunk - 1) * rbaPack)) => ∀ (g : Nat → Bool), PatternBits g p 0 64 help0 → PatternBits g p 64 ((64 / p + 1) * p % 64) help1 → RowWords g p p si ⦄

The first p words of the row of a prime p < 64: for every pattern g of period p whose window at 0 is help0 and whose diff_shift bits after it are help1, word a < p is the window of g at 64 a.

theorem Ratpoints.Sieve.PatternBits.or_shiftLeft_self {g : Nat → Bool} {p i : Nat} {x : UInt64} (hpi : p ∣ i) (hi : i < 64) (h : PatternBits g p 0 i x) : PatternBits g p 0 (min (2 * i) 64) (x ||| x <<< UInt64.ofNat i)

One doubling x | x << i of the pattern of period p ∣ i in the bits below i < 64.

def Ratpoints.Sieve.PatternDoubleInvariant (g : Nat → Bool) (p : Nat) : Std.WP.WhileInvariant (UInt64 × Nat) Prop

The invariant of the loop of Ratpoints.Sieve.sieveInit1 that doubles the pattern of period p through the word, on the word and the shift.

Equations

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

theorem Ratpoints.Sieve.patternDoubleInvariant_init {g : Nat → Bool} {p : Nat} {x : UInt64} (hp : 0 < p) (h64 : p < 64) (h : PatternBits g p 0 p x) : PatternDoubleInvariant g p false (x, p)

theorem Ratpoints.Sieve.PatternDoubleInvariant.or_shiftLeft {g : Nat → Bool} {p i mb : Nat} {x : UInt64} (h : 64 - i = mb ∧ PatternDoubleInvariant g p false (x, i)) (hi : i < 64) : 64 - i <<< 1 < mb ∧ PatternDoubleInvariant g p false (x ||| x <<< UInt64.ofNat i, i <<< 1)

theorem Ratpoints.Sieve.PatternDoubleInvariant.exit {g : Nat → Bool} {p i mb : Nat} {x : UInt64} (h : 64 - i = mb ∧ PatternDoubleInvariant g p false (x, i)) (hi : ¬i < 64) : PatternDoubleInvariant g p true (x, i)

theorem Ratpoints.Sieve.lanePattern_mod_eq_admits {t : Entry} {b : Nat} (hb0 : 0 < b) (hbp : b < t.p) (N : Nat) : lanePattern t.isFSquare t.p 0 t.inverses[b]! (N % t.p) = t.admits b ↑N

The pattern of the lanes from 0 on with the inverse of 0 < b < p, read at the residue of a numerator, is the row of the residue b of the table.

theorem Ratpoints.Sieve.toArray_eq_closedRow_of_rowWords {t : Entry} {b : Nat} {ref : EntryRef} {store : RowStore} {si si' : Vector UInt64 ((t.p + chunk - 1) * rbaPack)} (hb0 : 0 < b) (hbp : b < t.p) (hrows : RowWords (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p t.p si) (hrep : ∀ (j : Nat), j < (t.p + chunk - 1) * rbaPack → si'[j]! = si[j % t.p]!) : (si', store.publish ref b si'.toArray).fst.toArray = closedRow t.admits t.p b ∧ (si', store.publish ref b si'.toArray).snd = store.publish ref b (closedRow t.admits t.p b)

The row of words whose first p words are the windows of the pattern of the lanes, copied through all the words, is the closed form of the row of 0 < b < p, and so is what the builder stores.

theorem Ratpoints.Sieve.doubleInvariant_init_of_pre {t : Entry} {b : Nat} {x : UInt64} (pre : 0 < b ∧ b < t.p ∧ t.p < 64 ∧ t.inverses[b]! < t.p) (h : PatternBits (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p 0 t.p x) : PatternDoubleInvariant (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p false (x, t.p)

theorem Ratpoints.Sieve.PatternBits.shiftRight_mod {g : Nat → Bool} {p : Nat} {x : UInt64} (hp : 0 < p) (h64 : p < 64) (h : PatternBits g p 0 p x) : PatternBits g p 64 ((64 / p + 1) * p % 64) (x >>> UInt64.ofNat (64 % p))

The pattern shifted right by 64 mod p holds the diff_shift bits after the window at 0.

theorem Ratpoints.Sieve.sieveInit1_post {t : Entry} {ref : EntryRef} {b : Nat} {store : RowStore} {x h0 : UInt64} {i : Nat} {si si' : Vector UInt64 ((t.p + chunk - 1) * rbaPack)} (pre : 0 < b ∧ b < t.p ∧ t.p < 64 ∧ t.inverses[b]! < t.p) (hx : PatternBits (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p 0 t.p x) (hd : PatternDoubleInvariant (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p true (h0, i)) (hrows : ∀ (g : Nat → Bool), PatternBits g t.p 0 64 h0 → PatternBits g t.p 64 ((64 / t.p + 1) * t.p % 64) (x >>> UInt64.ofNat (64 % t.p)) → RowWords g t.p t.p si) (hrep : ∀ (j : Nat), j < (t.p + chunk - 1) * rbaPack → si'[j]! = si[j % t.p]!) : (si', store.publish ref b si'.toArray).fst.toArray = closedRow t.admits t.p b ∧ (si', store.publish ref b si'.toArray).snd = store.publish ref b (closedRow t.admits t.p b)

theorem Ratpoints.Sieve.sieveInit1_spec (t : Entry) (ref : EntryRef) (b : Nat) (store : RowStore) : ⦃ 0 < b ∧ b < t.p ∧ t.p < 64 ∧ t.inverses[b]! < t.p ⦄ sieveInit1 t ref b store ⦃ fun (r : Vector UInt64 ((t.p + chunk - 1) * rbaPack) × RowStore) => r.fst.toArray = closedRow t.admits t.p b ∧ r.snd = store.publish ref b (closedRow t.admits t.p b) ⦄

The row of the residue 0 < b < p of a prime p < 64 by CODE_INIT_SIEVE1 is the closed form of the row of b of its table, for the inverse of b below p, and the builder stores it into the table of rows of the entry ref.

CODE_INIT_SIEVE2

theorem Ratpoints.Sieve.LanesAt.rebase {p d x ab ab1 ab2 ab3 : Nat} (h : LanesAt p d 0 x ab ab1 ab2 ab3) : LanesAt p d ab 0 ab ab1 ab2 ab3

The lanes at the bit x of the pattern from 0 on are at the bit 0 of the pattern from their first residue on.

theorem Ratpoints.Sieve.LanesAt.unbase {p d x y ab a0 a1 a2 a3 : Nat} (hab : ab = (0 + x * d) % p) (h : LanesAt p d ab y a0 a1 a2 a3) : LanesAt p d 0 (x + y) a0 a1 a2 a3

The lanes at the bit y of the pattern from the residue x d mod p on are at the bit x + y of the pattern from 0 on.

theorem Ratpoints.Sieve.PatternBits.unbase {isfs : Array Bool} {p d x m ab : Nat} {w : UInt64} (hab : ab = (0 + x * d) % p) (h : PatternBits (lanePattern isfs p ab d) p 0 m w) : PatternBits (lanePattern isfs p 0 d) p x m w

The pattern of the lanes from the residue x d mod p on is the pattern from 0 on at x.

theorem Ratpoints.Sieve.sieve2Word_rest_init {t : Entry} {d d4 n ab ab1 ab2 ab3 : Nat} {r : UInt64 × Nat × Nat × Nat × Nat × Nat} (pre : (0 < t.p ∧ d < t.p ∧ d4 = 4 * d % t.p) ∧ LanesAt t.p d 0 (64 * n) ab ab1 ab2 ab3) (h : r.snd.fst = 4 * ((if n < t.p / 64 then 64 else t.p % 64) / 4) ∧ ∀ (d' : Nat), d' < t.p → d4 = 4 * d' % t.p → LanesAt t.p d' ab 0 ab ab1 ab2 ab3 → FourLanes t.isFSquare t.p d' ab r.fst r.snd.snd.fst r.snd.snd.snd.fst r.snd.snd.snd.snd.fst r.snd.snd.snd.snd.snd (4 * ((if n < t.p / 64 then 64 else t.p % 64) / 4))) : RestInvariant t.isFSquare t.p d ab r.snd.fst [].length (r.fst, r.snd.snd.fst)

theorem Ratpoints.Sieve.sieve2Word_post {t : Entry} {d d4 n ab ab1 ab2 ab3 : Nat} {r : UInt64 × Nat × Nat × Nat × Nat × Nat} {st : UInt64 × Nat} (pre : (0 < t.p ∧ d < t.p ∧ d4 = 4 * d % t.p) ∧ LanesAt t.p d 0 (64 * n) ab ab1 ab2 ab3) (hr : r.snd.fst = 4 * ((if n < t.p / 64 then 64 else t.p % 64) / 4) ∧ ∀ (d' : Nat), d' < t.p → d4 = 4 * d' % t.p → LanesAt t.p d' ab 0 ab ab1 ab2 ab3 → FourLanes t.isFSquare t.p d' ab r.fst r.snd.snd.fst r.snd.snd.snd.fst r.snd.snd.snd.snd.fst r.snd.snd.snd.snd.snd (4 * ((if n < t.p / 64 then 64 else t.p % 64) / 4))) (h : RestInvariant t.isFSquare t.p d ab r.snd.fst (ForIn.toList [r.snd.fst:if n < t.p / 64 then 64 else t.p % 64]).length st) : PatternBits (lanePattern t.isFSquare t.p 0 d) t.p (64 * n) (if n < t.p / 64 then 64 else t.p % 64) st.fst ∧ ((if n < t.p / 64 then 64 else t.p % 64) % 4 = 0 → LanesAt t.p d 0 (64 * n + if n < t.p / 64 then 64 else t.p % 64) st.snd r.snd.snd.snd.fst r.snd.snd.snd.snd.fst r.snd.snd.snd.snd.snd)

The word n of the pattern of the row and the lanes after it.

theorem Ratpoints.Sieve.sieve2Word_spec (t : Entry) (d d4 n ab ab1 ab2 ab3 : Nat) : ⦃ (0 < t.p ∧ d < t.p ∧ d4 = 4 * d % t.p) ∧ LanesAt t.p d 0 (64 * n) ab ab1 ab2 ab3 ⦄ sieve2Word t d d4 n ab ab1 ab2 ab3 ⦃ fun (r : UInt64 × Nat × Nat × Nat × Nat) => PatternBits (lanePattern t.isFSquare t.p 0 d) t.p (64 * n) (if n < t.p / 64 then 64 else t.p % 64) r.fst ∧ ((if n < t.p / 64 then 64 else t.p % 64) % 4 = 0 → LanesAt t.p d 0 (64 * n + if n < t.p / 64 then 64 else t.p % 64) r.snd.fst r.snd.snd.fst r.snd.snd.snd.fst r.snd.snd.snd.snd) ⦄

Word n of the pattern of the row of a prime p in CODE_INIT_SIEVE2, from the lanes at the bit 64 n of the pattern from 0 on: the bits 64 n, … of the pattern, 64 of them for n < ⌊p / 64⌋ and p mod 64 for the last word, and after a whole word the lanes at the next.

def Ratpoints.Sieve.PatternWords (g : Nat → Bool) (p : Nat) {n : Nat} (help : Vector UInt64 n) : Prop

The words help[k], k ≤ ⌊p / 64⌋, hold the pattern g of period p: word k the bits 64 k, …, 64 of them for k < ⌊p / 64⌋ and p mod 64 for the last.

Equations

• Ratpoints.Sieve.PatternWords g p help = ∀ (k : Nat), k < p / 64 + 1 → Ratpoints.Sieve.PatternBits g p (64 * k) (if k < p / 64 then 64 else p % 64) help[k]!

def Ratpoints.Sieve.PatInvariant (g : Nat → Bool) (p d wp ds c : Nat) {n : Nat} (st : Vector UInt64 n × Nat × Nat × Nat × Nat) : Prop

The invariant of the loop of Ratpoints.Sieve.sieve2Pattern over the words of the pattern after the words below c: word k < c holds the bits 64 k, … of the pattern, 64 of them for k < wp and ds for k = wp, and the four lanes are at the bit 64 c.

Equations

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

theorem Ratpoints.Sieve.patInvariant_init {t : Entry} {b n : Nat} (help : Vector UInt64 n) (pre : 0 < t.p ∧ t.inverses[b]! < t.p) : PatInvariant (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p t.inverses[b]! (t.p / 64) (t.p % 64) [].length (help, 0, (initFourDecl t.p t.inverses[b]!).fst, (initFourDecl t.p t.inverses[b]!).snd.fst, (initFourDecl t.p t.inverses[b]!).snd.snd.fst)

theorem Ratpoints.Sieve.PatInvariant.pre {t : Entry} {b n cur : Nat} {pref suff : List Nat} {st : Vector UInt64 n × Nat × Nat × Nat × Nat} (pre : 0 < t.p ∧ t.inverses[b]! < t.p) (hl : ForIn.toList [:t.p / 64 + 1] = pref ++ cur :: suff) (h : PatInvariant (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p t.inverses[b]! (t.p / 64) (t.p % 64) pref.length st) : (0 < t.p ∧ t.inverses[b]! < t.p ∧ (initFourDecl t.p t.inverses[b]!).snd.snd.snd = 4 * t.inverses[b]! % t.p) ∧ LanesAt t.p t.inverses[b]! 0 (64 * cur) st.snd.fst st.snd.snd.fst st.snd.snd.snd.fst st.snd.snd.snd.snd

The precondition of the word cur of the pattern.

theorem Ratpoints.Sieve.PatInvariant.set! {t : Entry} {b n cur : Nat} {pref suff : List Nat} {st : Vector UInt64 n × Nat × Nat × Nat × Nat} {r : UInt64 × Nat × Nat × Nat × Nat} (hn : t.p / 64 + 1 ≤ n) (hl : ForIn.toList [:t.p / 64 + 1] = pref ++ cur :: suff) (h : PatInvariant (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p t.inverses[b]! (t.p / 64) (t.p % 64) pref.length st) (hw : PatternBits (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p (64 * cur) (if cur < t.p / 64 then 64 else t.p % 64) r.fst ∧ ((if cur < t.p / 64 then 64 else t.p % 64) % 4 = 0 → LanesAt t.p t.inverses[b]! 0 (64 * cur + if cur < t.p / 64 then 64 else t.p % 64) r.snd.fst r.snd.snd.fst r.snd.snd.snd.fst r.snd.snd.snd.snd)) : PatInvariant (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p t.inverses[b]! (t.p / 64) (t.p % 64) (pref ++ [cur]).length (st.fst.set! cur r.fst, r.snd.fst, r.snd.snd.fst, r.snd.snd.snd.fst, r.snd.snd.snd.snd)

A step of the loop of the pattern: word cur of help set to the word of the pattern.

theorem Ratpoints.Sieve.PatInvariant.post {g : Nat → Bool} {p d n : Nat} {st : Vector UInt64 n × Nat × Nat × Nat × Nat} (h : PatInvariant g p d (p / 64) (p % 64) (ForIn.toList [:p / 64 + 1]).length st) : PatternWords g p st.fst

theorem Ratpoints.Sieve.sieve2Pattern_spec (t : Entry) (b : Nat) (help : Vector UInt64 (t.p / 64 + 2)) : ⦃ 0 < t.p ∧ t.inverses[b]! < t.p ⦄ sieve2Pattern t b help ⦃ fun (help' : Vector UInt64 (t.p / 64 + 2)) => PatternWords (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p help' ⦄

The pattern of the row of the residue b of a prime p in CODE_INIT_SIEVE2, for the inverse d < p of b: word k ≤ ⌊p / 64⌋ of help holds the bits 64 k, … of the pattern of the lanes from 0 on, 64 of them for k < ⌊p / 64⌋ and p mod 64 for the last.

def Ratpoints.Sieve.RingState (g : Nat → Bool) (p wp ds s a1 : Nat) {n : Nat} (help : Vector UInt64 n) : Prop

The ring of CODE_INIT_SIEVE2 at the bit s of the pattern with the cursor a1 ≤ wp: word a1 holds the ds bits from s on, and word (a1 + 1 + k) mod (wp + 1) the 64 bits from s + ds + 64 k on, for k < wp.

Equations

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

theorem Ratpoints.Sieve.RingState.out {g : Nat → Bool} {p wp ds s a1 n : Nat} {help : Vector UInt64 n} (h : RingState g p wp ds s a1 help) (hwp : 0 < wp) (hds : ds < 64) : PatternBits g p s 64 (help[a1]! ||| help[if a1 = wp then 0 else a1 + 1]! <<< UInt64.ofNat ds)

The word that a step of the ring writes: the 64 bits from s on.

theorem Ratpoints.Sieve.RingState.cur {g : Nat → Bool} {p wp ds s a1 n t : Nat} {help : Vector UInt64 n} (h : RingState g p wp ds s a1 help) (hwp : 0 < wp) (hds0 : 0 < ds) (hds : ds < 64) (hn : wp < n) (ht : t = (a1 + 1) % (wp + 1)) (hta : a1 ≠ t) (htle : t ≤ wp) (x : UInt64) : PatternBits g p (s + 64) ds ((help.set! a1 x).set! t ((help.set! a1 x)[t]! >>> UInt64.ofNat (64 - ds)))[t]!

After a step of the ring, the word at the new cursor t, shifted right by 64 - ds, holds the ds bits from s + 64 on.

theorem Ratpoints.Sieve.RingState.rest {g : Nat → Bool} {p wp ds s a1 n t : Nat} {help : Vector UInt64 n} {x : UInt64} (h : RingState g p wp ds s a1 help) (hp : p = 64 * wp + ds) (hn : wp < n) (ht : t = (a1 + 1) % (wp + 1)) (hta : a1 ≠ t) (hout : PatternBits g p s 64 x) (k : Nat) : k < wp → PatternBits g p (s + 64 + ds + 64 * k) 64 ((help.set! a1 x).set! t ((help.set! a1 x)[t]! >>> UInt64.ofNat (64 - ds)))[(t + 1 + k) % (wp + 1)]!

After a step of the ring, the words after the new cursor hold the 64 bits from s + 64 + ds + 64 k on: the words of the ring before the step moved up by one, the last the word written.

theorem Ratpoints.Sieve.RingState.rotate {g : Nat → Bool} {p wp ds s a1 n : Nat} {help : Vector UInt64 n} (h : RingState g p wp ds s a1 help) (hp : p = 64 * wp + ds) (hwp : 0 < wp) (hds0 : 0 < ds) (hds : ds < 64) (hn : wp < n) : RingState g p wp ds (s + 64) (if a1 = wp then 0 else a1 + 1) ((help.set! a1 (help[a1]! ||| help[if a1 = wp then 0 else a1 + 1]! <<< UInt64.ofNat ds)).set! (if a1 = wp then 0 else a1 + 1) ((help.set! a1 (help[a1]! ||| help[if a1 = wp then 0 else a1 + 1]! <<< UInt64.ofNat ds))[if a1 = wp then 0 else a1 + 1]! >>> UInt64.ofNat (64 - ds)))

A step of the ring: help[a1] |= help[t] << ds, the cursor moved on to t, and help[t] >>= 64 - ds, for p = 64 wp + ds, 0 < wp, 0 < ds < 64: the ring at s + 64.

theorem Ratpoints.Sieve.sieve2_shifts {p : Nat} (pre : 64 ≤ p ∧ p % 64 ≠ 0) : p = 64 * (p / 64) + p % 64 ∧ 0 < p / 64 ∧ 0 < p % 64 ∧ p % 64 < 64

The shifts of CODE_INIT_SIEVE2 for 64 ≤ p with p mod 64 ≠ 0.

theorem Ratpoints.Sieve.RowWords.copy {p cur m : Nat} {pref suff : List Nat} {si : Vector UInt64 ((p + chunk - 1) * rbaPack)} {help : Vector UInt64 m} (pre : 64 ≤ p ∧ p % 64 ≠ 0) (hl : ForIn.toList [:p / 64] = pref ++ cur :: suff) (h : ∀ (g : Nat → Bool), PatternWords g p help → RowWords g p pref.length si) (g : Nat → Bool) : PatternWords g p help → RowWords g p (pref ++ [cur]).length (si.set! cur help[cur]!)

A copy of word cur < ⌊p / 64⌋ of the pattern into the row.

theorem Ratpoints.Sieve.ringState_init {p m : Nat} {help : Vector UInt64 m} {si : Vector UInt64 ((p + chunk - 1) * rbaPack)} (h : ∀ (g : Nat → Bool), PatternWords g p help → RowWords g p (ForIn.toList [:p / 64]).length si) (g : Nat → Bool) (hg : PatternWords g p help) : RingState g p (p / 64) (p % 64) (64 * (p / 64 + [].length)) (p / 64) help ∧ RowWords g p (p / 64 + [].length) si

The start of the ring: the cursor at wp, the ring at the bit 64 wp, the first wp words of the row copied.

theorem Ratpoints.Sieve.RingState.append {p cur m : Nat} {pref suff : List Nat} {help0 help : Vector UInt64 m} {si : Vector UInt64 ((p + chunk - 1) * rbaPack)} {a1 : Nat} (pre : 64 ≤ p ∧ p % 64 ≠ 0) (hm : p / 64 < m) (hl : ForIn.toList [p / 64:p] = pref ++ cur :: suff) (h : ∀ (g : Nat → Bool), PatternWords g p help0 → RingState g p (p / 64) (p % 64) (64 * (p / 64 + pref.length)) a1 help ∧ RowWords g p (p / 64 + pref.length) si) (g : Nat → Bool) : PatternWords g p help0 → RingState g p (p / 64) (p % 64) (64 * (p / 64 + (pref ++ [cur]).length)) (if a1 = p / 64 then 0 else a1 + 1) ((help.set! a1 (help[a1]! ||| help[if a1 = p / 64 then 0 else a1 + 1]! <<< UInt64.ofNat (p % 64))).set! (if a1 = p / 64 then 0 else a1 + 1) ((help.set! a1 (help[a1]! ||| help[if a1 = p / 64 then 0 else a1 + 1]! <<< UInt64.ofNat (p % 64)))[if a1 = p / 64 then 0 else a1 + 1]! >>> UInt64.ofNat (64 - p % 64))) ∧ RowWords g p (p / 64 + (pref ++ [cur]).length) (si.set! cur (help.set! a1 (help[a1]! ||| help[if a1 = p / 64 then 0 else a1 + 1]! <<< UInt64.ofNat (p % 64)))[a1]!)

A step of the loop of the ring, in the shape of the verification condition.

theorem Ratpoints.Sieve.RingState.post {p m : Nat} {help0 help : Vector UInt64 m} {si : Vector UInt64 ((p + chunk - 1) * rbaPack)} {a1 : Nat} (pre : 64 ≤ p ∧ p % 64 ≠ 0) (h : ∀ (g : Nat → Bool), PatternWords g p help0 → RingState g p (p / 64) (p % 64) (64 * (p / 64 + (ForIn.toList [p / 64:p]).length)) a1 help ∧ RowWords g p (p / 64 + (ForIn.toList [p / 64:p]).length) si) (g : Nat → Bool) (hg : PatternWords g p help0) : RowWords g p p si

theorem Ratpoints.Sieve.sieve2Rows_spec (p : Nat) (help : Vector UInt64 (p / 64 + 2)) : ⦃ 64 ≤ p ∧ p % 64 ≠ 0 ⦄ sieve2Rows p help ⦃ fun (si : Vector UInt64 ((p + chunk - 1) * rbaPack)) => ∀ (g : Nat → Bool), PatternWords g p help → RowWords g p p si ⦄

The first p words of the row of a prime p > 64 with p mod 64 ≠ 0 in CODE_INIT_SIEVE2: for every pattern g of period p held in the words help (Ratpoints.Sieve.PatternWords), word a < p of the row is the window of g at 64 a.

theorem Ratpoints.Sieve.sieveInit2_post {t : Entry} {ref : EntryRef} {b : Nat} {store : RowStore} {help : Vector UInt64 (t.p / 64 + 2)} {si si' : Vector UInt64 ((t.p + chunk - 1) * rbaPack)} (pre : 0 < b ∧ b < t.p ∧ 64 ≤ t.p ∧ t.p % 64 ≠ 0 ∧ t.inverses[b]! < t.p) (hpat : PatternWords (lanePattern t.isFSquare t.p 0 t.inverses[b]!) t.p help) (hrows : ∀ (g : Nat → Bool), PatternWords g t.p help → RowWords g t.p t.p si) (hrep : ∀ (j : Nat), j < (t.p + chunk - 1) * rbaPack → si'[j]! = si[j % t.p]!) : (si', store.publish ref b si'.toArray).fst.toArray = closedRow t.admits t.p b ∧ (si', store.publish ref b si'.toArray).snd = store.publish ref b (closedRow t.admits t.p b)

theorem Ratpoints.Sieve.sieveInit2_spec (t : Entry) (ref : EntryRef) (b : Nat) (store : RowStore) : ⦃ 0 < b ∧ b < t.p ∧ 64 ≤ t.p ∧ t.p % 64 ≠ 0 ∧ t.inverses[b]! < t.p ⦄ sieveInit2 t ref b store ⦃ fun (r : Vector UInt64 ((t.p + chunk - 1) * rbaPack) × RowStore) => r.fst.toArray = closedRow t.admits t.p b ∧ r.snd = store.publish ref b (closedRow t.admits t.p b) ⦄

The row of the residue 0 < b < p of a prime p ≥ 64 with p mod 64 ≠ 0 by CODE_INIT_SIEVE2 is the closed form of the row of b of its table, for the inverse of b below p, and the builder stores it into the table of rows of the entry ref. The words help that the builder clears from the last are overwritten by the pattern before they are read.