The set-up of a search

What ratpoints does with its input before the sieve, as far as the model has it: the refusals of a search, each with the error of the program (Ratpoints.Refusal); the reversal check of find_points_work_1, which refuses the binary form when the degree d of the polynomial is even and X ^ 2 divides the form (c₀ = c₁ = 0), and otherwise may reverse the polynomial, in three cases, exchanging x and z in the binary form (Ratpoints.Setup.reversal); and the test whether the coefficients are C longs (Ratpoints.fitsLong, Ratpoints.Setup.useCLong), which chooses the path of the table of a prime (Ratpoints.Sieve.examinePrime?). Ratpoints.findPointsWith, the search with a callback, of which Ratpoints.findPoints is an instance, runs the reversal check after the test of the leading zeros, with the switch of its normalized options, and the search that it runs on the polynomial handed on (Ratpoints.searchPoints) makes the test of the longs. For the tests on the denominators (Ratpoints.Sieve.denInfoTest, Ratpoints.Sieve.wordsTest), the C code computes the valuation of an integer at a prime, with its unit part, by repeated division (Ratpoints.Setup.valuation), and for a polynomial of odd degree whose leading coefficient is not ±1 it factors that coefficient over 2 and the odd primes of the table and lists its squarefree divisors up to the largest denominator, with the slopes of a valuation test (Ratpoints.Setup.setupUs1): the denominators of the points are such divisors times squares.

Main definitions

• Ratpoints.Refusal: the refusals of a search.
• Ratpoints.fitsLong: the C longs.
• Ratpoints.Setup.isSquare: the squares as GMP decides them.
• Ratpoints.Setup.reversal: the reversal check.
• Ratpoints.Setup.useCLong: whether the coefficients are longs.
• Ratpoints.Setup.valuation: the valuation of an integer at a prime, with its unit part.
• Ratpoints.Setup.factorLcf, Ratpoints.Setup.squarefreeDivisors, Ratpoints.Setup.slope: the factorization of the leading coefficient over the table, its squarefree divisors, and the slopes of the valuation test.
• Ratpoints.Setup.DenInfo, Ratpoints.Setup.setupUs1: for odd degree, the factorization of the leading coefficient and its squarefree divisors, which restrict the denominators.

inductive Ratpoints.Refusal : Type

The refusals of a search, each with the number of the error with which the program ratpoints refuses the input. The program itself refuses too many or too few coefficients, the height bound 0 and the heights that are not longs, before it calls the library; the library refuses a binary form that is not squarefree in the set-up of the search: when the leading zeros of n + 1 coefficients lower ⌈n / 2⌉, in the reversal check (Ratpoints.Setup.reversal) and with the remainder chain of the Sturm step (Ratpoints.Sturm.chain); and between the last two it refuses search intervals without l ≤ u, not increasing and strictly apart, or with a NaN end (Ratpoints.searchIntervals).

• tooManyCoefficients : Refusal

  More than Ratpoints.maxDegree + 1 coefficients: error 3.

• tooFewCoefficients : Refusal

  Fewer than two coefficients: error 5.

• incorrectHeight : Refusal

  The height bound 0, or one that is not a long (Ratpoints.fitsLong): error 4.

• notSquarefree : Refusal

  A binary form that is not squarefree: error 8.

• badArgs : Refusal

  Search intervals without l ≤ u, not increasing and strictly apart, or with a NaN end, which the library refuses with RATPOINTS_BAD_ARGS: error 9.

@[instance_reducible]

instance Ratpoints.instDecidableEqRefusal : DecidableEq Refusal

Equations

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

@[instance_reducible]

instance Ratpoints.instReprRefusal : Repr Refusal

Equations

• Ratpoints.instReprRefusal = { reprPrec := Ratpoints.instReprRefusal.repr }

def Ratpoints.instReprRefusal.repr : Refusal → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.instReprRefusal.repr Ratpoints.Refusal.badArgs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ratpoints.Refusal.badArgs")).group prec✝

def Ratpoints.fitsLong (a : Int) : Bool

Whether the integer a is a C long, -2 ^ 63 ≤ a < 2 ^ 63, as mpz_fits_slong_p of GMP decides it: ratpoints needs a long of 64 bits since version 3.0.0.

C: rp-private.h:41-43, rp-private.h:47

Deviation: the bounds of a long of 64 bits, fixed, where the C code does not compile unless an unsigned long has exactly 64 bits.

Equations

• Ratpoints.fitsLong a = (decide (-2 ^ 63 ≤ a) && decide (a < 2 ^ 63))

def Ratpoints.Setup.isSquare (a : Int) : Bool

Whether a is a square, as mpz_perfect_square_p of GMP decides it: 0 and the squares of the positive integers, so that no negative integer is a square.

Equations

• Ratpoints.Setup.isSquare a = (decide (0 ≤ a) && a.toNat.sqrt * a.toNat.sqrt == a.toNat)

def Ratpoints.Setup.reversal (allow : Bool) (c : List Int) (d : Nat) : Except Refusal (List Int × Nat × Bool)

The reversal check on the coefficients c of degree d, the leading zeros dropped, with the switch allow of the reversal: the list that the search goes on with, its degree, and whether it is reversed. If the switch is off, c itself. Otherwise, for even d with c₀ = 0, the refusal Ratpoints.Refusal.notSquarefree if also c₁ = 0, since X ^ 2 then divides the binary form, and else the list c_d, …, c₁, c₀ with the degree d - 1 (case 1); for even d with c_d a square and c₀ not (Ratpoints.Setup.isSquare), the list c_d, …, c₀ (case 2); for odd d with |c_d| ≠ 1, c₀ = 0 and |c₁| = 1, the list c₀, c_d, …, c₁ (case 3); and otherwise c itself. In each case the reversed list is the reflection of c in the even degree d + d % 2 of the binary form, so that its binary form is that of c with x and z exchanged (Ratpoints.Setup.binaryForm_eq_of_reversal_eq_ok).

C: find_points.c:4732-4739, find_points.c:4744-4756, find_points.c:4759-4770, find_points.c:4775-4790, find_points.c:4802-4803

Deviation: a new list for the reversal in place, and nothing written back to the caller: the reversed coefficients, the degree and the flag RATPOINTS_REVERSED are returned instead; the switch for the test of the flags RATPOINTS_NO_REVERSE and RATPOINTS_NO_REVERSE_AUTO, which is on when neither is set, as the normalized options give it (Ratpoints.Options.normalize: off for a search region or a range of the denominators); the square test of c_d made here, where the C code reads the flag lcfsq that the set-up computes before (line 4634), and no flag lcfsq for the reversed list, which case 2 clears, since Ratpoints.Sieve.pointsAtInfinity tests the leading coefficient of the list it is given; integers and their absolute values for the GMP integers, with no scratch integers work[0] and work[1]; the report under RATPOINTS_VERBOSE printed by the caller from the result (Ratpoints.Report.reversal).

Equations

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

def Ratpoints.Setup.useCLong (c : List Int) (d : Nat) : Bool

Whether the coefficients c₀, …, c_d are all C longs (Ratpoints.fitsLong): the flag use_c_long, with which the table of a prime reduces the coefficients on the path through longs, by the helper mod of the C code (Ratpoints.Sieve.modLong), and otherwise on the path through GMP integers (Ratpoints.Sieve.examinePrime?); on the first path the inputs of mod are longs (Ratpoints.Setup.fitsLong_getD_of_useCLong).

C: find_points.c:4599-4600, find_points.c:4814-4823

Deviation: no array c_long: the coefficients stay integers, which Ratpoints.Sieve.modLong reads as longs, as mpz_get_si gives them exactly when they fit; the flag is returned, for the int that the loop sets, and the loop, which stops at the first coefficient that is not a long, is List.all.

Equations

• Ratpoints.Setup.useCLong c d = (List.range (d + 1)).all fun (i : Nat) => Ratpoints.fitsLong (c.getD i 0)

def Ratpoints.Setup.valuation (n : Int) (p : Nat) : Id (Nat × Nat)

The valuation of the integer n at p and the unit part of n modulo p: for n ≠ 0, the pair (v, r) with p ^ v ∣ |n|, p ∤ |n| / p ^ v and r = (|n| / p ^ v) mod p, by repeated division with remainder; for n = 0, (Ratpoints.veryBig, 0). For p = 1 and n ≠ 0 the loop does not end, as in the C code.

C: find_points.c:424-454

Deviation: one function for valuation on GMP integers, with its scratch integer vvv, and valuation1 on longs, which gives v alone and is the first component; natural numbers for |n|, the quotients and the remainders; the pair returned, for the remainder that valuation stores through its pointer r.

Equations

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

structure Ratpoints.Setup.DenInfo : Type

What the valuation test of the divisor shape (Ratpoints.Sieve.denInfoTest) knows of a prime p of the leading coefficient c_d of a polynomial of odd degree d: p, its valuation val in c_d, and the slope, the least n ≥ 1 with (d - k) n > val - v_p(c_k) for every k < d, with v_p(0) = Ratpoints.veryBig. A denominator b with v_p(b) ≥ slope and v_p(b) + val odd carries no point (Ratpoints.Setup.DenInfo.excludes_eq_false_of_sq_eq).

C: find_points.c:155

Deviation: natural numbers for the int fields, which the primes fit, a cofactor below the square of a prime of the table among them (Ratpoints.Setup.mul_self_lt_of_mem_primeTable), and the valuations and the slopes for coefficients below 2 ^ (2 ^ 31 - 1).

• p : Nat

  The prime.

• val : Nat

  Its valuation in the leading coefficient.

• slope : Nat

  The slope.

@[instance_reducible]

instance Ratpoints.Setup.instDecidableEqDenInfo : DecidableEq DenInfo

Equations

• Ratpoints.Setup.instDecidableEqDenInfo = Ratpoints.Setup.instDecidableEqDenInfo.decEq

def Ratpoints.Setup.instDecidableEqDenInfo.decEq (x✝ x✝¹ : DenInfo) : Decidable (x✝ = x✝¹)

Equations

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

def Ratpoints.Setup.instReprDenInfo.repr : DenInfo → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Ratpoints.Setup.instReprDenInfo : Repr DenInfo

Equations

• Ratpoints.Setup.instReprDenInfo = { reprPrec := Ratpoints.Setup.instReprDenInfo.repr }

def Ratpoints.Setup.factorLcf (w : Nat) : Id (List (Nat × Nat) × Nat)

The factorization of w ≥ 1 over 2 and the odd primes of Ratpoints.primeTable, as setup_us1 makes it, with the cofactor that it leaves: the power of 2 is divided off; then for the odd primes p of the table in turn, while the cofactor is not 1, a cofactor below p ^ 2, which has no prime factor below p and so is a prime, is taken with the valuation 1 (when it is a long, which it always is) and leaves the cofactor 1, and otherwise p is divided off with its valuation when it divides. The factorization is complete exactly when the cofactor is 1: when the part of w prime to 2 · 3 ⋯ 1019 is below 1021 ^ 2 or a power of 1021.

C: find_points.c:777-860

Deviation: the valuations by Ratpoints.Setup.valuation, for mpz_scan1 at 2 and for the loop of divisions with remainder at the odd primes, the power then divided off at once; natural numbers for the GMP integers work[0] and work[1], the longs, and the int p with its square p * p (line 800), which is below 2 ^ 31 (Ratpoints.Setup.mul_self_lt_of_mem_primeTable); a list of pairs of natural numbers and the cofactor returned, for the int fields p and val of the entries of den_info (they hold the primes, the cofactor below p ^ 2 and, for coefficients below 2 ^ (2 ^ 31 - 1), the valuations: Ratpoints.Setup.DenInfo), for their count, the terminating zero and the integer work[0]; no output under DEBUG.

Equations

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

def Ratpoints.Setup.squarefreeDivisors (ps : List Nat) (bHigh : Nat) : Id (List Nat)

The squarefree divisors at most bHigh of a product of the distinct primes ps, as setup_us1 lists them: from [1], for each prime p in turn, each divisor x found so far with x ≤ ⌊bHigh / p⌋ gives x p, appended in the order of the x; the list stops as soon as it has Ratpoints.maxDivisors entries. So it lists the products at most bHigh of the subsets of the primes in the order of binary counting, the first prime the lowest bit, unless it stops.

C: find_points.c:864-880

Deviation: a list, for the array divisors and its pointers div, div0 and div1; natural numbers for the longs, the products x p being formed only for x ≤ ⌊bHigh / p⌋, so that they are at most bHigh and longs for a long bHigh (Ratpoints.Setup.fitsLong_mul_of_le_div).

Equations

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

def Ratpoints.Setup.slope (c : List Int) (d p val : Nat) : Id Nat

The slope of the valuation test of the divisor shape (Ratpoints.Sieve.denInfoTest) at the prime p with the valuation val in the leading coefficient c_d of the polynomial of odd degree d with the coefficient list c: the largest of 1 and the ⌈(1 + val - v_p(c_k)) / (d - k)⌉ for k = d - 1, …, 0, with the valuations of Ratpoints.Setup.valuation, by the macro CEIL, which rounds up for every sign: the least n ≥ 1 with (d - k) n > val - v_p(c_k) for every k < d, with v_p(0) = Ratpoints.veryBig, so that a zero coefficient imposes nothing when val ≤ Ratpoints.veryBig.

C: find_points.c:894-912, rp-private.h:87

Deviation: integers for the ints, and the slope as a natural number; no output under DEBUG.

Equations

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

def Ratpoints.Setup.setupUs1 (c : List Int) (d bHigh : Nat) : Id (Option (List DenInfo × List Nat))

For a polynomial of odd degree d with the coefficient list c and |c_d| ≠ 1, and the largest denominator bHigh: the primes of |c_d| with their valuations and slopes (Ratpoints.Setup.DenInfo, Ratpoints.Setup.slope) and the squarefree divisors of c_d at most bHigh (Ratpoints.Setup.squarefreeDivisors), or none when the factorization over 2 and the odd primes of the table is not complete (Ratpoints.Setup.factorLcf) or there are Ratpoints.maxDivisors divisors or more. The denominators of the points are then these divisors times squares, which the divisor shape of the loop over the denominators visits divisor by divisor (Ratpoints.Sieve.squares1Block).

C: find_points.c:766-776, find_points.c:863, find_points.c:881-893, find_points.c:914-935, ratpoints.h:390

Deviation: the leading coefficient read from the list, for the integer work[0] that the caller sets to |c_d| (lines 4911-4912); lists, for the arrays den_info and divisors of the arguments (ratpoints.h:390) with their terminating zeros; none for a factorization that is not complete or too many divisors, where setup_us1 leaves the flag RATPOINTS_USE_SQUARES1 clear, and the lists returned, where it sets the flag; no output under DEBUG.

Equations

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

Examples

What ratpoints 3.1.1 does at the pinned commit: with -v it says whether it reverses and in which case, and prints the coefficients of case 3; -k switches the reversal off; and ratpoints '0 0 1 1 1' 5 -q -s, without the Sturm step, which would refuse the form too, ends with error 8, which -s -k does not. The test of the longs is checked at the ends of their range. The valuation is checked at 2, 3 and 5 and at 0; the factorizations over the table with their cofactors, the squarefree divisors and the slopes against what the build of ratpoints with DEBUG prints with -v, a factorization that is not complete among them; and the boundary of Ratpoints.maxDivisors divisors (511 at the height 2066, 512 at 2067).