The contracts of the packing

The packing of the numerators of each class of the denominators modulo 64 into one class modulo a power of 2 (Ratpoints.Model.Packing), as @[spec] theorems proved with vcgen, the program logic of Lean core, with loop invariants that are named definitions. The class of the word w of the admissible numerators modulo 64 of a class of denominators packs it (Ratpoints.Sieve.NumClass.Packs): its stride 2 ^ k is that of a packing, k ≤ 6 and k < Ratpoints.numStrides, every set bit of w lies in the class a₀ mod 2 ^ k, and its pattern has the bit of the numerator a₀ + 2 ^ k t at t, so that the class word lets the numerator of a bit through exactly when the pattern has the bit, and lets nothing off the class through. The loop over the 64 classes makes such classes, with no row offsets yet, and the word den_bits of the classes whose word is not 0. The number of the packings counts the first class of each key 2 ^ k + a₀ among the classes with a pattern (Ratpoints.Sieve.firstKeys). The row offsets of the packings read, of each sieve entry, an odd modulus 1 < p ≤ Ratpoints.maxPrimeEven with its reciprocal, the inverse of Ratpoints.rbaLength modulo p and the bias, the least multiple of p from Ratpoints.rowBias on, as examine_prime, make_power and make_modulus set them (Ratpoints.Sieve.SieveEntry.Packable), which the sieve entry of a modulus has (Ratpoints.IsModulusEntry); they give each class with a pattern a row of the array of the offsets, with the offset of its packing for each sieve entry (Ratpoints.Sieve.SieveEntry.PackedFor): between Ratpoints.rowBias and Ratpoints.rowBias + 2 p, a₀ (2 ^ k Ratpoints.rbaLength)⁻¹ modulo p, with the inverse of the stride modulo p in the entry. fill_bp_list divides the denominator by the stride modulo each modulus, exactly in each of its branches, since its products stay below 2 ^ 64 / p.

Main definitions

• Ratpoints.Sieve.NumClass.numerator: the numerator a₀ + 2 ^ k j of bit j of a class.
• Ratpoints.Sieve.NumClass.WF, Ratpoints.Sieve.NumClass.Packs: the stride and the residue of a packing, and a class that packs a word of numerators modulo 64.
• Ratpoints.Sieve.NumClass.key, Ratpoints.Sieve.IsFirstKey, Ratpoints.Sieve.firstKeys: the key 2 ^ k + a₀ of a packing, and the number of the distinct packings of the classes below n.
• Ratpoints.Sieve.halveIter, Ratpoints.Sieve.halveChain: the halvings modulo an odd modulus.
• Ratpoints.Sieve.classOffset: the offset of the row of a class for a sieve entry.
• Ratpoints.Sieve.SieveEntry.Packable, Ratpoints.Sieve.SieveEntry.PackedFor, Ratpoints.Sieve.OffsetsFor: the fields of a sieve entry that the row offsets of the packing read, the offset of the packing of a class for an entry, and the rows of offsets of all the classes with a pattern.

Main statements

• Ratpoints.Sieve.NumClass.Packs.classBit_bits, Ratpoints.Sieve.NumClass.Packs.emod_eq_of_classBit, Ratpoints.Sieve.NumClass.Packs.bits_eq_zero_iff: the pattern lets bit j through exactly when the word lets the numerator of j through, the word lets nothing off the class through, and the pattern is 0 exactly when the word is; Ratpoints.Sieve.NumClass.Packs.filter_filter_emod: so the numerators that the word lets through are among those of the class; Ratpoints.Sieve.NumClass.Packs.bits_bne_zero: the test of the pattern is the test of the word.
• Ratpoints.Sieve.getLsbD_classMasks: the masks of the strides, 0 beyond the seven of k ≤ 6.
• Ratpoints.Sieve.packPattern_spec, Ratpoints.Sieve.numClasses_spec: the packed pattern, and the classes of the 64 words with den_bits.
• Ratpoints.Sieve.numPackings_spec: the number of the packings is that of the distinct keys, at least 1.
• Ratpoints.Sieve.classRows_spec, Ratpoints.Sieve.classOffsets_spec: the rows of offsets of the classes and the inverses of the strides in the entries.
• Ratpoints.Sieve.SieveEntry.PackedFor.fits: the sieve spec of an entry with the offset of the packing of a class and the closed form of a row fits the reductions of the row indices of the first two stages and the chunked first stage.
• Ratpoints.Sieve.fillBpList_eq_map: the residues of the denominator divided by the stride.

Implementation notes

The file uses Lean core and Std only, so that the contracts of the sieve, in files without Mathlib, can use it. The proofs use only the facts on the constants that decide checks next to them, never their values: here that Ratpoints.numStrides ≥ 1, that Ratpoints.maxBitsInPrime ≤ 10 (Ratpoints.maxPrimeEven_le_two_pow_10) and that Ratpoints.mulModLimit < 2 ^ 32; that the masks of the strides beyond k = 6 are 0 is read with the default of the array. The facts on words that are not about the model are in Ratpoints.Proof.Bits, those on natural numbers and integers in Ratpoints.Proof.Containers. The bounds of the products of fill_bp_list and of class_offsets are in Ratpoints.Proof.Reductions, the bits of an interval of numerators and the other range lemmas of the longs of the packing in Ratpoints.Proof.BitRange.

Residues modulo 64 and the strides of the packing

The classes

def Ratpoints.Sieve.NumClass.numerator (cl : NumClass) (j : Int) : Int

The numerator of bit j in the packing of the class cl: a₀ + 2 ^ k j.

Equations

• cl.numerator j = ↑cl.a0 + 2 ^ cl.k * j

structure Ratpoints.Sieve.NumClass.WF (cl : NumClass) : Prop

The stride and the residue of a class are those of a packing: the stride exponent below Ratpoints.numStrides and at most 6, the residue below the stride. The keys 2 ^ k + a₀ of such packings are below 2 ^ Ratpoints.numStrides and 128.

• k_lt : cl.k < numStrides

  The stride exponent is below Ratpoints.numStrides.

• k_le : cl.k ≤ 6

  The stride is at most 2 ^ 6, the modulus 64 of the 2-adic information.

• a0_lt : cl.a0 < 2 ^ cl.k

  The residue is below the stride.

structure Ratpoints.Sieve.NumClass.Packs (cl : NumClass) (w : UInt64) extends cl.WF : Prop

The class cl packs the word w of the numerators modulo 64 of a class of denominators: its stride and residue are those of a packing (Ratpoints.Sieve.NumClass.WF), every set bit a < 64 of w is a₀ modulo 2 ^ k, and bit t of the pattern is bit (a₀ + 2 ^ k t) mod 64 of w.

• k_lt : cl.k < numStrides
• k_le : cl.k ≤ 6
• a0_lt : cl.a0 < 2 ^ cl.k
• mod_eq (a : Nat) : a < 64 → w.toBitVec.getLsbD a = true → a % 2 ^ cl.k = cl.a0

  Every set bit of the word lies in the class a₀ mod 2 ^ k.

• getLsbD_bits (t : Nat) : t < 64 → cl.bits.toBitVec.getLsbD t = w.toBitVec.getLsbD ((cl.a0 + 2 ^ cl.k * t) % 64)

  Bit t of the pattern is the bit of the numerator of bit t.

theorem Ratpoints.Sieve.NumClass.Packs.classBit_bits {cl : NumClass} {w : UInt64} (h : cl.Packs w) (j : Int) : classBit cl.bits j = classBit w (cl.numerator j)

The class word lets the numerator of bit j of the pattern through exactly when the pattern has bit j.

theorem Ratpoints.Sieve.NumClass.Packs.emod_eq_of_classBit {cl : NumClass} {w : UInt64} (h : cl.Packs w) {a : Int} (ha : classBit w a = true) : a % 2 ^ cl.k = ↑cl.a0

A numerator that the class word lets through lies in the class a₀ mod 2 ^ k.

theorem Ratpoints.Sieve.NumClass.Packs.bits_eq_zero_iff {cl : NumClass} {w : UInt64} (h : cl.Packs w) : cl.bits = 0 ↔ w = 0

theorem Ratpoints.Sieve.NumClass.Packs.filter_filter_emod {cl : NumClass} {w : UInt64} (h : cl.Packs w) (l : List Int) (p : Int → Bool) : List.filter (fun (a : Int) => classBit w a && p a) (List.filter (fun (a : Int) => a % 2 ^ cl.k == ↑cl.a0) l) = List.filter (fun (a : Int) => classBit w a && p a) l

The numerators in the class a₀ mod 2 ^ k of a list that the class word w and a test p let through are those of the list that they let through, since the class word lets nothing off the class through.

theorem Ratpoints.Sieve.NumClass.Packs.bits_bne_zero {cl : NumClass} {w : UInt64} (h : cl.Packs w) : (cl.bits != 0) = (w != 0)

The test EXT0(cl->bits) of the C code on a class that packs the word w is the test w ≠ 0: the classes with a pattern are those whose word admits a numerator, the classes of den_bits.

theorem Ratpoints.Sieve.NumClass.Packs.withOffset {cl : NumClass} {w : UInt64} (h : cl.Packs w) (o : Option Nat) : { bits := cl.bits, k := cl.k, a0 := cl.a0, offset := o }.Packs w

Ratpoints.Sieve.NumClass.Packs reads only the pattern, the stride and the residue of the class, not its row offsets.

def Ratpoints.Sieve.NumClass.key (cl : NumClass) : Nat

The key 2 ^ k + a₀ of the packing of a class, by which num_packings and class_offsets tell the packings apart.

Equations

• cl.key = 2 ^ cl.k + cl.a0

theorem Ratpoints.Sieve.NumClass.WF.key_lt {cl : NumClass} (h : cl.WF) : cl.key < 2 ^ (cl.k + 1)

theorem Ratpoints.Sieve.NumClass.WF.key_lt_128 {cl : NumClass} (h : cl.WF) : cl.key < 128

theorem Ratpoints.Sieve.NumClass.WF.a0_lt_sixty_four {cl : NumClass} (h : cl.WF) : cl.a0 < 64

theorem Ratpoints.Sieve.NumClass.WF.key_lt_two_pow_numStrides {cl : NumClass} (h : cl.WF) : cl.key < 2 ^ numStrides

theorem Ratpoints.Sieve.NumClass.WF.key_lt_key {cl cl' : NumClass} (h : cl.WF) (hk : cl.k < cl'.k) : cl.key < cl'.key

theorem Ratpoints.Sieve.NumClass.WF.k_eq_and_a0_eq_of_key_eq {cl cl' : NumClass} (h : cl.WF) (h' : cl'.WF) (hk : cl.key = cl'.key) : cl.k = cl'.k ∧ cl.a0 = cl'.a0

The masks of the strides

theorem Ratpoints.Sieve.getElem!_classMasks_of_lt {k : Nat} (hk : 6 < k) : classMasks[k]! = 0

A mask beyond the seven of the strides k ≤ 6 is read as 0.

theorem Ratpoints.Sieve.getLsbD_classMasks (k : Nat) {a : Nat} (ha : a < 64) : classMasks[k]!.toBitVec.getLsbD a = (decide (k ≤ 6) && a % 2 ^ k == 0)

Bit a < 64 of mask k is set exactly when 2 ^ k ∣ a for the seven strides k ≤ 6; the masks beyond them are read as 0.

theorem Ratpoints.Sieve.getLsbD_classMasks_shiftLeft {k s : Nat} (hk : k ≤ 6) (hs : s < 2 ^ k) (a : Nat) : (classMasks[k]! <<< s.toUInt64).toBitVec.getLsbD a = (decide (a < 64) && a % 2 ^ k == s)

def Ratpoints.Sieve.ClassOf (w : UInt64) (c k : Nat) : Prop

Every set bit a < 64 of w is ≡ c (mod 2 ^ k).

Equations

• Ratpoints.Sieve.ClassOf w c k = ∀ (a : Nat), a < 64 → w.toBitVec.getLsbD a = true → a % 2 ^ k = c % 2 ^ k

theorem Ratpoints.Sieve.classOf_zero (w : UInt64) (c : Nat) : ClassOf w c 0

theorem Ratpoints.Sieve.le_six_and_classOf_of_and_not {w : UInt64} {c k : Nat} (hw : w ≠ 0) (h : ¬(w &&& ~~~(classMasks[k]! <<< (c % 2 ^ k).toUInt64) != 0) = true) : k ≤ 6 ∧ ClassOf w c k

The test of the loop over the strides of Ratpoints.Sieve.numClasses at k lets the loop go on only for k ≤ 6, where the masks are not 0, and when every set bit of w ≠ 0 is ≡ c (mod 2 ^ k).

The pattern of a class

def Ratpoints.Sieve.PackInvariant (w : UInt64) (k a0 n : Nat) (packed : UInt64) : Prop

The invariant of the loop of Ratpoints.Sieve.packPattern over the set bits of w: the packed word after the set bits below n, bit t set exactly when some set bit j < n has the place t.

Equations

• Ratpoints.Sieve.PackInvariant w k a0 n packed = ∀ (t : Nat), packed.toBitVec.getLsbD t = decide (∃ (j : Nat), j < n ∧ w.toBitVec.getLsbD j = true ∧ (j - a0) % 64 / 2 ^ k = t)

def Ratpoints.Sieve.DoubleInvariant (k : Nat) (p0 : UInt64) : Std.WP.WhileInvariant (UInt64 × Nat) Prop

The invariant of the doubling loop of Ratpoints.Sieve.packPattern, from the packed word p0 of period 64 / 2 ^ k: the shift s = 2 ^ j, from 64 / 2 ^ k up to 64, and bit t of the word the bit t mod (64 / 2 ^ k) of p0 below s.

Equations

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

theorem Ratpoints.Sieve.packInvariant_zero (w : UInt64) (k a0 : Nat) : PackInvariant w k a0 0 0

theorem Ratpoints.Sieve.PackInvariant.or_shiftLeft {w x packed : UInt64} {k a0 n : Nat} (h : PackInvariant w k a0 n packed) (hcl : ClearedBelow w n x) (hx : x ≠ 0) : PackInvariant w k a0 (x.toBitVec.ctz.toNat + 1) (packed ||| 1 <<< ((x.toBitVec.ctz.toNat - a0) % 64 / 2 ^ k).toUInt64)

theorem Ratpoints.Sieve.WalkWhileInvariant.doubleInvariant {w p0 x : UInt64} {k a0 : Nat} (hk : k ≤ 6) (h : WalkWhileInvariant w (PackInvariant w k a0) true (p0, x)) : DoubleInvariant k p0 false (p0, 64 / 2 ^ k)

At the exit of the packing loop the packed word has its bits below 64 / 2 ^ k.

theorem Ratpoints.Sieve.DoubleInvariant.or_shiftLeft {k s mb : Nat} {p0 packed : UInt64} (hk : k ≤ 6) (h : 64 - s = mb ∧ DoubleInvariant k p0 false (packed, s)) (hs : s < 64) : 64 - 2 * s < mb ∧ DoubleInvariant k p0 false (packed ||| packed <<< UInt64.ofNat s, 2 * s)

theorem Ratpoints.Sieve.DoubleInvariant.exit {k s mb : Nat} {p0 packed : UInt64} (hs : ¬s < 64) (h : 64 - s = mb ∧ DoubleInvariant k p0 false (packed, s)) : DoubleInvariant k p0 true (packed, s)

theorem Ratpoints.Sieve.exists_getLsbD_sub_mod_div_iff {w : UInt64} {c k t : Nat} (hk : k ≤ 6) (hcl : ClassOf w c k) : (∃ (j : Nat), j < 64 ∧ w.toBitVec.getLsbD j = true ∧ (j - c % 2 ^ k) % 64 / 2 ^ k = t % (64 / 2 ^ k)) ↔ w.toBitVec.getLsbD ((c % 2 ^ k + 2 ^ k * t) % 64) = true

The bit of the packed pattern at t, read off the set bits of w: some set bit j has its place t mod (64 / 2 ^ k) exactly when bit (a0 + 2 ^ k t) mod 64 of w is set.

theorem Ratpoints.Sieve.getLsbD_of_doubleInvariant {w p0 x packed : UInt64} {c k s : Nat} (hk : k ≤ 6) (hcl : ClassOf w c k) (hw : WalkWhileInvariant w (PackInvariant w k (c % 2 ^ k)) true (p0, x)) (h : DoubleInvariant k p0 true (packed, s)) (t : Nat) : t < 64 → packed.toBitVec.getLsbD t = w.toBitVec.getLsbD ((c % 2 ^ k + 2 ^ k * t) % 64)

The packed word at the exit of the loops of Ratpoints.Sieve.packPattern.

theorem Ratpoints.Sieve.packPattern_spec (w : UInt64) (k c : Nat) : ⦃ k ≤ 6 ∧ ClassOf w c k ⦄ packPattern w k (c % 2 ^ k) ⦃ fun (packed : UInt64) => ∀ (t : Nat), t < 64 → packed.toBitVec.getLsbD t = w.toBitVec.getLsbD ((c % 2 ^ k + 2 ^ k * t) % 64) ⦄

Bit t of the packed pattern of w for the stride 2 ^ k, k ≤ 6, and the residue a₀ = c mod 2 ^ k of all the set bits of w is bit (a₀ + 2 ^ k t) mod 64 of w.

The classes of the 64 words

theorem Ratpoints.Sieve.NumClass.packs_mk {w packed : UInt64} {c k : Nat} (hk : k < numStrides) (hk6 : k ≤ 6) (hcl : ClassOf w c k) (hp : ∀ (t : Nat), t < 64 → packed.toBitVec.getLsbD t = w.toBitVec.getLsbD ((c % 2 ^ k + 2 ^ k * t) % 64)) : { bits := packed, k := k, a0 := c % 2 ^ k, offset := none }.Packs w

A class of the stride 2 ^ k, k ≤ 6 and k < Ratpoints.numStrides, with the residue c mod 2 ^ k of all the set bits of w and the pattern of bit t the bit (a₀ + 2 ^ k t) mod 64 of w packs w.

theorem Ratpoints.Sieve.NumClass.packs_zero {w : UInt64} (hw : ¬(w != 0) = true) : { bits := 0, k := 0, a0 := 0, offset := none }.Packs w

The class of the word 0: the stride 1, the residue 0 and the pattern 0.

def Ratpoints.Sieve.StrideInvariant (w : UInt64) (c : Nat) : Std.WP.WhileInvariant Nat Prop

The invariant of the loop over the strides of Ratpoints.Sieve.numClasses for the word w with its lowest set bit c: the stride exponent k from 1 up to Ratpoints.numStrides and 7, and every set bit of w ≡ c (mod 2 ^ (k - 1)).

Equations

• Ratpoints.Sieve.StrideInvariant w c = Std.WP.WhileInvariant.mk fun (x : Bool) (k : Nat) => 1 ≤ k ∧ k ≤ Ratpoints.numStrides ∧ k ≤ 7 ∧ Ratpoints.Sieve.ClassOf w c (k - 1)

theorem Ratpoints.Sieve.strideInvariant_one (w : UInt64) (c : Nat) : StrideInvariant w c false 1

theorem Ratpoints.Sieve.strideInvariant_add_one {w : UInt64} {c k : Nat} (hw : (w != 0) = true) (hk : k < numStrides) (hb : ¬(w &&& ~~~(classMasks[k]! <<< UInt64.ofNat (c % 2 ^ k)) != 0) = true) : StrideInvariant w c false (k + 1)

The loop over the strides goes on at k: k ≤ 6 and every set bit ≡ c (mod 2 ^ k).

theorem Ratpoints.Sieve.StrideInvariant.le_six_and_classOf {w : UInt64} {c k : Nat} (h : StrideInvariant w c true k) : k - 1 ≤ 6 ∧ ClassOf w c (k - 1)

theorem Ratpoints.Sieve.StrideInvariant.packs {w packed : UInt64} {c k : Nat} (h : StrideInvariant w c true k) (hp : ∀ (t : Nat), t < 64 → packed.toBitVec.getLsbD t = w.toBitVec.getLsbD ((c % 2 ^ (k - 1) + 2 ^ (k - 1) * t) % 64)) : { bits := packed, k := k - 1, a0 := c % 2 ^ (k - 1), offset := none }.Packs w

The class after the loop over the strides packs the word, with the pattern w itself for k = 1 and with the packed pattern packed otherwise.

theorem Ratpoints.Sieve.StrideInvariant.packs_self {w : UInt64} {c k : Nat} (h : StrideInvariant w c true k) (hk : k - 1 = 0) : { bits := w, k := k - 1, a0 := c % 2 ^ (k - 1), offset := none }.Packs w

def Ratpoints.Sieve.NumClassesInvariant (nb : Vector UInt64 64) (n : Nat) (s : Vector NumClass 64 × UInt64) : Prop

The invariant of the loop over the classes of Ratpoints.Sieve.numClasses after the classes below n: each packs its word and has no row offsets yet, and the word den_bits has the bits of the classes below n whose word is not 0.

Equations

• Ratpoints.Sieve.NumClassesInvariant nb n s = ((∀ (b : Nat), b < n → s.fst[b]!.Packs nb[b]! ∧ s.fst[b]!.offset = none) ∧ ∀ (j : Nat), s.snd.toBitVec.getLsbD j = (decide (j < n) && nb[j]! != 0))

theorem Ratpoints.Sieve.numClassesInvariant_zero (nb : Vector UInt64 64) : NumClassesInvariant nb [].length (Vector.replicate 64 default, 0)

theorem Ratpoints.Sieve.NumClassesInvariant.set {nb : Vector UInt64 64} {pref suff : List Nat} {cur : Nat} (hl : ForIn.toList [:64] = pref ++ cur :: suff) {cls : Vector NumClass 64} {db db' : UInt64} (h : NumClassesInvariant nb pref.length (cls, db)) {cl : NumClass} (hc : cur < 64) (hcl : cl.Packs nb[cur]) (hoff : cl.offset = none) (hdb : ∀ (j : Nat), db'.toBitVec.getLsbD j = (db.toBitVec.getLsbD j || decide (j = cur) && nb[cur] != 0)) : NumClassesInvariant nb (pref ++ [cur]).length (cls.set cur cl hc, db')

The class cur set to cl, which packs its word, and its bit put into den_bits if its word is not 0.

theorem Ratpoints.Sieve.NumClassesInvariant.set_or {nb : Vector UInt64 64} {pref suff : List Nat} {cur : Nat} (hl : ForIn.toList [:64] = pref ++ cur :: suff) {cls : Vector NumClass 64} {db : UInt64} (h : NumClassesInvariant nb pref.length (cls, db)) {cl : NumClass} (hc : cur < 64) (hw : (nb[cur] != 0) = true) (hcl : cl.Packs nb[cur]) (hoff : cl.offset = none) : NumClassesInvariant nb (pref ++ [cur]).length (cls.set cur cl hc, db ||| 1 <<< UInt64.ofNat cur)

theorem Ratpoints.Sieve.NumClassesInvariant.set_zero {nb : Vector UInt64 64} {pref suff : List Nat} {cur : Nat} (hl : ForIn.toList [:64] = pref ++ cur :: suff) {cls : Vector NumClass 64} {db : UInt64} (h : NumClassesInvariant nb pref.length (cls, db)) (hc : cur < 64) (hw : ¬(nb[cur] != 0) = true) : NumClassesInvariant nb (pref ++ [cur]).length (cls.set cur { bits := 0, k := 0, a0 := 0, offset := none } hc, db)

theorem Ratpoints.Sieve.NumClassesInvariant.post {nb : Vector UInt64 64} {cls : Vector NumClass 64} {db : UInt64} (h : NumClassesInvariant nb (ForIn.toList [:64]).length (cls, db)) : (∀ (b : Nat), b < 64 → cls[b]!.Packs nb[b]! ∧ cls[b]!.offset = none) ∧ ∀ (j : Nat), db.toBitVec.getLsbD j = (decide (j < 64) && nb[j]! != 0)

theorem Ratpoints.Sieve.numClasses_spec (nb : Vector UInt64 64) : ⦃ True ⦄ numClasses nb ⦃ fun (r : Vector NumClass 64 × UInt64) => (∀ (b : Nat), b < 64 → r.fst[b]!.Packs nb[b]! ∧ r.fst[b]!.offset = none) ∧ ∀ (j : Nat), r.snd.toBitVec.getLsbD j = (decide (j < 64) && nb[j]! != 0) ⦄

Each class packs its word of the 2-adic information and has no row offsets yet, and the word den_bits has the bit of each class whose word is not 0, as Ratpoints.Sieve.denBits has.

theorem Ratpoints.Sieve.packs_getElem!_fst_run_numClasses (nb : Vector UInt64 64) {b : Nat} (hb : b < 64) : (numClasses nb).run.fst[b]!.Packs nb[b]!

Each class that Ratpoints.Sieve.numClasses makes packs its word of the 2-adic information (Ratpoints.Sieve.numClasses_spec).

The fields of the sieve entries

structure Ratpoints.Sieve.SieveEntry.Packable (e : SieveEntry) : Prop

The fields of a sieve entry that the row offsets of the packing read: an odd modulus 1 < p ≤ Ratpoints.maxPrimeEven with its reciprocal, the inverse rbainv < p of Ratpoints.rbaLength modulo p, and the bias, a multiple of p from Ratpoints.rowBias to below Ratpoints.rowBias + p, as examine_prime, make_power and make_modulus set them.

• one_lt : 1 < e.p

  The modulus is above 1.

• odd : e.p % 2 = 1

  The modulus is odd.

• le_maxPrimeEven : e.p ≤ maxPrimeEven

  The modulus is at most Ratpoints.maxPrimeEven.

• magic_eq : e.magic = Sieve.magic e.p

  The reciprocal is that of the modulus.

• rbainv_mul_mod : e.rbainv * rbaLength % e.p = 1

  rbainv is the inverse of Ratpoints.rbaLength modulo the modulus.

• rbainv_lt : e.rbainv < e.p

  rbainv is below the modulus.

• bias_mod : e.bias % e.p = 0

  The bias is a multiple of the modulus.

• rowBias_le_bias : rowBias ≤ e.bias

  The bias is at least Ratpoints.rowBias.

• bias_lt : e.bias < rowBias + e.p

  The bias is below Ratpoints.rowBias + p.

The number of the packings

def Ratpoints.Sieve.IsFirstKey (cls : Vector NumClass 64) (b : Nat) : Prop

Whether the class b of cls is the first with a pattern whose packing has its key.

Equations

• Ratpoints.Sieve.IsFirstKey cls b = (cls[b]!.bits ≠ 0 ∧ ∀ (b' : Nat), b' < b → cls[b']!.bits ≠ 0 → cls[b']!.key ≠ cls[b]!.key)

@[instance_reducible]

instance Ratpoints.Sieve.instDecidableIsFirstKey (cls : Vector NumClass 64) (b : Nat) : Decidable (IsFirstKey cls b)

Equations

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

def Ratpoints.Sieve.firstKeys (cls : Vector NumClass 64) (n : Nat) : Nat

The number of the distinct packings of the classes below n with a pattern, the classes that are the first with their key.

Equations

• Ratpoints.Sieve.firstKeys cls n = (List.filter (fun (b : Nat) => decide (Ratpoints.Sieve.IsFirstKey cls b)) (List.range n)).length

theorem Ratpoints.Sieve.firstKeys_succ (cls : Vector NumClass 64) (n : Nat) : firstKeys cls (n + 1) = firstKeys cls n + if IsFirstKey cls n then 1 else 0

theorem Ratpoints.Sieve.firstKeys_mono (cls : Vector NumClass 64) {m n : Nat} (h : m ≤ n) : firstKeys cls m ≤ firstKeys cls n

def Ratpoints.Sieve.NumPackingsInvariant (cls : Vector NumClass 64) (n : Nat) (s : Array UInt64 × Nat) : Prop

The invariant of the loop of Ratpoints.Sieve.numPackings after the classes below n: the two words seen mark the keys of the classes below n with a pattern, and the count is the number of their distinct packings.

Equations

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

theorem Ratpoints.Sieve.numPackingsInvariant_zero (cls : Vector NumClass 64) : NumPackingsInvariant cls [].length (#[0, 0], 0)

theorem Ratpoints.Sieve.NumPackingsInvariant.post {cls : Vector NumClass 64} {seen : Array UInt64} {n : Nat} (h : NumPackingsInvariant cls (ForIn.toList [:64]).length (seen, n)) : (if 0 < n then n else 1) = max 1 (firstKeys cls 64)

theorem Ratpoints.Sieve.NumPackingsInvariant.test_eq_decide {cls : Vector NumClass 64} {cur : Nat} (hwf : ∀ (b : Nat), b < 64 → cls[b]!.WF) {seen : Array UInt64} {n : Nat} (h : NumPackingsInvariant cls cur (seen, n)) (hc : cur < 64) : (cls[cur].bits != 0 && seen[(2 ^ cls[cur].k + cls[cur].a0) / 64]! >>> UInt64.ofNat ((2 ^ cls[cur].k + cls[cur].a0) % 64) &&& 1 == 0) = decide (IsFirstKey cls cur)

The test of num_packings at the class cur, that it has a pattern and that seen does not mark its key, is whether it is the first class with its key.

theorem Ratpoints.Sieve.NumPackingsInvariant.mark {cls : Vector NumClass 64} {cur : Nat} (hwf : ∀ (b : Nat), b < 64 → cls[b]!.WF) {seen : Array UInt64} {n : Nat} (h : NumPackingsInvariant cls cur (seen, n)) (hc : cur < 64) (hb : (cls[cur].bits != 0 && seen[(2 ^ cls[cur].k + cls[cur].a0) / 64]! >>> UInt64.ofNat ((2 ^ cls[cur].k + cls[cur].a0) % 64) &&& 1 == 0) = true) : NumPackingsInvariant cls (cur + 1) (seen.set! ((2 ^ cls[cur].k + cls[cur].a0) / 64) (seen[(2 ^ cls[cur].k + cls[cur].a0) / 64]! ||| 1 <<< UInt64.ofNat ((2 ^ cls[cur].k + cls[cur].a0) % 64)), n + 1)

A class that is the first with its key gets its key marked and is counted.

theorem Ratpoints.Sieve.NumPackingsInvariant.skip {cls : Vector NumClass 64} {cur : Nat} (hwf : ∀ (b : Nat), b < 64 → cls[b]!.WF) {seen : Array UInt64} {n : Nat} (h : NumPackingsInvariant cls cur (seen, n)) (hc : cur < 64) (hb : ¬(cls[cur].bits != 0 && seen[(2 ^ cls[cur].k + cls[cur].a0) / 64]! >>> UInt64.ofNat ((2 ^ cls[cur].k + cls[cur].a0) % 64) &&& 1 == 0) = true) : NumPackingsInvariant cls (cur + 1) (seen, n)

A class that is not the first with its key leaves the marks and the count as they are.

theorem Ratpoints.Sieve.numPackings_spec (cls : Vector NumClass 64) : ⦃ ∀ (b : Nat), b < 64 → cls[b]!.WF ⦄ numPackings cls ⦃ fun (n : Nat) => n = max 1 (firstKeys cls 64) ⦄

The number of the distinct packings of the classes with a pattern, at least 1.

The rows of the packings

def Ratpoints.Sieve.classOffset (es : Array SieveEntry) (rinv : Array (Array Nat)) (cl : NumClass) (n : Nat) : Nat

The offset of the row of the packing of the class cl for the n-th modulus p of the sieve entries es, from the inverse rinv[n][k] of 2 ^ k Ratpoints.rbaLength modulo p: the remainder of a₀ rinv[n][k] by a multiplication with the reciprocal of the entry, plus its bias, as class_offsets computes it.

Equations

• Ratpoints.Sieve.classOffset es rinv cl n = Ratpoints.Sieve.mulMod (cl.a0 * rinv[n]![cl.k]!) es[n]!.p es[n]!.magic + es[n]!.bias

structure Ratpoints.Sieve.ClassRowsInvariant (cls : Vector NumClass 64) (es : Array SieveEntry) (rinv : Array (Array Nat)) (np size m : Nat) (cls' : Vector NumClass 64) (o : Array Nat) (rowOf : Array (Option Nat)) (rows : Nat) : Prop

The invariant of the loop of Ratpoints.Sieve.classRows over the classes after those below m, for the classes cls it starts from and the sieve entries es with the inverses rinv, rows of np offsets: the state is the classes cls', the array of the offsets o, the table of the rows rowOf at the keys of the packings and the number rows of rows made.

• size_eq : o.size = size

  The array of the offsets keeps its size.

• size_rowOf : rowOf.size = 2 ^ numStrides

  The table of the rows keeps its 2 ^ Ratpoints.numStrides entries.

• rows_eq : rows = firstKeys cls m

  One row is made for each distinct packing of the classes below m with a pattern.

• eq_of_le (b : Nat) : b < 64 → m ≤ b → cls'[b]! = cls[b]!

  The classes from m on are as they were.

• entry (b : Nat) : b < m → (cls'[b]! = let __src := cls[b]!; { bits := __src.bits, k := __src.k, a0 := __src.a0, offset := cls'[b]!.offset }) ∧ (cls[b]!.bits ≠ 0 → ∃ (r : Nat), r < rows ∧ cls'[b]!.offset = some (r * np) ∧ rowOf[cls[b]!.key]! = some (r * np) ∧ ∀ (n : Nat), n < np → o[r * np + n]! = classOffset es rinv cls[b]! n)

  Each class below m changes only in its row offsets, and one with a pattern has the row of its packing, at a position r np for some r < rows, which the table of the rows holds at its key and whose np offsets are those of the class.

• exists_of_isSome (K : Nat) : rowOf[K]!.isSome = true → ∃ (b : Nat), b < m ∧ cls[b]!.bits ≠ 0 ∧ cls[b]!.key = K

  The table holds a row only at the key of a class below m with a pattern.

def Ratpoints.Sieve.RowInvariant (es : Array SieveEntry) (rinv : Array (Array Nat)) (cl : NumClass) (row : Nat) (o0 : Array Nat) (j : Nat) (o : Array Nat) : Prop

The invariant of the loop of Ratpoints.Sieve.classRows that writes the row of the class cl at the position row into the array of the offsets o₀, after the moduli below j: the array keeps its size, and holds the offsets of the class for these moduli at their positions in the array.

Equations

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

theorem Ratpoints.Sieve.classRowsInvariant_init (cls : Vector NumClass 64) (es : Array SieveEntry) (rinv : Array (Array Nat)) (np : Nat) (offsets : Array Nat) : ClassRowsInvariant cls es rinv np offsets.size [].length cls offsets (Array.replicate (2 ^ numStrides) none) 0

theorem Ratpoints.Sieve.ClassRowsInvariant.post {cls : Vector NumClass 64} {es : Array SieveEntry} {rinv : Array (Array Nat)} {np : Nat} {offsets : Array Nat} {cls' : Vector NumClass 64} {o : Array Nat} {rowOf : Array (Option Nat)} {rows : Nat} (h : ClassRowsInvariant cls es rinv np offsets.size (ForIn.toList [:64]).length cls' o rowOf rows) {b : Nat} (hb : b < 64) : (cls'[b]! = have __src := cls[b]!; { bits := __src.bits, k := __src.k, a0 := __src.a0, offset := cls'[b]!.offset }) ∧ (¬cls[b]!.bits = 0 → ∃ (pos : Nat), cls'[b]!.offset = some pos ∧ ∀ (n : Nat), n < np → o[pos + n]! = classOffset es rinv cls[b]! n)

theorem Ratpoints.Sieve.ClassRowsInvariant.skip {cls : Vector NumClass 64} {es : Array SieveEntry} {rinv : Array (Array Nat)} {np size : Nat} {pref suff : List Nat} {cur : Nat} (hl : ForIn.toList [:64] = pref ++ cur :: suff) {cls' : Vector NumClass 64} {o : Array Nat} {rowOf : Array (Option Nat)} {rows : Nat} (h : ClassRowsInvariant cls es rinv np size pref.length cls' o rowOf rows) (hc : cur < 64) (hb : (cls'[cur].bits == 0) = true) : ClassRowsInvariant cls es rinv np size (pref ++ [cur]).length cls' o rowOf rows

A class without a pattern is stepped over: it is not the first with its key, and it keeps its offsets.

theorem Ratpoints.Sieve.ClassRowsInvariant.exists_row_of_getElem!_eq_some {cls : Vector NumClass 64} {es : Array SieveEntry} {rinv : Array (Array Nat)} {np size cur : Nat} (hwf : ∀ (b : Nat), b < 64 → cls[b]!.WF) {cls' : Vector NumClass 64} {o : Array Nat} {rowOf : Array (Option Nat)} {rows : Nat} (h : ClassRowsInvariant cls es rinv np size cur cls' o rowOf rows) (hc : cur < 64) {row : Nat} (hrow : rowOf[cls[cur]!.key]! = some row) : ∃ (r : Nat), r < rows ∧ row = r * np ∧ (∀ (n : Nat), n < np → o[r * np + n]! = classOffset es rinv cls[cur]! n) ∧ ¬IsFirstKey cls cur

A key with a row is the key of an earlier class with a pattern, whose row it is: a class with that key is not the first with it, and its row holds its offsets, since the earlier class has the same stride and residue.

theorem Ratpoints.Sieve.ClassRowsInvariant.reuse {cls : Vector NumClass 64} {es : Array SieveEntry} {rinv : Array (Array Nat)} {np size : Nat} {pref suff : List Nat} {cur : Nat} (hl : ForIn.toList [:64] = pref ++ cur :: suff) (hwf : ∀ (b : Nat), b < 64 → cls[b]!.WF) {cls' : Vector NumClass 64} {o : Array Nat} {rowOf : Array (Option Nat)} {rows : Nat} (h : ClassRowsInvariant cls es rinv np size pref.length cls' o rowOf rows) (hc : cur < 64) {row : Nat} (hrow : rowOf[2 ^ cls'[cur].k + cls'[cur].a0]! = some row) : ClassRowsInvariant cls es rinv np size (pref ++ [cur]).length (cls'.set cur (have __src := cls'[cur]; { bits := __src.bits, k := __src.k, a0 := __src.a0, offset := some row }) hc) o rowOf rows

A class with a pattern whose key has a row already gets that row: an earlier class has its key, so it is not the first with it, and has the same stride and residue, so the same offsets.

theorem Ratpoints.Sieve.rowInvariant_nil (es : Array SieveEntry) (rinv : Array (Array Nat)) (cl : NumClass) (row : Nat) (o : Array Nat) : RowInvariant es rinv cl row o [].length o

theorem Ratpoints.Sieve.RowInvariant.set! {es : Array SieveEntry} {rinv : Array (Array Nat)} {cl : NumClass} {row np : Nat} {o0 o : Array Nat} {pref suff : List Nat} {n : Nat} (hl : ForIn.toList [:np] = pref ++ n :: suff) (h : RowInvariant es rinv cl row o0 pref.length o) : RowInvariant es rinv cl row o0 (pref ++ [n]).length (o.set! (row + n) (classOffset es rinv cl n))

theorem Ratpoints.Sieve.ClassRowsInvariant.isFirstKey {cls : Vector NumClass 64} {es : Array SieveEntry} {rinv : Array (Array Nat)} {np size cur : Nat} {cls' : Vector NumClass 64} {o : Array Nat} {rowOf : Array (Option Nat)} {rows : Nat} (h : ClassRowsInvariant cls es rinv np size cur cls' o rowOf rows) (hb : cls[cur]!.bits ≠ 0) (hnone : rowOf[cls[cur]!.key]! = none) : IsFirstKey cls cur

The class cur with a pattern whose key has no row is the first with its key: an earlier class with its key would have put its row into the table.

theorem Ratpoints.Sieve.ClassRowsInvariant.add_one_mul_le {cls : Vector NumClass 64} {es : Array SieveEntry} {rinv : Array (Array Nat)} {np size cur : Nat} {cls' : Vector NumClass 64} {o : Array Nat} {rowOf : Array (Option Nat)} {rows : Nat} (h : ClassRowsInvariant cls es rinv np size cur cls' o rowOf rows) (hf : IsFirstKey cls cur) (hcur : cur < 64) (hsize : firstKeys cls 64 * np ≤ size) : (rows + 1) * np ≤ size

The first class with its key gets the row rows, which the array has room for when it has room for a row for each distinct packing.

theorem Ratpoints.Sieve.ClassRowsInvariant.newRow {cls : Vector NumClass 64} {es : Array SieveEntry} {rinv : Array (Array Nat)} {np size : Nat} {pref suff : List Nat} {cur : Nat} (hl : ForIn.toList [:64] = pref ++ cur :: suff) (hwf : ∀ (b : Nat), b < 64 → cls[b]!.WF) (hsize : firstKeys cls 64 * np ≤ size) {cls' : Vector NumClass 64} {o : Array Nat} {rowOf : Array (Option Nat)} {rows : Nat} (h : ClassRowsInvariant cls es rinv np size pref.length cls' o rowOf rows) (hc : cur < 64) (hb : ¬(cls'[cur].bits == 0) = true) {x : Option Nat} (hnone : ∀ (row : Nat), x = some row → False) (hx : rowOf[2 ^ cls'[cur].k + cls'[cur].a0]! = x) {o' : Array Nat} (hrow : RowInvariant es rinv cls'[cur] (rows * np) o (ForIn.toList [:np]).length o') : ClassRowsInvariant cls es rinv np size (pref ++ [cur]).length (cls'.set cur (have __src := cls'[cur]; { bits := __src.bits, k := __src.k, a0 := __src.a0, offset := some (rows * np) }) hc) o' (rowOf.set! (2 ^ cls'[cur].k + cls'[cur].a0) (some (rows * np))) (rows + 1)

A class with a pattern whose key has no row gets a new row, after the rows made so far: it is the first with its key, and the earlier rows keep their offsets.

theorem Ratpoints.Sieve.classRows_spec (cls : Vector NumClass 64) (es : Array SieveEntry) (rinv : Array (Array Nat)) (np : Nat) (offsets : Array Nat) : ⦃ (∀ (b : Nat), b < 64 → cls[b]!.WF) ∧ firstKeys cls 64 * np ≤ offsets.size ⦄ classRows cls es rinv np offsets ⦃ fun (r : Vector NumClass 64 × Array Nat) => ∀ (b : Nat), b < 64 → r.fst[b]! = { bits := cls[b]!.bits, k := cls[b]!.k, a0 := cls[b]!.a0, offset := r.fst[b]!.offset } ∧ (¬cls[b]!.bits = 0 → ∃ (pos : Nat), r.fst[b]!.offset = some pos ∧ ∀ (n : Nat), n < np → r.snd[pos + n]! = classOffset es rinv cls[b]! n) ⦄

Each class with a pattern gets the row of its packing, whose offset for the n-th modulus is Ratpoints.Sieve.classOffset, when the array of the offsets has room for a row of np offsets for each distinct packing; the classes keep their patterns, strides and residues.

The offsets of the rows

def Ratpoints.Sieve.halveIter (p : Nat) : Nat → Nat → Nat

x halved n times modulo p (Ratpoints.Sieve.halve).

Equations

• Ratpoints.Sieve.halveIter p 0 x✝ = x✝
• Ratpoints.Sieve.halveIter p n.succ x✝ = Ratpoints.Sieve.halve (Ratpoints.Sieve.halveIter p n x✝) p

def Ratpoints.Sieve.halveChain (p n x : Nat) : List Nat

The chain of halvings of x modulo p of class_offsets, x, x / 2, … modulo p, n of them.

Equations

• Ratpoints.Sieve.halveChain p n x = List.map (fun (x_1 : Nat) => Ratpoints.Sieve.halveIter p x_1 x) (List.range n)

theorem Ratpoints.Sieve.halve_lt {x p : Nat} (hx : x < p) : halve x p < p

theorem Ratpoints.Sieve.two_mul_halve_mod {x p : Nat} (hp : p % 2 = 1) : 2 * halve x p % p = x % p

theorem Ratpoints.Sieve.halveIter_lt {x p : Nat} (hx : x < p) (n : Nat) : halveIter p n x < p

theorem Ratpoints.Sieve.halveIter_mul_two_pow_mod {p : Nat} (hp : p % 2 = 1) (x n : Nat) : halveIter p n x * 2 ^ n % p = x % p

Halving n times modulo the odd p divides by 2 ^ n modulo p.

theorem Ratpoints.Sieve.halveIter_mul_two_pow_mul_mod {p x0 L : Nat} (hp : p % 2 = 1) (hx : x0 * L % p = 1) (k : Nat) : halveIter p k x0 * (2 ^ k * L) % p = 1

The inverse x₀ of L modulo the odd p, halved k times, is the inverse of 2 ^ k L.

theorem Ratpoints.Sieve.getElem!_toArray_halveChain {p n x k : Nat} (hk : k < n) : (halveChain p n x).toArray[k]! = halveIter p k x

structure Ratpoints.Sieve.SieveEntry.PackedFor (e : SieveEntry) (cl : NumClass) (off : Nat) : Prop

The offset off of the row of the packing of the class cl for the sieve entry e with its inverses of the strides: off lies between Ratpoints.rowBias and Ratpoints.rowBias + 2 p, it shifts the rows so that bit t of the bit array with the word number w stands for the numerator a₀ + 2 ^ k (Ratpoints.rbaLength w + t) (off 2 ^ k Ratpoints.rbaLength ≡ a₀ (mod p)), and the inverse of the stride 2 ^ k modulo p is entry k of dinv.

• pos : 0 < e.p

  The modulus is positive.

• le_maxPrimeEven : e.p ≤ maxPrimeEven

  The modulus is at most Ratpoints.maxPrimeEven.

• rowBias_le : rowBias ≤ off

  The offset is at least Ratpoints.rowBias.

• lt_rowBias_add : off < rowBias + 2 * e.p

  The offset is below Ratpoints.rowBias + 2 p.

• mul_mod : off * (2 ^ cl.k * rbaLength) % e.p = cl.a0 % e.p

  The offset times 2 ^ k Ratpoints.rbaLength is the residue a₀ modulo the modulus.

• dinv_mul_mod : e.dinv[cl.k]! * 2 ^ cl.k % e.p = 1

  Entry k of dinv is the inverse of 2 ^ k modulo the modulus.

• dinv_lt : e.dinv[cl.k]! < e.p

  Entry k of dinv is below the modulus.

theorem Ratpoints.Sieve.SieveEntry.PackedFor.withOffset {e : SieveEntry} {cl : NumClass} {off : Nat} (h : e.PackedFor cl off) (o : Option Nat) : e.PackedFor { bits := cl.bits, k := cl.k, a0 := cl.a0, offset := o } off

Ratpoints.Sieve.SieveEntry.PackedFor reads only the stride and the residue of the class, not its row offsets.

theorem Ratpoints.Sieve.SieveEntry.PackedFor.fits {e : SieveEntry} {cl : NumClass} {off : Nat} (h : e.PackedFor cl off) (r st : Nat) : { p := e.p, offset := off, row := closedRow e.admits e.p r, start := st, stop := e.p }.Fits

The sieve spec of a modulus with the offset of the packing of a class, the closed form of a row of the entry and the end p has the modulus and the offset in the range that the reductions of the row indices need, and the copies of the first bit arrays of its row (Ratpoints.Sieve.SieveEntry.wraps_closedRow).

def Ratpoints.Sieve.OffsetsFor (cls : Vector NumClass 64) (es : List SieveEntry) (offsets : Array Nat) : Prop

Every class with a pattern among cls has a row of offsets in the array offsets, at the position pos that it holds, with the offset for the n-th sieve entry of es at pos + n.

Equations

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

theorem Ratpoints.Sieve.OffsetsFor.take {cls : Vector NumClass 64} {es : List SieveEntry} {offsets : Array Nat} (h : OffsetsFor cls es offsets) (k : Nat) : OffsetsFor cls (List.take k es) offsets

The rows of offsets of the classes for the sieve entries es serve the first k of them.

theorem Ratpoints.Sieve.SieveEntry.Packable.packedFor {e : SieveEntry} (he : e.Packable) {cl : NumClass} (hcl : cl.WF) {kmax : Nat} (hk : cl.k ≤ kmax) : { p := e.p, factors := e.factors, magic := e.magic, bias := e.bias, rbainv := e.rbainv, dinv := (halveChain e.p (kmax + 1) 1).toArray, ref := e.ref, init := e.init, r := e.r, nf := e.nf }.PackedFor cl (mulMod (cl.a0 * halveIter e.p cl.k e.rbainv) e.p e.magic + e.bias)

The offset that class_offsets computes for the class cl and the sieve entry e, from the inverse of 2 ^ k Ratpoints.rbaLength that the halvings give, is that of the packing.

The loops of the row offsets

def Ratpoints.Sieve.KmaxInvariant (cls : Vector NumClass 64) (m kmax : Nat) : Prop

The invariant of the loop of Ratpoints.Sieve.classOffsets that finds the largest stride exponent: the classes below m with a pattern have stride exponents at most kmax.

Equations

• Ratpoints.Sieve.KmaxInvariant cls m kmax = ∀ (b : Nat), b < m → cls[b]!.bits ≠ 0 → cls[b]!.k ≤ kmax

theorem Ratpoints.Sieve.kmaxInvariant_nil (cls : Vector NumClass 64) : KmaxInvariant cls [].length 0

theorem Ratpoints.Sieve.KmaxInvariant.append_of_le {cls : Vector NumClass 64} {pref suff : List Nat} {cur kmax kmax' : Nat} (hl : ForIn.toList [:64] = pref ++ cur :: suff) (h : KmaxInvariant cls pref.length kmax) (hc : cur < 64) (hle : kmax ≤ kmax') (hk : cls[cur].bits ≠ 0 → cls[cur].k ≤ kmax') : KmaxInvariant cls (pref ++ [cur]).length kmax'

theorem Ratpoints.Sieve.KmaxInvariant.append_of_lt {cls : Vector NumClass 64} {pref suff : List Nat} {cur kmax : Nat} (hl : ForIn.toList [:64] = pref ++ cur :: suff) (h : KmaxInvariant cls pref.length kmax) (hc : cur < 64) (hb : (cls[cur].bits != 0 && decide (kmax < cls[cur].k)) = true) : KmaxInvariant cls (pref ++ [cur]).length cls[cur].k

theorem Ratpoints.Sieve.KmaxInvariant.append_of_not_lt {cls : Vector NumClass 64} {pref suff : List Nat} {cur kmax : Nat} (hl : ForIn.toList [:64] = pref ++ cur :: suff) (h : KmaxInvariant cls pref.length kmax) (hc : cur < 64) (hb : ¬(cls[cur].bits != 0 && decide (kmax < cls[cur].k)) = true) : KmaxInvariant cls (pref ++ [cur]).length kmax

def Ratpoints.Sieve.HalvingInvariant (p x0 j : Nat) (s : Nat × Nat × Array Nat × Array Nat) : Prop

The invariant of the loop over the halvings of Ratpoints.Sieve.classOffsets for the modulus p and the inverse x₀ of Ratpoints.rbaLength, after j steps: d and x are 1 and x₀ halved j times, and the arrays dinv and ri hold the chains of the halvings so far.

Equations

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

theorem Ratpoints.Sieve.halvingInvariant_zero (p x0 : Nat) : HalvingInvariant p x0 [].length (1, x0, #[], #[])

theorem Ratpoints.Sieve.HalvingInvariant.push {p x0 : Nat} {pref : List Nat} {cur : Nat} {s : Nat × Nat × Array Nat × Array Nat} (h : HalvingInvariant p x0 pref.length s) : HalvingInvariant p x0 (pref ++ [cur]).length (halve s.fst p, halve s.snd.fst p, s.snd.snd.fst.push s.fst, s.snd.snd.snd.push s.snd.fst)

def Ratpoints.Sieve.EntriesInvariant (kmax : Nat) (pref : List SieveEntry) (s : Array SieveEntry × Array (Array Nat)) : Prop

The invariant of the loop over the sieve entries of Ratpoints.Sieve.classOffsets after the entries pref: the entries so far with their inverses of the strides, and the chains of the halvings of their inverses of Ratpoints.rbaLength, for the strides up to kmax.

Equations

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

theorem Ratpoints.Sieve.entriesInvariant_nil (kmax : Nat) : EntriesInvariant kmax [] (#[], #[])

theorem Ratpoints.Sieve.EntriesInvariant.push {kmax : Nat} {pref : List SieveEntry} {e : SieveEntry} {es' : Array SieveEntry} {rinv : Array (Array Nat)} (h : EntriesInvariant kmax pref (es', rinv)) {s : Nat × Nat × Array Nat × Array Nat} (hs : HalvingInvariant e.p e.rbainv (ForIn.toList [:kmax + 1]).length s) : EntriesInvariant kmax (pref ++ [e]) (es'.push { p := e.p, factors := e.factors, magic := e.magic, bias := e.bias, rbainv := e.rbainv, dinv := s.snd.snd.fst, ref := e.ref, init := e.init, r := e.r, nf := e.nf }, rinv.push s.snd.snd.snd)

theorem Ratpoints.Sieve.EntriesInvariant.packedFor {kmax : Nat} {es : List SieveEntry} {es' : Array SieveEntry} {rinv : Array (Array Nat)} (he : EntriesInvariant kmax es (es', rinv)) (hes : ∀ (e : SieveEntry), e ∈ es → e.Packable) {cl : NumClass} (hcl : cl.WF) (hk : cl.k ≤ kmax) {n : Nat} (hn : n < es.length) : es'[n]!.PackedFor cl (classOffset es' rinv cl n)

The offset of the row of a class for the n-th entry, from the arrays that the halvings give, is that of the packing of the class for that entry with its inverses of the strides.

theorem Ratpoints.Sieve.classOffsets_post {cls cls' : Vector NumClass 64} {es : List SieveEntry} {kmax : Nat} {es' : Array SieveEntry} {rinv : Array (Array Nat)} {size : Nat} {o : Array Nat} (hpre : (∀ (e : SieveEntry), e ∈ es → e.Packable) ∧ (∀ (b : Nat), b < 64 → cls[b]!.WF) ∧ firstKeys cls 64 * es.length ≤ size) (hk : KmaxInvariant cls (ForIn.toList [:64]).length kmax) (he : EntriesInvariant kmax es (es', rinv)) (hr : ∀ (b : Nat), b < 64 → (cls'[b]! = have __src := cls[b]!; { bits := __src.bits, k := __src.k, a0 := __src.a0, offset := cls'[b]!.offset }) ∧ (¬cls[b]!.bits = 0 → ∃ (pos : Nat), cls'[b]!.offset = some pos ∧ ∀ (n : Nat), n < es.length → o[pos + n]! = classOffset es' rinv cls[b]! n)) : (∀ (b : Nat), b < 64 → cls'[b]! = have __src := cls[b]!; { bits := __src.bits, k := __src.k, a0 := __src.a0, offset := cls'[b]!.offset }) ∧ (∃ (f : SieveEntry → Array Nat), es'.toList = List.map (fun (e : SieveEntry) => { p := e.p, factors := e.factors, magic := e.magic, bias := e.bias, rbainv := e.rbainv, dinv := f e, ref := e.ref, init := e.init, r := e.r, nf := e.nf }) es) ∧ OffsetsFor cls' es'.toList o

The classes after class_offsets have the rows of their packings for the entries with their inverses of the strides.

theorem Ratpoints.Sieve.classOffsets_spec (cls : Vector NumClass 64) (es : List SieveEntry) (offsets : Array Nat) : ⦃ (∀ (e : SieveEntry), e ∈ es → e.Packable) ∧ (∀ (b : Nat), b < 64 → cls[b]!.WF) ∧ firstKeys cls 64 * es.length ≤ offsets.size ⦄ classOffsets cls es offsets ⦃ fun (r : Vector NumClass 64 × List SieveEntry × Array Nat) => (∀ (b : Nat), b < 64 → r.fst[b]! = { bits := cls[b]!.bits, k := cls[b]!.k, a0 := cls[b]!.a0, offset := r.fst[b]!.offset }) ∧ (∃ (f : SieveEntry → Array Nat), r.snd.fst = List.map (fun (e : SieveEntry) => { p := e.p, factors := e.factors, magic := e.magic, bias := e.bias, rbainv := e.rbainv, dinv := f e, ref := e.ref, init := e.init, r := e.r, nf := e.nf }) es) ∧ OffsetsFor r.fst r.snd.fst r.snd.snd ⦄

The row offsets of the classes, once the moduli of the run are known: each class with a pattern gets the row of its packing in the array of the offsets, for the sieve entries with their inverses of the strides, when the array has room for a row for each distinct packing; the classes keep their patterns, strides and residues, and the entries are those of the run with the inverses of the strides.

The residues of a denominator

theorem Ratpoints.Sieve.mulMod_mul_magic {b d p : Nat} (hp : 0 < p) (hpm : p ≤ maxPrimeEven) (hd : d < p) (hb : b ≤ mulModLimit / maxPrimeEven) : mulMod (b * d) p (magic p) = b * d % p

The first branch of fill_bp_list: for b ≤ Ratpoints.mulModLimit / Ratpoints.maxPrimeEven the product b dinv is reduced at once, exactly.

theorem Ratpoints.Sieve.mulMod_mulMod_mul_magic {b d p : Nat} (hp : 0 < p) (hpm : p ≤ maxPrimeEven) (hd : d < p) (hb : b ≤ mulModLimit) : mulMod (mulMod b p (magic p) * d) p (magic p) = b * d % p

The second branch of fill_bp_list: for b ≤ Ratpoints.mulModLimit, b is reduced first and then its product with dinv, both exactly.

theorem Ratpoints.Sieve.mulMod_toNat_modLong_mul_magic {b d p : Nat} (hp : 0 < p) (hpm : p ≤ maxPrimeEven) (hd : d < p) : mulMod ((modLong ↑b ↑p).toNat * d) p (magic p) = b * d % p

The third branch of fill_bp_list: b reduced by the helper mod of the C code, then the product with dinv exactly.

theorem Ratpoints.Sieve.fillBpList_eq_map {b k : Nat} {es : List SieveEntry} (hes : ∀ (e : SieveEntry), e ∈ es → 0 < e.p ∧ e.p ≤ maxPrimeEven ∧ e.dinv[k]! < e.p) : fillBpList b k es (List.map (fun (x : SieveEntry) => magic x.p) es) = List.map (fun (e : SieveEntry) => b * e.dinv[k]! % e.p) es

fill_bp_list computes b dinv[k] mod p for every modulus 0 < p ≤ Ratpoints.maxPrimeEven with dinv[k] < p, in each of its three branches, with the reciprocals of the moduli.