The 2-adic information

The words of the classes of the denominators modulo 64 (Ratpoints.Sieve.twoAdic) let the numerator of every point through, and the word of the classes that admit a numerator (Ratpoints.Sieve.denBits) has the bit of every class whose word is not 0. The mask of the squares modulo 64 is checked by decide; Horner's rule on words is exact modulo 2 ^ 64 and so modulo 64 (UInt64.natCast_toNat_foldr, UInt64.natCast_toNat_foldl), so that the word of f (Ratpoints.Sieve.fsq) has bit k set exactly when f(k) is a square modulo 64, and the word of the reversed polynomial (Ratpoints.Sieve.gsq) bit t for the even t at which it takes a square value; the loops of Ratpoints.Sieve.twoAdic scatter these bits into the words of the classes. A point (a, y, b) with odd b has a ≡ k b (mod 64) for a k with f(k) a square, since F(a, b) = b ^ D f(k) modulo 64, and one with even b an odd a and b ≡ t a (mod 64) for an even t at which the reversed polynomial takes a square value; so when no class admits a numerator, the curve has no points at all, not even at infinity (Ratpoints.Sieve.not_isPoint_of_denBits_eq_zero).

Main definitions

• Ratpoints.Sieve.TwoAdicBits: the bits of the words of the classes after the scatter of the set bits k < k0 of the word of f into the odd classes and of the set bits t < t0 of the word of the reversed polynomial into the even ones, the postcondition of Ratpoints.Sieve.twoAdic_spec for k0 = t0 = 64.

Main statements

• Ratpoints.Sieve.squares64_test_iff: the test of the mask Ratpoints.Sieve.squares64 is the test of the squares modulo 64.
• Ratpoints.Sieve.getLsbD_fsq_coeffsMod64, Ratpoints.Sieve.getLsbD_gsq_coeffsMod64: the bits of the words of f and of the reversed polynomial.
• Ratpoints.Sieve.twoAdic_spec: bit a of the word of the class b < 64 is set exactly when b is odd and a ≡ k b for a set bit k of the word of f, or a < 64 is odd and b ≡ t a for a set bit t of the word of the reversed polynomial; Ratpoints.Sieve.getLsbD_run_twoAdic states this as a plain statement.
• Ratpoints.Sieve.classBit_twoAdic_of_sq_eq: for a point (a, y, b), bit a mod 64 of the word of the class b mod 64 is set; Ratpoints.Sieve.getElem!_twoAdic_ne_zero: so the word of the class of the denominator of a point is not 0.
• Ratpoints.Sieve.getLsbD_denBits: bit j of Ratpoints.Sieve.denBits nb says whether nb[j] is not 0; Ratpoints.Sieve.snd_run_numClasses: the word den_bits of Ratpoints.Sieve.numClasses is Ratpoints.Sieve.denBits.
• Ratpoints.Sieve.not_isPoint_of_denBits_eq_zero: when no class of the denominators admits a numerator, the curve has no points, so that the 2-adic exit of the search is sound.

Implementation notes

The square values that a point gives in a commutative ring (Ratpoints.isSquare_sum_mul_pow_of_sq_eq_binaryForm, Ratpoints.isSquare_sum_mul_pow_sub_of_sq_eq_binaryForm) are stated in Ratpoints.Proof.Tables, where the square value modulo a prime follows from the first.

The squares modulo 64 and Horner's rule on words

theorem Ratpoints.Sieve.squares64_test_iff_of_lt {x : ℕ} (hx : x < 64) : (squares64 >>> UInt64.ofNat x &&& 1 != 0) = true ↔ IsSquare ↑x

theorem Ratpoints.Sieve.squares64_test_iff (s : UInt64) : (squares64 >>> (s &&& 63) &&& 1 != 0) = true ↔ IsSquare ↑s.toNat

The test of the mask of the squares modulo 64 (Ratpoints.Sieve.squares64) on the residue s mod 64 of a word, as Ratpoints.Sieve.fsq and Ratpoints.Sieve.gsq make it, is the test of the squares modulo 64, which decide checks for each residue.

theorem UInt64.natCast_toNat_foldr {n : ℕ} (hn : n ∣ 2 ^ 64) (l : List UInt64) (x : UInt64) : ↑(List.foldr (fun (a s : UInt64) => s * x + a) 0 l).toNat = ∑ i ∈ Finset.range l.length, ↑(l.getD i 0).toNat * ↑x.toNat ^ i

Horner's rule on words from the last entry of l down, as Ratpoints.Sieve.fsq evaluates f, read in ZMod n for n ∣ 2 ^ 64: the value of the polynomial with the coefficients l at x.

theorem UInt64.natCast_toNat_foldl {n : ℕ} (hn : n ∣ 2 ^ 64) (l : List UInt64) (x s : UInt64) : ↑(List.foldl (fun (s a : UInt64) => s * x + a) s l).toNat = ↑s.toNat * ↑x.toNat ^ l.length + ∑ i ∈ Finset.range l.length, ↑(l.getD i 0).toNat * ↑x.toNat ^ (l.length - 1 - i)

Horner's rule on words from the first entry of l on and from the value s, as Ratpoints.Sieve.gsq evaluates the reversed polynomial, read in ZMod n for n ∣ 2 ^ 64.

The words of f and of the reversed polynomial

theorem Ratpoints.Sieve.length_toList_coeffsMod64 (c : List ℤ) (d : ℕ) : (coeffsMod64 c d).toList.length = d + d % 2 + 1

theorem Ratpoints.Sieve.natCast_toNat_getD_coeffsMod64 (c : List ℤ) (d i : ℕ) : ↑((coeffsMod64 c d).toList.getD i 0).toNat = if i ≤ d then ↑(c.getD i 0) else 0

theorem Ratpoints.Sieve.sum_range_coeffsMod64 (c : List ℤ) (d : ℕ) (g : ℕ → ZMod 64) : ∑ i ∈ Finset.range (d + d % 2 + 1), ↑((coeffsMod64 c d).toList.getD i 0).toNat * g i = ∑ i ∈ Finset.range (d + 1), ↑(c.getD i 0) * g i

theorem Ratpoints.Sieve.getLsbD_fsq_coeffsMod64 (c : List ℤ) (d k : ℕ) : (fsq (coeffsMod64 c d)).toBitVec.getLsbD k = true ↔ k < 64 ∧ IsSquare (∑ i ∈ Finset.range (d + 1), ↑(c.getD i 0) * ↑k ^ i)

Bit k of the word of f (Ratpoints.Sieve.fsq) for the coefficients modulo 64 is set exactly when k < 64 and f(k) = ∑ cᵢ kⁱ is a square modulo 64.

theorem Ratpoints.Sieve.getLsbD_gsq_coeffsMod64 (c : List ℤ) (d t : ℕ) : (gsq (coeffsMod64 c d)).toBitVec.getLsbD t = true ↔ t < 64 ∧ t % 2 = 0 ∧ IsSquare (∑ i ∈ Finset.range (d + 1), ↑(c.getD i 0) * ↑t ^ (d + d % 2 - i))

Bit t of the word of the reversed polynomial (Ratpoints.Sieve.gsq) for the coefficients modulo 64 is set exactly when t < 64 is even and ∑ cᵢ t^(D - i) is a square modulo 64, for D = d + d % 2.

The scatter

def Ratpoints.Sieve.TwoAdicBits (f g : UInt64) (k0 t0 : ℕ) (nb : Vector UInt64 64) : Prop

The bits of the words nb of the classes after the scatter of the set bits k < k0 of f into the odd classes and of the set bits t < t0 of g into the even ones: bit a of the word of the class b < 64 is set exactly when b is odd and a = k b mod 64 for a set bit k < k0 of f, or a < 64 is odd and b = t a mod 64 for a set bit t < t0 of g.

Equations

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

def Ratpoints.Sieve.ScatterOddInvariant (nb0 : Vector UInt64 64) (k : ℕ) (pref : List ℕ) (nb : Vector UInt64 64) : Prop

The invariant of the loop of Ratpoints.Sieve.twoAdic that scatters the bit k of f into the odd classes, from the words nb0: after the classes 1, 3, … of the positions pref, the words are those of nb0 with bit k b mod 64 set in the word of each of these classes b.

Equations

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

def Ratpoints.Sieve.ScatterEvenInvariant (nb0 : Vector UInt64 64) (t : ℕ) (pref : List ℕ) (nb : Vector UInt64 64) : Prop

The invariant of the loop of Ratpoints.Sieve.twoAdic that scatters the bit t of g into the even classes, from the words nb0: after the numerators 1, 3, … of the positions pref, the words are those of nb0 with bit a set in the word of the class t a mod 64 of each of them.

Equations

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

theorem Ratpoints.Sieve.twoAdicBits_replicate_zero (f g : UInt64) : TwoAdicBits f g 0 0 (Vector.replicate 64 0)

theorem Ratpoints.Sieve.twoAdicBits_of_walkWhileInvariant_left {f g w : UInt64} {nb : Vector UInt64 64} (h : WalkWhileInvariant f (fun (k0 : ℕ) => TwoAdicBits f g k0 0) true (nb, w)) : TwoAdicBits f g 64 0 nb

At the exit of the loop over the set bits of f, all of them are scattered into the odd classes.

theorem Ratpoints.Sieve.twoAdicBits_of_walkWhileInvariant_right {f g w : UInt64} {nb : Vector UInt64 64} (h : WalkWhileInvariant g (TwoAdicBits f g 64) true (nb, w)) : TwoAdicBits f g 64 64 nb

At the exit of the loop over the set bits of g, all of them are scattered into the even classes.

theorem Ratpoints.Sieve.scatterOddInvariant_nil (nb : Vector UInt64 64) (k : ℕ) : ScatterOddInvariant nb k [] nb

theorem Ratpoints.Sieve.scatterEvenInvariant_nil (nb : Vector UInt64 64) (t : ℕ) : ScatterEvenInvariant nb t [] nb

theorem Ratpoints.Sieve.ScatterOddInvariant.set! {nb0 nb : Vector UInt64 64} {k : ℕ} {pref suff : List ℕ} {cur : ℕ} (hl : ForIn.toList [:32] = pref ++ cur :: suff) (h : ScatterOddInvariant nb0 k pref nb) : ScatterOddInvariant nb0 k (pref ++ [cur]) (nb.set! (2 * cur + 1) (nb[2 * cur + 1]! ||| 1 <<< UInt64.ofNat (k * (2 * cur + 1) % 64)))

theorem Ratpoints.Sieve.ScatterEvenInvariant.set! {nb0 nb : Vector UInt64 64} {t : ℕ} {pref suff : List ℕ} {cur : ℕ} (hl : ForIn.toList [:32] = pref ++ cur :: suff) (h : ScatterEvenInvariant nb0 t pref nb) : ScatterEvenInvariant nb0 t (pref ++ [cur]) (nb.set! (t * (2 * cur + 1) % 64) (nb[t * (2 * cur + 1) % 64]! ||| 1 <<< UInt64.ofNat (2 * cur + 1)))

theorem Ratpoints.Sieve.TwoAdicBits.of_scatterOddInvariant {f g w : UInt64} {nb0 nb : Vector UInt64 64} {k k0 : ℕ} (hw : (w != 0) = true) (hk : k = w.toBitVec.ctz.toNat) (hs : ScatterOddInvariant nb0 k (ForIn.toList [:32]) nb) (hcl : ClearedBelow f k0 w) (h : TwoAdicBits f g k0 0 nb0) : TwoAdicBits f g (w.toBitVec.ctz.toNat + 1) 0 nb

The scatter of the lowest set bit k of w into the odd classes, for a word w with the bits of f from k0 on: the bits of the set bits of f below k0 become those of its set bits up to k.

theorem Ratpoints.Sieve.TwoAdicBits.of_scatterEvenInvariant {f g w : UInt64} {nb0 nb : Vector UInt64 64} {t t0 : ℕ} (hw : (w != 0) = true) (ht : t = w.toBitVec.ctz.toNat) (hs : ScatterEvenInvariant nb0 t (ForIn.toList [:32]) nb) (hcl : ClearedBelow g t0 w) (h : TwoAdicBits f g 64 t0 nb0) : TwoAdicBits f g 64 (w.toBitVec.ctz.toNat + 1) nb

The scatter of the lowest set bit t of w into the even classes, for a word w with the bits of g from t0 on: the bits of the set bits of g below t0 become those of its set bits up to t.

theorem Ratpoints.Sieve.twoAdic_spec (c : List ℤ) (d : ℕ) : ⦃ True ⦄ twoAdic c d ⦃ fun (nb : Vector UInt64 64) => TwoAdicBits (fsq (coeffsMod64 c d)) (gsq (coeffsMod64 c d)) 64 64 nb ⦄

The loops over the set bits end, since clearing the lowest set bit makes a word other than 0 smaller.

theorem Ratpoints.Sieve.getLsbD_run_twoAdic (c : List ℤ) (d : ℕ) {b : ℕ} (hb : b < 64) (a : ℕ) : (twoAdic c d).run[b]!.toBitVec.getLsbD a = true ↔ (b % 2 = 1 ∧ ∃ k < 64, (fsq (coeffsMod64 c d)).toBitVec.getLsbD k = true ∧ k * b % 64 = a) ∨ a % 2 = 1 ∧ a < 64 ∧ ∃ t < 64, (gsq (coeffsMod64 c d)).toBitVec.getLsbD t = true ∧ t * a % 64 = b

Ratpoints.Sieve.twoAdic_spec as a plain statement, which the soundness of the classes uses without the program logic.

The classes of a point

theorem Ratpoints.Sieve.exists_getLsbD_fsq_of_sq_eq {c : List ℤ} {a y : ℤ} {b : ℕ} (hb : b % 2 = 1) (hy : y ^ 2 = binaryForm c a ↑b) : ∃ k < 64, (fsq (coeffsMod64 c (degree c))).toBitVec.getLsbD k = true ∧ k * (b % 64) % 64 = (a % 64).toNat

A point (a, y, b) with odd b has a ≡ k b (mod 64) for a set bit k of the word of f (Ratpoints.Sieve.fsq), since f(k) is a square modulo 64 (Ratpoints.isSquare_sum_mul_pow_of_sq_eq_binaryForm).

theorem Ratpoints.Sieve.exists_getLsbD_gsq_of_sq_eq {c : List ℤ} {a y : ℤ} {b : ℕ} (hb : b % 2 = 0) (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : (a % 64).toNat % 2 = 1 ∧ (a % 64).toNat < 64 ∧ ∃ t < 64, (gsq (coeffsMod64 c (degree c))).toBitVec.getLsbD t = true ∧ t * (a % 64).toNat % 64 = b % 64

A point (a, y, b) with even b has an odd a, since gcd(a, b) = 1, and b ≡ t a (mod 64) for a set bit t of the word of the reversed polynomial (Ratpoints.Sieve.gsq), since it takes a square value at t (Ratpoints.isSquare_sum_mul_pow_sub_of_sq_eq_binaryForm).

theorem Ratpoints.Sieve.classBit_twoAdic_of_sq_eq {c : List ℤ} {a y : ℤ} {b : ℕ} (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : classBit (twoAdic c (degree c)).run[b % 64]! a = true

The 2-adic information lets the numerator a of every point (a, y, b) through the word of the class b mod 64: a or b is odd, since gcd(a, b) = 1, and F(a, b) is a square, so a square modulo 64; neither b ≥ 1 nor a degree of a given parity is needed.

theorem Ratpoints.Sieve.getElem!_twoAdic_ne_zero {c : List ℤ} {b : ℕ} {xs : List ℤ} (h : BruteForce.pointsOfDen c (degree c) (↑b) xs ≠ []) : (twoAdic c (degree c)).run[b % 64]! ≠ 0

The word of the class of the denominator of a point is not 0 (Ratpoints.Sieve.classBit_twoAdic_of_sq_eq).

The classes that admit a numerator

theorem Ratpoints.Sieve.getLsbD_denBits (nb : Vector UInt64 64) (j : ℕ) : (denBits nb).toBitVec.getLsbD j = (decide (j < 64) && nb[j]! != 0)

theorem Ratpoints.Sieve.snd_run_numClasses (nb : Vector UInt64 64) : (numClasses nb).run.2 = denBits nb

The word den_bits that Ratpoints.Sieve.numClasses returns with the classes is Ratpoints.Sieve.denBits (Ratpoints.Sieve.numClasses_spec).

The 2-adic exit

theorem Ratpoints.Sieve.not_isPoint_of_denBits_eq_zero {c : List ℤ} (h : denBits (twoAdic c (degree c)).run = 0) (H : ℕ) (q : ℤ × ℤ × ℤ) : ¬IsPoint c H q

When no class of the denominators modulo 64 admits a numerator (Ratpoints.Sieve.denBits), the curve has no normalized point of any height, a point at infinity included: the word of the class of the denominator b of a point (a, y, b), b = 0 included, has bit a mod 64 set (Ratpoints.Sieve.classBit_twoAdic_of_sq_eq), so the class has its bit in Ratpoints.Sieve.denBits (Ratpoints.Sieve.getLsbD_denBits). So the 2-adic exit of the search needs no test of the points at infinity: no class admits a numerator only for even degree and c_d not a square modulo 64.