The bits of an interval of numerators and the longs of the packing

numerators_to_bits turns an interval of numerators into the bits of the packing of a class, whose bit j stands for the numerator a₀ + 2 ^ k j (Ratpoints.Sieve.NumClass.numerator), on the longs of the C code (Ratpoints.Sieve.numeratorsToBits): in both its forms it gives ⌈(low - a₀) / 2 ^ k⌉ and ⌊(high - a₀) / 2 ^ k⌋, the split form for all ends and the plain form when the differences a₀ - low and high - a₀ are longs, with no overflow, since the arithmetic shift of a long is the floor of its quotient by 2 ^ k and its and with the mask 2 ^ k - 1 the Euclidean remainder. For the numerators -H, …, H of a height bound H < 2 ^ 63, a numerator of the class lies in the interval exactly when its bit lies between the two bits, and the numerators of these bits, in increasing order, are those of -H, …, H in the class a₀ mod 2 ^ k. The values that the C code holds in longs for the packing stay in range (Ratpoints.fitsLong): the offsets of the rows, the first and the last bit of the bit arrays of -H, …, H, the numerators of their bits, and the sums of a word number and an offset that the first two stages reduce outside the test small; the products of fill_bp_list and of class_offsets are bounded in Ratpoints.Proof.Reductions. The ranges of the numerators that the bounds of the search intervals give for a denominator are stated here too, on Lean core.

Main definitions

• Ratpoints.Sieve.IntervalBounds.Represents, Ratpoints.Sieve.RangesFor, Ratpoints.Sieve.inRanges: the range of the numerators that the bounds of a search interval give for a denominator, the ranges of the search intervals of a run, and the membership in them, the interface between the bounds of the search intervals (Ratpoints.Proof.Bounds) and the sieve of one denominator (Ratpoints.Sieve.sift_spec).

Main statements

• Ratpoints.Sieve.toInt_numeratorsToBits: the bits of the numerators of an interval, in both forms.
• Ratpoints.Sieve.NumClass.le_numerator_and_numerator_le_iff, Ratpoints.Sieve.NumClass.WF.map_range_numerator_eq_filter_numerators: the numerator of a bit lies in an interval exactly when the bit lies between its bits, and the numerators of the bits of -H, …, H are those of -H, …, H in the class of the packing, in increasing order.
• Ratpoints.Sieve.SieveEntry.PackedFor.lt_two_pow_32: the offsets of the rows are below 2 ^ 32, so longs.
• Ratpoints.Sieve.neg_two_pow_le_rbaLength_mul_ediv, Ratpoints.Sieve.rbaLength_mul_ediv_add_one_le_two_pow: the first bit of the bit array of a bit lo ≥ -2 ^ (63 - k) and the bit after the bit array of a bit hi < 2 ^ (63 - k) lie in [-2 ^ (63 - k), 2 ^ (63 - k)], for k ≤ 6.
• Ratpoints.Sieve.NumClass.fitsLong_numerator: the numerators of the bits of the bit arrays of -H, …, H are longs.
• Ratpoints.Sieve.fitsLong_neg_sub, Ratpoints.Sieve.fitsLong_add: the values -w_low - offset and i + offset that the first two stages reduce by the helper mod are longs.
• Ratpoints.Sieve.flatMap_flatMap_filter_eq_flatMap_filter_inRanges: for ranges that increase and are strictly apart, the points of the elements of an increasing list, range after range, are those of the elements in one of the ranges.

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: that Ratpoints.rbaLength = 2 ^ Ratpoints.rbaShift with Ratpoints.rbaShift < 32, that Ratpoints.rbaPack > 0, that Ratpoints.maxBitsInPrime ≤ 10 and that 2 Ratpoints.rowBias - 1 ≤ Ratpoints.mulModLimit < 2 ^ 32; 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 lemmas on the longs of the offsets and of the bit ranges and Ratpoints.Sieve.NumClass.fitsLong_numerator discharge range obligations that the Deviation paragraphs of the model cite, and no contract uses them.

The bits of the numerators

theorem Ratpoints.Sieve.toInt_numeratorsToBits_false {low high : Int64} {cl : NumClass} (hcl : cl.WF) (h1 : ↑cl.a0 - low.toInt < 2 ^ 63) (h2 : -2 ^ 63 ≤ high.toInt - ↑cl.a0) : (numeratorsToBits low high cl false).fst.toInt = -((↑cl.a0 - low.toInt) / 2 ^ cl.k) ∧ (numeratorsToBits low high cl false).snd.toInt = (high.toInt - ↑cl.a0) / 2 ^ cl.k

theorem Ratpoints.Sieve.toInt_numeratorsToBits_true {low high : Int64} {cl : NumClass} (hcl : cl.WF) : (numeratorsToBits low high cl true).fst.toInt = -((↑cl.a0 - low.toInt) / 2 ^ cl.k) ∧ (numeratorsToBits low high cl true).snd.toInt = (high.toInt - ↑cl.a0) / 2 ^ cl.k

theorem Ratpoints.Sieve.toInt_numeratorsToBits {low high : Int64} {cl : NumClass} (hcl : cl.WF) {split : Bool} (hplain : split = false → ↑cl.a0 - low.toInt < 2 ^ 63 ∧ -2 ^ 63 ≤ high.toInt - ↑cl.a0) : (numeratorsToBits low high cl split).fst.toInt = -((↑cl.a0 - low.toInt) / 2 ^ cl.k) ∧ (numeratorsToBits low high cl split).snd.toInt = (high.toInt - ↑cl.a0) / 2 ^ cl.k

The bits of the numerators low, …, high in the packing of a class with k ≤ 6 and a₀ < 2 ^ k, from ⌈(low - a₀) / 2 ^ k⌉ to ⌊(high - a₀) / 2 ^ k⌋, in either form: the split one for all ends, the plain one when the differences a₀ - low and high - a₀ are longs, so that no operation leaves the range of a long.

theorem Ratpoints.Sieve.NumClass.le_numerator_and_numerator_le_iff (cl : NumClass) (lo hi t : Int) : lo ≤ cl.numerator t ∧ cl.numerator t ≤ hi ↔ -((↑cl.a0 - lo) / 2 ^ cl.k) ≤ t ∧ t ≤ (hi - ↑cl.a0) / 2 ^ cl.k

The numerator of bit t of a class lies in lo, …, hi exactly when t lies between the bits of numerators_to_bits (Ratpoints.Sieve.toInt_numeratorsToBits).

theorem Ratpoints.Sieve.NumClass.map_range_eq_filter_map_range (cl : NumClass) {H : Nat} {lo hi : Int} (hlo : -↑H ≤ lo) (hhi : hi ≤ ↑H) : List.map (fun (i : Nat) => -((↑cl.a0 - lo) / 2 ^ cl.k) + ↑i) (List.range ((hi - ↑cl.a0) / 2 ^ cl.k + 1 - -((↑cl.a0 - lo) / 2 ^ cl.k)).toNat) = List.filter (fun (j : Int) => decide (lo ≤ cl.numerator j ∧ cl.numerator j ≤ hi)) (List.map (fun (i : Nat) => -((↑cl.a0 + ↑H) / 2 ^ cl.k) + ↑i) (List.range ((↑H - ↑cl.a0) / 2 ^ cl.k + 1 - -((↑cl.a0 + ↑H) / 2 ^ cl.k)).toNat))

The bits from ⌈(lo - a₀) / 2 ^ k⌉ to ⌊(hi - a₀) / 2 ^ k⌋ of the packing of a class, for -H ≤ lo and hi ≤ H, are those from ⌈(-H - a₀) / 2 ^ k⌉ to ⌊(H - a₀) / 2 ^ k⌋, the bits of the numerators -H, …, H (Ratpoints.Sieve.toInt_numeratorsToBits), whose numerators lie in lo, …, hi (Ratpoints.Sieve.NumClass.le_numerator_and_numerator_le_iff).

theorem Ratpoints.BruteForce.filter_numerators_emod_eq {a0 m : Nat} (ha : a0 < m) (H : Nat) : List.filter (fun (a : Int) => a % ↑m == ↑a0) (numerators H) = List.map (fun (j : Nat) => (↑a0 + ↑H) % ↑m + ↑m * ↑j - ↑H) (List.range ((2 * H + 1 + (m - 1 - (a0 + H) % m)) / m))

The numerators of -H, …, H that are a₀ modulo m, for a₀ < m, in increasing order: r - H, r + m - H, …, for the residue r of a₀ + H modulo m.

theorem Ratpoints.Sieve.NumClass.WF.map_range_numerator_eq_filter_numerators {cl : NumClass} (hcl : cl.WF) {H : Nat} {lo hi : Int} (hlo : lo = -((↑cl.a0 + ↑H) / 2 ^ cl.k)) (hhi : hi = (↑H - ↑cl.a0) / 2 ^ cl.k) : List.map (fun (i : Nat) => cl.numerator (lo + ↑i)) (List.range (hi + 1 - lo).toNat) = List.filter (fun (a : Int) => a % 2 ^ cl.k == ↑cl.a0) (BruteForce.numerators H)

The numerators of -H, …, H that are a₀ modulo the stride 2 ^ k of a class, in increasing order, are those of the bits from lo = ⌈(-H - a₀) / 2 ^ k⌉ to hi = ⌊(H - a₀) / 2 ^ k⌋.

The longs of the offsets and of the bit ranges

theorem Ratpoints.Sieve.SieveEntry.PackedFor.lt_two_pow_32 {e : SieveEntry} {cl : NumClass} {off : Nat} (h : e.PackedFor cl off) : off < 2 ^ 32

The offsets of the rows are below Ratpoints.rowBias + 2 p ≤ 2 ^ 31 + 2 ^ 11 < 2 ^ 32, so longs, and in the range that Ratpoints.Sieve.fitsLong_neg_sub and Ratpoints.Sieve.fitsLong_add take.

theorem Ratpoints.Sieve.neg_two_pow_le_rbaLength_mul_ediv {k : Nat} (hk : k ≤ 6) {lo : Int} (hlo : -2 ^ (63 - k) ≤ lo) : -2 ^ (63 - k) ≤ ↑rbaLength * (lo / ↑rbaLength)

The first bit Ratpoints.rbaLength ⌊lo / Ratpoints.rbaLength⌋ of the bit array of the bit lo ≥ -2 ^ (63 - k) is at least -2 ^ (63 - k), for a stride 2 ^ k, k ≤ 6, since Ratpoints.rbaLength divides 2 ^ (63 - k).

theorem Ratpoints.Sieve.rbaLength_mul_ediv_add_one_le_two_pow {k : Nat} (hk : k ≤ 6) {hi : Int} (hhi : hi < 2 ^ (63 - k)) : ↑rbaLength * (hi / ↑rbaLength + 1) ≤ 2 ^ (63 - k)

The bit Ratpoints.rbaLength (⌊hi / Ratpoints.rbaLength⌋ + 1) after the bit array of the bit hi < 2 ^ (63 - k) is at most 2 ^ (63 - k), for a stride 2 ^ k, k ≤ 6, since Ratpoints.rbaLength divides 2 ^ (63 - k).

theorem Ratpoints.Sieve.NumClass.fitsLong_numerator {cl : NumClass} (hcl : cl.WF) {H : Nat} (hH : H < 2 ^ 63) {j : Int} (hj : ↑rbaLength * (-((↑cl.a0 + ↑H) / 2 ^ cl.k) / ↑rbaLength) ≤ j) (hj' : j < ↑rbaLength * ((↑H - ↑cl.a0) / 2 ^ cl.k / ↑rbaLength + 1)) : fitsLong (cl.numerator j) = true

The numerators of the bits of the bit arrays from ⌊lo / Ratpoints.rbaLength⌋ to ⌊hi / Ratpoints.rbaLength⌋, for the bits lo = ⌈(-H - a₀) / 2 ^ k⌉ and hi = ⌊(H - a₀) / 2 ^ k⌋ of the numerators -H, …, H of a height bound H < 2 ^ 63 in the packing of a class (Ratpoints.Sieve.toInt_numeratorsToBits), are longs: the extraction computes them, and the first numerators of the words, as longs.

theorem Ratpoints.Sieve.fitsLong_neg_sub {w : Int} {off : Nat} (hw : -2 ^ 63 ≤ ↑rbaLength * w) (hw' : ↑rbaLength * w ≤ 2 ^ 63) (hoff : off < 2 ^ 32) : fitsLong (-w - ↑off) = true

A word number w with -2 ^ 63 ≤ Ratpoints.rbaLength w ≤ 2 ^ 63, the word numbers of the bit arrays of the numerators of a height bound below 2 ^ 63 (Ratpoints.Sieve.neg_two_pow_le_rbaLength_mul_ediv, Ratpoints.Sieve.rbaLength_mul_ediv_add_one_le_two_pow), minus an offset below 2 ^ 32 is a long: the value -w_low - offset that the first stage reduces by the helper mod outside the test small.

theorem Ratpoints.Sieve.fitsLong_add {w : Int} {off : Nat} (hw : -2 ^ 63 ≤ ↑rbaLength * w) (hw' : ↑rbaLength * w ≤ 2 ^ 63) (hoff : off < 2 ^ 32) : fitsLong (w + ↑off) = true

A word number w with -2 ^ 63 ≤ Ratpoints.rbaLength w ≤ 2 ^ 63, the word numbers of the bit arrays of the numerators of a height bound below 2 ^ 63 (Ratpoints.Sieve.neg_two_pow_le_rbaLength_mul_ediv, Ratpoints.Sieve.rbaLength_mul_ediv_add_one_le_two_pow), plus an offset below 2 ^ 32 is a long: the values w_low + offset and i + offset that the chunked first stage and the second stage reduce by the helper mod outside the test small.

The numerator ranges of the search intervals

structure Ratpoints.Sieve.IntervalBounds.Represents (bd : IntervalBounds) (b H : Nat) (lo hi : Int) : Prop

The bounds bd of a search interval give, for the denominator b and the height bound H, the range of the numerators lo, …, hi (empty when hi < lo), as Ratpoints.Sieve.intervalBits reads them for every class with k ≤ 6, k < Ratpoints.numStrides and a₀ < 2 ^ k (Ratpoints.Sieve.NumClass.WF): the code 2 only when the range lies above H, the code 1 only when it lies below -H, and otherwise the bits of the numerators from max lo (-H) to min hi H in the packing of the class (Ratpoints.Sieve.toInt_numeratorsToBits). For the bounds of a search interval [l, u] and a denominator up to the largest one, lo = ⌈b l⌉ and hi = ⌊b u⌋.

• two (cl : NumClass) : cl.WF → (intervalBits b.toInt64 bd H.toInt64 cl).fst = 2 → ↑H < lo

  The code 2 only for a range above H.

• one (cl : NumClass) : cl.WF → (intervalBits b.toInt64 bd H.toInt64 cl).fst = 1 → hi < -↑H

  The code 1 only for a range below -H.

• bits (cl : NumClass) : cl.WF → (intervalBits b.toInt64 bd H.toInt64 cl).fst ≠ 1 → (intervalBits b.toInt64 bd H.toInt64 cl).fst ≠ 2 → (intervalBits b.toInt64 bd H.toInt64 cl).snd.fst.toInt = -((↑cl.a0 - max lo (-↑H)) / 2 ^ cl.k) ∧ (intervalBits b.toInt64 bd H.toInt64 cl).snd.snd.toInt = (min hi ↑H - ↑cl.a0) / 2 ^ cl.k

  Otherwise the bits of the numerators of the range within -H, …, H.

structure Ratpoints.Sieve.RangesFor (iv : Array IntervalBounds) (b H : Nat) (rs : List (Int × Int)) : Prop

The bounds iv of the search intervals of a run give, for the denominator b and the height bound H, the ranges of the numerators rs, one for each interval in turn (Ratpoints.Sieve.IntervalBounds.Represents), each with lo ≤ hi + 1, increasing and strictly apart: what the loop of Ratpoints.Sieve.sift over the intervals needs, which returns at the first interval above H.

• length_eq : iv.size = rs.length

  One range for each interval.

• represents (p : IntervalBounds × Int × Int) : p ∈ iv.toList.zip rs → p.fst.Represents b H p.snd.fst p.snd.snd

  Each interval gives its range.

• le_add_one (r : Int × Int) : r ∈ rs → r.fst ≤ r.snd + 1

  Each range is empty at most by one.

• pairwise : List.Pairwise (fun (r s : Int × Int) => r.snd < s.fst) rs

  The ranges are increasing and strictly apart.

def Ratpoints.Sieve.inRanges (rs : List (Int × Int)) (a : Int) : Bool

Whether the integer a lies in one of the ranges lo, …, hi of rs.

Equations

• Ratpoints.Sieve.inRanges rs a = rs.any fun (r : Int × Int) => decide (r.fst ≤ a ∧ a ≤ r.snd)

theorem Ratpoints.Sieve.RangesFor.represents_of_eq_append_cons {iv : Array IntervalBounds} {b H : Nat} {rs : List (Int × Int)} (h : RangesFor iv b H rs) {pref suff : List IntervalBounds} {cur : IntervalBounds} (hl : ForIn.toList iv = pref ++ cur :: suff) : ∃ (hk : pref.length < rs.length), cur.Represents b H rs[pref.length].fst rs[pref.length].snd

The bounds cur of a search interval at the position pref.length of the array iv give the range of the numerators at that position of the ranges rs of iv.

theorem Ratpoints.Sieve.RangesFor.lt_fst_of_mem_drop {iv : Array IntervalBounds} {b H : Nat} {rs : List (Int × Int)} (h : RangesFor iv b H rs) {k : Nat} (hk : k < rs.length) {x : Int} (hx : x < rs[k].fst) (rg : Int × Int) : rg ∈ List.drop k rs → x < rg.fst

The ranges of the search intervals from the position k on lie above a number x below the first numerator of the range at k: they are increasing and strictly apart, and each is empty at most by one.

theorem Ratpoints.Sieve.flatMap_flatMap_filter_eq_flatMap_filter_inRanges {l : List Int} (hl : List.Pairwise (fun (x1 x2 : Int) => x1 < x2) l) {rs : List (Int × Int)} (hrs : List.Pairwise (fun (r s : Int × Int) => r.snd < s.fst) rs) (q : Int → Bool) (g : Int → List (Int × Int × Int)) : List.flatMap (fun (rg : Int × Int) => List.flatMap g (List.filter (fun (a : Int) => decide (rg.fst ≤ a ∧ a ≤ rg.snd) && q a) l)) rs = List.flatMap g (List.filter (fun (a : Int) => inRanges rs a && q a) l)

The points of the elements of an increasing list l in each of the ranges rs, which are increasing and strictly apart, that pass q, range after range, are those of the elements of l in one of the ranges (Ratpoints.Sieve.inRanges) that pass q (List.flatMap_filter_eq_filter_any).