The tables and the sieve entries

The tables from which the sieve makes its rows, each in its place in the C function find_points_work_1: the table of a prime with the exit when the curve has no points modulo it, on the coefficients reduced by the helper mod of the C code for longs or by the Euclidean % for GMP integers, by Horner's rule with Barrett's reduction on a fixed schedule, handing back the coefficients reduced modulo the prime (Ratpoints.Sieve.examinePrime?, Ratpoints.Sieve.modLong, Ratpoints.Sieve.hornerBarrett), the tables of a prime power (Ratpoints.Sieve.examinePower), and the sieve entry of a modulus, a prime, a prime power or a product of them, by its factors and with the reciprocal of the modulus and what the packing of the numerators needs (Ratpoints.Sieve.SieveEntry), with the admission test of the rows of a denominator (Ratpoints.Sieve.SieveEntry.admits), the kinds of the builders of the rows (Ratpoints.Sieve.RowInit) and the references to the entries that hold the tables of rows (Ratpoints.Sieve.EntryRef). The reciprocal of a modulus gives the remainder and the quotient by a multiplication on 64-bit words, with the high half of the 128-bit product from the products of the 32-bit halves (Ratpoints.Sieve.magic, Ratpoints.Sieve.mulHi, Ratpoints.Sieve.mulMod, Ratpoints.Sieve.mulDiv), and the remainder of a long of either sign (Ratpoints.Sieve.modMul). The table of a prime without the exit (Ratpoints.Sieve.examinePrime) is the reference of the table with it, which gives the same table for 0 < p < Ratpoints.maxPrimeEven whenever it gives one (Ratpoints.Sieve.examinePrime?_spec). The tables that the build of ratpoints generates are computed here: the squares and the inverses by Ratpoints.Sieve.squaresMod and Ratpoints.Sieve.inversesMod, and the table sieve_init of the builders of the rows of the primes by Ratpoints.Sieve.sieveInit; the row of 0 of a prime, Ratpoints.Sieve.sieves0, and the builders of the rows are in Ratpoints.Model.Rows, and the admission tests here are their reference. The loop of the tables (Ratpoints.tablesLoop, Ratpoints.examineInLoop), the sieve entries of the primes and of the composite moduli (Ratpoints.primeEntry, Ratpoints.makeModulus) and the prime powers that the composite moduli are made of (Ratpoints.powerIndex) are in Ratpoints.Model.Choice; the sieve that reads the rows from the tables of rows of the run, and has the missing ones built (Ratpoints.Sieve.buildRows), is in Ratpoints.Model.Sieve.

Main definitions

• Ratpoints.Sieve.squaresMod, Ratpoints.Sieve.inversesMod: the squares and the inverses modulo p.
• Ratpoints.Sieve.examinePrime: the table of a prime, the reference of the table with the exit.
• Ratpoints.Sieve.modLong: the helper mod of the C code, the remainder of a long modulo a positive long.
• Ratpoints.Sieve.barrett, Ratpoints.Sieve.hornerBarrett: Barrett's reduction, and Horner's rule modulo a prime with it on a fixed schedule.
• Ratpoints.Sieve.examinePrime?: the table of a prime on the path through longs or GMP integers, with the coefficients reduced modulo the prime, the code of examine_prime and the density of the prime, or none when the curve has no points modulo the prime.
• Ratpoints.Sieve.modinv, Ratpoints.Sieve.bitAt, Ratpoints.Sieve.setBitAt, Ratpoints.Sieve.Power, Ratpoints.Sieve.setSquareBits, Ratpoints.Sieve.unitInverses, Ratpoints.Sieve.powerDensity, Ratpoints.Sieve.setRevBits, Ratpoints.Sieve.Power.useful, Ratpoints.Sieve.examinePower: the inverse modulo m by the extended Euclidean algorithm, a bit of a bit array of words read and set, and the tables of a prime power, with the bit array of the squares, the inverses of the units, its density and whether it says more than nothing.
• Ratpoints.Sieve.magic, Ratpoints.Sieve.mulHi, Ratpoints.Sieve.mulMod, Ratpoints.Sieve.mulDiv, Ratpoints.Sieve.modMul: the reciprocal of a modulus, the high half of the product of two 64-bit words, the remainder and the quotient by a multiplication with the reciprocal, and the remainder of a long of either sign.
• Ratpoints.Sieve.Entry.admits, Ratpoints.Sieve.Power.admits, Ratpoints.Sieve.Factor, Ratpoints.Sieve.Factor.modulus, Ratpoints.Sieve.SieveEntry, Ratpoints.Sieve.SieveEntry.admits, Ratpoints.Sieve.survives: the admission tests of the rows of a denominator for a prime, for a prime power, and for a modulus by its factors, with the modulus of a factor.
• Ratpoints.Sieve.RowInit, Ratpoints.Sieve.sieveInit, Ratpoints.Sieve.EntryRef: the kinds of the builders of the rows, that of a prime of the table, and the references to the entries that hold the tables of rows.
• Ratpoints.Sieve.Factor.ref, Ratpoints.Sieve.Factor.init, Ratpoints.Sieve.SieveEntry.refInit: the reference and the kind of the builder of the entry of a factor, and of the sieve entry of a modulus at its position.

The tables of a prime

def Ratpoints.Sieve.squaresMod (p : Nat) : Array Bool

The squares modulo p, as a table of Booleans indexed by the residues: zero and the squares of the odd residues i < p, as the generator of the tables of ratpoints marks them; for odd p, the squares of i and of p - i agree, so these are all the squares.

C: find_points.c:37, gen_find_points_h.c:69-88

Deviation: a function of p, computed when it is called, for the row of p in the table squares that the build generates and that find_points.c includes.

Equations

• Ratpoints.Sieve.squaresMod p = List.foldl (fun (w : Array Bool) (i : Nat) => w.set! (i * i % p) true) ((Array.replicate p false).set! 0 true) (List.range' 1 (p / 2) 2)

def Ratpoints.Sieve.inversesMod (p : Nat) : Array Nat

The inverses modulo p, as a table indexed by the residues: 0 for 0, and for every other residue b the least i ≥ 1 with i b ≡ 1 (mod p), found by trial.

C: find_points.c:37, gen_find_points_h.c:33-44, gen_find_points_h.c:90-100

Deviation: a function of p, computed when it is called, for the row of p in the table inverses that the build generates and that find_points.c includes; the trial stops before p and gives 0 when it finds nothing, where inv_mod_p would not stop, which never happens for a prime p and a residue other than 0.

Equations

• Ratpoints.Sieve.inversesMod p = Array.map (fun (b : Nat) => (List.find? (fun (x : Nat) => x * b % p == 1) (List.range' 1 (p - 1))).getD 0) (Array.range p)

def Ratpoints.Sieve.evalMod (cs : List Nat) (p x : Nat) : Nat

Horner's rule modulo p: the value modulo p at x of the polynomial with the coefficient list cs, constant term first, reduced at every step.

Equations

• Ratpoints.Sieve.evalMod cs p x = List.foldr (fun (a v : Nat) => (a + x * v) % p) 0 cs

structure Ratpoints.Sieve.Entry : Type

What the sieve keeps of a prime p: p, the table of p + 1 entries, entry x < p whether f(x) is a square modulo p and entry p whether there are points at infinity modulo p, and the inverses modulo p.

C: rp-private.h:542-555

Deviation: only the fields that the rows of a prime read; the rows of the residues, which ratpoints keeps in the field sieve, that of 0 from the build and the others made by init when a denominator first needs them, are kept in the table of rows of the prime in the store of the run (Ratpoints.Sieve.EntryRef.prime, Ratpoints.Sieve.primeRows), from which the run reads them and into which it builds them (Ratpoints.Sieve.setRows, Ratpoints.Sieve.buildRows); the fields init, magic, nf, factor and pw are those of the sieve entry Ratpoints.Sieve.SieveEntry, of which the prime is the single factor, and so are bias, rbainv, dinv and the density r.

• p : Nat

  The prime.

• isFSquare : Array Bool

  For each residue x modulo p, whether f(x) is a square modulo p; and at p, whether there are points at infinity modulo p.

• inverses : Array Nat

  The inverses modulo p of the residues.

@[instance_reducible]

instance Ratpoints.Sieve.instInhabitedEntry : Inhabited Entry

Equations

• Ratpoints.Sieve.instInhabitedEntry = { default := Ratpoints.Sieve.instInhabitedEntry.default }

def Ratpoints.Sieve.examinePrime (c : List Int) (d p : Nat) : Entry

The table of the prime p for the polynomial f of degree d with the coefficient list c: for each residue x modulo p, whether f(x) is a square modulo p, with f(x) by Horner's rule modulo p (Ratpoints.Sieve.evalMod) on the coefficients reduced modulo p by the Euclidean %, and the squares of Ratpoints.Sieve.squaresMod, and as entry p whether there are points at infinity modulo p, for odd d or c_d a square modulo p; kept with p and the inverses modulo p (Ratpoints.Sieve.inversesMod). It is the reference of the table of a prime with the exit, Ratpoints.Sieve.examinePrime?, which models examine_prime and gives this table, on both of its paths, for 0 < p < Ratpoints.maxPrimeEven whenever it gives one (Ratpoints.Sieve.examinePrime?_spec); the lemmas on the table and its rows are stated for it.

Equations

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

def Ratpoints.Sieve.modLong (a b : Int) : Int

The helper mod of the C code, the remainder of the long a modulo the long b > 0: for a < -16 b, by C's division, which truncates (Int.tmod), with b added to a negative remainder; for a ≥ 16 b, by C's division; and otherwise by adding 16 b to a negative a, then subtracting 8 b, 4 b, 2 b and b where it can. For every integer a and every b ≥ 0 it is the Euclidean % (Ratpoints.Sieve.modLong_eq_emod). Its copy in find_points.c reduces, among others, the coefficients in examine_prime and examine_power (Ratpoints.Sieve.examinePrime?, Ratpoints.Sieve.examinePower) and a denominator above Ratpoints.mulModLimit in fill_bp_list (Ratpoints.Sieve.fillBpList), and its copy in sift.c the row indices of the first two stages of the sieve where they cannot be reduced by a multiplication with the reciprocal (Ratpoints.Sieve.andRows, Ratpoints.Sieve.chunkStarts, Ratpoints.Sieve.secondStage, Ratpoints.Sieve.secondStageWord).

C: find_points.c:477-492, sift.c:370-389

Deviation: one definition for the two copies of the function, in find_points.c and in sift.c, which are the same but for the hooks of the counts of the reductions in sift.c (RP_MOD_TICK, RP_MOD_DIV), empty unless RP_MOD_COUNTS is set; integers for the longs, with the obligations that the values it computes stay in the range of a long stated as lemmas: for 0 ≤ b < 2 ^ 59, 16 b (Ratpoints.fitsLong_sixteen_mul), its negation (Ratpoints.fitsLong_neg), and a + 16 b for -16 b ≤ a < 0 (Ratpoints.fitsLong_add_sixteen_mul), its other values lying between -b and 16 b; Int.tmod for C's division of longs, which truncates; the multiples 16 b, 8 b, 4 b and 2 b as products, for the shifts of b1.

Equations

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

def Ratpoints.Sieve.barrett (u p m : Nat) : Nat

The remainder of u modulo p ≥ 1 by Barrett's reduction with the reciprocal m: the quotient ⌊u m / 2 ^ 64⌋ times p subtracted from u, and p once more when the difference is still at least p. For m = ⌊(2 ^ 64 - 1) / p⌋ and u < 2 ^ 64 the quotient is ⌊u / p⌋ or one less, so that the result is u % p.

C: find_points.c:1639-1650

Deviation: natural numbers for the unsigned longs, the product u m exact as the 128-bit product of the C code, and the difference exact, which does not wrap since the quotient times p is at most u for m ≤ (2 ^ 64 - 1) / p; the obligation that u is below 2 ^ 64, which the C type gives, a hypothesis of the lemma that the result is u % p (Ratpoints.Sieve.barrett_eq); the form with the 128-bit product, which the modelled builds compile (the compiler defines __SIZEOF_INT128__, and RP_NO_INT128 is not set), for the division u % p of the other builds, which gives the same remainder.

Equations

• Ratpoints.Sieve.barrett u p m = if p ≤ u - u * m / 2 ^ 64 * p then u - u * m / 2 ^ 64 * p - p else u - u * m / 2 ^ 64 * p

def Ratpoints.Sieve.hornerBarrett (cm : Array Nat) (d p recip a : Nat) : Id Nat

The value modulo the prime p at the residue a of the polynomial of degree d whose coefficients reduced modulo p are cm, constant term first, as examine_prime computes it by Horner's rule: from cm[d], the steps s ↦ s a + cm[n] for n = d - 1, …, 0, and Barrett's reduction with the reciprocal recip (Ratpoints.Sieve.barrett) at the end, for d ≤ Ratpoints.hornerSteps; for larger d also after every Ratpoints.hornerSteps steps. For p < Ratpoints.maxPrimeEven, a < p, the entries of cm below p and recip = ⌊(2 ^ 64 - 1) / p⌋, the accumulator stays below 2 ^ 64, and the value is that of Horner's rule reduced at every step (Ratpoints.Sieve.evalMod).

C: find_points.c:1724, find_points.c:1726-1731, find_points.c:1735, find_points.c:1737-1744

Deviation: the choice between the two branches made for each residue, where examine_prime makes it once, around its loop over the residues; natural numbers for the unsigned long accumulator, with the obligation that it stays below 2 ^ 64 stated as a lemma (Ratpoints.Sieve.HornerInvariant.lt_two_pow_64); the steps counted up from 0 to d - 1, for the index n that counts down.

Equations

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

def Ratpoints.Sieve.examinePrime? (c : List Int) (d p : Nat) (useCLong : Bool) : Id (Option (Entry × Array Nat × Nat × Float))

The table of the prime p for the polynomial f of degree d with the coefficient list c, as examine_prime makes it, with the flag useCLong of the longs (Ratpoints.Setup.useCLong), and the coefficients reduced modulo p, which it hands back: the coefficients reduced on the path that the flag chooses, by the helper mod of the C code (Ratpoints.Sieve.modLong) for longs and by the Euclidean % for GMP integers (mpz_fdiv_r_ui), two paths with the same result (Ratpoints.Sieve.examinePrime?_eq_examinePrime?_false); entry 0 of the table, whether c_0 is a square modulo p (Ratpoints.Sieve.squaresMod); then, in the loop over the residues a = 1, …, p - 1, whether f(a) is a square modulo p, by Horner's rule with Barrett's reduction on its fixed schedule (Ratpoints.Sieve.hornerBarrett, with the reciprocal ⌊(2 ^ 64 - 1) / p⌋); entry p, whether there are points at infinity modulo p, for odd d or c_d a square modulo p; and none when the curve has no points modulo p, no entry of the table being true, where examine_prime returns -1 and the search ends with no points. Otherwise the entry with p, the table and the inverses modulo p (Ratpoints.Sieve.inversesMod), that of the reference Ratpoints.Sieve.examinePrime for 0 < p < Ratpoints.maxPrimeEven (Ratpoints.Sieve.examinePrime?_spec), with the array of the d + 1 coefficients reduced modulo p, the code of examine_prime and the density of the prime: the code 0 when f(x) is a square modulo p for every residue, np = p in the count np of the residues with a square value, and there are no points at infinity modulo p, so that the prime says nothing; else the density r, (np + 1)(p - 1) / p ^ 2 with points at infinity modulo p and np / p without, in doubles, and the code 2 for np = p, when the prime says only that numerator and denominator are coprime, and 1 otherwise. A curve without points modulo a prime has no points (Ratpoints.Sieve.not_isPoint_of_run_examinePrime?_eq_none).

C: find_points.c:1683-1697, find_points.c:1703-1723, find_points.c:1725, find_points.c:1732-1734, find_points.c:1736, find_points.c:1745-1749, find_points.c:1761-1781, find_points.c:1795-1819, find_points.c:1822-1826

Deviation: the prime p itself, for its index pn in the table prime; the table a fresh array of p + 1 entries, for the integers that examine_prime takes from the buffer int_next and hands back through is_f_square_p, and the coefficients a fresh array returned with the entry, for the array coeffs_mod_p of its caller, which it fills; one loop over the residues, for the two loops of the two branches of the schedule of Horner's rule, between which Ratpoints.Sieve.hornerBarrett chooses for each residue; the exit -1 as none, and the codes 0, 1 and 2 returned with the entry, the coefficients and the density, as natural numbers, the entry made and returned for the code 0 too, where examine_prime makes none, and the density 0.0 for that code, which examine_prime does not compute; the fields p, mask and nf of the record prec_entry of the ranking, which examine_prime sets with the density (lines 1782-1785), made by the caller from the table, the position of the prime and the code (Ratpoints.ModulusCandidate.ofPrime); the entry is a fresh value, for the space that examine_prime takes from the buffer of the sieve entries (se_next), and returned, where examine_prime stores it in the field ssp of prec_entry; it keeps only p, the table and the inverses (Ratpoints.Sieve.Entry), and no rows: the table of rows of the prime, with the row of 0 from the build and the others absent (lines 1820-1821, Ratpoints.Sieve.primeRows), is made in the store of the run by the loop of the tables when the prime says something (Ratpoints.examineInLoop), and for a prime that the third stage takes into the pool by the end of the choice (Ratpoints.choiceEnd, with Ratpoints.Sieve.SieveEntry.addTables); the fields init, nf and pw that examine_prime sets (lines 1800 and 1817) and its reciprocal magic (line 1808) are those of the sieve entry of the prime (Ratpoints.Sieve.SieveEntry), of which the prime is the single factor, made by the entries that the choice of the moduli makes (Ratpoints.primeEntry), which set the reciprocal there, and so are the bias bias, the inverse rbainv of Ratpoints.rbaLength, the density and the count of factors (lines 1811 and 1815-1817), which they set there with the formulas of these lines.

Equations

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

The tables of a prime power

def Ratpoints.Sieve.modinv (x m : Nat) : Id Nat

The inverse of x modulo m for x prime to m, by the extended Euclidean algorithm: from r₀ = m, r₁ = x mod m and the cofactors s₀ = 0, s₁ = 1, which keep rᵢ ≡ sᵢ x (mod m), while r₁ ≠ 0, with q = ⌊r₀ / r₁⌋, (r₀, r₁) becomes (r₁, r₀ - q r₁) and (s₀, s₁) becomes (s₁, s₀ - q s₁); then s₀, plus m if it is negative.

C: find_points.c:2241-2252

Deviation: natural numbers for x, m and the remainders, which are never negative for x ≥ 0, so that the correction of a negative x % m has no counterpart; integers for the long cofactors, which stay between -m and m (Ratpoints.Sieve.ModinvInvariant.natAbs_add_mul_le); the result a natural number.

Equations

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

def Ratpoints.Sieve.bitAt (ws : Array UInt64) (x : Nat) : Bool

Bit x of the bit array ws of 64-bit words, bit x mod 64 of word ⌊x / 64⌋, as the C code reads the bit arrays of the tables of a prime power and the local bit array of the squares of examine_power (RP_SQ_M), (ws[x >> LONG_SHIFT] >> (x & LONG_MASK)) & 1, with the division and the remainder by 64 for the shift and the mask.

Equations

• Ratpoints.Sieve.bitAt ws x = (ws[x / 64]! >>> (x % 64).toUInt64 &&& 1 != 0)

def Ratpoints.Sieve.setBitAt (ws : Array UInt64) (x : Nat) : Array UInt64

The bit array ws of 64-bit words with bit x set, as the C code sets a bit of the bit arrays of the tables of a prime power, of the local bit array of the squares of examine_power and of the pattern of a row, ws[x >> LONG_SHIFT] |= 1UL << (x & LONG_MASK), with the division and the remainder by 64 for the shift and the mask.

Equations

• Ratpoints.Sieve.setBitAt ws x = ws.set! (x / 64) (ws[x / 64]! ||| 1 <<< (x % 64).toUInt64)

structure Ratpoints.Sieve.Power : Type

What the sieve keeps of a prime power m = p ^ e for the polynomial f of degree d: p, e and m; the bit array fsq of Ratpoints.modWords words, its bit x < m (Ratpoints.Sieve.bitAt) set when f(x) is a square modulo m; the bit array gsq of modWords words, its bit t < m set when p ∣ t and frev(t) is a square modulo m, for the reversed polynomial frev(t) = ∑ₖ cₖ t ^ (D - k) of the even degree D = d + d % 2; and the inverses modulo m of the units, 0 for the other residues; and the density r of the prime power (Ratpoints.Sieve.powerDensity).

C: rp-private.h:531-534

Deviation: an array of m natural numbers for the unsigned short inverses, for an array sized by RATPOINTS_MAX_PRIME_EVEN; no count np, which examine_power stores (find_points.c:2304) and nothing reads.

• p : Nat

  The prime.

• e : Nat

  The exponent.

• m : Nat

  The modulus p ^ e.

• fsq : Array UInt64

  The bit array of Ratpoints.modWords words whose bit x < m is set when f(x) is a square modulo m.

• gsq : Array UInt64

  The bit array of Ratpoints.modWords words whose bit t < m is set when p ∣ t and frev(t) is a square modulo m.

• inv : Array Nat

  The inverses modulo m of the units, 0 for the other residues.

• r : Float

  The density: the mean over the classes of the denominator modulo m of the share of the numerators that its row admits (Ratpoints.Sieve.powerDensity).

@[instance_reducible]

instance Ratpoints.Sieve.instInhabitedPower : Inhabited Power

Equations

• Ratpoints.Sieve.instInhabitedPower = { default := Ratpoints.Sieve.instInhabitedPower.default }

def Ratpoints.Sieve.setSquareBits (m : Nat) (sq : Array UInt64) : Id (Array UInt64)

The bit array sq of 64-bit words with the bits of the squares x ^ 2 mod m of the residues x < m set (Ratpoints.Sieve.setBitAt), in examine_power.

C: find_points.c:2283-2284

Deviation: the bit array passed and returned, for the local array sq of examine_power; natural numbers for the longs, the squares x x with x < m staying below m ^ 2, with the obligation stated as a lemma (Ratpoints.mul_self_lt_two_pow_63_of_lt_maxPrimeEven).

Equations

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

def Ratpoints.Sieve.unitInverses (p m : Nat) : Id (Array Nat)

The inverses modulo the prime power m = p ^ e of the residues below m, as examine_power makes them: 0 for the residue 0, and then, in the loop over the residues x = 1, …, m - 1, the inverse of a unit by the extended Euclidean algorithm (Ratpoints.Sieve.modinv) and 0 for the other residues.

C: find_points.c:2302-2303

Deviation: the inverses a fresh array, returned, for the array inv of the entry pw that examine_power fills; natural numbers for the longs and for the unsigned short inverses, which are below m, with the obligation stated as a lemma (Ratpoints.Sieve.getElem!_inv_run_examinePower_lt_two_pow_16).

Equations

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

def Ratpoints.Sieve.powerDensity (p e m np : Nat) (gsq : Array UInt64) (pinf : Bool) : Id Float

The density of the prime power m = p ^ e, from the count np of the residues x with f(x) a square modulo m, the bit array gsq of the multiples t of p with frev(t) a square modulo m (Ratpoints.Sieve.Power), and whether denominators divisible by p occur at all (pinf, the entry at infinity of the table of p), as examine_power computes it in doubles: with u = m - m / p the number of the units, first u np / m; with pinf, for each valuation v from 1 to e the count good of the residues t of the valuation v (all multiples of p ^ e for v = e, and those whose quotient by p ^ v is prime to p for v < e) with bit t of gsq set, good u / m added, and the sum divided by m; without pinf, u np / m divided by u.

C: find_points.c:2306-2329

Deviation: the density returned, for the field r of the record pw that examine_power sets; natural numbers for the longs; the residues t stepped through by a while loop.

Equations

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

def Ratpoints.Sieve.setRevBits (cmD : List Nat) (m p : Nat) (sq gsq : Array UInt64) : Id (Array UInt64)

The bit array gsq with the bits of the multiples t = 0, p, 2 p, … of p below m set at which frev(t), by Horner's rule modulo m on the reversed coefficients cmD.reverse (Ratpoints.Sieve.evalMod), is a square modulo m, read from the bit array sq of the squares (Ratpoints.Sieve.bitAt, Ratpoints.Sieve.setBitAt), as examine_power sets them.

C: find_points.c:2294-2300

Deviation: the bit array passed and returned, for the array of the entry pw; the variable t for the multiples of p, where the C code reuses x; a while loop for the loop for with the step p; natural numbers for the longs and unsigned longs.

Equations

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

def Ratpoints.Sieve.Power.useful (pw : Power) : Bool

Whether the prime power pw says more than nothing, the code that examine_power returns: its density below 1 - 10 ^ -9.

C: find_points.c:2330

Deviation: a Boolean read from the density of the record, for the code 1 or 0 that examine_power returns.

Equations

• pw.useful = decide (pw.r < 1.0 - 10e-10)

def Ratpoints.Sieve.examinePower (c : List Int) (d p e : Nat) (useCLong pinf : Bool) : Id Power

The tables of the prime power m = p ^ e for the polynomial f of degree d with the coefficient list c, as examine_power makes them, with the flag useCLong of the longs (Ratpoints.Setup.useCLong): the coefficients c_0, …, c_d reduced modulo m on the path that the flag chooses, by the helper mod of the C code (Ratpoints.Sieve.modLong) for longs and by the Euclidean % for GMP integers (mpz_fdiv_ui), with c_D = 0 for odd d and D = d + 1; the bit arrays sq, fsq and gsq of Ratpoints.modWords words cleared in one loop; the bit array sq of the squares x ^ 2 mod m of the residues x, set bit by bit (Ratpoints.Sieve.setSquareBits) and read by Ratpoints.Sieve.bitAt; in the loop over the residues x, bit x of fsq set (Ratpoints.Sieve.setBitAt) when f(x) is a square modulo m, by Horner's rule reduced at every step (Ratpoints.Sieve.evalMod); in the loop over the multiples t = 0, p, 2 p, … of p below m, bit t of gsq set when frev(t) = ∑ₖ cₖ t ^ (D - k) is a square modulo m, by Horner's rule on the reversed coefficients (Ratpoints.Sieve.setRevBits); the inverses modulo m of the units, 0 for the other residues (Ratpoints.Sieve.unitInverses); and the density of the prime power from the count of the residues x with f(x) a square modulo m and the switch pinf (Ratpoints.Sieve.powerDensity), whether denominators divisible by p occur.

C: find_points.c:2267-2282, find_points.c:2285-2293, find_points.c:2301, find_points.c:2331

Deviation: the tables returned as a fresh value, for the entry pw of the buffer of the prime powers that examine_power fills; m as p ^ e, for the product of e factors p; the bit arrays sq, fsq and gsq fresh arrays of Ratpoints.modWords words, which the loop at line 2282 clears, for the local array that the function leaves unset and the arrays of the entry pw; natural numbers for the longs and unsigned longs, the variable t for the multiples of p, where the C code reuses x, and the steps v x + c of Horner's rule, with v, x and c below m, staying below m ^ 2, with the obligation stated as a lemma (Ratpoints.mul_add_lt_two_pow_64_of_lt_maxPrimeEven); the code that examine_power returns read from the density by Ratpoints.Sieve.Power.useful.

Equations

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

The reductions by a reciprocal

def Ratpoints.Sieve.magic (p : Nat) : Nat

The reciprocal ⌊(2 ^ 64 - 1) / p⌋ + 1 of the modulus p ≥ 2, which is 2 ^ 64 / p rounded up: with it, the remainder (Ratpoints.Sieve.mulMod) and the quotient (Ratpoints.Sieve.mulDiv) by p of every u with u p < 2 ^ 64 are computed by multiplications. The C code computes it as ULONG_MAX/p + 1 where it sets a field magic: in the sieve entries of the moduli, which examine_prime, make_power and make_modulus make (lines 1808, 2422 and 2454 of find_points.c; here Ratpoints.primeEntry and Ratpoints.makeModulus), in the tables of the Jacobi test (line 700; here Ratpoints.Sieve.jacobiSetup), and in the entries of the forbidden divisors tested with words (lines 2648, 2668 and 2738; here Ratpoints.Sieve.ForbiddenEntry.magic), with which the C code reduces the word number of the first word of a block (Ratpoints.Sieve.forbStarts). For p = 1, which is no modulus, it is 2 ^ 64, where ULONG_MAX / 1 + 1 wraps to 0 in the C code; the reductions, which read it as a 64-bit word, read 0 too.

Equations

• Ratpoints.Sieve.magic p = (2 ^ 64 - 1) / p + 1

def Ratpoints.Sieve.mulHi (a b : UInt64) : UInt64

The high 64 bits of the 128-bit product of the 64-bit words a and b, ⌊a b / 2 ^ 64⌋, from the four products of their 32-bit halves: the high half of the low product and the low halves of the two middle products make mid, whose high half is the carry into the high half of the result, the high product plus the high halves of the middle products and the carry; no product and no partial sum leaves the range of a 64-bit word. It is the shift by 64 bits of the 128-bit product of RP_MULMOD (Ratpoints.Sieve.mulMod) and of RP_MULDIV (Ratpoints.Sieve.mulDiv).

C: rp-private.h:404-408, rp-private.h:409-410

Deviation: the high half of the product from the products of the 32-bit halves, for the product of type __uint128_t that gcc provides and Lean core does not.

Equations

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

def Ratpoints.Sieve.mulMod (u p m : Nat) : Nat

The remainder of u modulo p by a multiplication with the reciprocal m, RP_MULMOD: the low 64 bits of m u, times p, shifted right by 64 bits, on 64-bit words (Ratpoints.Sieve.mulHi). For the reciprocal m = Ratpoints.Sieve.magic p of a modulus p ≥ 1 it is u % p whenever u p < 2 ^ 64, which the C code ensures by reducing only values below 2 ^ 32 modulo moduli below 2 ^ 32.

C: rp-private.h:404-408, rp-private.h:411, rp-private.h:413-414, rp-private.h:417

Deviation: natural numbers for the unsigned long reciprocal, the longs u and p, and the long result, which is below p; the arguments converted to UInt64, as the macro converts u and p to unsigned longs, so that the product m u wraps as the product of unsigned longs does; the argument u a natural number, for the long that the C code passes non-negative; the high half of the 128-bit product by Ratpoints.Sieve.mulHi; the form with the 128-bit product, which the modelled builds compile (the compiler defines __SIZEOF_INT128__, and neither RP_MULMOD_DIVIDE nor RP_NO_INT128 is set), for the division u % p of the other builds, which gives the same remainder where the multiplication is exact.

Equations

• Ratpoints.Sieve.mulMod u p m = (Ratpoints.Sieve.mulHi (m.toUInt64 * u.toUInt64) p.toUInt64).toNat

def Ratpoints.Sieve.mulDiv (u m : Nat) : Nat

The quotient of u by p by a multiplication with the reciprocal m, RP_MULDIV: the high 64 bits of u m, on 64-bit words (Ratpoints.Sieve.mulHi). For the reciprocal m = Ratpoints.Sieve.magic p of a modulus p ≥ 2 it is u / p whenever u p < 2 ^ 64.

C: rp-private.h:409-410, rp-private.h:415-416

Deviation: natural numbers for the unsigned long reciprocal, the long u and the long result, the arguments converted to UInt64, as the macro converts u to an unsigned long; the high half of the 128-bit product by Ratpoints.Sieve.mulHi; no argument p, which that form does not read; the form with the 128-bit product, which the modelled builds compile, for the division u / p of the other builds, which gives the same quotient where the multiplication is exact.

Equations

• Ratpoints.Sieve.mulDiv u m = (Ratpoints.Sieve.mulHi u.toUInt64 m.toUInt64).toNat

def Ratpoints.Sieve.modMul (a : Int) (p m : Nat) : Int

The remainder of a modulo p by a multiplication with the reciprocal m, mod_mul of sift.c: the remainder r of |a| by Ratpoints.Sieve.mulMod, and p - r for a negative a with r ≠ 0. For the reciprocal m = Ratpoints.Sieve.magic p of a modulus p ≥ 1 it is the Euclidean a % p whenever |a| p < 2 ^ 64, which the C code ensures by reducing only |a| ≤ RP_MULMOD_LIMIT modulo moduli below 2 ^ 32: the first stage of the sieve reduces its first row index so when the word numbers of the piece allow it (Ratpoints.Sieve.andRows, Ratpoints.Sieve.chunkStarts, the test small of Ratpoints.Sieve.siftPiece).

C: sift.c:243-247

Deviation: integers for the longs a and the result, and natural numbers for the long p and the unsigned long reciprocal m; |a| a natural number, for the long that RP_MULMOD converts to an unsigned long.

Equations

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

The admission tests of the rows of a denominator

def Ratpoints.Sieve.Entry.admits (e : Entry) (b : Nat) (a : Int) : Bool

Whether the row of the denominator b in the table e of the prime p admits the numerator a: for the residues r = b mod p and x = a mod p, the entry of the table at x r⁻¹ mod p if r ≠ 0, and whether x ≠ 0 if r = 0. It is the reference of the rows of a prime: ratpoints builds the row of a residue r ≠ 0 once, when a denominator first needs it, as a bit pattern of p bits repeated through words, by a function for each prime that the build generates (Ratpoints.Sieve.sieveInit1, Ratpoints.Sieve.sieveInit2), and takes the row of 0 from the pattern sieves0 that the build generates (Ratpoints.Sieve.sieves0), whose bit N is clear exactly when p divides N.

Equations

• e.admits b a = if b % e.p = 0 then (a % ↑e.p).toNat != 0 else e.isFSquare[(a % ↑e.p).toNat * e.inverses[b % e.p]! % e.p]!

def Ratpoints.Sieve.Power.admits (pw : Power) (b : Nat) (a : Int) : Bool

Whether the row of the denominator b for the prime power pw of the modulus m = p ^ e admits the numerator a: for the residues r = b mod m and x = a mod m, the bit of fsq at x r⁻¹ mod m if p ∤ r, and for p ∣ r whether p ∤ x and the bit of gsq at r x⁻¹ mod m (Ratpoints.Sieve.bitAt). It is the reference of the rows of a prime power: _ratpoints_sieve_init_power builds the pattern of the row of a residue once, when a denominator first needs it, stepping through the residues x r⁻¹ by additions of r⁻¹ for a unit r, and lays it out in words (Ratpoints.Sieve.sieveInitPower).

Equations

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

inductive Ratpoints.Sieve.Factor : Type

A factor of a modulus of the sieve: a prime with its table (Ratpoints.Sieve.Entry) or a prime power with its tables (Ratpoints.Sieve.Power), as the sieve entry of a product points to the entries of its factors, which are those of primes and prime powers (Ratpoints.Sieve.SieveEntry).

• prime (e : Entry) : Factor

  A prime with its table.

• power (pw : Power) : Factor

  A prime power with its tables.

@[instance_reducible]

instance Ratpoints.Sieve.instInhabitedFactor : Inhabited Factor

Equations

• Ratpoints.Sieve.instInhabitedFactor = { default := Ratpoints.Sieve.instInhabitedFactor.default }

def Ratpoints.Sieve.Factor.admits : Factor → Nat → Int → Bool

f.admits b a: whether the row of the denominator b for the factor f admits the numerator a: the row of the prime (Ratpoints.Sieve.Entry.admits) or of the prime power (Ratpoints.Sieve.Power.admits).

Equations

• (Ratpoints.Sieve.Factor.prime e).admits x✝¹ x✝ = e.admits x✝¹ x✝
• (Ratpoints.Sieve.Factor.power pw).admits x✝¹ x✝ = pw.admits x✝¹ x✝

def Ratpoints.Sieve.Factor.modulus : Factor → Nat

The modulus of a factor of a sieve entry, the field p of the entry of the factor that the C code reads in _ratpoints_sieve_init_product: the prime of a prime, the prime power m of a prime power.

Equations

• (Ratpoints.Sieve.Factor.prime t).modulus = t.p
• (Ratpoints.Sieve.Factor.power pw).modulus = pw.m

inductive Ratpoints.Sieve.RowInit : Type

The builder of the rows of a sieve entry, init, by its kind: the function that the build generates for a prime below 64 from CODE_INIT_SIEVE1 (Ratpoints.Sieve.sieveInit1) and for a prime above 64 from CODE_INIT_SIEVE2 (Ratpoints.Sieve.sieveInit2), the builder of the rows of a prime power (Ratpoints.Sieve.sieveInitPower), and that of the rows of a product (Ratpoints.Sieve.sieveInitProduct).

C: rp-private.h:497-498

Deviation: the kind of the builder, for the pointer to the function of the type ratpoints_init_fun, which for a prime points to the function that the build generates for it; the call through the pointer a match on the kind (Ratpoints.Sieve.SieveEntry.initRow, Ratpoints.Sieve.initFactorRow).

• sieve1 : RowInit

  The function of a prime below 64, from CODE_INIT_SIEVE1.

• sieve2 : RowInit

  The function of a prime above 64, from CODE_INIT_SIEVE2.

• power : RowInit

  The builder of the rows of a prime power, _ratpoints_sieve_init_power.

• product : RowInit

  The builder of the rows of a product, _ratpoints_sieve_init_product.

@[instance_reducible]

instance Ratpoints.Sieve.instDecidableEqRowInit : DecidableEq RowInit

Equations

• Ratpoints.Sieve.instDecidableEqRowInit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ratpoints.Sieve.instReprRowInit.repr : RowInit → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Ratpoints.Sieve.instReprRowInit : Repr RowInit

Equations

• Ratpoints.Sieve.instReprRowInit = { reprPrec := Ratpoints.Sieve.instReprRowInit.repr }

@[instance_reducible]

instance Ratpoints.Sieve.instInhabitedRowInit : Inhabited RowInit

Equations

• Ratpoints.Sieve.instInhabitedRowInit = { default := Ratpoints.Sieve.instInhabitedRowInit.default }

def Ratpoints.Sieve.sieveInit (p : Nat) : RowInit

The kind of the builder of the rows of the prime p of the table, the entry of p in the table sieve_init that the build generates: the function from CODE_INIT_SIEVE1 for p < 64, and that from CODE_INIT_SIEVE2 otherwise.

C: find_points.c:133, gen_init_sieve_h.c:48-62, init.c:246

Deviation: a function of p, for the entry of p in the table of the pointers to the functions that the build generates, one for each prime, and that init.c includes; the kind of the function, for the pointer to it.

Equations

• Ratpoints.Sieve.sieveInit p = if p < 64 then Ratpoints.Sieve.RowInit.sieve1 else Ratpoints.Sieve.RowInit.sieve2

inductive Ratpoints.Sieve.EntryRef : Type

A reference to the entry that holds a table of rows (Ratpoints.Sieve.RowStore), for a pointer to a sieve entry of ratpoints, whose array sieve holds the rows of the residues: a prime p by itself, for the entry prime_se[pn] of the prime p = prime[pn] that examine_prime makes; a prime power p ^ e by its prime and its exponent, for the entry power_se[idx] that make_power makes once, when a modulus first needs it, and that the prime power as a modulus and as a factor of products shares, whose index idx add_moduli keeps in pw_idx[pn][e] (lines 2352-2354 and 2387-2393 of find_points.c); and a product by the position n of its modulus among the moduli of the parameters, for the entry of its own that make_modulus makes.

• prime (p : Nat) : EntryRef

  The entry of the prime p.

• power (p e : Nat) : EntryRef

  The entry of the prime power p ^ e.

• product (n : Nat) : EntryRef

  The entry of the product that is the modulus at the position n of the parameters.

def Ratpoints.Sieve.instDecidableEqEntryRef.decEq (x✝ x✝¹ : EntryRef) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.Sieve.instDecidableEqEntryRef.decEq (Ratpoints.Sieve.EntryRef.prime a) (Ratpoints.Sieve.EntryRef.prime b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Ratpoints.Sieve.instDecidableEqEntryRef.decEq (Ratpoints.Sieve.EntryRef.prime p) (Ratpoints.Sieve.EntryRef.power p_1 e) = isFalse ⋯
• Ratpoints.Sieve.instDecidableEqEntryRef.decEq (Ratpoints.Sieve.EntryRef.prime p) (Ratpoints.Sieve.EntryRef.product n) = isFalse ⋯
• Ratpoints.Sieve.instDecidableEqEntryRef.decEq (Ratpoints.Sieve.EntryRef.power p e) (Ratpoints.Sieve.EntryRef.prime p_1) = isFalse ⋯
• Ratpoints.Sieve.instDecidableEqEntryRef.decEq (Ratpoints.Sieve.EntryRef.power p e) (Ratpoints.Sieve.EntryRef.product n) = isFalse ⋯
• Ratpoints.Sieve.instDecidableEqEntryRef.decEq (Ratpoints.Sieve.EntryRef.product n) (Ratpoints.Sieve.EntryRef.prime p) = isFalse ⋯
• Ratpoints.Sieve.instDecidableEqEntryRef.decEq (Ratpoints.Sieve.EntryRef.product n) (Ratpoints.Sieve.EntryRef.power p e) = isFalse ⋯
• Ratpoints.Sieve.instDecidableEqEntryRef.decEq (Ratpoints.Sieve.EntryRef.product a) (Ratpoints.Sieve.EntryRef.product b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Ratpoints.Sieve.instDecidableEqEntryRef : DecidableEq EntryRef

Equations

• Ratpoints.Sieve.instDecidableEqEntryRef = Ratpoints.Sieve.instDecidableEqEntryRef.decEq

def Ratpoints.Sieve.instHashableEntryRef.hash : EntryRef → UInt64

Equations

• Ratpoints.Sieve.instHashableEntryRef.hash (Ratpoints.Sieve.EntryRef.prime a) = mixHash 0 (hash a)
• Ratpoints.Sieve.instHashableEntryRef.hash (Ratpoints.Sieve.EntryRef.power a a_1) = mixHash (mixHash 1 (hash a)) (hash a_1)
• Ratpoints.Sieve.instHashableEntryRef.hash (Ratpoints.Sieve.EntryRef.product a) = mixHash 2 (hash a)

@[instance_reducible]

instance Ratpoints.Sieve.instHashableEntryRef : Hashable EntryRef

Equations

• Ratpoints.Sieve.instHashableEntryRef = { hash := Ratpoints.Sieve.instHashableEntryRef.hash }

@[instance_reducible]

instance Ratpoints.Sieve.instReprEntryRef : Repr EntryRef

Equations

• Ratpoints.Sieve.instReprEntryRef = { reprPrec := Ratpoints.Sieve.instReprEntryRef.repr }

def Ratpoints.Sieve.instReprEntryRef.repr : EntryRef → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Ratpoints.Sieve.instInhabitedEntryRef : Inhabited EntryRef

Equations

• Ratpoints.Sieve.instInhabitedEntryRef = { default := Ratpoints.Sieve.instInhabitedEntryRef.default }

def Ratpoints.Sieve.Factor.ref : Factor → EntryRef

The reference to the entry of a factor (Ratpoints.Sieve.EntryRef), the entry to which the field factor of the sieve entry of a product points: that of the prime, prime_se[pn], by the prime, or that of the prime power p ^ e, power_se[idx] with the index idx in pw_idx[pn][e], by its prime and its exponent.

Equations

• (Ratpoints.Sieve.Factor.prime t).ref = Ratpoints.Sieve.EntryRef.prime t.p
• (Ratpoints.Sieve.Factor.power pw).ref = Ratpoints.Sieve.EntryRef.power pw.p pw.e

def Ratpoints.Sieve.Factor.init : Factor → RowInit

The kind of the builder of the rows of the entry of a factor (Ratpoints.Sieve.RowInit), the field init of that entry: for a prime the function that the build generates for it (Ratpoints.Sieve.sieveInit), which examine_prime sets (line 1800 of find_points.c), and for a prime power the builder of the rows of a prime power, which make_power sets (line 2420).

Equations

• (Ratpoints.Sieve.Factor.prime t).init = Ratpoints.Sieve.sieveInit t.p
• (Ratpoints.Sieve.Factor.power pw).init = Ratpoints.Sieve.RowInit.power

structure Ratpoints.Sieve.SieveEntry : Type

The sieve entry of a modulus p of the sieve, a prime, a prime power or a product of primes and prime powers, given by its factors (Ratpoints.Sieve.Factor): one for a prime or a prime power, two or more for a product; with the reciprocal of p (Ratpoints.Sieve.magic), which the third stage of the sieve copies for its primes (Ratpoints.Sieve.checkOf) and with which the first two stages reduce their row indices (Ratpoints.Sieve.andRows, Ratpoints.Sieve.chunkStarts, Ratpoints.Sieve.secondStage); and with what the packing of the numerators needs: the bias, the least multiple of p that is at least Ratpoints.rowBias, which the row offsets carry (Ratpoints.Sieve.classOffsets), the inverse of Ratpoints.rbaLength modulo p, from which the row offsets are computed, and the inverses of the strides 2 ^ k modulo p for the strides in use, with which fill_bp_list divides the denominator by the stride (Ratpoints.Sieve.fillBpList). Its row for a denominator is the and of the rows of its factors (Ratpoints.Sieve.SieveEntry.admits).

C: rp-private.h:542-555

Deviation: the kinds of modulus as the list of the factors: one prime factor for a prime, whose entry has nf = 0 and the tables is_f_square and inverses of its own; one prime-power factor for a prime power, whose entry has nf = 1 and its tables pw; and two or more for a product, whose entry has nf ≥ 2 and points to the entries factor of its factors; no bound RP_MAX_FACTORS on the number of factors, which the choice of the moduli keeps when it offers a composite modulus (Ratpoints.takeFactor); the rows of the residues, which ratpoints keeps in the array sieve of the entry, kept in the store of the run (Ratpoints.Sieve.RowStore) in the table of rows of the reference ref; the reference ref to the entry whose table of rows holds its rows (Ratpoints.Sieve.EntryRef), for the pointer to the entry: a prime or a prime power that of its one factor, so that the modulus and the products with it as a factor read one table of rows, as they read one entry in the C code, and a product its own; the kind of its builder init (Ratpoints.Sieve.RowInit), for the pointer to the function; a natural number for the unsigned long reciprocal magic, and natural numbers for the longs bias and rbainv; the inverses dinv an array, for the array of RP_NUM_STRIDES longs, which the row offsets of the packing fill (Ratpoints.Sieve.classOffsets) with an entry for each stride up to the largest in use, where the entries of the C code beyond it stay unset and unread; the density r, which the correction of the moduli during the run reads (Ratpoints.Sieve.adaptPrimes), a Float for the double, and the count nf of the factors, an integer for the long, 0 for a prime, 1 for a prime power and the number of factors for a product, kept with the list of the factors.

• p : Nat

  The modulus.

• factors : List Factor

  The factors: one for a prime or a prime power, two or more for a product.

• magic : Nat

  The reciprocal of the modulus (Ratpoints.Sieve.magic).

• bias : Nat

  The bias of the row offsets: the least multiple of the modulus that is at least Ratpoints.rowBias.

• rbainv : Nat

  The inverse of Ratpoints.rbaLength modulo the modulus.

• dinv : Array Nat

  Entry k the inverse of 2 ^ k modulo the modulus, for the strides 2 ^ k in use; empty until the row offsets of the packing fill it (Ratpoints.Sieve.classOffsets).

• ref : EntryRef

  The reference to the entry whose table of rows holds the rows (Ratpoints.Sieve.EntryRef): that of the one factor of a prime or a prime power, and the product's own.

• init : RowInit

  The kind of the builder of the rows (Ratpoints.Sieve.RowInit).

• r : Float

  The density of the modulus.

• nf : Int

  The count of the factors: 0 for a prime, 1 for a prime power, else the number of factors.

@[instance_reducible]

instance Ratpoints.Sieve.instInhabitedSieveEntry : Inhabited SieveEntry

Equations

• Ratpoints.Sieve.instInhabitedSieveEntry = { default := Ratpoints.Sieve.instInhabitedSieveEntry.default }

def Ratpoints.Sieve.SieveEntry.refInit (n : Nat) : List Factor → EntryRef × RowInit

The reference to the entry that holds the rows of a modulus with the factors fs, at the position n among the moduli of the parameters, and the kind of its builder: for a prime or a prime power, those of the entry of its one factor (Ratpoints.Sieve.Factor.ref, Ratpoints.Sieve.Factor.init), whose entry the modulus shares, as sieve_list[n] is prime_se[pn] or power_se[idx] in the C code; for a product, its own entry with the builder of the rows of a product.

Equations

• Ratpoints.Sieve.SieveEntry.refInit n [f] = (f.ref, f.init)
• Ratpoints.Sieve.SieveEntry.refInit n x✝ = (Ratpoints.Sieve.EntryRef.product n, Ratpoints.Sieve.RowInit.product)

def Ratpoints.Sieve.SieveEntry.admits (e : SieveEntry) (b : Nat) (a : Int) : Bool

Whether the row of the denominator b in the sieve entry e of the modulus p admits the numerator a: for the residues r = b mod p and x = a mod p, the row of r of every factor admits x (Ratpoints.Sieve.Factor.admits), each factor reading r and x modulo its own modulus, which divides p. It is the reference of the rows of a modulus: _ratpoints_sieve_init_product builds the row of a product once, when a denominator first needs it, as the and of the rows of its factors for r modulo the modulus of the factor, laid down in blocks of the length of the factor (Ratpoints.Sieve.sieveInitProduct); and a prime or a prime power has the row of its one factor, the entry of the prime or the prime power being the factor's own.

Equations

• e.admits b a = e.factors.all fun (x : Ratpoints.Sieve.Factor) => x.admits (b % e.p) (a % ↑e.p)

def Ratpoints.Sieve.survives (entries : List SieveEntry) (b : Nat) (a : Int) : Bool

Whether the numerator a survives the sieve entries entries for the denominator b: the row of b in every entry admits a (Ratpoints.Sieve.SieveEntry.admits). This test, a function of the numerator, is the interface between the sieve and the check.

Equations

• Ratpoints.Sieve.survives entries b a = entries.all fun (x : Ratpoints.Sieve.SieveEntry) => x.admits b a

Examples