The sieving parameters

The free choices of the sieve: which moduli it uses, in which order and in which stage, at most how many forbidden divisors of the denominators it tests, whether it runs the Jacobi test, and at most how many bit arrays it treats at a time. ratpoints chooses the moduli and their stages from the curve and corrects the choice during the run, and takes the other choices from its options or its defaults (the program passes the array size Ratpoints.defaultArraySize); none of this changes the points found or their order, since a modulus only removes candidates that are not points, the pieces of the numerators follow one another in increasing order, a test on the denominators removes only denominators without points, and the two shapes of the loop over the denominators between which these choices decide, the words of 64 denominators and every denominator, both run in increasing order. The model makes the choice inside the search, as find_points does, and the theorems hold for every value of the options of the sieve, whatever moduli the search chooses.

The parameters are the result of the choice of the moduli from the curve (Ratpoints.sievingInfo), from the options of the sieve that the caller gives (Ratpoints.SieveOptions) as the search normalizes them (Ratpoints.SieveOptions.normalize), with the end of the third stage, the number of primes looked at in all and the estimates of the run that the correction of the moduli reads; the moduli come to the sieve as their sieve entries (Ratpoints.SievingInfo.entries). The sieve reads the cut points of its stages and the array size, and the tests on the denominators read the bound on the forbidden divisors and the switch of the Jacobi test.

Main definitions

• Ratpoints.Params: the sieving parameters, the result of the choice of the moduli.
• Ratpoints.arraySizeAt, Ratpoints.Params.arraySizeAt: at most how many bit arrays a piece of the numerators has, for a height bound.
• Ratpoints.SieveOptions: the values of the options of the program that tune the sieve.
• Ratpoints.SieveOptions.normalize: those values as the search normalizes them.

structure Ratpoints.Params : Type

The sieving parameters: the free choices of the sieve, internal to the search, as the choice of the moduli gives them to the run (Ratpoints.sievingInfo): the cut points of the stages of the moduli, the first sp1 of them, then those up to sp2, then those up to sp3, the rest being the reserve from which the correction of the moduli may take further primes; how many primes were looked at in all; at most how many forbidden divisors are tested, whether the Jacobi test may run, at most how many bit arrays a piece of the numerators has; and the estimates of the run, the cost of one exact check and the number of words at which the first correction of the moduli is made. The run of the search reads the cut points of the stages and the array size, and the correction of the moduli between its blocks the estimates of the run, the cost of a check and the words of the first correction; the moduli come to the run as their sieve entries (Ratpoints.SievingInfo).

C: ratpoints.h:368, ratpoints.h:395-397, ratpoints.h:406

Deviation: the parameters as a structure of their own, for the fields of the arguments that find_points_work normalizes and sieving_info sets (sp1, sp2, sp3, max_forbidden, array_size, run_words, run_denoms, adapt_at, check_rel; sp3_max as the length of Ratpoints.SievingInfo.entries) and the local pn_lim of sieving_info at the end (lookedAt); the Jacobi switch a Boolean (Ratpoints.Params.jacobi), true when the bit RATPOINTS_NO_JACOBI of the flags is clear, for that bit of args->flags, which main.c clears with the others; a natural number for the long field array_size (Ratpoints.Params.arraySize), 0 for the default, which the library takes for every value ≤ 0 (Ratpoints.Params.arraySizeAt); Floats for the doubles and a UInt64 for the unsigned long.

• lookedAt : Nat

  How many primes were looked at in all, the third stage included.

• sp1 : Nat

  The end of the first stage, a position in the sieve entries of the choice (Ratpoints.SievingInfo.entries).

• sp2 : Nat

  The end of the second stage, a position in the sieve entries of the choice (Ratpoints.SievingInfo.entries).

• sp3 : Nat

  The end of the third stage, a position in the sieve entries of the choice (Ratpoints.SievingInfo.entries); the reserve is the rest.

• maxForbidden : Nat

  At most how many forbidden divisors of the denominators are tested.

• jacobi : Bool

  Whether the Jacobi test on the denominators may run: it runs when also the polynomial searched, after the reversal check, has even degree and a leading coefficient that is not a square.

• arraySize : Nat

  At most how many bit arrays a piece of the numerators has, the field array_size of the arguments of the library; 0 for Ratpoints.defaultArraySize.

• runWords : Float

  The estimate of the number of words that the run sweeps, run_words.

• runDenoms : Float

  The estimate of the number of denominators that the run sifts, run_denoms.

• checkRel : Float

  The cost of one exact check relative to Ratpoints.checkReference, check_rel.

• adaptAt : UInt64

  The number of words at which the first correction of the moduli is made, adapt_at, or 2 ^ 64 - 1 when the search may not correct its choice.

def Ratpoints.arraySizeAt (a H : Nat) : Nat

At most how many bit arrays a piece of the numerators has for the field a of the array size, 0 for Ratpoints.defaultArraySize, and the height bound H: a, or Ratpoints.defaultArraySize for 0, capped at 2 ⌈H / 64⌉ and at Ratpoints.maxArraySize, then rounded up to a multiple of Ratpoints.chunk, which stays at most the cap Ratpoints.maxArraySize, a multiple of the chunk; at least 1 for H ≥ 1 (Ratpoints.one_le_arraySizeAt).

C: rp-private.h:87, find_points.c:4666-4677

Deviation: a Nat for the long field, so that only 0 stands for the default, which the library takes for every value ≤ 0; 64 for LONG_LENGTH; and the macro CEIL of a natural number x by d as (x + d - 1) / d, which is its value for every x ≥ 0.

Equations

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

def Ratpoints.Params.arraySizeAt (P : Params) (H : Nat) : Nat

At most how many bit arrays a piece of the numerators has for the height bound H, by the field arraySize of the parameters P (Ratpoints.arraySizeAt); at least 1 for H ≥ 1 (Ratpoints.Params.one_le_arraySizeAt). It models no C code of its own.

Equations

• P.arraySizeAt H = Ratpoints.arraySizeAt P.arraySize H

structure Ratpoints.SieveOptions : Type

The values of the options of ratpoints that tune the sieve, as the program reads them into the fields of its ratpoints_args (Ratpoints.SieveOptions.store): -p, -n, -N, -R, -A, -P and -F give C longs, which are -1, as in main.c, when the option is absent; -r, -U, -C, -Q and -W give doubles, -1.0 when absent; -j switches the Jacobi test off and -J on again; and the array size is Ratpoints.defaultArraySize, which the program sets.

C: main.c:337-347, main.c:349-350, main.c:352, ratpoints.h:365-367

Deviation: integers for the longs of the fields, doubles by their bits (Ratpoints.Double) for the doubles, as the program reads doubles (Ratpoints.Cli.scanDouble?), and a Boolean for the bit RATPOINTS_NO_JACOBI of the flags, which main.c clears with the others; the bit of the reversal is in Ratpoints.Options.

• numPrimes : Int

  The value of -p: how many primes are looked at (examined).

• sp1 : Int

  The value of -n: the end of the first stage, negative to choose it from the curve.

• sp2 : Int

  The value of -N: the end of the second stage, negative to choose it from the curve.

• survivorsPerWord : Double

  The value of -r: the target of the rule that ends the first stage, survivors_per_word; values not > 0, that is ≤ 0 or NaN, for Ratpoints.survivorsPerWord.

• sp2Extra : Int

  The value of -R: how many moduli the second stage adds in a long run, sp2_extra; negative for Ratpoints.sp2Extra.

• sp2U0 : Double

  The value of -U: the run length at which a modulus of the second stage pays for itself, sp2_u0; values not ≥ 0, that is negative or NaN, for Ratpoints.sp2U0.

• costTable : Double

  The value of -C: what one row of a sieve table costs, cost_table; values not ≥ 0, that is negative or NaN, for Ratpoints.costTable.

• adapt : Int

  The value of -A: how much of the choice is corrected during the run, adapt: 0 none, 1 the third stage, 2 and more the second too, negative for 1.

• sp3Extra : Int

  The value of -P: how many primes the third stage adds, negative to choose it from the curve.

• sp3PerDenom : Double

  The value of -Q: what one prime of the third stage costs per denominator, sp3_per_denom; values not ≥ 0, that is negative or NaN, for Ratpoints.sp3PerDenom.

• checkCost : Double

  The value of -W: what one exact check costs, check_cost; values not > 0, that is ≤ 0 or NaN, to estimate it from the curve (Ratpoints.checkCost).

• arraySize : Int

  The array size, array_size: at most how many bit arrays a piece of the numerators has; values ≤ 0 for Ratpoints.defaultArraySize.

• maxForbidden : Int

  The value of -F: at most how many forbidden divisors are tested.

• jacobi : Bool

  Whether the Jacobi test runs: false when -j is the last of -j and -J.

def Ratpoints.SieveOptions.normalize (s : SieveOptions) : SieveOptions

The options s as find_points_work_1 normalizes the fields of the arguments that hold them: the number of the primes looked at Ratpoints.defaultNumPrimes for a negative one and at most Ratpoints.numPrimes; the end of the second stage at most that number, and that of the first at most that of the second when the second is given (≥ 0); at most Ratpoints.defaultMaxForbidden forbidden divisors for a negative bound and at most the size of the table. Whether the caller left the number of primes to the search (np_is_default) is read from s before this normalization. The search normalizes the options so (Ratpoints.findPointsWork) and makes the choice of the moduli with the normalized options (Ratpoints.sievingInfo).

C: find_points.c:4643-4649, find_points.c:4655-4656, find_points.c:4662-4665

Deviation: the normalized options returned, for the fields of the arguments that the C code normalizes in place and restores in find_points_work (lines 4542-4545 and 4560-4563); the array size normalized with the height bound where it is read (Ratpoints.arraySizeAt); no enlargement of the buffer of the rows (line 4654), which the model does not have; integers for the longs.

Equations

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

Examples