The denominators

The side of the denominators of the sieve, each component in its place in find_points_work_1: the 2-adic information, which says for each class of the denominators modulo 64 which numerators modulo 64 it admits (Ratpoints.Sieve.twoAdic), and which classes admit a numerator at all (Ratpoints.Sieve.denBits), from which the packings of the classes are made (Ratpoints.Sieve.numClasses, in Ratpoints.Model.Packing); the forbidden divisors of the denominators of a polynomial of even degree, primes tested with words of 64 denominators or by their valuations, that an examined prime gives from what its table hands back in the loop of the tables of sieving_info, which also takes the exit (Ratpoints.Sieve.forbiddenOfPrime, which the loop of the tables of the choice of the moduli, Ratpoints.examineInLoop, calls), and that the further primes give (Ratpoints.Sieve.forbidden); the Jacobi test, by the binary algorithm (Ratpoints.Sieve.jacobi) or by tables (Ratpoints.Sieve.jacobiSetup, Ratpoints.Sieve.jacobiTest); and the loop over the denominators in its four shapes, as run_setup chooses them (Ratpoints.Sieve.Shape, Ratpoints.Sieve.runSetup): the squares, the divisors of the leading coefficient times squares (Ratpoints.Setup.setupUs1), the words of 64 denominators, and every denominator, with the tests of the divisor shape and the word shape on a single denominator (Ratpoints.Sieve.denInfoTest, Ratpoints.Sieve.wordsTest); the run itself, in blocks, is in Ratpoints.Model.Blocks (Ratpoints.Sieve.sieveRun), with the residues of a denominator divided by the stride of its class in Ratpoints.Model.Packing (Ratpoints.Sieve.fillBpList). Every class word lets every numerator of a point through, and so does its packing; no forbidden divisor excludes the denominator of a point, the primes examined for them being primes of the table; both Jacobi tests let it through, and so does every test of a shape, so that the run delivers the points of the denominators of its shape in the search intervals (with the bounds that Ratpoints.Sieve.runSetup makes, Ratpoints.Sieve.exactBounds) to the callback of the search, in the order of its loop: increasing, except for the divisors; it returns when the callback stops the search.

Main definitions

• Ratpoints.Sieve.squares64: the squares modulo 64 as a word.
• Ratpoints.Sieve.coeffsMod64, Ratpoints.Sieve.fsq, Ratpoints.Sieve.gsq: the coefficients modulo 64 and the residues at which the polynomial and its reversal are squares modulo 64.
• Ratpoints.Sieve.twoAdic, Ratpoints.Sieve.denBits: the numerators modulo 64 that each class of the denominators admits, and the classes that admit one.
• Ratpoints.Sieve.ForbiddenEntry, Ratpoints.Sieve.ForbiddenVal: the forbidden divisors tested with words and by their valuations.
• Ratpoints.Sieve.unitParts, Ratpoints.Sieve.forbiddenAt, Ratpoints.Sieve.forbiddenValuations, Ratpoints.Sieve.allValuations: the valuations at a prime of the leading coefficient that no denominator of a point has, and those that a denominator can have at all.
• Ratpoints.Sieve.forbiddenOfPrime, Ratpoints.Sieve.forbidden: the forbidden divisor of an examined prime, and the forbidden divisors among the further primes.
• Ratpoints.Sieve.jacobi: the Jacobi test by the binary algorithm, with its helpers Ratpoints.Sieve.twoSign, Ratpoints.Sieve.jacobiReduce and Ratpoints.Sieve.jacobiRound.
• Ratpoints.Sieve.JacobiInfo, Ratpoints.Sieve.nonSquares, Ratpoints.Sieve.jacobiSigns, Ratpoints.Sieve.jacobiSetup, Ratpoints.Sieve.jacobiTest: the Jacobi test by tables.
• Ratpoints.Sieve.ceilSqrt, Ratpoints.Sieve.floorSqrt: the bounds of the square shapes.
• Ratpoints.Sieve.denInfoTest, Ratpoints.Sieve.wordsTest: the tests of the divisor shape and the word shape on a single denominator.
• Ratpoints.Sieve.Shape, Ratpoints.Sieve.runSetup: the shapes, and the choice of the shape and the bounds of the search intervals of the run.

The 2-adic information

def Ratpoints.Sieve.squares64 : UInt64

The squares modulo 64 as a word, RP_SQUARES64: bit s is set exactly when s is a square modulo 64, for the twelve residues 0, 1, 4, 9, 16, 17, 25, 33, 36, 41, 49, 57.

C: find_points.c:981

Equations

• Ratpoints.Sieve.squares64 = 144680414395695635

def Ratpoints.Sieve.coeffsMod64 (c : List Int) (d : Nat) : Array UInt64

The coefficients modulo 64 of the polynomial of degree d with the coefficient list c, as the binary form of the even degree D = d + d % 2 reads them: the non-negative residue of c_k for k ≤ d, and 0 for k = D = d + 1 when d is odd.

C: find_points.c:1002-1004

Deviation: an array of D + 1 words, for the array cm on the stack; the Euclidean % of the integers, for mpz_fdiv_ui.

Equations

• Ratpoints.Sieve.coeffsMod64 c d = Array.map (fun (k : Nat) => if k ≤ d then (c.getD k 0 % 64).toNat.toUInt64 else 0) (Array.range (d + d % 2 + 1))

def Ratpoints.Sieve.fsq (cm : Array UInt64) : UInt64

The residues k modulo 64 at which the polynomial f with the coefficients cm modulo 64 (Ratpoints.Sieve.coeffsMod64) is a square modulo 64, as a word: bit k is set when f(k) mod 64 is a square modulo 64 (Ratpoints.Sieve.squares64), with f(k) by Horner's rule in the arithmetic of UInt64, which is exact modulo 2 ^ 64 and so modulo 64.

C: find_points.c:1006-1014

Deviation: Horner's rule from 0, where the C code starts from cm[D], with the same value.

Equations

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

def Ratpoints.Sieve.gsq (cm : Array UInt64) : UInt64

The even residues t modulo 64 at which the reversed polynomial frev(t) = c₀ t^D + c₁ t^(D - 1) + ⋯ + c_D with the coefficients cm modulo 64 (Ratpoints.Sieve.coeffsMod64) is a square modulo 64, as a word: bit t, for even t, is set when frev(t) mod 64 is a square modulo 64 (Ratpoints.Sieve.squares64), by Horner's rule in the arithmetic of UInt64; the bits of the odd t are clear.

C: find_points.c:1015-1021

Deviation: Horner's rule from 0, where the C code starts from cm[0], with the same value.

Equations

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

def Ratpoints.Sieve.twoAdic (c : List Int) (d : Nat) : Id (Vector UInt64 64)

The 2-adic information of the polynomial of degree d with the coefficient list c: for each residue b modulo 64 the word nb[b] of the numerators modulo 64 that the denominators ≡ b admit, bit a set exactly when a or b is odd and F(a, b) mod 64 is a square modulo 64. The words start at 0; for each set bit k of the word of f (Ratpoints.Sieve.fsq), lowest first (Ratpoints.Sieve.ctz), bit k b mod 64 is set in the word of every odd b, and for each set bit t of the word of the reversed polynomial (Ratpoints.Sieve.gsq), bit a in the word of t a mod 64 for every odd a. From the words the packings of the classes are made, with the word den_bits of the classes that admit a numerator (Ratpoints.Sieve.numClasses), in which the run sifts the numerators of each denominator; and a denominator whose class has the word 0 carries no point (Ratpoints.Sieve.denBits).

C: find_points.c:983-994, find_points.c:996-1000, find_points.c:1023-1050, find_points.c:1115

Deviation: the words returned, for the classes cls and the word den_bits that get_2adic_info fills from them in the same function, which Ratpoints.Sieve.numClasses makes from the words; the lowest set bit by the loop of RP_CTZL (Ratpoints.Sieve.ctz); remainders for the masks by 0x3f; natural numbers for the longs k, b, t and a; no output under DEBUG.

Equations

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

def Ratpoints.Sieve.denBits (nb : Vector UInt64 64) : UInt64

The classes of the denominators modulo 64 that admit a numerator, for the words nb of the 2-adic information (Ratpoints.Sieve.twoAdic): bit b is set exactly when nb[b] ≠ 0. A denominator whose class has its bit clear carries no point; when no bit is set, the curve has no point at all, not even at infinity (Ratpoints.Sieve.not_isPoint_of_denBits_eq_zero), and ratpoints ends the search with none, after a test of the points at infinity that then always passes (the 2-adic exit of Ratpoints.searchPoints). It is the reference of the word den_bits that get_2adic_info computes in the loop that makes the classes, with them (Ratpoints.Sieve.numClasses).

Equations

• Ratpoints.Sieve.denBits nb = Nat.fold 64 (fun (b : Nat) (h : b < 64) (db : UInt64) => if (nb[b] != 0) = true then db ||| 1 <<< b.toUInt64 else db) 0

The forbidden divisors

structure Ratpoints.Sieve.ForbiddenEntry : Type

A forbidden divisor tested with words: a prime p that divides no denominator of a point, with its p words, word r with bit j clear exactly when p ∣ 64 r + j (Ratpoints.Sieve.forbiddenRow; for one of the first Ratpoints.numPrimes primes of the table the first p words of its row of 0, Ratpoints.Sieve.sieves0), so that word w mod p says which of the 64 denominators 64 w + j the prime leaves; and the reciprocal of p (Ratpoints.Sieve.magic), with which the C code reduces the word number of the first word of a block by a multiplication (Ratpoints.Sieve.forbStarts).

C: find_points.c:157-161

Deviation: the words as an array, for the pointers start and end into the pattern sieves0 of the build or into the buffer of the arguments; a natural number for the long p and for the unsigned long reciprocal magic.

• p : Nat

  The prime.

• words : Array UInt64

  Its p words.

• magic : Nat

  The reciprocal of the prime (Ratpoints.Sieve.magic), with which the C code reduces the word number of the first word of a block by a multiplication.

@[instance_reducible]

instance Ratpoints.Sieve.instInhabitedForbiddenEntry : Inhabited ForbiddenEntry

Equations

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

structure Ratpoints.Sieve.ForbiddenVal : Type

A forbidden divisor tested by its valuation: a prime p and the mask of the valuations that no denominator of a point has at p, bit m of mask set when v_p(b) = m is excluded (Ratpoints.Sieve.forbiddenValuations).

C: find_points.c:166

Deviation: a natural number for the long p, and one for the unsigned long mask, so that it holds every valuation of a denominator, also beyond the 64 bits of a word (Ratpoints.Sieve.forbiddenValuations).

• p : Nat

  The prime.

• mask : Nat

  The mask of the excluded valuations.

def Ratpoints.Sieve.unitParts (c : List Int) (d p : Nat) (cm : Array Nat) : Id (Array (Option (Nat × Nat)))

The coefficients of the polynomial of degree d with the coefficient list c at the prime p, from the leading one down, with the coefficients cm reduced modulo p that the table of p hands back (Ratpoints.Sieve.examinePrime?): for each j ≤ d, none when c_{d-j} = 0, and otherwise, when cm[d - j] = 0, the valuation w_j of c_{d-j} at p with its unit part r_j modulo p, the sign included (Ratpoints.Setup.valuation), and when cm[d - j] ≠ 0, w_j = 0 and r_j = cm[d - j].

C: find_points.c:2198-2200, find_points.c:2204-2215

Deviation: an array of options of pairs, for the arrays present, w and r on the stack; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.forbiddenAt (us : Array (Option (Nat × Nat))) (sq : Array Bool) (m : Nat) : Id Bool

Whether no denominator b with v_p(b) = m carries a point, by the terms of F(a, b) at the prime p with the valuations and unit parts us of the coefficients (Ratpoints.Sieve.unitParts) and the squares sq modulo p: the least of the w_j + j m over the coefficients present is taken at one j only, j₀, and is odd, or j₀ is even and r_{j₀} is not a square modulo p; the term with the least valuation then makes F(a, b) a non-square.

C: find_points.c:2218-2228

Deviation: the valuations and unit parts of the coefficients as the array of options us (Ratpoints.Sieve.unitParts), for the arrays present, w and r, its size d + 1 for the bound degree of the loop, and the squares modulo p as the argument sq (Ratpoints.Sieve.squaresMod), for the row squares[pn] of the table of the build; the test returned, for the bit that the caller sets; remainders by 2 for the masks & 1; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.forbiddenValuations (c : List Int) (d p bHigh : Nat) (cm : Array Nat) : Id Nat

The valuations at the prime p ∣ c_d that no denominator b ≤ bHigh of a point has, for the polynomial of even degree d with the coefficient list c and its coefficients cm reduced modulo p, as a mask: bit m is set, for m = 1, 2, … while p ^ m ≤ bHigh, when the terms of F(a, b) exclude the valuation m (Ratpoints.Sieve.forbiddenAt, with the valuations and unit parts of the coefficients, Ratpoints.Sieve.unitParts, and the squares modulo p, Ratpoints.Sieve.squaresMod).

C: find_points.c:2192-2197, find_points.c:2201-2203, find_points.c:2216-2217, find_points.c:2229-2234

Deviation: the prime p itself, for its index pn in the table prime, and the squares modulo p by Ratpoints.Sieve.squaresMod, for the row of p in the table squares of the build; an array for the pointer coeffs_mod_p; a natural number for the unsigned long mask, without the cap m < LONG_LENGTH - 1 of the loop, which never binds for a long b_high and an odd prime, the loop ending before m = 40 (Ratpoints.Sieve.lt_forty_of_pow_le), and for p ≤ 1, which the C code never examines, the loop, once entered, does not end; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.allValuations (p bHigh : Nat) : Id Nat

The valuations at the prime p that a denominator b ≤ bHigh can have at all, as a mask: bit m set for m = 1, 2, … with p ^ m ≤ bHigh. A mask of forbidden valuations (Ratpoints.Sieve.forbiddenValuations) that holds all of them says that p divides no denominator of a point.

C: find_points.c:2632-2641

Deviation: a natural number for the unsigned long mask, without the cap m < LONG_LENGTH - 1 of the loop, which never binds for a long b_high and an odd prime, the loop ending before m = 40 (Ratpoints.Sieve.lt_forty_of_pow_le), and for p ≤ 1, which the C code never examines, the loop, once entered, does not end; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.forbiddenOfPrime (c : List Int) (d p bHigh : Nat) (cm : Array Nat) (atInf : Bool) : Id (Option (ForbiddenEntry ⊕ ForbiddenVal))

The forbidden divisor that the examined prime p gives for the polynomial of even degree d with the coefficient list c and the largest denominator bHigh, if any, from what the table of p hands back (Ratpoints.Sieve.examinePrime?), the coefficients cm reduced modulo p and the entry atInf of the table at p, whether there are points at infinity modulo p: for cm[d] = 0, that is p ∣ c_d, the mask of the forbidden valuations (Ratpoints.Sieve.forbiddenValuations), when it is not 0, gives p with its words, the first p words of the row of 0 of p (Ratpoints.Sieve.sieves0), if it holds every valuation that a denominator can have (Ratpoints.Sieve.allValuations), and p with the mask otherwise; for p ∤ c_d, p with its words when there are no points at infinity modulo p, which for even d says that c_d is not a square modulo p.

C: find_points.c:2627-2631, find_points.c:2642-2676

Deviation: the entry returned, for the entries that the C code writes into the arrays args->forb_ba and args->forbidden and counts; the words of the prime an array of the first p words of the pattern sieves0 of the build, for the pointers start and end into it; natural numbers for the longs and the reciprocal; no output under DEBUG.

Equations

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

def Ratpoints.Sieve.forbidden (c : List Int) (d examined maxForbidden bHigh : Nat) (ba : Array ForbiddenEntry) (val : Array ForbiddenVal) : Id (List ForbiddenEntry × List ForbiddenVal)

The forbidden divisors of the denominators of the polynomial of even degree d with the coefficient list c, at most maxForbidden of them, for the largest denominator bHigh, from those found in the loop of the tables over the first examined primes of Ratpoints.primeTable, ba tested with words (Ratpoints.Sieve.ForbiddenEntry) and val by their valuations (Ratpoints.Sieve.ForbiddenVal): unless c_d is a square (Ratpoints.Setup.isSquare), the primes p of the table from the position examined on, while fewer than maxForbidden are found and p ^ 2 ≤ bHigh, each with its words when c_d is not a square modulo p, that is when the Kronecker symbol (c_d / p) is -1: for one of the first Ratpoints.numPrimes primes of the table the first p words of its row of 0 (Ratpoints.Sieve.sieves0), and for a prime beyond them its words made as the C code makes them after the loop (Ratpoints.Sieve.forbiddenRow); both lists in the order found.

C: find_points.c:2533-2536, find_points.c:2561-2562, find_points.c:2709-2772, find_points.c:2778-2789

Deviation: the position examined as an argument, for the final pn_lim of the loop of the tables; the Kronecker symbol by the table of the squares modulo p, which marks 0 as a square, for mpz_kronecker_si; the flag RATPOINTS_CHECK_DENOM not tested, since the search computes the forbidden divisors only when the flag is set, for even degree (Ratpoints.sievingInfo); lists, for the two arrays of the arguments with their terminating zeros; the words of one of the first Ratpoints.numPrimes primes an array of the first p words of the pattern sieves0, for the pointers start and end into it, and those of a prime beyond them made with its entry, for the words that sieving_info makes after this loop in the buffer forb_words, with no failure for lack of memory, where sieving_info drops those whose words it cannot store; natural numbers for the longs and the reciprocals; no output under DEBUG.

Equations

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

The Jacobi test

def Ratpoints.Sieve.twoSign (m : Nat) (s : Int) : Int

The sign s times (2 / m) for odd m: negated when bit 1 of m is set (m ≡ 3, 7 (mod 8)) and again when bit 2 is (m ≡ 5, 7 (mod 8)), so negated in all exactly for m ≡ 3, 5 (mod 8), where (2 / m) = -1.

Equations

• Ratpoints.Sieve.twoSign m s = if (m &&& 4 != 0) = true then -if (m &&& 2 != 0) = true then -s else s else if (m &&& 2 != 0) = true then -s else s

def Ratpoints.Sieve.jacobiReduce (x y : Nat) (s : Int) : Id (Nat × Int)

One subtraction loop of the binary algorithm (Ratpoints.Sieve.jacobi) on the odd x and y: while x > y, x becomes x - y and is then halved until it is odd again, the sign s taking the factor (2 / y) at each halving (Ratpoints.Sieve.twoSign); the new x and the sign.

Equations

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

def Ratpoints.Sieve.jacobiRound (f b : Nat) : Id (Nat × Int)

One round of the binary algorithm (Ratpoints.Sieve.jacobi) for the symbol (f / b), f > 0 and b odd: from n = f and m = b, the factors 2 are taken out of n with the sign of (2 / m); then the two are exchanged, with the sign of the reciprocity when both are ≡ 3 (mod 4), and the larger reduced by the smaller (Ratpoints.Sieve.jacobiReduce), in turn, until they are equal. The common value g, the gcd of f and b, is returned with the sign, which is the symbol (f / b) when g = 1.

Equations

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

def Ratpoints.Sieve.jacobi (b : Nat) (lcf : Int) : Id Int

The Jacobi symbol (lcf / b*) for b > 0, where b* is b with the prime factors of 2 lcf taken out, so that it is ±1, by the binary algorithm of the C code: the factors 2 are taken out of b, and f = lcf mod b; while f ≠ 0, a round of the algorithm (Ratpoints.Sieve.jacobiRound) gives the symbol (f / b) when f and b are coprime, and otherwise their gcd, which is divided out of b, f being reduced modulo the new b when it is not smaller. When f is 0, b* is 1, and so is the symbol. For b = 0 the loop does not end.

C: find_points.c:498-566, find_points.c:568-641

Deviation: one function for jacobi, on the GMP integer lcf, and jacobi1, on a long, which the run calls when all coefficients are longs (use_c_long), with the steps of jacobi: jacobi1 takes the sign of lcf out as (-1 / b)^neg and its value LONG_MIN as LONG_MIN / 4, so that the negation of a negative lcf is a long (Ratpoints.fitsLong_neg_ite_div_four), reduces |lcf| modulo b only for b < 2^59, and does not reduce it after dividing b by the gcd, which changes the steps but not the symbol; the round of the algorithm and its two subtraction loops, which the C code writes out twice each, as helpers (Ratpoints.Sieve.jacobiRound, Ratpoints.Sieve.jacobiReduce, Ratpoints.Sieve.twoSign); natural numbers for the longs b, f, n and m, and integers for the long sign s and the long lcf of jacobi1; f the Euclidean lcf % b, for mpz_fdiv_r_ui with its scratch integer tmp; the tests f = 0 of the C code, at the start and after each division of b, as the condition of the outer loop; the masks of the signs by &&& on natural numbers; the symbol as an integer, for the int.

Equations

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

structure Ratpoints.Sieve.JacobiInfo : Type

What the Jacobi test by tables knows of the leading coefficient lcf = ±2^v ∏ q_i^(e_i): its odd primes q_i in increasing order, each with the table of the non-squares modulo q_i when e_i is odd (entry r true when r is not a nonzero square modulo q_i) and none when e_i is even, and the eight signs, entry i true when (-1 / b)^neg (2 / b)^v times the signs of the reciprocity of the q_i with odd e_i is -1 for b ≡ i (mod 8); and the reciprocals of the q_i (Ratpoints.Sieve.magic), in their order, with which the test reduces modulo them.

C: find_points.c:672-681

Deviation: a list of pairs for the arrays q and nonsq and their count nq, and an array of its own for the array magic; the tables as arrays of their own, for the space that they take from the table jtab of the run; natural numbers for the longs q and the unsigned longs magic, and Booleans for the unsigned chars of the tables and of the signs.

• primes : List (Nat × Option (Array Bool))

  The odd primes of the leading coefficient, each with its table of non-squares when its exponent is odd.

• magic : Array Nat

  The reciprocals of the primes, in their order.

• sign : Array Bool

  The eight signs, indexed by the residues modulo 8.

def Ratpoints.Sieve.nonSquares (q : Nat) : Id (Array Bool)

The non-squares modulo the odd prime q, as a table: all entries true, then the entry of x ^ 2 mod q cleared for 0 < x ≤ q / 2, the squares reached by the steps 2 x + 1, with one subtraction of q; the entry of 0 stays true and is never read.

C: find_points.c:709-713

Deviation: a fresh array, for the space in the table jtab of the run; Booleans for the unsigned chars, natural numbers for the longs x and s.

Equations

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

def Ratpoints.Sieve.jacobiSigns (n3 : Nat) (neg : Bool) (v : Nat) : Array Bool

The eight signs of the Jacobi test by tables, entry i for b* ≡ i (mod 8): the parity of [i ≡ 3 (mod 4)] (n₃ + neg) + [i ≡ 3, 5 (mod 8)] v, for the number n₃ of the primes ≡ 3 (mod 4) of the leading coefficient with an odd exponent, whether it is negative (neg) and the exponent v of 2 in it: the product of (-1 / b*)^neg, (2 / b*)^v and the signs of the reciprocity.

C: find_points.c:721-729

Deviation: Booleans for the bits.

Equations

• Ratpoints.Sieve.jacobiSigns n3 neg v = Array.map (fun (i : Nat) => i &&& 3 == 3 && (n3 + if neg = true then 1 else 0) % 2 == 1 ^^ (i == 3 || i == 5) && v % 2 == 1) (Array.range 8)

def Ratpoints.Sieve.jacobiSetup (lcf : Int) (bHigh : Nat) : Id (Option JacobiInfo)

The tables of the Jacobi test by tables (Ratpoints.Sieve.JacobiInfo) for the leading coefficient lcf ≠ 0 and the largest denominator bHigh, or none where they do not apply: when bHigh > Ratpoints.mulModLimit, when the odd part of |lcf| has a prime factor beyond Ratpoints.primeTable or more than Ratpoints.jacobiPrimes distinct prime factors, or when the primes with an odd exponent sum to more than Ratpoints.jacobiTable. The power 2^v is divided off; then each prime q of the table that divides the cofactor, in turn while the cofactor is not 1, with its exponent, its reciprocal (Ratpoints.Sieve.magic) and, for an odd exponent, the table of the non-squares modulo q (Ratpoints.Sieve.nonSquares), counting the primes ≡ 3 (mod 4) with an odd exponent; and the signs (Ratpoints.Sieve.jacobiSigns).

C: find_points.c:683-708, find_points.c:714-720, find_points.c:730-731

Deviation: the tables as fresh arrays, for the table jtab of the run that tab and tab_len give, whose bound Ratpoints.jacobiTable on their total size is kept; the valuations by Ratpoints.Setup.valuation, for mpz_scan1 at 2 and the loop of exact divisions at the odd primes, the power then divided off at once; natural numbers for the GMP integer tmp, the longs and the unsigned longs of the reciprocals, which are ULONG_MAX / q + 1 for the odd primes q; none and the tables returned, for the return values 0 and 1 and the structure that ji points to.

Equations

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

def Ratpoints.Sieve.jacobiTest (ji : JacobiInfo) (b : Nat) : Id Bool

Whether (lcf / b*) = 1 for the denominator 0 < b ≤ Ratpoints.mulModLimit (more generally b q < 2 ^ 64 for every prime q of ji), by the tables ji of the leading coefficient lcf (Ratpoints.Sieve.jacobiSetup): the odd part of b (Ratpoints.Sieve.ctz), out of which every prime q of lcf is divided as often as it divides, is b*; the sign of b* mod 8 is combined by exclusive or with the entry of b* mod q in the table of each prime with an odd exponent, and the test passes when the result is false. The quotient k by q and the remainder b - k q are computed by a multiplication with the reciprocal of q that the tables hold (Ratpoints.Sieve.mulDiv), which gives the quotient for b q < 2 ^ 64: for the denominators up to the bound Ratpoints.mulModLimit < 2 ^ 32 for which the tables are made, and their primes, primes of Ratpoints.primeTable, below 2 ^ 10. For b = 0 and every multiple of 2 ^ 64, whose word b.toUInt64 is 0, the loop of Ratpoints.Sieve.ctz does not end.

C: find_points.c:734-759

Deviation: the list of the primes with their tables walked with the positions (List.zipIdx), at which the reciprocals are read, for the index i of the arrays; the odd part as the shift by the lowest set bit of the word b (Ratpoints.Sieve.ctz, the loop of RP_CTZL); b mod 8 for b & 7; natural numbers for the longs, the difference b - k q truncated at 0, which is the difference of the C code, since k q ≤ b where the multiplication gives the quotient; a Boolean for the unsigned char s, with exclusive or for ^= and negation for the test s == 0, and the test returned as a Boolean, for the int.

Equations

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

The shapes of the run

def Ratpoints.Sieve.ceilSqrt (n : Nat) : Nat

The least k ≥ 1 with k ^ 2 ≥ n, for n ≥ 1: ⌊√(n - 1)⌋ + 1.

C: find_points.c:464-471

Deviation: the exact square root of the natural numbers (Nat.sqrt), for the square root in double corrected by a step either way; 1 for n = 0, where the C code divides by 0; natural numbers for the longs, so that a negative argument, whose square root in double is not a number, cannot occur.

Equations

• Ratpoints.Sieve.ceilSqrt n = (n - 1).sqrt + 1

def Ratpoints.Sieve.floorSqrt (n : Nat) : Nat

The largest k with k ^ 2 ≤ n, ⌊√n⌋.

C: find_points.c:3766-3774

Deviation: the exact square root of the natural numbers (Nat.sqrt), for the square root in double corrected by a step either way; natural numbers for the longs, so that 0 is the only case n < 1.

Equations

• Ratpoints.Sieve.floorSqrt n = n.sqrt

def Ratpoints.Sieve.denInfoTest (info : List Setup.DenInfo) (b : Nat) : Id Bool

The valuation test of the divisor shape on the denominator b: false when for some prime p of the leading coefficient, with its valuation val and its slope (Ratpoints.Setup.DenInfo, made by Ratpoints.Setup.setupUs1), the valuation v = v_p(b) (Ratpoints.Setup.valuation) has v ≥ slope and v + val odd, and true otherwise.

C: find_points.c:3944-3953

Deviation: the test returned, for the flag flag; natural numbers for the ints and longs.

Equations

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

def Ratpoints.Sieve.wordsTest (forbVal : List ForbiddenVal) (useJacobi : Bool) (fast : Option JacobiInfo) (lcf : Int) (b : Nat) : Id Bool

The tests of the word shape on a denominator b that its word leaves (Ratpoints.Sieve.denWord): with the tables fast of the Jacobi test, their test (Ratpoints.Sieve.jacobiTest); then that no forbidden divisor tested by its valuation excludes v_p(b) (Ratpoints.Setup.valuation); then, with the Jacobi test on (useJacobi) and no tables, that the binary algorithm (Ratpoints.Sieve.jacobi) gives (lcf / b*) = 1.

C: find_points.c:4010-4011, find_points.c:4013-4041

Deviation: the binary algorithm of jacobi also where the run calls jacobi1 on the long lcf_long (Ratpoints.Sieve.jacobi); bit v_p(b) of the mask of a natural number, false beyond its bits (Nat.testBit), for the shift and the mask of the unsigned long; the test returned, where the loop goes on to the sieve or to the next denominator; natural numbers for the longs; no output under DEBUG.

Equations

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

inductive Ratpoints.Sieve.Shape : Type

The shape of the loop over the denominators, as run_setup chooses it (Ratpoints.Sieve.runSetup), with its data: the squares (odd degree, |c_d| = 1); the divisors of the leading coefficient times squares, with the primes of the valuation test and the divisors (odd degree otherwise, when Ratpoints.Setup.setupUs1 succeeds); the words of 64 denominators, with the forbidden divisors tested with words and by their valuations, the switch of the Jacobi test, its tables when they apply and the leading coefficient (even degree, when there is a test); and every denominator.

C: find_points.c:3725-3728, find_points.c:3736-3749, find_points.c:3763

Deviation: an inductive type with the data of each shape, for the constant shape and the fields of rp_run that the shapes read, with these exceptions: the forbidden divisors as lists, for forb_ba and forbidden with no count nfb, a list having its length; the tables of the Jacobi test as an option, for ji, jtab and fast_jacobi; with the words, the bit RATPOINTS_USE_JACOBI of the flags and the leading coefficient args->cof[args->degree], which run_block reads through the field args, the run taking the rest of what it reads of the arguments as its own arguments (Ratpoints.Sieve.sieveRun); no copies of use_c_long and lcf_long, which only jacobi1 reads (Ratpoints.Sieve.jacobi); the segments and the blocks (Ratpoints.Sieve.BlockPlan) and the counters and the decisions of the correction of the moduli (Ratpoints.Sieve.Correction) structures of their own; the bounds of the search intervals (the struct iv of the run, Ratpoints.Sieve.runSetup), the classes with their row offsets and den_bits passed to the run apart (Ratpoints.Sieve.sieveRun).

• squares : Shape

  RP_SHAPE_SQUARES: the squares.

• squares1 (info : List Setup.DenInfo) (divisors : List Nat) : Shape

  RP_SHAPE_SQUARES1: the divisors of the leading coefficient times squares.

• words (forb : List ForbiddenEntry) (forbVal : List ForbiddenVal) (useJacobi : Bool) (fast : Option JacobiInfo) (lcf : Int) : Shape

  RP_SHAPE_WORDS: the words of 64 denominators.

• all : Shape

  RP_SHAPE_ALL: every denominator.

def Ratpoints.Sieve.runSetup (useSquares : Bool) (us1 : Option (List Setup.DenInfo × List Nat)) (checkDenom useJacobi : Bool) (forb : List ForbiddenEntry) (forbVal : List ForbiddenVal) (lcf : Int) (H bHigh : Nat) (domain : List (Double × Double)) : Id (Shape × Array IntervalBounds)

The shape of the run (Ratpoints.Sieve.Shape), as run_setup chooses it from the flags of the search, and the bounds of its search intervals: the squares when useSquares; the divisors with their data when the divisor set-up has succeeded (us1, Ratpoints.Setup.setupUs1); the words when checkDenom, with the forbidden divisors forb and forbVal, the switch useJacobi of the Jacobi test, its tables when the test is on and they apply to the leading coefficient lcf and the largest denominator bHigh (Ratpoints.Sieve.jacobiSetup), and lcf; and every denominator otherwise. The bounds of the search intervals domain for the height bound H and the denominators up to bHigh (Ratpoints.Sieve.exactBounds) are made after the shape, once for the run.

C: find_points.c:3778-3806, find_points.c:3869-3870, find_points.c:3876-3877

Deviation: the shape returned with its data, for the fields of the run that run_setup fills, and Booleans and an option for the bits RATPOINTS_USE_SQUARES, RATPOINTS_USE_SQUARES1, RATPOINTS_CHECK_DENOM and RATPOINTS_USE_JACOBI of the flags; the bounds of the search intervals returned as an array with the shape, for the struct iv of the run with its pointers bd and end; the search intervals, the height bound and the largest denominator as arguments, for the fields of the arguments that exact_bounds reads; no count nfb, a list having its length; no copies of use_c_long and lcf_long, which only jacobi1 reads (Ratpoints.Sieve.jacobi); the segments and the blocks made by Ratpoints.Sieve.Shape.blockPlan, and the counters and the decisions of the correction by Ratpoints.Sieve.Correction.start; no failure for lack of memory.

Equations

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

Examples

The words of the 2-adic information and the tables of the Jacobi test against those that a build of ratpoints at the pinned commit prints with a dump of the side of the denominators on the standard error (the words fsq, gsq and nb of get_2adic_info, den_bits and the tables of the Jacobi test), and against their rule. The forbidden divisors that the dump prints are in the examples of Ratpoints.Model.Choice, the denominators that the run sifts and the run of the divisor shape against the points that ratpoints prints in those of Ratpoints.Model.Blocks.