The contracts of the scan of a piece

The contracts of 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, as @[spec] theorems proved with vcgen, the program logic of Lean core, with loop invariants that are named definitions. Each component hands the points it finds to the callback of the caller on a delivery (Ratpoints.Delivery), whose flag of the stop is clear at the start, and returns as soon as a call sets it; its contract says that the delivery it returns is the reference of the delivery (Ratpoints.Delivery.deliver) of the list of the points it finds, which passes over the points after the stop. The contracts speak of the bits j of the packing of a class cl (Ratpoints.Sieve.NumClass), each standing for the numerator a₀ + 2 ^ k j (Ratpoints.Sieve.NumClass.numerator), and of the words of the bit arrays and-ed with the rows of the moduli of the second stage at their offsets (Ratpoints.Sieve.andWords); the points of a numerator are those that the exact check delivers with the flags of the search (Ratpoints.Sieve.acceptedPoints).

Main definitions

• Ratpoints.Sieve.WalkDeliveryInvariant, Ratpoints.Sieve.SiftBitArrayInvariant, Ratpoints.Sieve.ScanPieceInvariant: the deliveries of the walk through a word, of the loops of the extraction of one bit array and of the scan of a piece, before a stop.

Main statements

• Ratpoints.Sieve.walkWord_spec: the walk through the set bits of a word delivers the points of the numerators a0 + step t of its set bits t, in increasing order.
• Ratpoints.Sieve.siftBitArrayByWords_spec, Ratpoints.Sieve.siftBitArrayWhole_spec, Ratpoints.Sieve.siftBitArray_spec: in either arm of the second stage, one bit array delivers the points of the numerators of the set bits of its words and-ed with the rows of the moduli of the second stage, in increasing order.
• Ratpoints.Sieve.scanPiece_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 delivers the points of the numerators of its bits that pass keep, in increasing order.

Implementation notes

The file uses Lean core and Std only, as Ratpoints.Proof.Stages, Ratpoints.Proof.Packing and Ratpoints.Proof.Delivery do. The walk reads the test of a candidate as its value (Ratpoints.Sieve.acceptedPoints), so that the contracts need nothing of the numerators and the denominator. The loops return at a stop: their invariants hold the delivery of the points found so far with the flag clear before a return, and the value returned after it, the delivery of all the points, since the reference passes over the points after the first call that sets the flag (Ratpoints.Delivery.deliver_eq_of_prefix); their verification conditions are closed by lemmas in their shape. The contracts of the counters of these components are in Ratpoints.Proof.ScanCounts; those of the pieces and of the bits of one interval are in Ratpoints.Proof.SiftBits, and that of the sieve of one denominator in Ratpoints.Proof.Sift.

The walk through the set bits of a word

def Ratpoints.Sieve.WalkDeliveryInvariant {σ : Type} (process : Int → Int → Int → σ → Answer σ) (g : Int → List (Int × Int × Int)) (x0 : UInt64) (a0 : Int) (step : Nat) (r0 : Delivery σ) (k : Nat) (r : Delivery σ) : Prop

The property of the delivery r of a walk through the set bits of the word x0, lowest first, bit t standing for the numerator a0 + step t, that delivers the list g a of the numerator a of each set bit from the delivery r0, after the set bits below k: the callback has not stopped the search, and r is the delivery of the lists of the numerators of the set bits t < k of x0, in increasing order. In Ratpoints.Sieve.walkWord, g a is the list of the points that Ratpoints.Sieve.acceptedPoints gives for the numerator a.

Equations

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

def Ratpoints.Sieve.WalkDeliveryWhileInvariant {σ : Type} (process : Int → Int → Int → σ → Answer σ) (g : Int → List (Int × Int × Int)) (x0 : UInt64) (a0 : Int) (step : Nat) (r0 : Delivery σ) : Std.WP.WhileInvariant (Option (Delivery σ × Counters) × UInt64 × Delivery σ × Counters) Prop

The invariant of the while loop of Ratpoints.Sieve.walkWord, whose state is the value of a return, the word and the delivery: before a return, Ratpoints.Sieve.WalkWhileInvariant for Ratpoints.Sieve.WalkDeliveryInvariant; after the return at a stop, the value returned is the delivery of the lists of the numerators of all the set bits of x0, since those after the stop are passed over.

Equations

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

theorem Ratpoints.Sieve.walkDeliveryInvariant_zero {σ : Type} {process : Int → Int → Int → σ → Answer σ} {r0 : Delivery σ} (g : Int → List (Int × Int × Int)) (x0 : UInt64) (a0 : Int) (step : Nat) (h : r0.quit = false) : WalkDeliveryInvariant process g x0 a0 step r0 0 r0

theorem Ratpoints.Sieve.WalkDeliveryInvariant.eq_deliver_succ {σ : Type} {process : Int → Int → Int → σ → Answer σ} {g : Int → List (Int × Int × Int)} {x0 x : UInt64} {a0 : Int} {step : Nat} {r0 r r' : Delivery σ} {k : Nat} (h : WalkDeliveryInvariant process g x0 a0 step r0 k r) (hx : ClearedBelow x0 k x) (hx0 : x ≠ 0) (hr' : r.quit = false → r' = Delivery.deliver process r (g (a0 + ↑step * ↑x.toBitVec.ctz.toNat))) : r' = Delivery.deliver process r0 (List.flatMap g (List.map (fun (t : Nat) => a0 + ↑step * ↑t) (List.filter (fun (x : Nat) => x0.toBitVec.getLsbD x) (List.range (x.toBitVec.ctz.toNat + 1)))))

The step of the walk at the lowest set bit of x, which has the bits of x0 below k cleared.

theorem Ratpoints.Sieve.WalkDeliveryInvariant.and_sub_one {σ : Type} {process : Int → Int → Int → σ → Answer σ} {g : Int → List (Int × Int × Int)} {x0 x : UInt64} {a0 : Int} {step : Nat} {r0 r r' : Delivery σ} {o : Option (Delivery σ × Counters)} {mb : Nat} (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 (WalkDeliveryInvariant process g x0 a0 step r0) false (r, x)) (hx : (x != 0) = true) (hr' : r.quit = false → r' = Delivery.deliver process r (g (a0 + ↑step * ↑x.toBitVec.ctz.toNat))) (hq : r.quit = false → r'.quit = false) : (x &&& x - 1).toNat < mb ∧ WalkWhileInvariant x0 (WalkDeliveryInvariant process g x0 a0 step r0) false (r', x &&& x - 1)

A step of the walk at which the callback does not stop the search.

theorem Ratpoints.Sieve.WalkDeliveryInvariant.eq_deliver_of_quit {σ : Type} {process : Int → Int → Int → σ → Answer σ} {g : Int → List (Int × Int × Int)} {x0 x : UInt64} {a0 : Int} {step : Nat} {r0 r r' : Delivery σ} {o : Option (Delivery σ × Counters)} {mb : Nat} (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 (WalkDeliveryInvariant process g x0 a0 step r0) false (r, x)) (hx : (x != 0) = true) (hr' : r.quit = false → r' = Delivery.deliver process r (g (a0 + ↑step * ↑x.toBitVec.ctz.toNat))) (hq : r'.quit = true) : r' = Delivery.deliver process r0 (List.flatMap g (List.map (fun (t : Nat) => a0 + ↑step * ↑t) (List.filter (fun (x : Nat) => x0.toBitVec.getLsbD x) (List.range 64))))

The step of the walk at which the callback stops the search: the delivery is that of the lists of the numerators of all the set bits, since the bits after the stop are passed over.

theorem Ratpoints.Sieve.WalkDeliveryInvariant.exit {σ : Type} {process : Int → Int → Int → σ → Answer σ} {g : Int → List (Int × Int × Int)} {x0 x : UInt64} {a0 : Int} {step : Nat} {r0 r : Delivery σ} {o : Option (Delivery σ × Counters)} {mb : Nat} (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 (WalkDeliveryInvariant process g x0 a0 step r0) false (r, x)) (hx : ¬(x != 0) = true) : WalkWhileInvariant x0 (WalkDeliveryInvariant process g x0 a0 step r0) true (r, x)

The exit of the walk, when the word is 0.

theorem Ratpoints.Sieve.WalkDeliveryInvariant.eq_deliver_of_exit {σ : Type} {process : Int → Int → Int → σ → Answer σ} {g : Int → List (Int × Int × Int)} {x0 x : UInt64} {a0 : Int} {step : Nat} {r0 r : Delivery σ} (h : WalkWhileInvariant x0 (WalkDeliveryInvariant process g x0 a0 step r0) true (r, x)) : r = Delivery.deliver process r0 (List.flatMap g (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 delivery is that of the lists of the numerators of all the set bits of x0.

theorem Ratpoints.Sieve.WalkDeliveryInvariant.and_sub_one_of_accepted {σ : Type} {process : Int → Int → Int → σ → Answer σ} {x0 x : UInt64} {a0 : Int} {step : Nat} {r0 r : Delivery σ} {o : Option (Delivery σ × Counters)} {mb : Nat} {w : Thunk (List Int)} {d b : Nat} {fl : CheckFlags} {checks : Thunk (List CheckSpec)} {cnt : Counters} (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 (WalkDeliveryInvariant process (acceptedPoints w d b fl checks) x0 a0 step r0) false (r, x)) (hx : (x != 0) = true) (hq : ¬(checkPoint process w d (↑b) fl (a0 + ↑step * ↑x.toBitVec.ctz.toNat) r).quit = true) (ha : true = (accepted (a0 + ↑step * ↑x.toBitVec.ctz.toNat) b checks cnt).run.fst) : (x &&& x - 1).toNat < mb ∧ WalkWhileInvariant x0 (WalkDeliveryInvariant process (acceptedPoints w d b fl checks) x0 a0 step r0) false (checkPoint process w d (↑b) fl (a0 + ↑step * ↑x.toBitVec.ctz.toNat) r, x &&& x - 1)

A step of the walk at a numerator that passes the test of a candidate and whose exact check does not stop the search.

theorem Ratpoints.Sieve.WalkDeliveryInvariant.and_sub_one_of_not_accepted {σ : Type} {process : Int → Int → Int → σ → Answer σ} {x0 x : UInt64} {a0 : Int} {step : Nat} {r0 r : Delivery σ} {o : Option (Delivery σ × Counters)} {mb : Nat} {w : Thunk (List Int)} {d b : Nat} {fl : CheckFlags} {checks : Thunk (List CheckSpec)} {cnt : Counters} (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 (WalkDeliveryInvariant process (acceptedPoints w d b fl checks) x0 a0 step r0) false (r, x)) (hx : (x != 0) = true) (ha : ¬(accepted (a0 + ↑step * ↑x.toBitVec.ctz.toNat) b checks cnt).run.fst = true) : (x &&& x - 1).toNat < mb ∧ WalkWhileInvariant x0 (WalkDeliveryInvariant process (acceptedPoints w d b fl checks) x0 a0 step r0) false (r, x &&& x - 1)

A step of the walk at a numerator that does not pass the test of a candidate.

theorem Ratpoints.Sieve.WalkDeliveryInvariant.eq_deliver_of_accepted_of_quit {σ : Type} {process : Int → Int → Int → σ → Answer σ} {x0 x : UInt64} {a0 : Int} {step : Nat} {r0 r : Delivery σ} {o : Option (Delivery σ × Counters)} {mb : Nat} {w : Thunk (List Int)} {d b : Nat} {fl : CheckFlags} {checks : Thunk (List CheckSpec)} {cnt : Counters} (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 (WalkDeliveryInvariant process (acceptedPoints w d b fl checks) x0 a0 step r0) false (r, x)) (hx : (x != 0) = true) (hq : (checkPoint process w d (↑b) fl (a0 + ↑step * ↑x.toBitVec.ctz.toNat) r).quit = true) (ha : true = (accepted (a0 + ↑step * ↑x.toBitVec.ctz.toNat) b checks cnt).run.fst) : checkPoint process w d (↑b) fl (a0 + ↑step * ↑x.toBitVec.ctz.toNat) r = Delivery.deliver process r0 (List.flatMap (acceptedPoints w d b fl checks) (List.map (fun (t : Nat) => a0 + ↑step * ↑t) (List.filter (fun (x : Nat) => x0.toBitVec.getLsbD x) (List.range 64))))

The step of the walk at a numerator that passes the test of a candidate and whose exact check stops the search.

theorem Ratpoints.Sieve.walkWord_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) : ⦃ r.quit = false ⦄ walkWord process w d b fl checks x a0 step r cnt ⦃ fun (r' : Delivery σ × Counters) => r'.fst = Delivery.deliver process r (List.flatMap (acceptedPoints w d b fl checks) (List.map (fun (t : Nat) => a0 + ↑step * ↑t) (List.filter (fun (x_1 : Nat) => x.toBitVec.getLsbD x_1) (List.range 64)))) ⦄

The loop ends, since clearing the lowest set bit makes a word other than 0 smaller, or at a stop; the test of a candidate is read as its value, Ratpoints.Sieve.acceptedPoints.

The second stage and the extraction of one bit array

def Ratpoints.Sieve.SiftBitArrayInvariant {σ : Type} (process : Int → Int → Int → σ → Answer σ) (words : Nat → UInt64) (g : Int → List (Int × Int × Int)) (cl : NumClass) (i : Int) (r0 : Delivery σ) (k : Nat) (r : Delivery σ) : Prop

The invariant of the loops of the two arms of Ratpoints.Sieve.siftBitArray over the words of the bit array with the word number i, after its first k words, for the words words κ that the walks go through, the class cl and the points g a of a numerator a, from the delivery r0: the callback has not stopped the search, and r is the delivery of the points of the numerators of the bit numbers rbaLength i + 64 κ + t of the set bits t of the words κ < k (Ratpoints.Sieve.bitNumbers) in the packing of cl (Ratpoints.Sieve.NumClass.numerator), in increasing order. The invariant of the scan of a piece (Ratpoints.Sieve.ScanPieceInvariant) is this one for the words of the piece from its first word number on.

Equations

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

def Ratpoints.Sieve.SiftBitArrayWalkInvariant {σ : Type} (process : Int → Int → Int → σ → Answer σ) (words : Nat → UInt64) (g : Int → List (Int × Int × Int)) (cl : NumClass) (i : Int) (r0 : Delivery σ) (k : Nat) (s : Delivery σ × Int) : Prop

Ratpoints.Sieve.SiftBitArrayInvariant 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, for the stride 2 ^ cl.k of the class: the invariant of the loop over the words after the first in the arm of the second stage on the whole bit array (Ratpoints.Sieve.siftBitArrayWhole), which steps a0 from one word to the next before it walks through the word, as the C code does.

Equations

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

def Ratpoints.Sieve.SiftBitArrayLoopInvariant {σ : Type} (process : Int → Int → Int → σ → Answer σ) (words : Nat → UInt64) (g : Int → List (Int × Int × Int)) (cl : NumClass) (i : Int) (r0 : Delivery σ) : Std.WP.Invariant Nat (Option (Delivery σ × Counters) × Delivery σ × Counters) Prop

The invariant of the loop of Ratpoints.Sieve.siftBitArrayByWords over [0:rbaPack], whose state is the value of a return and the delivery: before a return, Ratpoints.Sieve.SiftBitArrayInvariant after the words done; after the return at a stop, the value returned is the delivery of the points of the numerators of the set bits of all the words of the bit array.

Equations

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

def Ratpoints.Sieve.SiftBitArrayWalkLoopInvariant {σ : Type} (process : Int → Int → Int → σ → Answer σ) (words : Nat → UInt64) (g : Int → List (Int × Int × Int)) (cl : NumClass) (i : Int) (r0 : Delivery σ) : Std.WP.Invariant Nat (Option (Delivery σ × Counters) × Delivery σ × Counters × Int) Prop

The invariant of the loop of Ratpoints.Sieve.siftBitArrayWhole over [1:rbaPack], whose state is the value of a return, the delivery and the numerator of bit 0 of the word: Ratpoints.Sieve.SiftBitArrayWalkInvariant after the words done before a return, and after the return at a stop the delivery of the points of the numerators of the set bits of all the words of the bit array as the value returned.

Equations

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

theorem Ratpoints.Sieve.flatMap_numerator_bitNumbers_succ (words : Nat → UInt64) {β : Type} (g : Int → List β) (cl : NumClass) (i : Int) (k : Nat) : List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers words (↑rbaLength * i) (k + 1)) = List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers words (↑rbaLength * i) k) ++ List.flatMap g (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)))

The points of 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, whose numerators the walk through it computes from the numerator a₀ + i (rbaLength 2 ^ cl.k) + k (64 2 ^ cl.k) of its bit 0.

theorem Ratpoints.Sieve.SiftBitArrayInvariant.quit_eq_false {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 r : Delivery σ} {k : Nat} {o : Option (Delivery σ × Counters)} (h : o = none ∧ SiftBitArrayInvariant process words g cl i r0 k r) : r.quit = false

theorem Ratpoints.Sieve.siftBitArrayInvariant_zero {σ : Type} {process : Int → Int → Int → σ → Answer σ} {r0 : Delivery σ} (words : Nat → UInt64) (g : Int → List (Int × Int × Int)) (cl : NumClass) (i : Int) (h : r0.quit = false) : SiftBitArrayInvariant process words g cl i r0 0 r0

theorem Ratpoints.Sieve.SiftBitArrayInvariant.deliver_of_flatMap_eq {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 r : Delivery σ} {k k' : Nat} {D : List (Int × Int × Int)} (h : SiftBitArrayInvariant process words g cl i r0 k r) (hD : List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers words (↑rbaLength * i) k') = List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers words (↑rbaLength * i) k) ++ D) (hq : ¬(Delivery.deliver process r D).quit = true) : SiftBitArrayInvariant process words g cl i r0 k' (Delivery.deliver process r D)

The delivery of the list D of the points that follow those of the bit numbers of the words before k among those of the words before k', when the callback does not stop the search in it.

theorem Ratpoints.Sieve.SiftBitArrayInvariant.deliver_eq_of_quit {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 r : Delivery σ} {k k' m : Nat} {D : List (Int × Int × Int)} (h : SiftBitArrayInvariant process words g cl i r0 k r) (hD : List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers words (↑rbaLength * i) k') = List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers words (↑rbaLength * i) k) ++ D) (hk' : k' ≤ m) (hq : (Delivery.deliver process r D).quit = true) : Delivery.deliver process r D = Delivery.deliver process r0 (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers words (↑rbaLength * i) m))

The delivery of the list D of the points that follow those of the bit numbers of the words before k among those of the words before k', when the callback stops the search in it: the delivery is that of the points of the words before any m ≥ k', since the points after the stop are passed over.

theorem Ratpoints.Sieve.SiftBitArrayInvariant.succ {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 r : Delivery σ} {k : Nat} (h : SiftBitArrayInvariant process words g cl i r0 k r) (hq : ¬(Delivery.deliver process r (List.flatMap g (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))))).quit = true) : SiftBitArrayInvariant process words g cl i r0 (k + 1) (Delivery.deliver process r (List.flatMap g (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)))))

The walk through word k from its first numerator, when the callback does not stop the search in it.

theorem Ratpoints.Sieve.SiftBitArrayInvariant.append {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 r : Delivery σ} {done suff : List Nat} {cur : Nat} {o : Option (Delivery σ × Counters)} (h : o = none ∧ SiftBitArrayInvariant process words g cl i r0 done.length r) (hl : ForIn.toList [:rbaPack] = done ++ cur :: suff) (hq : ¬(Delivery.deliver process r (List.flatMap g (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))))).quit = true) : SiftBitArrayInvariant process words g cl i r0 (done ++ [cur]).length (Delivery.deliver process r (List.flatMap g (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)))))

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

theorem Ratpoints.Sieve.SiftBitArrayInvariant.append_of_eq_zero {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 r : Delivery σ} {done suff : List Nat} {cur : Nat} {o : Option (Delivery σ × Counters)} (h' : o = none ∧ SiftBitArrayInvariant process words g cl i r0 done.length r) (hl : ForIn.toList [:rbaPack] = done ++ cur :: suff) (hz : words cur = 0) : SiftBitArrayInvariant process words g cl i r0 (done ++ [cur]).length r

A word that is zero adds nothing.

theorem Ratpoints.Sieve.SiftBitArrayInvariant.eq_deliver_of_quit_append {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 r : Delivery σ} {done suff : List Nat} {cur : Nat} {o : Option (Delivery σ × Counters)} (h : o = none ∧ SiftBitArrayInvariant process words g cl i r0 done.length r) (hl : ForIn.toList [:rbaPack] = done ++ cur :: suff) (hq : (Delivery.deliver process r (List.flatMap g (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))))).quit = true) : Delivery.deliver process r (List.flatMap g (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)))) = Delivery.deliver process r0 (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers words (↑rbaLength * i) rbaPack))

The walk through word cur of the loop over [0:rbaPack], when the callback stops the search in it: the delivery is that of all the words of the bit array.

theorem Ratpoints.Sieve.SiftBitArrayInvariant.eq_deliver {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 r : Delivery σ} (h : SiftBitArrayInvariant process words g cl i r0 (ForIn.toList [:rbaPack]).length r) : r = Delivery.deliver process r0 (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers words (↑rbaLength * i) rbaPack))

At the end of the loop over [0:rbaPack], the delivery is that of all the words of the bit array.

theorem Ratpoints.Sieve.siftBitArrayWalkInvariant_zero {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 : Delivery σ} (hr : r0.quit = false) (hq : ¬(Delivery.deliver process r0 (List.flatMap g (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))))).quit = true) : SiftBitArrayWalkInvariant process words g cl i r0 0 (Delivery.deliver process r0 (List.flatMap g (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)))), ↑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 loop over the other words.

theorem Ratpoints.Sieve.add_eq_numerator_succ {cl : NumClass} {i a : Int} {k : Nat} (ha : a = ↑cl.a0 + i * (↑rbaLength * 2 ^ cl.k) + ↑k * (64 * 2 ^ cl.k)) : a + ↑(64 * 2 ^ cl.k) = ↑cl.a0 + i * (↑rbaLength * 2 ^ cl.k) + ↑(k + 1) * (64 * 2 ^ cl.k)

The numerator of bit 0 of word k + 1, stepped by 64 2 ^ cl.k from that of word k, as the walk through the words of a bit array computes it.

theorem Ratpoints.Sieve.SiftBitArrayWalkInvariant.quit_eq_false {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 : Delivery σ} {k : Nat} {s : Delivery σ × Int} {o : Option (Delivery σ × Counters)} (h : o = none ∧ SiftBitArrayWalkInvariant process words g cl i r0 k s) : s.fst.quit = false

theorem Ratpoints.Sieve.SiftBitArrayWalkInvariant.append {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 : Delivery σ} {done suff : List Nat} {cur : Nat} {s : Delivery σ × Int} {o : Option (Delivery σ × Counters)} (h' : o = none ∧ SiftBitArrayWalkInvariant process words g cl i r0 done.length s) (hl : ForIn.toList [1:rbaPack] = done ++ cur :: suff) (hq : ¬(Delivery.deliver process s.fst (List.flatMap g (List.map (fun (t : Nat) => s.snd + ↑(64 * 2 ^ cl.k) + ↑(2 ^ cl.k) * ↑t) (List.filter (fun (x : Nat) => (words cur).toBitVec.getLsbD x) (List.range 64))))).quit = true) : SiftBitArrayWalkInvariant process words g cl i r0 (done ++ [cur]).length (Delivery.deliver process s.fst (List.flatMap g (List.map (fun (t : Nat) => s.snd + ↑(64 * 2 ^ cl.k) + ↑(2 ^ cl.k) * ↑t) (List.filter (fun (x : Nat) => (words cur).toBitVec.getLsbD x) (List.range 64)))), s.snd + ↑(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.SiftBitArrayWalkInvariant.eq_deliver_of_quit {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 : Delivery σ} {done suff : List Nat} {cur : Nat} {s : Delivery σ × Int} {o : Option (Delivery σ × Counters)} (h' : o = none ∧ SiftBitArrayWalkInvariant process words g cl i r0 done.length s) (hl : ForIn.toList [1:rbaPack] = done ++ cur :: suff) (hq : (Delivery.deliver process s.fst (List.flatMap g (List.map (fun (t : Nat) => s.snd + ↑(64 * 2 ^ cl.k) + ↑(2 ^ cl.k) * ↑t) (List.filter (fun (x : Nat) => (words cur).toBitVec.getLsbD x) (List.range 64))))).quit = true) : Delivery.deliver process s.fst (List.flatMap g (List.map (fun (t : Nat) => s.snd + ↑(64 * 2 ^ cl.k) + ↑(2 ^ cl.k) * ↑t) (List.filter (fun (x : Nat) => (words cur).toBitVec.getLsbD x) (List.range 64)))) = Delivery.deliver process r0 (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers words (↑rbaLength * i) rbaPack))

The walk through word cur of the loop over [1:rbaPack], when the callback stops the search in it: the delivery is that of all the words of the bit array.

theorem Ratpoints.Sieve.SiftBitArrayWalkInvariant.eq_deliver {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 : Delivery σ} {s : Delivery σ × Int} {words' : Nat → UInt64} (hw : ∀ (κ : Nat), κ < rbaPack → words κ = words' κ) (h : SiftBitArrayWalkInvariant process words g cl i r0 (ForIn.toList [1:rbaPack]).length s) : s.fst = Delivery.deliver process r0 (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers words' (↑rbaLength * i) rbaPack))

At the end of the loop over [1:rbaPack], the delivery is that of all the words of the bit array.

theorem Ratpoints.Sieve.eq_deliver_of_quit_of_forall_eq {σ : Type} {process : Int → Int → Int → σ → Answer σ} {words : Nat → UInt64} {g : Int → List (Int × Int × Int)} {cl : NumClass} {i : Int} {r0 : Delivery σ} {words' : Nat → UInt64} (hr : r0.quit = false) (hw : ∀ (κ : Nat), κ < rbaPack → words κ = words' κ) (hq : (Delivery.deliver process r0 (List.flatMap g (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))))).quit = true) : Delivery.deliver process r0 (List.flatMap g (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)))) = Delivery.deliver process r0 (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers words' (↑rbaLength * i) rbaPack))

The walk through the first word of words that agree with words', from the first numerator a₀ + i (rbaLength 2 ^ cl.k) of the bit array, when the callback stops the search in it: the delivery is that of all the words of words'.

theorem Ratpoints.Sieve.eq_deliver_of_isZeroAt {σ : Type} {process : Int → Int → Int → σ → Answer σ} {g : Int → List (Int × Int × Int)} {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) (r : Delivery σ) : r = Delivery.deliver process r (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers (fun (κ : Nat) => andWords specs nums[κ]! i κ) (↑rbaLength * i) rbaPack))

The words of a bit array that the second stage leaves zero have no set bits: nothing is delivered.

theorem Ratpoints.Sieve.siftBitArrayByWords_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) : ⦃ r.quit = false ∧ 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 = Delivery.deliver process r (List.flatMap (fun (j : Int) => acceptedPoints w d b fl checks (cl.numerator j)) (bitNumbers (fun (κ : Nat) => andWords specs nums[κ]! i κ) (↑rbaLength * i) rbaPack)) ⦄

The arm for one word at a time walks through the set bits of the words of nums and-ed with the rows of the moduli of specs (Ratpoints.Sieve.secondStageWord_spec), each bit j standing for the numerator a₀ + 2 ^ k j of the class cl, and skips a word that is zero, which loses nothing; it returns at a stop.

theorem Ratpoints.Sieve.siftBitArrayWhole_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 σ) (cnt : Counters) : ⦃ r0.quit = false ∧ StageFits specs mgs small i (i + 1) ⦄ siftBitArrayWhole process w d b fl specs mgs small checks cl i nums r0 cnt ⦃ fun (r' : Delivery σ × Counters) => r'.fst = Delivery.deliver process r0 (List.flatMap (fun (j : Int) => acceptedPoints w d b fl checks (cl.numerator j)) (bitNumbers (fun (κ : Nat) => andWords specs nums[κ]! i κ) (↑rbaLength * i) rbaPack)) ⦄

The arm of the second stage on the whole bit array walks through the set bits of the words of nums and-ed with the rows of the moduli of specs (Ratpoints.Sieve.secondStage_spec), each bit j standing for the numerator a₀ + 2 ^ k j of the class cl, and skips the walks when the second stage leaves the bit array zero, which loses nothing; it returns at a stop.

theorem Ratpoints.Sieve.siftBitArray_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) : ⦃ r.quit = false ∧ 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 = Delivery.deliver process r (List.flatMap (fun (j : Int) => acceptedPoints w d b fl checks (cl.numerator j)) (bitNumbers (fun (κ : Nat) => andWords specs nums[κ]! i κ) (↑rbaLength * i) rbaPack)) ⦄

Both arms deliver the points 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_spec, Ratpoints.Sieve.siftBitArrayWhole_spec).

The scan of a piece

def Ratpoints.Sieve.ScanPieceSentinelInvariant {m : Nat} (n : Nat) (surv : Vector UInt64 m) (k : Nat) (sv : Vector UInt64 m) : Prop

The invariant of the loop of Ratpoints.Sieve.scanPiece that writes the sentinel into bit array n of surv: the words of the piece are those of surv, and the first k words of bit array n are all ones.

Equations

• Ratpoints.Sieve.ScanPieceSentinelInvariant n surv k sv = ((∀ (y : Nat), y < n * Ratpoints.rbaPack → sv[y]! = surv[y]!) ∧ ∀ (κ : Nat), κ < k → sv[Ratpoints.rbaPack * n + κ]! = ~~~0)

def Ratpoints.Sieve.ScanPieceInvariant {σ : Type} (process : Int → Int → Int → σ → Answer σ) {m : Nat} (sv : Vector UInt64 m) (specs : List SieveSpec) (g : Int → List (Int × Int × Int)) (cl : NumClass) (w0 : Int) (n : Nat) (r0 : Delivery σ) (pos : Nat) (r : Delivery σ) : Prop

The invariant 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, the moduli specs of the second stage with their rows and the points g a of the numerator a of a bit in the packing of the class cl (in the scan, those of Ratpoints.Sieve.acceptedPoints), from the delivery r0: pos ≤ n, the callback has not stopped the search, and r is the delivery of the points 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), in increasing order: the invariant of the extraction of one bit array (Ratpoints.Sieve.SiftBitArrayInvariant) for the words of the piece from w0 on.

Equations

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

def Ratpoints.Sieve.ScanPieceWhileInvariant {σ : Type} (process : Int → Int → Int → σ → Answer σ) {m : Nat} (sv : Vector UInt64 m) (specs : List SieveSpec) (g : Int → List (Int × Int × Int)) (cl : NumClass) (w0 : Int) (n : Nat) (r0 : Delivery σ) : Std.WP.WhileInvariant (Option (Delivery σ × Counters) × Nat × Delivery σ × Counters) Prop

Ratpoints.Sieve.ScanPieceInvariant as the invariant of the scan of Ratpoints.Sieve.scanPiece, whose state is the value of a return, the position and the delivery, with all n bit arrays done at the exit; after the return at a stop, the value returned is the delivery of the points of all the bit arrays of the piece.

Equations

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

def Ratpoints.Sieve.ScanPieceZeroInvariant {σ : Type} (process : Int → Int → Int → σ → Answer σ) {m : Nat} (sv : Vector UInt64 m) (specs : List SieveSpec) (g : Int → List (Int × Int × Int)) (cl : NumClass) (w0 : Int) (n : Nat) (r0 : Delivery σ) (pos0 : Nat) (r : Delivery σ) : Std.WP.WhileInvariant Nat Prop

The invariant of the loop of Ratpoints.Sieve.scanPiece that steps over the bit arrays that are zero, from bit array pos0 on, with the delivery r of the bit arrays before pos0: the position is at least pos0, and Ratpoints.Sieve.ScanPieceInvariant holds there with r, since a bit array that is zero has no set bits.

Equations

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

theorem Ratpoints.Sieve.scanPieceSentinelInvariant_zero {m : Nat} (n : Nat) (surv : Vector UInt64 m) : ScanPieceSentinelInvariant n surv 0 surv

theorem Ratpoints.Sieve.ScanPieceSentinelInvariant.append_set! {n : Nat} {surv sv : Vector UInt64 ((n + 1) * rbaPack)} {done suff : List Nat} {cur : Nat} (h : ScanPieceSentinelInvariant n surv done.length sv) (hl : ForIn.toList [:rbaPack] = done ++ cur :: suff) : ScanPieceSentinelInvariant n surv (done ++ [cur]).length (sv.set! (rbaPack * n + cur) (~~~0))

theorem Ratpoints.Sieve.ScanPieceSentinelInvariant.ne_of_isZeroAt {m n : Nat} {surv sv : Vector UInt64 m} (h : ScanPieceSentinelInvariant n surv (ForIn.toList [:rbaPack]).length sv) {pos : Nat} (hz : isZeroAt sv pos = true) : pos ≠ n

A bit array that is zero is not the sentinel, whose words are all ones.

theorem Ratpoints.Sieve.ScanPieceSentinelInvariant.bitNumbers_eq {m n : Nat} {surv sv : Vector UInt64 m} (hs : ScanPieceSentinelInvariant n surv (ForIn.toList [:rbaPack]).length sv) (specs : List SieveSpec) (w0 : Int) : bitNumbers (fun (y : Nat) => andWords specs sv[y]! w0 y) (↑rbaLength * w0) (rbaPack * n) = bitNumbers (fun (y : Nat) => andWords specs surv[y]! w0 y) (↑rbaLength * w0) (n * rbaPack)

The bit numbers of the set bits of the words of a piece before the sentinel are those of the words of surv, since the sentinel was written past them.

theorem Ratpoints.Sieve.ScanPieceSentinelInvariant.isZeroAt_eq {m n : Nat} {surv sv : Vector UInt64 m} (hs : ScanPieceSentinelInvariant n surv (ForIn.toList [:rbaPack]).length sv) {p : Nat} (hp : p < n) : isZeroAt sv p = isZeroAt surv p

The bit arrays of a piece before the sentinel are those of surv, since the sentinel was written past them.

theorem Ratpoints.Sieve.bitNumbers_rbaPack_mul_succ {m : Nat} (sv : Vector UInt64 m) (specs : List SieveSpec) (w0 : Int) (pos : Nat) : bitNumbers (fun (y : Nat) => andWords specs sv[y]! w0 y) (↑rbaLength * w0) (rbaPack * (pos + 1)) = bitNumbers (fun (y : Nat) => andWords specs sv[y]! w0 y) (↑rbaLength * w0) (rbaPack * pos) ++ bitNumbers (fun (κ : Nat) => andWords specs (Vector.ofFn fun (κ : Fin rbaPack) => sv[rbaPack * pos + ↑κ]!)[κ]! (w0 + ↑pos) κ) (↑rbaLength * (w0 + ↑pos)) rbaPack

The bit numbers of the set bits of the first pos + 1 bit arrays of a piece are those of the first pos followed by those of bit array pos, copied and passed through Ratpoints.Sieve.siftBitArray with its word number w0 + pos.

theorem Ratpoints.Sieve.ScanPieceInvariant.le {σ : Type} {process : Int → Int → Int → σ → Answer σ} {m : Nat} {sv : Vector UInt64 m} {specs : List SieveSpec} {cl : NumClass} {g : Int → List (Int × Int × Int)} {w0 : Int} {n pos : Nat} {r0 r : Delivery σ} (h : ScanPieceInvariant process sv specs g cl w0 n r0 pos r) : pos ≤ n

theorem Ratpoints.Sieve.scanPieceInvariant_zero {σ : Type} {process : Int → Int → Int → σ → Answer σ} {m : Nat} {r0 : Delivery σ} (sv : Vector UInt64 m) (specs : List SieveSpec) (g : Int → List (Int × Int × Int)) (cl : NumClass) (w0 : Int) (n : Nat) (h : r0.quit = false) : ScanPieceInvariant process sv specs g cl w0 n r0 0 r0

theorem Ratpoints.Sieve.ScanPieceInvariant.add_one_of_siftBitArray {σ : Type} {process : Int → Int → Int → σ → Answer σ} {m : Nat} {sv : Vector UInt64 m} {specs : List SieveSpec} {cl : NumClass} {g : Int → List (Int × Int × Int)} {w0 : Int} {n pos : Nat} {r0 r : Delivery σ} {pos0 mb : Nat} {o : Option (Delivery σ × Counters)} {r' : Delivery σ} (hm : n - pos0 = mb ∧ o = none ∧ ScanPieceInvariant process sv specs g cl w0 n r0 pos0 r' ∧ (False → pos0 = n)) (h' : pos0 ≤ pos ∧ ScanPieceInvariant process sv specs g cl w0 n r0 pos r) (hlt : ¬n ≤ pos) (hq : ¬(Delivery.deliver process r (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers (fun (κ : Nat) => andWords specs (Vector.ofFn fun (κ : Fin rbaPack) => sv[rbaPack * pos + ↑κ]!)[κ]! (w0 + ↑pos) κ) (↑rbaLength * (w0 + ↑pos)) rbaPack))).quit = true) : n - (pos + 1) < mb ∧ ScanPieceInvariant process sv specs g cl w0 n r0 (pos + 1) (Delivery.deliver process r (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers (fun (κ : Nat) => andWords specs (Vector.ofFn fun (κ : Fin rbaPack) => sv[rbaPack * pos + ↑κ]!)[κ]! (w0 + ↑pos) κ) (↑rbaLength * (w0 + ↑pos)) rbaPack))) ∧ (False → pos + 1 = n)

Bit array pos, copied and passed through Ratpoints.Sieve.siftBitArray with its word number w0 + pos, when the callback does not stop the search in it.

theorem Ratpoints.Sieve.ScanPieceInvariant.eq_deliver_of_quit {σ : Type} {process : Int → Int → Int → σ → Answer σ} {m : Nat} {sv : Vector UInt64 m} {specs : List SieveSpec} {cl : NumClass} {g : Int → List (Int × Int × Int)} {w0 : Int} {n pos : Nat} {r0 r : Delivery σ} {pos0 : Nat} (h' : pos0 ≤ pos ∧ ScanPieceInvariant process sv specs g cl w0 n r0 pos r) (hlt : ¬n ≤ pos) (hq : (Delivery.deliver process r (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers (fun (κ : Nat) => andWords specs (Vector.ofFn fun (κ : Fin rbaPack) => sv[rbaPack * pos + ↑κ]!)[κ]! (w0 + ↑pos) κ) (↑rbaLength * (w0 + ↑pos)) rbaPack))).quit = true) : Delivery.deliver process r (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers (fun (κ : Nat) => andWords specs (Vector.ofFn fun (κ : Fin rbaPack) => sv[rbaPack * pos + ↑κ]!)[κ]! (w0 + ↑pos) κ) (↑rbaLength * (w0 + ↑pos)) rbaPack)) = Delivery.deliver process r0 (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers (fun (y : Nat) => andWords specs sv[y]! w0 y) (↑rbaLength * w0) (rbaPack * n)))

Bit array pos, copied and passed through Ratpoints.Sieve.siftBitArray with its word number w0 + pos, when the callback stops the search in it: the delivery is that of the whole piece.

theorem Ratpoints.Sieve.ScanPieceInvariant.add_one_of_isZeroAt {σ : Type} {process : Int → Int → Int → σ → Answer σ} {m : Nat} {sv : Vector UInt64 m} {specs : List SieveSpec} {cl : NumClass} {g : Int → List (Int × Int × Int)} {w0 : Int} {n pos : Nat} {r0 r : Delivery σ} {surv : Vector UInt64 m} {pos0 mb : Nat} (h : n - pos = mb ∧ pos0 ≤ pos ∧ ScanPieceInvariant process sv specs g cl w0 n r0 pos r) (hs : ScanPieceSentinelInvariant n surv (ForIn.toList [:rbaPack]).length sv) (hz : isZeroAt sv pos = true) : n - (pos + 1) < mb ∧ pos0 ≤ pos + 1 ∧ ScanPieceInvariant process sv specs g cl w0 n r0 (pos + 1) r

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.ScanPieceInvariant.quit_eq_false {σ : Type} {process : Int → Int → Int → σ → Answer σ} {m : Nat} {sv : Vector UInt64 m} {specs : List SieveSpec} {cl : NumClass} {g : Int → List (Int × Int × Int)} {w0 : Int} {n pos : Nat} {r0 r : Delivery σ} {pos0 : Nat} (h : pos0 ≤ pos ∧ ScanPieceInvariant process sv specs g cl w0 n r0 pos r) : r.quit = false

theorem Ratpoints.Sieve.ScanPieceSentinelInvariant.eq_deliver_of_eq {σ : Type} {process : Int → Int → Int → σ → Answer σ} {m : Nat} {sv : Vector UInt64 m} {specs : List SieveSpec} {cl : NumClass} {g : Int → List (Int × Int × Int)} {w0 : Int} {n : Nat} {r0 : Delivery σ} {surv : Vector UInt64 m} {r' : Delivery σ} (h : r' = Delivery.deliver process r0 (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers (fun (y : Nat) => andWords specs sv[y]! w0 y) (↑rbaLength * w0) (rbaPack * n)))) (hs : ScanPieceSentinelInvariant n surv (ForIn.toList [:rbaPack]).length sv) : r' = Delivery.deliver process r0 (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers (fun (y : Nat) => andWords specs surv[y]! w0 y) (↑rbaLength * w0) (n * rbaPack)))

The value returned at a stop in the scan, the delivery of the points of the bits of the words before the sentinel, is the delivery of those of the words of surv.

theorem Ratpoints.Sieve.ScanPieceInvariant.eq_deliver {σ : Type} {process : Int → Int → Int → σ → Answer σ} {m : Nat} {sv : Vector UInt64 m} {specs : List SieveSpec} {cl : NumClass} {g : Int → List (Int × Int × Int)} {w0 : Int} {n pos : Nat} {r0 r : Delivery σ} {surv : Vector UInt64 m} (h : ScanPieceInvariant process sv specs g cl w0 n r0 pos r ∧ (True → pos = n)) (hs : ScanPieceSentinelInvariant n surv (ForIn.toList [:rbaPack]).length sv) : r = Delivery.deliver process r0 (List.flatMap (fun (j : Int) => g (cl.numerator j)) (bitNumbers (fun (y : Nat) => andWords specs surv[y]! w0 y) (↑rbaLength * w0) (n * rbaPack)))

At the end of the scan, the delivery is that of the points of the set bits of the words of the piece and-ed with the rows, which are those of surv, since the sentinel was written past them.

theorem Ratpoints.Sieve.scanPiece_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) : ⦃ r.quit = false ∧ 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 = Delivery.deliver process r (List.flatMap (fun (j : Int) => acceptedPoints w d b fl checks (cl.numerator j)) (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 the 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.