The counters of the scan of a piece

The counts that the components of the model on words from the walk through the set bits of a word on, through the second stage and the extraction of one bit array, up to the scan of a piece, add to the counters of the sieving thread (Ratpoints.Sieve.Counters), as contracts proved with vcgen, the program logic of Lean core, with loop invariants that are named definitions. When the callback does not stop the search, each component adds closed forms that depend neither on the callback nor on the delivery: the counts of the tests of a candidate (Ratpoints.Sieve.testedCounts) of the numerators that the contracts of Ratpoints.Proof.Scan deliver the points of, and, for the scan of a piece, the number of its bit arrays that are not zero; so the counters, from which the search of ratpoints corrects its moduli between the blocks, do not depend on the callback, the flags of the output or the store of the tables of rows.

Main definitions

• Ratpoints.Sieve.WalkCountsInvariant, Ratpoints.Sieve.SiftBitArrayCounts, Ratpoints.Sieve.ScanPieceCounts: the counters of the walk through a word, of the loops of the extraction of one bit array and of the scan of a piece.

Main statements

• Ratpoints.Sieve.walkWord_counters_spec: the walk through the set bits of a word adds the counts of the tests of the numerators of its set bits.
• Ratpoints.Sieve.siftBitArrayByWords_counters_spec, Ratpoints.Sieve.siftBitArrayWhole_counters_spec, Ratpoints.Sieve.siftBitArray_counters_spec: in either arm of the second stage, one bit array adds the counts of the tests of the numerators of the set bits of its words and-ed with the rows of the moduli of the second stage.
• Ratpoints.Sieve.scanPiece_counters_spec: if the bits of a piece and-ed with the rows of the second stage are a test keep of the bits, the scan of the piece adds the number of its bit arrays that are not zero and the counts of the tests of the numerators of its bits that pass keep.
• Ratpoints.Sieve.isZeroAt_eq_not_any: a bit array whose bits are a test of the bits is zero exactly when none of its bits passes the test.

Implementation notes

The file uses Lean core and Std only, as Ratpoints.Proof.Scan does. The contracts of the counters are apart from those of the delivery, which vcgen uses for the calls of the components: the proofs of the counters name the contracts of the counters of the components they call. Their loop invariants hold the counters before a return, which comes only at a stop; the counts of the tests of a candidate are irreducible, so that the verification conditions are closed by the lemmas of their lists. The contracts of the counters of the pieces, of the bits of one interval and of the sieve of one denominator are in Ratpoints.Proof.SiftBits and Ratpoints.Proof.Sift.

The counters of the walk

def Ratpoints.Sieve.WalkCountsInvariant (b : Nat) (checks : Thunk (List CheckSpec)) (x0 : UInt64) (a0 : Int) (step : Nat) (cnt0 : Counters) (k : Nat) (c : Counters) : Prop

The property of the counters c of a walk through the set bits of the word x0, lowest first, bit t standing for the numerator a0 + step t, from the counters cnt0, after the set bits below k: they are cnt0 plus the counts of the tests of a candidate of the numerators of the set bits t < k of x0, over the denominator b with the thunk checks of the third stage (Ratpoints.Sieve.testedCounts).

Equations

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

def Ratpoints.Sieve.WalkCountsWhileInvariant {σ : Type} (b : Nat) (checks : Thunk (List CheckSpec)) (x0 : UInt64) (a0 : Int) (step : Nat) (cnt0 : Counters) : Std.WP.WhileInvariant (Option (Delivery σ × Counters) × UInt64 × Delivery σ × Counters) Prop

The invariant of the while loop of Ratpoints.Sieve.walkWord for its counters, whose state is the value of a return, the word, the delivery and the counters: before a return, Ratpoints.Sieve.WalkWhileInvariant for Ratpoints.Sieve.WalkCountsInvariant; the return comes at a stop, with the flag of the delivery returned set.

Equations

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

theorem Ratpoints.Sieve.walkCountsInvariant_zero (b : Nat) (checks : Thunk (List CheckSpec)) (x0 : UInt64) (a0 : Int) (step : Nat) (cnt0 : Counters) : WalkWhileInvariant x0 (WalkCountsInvariant b checks x0 a0 step cnt0) false (cnt0, x0)

theorem Ratpoints.Sieve.WalkCountsInvariant.and_sub_one {σ : Type} {b : Nat} {checks : Thunk (List CheckSpec)} {x0 x : UInt64} {a0 : Int} {step : Nat} {cnt0 c c' : Counters} {o : Option (Delivery σ × Counters)} {mb : Nat} {ok : Bool} (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 (WalkCountsInvariant b checks x0 a0 step cnt0) false (c, x)) (hx : (x != 0) = true) (hc : (ok, c') = (accepted (a0 + ↑step * ↑x.toBitVec.ctz.toNat) b checks { words := c.words, arrays := c.arrays, bits := c.bits + 1, coprime := c.coprime, checks := c.checks, sifts := c.sifts }).run) : (x &&& x - 1).toNat < mb ∧ WalkWhileInvariant x0 (WalkCountsInvariant b checks x0 a0 step cnt0) false (c', x &&& x - 1)

A step of the walk, at the lowest set bit of x, whose numerator the test of a candidate counts after the count in bits.

theorem Ratpoints.Sieve.WalkCountsInvariant.exit {σ : Type} {b : Nat} {checks : Thunk (List CheckSpec)} {x0 x : UInt64} {a0 : Int} {step : Nat} {cnt0 c : Counters} {o : Option (Delivery σ × Counters)} {mb : Nat} (hx : ¬(x != 0) = true) (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 (WalkCountsInvariant b checks x0 a0 step cnt0) false (c, x)) : WalkWhileInvariant x0 (WalkCountsInvariant b checks x0 a0 step cnt0) true (c, x)

theorem Ratpoints.Sieve.WalkCountsInvariant.eq_of_exit {b : Nat} {checks : Thunk (List CheckSpec)} {x0 x : UInt64} {a0 : Int} {step : Nat} {cnt0 c : Counters} (h : WalkWhileInvariant x0 (WalkCountsInvariant b checks x0 a0 step cnt0) true (c, x)) : c = cnt0 + testedCounts b checks (List.map (fun (t : Nat) => a0 + ↑step * ↑t) (List.filter (fun (x : Nat) => x0.toBitVec.getLsbD x) (List.range 64)))

At the exit of the walk, the counters are those of the tests of the numerators of all the set bits of x0.

theorem Ratpoints.Sieve.walkWord_counters_spec {σ : Type} (process : Int → Int → Int → σ → Answer σ) (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) (checks : Thunk (List CheckSpec)) (x : UInt64) (a0 : Int) (step : Nat) (r : Delivery σ) (cnt : Counters) : ⦃ True ⦄ walkWord process w d b fl checks x a0 step r cnt ⦃ fun (r' : Delivery σ × Counters) => r'.fst.quit = false → r'.snd = cnt + testedCounts b checks (List.map (fun (t : Nat) => a0 + ↑step * ↑t) (List.filter (fun (x_1 : Nat) => x.toBitVec.getLsbD x_1) (List.range 64))) ⦄

When the callback does not stop the search, the walk through the set bits of a word adds to the counters the counts of the tests of a candidate of the numerators a0 + step t of its set bits t (Ratpoints.Sieve.testedCounts); the test of a candidate is read as its value.

The counters of one bit array

def Ratpoints.Sieve.SiftBitArrayCounts (words : Nat → UInt64) (b : Nat) (checks : Thunk (List CheckSpec)) (cl : NumClass) (i : Int) (cnt0 : Counters) (k : Nat) (c : Counters) : Prop

The property of the counters c of the loops of the two arms of Ratpoints.Sieve.siftBitArray over the words words κ of the bit array with the word number i, in the packing of the class cl, from the counters cnt0, after its first k words: they are cnt0 plus the counts of the tests of a candidate (Ratpoints.Sieve.testedCounts) of the numerators of the bit numbers rbaLength i + 64 κ + t of the set bits t of the words κ < k (Ratpoints.Sieve.bitNumbers), over the denominator b with the thunk checks of the third stage.

Equations

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

def Ratpoints.Sieve.SiftBitArrayCountsLoopInvariant {σ : Type} (words : Nat → UInt64) (b : Nat) (checks : Thunk (List CheckSpec)) (cl : NumClass) (i : Int) (cnt0 : Counters) : Std.WP.Invariant Nat (Option (Delivery σ × Counters) × Delivery σ × Counters) Prop

The invariant of the loop of Ratpoints.Sieve.siftBitArrayByWords over [0:rbaPack] for its counters, whose state is the value of a return, the delivery and the counters: Ratpoints.Sieve.SiftBitArrayCounts after the words done before a return; the return comes at a stop.

Equations

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

theorem Ratpoints.Sieve.map_numerator_bitNumbers_succ (words : Nat → UInt64) (cl : NumClass) (i : Int) (k : Nat) : List.map cl.numerator (bitNumbers words (↑rbaLength * i) (k + 1)) = List.map cl.numerator (bitNumbers words (↑rbaLength * i) k) ++ List.map (fun (t : Nat) => ↑cl.a0 + i * (↑rbaLength * 2 ^ cl.k) + ↑k * (64 * 2 ^ cl.k) + ↑(2 ^ cl.k) * ↑t) (List.filter (fun (x : Nat) => (words k).toBitVec.getLsbD x) (List.range 64))

Ratpoints.Sieve.flatMap_numerator_bitNumbers_succ for the numerators themselves: the numerators of the bit numbers of the set bits of the words 0, …, k are those of the words 0, …, k - 1 followed by those of word k, as the walk through it computes them.

theorem Ratpoints.Sieve.siftBitArrayCounts_zero (words : Nat → UInt64) (b : Nat) (checks : Thunk (List CheckSpec)) (cl : NumClass) (i : Int) (cnt0 : Counters) : SiftBitArrayCounts words b checks cl i cnt0 0 cnt0

theorem Ratpoints.Sieve.SiftBitArrayCounts.succ {words : Nat → UInt64} {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {i : Int} {cnt0 c c' : Counters} {k : Nat} (h : SiftBitArrayCounts words b checks cl i cnt0 k c) (hc : c' = c + testedCounts b checks (List.map (fun (t : Nat) => ↑cl.a0 + i * (↑rbaLength * 2 ^ cl.k) + ↑k * (64 * 2 ^ cl.k) + ↑(2 ^ cl.k) * ↑t) (List.filter (fun (x : Nat) => (words k).toBitVec.getLsbD x) (List.range 64)))) : SiftBitArrayCounts words b checks cl i cnt0 (k + 1) c'

The walk through word k from its first numerator adds the counts of its numerators.

theorem Ratpoints.Sieve.SiftBitArrayCounts.append {σ : Type} {words : Nat → UInt64} {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {i : Int} {cnt0 c c' : Counters} {o : Option (Delivery σ × Counters)} {done suff : List Nat} {cur : Nat} {r : Delivery σ} (h : o = none ∧ SiftBitArrayCounts words b checks cl i cnt0 done.length c) (hl : ForIn.toList [:rbaPack] = done ++ cur :: suff) (hq : ¬r.quit = true) (hc : r.quit = false → c' = c + testedCounts b checks (List.map (fun (t : Nat) => ↑cl.a0 + i * (↑rbaLength * 2 ^ cl.k) + ↑cur * (64 * 2 ^ cl.k) + ↑(2 ^ cl.k) * ↑t) (List.filter (fun (x : Nat) => (words cur).toBitVec.getLsbD x) (List.range 64)))) : SiftBitArrayCounts words b checks cl i cnt0 (done ++ [cur]).length c'

The walk through word cur of the loop over [0:rbaPack], when the callback does not stop the search in it, in the shape of the verification condition.

theorem Ratpoints.Sieve.SiftBitArrayCounts.append_of_eq_zero {σ : Type} {words : Nat → UInt64} {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {i : Int} {cnt0 c : Counters} {o : Option (Delivery σ × Counters)} {done suff : List Nat} {cur : Nat} (h : o = none ∧ SiftBitArrayCounts words b checks cl i cnt0 done.length c) (hl : ForIn.toList [:rbaPack] = done ++ cur :: suff) (hz : words cur = 0) : SiftBitArrayCounts words b checks cl i cnt0 (done ++ [cur]).length c

A word that is zero adds nothing.

theorem Ratpoints.Sieve.SiftBitArrayCounts.congr {words : Nat → UInt64} {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {i : Int} {cnt0 c : Counters} {words' : Nat → UInt64} {k : Nat} (hw : ∀ (κ : Nat), κ < k → words κ = words' κ) (h : SiftBitArrayCounts words b checks cl i cnt0 k c) : SiftBitArrayCounts words' b checks cl i cnt0 k c

The counters of the numerators of the set bits of words that agree.

theorem Ratpoints.Sieve.SiftBitArrayCounts.eq_of_rbaPack {words : Nat → UInt64} {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {i : Int} {cnt0 c : Counters} {words' : Nat → UInt64} (hw : ∀ (κ : Nat), κ < rbaPack → words κ = words' κ) (h : SiftBitArrayCounts words b checks cl i cnt0 rbaPack c) : c = cnt0 + testedCounts b checks (List.map cl.numerator (bitNumbers words' (↑rbaLength * i) rbaPack))

After all the words of the bit array, the counters are those of their numerators.

theorem Ratpoints.Sieve.SiftBitArrayCounts.eq {words : Nat → UInt64} {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {i : Int} {cnt0 c : Counters} (h : SiftBitArrayCounts words b checks cl i cnt0 (ForIn.toList [:rbaPack]).length c) : c = cnt0 + testedCounts b checks (List.map cl.numerator (bitNumbers words (↑rbaLength * i) rbaPack))

At the end of the loop over [0:rbaPack], the counters are those of the numerators of all the words of the bit array.

theorem Ratpoints.Sieve.siftBitArrayByWords_counters_spec {σ : Type} (process : Int → Int → Int → σ → Answer σ) (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (checks : Thunk (List CheckSpec)) (cl : NumClass) (i : Int) (nums : Vector UInt64 rbaPack) (r : Delivery σ) (cnt : Counters) : ⦃ StageFits specs mgs small i (i + 1) ⦄ siftBitArrayByWords process w d b fl specs mgs small checks cl i nums r cnt ⦃ fun (r' : Delivery σ × Counters) => r'.fst.quit = false → r'.snd = cnt + testedCounts b checks (List.map cl.numerator (bitNumbers (fun (κ : Nat) => andWords specs nums[κ]! i κ) (↑rbaLength * i) rbaPack)) ⦄

When the callback does not stop the search, the arm for one word at a time adds to the counters the counts of the tests of a candidate of the numerators of the set bits of the words of nums and-ed with the rows of the moduli of specs.

def Ratpoints.Sieve.SiftBitArrayWalkCounts (words : Nat → UInt64) (b : Nat) (checks : Thunk (List CheckSpec)) (cl : NumClass) (i : Int) (cnt0 : Counters) (k : Nat) (s : Counters × Int) : Prop

Ratpoints.Sieve.SiftBitArrayCounts after the words 0, …, k, with the numerator a0 of bit 0 of word k, a₀ + i (rbaLength 2 ^ cl.k) + k (64 2 ^ cl.k) as the program computes it: the invariant of the counters of the loop over the words after the first in Ratpoints.Sieve.siftBitArrayWhole.

Equations

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

def Ratpoints.Sieve.SiftBitArrayWalkCountsLoopInvariant {σ : Type} (words : Nat → UInt64) (b : Nat) (checks : Thunk (List CheckSpec)) (cl : NumClass) (i : Int) (cnt0 : Counters) : Std.WP.Invariant Nat (Option (Delivery σ × Counters) × Delivery σ × Counters × Int) Prop

The invariant of the loop of Ratpoints.Sieve.siftBitArrayWhole over [1:rbaPack] for its counters, whose state is the value of a return, the delivery, the counters and the numerator of bit 0 of the word: Ratpoints.Sieve.SiftBitArrayWalkCounts after the words done before a return; the return comes at a stop.

Equations

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

theorem Ratpoints.Sieve.siftBitArrayWalkCounts_zero {σ : Type} {words : Nat → UInt64} {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {i : Int} {cnt0 c : Counters} {r : Delivery σ} (hq : ¬r.quit = true) (hc : r.quit = false → c = cnt0 + testedCounts b checks (List.map (fun (t : Nat) => ↑cl.a0 + i * (↑rbaLength * 2 ^ cl.k) + ↑(2 ^ cl.k) * ↑t) (List.filter (fun (x : Nat) => (words 0).toBitVec.getLsbD x) (List.range 64)))) : SiftBitArrayWalkCounts words b checks cl i cnt0 [].length (c, ↑cl.a0 + i * (↑rbaLength * 2 ^ cl.k))

The walk through the first word, from the first numerator a₀ + i (rbaLength 2 ^ cl.k) of the bit array, when the callback does not stop the search in it, starts the invariant of the counters of the loop over the other words.

theorem Ratpoints.Sieve.SiftBitArrayWalkCounts.append {σ : Type} {words : Nat → UInt64} {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {i : Int} {cnt0 c c' : Counters} {o : Option (Delivery σ × Counters)} {done suff : List Nat} {cur : Nat} {a : Int} {r : Delivery σ} (h' : o = none ∧ SiftBitArrayWalkCounts words b checks cl i cnt0 done.length (c, a)) (hl : ForIn.toList [1:rbaPack] = done ++ cur :: suff) (hc : r.quit = false → c' = c + testedCounts b checks (List.map (fun (t : Nat) => a + ↑(64 * 2 ^ cl.k) + ↑(2 ^ cl.k) * ↑t) (List.filter (fun (x : Nat) => (words cur).toBitVec.getLsbD x) (List.range 64)))) (hq : ¬r.quit = true) : SiftBitArrayWalkCounts words b checks cl i cnt0 (done ++ [cur]).length (c', a + ↑(64 * 2 ^ cl.k))

The step 64 2 ^ cl.k to the first numerator of word cur of the loop over [1:rbaPack], and the walk through it from there, when the callback does not stop the search in it.

theorem Ratpoints.Sieve.SiftBitArrayWalkCounts.eq {words : Nat → UInt64} {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {i : Int} {cnt0 c : Counters} {a : Int} {words' : Nat → UInt64} (hw : ∀ (κ : Nat), κ < rbaPack → words κ = words' κ) (h : SiftBitArrayWalkCounts words b checks cl i cnt0 (ForIn.toList [1:rbaPack]).length (c, a)) : c = cnt0 + testedCounts b checks (List.map cl.numerator (bitNumbers words' (↑rbaLength * i) rbaPack))

At the end of the loop over [1:rbaPack], the counters are those of the numerators of all the words of the bit array.

theorem Ratpoints.Sieve.eq_add_testedCounts_of_isZeroAt {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {i : Int} {specs : List SieveSpec} {nums nums' : Vector UInt64 rbaPack} (hw : ∀ (κ : Nat), κ < rbaPack → nums'[κ]! = andWords specs nums[κ]! i κ) (hz : ¬(!isZeroAt nums' 0) = true) (c : Counters) : c = c + testedCounts b checks (List.map cl.numerator (bitNumbers (fun (κ : Nat) => andWords specs nums[κ]! i κ) (↑rbaLength * i) rbaPack))

When the second stage leaves the bit array zero, the words walked through have no set bits, and nothing is counted.

theorem Ratpoints.Sieve.siftBitArrayWhole_counters_spec {σ : Type} (process : Int → Int → Int → σ → Answer σ) (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (checks : Thunk (List CheckSpec)) (cl : NumClass) (i : Int) (nums : Vector UInt64 rbaPack) (r0 : Delivery σ) (cnt0 : Counters) : ⦃ StageFits specs mgs small i (i + 1) ⦄ siftBitArrayWhole process w d b fl specs mgs small checks cl i nums r0 cnt0 ⦃ fun (r' : Delivery σ × Counters) => r'.fst.quit = false → r'.snd = cnt0 + testedCounts b checks (List.map cl.numerator (bitNumbers (fun (κ : Nat) => andWords specs nums[κ]! i κ) (↑rbaLength * i) rbaPack)) ⦄

When the callback does not stop the search, the arm of the second stage on the whole bit array adds to the counters the counts of the tests of a candidate of the numerators of the set bits of the words of nums and-ed with the rows of the moduli of specs, nothing when the second stage leaves the bit array zero.

theorem Ratpoints.Sieve.siftBitArray_counters_spec {σ : Type} (process : Int → Int → Int → σ → Answer σ) (useLong : Bool) (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (checks : Thunk (List CheckSpec)) (cl : NumClass) (i : Int) (nums : Vector UInt64 rbaPack) (r : Delivery σ) (cnt : Counters) : ⦃ StageFits specs mgs small i (i + 1) ⦄ siftBitArray process useLong w d b fl specs mgs small checks cl i nums r cnt ⦃ fun (r' : Delivery σ × Counters) => r'.fst.quit = false → r'.snd = cnt + testedCounts b checks (List.map cl.numerator (bitNumbers (fun (κ : Nat) => andWords specs nums[κ]! i κ) (↑rbaLength * i) rbaPack)) ⦄

Both arms add to the counters the counts of the tests of a candidate of the numerators of the set bits of the same words, the words of nums and-ed with the rows of the moduli of specs (Ratpoints.Sieve.siftBitArrayByWords_counters_spec, Ratpoints.Sieve.siftBitArrayWhole_counters_spec), when the callback does not stop the search.

The counters of the scan of a piece

def Ratpoints.Sieve.ScanPieceCounts {m : Nat} (sv : Vector UInt64 m) (specs : List SieveSpec) (b : Nat) (checks : Thunk (List CheckSpec)) (cl : NumClass) (w0 : Int) (n : Nat) (cnt0 : Counters) (pos : Nat) (c : Counters) : Prop

The property of the counters c of the scan of Ratpoints.Sieve.scanPiece at bit array pos of the words sv, for a piece of n bit arrays from the word number w0 on and the moduli specs of the second stage with their rows, from the counters cnt0: pos ≤ n, and c is cnt0 plus the number of the bit arrays before pos that are not zero, in arrays, plus the counts of the tests of a candidate (Ratpoints.Sieve.testedCounts), over the denominator b with the thunk checks of the third stage, of the numerators in the packing of the class cl of the bits rbaLength w0 + 64 y + t of the set bits t of the words y < rbaPack pos and-ed with the rows of specs (Ratpoints.Sieve.andWords).

Equations

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

def Ratpoints.Sieve.ScanPieceCountsWhileInvariant {σ : Type} {m : Nat} (sv : Vector UInt64 m) (specs : List SieveSpec) (b : Nat) (checks : Thunk (List CheckSpec)) (cl : NumClass) (w0 : Int) (n : Nat) (cnt0 : Counters) : Std.WP.WhileInvariant (Option (Delivery σ × Counters) × Nat × Delivery σ × Counters) Prop

Ratpoints.Sieve.ScanPieceCounts as the invariant of the counters of the scan of Ratpoints.Sieve.scanPiece, whose state is the value of a return, the position, the delivery and the counters, with all n bit arrays done at the exit; the return comes at a stop.

Equations

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

def Ratpoints.Sieve.ScanPieceCountsZeroInvariant {m : Nat} (sv : Vector UInt64 m) (specs : List SieveSpec) (b : Nat) (checks : Thunk (List CheckSpec)) (cl : NumClass) (w0 : Int) (n : Nat) (cnt0 : Counters) (pos0 : Nat) (c : Counters) : Std.WP.WhileInvariant Nat Prop

The invariant of the counters of the loop of Ratpoints.Sieve.scanPiece that steps over the bit arrays that are zero, from bit array pos0 on, with the counters c of the bit arrays before pos0: the position is at least pos0, and Ratpoints.Sieve.ScanPieceCounts holds there with c.

Equations

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

theorem Ratpoints.Sieve.scanPieceCounts_zero {m : Nat} (sv : Vector UInt64 m) (specs : List SieveSpec) (b : Nat) (checks : Thunk (List CheckSpec)) (cl : NumClass) (w0 : Int) (n : Nat) (cnt0 : Counters) : ScanPieceCounts sv specs b checks cl w0 n cnt0 0 cnt0 ∧ (False → 0 = n)

theorem Ratpoints.Sieve.ScanPieceCounts.le {m : Nat} {sv : Vector UInt64 m} {specs : List SieveSpec} {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {w0 : Int} {n pos : Nat} {cnt0 c : Counters} (h : ScanPieceCounts sv specs b checks cl w0 n cnt0 pos c) : pos ≤ n

theorem Ratpoints.Sieve.ScanPieceCounts.add_one_of_isZeroAt {m : Nat} {sv : Vector UInt64 m} {specs : List SieveSpec} {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {w0 : Int} {n pos pos0 mb : Nat} {cnt0 c : Counters} {surv : Vector UInt64 m} (h : n - pos = mb ∧ pos0 ≤ pos ∧ ScanPieceCounts sv specs b checks cl w0 n cnt0 pos c ∧ (False → isZeroAt sv pos = false)) (hs : ScanPieceSentinelInvariant n surv (ForIn.toList [:rbaPack]).length sv) (hz : isZeroAt sv pos = true) : n - (pos + 1) < mb ∧ pos0 ≤ pos + 1 ∧ ScanPieceCounts sv specs b checks cl w0 n cnt0 (pos + 1) c ∧ (False → isZeroAt sv (pos + 1) = false)

A bit array that is zero adds nothing; it is not the sentinel, so that the measure n - pos of the loop that steps over the bit arrays that are zero decreases.

theorem Ratpoints.Sieve.ScanPieceCounts.add_one_of_siftBitArray {σ : Type} {m : Nat} {sv : Vector UInt64 m} {specs : List SieveSpec} {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {w0 : Int} {n pos pos0 mb : Nat} {cnt0 c c' : Counters} {o : Option (Delivery σ × Counters)} {r : Delivery σ} {c0 : Counters} (hm : n - pos0 = mb ∧ o = none ∧ ScanPieceCounts sv specs b checks cl w0 n cnt0 pos0 c0 ∧ (False → pos0 = n)) (h' : pos0 ≤ pos ∧ ScanPieceCounts sv specs b checks cl w0 n cnt0 pos c ∧ (True → isZeroAt sv pos = false)) (hlt : ¬n ≤ pos) (hc : r.quit = false → c' = { words := c.words, arrays := c.arrays + 1, bits := c.bits, coprime := c.coprime, checks := c.checks, sifts := c.sifts } + testedCounts b checks (List.map cl.numerator (bitNumbers (fun (κ : Nat) => andWords specs (Vector.ofFn fun (κ : Fin rbaPack) => sv[rbaPack * pos + ↑κ]!)[κ]! (w0 + ↑pos) κ) (↑rbaLength * (w0 + ↑pos)) rbaPack))) (hq : ¬r.quit = true) : n - (pos + 1) < mb ∧ ScanPieceCounts sv specs b checks cl w0 n cnt0 (pos + 1) c' ∧ (False → pos + 1 = n)

Bit array pos, which is not zero, copied and passed through Ratpoints.Sieve.siftBitArray with its word number w0 + pos after the count arrays one up, when the callback does not stop the search in it.

theorem Ratpoints.Sieve.ScanPieceCounts.eq {m : Nat} {sv : Vector UInt64 m} {specs : List SieveSpec} {b : Nat} {checks : Thunk (List CheckSpec)} {cl : NumClass} {w0 : Int} {n pos : Nat} {cnt0 c : Counters} {surv : Vector UInt64 m} (h : ScanPieceCounts sv specs b checks cl w0 n cnt0 pos c ∧ (True → pos = n)) (hs : ScanPieceSentinelInvariant n surv (ForIn.toList [:rbaPack]).length sv) : c = cnt0 + { arrays := (List.countP (fun (p : Nat) => !isZeroAt surv p) (List.range n)).toUInt64 } + testedCounts b checks (List.map cl.numerator (bitNumbers (fun (y : Nat) => andWords specs surv[y]! w0 y) (↑rbaLength * w0) (n * rbaPack)))

At the end of the scan, the counters are those of the bit arrays of the piece that are not zero and of the numerators of the set bits of its words and-ed with the rows, which are those of surv, since the sentinel was written past them.

theorem Ratpoints.Sieve.scanPiece_counters_spec {σ : Type} (process : Int → Int → Int → σ → Answer σ) (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (checks : Thunk (List CheckSpec)) (cl : NumClass) (w0 : Int) (n : Nat) (surv : Vector UInt64 ((n + 1) * rbaPack)) (r : Delivery σ) (cnt : Counters) : ⦃ StageFits specs mgs small w0 (w0 + ↑n) ⦄ scanPiece process w d b fl specs mgs small checks cl w0 n surv r cnt ⦃ fun (r' : Delivery σ × Counters) => ∀ (keep : Int → Bool), (∀ (y : Nat), y < n * rbaPack → ∀ (t : Nat), (andWords specs surv[y]! w0 y).toBitVec.getLsbD t = (decide (t < 64) && keep (↑rbaLength * w0 + 64 * ↑y + ↑t))) → r'.fst.quit = false → r'.snd = cnt + { arrays := (List.countP (fun (p : Nat) => !isZeroAt surv p) (List.range n)).toUInt64 } + testedCounts b checks (List.map cl.numerator (List.filter keep (List.map (fun (k : Nat) => ↑rbaLength * w0 + ↑k) (List.range (n * rbaLength))))) ⦄

The loop over the zero bit arrays ends at the sentinel at latest, so that both loops of the scan end by the measure n - pos; the test keep is quantified in the postcondition, since the program does not mention it. When the callback does not stop the search, the scan adds to the counters the number of the bit arrays of the piece that are not zero, in arrays, and the counts of the tests of a candidate (Ratpoints.Sieve.testedCounts) of the numerators of its bits that pass keep, the bits of the piece and-ed with the rows of the second stage.

theorem Ratpoints.Sieve.isZeroAt_eq_not_any {m n : Nat} {v : Vector UInt64 m} {w0 : Int} {keep : Int → Bool} (hv : ∀ (y : Nat), y < n * rbaPack → ∀ (t : Nat), v[y]!.toBitVec.getLsbD t = (decide (t < 64) && keep (↑rbaLength * w0 + 64 * ↑y + ↑t))) {pos : Nat} (hpos : pos < n) : isZeroAt v pos = !(List.range rbaLength).any fun (t : Nat) => keep (↑rbaLength * (w0 + ↑pos) + ↑t)

A bit array of the words v, among the first n, whose bits are a test keep of the bits rbaLength w0 + 64 y + t of the set bits t < 64 of the words y, for the number rbaLength of bits of a bit array (Ratpoints.rbaLength), is zero exactly when none of its bits passes keep.