The contract of the chunked first stage

The contracts of the arm of the first stage for a chunk from 2 to 16 (Ratpoints.Sieve.andRowsChunked): the starts of the rows at the first word number of a piece (Ratpoints.Sieve.chunkStarts), a start stepped back by the modulus (Ratpoints.Sieve.wrapStart), one chunk in registers (Ratpoints.Sieve.chunkSieve), the whole chunks of a piece (Ratpoints.Sieve.andChunks), one leg over the tail (Ratpoints.Sieve.tailLeg) and the tail in legs of 8, 4, 2 and 1 bit arrays (Ratpoints.Sieve.tailLegs), as @[spec] theorems proved with vcgen, the program logic of Lean core, with loop invariants that are named definitions. The chunked arm leaves the words of the piece that the arm one row at a time leaves (Ratpoints.Sieve.andRowsChunked_spec, with the postcondition of Ratpoints.Sieve.andRows_spec).

The chunked arm reads each row from its start, which it moves on by the chunk after each chunk and back into the first p bit arrays of the row: from the starts at the first word number of the piece to those at the word number of the next chunk (Ratpoints.Sieve.SieveSpec.startAt_advance). The registers read up to chunk - 1 bit arrays past the first p of a row, which repeat its first ones, and so hold the words of the first stage at the word numbers of the chunk (Ratpoints.Sieve.partialReg_map_startAt).

Main definitions

• Ratpoints.Sieve.SieveSpec.startAt, Ratpoints.Sieve.SieveSpec.advance: a sieve spec with its start at a word number, and with its start moved on.
• Ratpoints.Sieve.partialReg, Ratpoints.Sieve.RegsInvariant, Ratpoints.Sieve.RegsStored: the registers of a chunk or a leg after some of the moduli, the invariant of the loops that and the rows into them, and the bit arrays that the legs store.

Main statements

• Ratpoints.Sieve.wrapStart_spec: the start stepped back is the start modulo p.
• Ratpoints.Sieve.chunkStarts_spec: the starts of the rows at the first word number.
• Ratpoints.Sieve.chunkSieve_spec, Ratpoints.Sieve.andChunks_spec: one chunk, and the whole chunks of a piece.
• Ratpoints.Sieve.tailLeg_spec, Ratpoints.Sieve.tailLegs_spec: one leg, and the tail.
• Ratpoints.Sieve.andRowsChunked_spec: the chunked arm leaves each word of the piece the class word and-ed with its row words (Ratpoints.Sieve.andWords).

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; the cover of the tail by the legs is a fact decided over the tails below 16, which the arm's chunk of at most 16 bounds.

The starts of the rows

def Ratpoints.Sieve.SieveSpec.startAt (w0 : Int) (s : SieveSpec) : SieveSpec

The sieve spec s with its start at the word number w0: the bit array (w0 + offset) mod p of the row, which the bit array with the word number w0 reads.

Equations

• Ratpoints.Sieve.SieveSpec.startAt w0 s = { p := s.p, offset := s.offset, row := s.row, start := ((w0 + ↑s.offset) % ↑s.p).toNat, stop := s.stop }

def Ratpoints.Sieve.SieveSpec.advance (c : Nat) (s : SieveSpec) : SieveSpec

The sieve spec s with its start moved on by c bit arrays and back into the first p bit arrays of the row.

Equations

• Ratpoints.Sieve.SieveSpec.advance c s = { p := s.p, offset := s.offset, row := s.row, start := (s.start + c) % s.p, stop := s.stop }

theorem Ratpoints.Sieve.SieveSpec.startAt_advance (s : SieveSpec) (hp : 0 < s.p) (w : Int) (c : Nat) : advance c (startAt w s) = startAt (w + ↑c) s

The registers of a chunk

def Ratpoints.Sieve.partialReg (l : List SieveSpec) (cw : UInt64) (x κ : Nat) : UInt64

The registers of the chunked first stage at word κ of bit array x after the moduli l: the class word cw and-ed in turn with word κ of bit array start + x of each row, read past the first p bit arrays into the copies of the first ones.

Equations

• Ratpoints.Sieve.partialReg l cw x κ = List.foldl (fun (acc : UInt64) (s : Ratpoints.Sieve.SieveSpec) => acc &&& s.row[Ratpoints.rbaPack * (s.start + x) + κ]!) cw l

theorem Ratpoints.Sieve.partialReg_concat (l : List SieveSpec) (s : SieveSpec) (cw : UInt64) (x κ : Nat) : partialReg (l ++ [s]) cw x κ = partialReg l cw x κ &&& s.row[rbaPack * (s.start + x) + κ]!

theorem Ratpoints.Sieve.partialReg_map_startAt {specs : List SieveSpec} (h : ∀ (s : SieveSpec), s ∈ specs → s.Fits) (cw : UInt64) (w : Int) {x κ : Nat} (hx : x < chunk) (hκ : κ < rbaPack) : partialReg (List.map (fun (x : SieveSpec) => SieveSpec.startAt w x) specs) cw x κ = andWords specs cw w (rbaPack * x + κ)

The registers of a chunk, read from the starts of the rows at the word number w up to chunk - 1 bit arrays past them, hold the words of the first stage at the word numbers from w on (Ratpoints.Sieve.andWords), since the rows repeat their first bit arrays after the first p (Ratpoints.Sieve.SieveSpec.Wraps).

theorem Ratpoints.Sieve.partialReg_take_succ {sv : Array SieveSpec} {K : Nat} (hK : K < sv.size) (cw : UInt64) (x κ : Nat) : partialReg (List.take (K + 1) sv.toList) cw x κ = partialReg (List.take K sv.toList) cw x κ &&& sv[K]!.row[rbaPack * (sv[K]!.start + x) + κ]!

def Ratpoints.Sieve.RegsInvariant (sv : Array SieveSpec) (cw : UInt64) (w K c : Nat) (f : Nat → Nat) {m : Nat} (regs : Vector UInt64 m) : Prop

The w registers regs of the chunked first stage, register j reading bit array start + f j of the rows, after the row of the modulus K of the local array sv is and-ed into the registers below c: register j holds the class word cw and-ed with the rows of the first K + 1 moduli for j < c and of the first K otherwise (Ratpoints.Sieve.partialReg). The invariant of the loops of Ratpoints.Sieve.chunkSieve (f j = j) and of Ratpoints.Sieve.tailLeg (f j = off + j) that and the row of a modulus into the registers.

Equations

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

theorem Ratpoints.Sieve.getElem!_loadBitArray_take_one {sv : Array SieveSpec} {cw : UInt64} {f : Nat → Nat} {M w cur q : Nat} {pref suff : List Nat} {regs : Vector UInt64 (M * rbaPack)} (hs : 0 < sv.size) (hw : w ≤ M) (hl : ForIn.toList [:w] = pref ++ cur :: suff) (hq : q = sv[0]!.start + f cur) (h : ∀ (j : Nat), j < pref.length → ∀ (κ : Nat), κ < rbaPack → regs[rbaPack * j + κ]! = partialReg (List.take 1 sv.toList) cw (f j) κ) (j : Nat) : j < (pref ++ [cur]).length → ∀ (κ : Nat), κ < rbaPack → (loadBitArray regs cur cw sv[0]!.row q)[rbaPack * j + κ]! = partialReg (List.take 1 sv.toList) cw (f j) κ

A step of the loops of Ratpoints.Sieve.chunkSieve and Ratpoints.Sieve.tailLeg that load the row of the first modulus into w ≤ M registers, register j reading bit array start + f j of the row: register cur holds the class word cw and-ed with its bit array, the registers before it as they were.

theorem Ratpoints.Sieve.regsInvariant_init {sv : Array SieveSpec} {cw : UInt64} {f : Nat → Nat} {m w N cur : Nat} {pref suff : List Nat} {regs : Vector UInt64 m} (hl : ForIn.toList [1:N] = pref ++ cur :: suff) (h : ∀ (j : Nat), j < w → ∀ (κ : Nat), κ < rbaPack → regs[rbaPack * j + κ]! = partialReg (List.take (1 + pref.length) sv.toList) cw (f j) κ) : RegsInvariant sv cw w cur [].length f regs

The start of the loop of Ratpoints.Sieve.chunkSieve or Ratpoints.Sieve.tailLeg that ands the row of the modulus cur into the registers, which hold the moduli before it.

theorem Ratpoints.Sieve.RegsInvariant.append_andBitArray {sv : Array SieveSpec} {cw : UInt64} {f : Nat → Nat} {M w N K cur q : Nat} {s : SieveSpec} {pref' suff' pref suff : List Nat} {regs : Vector UInt64 (M * rbaPack)} (hl' : ForIn.toList [1:N] = pref' ++ K :: suff') (hN : N = sv.size) (hs : s = sv[K]!) (hq : q = s.start + f cur) (hw : w ≤ M) (hl : ForIn.toList [:w] = pref ++ cur :: suff) (h : RegsInvariant sv cw w K pref.length f regs) : RegsInvariant sv cw w K (pref ++ [cur]).length f (andBitArray regs cur s.row q)

A step of the loops of Ratpoints.Sieve.chunkSieve and Ratpoints.Sieve.tailLeg that and the row of the modulus K into w ≤ M registers, register j reading bit array start + f j of the row: register cur and-ed with its bit array of the row of s, the sieve spec of K with the start that the loop moves on only after the registers, holds the moduli up to K.

theorem Ratpoints.Sieve.RegsInvariant.next {sv : Array SieveSpec} {cw : UInt64} {f : Nat → Nat} {m w N cur : Nat} {pref suff : List Nat} {regs : Vector UInt64 m} (hl : ForIn.toList [1:N] = pref ++ cur :: suff) (h : RegsInvariant sv cw w cur (ForIn.toList [:w]).length f regs) (j : Nat) : j < w → ∀ (κ : Nat), κ < rbaPack → regs[rbaPack * j + κ]! = partialReg (List.take (1 + (pref ++ [cur]).length) sv.toList) cw (f j) κ

At the end of the loop that ands the row of the modulus cur into the registers, they hold the moduli up to cur.

def Ratpoints.Sieve.RegsStored (sv : Array SieveSpec) (cw : UInt64) (base lo hi : Nat) {m : Nat} (surv surv' : Vector UInt64 m) : Prop

The words of the bit arrays from lo to below hi of surv' are the class word cw and-ed with the rows of all the moduli of the local array sv, read at their starts plus the bit array minus base (Ratpoints.Sieve.partialReg), and the other words those of surv: what the legs of the tail from the bit array base on store (Ratpoints.Sieve.tailLeg, Ratpoints.Sieve.tailLegs).

Equations

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

theorem Ratpoints.Sieve.regsStored_of_le (sv : Array SieveSpec) (cw : UInt64) (base : Nat) {lo hi : Nat} (h : hi ≤ lo) {m : Nat} (surv : Vector UInt64 m) : RegsStored sv cw base lo hi surv surv

The starts at the first word number

def Ratpoints.Sieve.ChunkStartsInvariant (w0 : Int) (specs : List SieveSpec) (mgs : List Nat) (pref : List SieveSpec) (st : Array SieveSpec × List Nat) : Prop

The invariant of the loop of Ratpoints.Sieve.chunkStarts over the moduli specs and, in step with them, their reciprocals mgs, after the moduli pref, whose state is the local array of the sieve specs 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 array holds the sieve specs of pref with their starts at the word number w0.

Equations

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

theorem Ratpoints.Sieve.chunkStartsInvariant_nil (w0 : Int) (specs : List SieveSpec) (mgs : List Nat) : ChunkStartsInvariant w0 specs mgs [] (#[], Std.toStream mgs)

theorem Ratpoints.Sieve.ChunkStartsInvariant.push {w0 : Int} {small : Bool} {specs pref suff : List SieveSpec} {s : SieveSpec} {mgs rest rest' : List Nat} {mg : Nat} {sv : Array SieveSpec} (pre : StageFits specs mgs small w0 w0) (hs : specs = pref ++ s :: suff) (h : ChunkStartsInvariant w0 specs mgs pref (sv, rest)) (hnext : Std.Stream.next? rest = some (mg, rest')) : ChunkStartsInvariant w0 specs mgs (pref ++ [s]) (sv.push { p := s.p, offset := s.offset, row := s.row, start := (if small = true then modMul (w0 + ↑s.offset) s.p mg else modLong (w0 + ↑s.offset) ↑s.p).toNat, stop := s.stop }, rest')

A step of the loop of Ratpoints.Sieve.chunkStarts: the start of the modulus s at w0 by the reduction with the reciprocal of the cursor, which is that of s (Ratpoints.Sieve.SieveSpec.Fits.ite_modMul_modLong_add_eq_emod).

theorem Ratpoints.Sieve.ChunkStartsInvariant.next?_ne_none {w0 : Int} {small : Bool} {specs pref suff : List SieveSpec} {s : SieveSpec} {mgs rest : List Nat} {sv : Array SieveSpec} (pre : StageFits specs mgs small w0 w0) (hs : specs = pref ++ s :: suff) (h : ChunkStartsInvariant w0 specs mgs pref (sv, rest)) : Std.Stream.next? rest ≠ none

theorem Ratpoints.Sieve.ChunkStartsInvariant.toList_eq {w0 : Int} {mgs : List Nat} {specs : List SieveSpec} {st : Array SieveSpec × List Nat} (h : ChunkStartsInvariant w0 specs mgs specs st) : st.fst.toList = List.map (fun (x : SieveSpec) => SieveSpec.startAt w0 x) specs

theorem Ratpoints.Sieve.chunkStarts_spec (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (w0 : Int) : ⦃ StageFits specs mgs small w0 w0 ⦄ chunkStarts specs mgs small w0 ⦃ fun (sv : Array SieveSpec) => sv.toList = List.map (fun (x : SieveSpec) => SieveSpec.startAt w0 x) specs ⦄

The local array of the sieve specs holds them with their starts at the word number w0, the reduction by the reciprocal of the cursor under the test small giving the Euclidean remainder of w0 + offset; the reciprocals run in step with the moduli and do not run out before them.

The step back of a start

def Ratpoints.Sieve.WrapStartInvariant (st p : Nat) : Std.WP.WhileInvariant Nat Prop

The invariant of the loop of Ratpoints.Sieve.wrapStart: the start keeps its residue modulo p, and is below p at the exit.

Equations

• Ratpoints.Sieve.WrapStartInvariant st p = Std.WP.WhileInvariant.mk fun (exit : Bool) (s : Nat) => s % p = st % p ∧ (exit = true → s < p)

theorem Ratpoints.Sieve.WrapStartInvariant.sub {st p stop s mb : Nat} (h : s = mb ∧ WrapStartInvariant st p false s) (hs : stop ≤ s) (pre : 0 < p ∧ stop = p) : s - p < mb ∧ WrapStartInvariant st p false (s - p)

theorem Ratpoints.Sieve.WrapStartInvariant.exit {st p stop s mb : Nat} (hs : ¬stop ≤ s) (pre : 0 < p ∧ stop = p) (h : s = mb ∧ WrapStartInvariant st p false s) : WrapStartInvariant st p true s

theorem Ratpoints.Sieve.WrapStartInvariant.post {st p s : Nat} (h : WrapStartInvariant st p true s) : s = st % p

theorem Ratpoints.Sieve.wrapStart_spec (st stop p : Nat) : ⦃ 0 < p ∧ stop = p ⦄ wrapStart st stop p ⦃ fun (r : Nat) => r = st % p ⦄

For the end stop = p > 0, the start stepped back is its residue modulo p.

One chunk

def Ratpoints.Sieve.ChunkModInvariant (sv : Array SieveSpec) (cw : UInt64) (K : Nat) (st : Array SieveSpec) (regs : Vector UInt64 (chunk * rbaPack)) : Prop

The invariant of the loop of Ratpoints.Sieve.chunkSieve over the moduli after the first K of the local array sv: the registers hold the first K moduli, and the starts of those moduli are moved on by the chunk.

Equations

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

theorem Ratpoints.Sieve.chunkModInvariant_init {sv : Array SieveSpec} {cw : UInt64} {st : Nat} {regs : Vector UInt64 (chunk * rbaPack)} (h : ∀ (j : Nat), j < (ForIn.toList [:chunk]).length → ∀ (κ : Nat), κ < rbaPack → regs[rbaPack * j + κ]! = partialReg (List.take 1 sv.toList) cw j κ) (hst : st = (sv[0]!.start + chunk) % sv[0]!.p) : ChunkModInvariant sv cw (1 + [].length) (sv.set! 0 (have __src := sv[0]!; { p := __src.p, offset := __src.offset, row := __src.row, start := st, stop := __src.stop })) regs

The start of the loop over the further moduli: the registers hold the first modulus, its start moved on.

theorem Ratpoints.Sieve.ChunkModInvariant.post {sv : Array SieveSpec} {cw : UInt64} {st : Array SieveSpec} {regs : Vector UInt64 (chunk * rbaPack)} {N : Nat} (pre : 0 < sv.size ∧ ∀ (s : SieveSpec), s ∈ sv → 0 < s.p ∧ s.stop = s.p) (h : ChunkModInvariant sv cw (1 + (ForIn.toList [1:N]).length) st regs) (hN : N = sv.size) : (∀ (j : Nat), j < chunk → ∀ (κ : Nat), κ < rbaPack → regs[rbaPack * j + κ]! = partialReg sv.toList cw j κ) ∧ st.toList = List.map (SieveSpec.advance chunk) sv.toList

theorem Ratpoints.Sieve.ChunkModInvariant.getElem!_eq {sv st : Array SieveSpec} {cw : UInt64} {cur N : Nat} {pref suff : List Nat} {regs : Vector UInt64 (chunk * rbaPack)} (hl : ForIn.toList [1:N] = pref ++ cur :: suff) (h : ChunkModInvariant sv cw (1 + pref.length) st regs) (hN : N = sv.size) : st[cur]! = sv[cur]!

In the loop of Ratpoints.Sieve.chunkSieve over the further moduli, the sieve spec of the modulus cur is still that of the local array: its start moves on only after the registers.

theorem Ratpoints.Sieve.ChunkModInvariant.regsInvariant {sv st : Array SieveSpec} {cw : UInt64} {cur N : Nat} {pref suff : List Nat} {regs : Vector UInt64 (chunk * rbaPack)} (hl : ForIn.toList [1:N] = pref ++ cur :: suff) (h : ChunkModInvariant sv cw (1 + pref.length) st regs) : RegsInvariant sv cw chunk cur [].length (fun (j : Nat) => j) regs

theorem Ratpoints.Sieve.RegsInvariant.chunkModInvariant {sv : Array SieveSpec} {cw : UInt64} {cur st' N : Nat} {pref suff : List Nat} {st : Array SieveSpec} {regs regs0 : Vector UInt64 (chunk * rbaPack)} (hl : ForIn.toList [1:N] = pref ++ cur :: suff) (hmod : ChunkModInvariant sv cw (1 + pref.length) st regs0) (h : RegsInvariant sv cw chunk cur (ForIn.toList [:chunk]).length (fun (j : Nat) => j) regs) (hst' : st' = (st[cur]!.start + chunk) % st[cur]!.p) (hN : N = sv.size) : ChunkModInvariant sv cw (1 + (pref ++ [cur]).length) (st.set! cur (have __src := st[cur]!; { p := __src.p, offset := __src.offset, row := __src.row, start := st', stop := __src.stop })) regs

The ands of the modulus cur done: its start moves on.

theorem Ratpoints.Sieve.chunkSieve_spec (sv : Array SieveSpec) (cw : UInt64) : ⦃ 0 < sv.size ∧ ∀ (s : SieveSpec), s ∈ sv → 0 < s.p ∧ s.stop = s.p ⦄ chunkSieve sv cw ⦃ fun (r : Vector UInt64 (chunk * rbaPack) × Array SieveSpec) => (∀ (j : Nat), j < chunk → ∀ (κ : Nat), κ < rbaPack → r.fst[rbaPack * j + κ]! = partialReg sv.toList cw j κ) ∧ r.snd.toList = List.map (SieveSpec.advance chunk) sv.toList ⦄

The registers of a chunk hold the class word and-ed with the rows of all the moduli of the local array from their starts on (Ratpoints.Sieve.partialReg), and the starts move on by the chunk and back into the first p bit arrays of the rows (Ratpoints.Sieve.wrapStart_spec).

The whole chunks of a piece

def Ratpoints.Sieve.AndChunksInvariant (specs : List SieveSpec) (cw : UInt64) (w0 : Int) (full : Nat) {m : Nat} (surv : Vector UInt64 m) : Std.WP.WhileInvariant (Array SieveSpec × Vector UInt64 m × Nat) Prop

The invariant of the loop of Ratpoints.Sieve.andChunks over the chunks, on the local array of the sieve specs, the words of the piece and the first bit array c of the next chunk, for the moduli specs of the first stage over a piece from the word number w0 on: c a multiple of the chunk up to full, the starts at the word number w0 + c, and the words of the bit arrays below c those of the first stage (Ratpoints.Sieve.andWords), the others as in surv.

Equations

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

def Ratpoints.Sieve.StoreChunkInvariant (specs : List SieveSpec) (cw : UInt64) (w0 : Int) (c d : Nat) {m : Nat} (surv surv' : Vector UInt64 m) : Prop

The invariant of the stores of a chunk from the bit array c on into the words of the piece, after d of them.

Equations

• Ratpoints.Sieve.StoreChunkInvariant specs cw w0 c d surv surv' = ∀ (y : Nat), y < m → surv'[y]! = if y < (c + d) * Ratpoints.rbaPack then Ratpoints.Sieve.andWords specs cw w0 y else surv[y]!

theorem Ratpoints.Sieve.andChunksInvariant_init {specs : List SieveSpec} {sv : Array SieveSpec} {cw : UInt64} {w0 : Int} {full m : Nat} (surv : Vector UInt64 m) (pre : (∀ (s : SieveSpec), s ∈ specs → s.Fits) ∧ sv.toList = List.map (fun (x : SieveSpec) => SieveSpec.startAt w0 x) specs ∧ 0 < sv.size ∧ full % chunk = 0) : AndChunksInvariant specs cw w0 full surv false (sv, surv, 0)

theorem Ratpoints.Sieve.storeChunkInvariant_init {specs : List SieveSpec} {sv' : Array SieveSpec} {cw : UInt64} {w0 : Int} {full m c mb : Nat} {surv surv' : Vector UInt64 m} (h : full - c = mb ∧ AndChunksInvariant specs cw w0 full surv false (sv', surv', c)) : StoreChunkInvariant specs cw w0 c [].length surv surv'

theorem Ratpoints.Sieve.andWords_eq_div_mod (specs : List SieveSpec) (cw : UInt64) (w0 : Int) (y : Nat) : andWords specs cw w0 y = andWords specs cw (w0 + ↑(y / rbaPack)) (y % rbaPack)

The word y of a piece from the word number w0 on is word y mod rbaPack of the bit array with the word number w0 + y / rbaPack.

theorem Ratpoints.Sieve.StoreChunkInvariant.append_storeBitArray {specs : List SieveSpec} {sv sv' sv'' : Array SieveSpec} {cw : UInt64} {w0 : Int} {full m c mb cur : Nat} {pref suff : List Nat} {surv surv0 surv' : Vector UInt64 m} {regs : Vector UInt64 (chunk * rbaPack)} (pre : (∀ (s : SieveSpec), s ∈ specs → s.Fits) ∧ sv.toList = List.map (fun (x : SieveSpec) => SieveSpec.startAt w0 x) specs ∧ 0 < sv.size ∧ full % chunk = 0) (hc : full - c = mb ∧ AndChunksInvariant specs cw w0 full surv false (sv', surv0, c)) (hr : (∀ (j : Nat), j < chunk → ∀ (κ : Nat), κ < rbaPack → regs[rbaPack * j + κ]! = partialReg sv'.toList cw j κ) ∧ sv''.toList = List.map (SieveSpec.advance chunk) sv'.toList) (hl : ForIn.toList [:chunk] = pref ++ cur :: suff) (h : StoreChunkInvariant specs cw w0 c pref.length surv surv') : StoreChunkInvariant specs cw w0 c (pref ++ [cur]).length surv (storeBitArray surv' (c + cur) regs cur)

A store of a register of the chunk from the bit array c on into the words of the piece.

theorem Ratpoints.Sieve.AndChunksInvariant.add_chunk {specs : List SieveSpec} {sv sv' sv'' : Array SieveSpec} {cw : UInt64} {w0 : Int} {full m c mb : Nat} {surv surv0 surv' : Vector UInt64 m} {regs : Vector UInt64 (chunk * rbaPack)} (pre : (∀ (s : SieveSpec), s ∈ specs → s.Fits) ∧ sv.toList = List.map (fun (x : SieveSpec) => SieveSpec.startAt w0 x) specs ∧ 0 < sv.size ∧ full % chunk = 0) (hc : full - c = mb ∧ AndChunksInvariant specs cw w0 full surv false (sv', surv0, c)) (hcl : c < full) (hr : (∀ (j : Nat), j < chunk → ∀ (κ : Nat), κ < rbaPack → regs[rbaPack * j + κ]! = partialReg sv'.toList cw j κ) ∧ sv''.toList = List.map (SieveSpec.advance chunk) sv'.toList) (hs : StoreChunkInvariant specs cw w0 c (ForIn.toList [:chunk]).length surv surv') : full - (c + chunk) < mb ∧ AndChunksInvariant specs cw w0 full surv false (sv'', surv', c + chunk)

A chunk done: the starts move on by the chunk, and the words of its bit arrays are stored.

theorem Ratpoints.Sieve.AndChunksInvariant.exit {specs : List SieveSpec} {sv' : Array SieveSpec} {cw : UInt64} {w0 : Int} {full m c mb : Nat} {surv surv' : Vector UInt64 m} (h : full - c = mb ∧ AndChunksInvariant specs cw w0 full surv false (sv', surv', c)) (hcl : ¬c < full) : AndChunksInvariant specs cw w0 full surv true (sv', surv', c)

theorem Ratpoints.Sieve.AndChunksInvariant.post {specs : List SieveSpec} {sv' : Array SieveSpec} {cw : UInt64} {w0 : Int} {full m c : Nat} {surv surv' : Vector UInt64 m} (h : AndChunksInvariant specs cw w0 full surv true (sv', surv', c)) : (∀ (y : Nat), y < m → surv'[y]! = if y < full * rbaPack then andWords specs cw w0 y else surv[y]!) ∧ sv'.toList = List.map (fun (x : SieveSpec) => SieveSpec.startAt (w0 + ↑full) x) specs

theorem Ratpoints.Sieve.andChunks_spec (specs : List SieveSpec) (w0 : Int) (sv : Array SieveSpec) (cw : UInt64) (full : Nat) {m : Nat} (surv : Vector UInt64 m) : ⦃ (∀ (s : SieveSpec), s ∈ specs → s.Fits) ∧ sv.toList = List.map (fun (x : SieveSpec) => SieveSpec.startAt w0 x) specs ∧ 0 < sv.size ∧ full % chunk = 0 ⦄ andChunks sv cw full surv ⦃ fun (r : Vector UInt64 m × Array SieveSpec) => (∀ (y : Nat), y < m → r.fst[y]! = if y < full * rbaPack then andWords specs cw w0 y else surv[y]!) ∧ r.snd.toList = List.map (fun (x : SieveSpec) => SieveSpec.startAt (w0 + ↑full) x) specs ⦄

The whole chunks below full, a multiple of the chunk, of a piece from the word number w0 on store into the words of their bit arrays those of the first stage with the moduli specs (Ratpoints.Sieve.andWords), read from the local array of their sieve specs with the starts at w0, which they move on to the word number w0 + full; the other words stay as they are. The moduli and the word number are arguments, since the program does not mention them.

One leg over the tail

theorem Ratpoints.Sieve.RegsStored.append_storeBitArray {sv : Array SieveSpec} {cw : UInt64} {m : Nat} {surv surv' : Vector UInt64 m} {reg : Vector UInt64 (8 * rbaPack)} {w off base cur : Nat} {pref suff : List Nat} (hreg : ∀ (i : Nat), i < w → ∀ (κ : Nat), κ < rbaPack → reg[rbaPack * i + κ]! = partialReg (List.take (1 + (ForIn.toList [1:sv.size]).length) sv.toList) cw (off + i) κ) (pre : 0 < sv.size ∧ w ≤ 8) (hl : ForIn.toList [:w] = pref ++ cur :: suff) (h : RegsStored sv cw base (base + off) (base + off + pref.length) surv surv') : RegsStored sv cw base (base + off) (base + off + (pref ++ [cur]).length) surv (storeBitArray surv' (base + off + cur) reg cur)

A store of register cur of a leg of Ratpoints.Sieve.tailLeg from off on into the bit array base + off + cur of the piece.

theorem Ratpoints.Sieve.RegsStored.length_toList {sv : Array SieveSpec} {cw : UInt64} {m : Nat} {surv surv' : Vector UInt64 m} {w base lo : Nat} (h : RegsStored sv cw base lo (lo + (ForIn.toList [:w]).length) surv surv') : RegsStored sv cw base lo (lo + w) surv surv'

theorem Ratpoints.Sieve.tailLeg_spec (w off : Nat) {m : Nat} (surv : Vector UInt64 m) (base : Nat) (cw : UInt64) (sv : Array SieveSpec) : ⦃ 0 < sv.size ∧ w ≤ 8 ⦄ tailLeg w off surv base cw sv ⦃ fun (surv' : Vector UInt64 m) => RegsStored sv cw base (base + off) (base + off + w) surv surv' ⦄

A leg of w ≤ 8 registers from off on stores into the bit arrays base + off + i, i < w, the class word and-ed with the rows of all the moduli of the local array at their starts plus off + i; the other words stay as they are.

The tail

theorem Ratpoints.Sieve.run_tailLegs (sv : Array SieveSpec) (cw : UInt64) (full n : Nat) {m : Nat} (surv : Vector UInt64 m) : (tailLegs sv cw full n surv).run = have t := n - full; have s1 := if 8 < chunk ∧ t &&& 8 ≠ 0 then (tailLeg 8 0 surv full cw sv).run else surv; have s2 := if 4 < chunk ∧ t &&& 4 ≠ 0 then (tailLeg 4 (t &&& 8) s1 full cw sv).run else s1; have s3 := if 2 < chunk ∧ t &&& 2 ≠ 0 then (tailLeg 2 (t &&& 12) s2 full cw sv).run else s2; if t &&& 1 ≠ 0 then (tailLeg 1 (t &&& 14) s3 full cw sv).run else s3

The four guarded legs over the tail as nested conditional values: the first stage over the tail of t = n - full bit arrays, the legs of 8, 4, 2 and 1 bit arrays from the offsets 0, t &&& 8, t &&& 12 and t &&& 14 on.

theorem Ratpoints.Sieve.RegsStored.leg {sv : Array SieveSpec} {cw : UInt64} {full u w t m : Nat} {surv s : Vector UInt64 m} {g : Prop} [Decidable g] (h : RegsStored sv cw full full (full + u) surv s) (hs : 0 < sv.size) (hw : w ≤ 8) (hg : g ↔ t &&& w ≠ 0) (htw : t &&& w ≠ 0 → t &&& w = w) : RegsStored sv cw full full (full + (u + (t &&& w))) surv (if g then (tailLeg w u s full cw sv).run else s)

A guarded leg of w bit arrays from the offset u on, which runs exactly when bit w of t is set, does the bit arrays from full + u on, t &&& w of them.

theorem Ratpoints.Sieve.tailLegs_spec (sv : Array SieveSpec) (cw : UInt64) (full n : Nat) {m : Nat} (surv : Vector UInt64 m) : ⦃ chunk ≤ 16 ∧ n - full < chunk ∧ 0 < sv.size ⦄ tailLegs sv cw full n surv ⦃ fun (surv' : Vector UInt64 m) => RegsStored sv cw full full (full + (n - full)) surv surv' ⦄

The legs over the tail of t = n - full < chunk ≤ 16 bit arrays do its bit arrays full, …, n - 1: the class word and-ed with the rows of all the moduli of the local array at their starts plus the place in the tail (Ratpoints.Sieve.partialReg); the other words stay as they are.

The chunked first stage

theorem Ratpoints.Sieve.AndRowsFillInvariant.getElem!_eq_andWords {specs : List SieveSpec} {sv : Array SieveSpec} {cw : UInt64} {w0 : Int} {n m : Nat} {surv : Vector UInt64 m} (hsv : sv.toList = List.map (fun (x : SieveSpec) => SieveSpec.startAt w0 x) specs) (hz : sv.size = 0) (h : AndRowsFillInvariant cw n (ForIn.toList [:n]).length surv) {y : Nat} (hy : y < n * rbaPack) : surv[y]! = andWords specs cw w0 y

With no modulus, the bit arrays set to the class word are the words of the first stage.

theorem Ratpoints.Sieve.andRowsChunked_spec (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (cw : UInt64) (w0 : Int) (n : Nat) (surv : Vector UInt64 ((n + 1) * rbaPack)) : ⦃ chunk ≤ 16 ∧ StageFits specs mgs small w0 (w0 + ↑n) ⦄ andRowsChunked 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 ⦄

The chunked first stage, for the arm's chunk of at most 16, leaves each word of the piece the class word cw and-ed with its row words (Ratpoints.Sieve.andWords), as the first stage one row at a time does (Ratpoints.Sieve.andRows_spec): the whole chunks and the tail read the rows from their starts at the first word number, into the copies of their first bit arrays (Ratpoints.Sieve.SieveSpec.Wraps), and with no modulus every bit array is the class word.