The set bits of a word

The bit of a numerator or a bit number in a word (Ratpoints.Sieve.classBit), the contract of the loop of the lowest set bit of a word (Ratpoints.Sieve.ctz), and the invariant of a while loop that walks through the set bits of a word, lowest first, clearing each with x &&& (x - 1) (Ratpoints.Sieve.WalkWhileInvariant), which the walks of the extraction, of the packing of the classes, of the 2-adic information and of the word shape share.

Main definitions

• Ratpoints.Sieve.classBit: whether a word lets a through, bit a mod 64 of the word.
• Ratpoints.Sieve.ClearedBelow: a word with the bits of another below a position cleared.
• Ratpoints.Sieve.WalkWhileInvariant: the invariant of a walk through the set bits of a word, lowest first.
• Ratpoints.Sieve.bitNumbers: the bit numbers of the set bits of some words, in increasing order.

Main statements

• Ratpoints.Sieve.ctz_spec, Ratpoints.Sieve.run_ctz: for a word other than 0, the loop of Ratpoints.Sieve.ctz ends with the number of its trailing zeros.
• Ratpoints.Sieve.ClearedBelow.filter_range_succ_ctz, Ratpoints.Sieve.ClearedBelow.exists_lt_succ_iff: the set bits of the word up to the lowest set bit of the word with the bits below k cleared.

Implementation notes

The file uses Lean core and Std only; the lemmas on words that are not about the model are in Ratpoints.Proof.Bits.

The bit of a number in a word

def Ratpoints.Sieve.classBit (cw : UInt64) (a : Int) : Bool

Whether the word cw lets a through: bit a mod 64 of cw. For the 2-adic word of a class of denominators (Ratpoints.Sieve.twoAdic), a is a numerator. For the pattern of a class in its packing (Ratpoints.Sieve.NumClass.bits), which Ratpoints.Sieve.andRows writes into every word of a piece, a is a bit number: bit a mod 64 of every word stands for the bits ≡ a (mod 64), since 64 divides Ratpoints.rbaLength. Ratpoints.Sieve.NumClass.Packs.classBit_bits converts between the two.

Equations

• Ratpoints.Sieve.classBit cw a = cw.toBitVec.getLsbD (a % 64).toNat

theorem Ratpoints.Sieve.classBit_eq (cw : UInt64) (a : Int) : classBit cw a = cw.toBitVec.getLsbD (a % 64).toNat

@[simp]

theorem Ratpoints.Sieve.classBit_zero (a : Int) : classBit 0 a = false

The lowest set bit

def Ratpoints.Sieve.CtzInvariant (w : UInt64) : Std.WP.WhileInvariant (UInt64 × Nat) Prop

The invariant of the loop of Ratpoints.Sieve.ctz on a word w ≠ 0: the word is w shifted right by the count, the count is at most the position of the lowest set bit of w, and it is that position at the exit.

Equations

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

theorem Ratpoints.Sieve.ctz_spec (w : UInt64) : ⦃ w ≠ 0 ⦄ ctz w ⦃ fun (t : Nat) => t = w.toBitVec.ctz.toNat ⦄

The loop ends, since the count stays at most the position of the lowest set bit, which is below 64.

theorem Ratpoints.Sieve.run_ctz {w : UInt64} (hw : w ≠ 0) : (ctz w).run = w.toBitVec.ctz.toNat

The walks through the set bits of a word

def Ratpoints.Sieve.ClearedBelow (x0 : UInt64) (k : Nat) (x : UInt64) : Prop

The word x is the word x0 with its bits below k ≤ 64 cleared.

Equations

• Ratpoints.Sieve.ClearedBelow x0 k x = (k ≤ 64 ∧ ∀ (t : Nat), x.toBitVec.getLsbD t = (x0.toBitVec.getLsbD t && decide (k ≤ t)))

theorem Ratpoints.Sieve.clearedBelow_zero (x0 : UInt64) : ClearedBelow x0 0 x0

theorem Ratpoints.Sieve.ClearedBelow.getLsbD_ctz_and_le_ctz {x0 x : UInt64} {k : Nat} (h : ClearedBelow x0 k x) (hx : x ≠ 0) : x0.toBitVec.getLsbD x.toBitVec.ctz.toNat = true ∧ k ≤ x.toBitVec.ctz.toNat

The lowest set bit of x is a set bit of x0, at k or above.

theorem Ratpoints.Sieve.ClearedBelow.and_sub_one {x0 x : UInt64} {k : Nat} (h : ClearedBelow x0 k x) (hx : x ≠ 0) : ClearedBelow x0 (x.toBitVec.ctz.toNat + 1) (x &&& x - 1)

Clearing the lowest set bit of x clears the bits of x0 up to that bit.

theorem Ratpoints.Sieve.ClearedBelow.filter_range_succ_ctz {x0 x : UInt64} {k : Nat} (h : ClearedBelow x0 k x) (hx : x ≠ 0) : List.filter (fun (x : Nat) => x0.toBitVec.getLsbD x) (List.range (x.toBitVec.ctz.toNat + 1)) = List.filter (fun (x : Nat) => x0.toBitVec.getLsbD x) (List.range k) ++ [x.toBitVec.ctz.toNat]

The set bits of x0 up to the lowest set bit of x are those below k, then that bit, since x has the bits of x0 from k on.

theorem Ratpoints.Sieve.ClearedBelow.filter_range_of_eq_zero {x0 : UInt64} {k : Nat} (h : ClearedBelow x0 k 0) : List.filter (fun (x : Nat) => x0.toBitVec.getLsbD x) (List.range k) = List.filter (fun (x : Nat) => x0.toBitVec.getLsbD x) (List.range 64)

theorem Ratpoints.Sieve.ClearedBelow.exists_lt_succ_iff {x0 x : UInt64} {k : Nat} (h : ClearedBelow x0 k x) (hx : x ≠ 0) (P : Nat → Prop) : (∃ (j : Nat), j < x.toBitVec.ctz.toNat + 1 ∧ x0.toBitVec.getLsbD j = true ∧ P j) ↔ (∃ (j : Nat), j < k ∧ x0.toBitVec.getLsbD j = true ∧ P j) ∨ P x.toBitVec.ctz.toNat

The set bits j of x0 up to the lowest set bit of x that have the property P are those below k, which x has cleared, and the lowest set bit of x if it has the property, a set bit of x0 too.

theorem Ratpoints.Sieve.ClearedBelow.exists_lt_iff_of_eq_zero {x0 : UInt64} {k : Nat} (h : ClearedBelow x0 k 0) (P : Nat → Prop) : (∃ (j : Nat), j < k ∧ x0.toBitVec.getLsbD j = true ∧ P j) ↔ ∃ (j : Nat), j < 64 ∧ x0.toBitVec.getLsbD j = true ∧ P j

def Ratpoints.Sieve.WalkWhileInvariant {σ : Type u} (x0 : UInt64) (P : Nat → σ → Prop) : Std.WP.WhileInvariant (σ × UInt64) Prop

The invariant of a while loop over the set bits of the word x0, lowest first, whose state is a value of σ and the word, for a property P k of the value after the set bits below k: the word is x0 with its bits below some k cleared (Ratpoints.Sieve.ClearedBelow), the value has the property P k, and the word is 0 at the exit.

Equations

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

theorem Ratpoints.Sieve.walkWhileInvariant_self {σ : Type u} {x0 : UInt64} {P : Nat → σ → Prop} {s : σ} (h : P 0 s) : WalkWhileInvariant x0 P false (s, x0)

theorem Ratpoints.Sieve.WalkWhileInvariant.and_sub_one {σ : Type u} {x0 w : UInt64} {P : Nat → σ → Prop} {s s' : σ} {mb : Nat} (h : w.toNat = mb ∧ WalkWhileInvariant x0 P false (s, w)) (hw : (w != 0) = true) (hP : ∀ (k : Nat), ClearedBelow x0 k w → P k s → P (w.toBitVec.ctz.toNat + 1) s') : (w &&& w - 1).toNat < mb ∧ WalkWhileInvariant x0 P false (s', w &&& w - 1)

The invariant after one step, with the lowest set bit of w cleared and the value s' with the property P up to that bit, in the shape of the verification condition: the measure w.toNat decreases.

theorem Ratpoints.Sieve.WalkWhileInvariant.exit {σ : Type u} {x0 w : UInt64} {P : Nat → σ → Prop} {s : σ} {mb : Nat} (hw : ¬(w != 0) = true) (h : w.toNat = mb ∧ WalkWhileInvariant x0 P false (s, w)) : WalkWhileInvariant x0 P true (s, w)

theorem Ratpoints.Sieve.WalkWhileInvariant.exists_clearedBelow_zero {σ : Type u} {x0 w : UInt64} {P : Nat → σ → Prop} {s : σ} (h : WalkWhileInvariant x0 P true (s, w)) : ∃ (k : Nat), ClearedBelow x0 k 0 ∧ P k s

The bit numbers of the set bits of words

def Ratpoints.Sieve.bitNumbers (words : Nat → UInt64) (base : Int) (k : Nat) : List Int

The bit numbers base + 64 κ + t of the set bits t of the words words κ, κ < k, in increasing order.

Equations

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

@[simp]

theorem Ratpoints.Sieve.bitNumbers_zero (words : Nat → UInt64) (base : Int) : bitNumbers words base 0 = []

theorem Ratpoints.Sieve.bitNumbers_succ (words : Nat → UInt64) (base : Int) (k : Nat) : bitNumbers words base (k + 1) = bitNumbers words base k ++ List.map (fun (t : Nat) => base + 64 * ↑k + ↑t) (List.filter (fun (x : Nat) => (words k).toBitVec.getLsbD x) (List.range 64))

theorem Ratpoints.Sieve.bitNumbers_add (words : Nat → UInt64) (base : Int) (k m : Nat) : bitNumbers words base (k + m) = bitNumbers words base k ++ bitNumbers (fun (x : Nat) => words (k + x)) (base + 64 * ↑k) m

theorem Ratpoints.Sieve.bitNumbers_prefix (words : Nat → UInt64) (base : Int) {k m : Nat} (h : k ≤ m) : bitNumbers words base k <+: bitNumbers words base m

theorem Ratpoints.Sieve.bitNumbers_congr {words words' : Nat → UInt64} {k : Nat} (h : ∀ (κ : Nat), κ < k → words κ = words' κ) (base : Int) : bitNumbers words base k = bitNumbers words' base k

theorem Ratpoints.Sieve.bitNumbers_eq_nil {words : Nat → UInt64} {k : Nat} (h : ∀ (κ : Nat), κ < k → words κ = 0) (base : Int) : bitNumbers words base k = []

theorem Ratpoints.Sieve.bitNumbers_eq_filter {words : Nat → UInt64} {base : Int} {p : Int → Bool} {k : Nat} (h : ∀ (κ : Nat), κ < k → ∀ (t : Nat), (words κ).toBitVec.getLsbD t = (decide (t < 64) && p (base + 64 * ↑κ + ↑t))) : bitNumbers words base k = List.filter p (List.map (fun (j : Nat) => base + ↑j) (List.range (64 * k)))

The bit numbers of the set bits of the words are the numbers base, …, base + 64 k - 1 that pass p, when bit t of word κ is t < 64 and p (base + 64 κ + t).