The loops of the shapes over a block

The loops of the four shapes over the steps of a block (Ratpoints.Sieve.squaresBlock, Ratpoints.Sieve.squares1Block, Ratpoints.Sieve.wordsBlock, Ratpoints.Sieve.allBlock, with the walk through the set bits of a word Ratpoints.Sieve.walkDens, the positions of the forbidden divisors at the first word Ratpoints.Sieve.forbStarts and the word of the denominators Ratpoints.Sieve.denWord), and the dispatch over the shapes (Ratpoints.Sieve.Shape.blockLoop), each for any step that sifts a denominator: when the step delivers the lists L x b of the denominator b, for every x with P x, keeps a property Q of the store of the tables of rows and adds the counts κ b to the counters when the callback does not stop the search, the loop delivers the lists of the denominators of its steps that pass the tests of the shape, in order, keeps Q, and adds their counts (Ratpoints.Sieve.BlockPost). The search for the decision in force for a block ends at the decision in force for it (Ratpoints.Sieve.Decision.InForce), the last whose first block is at most the block (Ratpoints.Sieve.findDecision_spec).

Main definitions

• Ratpoints.Sieve.BlockPost, Ratpoints.Sieve.BlockInv: what a loop of a block does to its state, and the invariant of the loops.
• Ratpoints.Sieve.ForbFits, Ratpoints.Sieve.PosAt: forbidden divisors tested with words whose positions at the first word of a block Ratpoints.Sieve.forbStarts finds, and their positions at a word.
• Ratpoints.Sieve.wordDens: the denominators of a word of the word shape.
• Ratpoints.Sieve.Shape.stepDens, Ratpoints.Sieve.Shape.ForbFits, Ratpoints.Sieve.Shape.LoopFits: the denominators of a step of a shape, and what the loops of the shapes need.
• Ratpoints.Sieve.Decision.InForce: the decision in force for a block.

Main statements

• Ratpoints.Sieve.squaresBlock_spec, Ratpoints.Sieve.squares1Block_spec, Ratpoints.Sieve.allBlock_spec, Ratpoints.Sieve.walkDens_spec, Ratpoints.Sieve.wordsBlock_spec: the contracts of the loops of the shapes over a block, for the contract of the step as a hypothesis.
• Ratpoints.Sieve.posAt_forbStarts, Ratpoints.Sieve.denWord_spec: the positions of the forbidden divisors at the first word of a block, and the word of the denominators of a word, that of Ratpoints.Sieve.wordBits, with the positions at the next word.
• Ratpoints.Sieve.Shape.blockLoop_spec: the loop of a shape over a block delivers the lists of the denominators of its steps (Ratpoints.Sieve.Shape.stepDens) that pass the tests of the shape.
• Ratpoints.Sieve.findDecision_spec: the decision in force for a block.

Implementation notes

The loops with a cursor (repeat, while) end by measures: the steps left for the loops of a block over a ≤ e, the word for the walk, the index for the search of the decision. The deliveries are stated for a family L x of lists with a property P x, since the run states its delivery for every choice of the words of the classes and the ranges of the numerators, which the program does not mention.

structure Ratpoints.Sieve.BlockPost {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) {ι : Type} (P : ι → Prop) (L : ι → ℕ → List (ℤ × ℤ × ℤ)) (κ : ℕ → Counters) (Q : RowStore → Prop) (M : List ℕ) (st st' : BlockState σ) : Prop

What a loop over the denominators M of a block does to its state, from st to st', for a step that delivers the points L b of each denominator b, keeps the property Q of the store of the tables of rows and adds the counts κ b to the counters: the delivery is that of the points of the denominators of M in order, the store has the property Q, and when the callback has not stopped the search, the counters are those of st plus the counts of the denominators of M.

• deliver (x : ι) : P x → st'.1 = Delivery.deliver process st.1 (List.flatMap (L x) M)

  The delivery is that of the points of the denominators of M, for every x with P x.

• store : Q st'.2.1

  The store has the property Q.

• counts : st'.1.quit = false → st'.2.2 = List.foldl (fun (x1 x2 : Counters) => x1 + x2) st.2.2 (List.map κ M)

  While the callback has not stopped the search, the counts of the denominators of M are added to the counters.

structure Ratpoints.Sieve.BlockInv {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) {ι : Type} (P : ι → Prop) (L : ι → ℕ → List (ℤ × ℤ × ℤ)) (κ : ℕ → Counters) (Q : RowStore → Prop) (st0 : BlockState σ) (M : List ℕ) (st : BlockState σ) : Prop

Ratpoints.Sieve.BlockPost with the callback not stopping the search: the invariant of the loops of the blocks after the denominators M.

• quit_eq_false : st.1.quit = false

  The callback has not stopped the search.

• post : BlockPost process P L κ Q M st0 st

  What the loop did to the state, after the denominators M.

theorem Ratpoints.Sieve.blockInv_nil {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 : BlockState σ} (hq : st0.1.quit = false) (hQ : Q st0.2.1) : BlockInv process P L κ Q st0 [] st0

theorem Ratpoints.Sieve.BlockInv.blockPost_append {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 st st' : BlockState σ} {M N : List ℕ} (h : BlockInv process P L κ Q st0 M st) (hs : BlockPost process P L κ Q N st st') : BlockPost process P L κ Q (M ++ N) st0 st'

The denominators N after the denominators M.

theorem Ratpoints.Sieve.BlockInv.blockPost_nil {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 st : BlockState σ} {M : List ℕ} (h : BlockInv process P L κ Q st0 M st) : BlockPost process P L κ Q [] st st

No denominator: the state is kept.

theorem Ratpoints.Sieve.BlockPost.blockInv {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 st : BlockState σ} {M : List ℕ} (h : BlockPost process P L κ Q M st0 st) (hq : ¬st.1.quit = true) : BlockInv process P L κ Q st0 M st

theorem Ratpoints.Sieve.BlockPost.of_prefix {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 st : BlockState σ} {M M' : List ℕ} (h : BlockPost process P L κ Q M st0 st) (hM : M <+: M') (hq : st.1.quit = true) : BlockPost process P L κ Q M' st0 st

At a stop, the delivery is that of the points of all the denominators of the block.

The loops over the steps of a block with a cursor

theorem Ratpoints.Sieve.blockInv_range'_init {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 : BlockState σ} {g : ℕ → List ℕ} {keep : ℕ → Bool} {a e : ℕ} (hae : a ≤ e) (hq : st0.1.quit = false) (hQ : Q st0.2.1) : a ≤ a ∧ a ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap g (List.range' a (a - a)))) st0

theorem Ratpoints.Sieve.BlockPost.of_eq_none_range' {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 s : BlockState σ} {g : ℕ → List ℕ} {keep : ℕ → Bool} {a e b : ℕ} {o : Option (BlockState σ)} (ho : o = none) (h : o = none ∧ a ≤ b ∧ b ≤ e ∧ b = e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap g (List.range' a (b - a + 1)))) s ∨ ∃ (r : BlockState σ), o = some r ∧ BlockPost process P L κ Q (List.filter keep (List.flatMap g (List.range' a (e + 1 - a)))) st0 r) : BlockPost process P L κ Q (List.filter keep (List.flatMap g (List.range' a (e + 1 - a)))) st0 s

At the exit of a loop of a block with a cursor, after its last step e.

theorem Ratpoints.Sieve.BlockInv.post_of_quit_range' {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 st st' : BlockState σ} {g : ℕ → List ℕ} {keep : ℕ → Bool} {a e b mb : ℕ} {o : Option (BlockState σ)} (h : e - b = mb ∧ o = none ∧ a ≤ b ∧ b ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap g (List.range' a (b - a)))) st) (hs : BlockPost process P L κ Q (List.filter keep (g b)) st st') (hq : st'.1.quit = true) : BlockPost process P L κ Q (List.filter keep (List.flatMap g (List.range' a (e + 1 - a)))) st0 st'

The step b of a loop of a block with a cursor after which the callback stops the search.

theorem Ratpoints.Sieve.BlockInv.append_range'_of_eq {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 st st' : BlockState σ} {g : ℕ → List ℕ} {keep : ℕ → Bool} {a e b mb : ℕ} {o : Option (BlockState σ)} (h : e - b = mb ∧ o = none ∧ a ≤ b ∧ b ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap g (List.range' a (b - a)))) st) (hs : BlockPost process P L κ Q (List.filter keep (g b)) st st') (hq : ¬st'.1.quit = true) (hbe : b = e) : a ≤ b ∧ b ≤ e ∧ b = e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap g (List.range' a (b - a + 1)))) st'

The step b = e of a loop of a block with a cursor, after which the loop ends.

theorem Ratpoints.Sieve.BlockInv.append_range'_of_ne {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 st st' : BlockState σ} {g : ℕ → List ℕ} {keep : ℕ → Bool} {a e b mb : ℕ} {o : Option (BlockState σ)} (h : e - b = mb ∧ o = none ∧ a ≤ b ∧ b ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap g (List.range' a (b - a)))) st) (hs : BlockPost process P L κ Q (List.filter keep (g b)) st st') (hq : ¬st'.1.quit = true) (hbe : ¬b = e) : e - (b + 1) < mb ∧ a ≤ b + 1 ∧ b + 1 ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap g (List.range' a (b + 1 - a)))) st'

A step b < e of a loop of a block with a cursor after which the callback has not stopped the search.

theorem Ratpoints.Sieve.BlockPost.filter_singleton {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st st' : BlockState σ} {keep : ℕ → Bool} {b : ℕ} (hk : keep b = true) (h : BlockPost process P L κ Q [b] st st') : BlockPost process P L κ Q (List.filter keep [b]) st st'

A step b with one denominator, sifted when it passes the test.

theorem Ratpoints.Sieve.BlockInv.append_range'_of_eq_of_not_keep {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 st : BlockState σ} {keep : ℕ → Bool} {a e b mb : ℕ} {o : Option (BlockState σ)} (h : e - b = mb ∧ o = none ∧ a ≤ b ∧ b ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap (fun (b : ℕ) => [b]) (List.range' a (b - a)))) st) (hk : ¬keep b = true) (hbe : b = e) : a ≤ b ∧ b ≤ e ∧ b = e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap (fun (b : ℕ) => [b]) (List.range' a (b - a + 1)))) st

The step b = e with one denominator that the test rejects.

theorem Ratpoints.Sieve.BlockInv.append_range'_of_ne_of_not_keep {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 st : BlockState σ} {keep : ℕ → Bool} {a e b mb : ℕ} {o : Option (BlockState σ)} (h : e - b = mb ∧ o = none ∧ a ≤ b ∧ b ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap (fun (b : ℕ) => [b]) (List.range' a (b - a)))) st) (hk : ¬keep b = true) (hbe : ¬b = e) : e - (b + 1) < mb ∧ a ≤ b + 1 ∧ b + 1 ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap (fun (b : ℕ) => [b]) (List.range' a (b + 1 - a)))) st

A step b < e with one denominator that the test rejects.

theorem Ratpoints.Sieve.BlockInv.pre_range' {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {D : ℕ → Prop} {st0 st : BlockState σ} {keep : ℕ → Bool} {a e b mb : ℕ} {o : Option (BlockState σ)} {N : List ℕ} (hD : ∀ b ∈ List.filter keep (List.range' a (e + 1 - a)), D b) (hk : keep b = true) (h : e - b = mb ∧ o = none ∧ a ≤ b ∧ b ≤ e ∧ BlockInv process P L κ Q st0 N st) : D b ∧ st.1.quit = false ∧ Q st.2.1

What the step at the denominator b of a loop with a cursor needs.

The loops over a range of steps

theorem Ratpoints.Sieve.BlockPost.of_eq_some {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 s : BlockState σ} {o : Option (BlockState σ)} {M : List ℕ} {R : Prop} (ho : o = some s) (h : o = none ∧ R ∨ ∃ (r : BlockState σ), o = some r ∧ BlockPost process P L κ Q M st0 r) : BlockPost process P L κ Q M st0 s

After the return of a loop of a block at a stop, the state returned.

theorem Ratpoints.Sieve.BlockPost.of_eq_none {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 s : BlockState σ} {f : ℕ → ℕ} {keep : ℕ → Bool} {a e : ℕ} {o : Option (BlockState σ)} {M : List ℕ} (ho : o = none) (h : o = none ∧ BlockInv process P L κ Q st0 (List.filter keep (List.map f (ForIn.toList [a:e + 1]))) s ∨ ∃ (r : BlockState σ), o = some r ∧ BlockPost process P L κ Q M st0 r) : BlockPost process P L κ Q (List.filter keep (List.map f (List.range' a (e + 1 - a)))) st0 s

At the end of a loop of a block over the steps a, …, e, the state after all of them.

theorem Ratpoints.Sieve.BlockInv.pre_map {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {D : ℕ → Prop} {st0 st : BlockState σ} {f : ℕ → ℕ} {keep : ℕ → Bool} {a e : ℕ} {pref suff : List ℕ} {cur : ℕ} {o : Option (BlockState σ)} {N : List ℕ} (hl : ForIn.toList [a:e + 1] = pref ++ cur :: suff) (hk : keep (f cur) = true) (hD : ∀ b ∈ List.filter keep (List.map f (List.range' a (e + 1 - a))), D b) (h : o = none ∧ BlockInv process P L κ Q st0 N st) : D (f cur) ∧ st.1.quit = false ∧ Q st.2.1

What the step at the step cur needs.

theorem Ratpoints.Sieve.BlockInv.post_of_quit_map {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 st st' : BlockState σ} {f : ℕ → ℕ} {keep : ℕ → Bool} {a e : ℕ} {pref suff : List ℕ} {cur : ℕ} {o : Option (BlockState σ)} (hl : ForIn.toList [a:e + 1] = pref ++ cur :: suff) (hk : keep (f cur) = true) (h : o = none ∧ BlockInv process P L κ Q st0 (List.filter keep (List.map f pref)) st) (hs : BlockPost process P L κ Q [f cur] st st') (hq : st'.1.quit = true) : BlockPost process P L κ Q (List.filter keep (List.map f (List.range' a (e + 1 - a)))) st0 st'

The step at the step cur at which the callback stops the search.

theorem Ratpoints.Sieve.BlockInv.append_map {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 st st' : BlockState σ} {f : ℕ → ℕ} {keep : ℕ → Bool} {pref : List ℕ} {cur : ℕ} {o : Option (BlockState σ)} (hk : keep (f cur) = true) (h : o = none ∧ BlockInv process P L κ Q st0 (List.filter keep (List.map f pref)) st) (hs : BlockPost process P L κ Q [f cur] st st') (hq : ¬st'.1.quit = true) : BlockInv process P L κ Q st0 (List.filter keep (List.map f (pref ++ [cur]))) st'

The step at the step cur after which the callback has not stopped the search.

theorem Ratpoints.Sieve.BlockInv.append_map_of_not_keep {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {st0 st : BlockState σ} {f : ℕ → ℕ} {keep : ℕ → Bool} {pref : List ℕ} {cur : ℕ} {o : Option (BlockState σ)} (hk : ¬keep (f cur) = true) (h : o = none ∧ BlockInv process P L κ Q st0 (List.filter keep (List.map f pref)) st) : BlockInv process P L κ Q st0 (List.filter keep (List.map f (pref ++ [cur]))) st

A step whose denominator the test rejects.

def Ratpoints.Sieve.MapBlockInvariant {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) {ι : Type} (P : ι → Prop) (L : ι → ℕ → List (ℤ × ℤ × ℤ)) (κ : ℕ → Counters) (Q : RowStore → Prop) (f : ℕ → ℕ) (keep : ℕ → Bool) (st0 : BlockState σ) (a e : ℕ) : Std.WP.Invariant ℕ (Option (BlockState σ) × BlockState σ) Prop

The invariant of the loops of Ratpoints.Sieve.squaresBlock and Ratpoints.Sieve.squares1Block over the steps a, …, e of a block, whose state is the value of a return and the state of the block, for the denominator f k of the step k and the test keep of the shape, from the state st0: before a return, Ratpoints.Sieve.BlockInv after the denominators of the steps done that pass the test; after the return at a stop, the state returned is that after all the denominators of the block that pass the test.

Equations

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

theorem Ratpoints.Sieve.squaresBlock_spec {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (step : ℕ → BlockState σ → Id (BlockState σ)) (D : ℕ → Prop) {ι : Type} (P : ι → Prop) (L : ι → ℕ → List (ℤ × ℤ × ℤ)) (κ : ℕ → Counters) (Q : RowStore → Prop) (hstep : ∀ (b : ℕ) (st : BlockState σ), ⦃ D b ∧ st.1.quit = false ∧ Q st.2.1 ⦄ step b st ⦃ fun (st' : BlockState σ) => BlockPost process P L κ Q [b] st st' ⦄) (cls : Vector NumClass 64) (a e : ℕ) (st : BlockState σ) : ⦃ st.1.quit = false ∧ Q st.2.1 ∧ ∀ b ∈ List.filter (fun (b : ℕ) => cls[b % 64]!.bits != 0) (List.map (fun (k : ℕ) => k * k) (List.range' a (e + 1 - a))), D b ⦄ squaresBlock step cls a e st ⦃ fun (st' : BlockState σ) => BlockPost process P L κ Q (List.filter (fun (b : ℕ) => cls[b % 64]!.bits != 0) (List.map (fun (k : ℕ) => k * k) (List.range' a (e + 1 - a)))) st st' ⦄

The loop of the square shape over the steps a, …, e of a block, for a step that delivers the lists of L, keeps Q and counts κ b for each denominator b with D b: the squares k ^ 2 of the steps whose class has a pattern, in order (Ratpoints.Sieve.BlockPost).

theorem Ratpoints.Sieve.squares1Block_spec {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (step : ℕ → BlockState σ → Id (BlockState σ)) (D : ℕ → Prop) {ι : Type} (P : ι → Prop) (L : ι → ℕ → List (ℤ × ℤ × ℤ)) (κ : ℕ → Counters) (Q : RowStore → Prop) (hstep : ∀ (b : ℕ) (st : BlockState σ), ⦃ D b ∧ st.1.quit = false ∧ Q st.2.1 ⦄ step b st ⦃ fun (st' : BlockState σ) => BlockPost process P L κ Q [b] st st' ⦄) (cls : Vector NumClass 64) (info : List Setup.DenInfo) (dv a e : ℕ) (st : BlockState σ) : ⦃ st.1.quit = false ∧ Q st.2.1 ∧ ∀ b ∈ List.filter (fun (b : ℕ) => cls[b % 64]!.bits != 0 && (denInfoTest info b).run) (List.map (fun (k : ℕ) => dv * k * k) (List.range' a (e + 1 - a))), D b ⦄ squares1Block step cls info dv a e st ⦃ fun (st' : BlockState σ) => BlockPost process P L κ Q (List.filter (fun (b : ℕ) => cls[b % 64]!.bits != 0 && (denInfoTest info b).run) (List.map (fun (k : ℕ) => dv * k * k) (List.range' a (e + 1 - a)))) st st' ⦄

The loop of a segment of the divisor shape, of the divisor dv, over the steps a, …, e of a block, for a step that delivers the lists of L, keeps Q and counts κ b for each denominator b with D b: the products dv k ^ 2 of the steps whose class has a pattern and that pass the valuation test (Ratpoints.Sieve.denInfoTest), in order.

def Ratpoints.Sieve.AllBlockInvariant {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) {ι : Type} (P : ι → Prop) (L : ι → ℕ → List (ℤ × ℤ × ℤ)) (κ : ℕ → Counters) (Q : RowStore → Prop) (keep : ℕ → Bool) (st0 : BlockState σ) (a e : ℕ) : Std.WP.WhileInvariant (Option (BlockState σ) × BlockState σ × ℕ) Prop

The invariant of the loop of Ratpoints.Sieve.allBlock over the denominators a, …, e of a block, whose state is the value of a return, the state of the block and the cursor b, for the test keep of the shape, from the state st0: before a return, a ≤ b ≤ e and Ratpoints.Sieve.BlockInv after the denominators before b, and after b too at the exit; after the return at a stop, the state returned is that after all the denominators of the block.

Equations

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

theorem Ratpoints.Sieve.allBlock_spec {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (step : ℕ → BlockState σ → Id (BlockState σ)) (D : ℕ → Prop) {ι : Type} (P : ι → Prop) (L : ι → ℕ → List (ℤ × ℤ × ℤ)) (κ : ℕ → Counters) (Q : RowStore → Prop) (hstep : ∀ (b : ℕ) (st : BlockState σ), ⦃ D b ∧ st.1.quit = false ∧ Q st.2.1 ⦄ step b st ⦃ fun (st' : BlockState σ) => BlockPost process P L κ Q [b] st st' ⦄) (cls : Vector NumClass 64) (a e : ℕ) (st : BlockState σ) : ⦃ st.1.quit = false ∧ Q st.2.1 ∧ a ≤ e ∧ ∀ b ∈ List.filter (fun (b : ℕ) => cls[b % 64]!.bits != 0) (List.range' a (e + 1 - a)), D b ⦄ allBlock step cls a e st ⦃ fun (st' : BlockState σ) => BlockPost process P L κ Q (List.filter (fun (b : ℕ) => cls[b % 64]!.bits != 0) (List.flatMap (fun (b : ℕ) => [b]) (List.range' a (e + 1 - a)))) st st' ⦄

The loop of the shape of every denominator over the steps a ≤ e of a block, for a step that delivers the lists of L, keeps Q and counts κ b for each denominator b with D b: the denominators a, …, e whose class has a pattern, in order; the loop ends, since the steps left decrease.

The walk through the set bits of a word of the word shape

def Ratpoints.Sieve.WalkDensWhileInvariant {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) {ι : Type} (P : ι → Prop) (L : ι → ℕ → List (ℤ × ℤ × ℤ)) (κ : ℕ → Counters) (Q : RowStore → Prop) (keep : ℕ → Bool) (x0 : UInt64) (base : ℕ) (st0 : BlockState σ) : Std.WP.WhileInvariant (Option (BlockState σ) × UInt64 × BlockState σ) Prop

The invariant of the loop of Ratpoints.Sieve.walkDens through the set bits of the word x0 of the denominators base + t, whose state is the value of a return, the word and the state of the block, for the test keep of the word shape, from the state st0: before a return, Ratpoints.Sieve.WalkWhileInvariant for Ratpoints.Sieve.BlockInv after the denominators of the set bits below k that pass the test; after the return at a stop, the state returned is that after all of them.

Equations

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

theorem Ratpoints.Sieve.ClearedBelow.filter_map_filter_range_succ_ctz {keep : ℕ → Bool} {x0 x : UInt64} {base k : ℕ} (hx : ClearedBelow x0 k x) (hx0 : x ≠ 0) : List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range (x.toBitVec.ctz.toNat + 1)))) = List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range k))) ++ List.filter keep [base + x.toBitVec.ctz.toNat]

The denominators base + t of the set bits t of x0 up to the lowest set bit of x, which has the bits of x0 below k cleared, that pass the test keep.

theorem Ratpoints.Sieve.walkDensInvariant_init {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {keep : ℕ → Bool} {x0 : UInt64} {base : ℕ} {st0 : BlockState σ} (hq : st0.1.quit = false) (hQ : Q st0.2.1) : WalkWhileInvariant x0 (fun (k : ℕ) (st : BlockState σ) => BlockInv process P L κ Q st0 (List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range k)))) st) false (st0, x0)

theorem Ratpoints.Sieve.BlockPost.of_eq_none_walk {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {keep : ℕ → Bool} {x0 x : UInt64} {base : ℕ} {st0 s : BlockState σ} {o : Option (BlockState σ)} (ho : o = none) (h : o = none ∧ WalkWhileInvariant x0 (fun (k : ℕ) (st : BlockState σ) => BlockInv process P L κ Q st0 (List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range k)))) st) true (s, x) ∨ ∃ (r : BlockState σ), o = some r ∧ BlockPost process P L κ Q (List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range 64)))) st0 r) : BlockPost process P L κ Q (List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range 64)))) st0 s

At the exit of the walk, after all the set bits of x0.

theorem Ratpoints.Sieve.walkDensInvariant_pre {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {D : ℕ → Prop} {keep : ℕ → Bool} {x0 x : UInt64} {base t mb : ℕ} {y : Bool} {st0 st : BlockState σ} {o : Option (BlockState σ)} (hD : ∀ b ∈ List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range 64))), D b) (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 (fun (k : ℕ) (st : BlockState σ) => BlockInv process P L κ Q st0 (List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range k)))) st) false (st, x)) (hx : (x != 0) = true) (ht : t = x.toBitVec.ctz.toNat) (hy : y = keep (base + t)) (hy' : y = true) : D (base + t) ∧ st.1.quit = false ∧ Q st.2.1

What the step at the lowest set bit of x needs: its denominator is one of the walk.

theorem Ratpoints.Sieve.walkDensInvariant_post_of_quit {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {keep : ℕ → Bool} {x0 x : UInt64} {base t mb : ℕ} {y : Bool} {st0 st st' : BlockState σ} {o : Option (BlockState σ)} (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 (fun (k : ℕ) (st : BlockState σ) => BlockInv process P L κ Q st0 (List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range k)))) st) false (st, x)) (hx : (x != 0) = true) (ht : t = x.toBitVec.ctz.toNat) (hy : y = keep (base + t)) (hy' : y = true) (hs : BlockPost process P L κ Q [base + t] st st') (hq : st'.1.quit = true) : BlockPost process P L κ Q (List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range 64)))) st0 st'

The step at the lowest set bit of x after which the callback stops the search.

theorem Ratpoints.Sieve.walkDensInvariant_and_sub_one {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {keep : ℕ → Bool} {x0 x : UInt64} {base t mb : ℕ} {st0 st st' : BlockState σ} {o : Option (BlockState σ)} (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 (fun (k : ℕ) (st : BlockState σ) => BlockInv process P L κ Q st0 (List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range k)))) st) false (st, x)) (hx : (x != 0) = true) (ht : t = x.toBitVec.ctz.toNat) (hs : BlockPost process P L κ Q (List.filter keep [base + t]) st st') (hq : ¬st'.1.quit = true) : (x &&& x - 1).toNat < mb ∧ WalkWhileInvariant x0 (fun (k : ℕ) (st : BlockState σ) => BlockInv process P L κ Q st0 (List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range k)))) st) false (st', x &&& x - 1)

A step of the walk at whose set bit the callback does not stop the search, or whose denominator the test rejects (st' = st).

theorem Ratpoints.Sieve.walkDensInvariant_and_sub_one_of_keep {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {keep : ℕ → Bool} {x0 x : UInt64} {base t mb : ℕ} {y : Bool} {st0 st st' : BlockState σ} {o : Option (BlockState σ)} (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 (fun (k : ℕ) (st : BlockState σ) => BlockInv process P L κ Q st0 (List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range k)))) st) false (st, x)) (hx : (x != 0) = true) (ht : t = x.toBitVec.ctz.toNat) (hy : y = keep (base + t)) (hy' : y = true) (hs : BlockPost process P L κ Q [base + t] st st') (hq : ¬st'.1.quit = true) : (x &&& x - 1).toNat < mb ∧ WalkWhileInvariant x0 (fun (k : ℕ) (st : BlockState σ) => BlockInv process P L κ Q st0 (List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range k)))) st) false (st', x &&& x - 1)

A step whose denominator the test passes.

theorem Ratpoints.Sieve.walkDensInvariant_and_sub_one_of_not_keep {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {keep : ℕ → Bool} {x0 x : UInt64} {base t mb : ℕ} {y : Bool} {st0 st : BlockState σ} {o : Option (BlockState σ)} (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 (fun (k : ℕ) (st : BlockState σ) => BlockInv process P L κ Q st0 (List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range k)))) st) false (st, x)) (hx : (x != 0) = true) (ht : t = x.toBitVec.ctz.toNat) (hy : y = keep (base + t)) (hy' : ¬y = true) : (x &&& x - 1).toNat < mb ∧ WalkWhileInvariant x0 (fun (k : ℕ) (st : BlockState σ) => BlockInv process P L κ Q st0 (List.filter keep (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x : ℕ) => x0.toBitVec.getLsbD x) (List.range k)))) st) false (st, x &&& x - 1)

A step whose denominator the test rejects.

theorem Ratpoints.Sieve.WalkWhileInvariant.exit_of_and {σ : Type} {x0 x : UInt64} {mb : ℕ} {st : BlockState σ} {o : Option (BlockState σ)} {W : ℕ → BlockState σ → Prop} (h : x.toNat = mb ∧ o = none ∧ WalkWhileInvariant x0 W false (st, x)) (hx : ¬(x != 0) = true) : WalkWhileInvariant x0 W true (st, x)

theorem Ratpoints.Sieve.walkDens_spec {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (step : ℕ → BlockState σ → Id (BlockState σ)) (D : ℕ → Prop) {ι : Type} (P : ι → Prop) (L : ι → ℕ → List (ℤ × ℤ × ℤ)) (κ : ℕ → Counters) (Q : RowStore → Prop) (hstep : ∀ (b : ℕ) (st : BlockState σ), ⦃ D b ∧ st.1.quit = false ∧ Q st.2.1 ⦄ step b st ⦃ fun (st' : BlockState σ) => BlockPost process P L κ Q [b] st st' ⦄) (test : ℕ → Id Bool) (x : UInt64) (base : ℕ) (st : BlockState σ) : ⦃ st.1.quit = false ∧ Q st.2.1 ∧ ∀ b ∈ List.filter (fun (b : ℕ) => (test b).run) (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x_1 : ℕ) => x.toBitVec.getLsbD x_1) (List.range 64))), D b ⦄ walkDens step test x base st ⦃ fun (st' : BlockState σ) => BlockPost process P L κ Q (List.filter (fun (b : ℕ) => (test b).run) (List.map (fun (x : ℕ) => base + x) (List.filter (fun (x_1 : ℕ) => x.toBitVec.getLsbD x_1) (List.range 64)))) st st' ⦄

The walk through the set bits t of the word x, lowest first, for a step that delivers the lists of L, keeps Q and counts κ b for each denominator b with D b: the denominators base + t that pass the test test, in order; the walk ends, since clearing the lowest set bit makes a word other than 0 smaller.

The words of the word shape

def Ratpoints.Sieve.ForbFits (forb : List ForbiddenEntry) : Prop

The forbidden divisors forb tested with words have positive primes p ≤ 2 ^ 32 with their reciprocals (Ratpoints.Sieve.magic), so that Ratpoints.Sieve.forbStarts finds the position of each at the first word of a block.

Equations

• Ratpoints.Sieve.ForbFits forb = ∀ f ∈ forb, 0 < f.p ∧ f.p ≤ 2 ^ 32 ∧ f.magic = Ratpoints.Sieve.magic f.p

def Ratpoints.Sieve.PosAt (forb : Array ForbiddenEntry) (cur : Array ℕ) (w : ℕ) : Prop

The positions cur of the forbidden divisors forb tested with words are those at the word w: one for each, w mod p for the prime p.

Equations

• Ratpoints.Sieve.PosAt forb cur w = (cur.size = forb.size ∧ ∀ n < forb.size, cur[n]! = w % forb[n]!.p)

theorem Ratpoints.Sieve.posAt_forbStarts {forb : Array ForbiddenEntry} (h : ForbFits forb.toList) (a : ℕ) : PosAt forb (forbStarts forb a) a

The positions of the forbidden divisors tested with words at the first word a of a block are those at a: a mod p, by the reciprocal of p when a ≤ Ratpoints.mulModLimit (Ratpoints.Sieve.mulMod_magic) and by Ratpoints.Sieve.modLong otherwise.

theorem Ratpoints.Sieve.wordBits_eq_foldl (db : UInt64) (forb : List ForbiddenEntry) (bLow bHigh w : ℕ) {x : UInt64} (hx : x = List.foldl (fun (x : UInt64) (e : ForbiddenEntry) => x &&& e.words[w % e.p]!) db forb) : wordBits db forb bLow bHigh w = if w = bHigh / 64 then (if w = bLow / 64 then x &&& ~~~0 <<< UInt64.ofNat (bLow % 64) else x) &&& ~~~0 >>> UInt64.ofNat (63 - bHigh % 64) else if w = bLow / 64 then x &&& ~~~0 <<< UInt64.ofNat (bLow % 64) else x

theorem Ratpoints.Sieve.denWord_spec (db : UInt64) (forb : Array ForbiddenEntry) (cur : Array ℕ) (lo0 hi0 bLow bHigh w : ℕ) : ⦃ (∀ f ∈ forb.toList, 0 < f.p) ∧ PosAt forb cur w ∧ lo0 = bLow / 64 ∧ hi0 = bHigh / 64 ⦄ denWord db forb cur lo0 hi0 bLow bHigh w ⦃ fun (r : UInt64 × Array ℕ) => r.1 = wordBits db forb.toList bLow bHigh w ∧ PosAt forb r.2 (w + 1) ⦄

The word of the denominators of the word w that the class test and the forbidden divisors forb tested with words leave, from their positions cur at w, with the masks of the first and the last word of the run: the word of Ratpoints.Sieve.wordBits; the positions are then those at w + 1.

def Ratpoints.Sieve.wordDens (db : UInt64) (forb : List ForbiddenEntry) (bLow bHigh w : ℕ) : List ℕ

The denominators 64 w + t of the word w of the word shape, of the set bits t of its word (Ratpoints.Sieve.wordBits), lowest first.

Equations

• Ratpoints.Sieve.wordDens db forb bLow bHigh w = List.map (fun (x : ℕ) => 64 * w + x) (List.filter (Ratpoints.Sieve.wordBits db forb bLow bHigh w).toBitVec.getLsbD (List.range 64))

def Ratpoints.Sieve.WordsBlockInvariant {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) {ι : Type} (P : ι → Prop) (L : ι → ℕ → List (ℤ × ℤ × ℤ)) (κ : ℕ → Counters) (Q : RowStore → Prop) (keep : ℕ → Bool) (db : UInt64) (forb : Array ForbiddenEntry) (bLow bHigh : ℕ) (st0 : BlockState σ) (a e : ℕ) : Std.WP.WhileInvariant (Option (BlockState σ) × Array ℕ × BlockState σ × ℕ) Prop

The invariant of the loop of Ratpoints.Sieve.wordsBlock over the words a, …, e of a block, whose state is the value of a return, the positions of the forbidden divisors forb tested with words, the state of the block and the word w, for the test keep of the word shape, from the state st0: before a return, a ≤ w ≤ e, Ratpoints.Sieve.BlockInv after the denominators of the words before w (Ratpoints.Sieve.wordDens), and of w too at the exit, and the positions those at w before it; after the return at a stop, the state returned is that after all the denominators of the block.

Equations

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

theorem Ratpoints.Sieve.wordsBlockInvariant_init {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {keep : ℕ → Bool} {db : UInt64} {forb : Array ForbiddenEntry} {bLow bHigh a e : ℕ} {st0 : BlockState σ} (hae : a ≤ e) (hq : st0.1.quit = false) (hQ : Q st0.2.1) (hforb : ForbFits forb.toList) : a ≤ a ∧ a ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (a - a)))) st0 ∧ PosAt forb (forbStarts forb a) a

theorem Ratpoints.Sieve.wordsBlockInvariant_pre_denWord {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {keep : ℕ → Bool} {db : UInt64} {forb : Array ForbiddenEntry} {bLow bHigh a e w mb : ℕ} {st0 st : BlockState σ} {o : Option (BlockState σ)} {cur : Array ℕ} (hforb : ForbFits forb.toList) (h : e - w = mb ∧ o = none ∧ a ≤ w ∧ w ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (w - a)))) st ∧ PosAt forb cur w) : (∀ f ∈ forb.toList, 0 < f.p) ∧ PosAt forb cur w ∧ bLow / 64 = bLow / 64 ∧ bHigh / 64 = bHigh / 64

What the word of the denominators of w needs.

theorem Ratpoints.Sieve.BlockPost.of_eq_none_words {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {keep : ℕ → Bool} {db : UInt64} {forb : Array ForbiddenEntry} {bLow bHigh a e w : ℕ} {st0 s : BlockState σ} {o : Option (BlockState σ)} (ho : o = none) (h : o = none ∧ a ≤ w ∧ w ≤ e ∧ w = e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (w - a + 1)))) s ∧ True ∨ ∃ (r : BlockState σ), o = some r ∧ BlockPost process P L κ Q (List.filter keep (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (e + 1 - a)))) st0 r) : BlockPost process P L κ Q (List.filter keep (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (e + 1 - a)))) st0 s

theorem Ratpoints.Sieve.BlockPost.wordDens_of_eq {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {keep : ℕ → Bool} {db x : UInt64} {forb : Array ForbiddenEntry} {bLow bHigh w : ℕ} {st st' : BlockState σ} {cur' : Array ℕ} (hx : x = wordBits db forb.toList bLow bHigh w ∧ PosAt forb cur' (w + 1)) (hs : BlockPost process P L κ Q (List.filter keep (List.map (HAdd.hAdd (64 * w)) (List.filter x.toBitVec.getLsbD (List.range 64)))) st st') : BlockPost process P L κ Q (List.filter keep (wordDens db forb.toList bLow bHigh w)) st st'

The walk through the word of w is through its denominators (Ratpoints.Sieve.wordDens).

theorem Ratpoints.Sieve.wordsBlockInvariant_pre_walk {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {D : ℕ → Prop} {keep : ℕ → Bool} {db x : UInt64} {forb : Array ForbiddenEntry} {bLow bHigh a e w mb : ℕ} {st0 st : BlockState σ} {o : Option (BlockState σ)} {cur cur' : Array ℕ} (hD : ∀ b ∈ List.filter keep (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (e + 1 - a))), D b) (hx : x = wordBits db forb.toList bLow bHigh w ∧ PosAt forb cur' (w + 1)) (h : e - w = mb ∧ o = none ∧ a ≤ w ∧ w ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (w - a)))) st ∧ PosAt forb cur w) : st.1.quit = false ∧ Q st.2.1 ∧ ∀ b ∈ List.filter keep (List.map (HAdd.hAdd (64 * w)) (List.filter x.toBitVec.getLsbD (List.range 64))), D b

What the walk through the word of w needs: its denominators are those of the block.

theorem Ratpoints.Sieve.wordsBlockInvariant_post_of_quit {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {keep : ℕ → Bool} {db x : UInt64} {forb : Array ForbiddenEntry} {bLow bHigh a e w mb : ℕ} {st0 st st' : BlockState σ} {o : Option (BlockState σ)} {cur cur' : Array ℕ} (hx : x = wordBits db forb.toList bLow bHigh w ∧ PosAt forb cur' (w + 1)) (hs : BlockPost process P L κ Q (List.filter keep (List.map (HAdd.hAdd (64 * w)) (List.filter x.toBitVec.getLsbD (List.range 64)))) st st') (hq : st'.1.quit = true) (h : e - w = mb ∧ o = none ∧ a ≤ w ∧ w ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (w - a)))) st ∧ PosAt forb cur w) : BlockPost process P L κ Q (List.filter keep (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (e + 1 - a)))) st0 st'

theorem Ratpoints.Sieve.wordsBlockInvariant_append_of_eq {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {keep : ℕ → Bool} {db x : UInt64} {forb : Array ForbiddenEntry} {bLow bHigh a e w mb : ℕ} {st0 st st' : BlockState σ} {o : Option (BlockState σ)} {cur cur' : Array ℕ} (hx : x = wordBits db forb.toList bLow bHigh w ∧ PosAt forb cur' (w + 1)) (hs : BlockPost process P L κ Q (List.filter keep (List.map (HAdd.hAdd (64 * w)) (List.filter x.toBitVec.getLsbD (List.range 64)))) st st') (hq : ¬st'.1.quit = true) (hwe : w = e) (h : e - w = mb ∧ o = none ∧ a ≤ w ∧ w ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (w - a)))) st ∧ PosAt forb cur w) : a ≤ w ∧ w ≤ e ∧ w = e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (w - a + 1)))) st' ∧ True

theorem Ratpoints.Sieve.wordsBlockInvariant_append_of_ne {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {ι : Type} {P : ι → Prop} {L : ι → ℕ → List (ℤ × ℤ × ℤ)} {κ : ℕ → Counters} {Q : RowStore → Prop} {keep : ℕ → Bool} {db x : UInt64} {forb : Array ForbiddenEntry} {bLow bHigh a e w mb : ℕ} {st0 st st' : BlockState σ} {o : Option (BlockState σ)} {cur cur' : Array ℕ} (hx : x = wordBits db forb.toList bLow bHigh w ∧ PosAt forb cur' (w + 1)) (hs : BlockPost process P L κ Q (List.filter keep (List.map (HAdd.hAdd (64 * w)) (List.filter x.toBitVec.getLsbD (List.range 64)))) st st') (hq : ¬st'.1.quit = true) (hwe : ¬w = e) (h : e - w = mb ∧ o = none ∧ a ≤ w ∧ w ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (w - a)))) st ∧ PosAt forb cur w) : e - (w + 1) < mb ∧ a ≤ w + 1 ∧ w + 1 ≤ e ∧ BlockInv process P L κ Q st0 (List.filter keep (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (w + 1 - a)))) st' ∧ PosAt forb cur' (w + 1)

theorem Ratpoints.Sieve.wordsBlock_spec {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (step : ℕ → BlockState σ → Id (BlockState σ)) (D : ℕ → Prop) {ι : Type} (P : ι → Prop) (L : ι → ℕ → List (ℤ × ℤ × ℤ)) (κ : ℕ → Counters) (Q : RowStore → Prop) (hstep : ∀ (b : ℕ) (st : BlockState σ), ⦃ D b ∧ st.1.quit = false ∧ Q st.2.1 ⦄ step b st ⦃ fun (st' : BlockState σ) => BlockPost process P L κ Q [b] st st' ⦄) (forb : Array ForbiddenEntry) (test : ℕ → Id Bool) (db : UInt64) (lo0 hi0 bLow bHigh a e : ℕ) (st : BlockState σ) : ⦃ st.1.quit = false ∧ Q st.2.1 ∧ a ≤ e ∧ lo0 = bLow / 64 ∧ hi0 = bHigh / 64 ∧ ForbFits forb.toList ∧ ∀ b ∈ List.filter (fun (b : ℕ) => (test b).run) (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (e + 1 - a))), D b ⦄ wordsBlock step forb test db lo0 hi0 bLow bHigh a e st ⦃ fun (st' : BlockState σ) => BlockPost process P L κ Q (List.filter (fun (b : ℕ) => (test b).run) (List.flatMap (wordDens db forb.toList bLow bHigh) (List.range' a (e + 1 - a)))) st st' ⦄

The loop of the word shape over the words a ≤ e of a block, with the first and last words of the run bLow / 64 and bHigh / 64 and forbidden divisors that have what the loop needs (Ratpoints.Sieve.ForbFits), for a step that delivers the lists of L, keeps Q and counts κ b for each denominator b with D b: the denominators of the words (Ratpoints.Sieve.wordDens) that pass the tests test, in order; the positions of the divisors step on with the words (Ratpoints.Sieve.posAt_forbStarts, Ratpoints.Sieve.denWord_spec), and the loop ends, since the words left decrease.

The loop of a shape over a block

def Ratpoints.Sieve.Shape.stepDens (shape : Shape) (db : UInt64) (bLow bHigh seg k : ℕ) : List ℕ

The denominators of the step k of the segment seg of the shape shape for the denominators bLow, …, bHigh, before the tests of the shape on a single denominator: the square k ^ 2, the product s k ^ 2 with the divisor s of the segment, the denominators of the word k that the class test and the forbidden divisors tested with words leave (Ratpoints.Sieve.wordDens, with the word db of the classes that admit a numerator), and k itself.

Equations

• Ratpoints.Sieve.Shape.squares.stepDens db bLow bHigh seg k = [k * k]
• (Ratpoints.Sieve.Shape.squares1 info divisors).stepDens db bLow bHigh seg k = [divisors[seg]! * k * k]
• (Ratpoints.Sieve.Shape.words forb forbVal useJacobi fast lcf).stepDens db bLow bHigh seg k = Ratpoints.Sieve.wordDens db forb bLow bHigh k
• Ratpoints.Sieve.Shape.all.stepDens db bLow bHigh seg k = [k]

def Ratpoints.Sieve.Shape.ForbFits : Shape → Prop

The forbidden divisors tested with words of the word shape have what the loop of a block over the words needs (Ratpoints.Sieve.ForbFits); the other shapes have none.

Equations

• (Ratpoints.Sieve.Shape.words forb forbVal useJacobi fast lcf).ForbFits = Ratpoints.Sieve.ForbFits forb
• x✝.ForbFits = True

def Ratpoints.Sieve.Shape.LoopFits (plan : BlockPlan) (bLow bHigh : ℕ) : Shape → Prop

What the loop of the shape over a block of the blocks plan for the denominators bLow, …, bHigh needs: for the word shape, forbidden divisors that have what the loop needs (Ratpoints.Sieve.ForbFits) and the first segment of the blocks from the word of bLow to that of bHigh, the first and last words of the run, which the masks compare with; nothing for the other shapes.

Equations

• Ratpoints.Sieve.Shape.LoopFits plan bLow bHigh (Ratpoints.Sieve.Shape.words forb forbVal useJacobi fast lcf) = (Ratpoints.Sieve.ForbFits forb ∧ plan.segs[0]! = (bLow / 64, bHigh / 64))
• Ratpoints.Sieve.Shape.LoopFits plan bLow bHigh x✝ = True

theorem Ratpoints.Sieve.run_keep_squares1 (info : List Setup.DenInfo) (divisors : List ℕ) (cls : Vector NumClass 64) (b : ℕ) : ((Shape.squares1 info divisors).keep cls b).run = (cls[b % 64]!.bits != 0 && (denInfoTest info b).run)

theorem Ratpoints.Sieve.filter_flatMap_stepDens_squares (db : UInt64) (cls : Vector NumClass 64) (bLow bHigh seg : ℕ) (l : List ℕ) : List.filter (fun (b : ℕ) => (Shape.squares.keep cls b).run) (List.flatMap (Shape.squares.stepDens db bLow bHigh seg) l) = List.filter (fun (b : ℕ) => cls[b % 64]!.bits != 0) (List.map (fun (k : ℕ) => k * k) l)

theorem Ratpoints.Sieve.filter_flatMap_stepDens_squares1 (info : List Setup.DenInfo) (divisors : List ℕ) (db : UInt64) (cls : Vector NumClass 64) (bLow bHigh seg : ℕ) (l : List ℕ) : List.filter (fun (b : ℕ) => ((Shape.squares1 info divisors).keep cls b).run) (List.flatMap ((Shape.squares1 info divisors).stepDens db bLow bHigh seg) l) = List.filter (fun (b : ℕ) => cls[b % 64]!.bits != 0 && (denInfoTest info b).run) (List.map (fun (k : ℕ) => divisors[seg]! * k * k) l)

theorem Ratpoints.Sieve.Shape.blockLoop_spec {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (shape : Shape) (step : ℕ → BlockState σ → Id (BlockState σ)) (D : ℕ → Prop) {ι : Type} (P : ι → Prop) (L : ι → ℕ → List (ℤ × ℤ × ℤ)) (κ : ℕ → Counters) (Q : RowStore → Prop) (hstep : ∀ (b : ℕ) (st : BlockState σ), ⦃ D b ∧ st.1.quit = false ∧ Q st.2.1 ⦄ step b st ⦃ fun (st' : BlockState σ) => BlockPost process P L κ Q [b] st st' ⦄) (cls : Vector NumClass 64) (db : UInt64) (plan : BlockPlan) (seg a e bLow bHigh : ℕ) (st : BlockState σ) : ⦃ st.1.quit = false ∧ Q st.2.1 ∧ a ≤ e ∧ LoopFits plan bLow bHigh shape ∧ ∀ b ∈ List.filter (fun (b : ℕ) => (shape.keep cls b).run) (List.flatMap (shape.stepDens db bLow bHigh seg) (List.range' a (e + 1 - a))), D b ⦄ shape.blockLoop step cls db plan seg a e bLow bHigh st ⦃ fun (st' : BlockState σ) => BlockPost process P L κ Q (List.filter (fun (b : ℕ) => (shape.keep cls b).run) (List.flatMap (shape.stepDens db bLow bHigh seg) (List.range' a (e + 1 - a)))) st st' ⦄

The loop of the shape over the steps a ≤ e of a block of the segment seg, each denominator that passes the tests of the shape handed to a step that delivers L b, keeps Q and counts κ b, for the denominators of the steps (Ratpoints.Sieve.Shape.stepDens) that pass the tests of the shape (Ratpoints.Sieve.Shape.keep), in order; for the word shape, with the first and last words of the run as the first segment of the blocks and forbidden divisors that have what the loop needs.

The decision in force for a block

def Ratpoints.Sieve.Decision.InForce (decs : Array Decision) (i dd : ℕ) : Prop

Decision dd of decs is the one in force for block i: it exists, its first block is at most i, and every later decision is for a block after i.

Equations

• Ratpoints.Sieve.Decision.InForce decs i dd = (dd < decs.size ∧ decs[dd]!.block ≤ i ∧ ∀ (j : ℕ), dd < j → j < decs.size → i < decs[j]!.block)

def Ratpoints.Sieve.DecisionSearchInvariant (decs : Array Decision) (i : ℕ) : Std.WP.WhileInvariant ℕ Prop

The invariant of the search of Ratpoints.Sieve.findDecision for the decision in force for block i, whose state is the index dd of a decision: while the search goes on, every later decision is for a block after i, and at the exit the decision dd is the one in force for block i (Ratpoints.Sieve.Decision.InForce).

Equations

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

theorem Ratpoints.Sieve.findDecision_spec (decs : Array Decision) (i : ℕ) : ⦃ 0 < decs.size ∧ decs[0]!.block = 0 ⦄ findDecision decs i ⦃ fun (dd : ℕ) => Decision.InForce decs i dd ⦄

For decisions of which the first is for block 0, the decision in force for block i is the last whose first block is at most i: the search from the last decision back ends there, at the first decision at the latest.