The sieve

The components of the sieve, each in its place in the C function find_points_work_1: the operations on the bit arrays of 64-bit words of the C code that the masks and the second stage use; the packing of the numerators of a class of the denominators modulo 64 into one class modulo a power of 2 (Ratpoints.Sieve.NumClass); the second stage, on a bit array that the first leaves nonzero or on one of its words, with the rows read at the word number plus their offsets (Ratpoints.Sieve.secondStage, Ratpoints.Sieve.secondStageWord); one bit array through the second stage and the extraction of the points of its numerators in the packing of a class, in either arm of the second stage, one word at a time or on the whole bit array (Ratpoints.Sieve.siftBitArray, Ratpoints.Sieve.siftBitArrayByWords, Ratpoints.Sieve.siftBitArrayWhole); one piece of bit arrays from the first stage, with the first moduli, in the arm that the chunk chooses, through the second, with the others, to the points of its numerators (Ratpoints.Sieve.siftPiece); the bits of an interval of numerators in the packing of a class (Ratpoints.Sieve.numeratorsToBits), the bits of the numerators of a search interval at a denominator, from the forms of its ends or from the products in 128 bits (Ratpoints.Sieve.intervalBits, Ratpoints.Sieve.intervalBitsExact, with the bounds of Ratpoints.Model.Bounds), the rows of the moduli for a denominator from the tables of rows of their entries with the row offsets of its class (Ratpoints.Sieve.setRows), the rows that are not built yet built into their tables of rows (Ratpoints.Sieve.buildRows), and the points of the bits of one interval in pieces (Ratpoints.Sieve.siftBits); and the numerators of one denominator in the search intervals, in the packing of its class, with the products of the check and what the third stage needs as thunks (Ratpoints.Sieve.sift). The components that take one numerator at a time, the test of a candidate that survives the first two stages, with the test for common factors and the third stage (Ratpoints.Sieve.accepted), the exact check (Ratpoints.Sieve.checkPoint) and its reference, the check of a numerator (Ratpoints.Sieve.checkNum), and the points at infinity (Ratpoints.Sieve.pointsAtInfinity), are in Ratpoints.Model.Candidate; the first stage in both arms, with the operations on bit arrays that it uses and the sieve specs (Ratpoints.Sieve.andRowsChunked, Ratpoints.Sieve.andRows, Ratpoints.Sieve.SieveSpec), is in Ratpoints.Model.FirstStage. The tables of the primes and of the prime powers and the sieve entries of the moduli, with the admission tests of the rows of a denominator, are in Ratpoints.Model.Tables; the classes of the denominators modulo 64 with their packings, the row offsets of the packings and the residues of a denominator divided by the stride of its class (Ratpoints.Sieve.numClasses, Ratpoints.Sieve.classOffsets, Ratpoints.Sieve.fillBpList) are in Ratpoints.Model.Packing; the 2-adic information that gives the words of the classes is in Ratpoints.Model.Denominators; the counters of the sieve (Ratpoints.Sieve.Counters) are in Ratpoints.Model.Candidate, and the loop over the denominators in blocks, with the correction of the moduli from those counters (Ratpoints.Sieve.sieveRun), in Ratpoints.Model.Blocks. The plain sieve of one denominator, one Boolean per numerator (Ratpoints.Sieve.sieveDen), and the test for common factors and the exact check of its survivors (Ratpoints.Sieve.checkDen) are not part of the run: they are the reference of the bit arrays of words (Ratpoints.Sieve.run_sift_eq_deliver_checkDen). Every row, and the word of the class of a denominator in the 2-adic information, let every point through, and the packing keeps every numerator that the word admits, the rows of the residue of the denominator divided by the stride, read at the row offsets of the class, admitting the numerators of the class that the rows of the denominator admit; so the sieve of a denominator delivers exactly its points in the brute-force reference Ratpoints.bruteForce whose x / z lies in a search interval (all of them for the one interval [-h, h], h ≥ H), in the same order, to the callback of the search (Ratpoints.Delivery), each mapped by Ratpoints.Sieve.swapPoint when the flag of the reversal is set: the map gives the point of the caller's curve for a point of a polynomial that the reversal check has reversed (Ratpoints.Setup.reversal), the exact check delivers the mapped points when its flag is set, as the points at infinity give them, and the components from the run down to the check hand the flags (Ratpoints.CheckFlags) and the delivery on. Each component tests the flag of a stop of the callback after each call that can set it and returns when it is set; under RATPOINTS_NO_CHECK the sieve delivers every numerator that passes it, and under RATPOINTS_NO_Y only the points with y ≥ 0. The rows of the moduli as words, with the row of 0 of a prime that the build of ratpoints generates (Ratpoints.Sieve.sieves0), the builders of the rows of the primes, the prime powers and the products, the row of a sieve entry read from its table of rows or built into it (Ratpoints.Sieve.SieveEntry.fetchRow) and the tables of rows of a run (Ratpoints.Sieve.RowStore), are in Ratpoints.Model.Rows.

Main definitions

• Ratpoints.Sieve.sieveDen, Ratpoints.Sieve.checkDen: the plain sieve of one denominator and the points of its survivors, the reference of the bit arrays of words.
• Ratpoints.Sieve.clearLowBits, Ratpoints.Sieve.clearHighBits, Ratpoints.Sieve.isZeroAt: the masks on the bit arrays of 64-bit words of the C code and the test for zero.
• Ratpoints.Sieve.NumClass: the packing of the numerators of a class of the denominators modulo 64, its stride, its residue, its pattern and the position of its row offsets.
• Ratpoints.Sieve.secondStage, Ratpoints.Sieve.secondStageWord: the second stage on a bit array and on one of its words, the rows of its moduli, read at the word number plus their offsets, and-ed in while a bit is left.
• Ratpoints.Sieve.walkWord: the walk through the set bits of a word, lowest first, each numerator going to the test of a candidate and, if it passes, to the exact check, which delivers its points to the callback; the walk returns when the callback stops the search.
• Ratpoints.Sieve.siftBitArrayByWords, Ratpoints.Sieve.siftBitArrayWhole, Ratpoints.Sieve.siftBitArray: one bit array that the first stage leaves nonzero, through the second stage one word at a time or on the whole bit array, and the walks through its words; and the choice between the two arms.
• Ratpoints.Sieve.scanPiece: the scan over the bit arrays of a piece up to a sentinel, stepping over those that are zero, and a copy of each of the others through the second stage and the extraction.
• Ratpoints.Sieve.siftPiece: one piece of bit arrays, from the first stage and the masks at its two ends, through the second stage, to the points of its numerators.
• Ratpoints.Sieve.numeratorsToBits: the bits of an interval of numerators in the packing of a class.
• Ratpoints.Sieve.intervalBitsExact, Ratpoints.Sieve.intervalBits: the bits of the numerators of a search interval at a denominator, from the products in 128 bits and from the forms of its ends.
• Ratpoints.Sieve.setRows, Ratpoints.Sieve.buildRows: the moduli of the first two stages with their rows from the tables of rows and their offsets for a denominator, the start 0 and the end p, and the rows that are not built yet built into their tables of rows.
• Ratpoints.Sieve.siftBits: the points of the numerators of an interval of bits, in pieces.
• Ratpoints.Sieve.sift: the points of one denominator, its numerators in the search intervals in the packing of its class, in pieces of bit arrays.

The plain sieve

def Ratpoints.Sieve.sieveDen (H b : Nat) (entries : List SieveEntry) : Id (Vector Bool (2 * H + 1))

The plain sieve of the denominator b: an array of 2H + 1 Booleans, one for each numerator a = i - H, all true at the start; for each sieve entry of entries in turn, every Boolean is replaced by its conjunction with the row of b at its numerator (Ratpoints.Sieve.SieveEntry.admits). With Ratpoints.Sieve.checkDen it is the reference of the bit arrays of words: for pieces of at least one bit array, a denominator 0 < b < 2 ^ 63, H < 2 ^ 63, a class that packs a word (Ratpoints.Sieve.NumClass.Packs) and has a row of offsets, entries of the first two stages whose tables of inverses invert and that are packed for the class at its offsets (Ratpoints.Sieve.SieveEntry.PackedFor), with the reciprocals of their moduli and the residues of b divided by the stride of the class, and entries of the third stage of the shape of Ratpoints.Sieve.SieveEntry.IsPrimeEntry, with the reciprocals of their moduli, the points that Ratpoints.Sieve.sift delivers in the packing of the class with the rows of the entries of its first two stages, from a store of the tables of rows that fits these entries (Ratpoints.Sieve.RowStore.Fits), and bounds of the search intervals that give the ranges of the numerators at b (Ratpoints.Sieve.RangesFor; all of -H, …, H for the one search interval [-h, h], h ≥ H), without RATPOINTS_NO_CHECK, are those that Ratpoints.Sieve.checkDen finds on the plain sieve with all these entries whose numerators lie in one of the ranges (Ratpoints.Sieve.inRanges) and pass the word, all of them for any word that admits the numerators of the points (such as the word nb[b mod 64] of Ratpoints.Sieve.twoAdic), each mapped by Ratpoints.Sieve.swapPoint when the flag of the reversal is set, and those with y < 0 left out under RATPOINTS_NO_Y (Ratpoints.Sieve.run_sift_eq_deliver_checkDen).

Equations

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

def Ratpoints.Sieve.checkDen (c : List Int) (d H b : Nat) (surv : Vector Bool (2 * H + 1)) : Id (Array (Int × Int × Int))

The points (a, y, b) with the denominator b and a numerator a = i - H whose entry in surv is true, by increasing a: each such numerator is tested for common factors with b and checked exactly, as the brute-force reference checks it (Ratpoints.BruteForce.pointsOfDen): F(a, b) by Horner's rule on the products cₖ b^(d - k), computed once, with one more factor b for odd d, then (a, y, b) and, for y ≠ 0, (a, -y, b) when F(a, b) = y ^ 2 with y ≥ 0. With the plain sieve Ratpoints.Sieve.sieveDen it is the reference of the bit arrays of words: under the hypotheses of Ratpoints.Sieve.run_sift_eq_deliver_checkDen, Ratpoints.Sieve.sift in the packing of a class of a word, with bounds of the search intervals that give the ranges of the numerators at b (Ratpoints.Sieve.RangesFor; all of -H, …, H for the one search interval [-h, h], h ≥ H), delivers the points that it finds on the plain sieve with all the sieve entries whose numerators lie in one of the ranges (Ratpoints.Sieve.inRanges) and pass the word, all of them for any word that admits the numerators of the points (such as the word nb[b mod 64] of Ratpoints.Sieve.twoAdic), each mapped by Ratpoints.Sieve.swapPoint when the flag of the reversal is set, those with y < 0 left out under RATPOINTS_NO_Y, without RATPOINTS_NO_CHECK.

Equations

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

Words and bit arrays

def Ratpoints.Sieve.clearLowBits {m : Nat} (v : Vector UInt64 m) (s : Nat) : Vector UInt64 m

The lowest s bits of bit array 0 of the words v cleared, for s < Ratpoints.rbaLength: the words below s / 64 are set to 0, and word s / 64 is and-ed with ~~~0 <<< (s % 64).

C: rp-private.h:153-155, rp-private.h:206-213, rp-private.h:242-244, rp-private.h:268-270, rp-private.h:291

Deviation: one definition for every build, the loop of the build with 512-bit bit arrays, of which the macros of the builds with 256-bit and 128-bit bit arrays are unrolled cases and that of the build with 64-bit bit arrays the case of one word; the bit array is the first Ratpoints.rbaPack words of an array, for the vector type of the build.

Equations

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

def Ratpoints.Sieve.clearHighBits {m : Nat} (v : Vector UInt64 m) (j s : Nat) : Vector UInt64 m

The highest s bits of bit array j of the words v cleared, for s < Ratpoints.rbaLength: for the number rbaPack of words of a bit array (Ratpoints.rbaPack), word q = rbaPack - 1 - s / 64 of the bit array is and-ed with ~~~0 >>> (s % 64), and its words above q are set to 0.

C: rp-private.h:156-159, rp-private.h:214-221, rp-private.h:245-247, rp-private.h:271-273, rp-private.h:292

Deviation: one definition for every build, the loop of the build with 512-bit bit arrays, of which the macros of the builds with 256-bit and 128-bit bit arrays are unrolled cases and that of the build with 64-bit bit arrays the case of one word; the bit array is given by its index in an array of words, rbaPack consecutive words, for a pointer to a value of the vector type of the build.

Equations

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

def Ratpoints.Sieve.isZeroAt {m : Nat} (v : Vector UInt64 m) (pos : Nat) : Bool

Whether bit array pos of the words v is zero: for the number rbaPack of words of a bit array (Ratpoints.rbaPack), its words rbaPack * pos + κ, κ < rbaPack, are all 0.

C: rp-private.h:137-152, rp-private.h:179-202, rp-private.h:241, rp-private.h:267, rp-private.h:290, rp-private.h:306-308

Deviation: one definition for every build, on a bit array given by its index in an array of words, rbaPack consecutive words that it compares with 0 one at a time, for the tests of the builds on the vector type, with vector instructions or by or-ing its words; the test for zero TESTZ also stands for its negation TEST.

Equations

• Ratpoints.Sieve.isZeroAt v pos = Ratpoints.rbaPack.all fun (κ : Nat) (x : κ < Ratpoints.rbaPack) => v[Ratpoints.rbaPack * pos + κ]! == 0

structure Ratpoints.Sieve.NumClass : Type

The packing of the numerators of the denominators of one class modulo 64, rp_num_class: the admissible numerators modulo 64 of the class (the word of the class in the 2-adic information, Ratpoints.Sieve.twoAdic) lie in one class a₀ mod 2 ^ k, with k the largest below Ratpoints.numStrides and at most 6 that allows this, so that the sieve in the packing holds only those, bit t of the bit array with the word number 0 standing for the numerator a₀ + 2 ^ k t; bits is the pattern of the class in that packing, bit t the bit (a₀ + 2 ^ k t) mod 64 of the word, from which the first stage starts in the packing, and 0 for a class without admissible numerators, which the run never sifts; offset is the position in the array of the row offsets of the run at which the offsets of the row of the packing (k, a₀) begin, one for each modulus, none until the row offsets of the packings are made (Ratpoints.Sieve.classOffsets). The classes of a run are made by Ratpoints.Sieve.numClasses.

C: rp-private.h:494-495

Deviation: one word for the bit array bits, the vector RBA(packed) of RBA_PACK copies of the word, which the first stage writes into every word of a bit array; natural numbers for the longs k and a0; the position of the row of offsets in the array of the offsets as an option, for the pointer offset into that array, none for NULL.

• bits : UInt64

  The pattern of the class in its packing, 0 for a class without admissible numerators.

• k : Nat

  The exponent of the stride 2 ^ k of the packing.

• a0 : Nat

  The residue a₀ < 2 ^ k of the admissible numerators.

• offset : Option Nat

  Where the offsets of the row of the packing begin in the array of the row offsets, none until they are made.

@[instance_reducible]

instance Ratpoints.Sieve.instInhabitedNumClass : Inhabited NumClass

Equations

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

The second stage

def Ratpoints.Sieve.secondStage (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (i : Int) (nums : Vector UInt64 rbaPack) : Id (Vector UInt64 rbaPack)

The second stage on the bit array nums with the word number i, a copy of a bit array that the first stage left nonzero: for each modulus p of specs with its row and its offset, and its reciprocal mg from mgs, in turn, while nums is not zero (Ratpoints.Sieve.isZeroAt), nums is and-ed with bit array (i + offset) mod p of the row (Ratpoints.Sieve.andBitArray), the remainder by a multiplication with mg (Ratpoints.Sieve.mulMod) when small says that the word numbers of the piece allow it, and by the helper mod of the C code otherwise (Ratpoints.Sieve.modLong). Stopping early loses nothing, since a zero bit array stays zero, so that the result is nums and-ed with the rows of all the moduli.

C: sift.c:1083, sift.c:1085, sift.c:1175-1202

Deviation: the moduli of the stage with their rows and their reciprocals as two lists, for the pointers ssp and mg that step through the sieve specs and the array magics from position sp1 on and the count sp2 - sp1, with no bound 2 RATPOINTS_NUM_PRIMES on their number (the length of magics, find_points.c:347), which ratpoints never reaches since each entry of sieve_list owns its own prime (find_points.c:329-331), where the model takes any moduli, which may repeat; one bit array of Ratpoints.rbaPack words, for the vector nums; natural numbers and integers for the longs, and the sum v a natural number for the long that RP_MULMOD converts to an unsigned long, which is not negative under small, and which stays a long where the helper mod reduces it outside small (Ratpoints.Sieve.fitsLong_add); a Boolean for the int small; no count of the ands of the second stage under RP_PHASE_COUNTS, and no output under DEBUG.

Equations

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

def Ratpoints.Sieve.secondStageWord (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (i : Int) (κ : Nat) (x : UInt64) : Id UInt64

The second stage on word κ < Ratpoints.rbaPack of the bit array with the word number i, the arm of the second stage for one word at a time: for each modulus p of specs with its row and its offset, and its reciprocal mg from mgs, in turn, while x ≠ 0, x is and-ed with word κ of bit array (i + offset) mod p of the row, the remainder by a multiplication with mg when small says that the word numbers of the piece allow it, and by the helper mod otherwise. Stopping early loses nothing, and the result is word κ of the result of Ratpoints.Sieve.secondStage on a bit array whose word κ is x.

C: sift.c:1135-1136, sift.c:1141-1152

Deviation: the moduli of the stage with their rows and their reciprocals as two lists, for the pointers sspk and mg that step through the sieve specs and the array magics from position sp1 on and the count sp2 - sp1, with no bound 2 RATPOINTS_NUM_PRIMES on their number (the length of magics, find_points.c:347), which ratpoints never reaches since each entry of sieve_list owns its own prime (find_points.c:329-331), where the model takes any moduli, which may repeat; natural numbers and integers for the longs, and the sum v a natural number for the long that RP_MULMOD converts to an unsigned long, which is not negative under small, and which stays a long where the helper mod reduces it outside small (Ratpoints.Sieve.fitsLong_add); a Boolean for the int small; no count of the ands of the second stage under RP_PHASE_COUNTS.

Equations

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

One piece

def Ratpoints.Sieve.walkWord {σ : Type} (process : Int → Int → Int → σ → Answer σ) (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) (checks : Thunk (List CheckSpec)) (x : UInt64) (a0 : Int) (step : Nat) (r : Delivery σ) (cnt : Counters) : Id (Delivery σ × Counters)

The set bits of the word x, lowest first, bit t standing for the numerator a = a0 + step t: while x ≠ 0, for the lowest set bit t of x (Ratpoints.Sieve.ctz), the numerator a goes to the test for common factors with the denominator b and the third stage (Ratpoints.Sieve.accepted, with the thunk checks of what that stage needs), and if it passes, to the exact check (Ratpoints.Sieve.checkPoint, with the thunk w of the products, the degree d and the flags fl), which delivers its points to the callback process on the delivery r, after which the walk returns if the callback has stopped the search; then that bit is cleared by x &&& (x - 1). Each numerator counts one up the count bits of the counters cnt (Ratpoints.Sieve.Counters), and the test of a candidate counts its own. This is the loop RP_EACH_SET_BIT of the C code with the body that the extraction runs for each set bit; the step is the stride 2 ^ k of the packing of the class of b. The callers call it only while the flag quit of r is clear, and return when it is set after it.

C: sift.c:262-264, sift.c:1161-1171, sift.c:1227-1255, sift.c:1265-1292

Deviation: the lowest set bit by the loop of RP_CTZL for a compiler without the builtin (Ratpoints.Sieve.ctz); one definition for the body at the three places of the extraction, the first word of a bit array, the others, and a word of the arm of the second stage for one word at a time; natural numbers and integers for the longs; the delivery r passed and returned, for the pointers info and wk->quit and the count total of _ratpoints_sift0, to which RP_CHECK_POINT adds the count of the check (lines 1168, 1240, 1250, 1279, 1287); the return after a stop (lines 1169, 1241, 1251, 1280, 1288) a return from the walk, which its callers pass on, testing the flag after it (Ratpoints.Sieve.siftBitArrayByWords, Ratpoints.Sieve.siftBitArrayWhole, then Ratpoints.Sieve.scanPiece after the bit array), where the C code returns from _ratpoints_sift0; the counters passed and returned, for the field n_bits of the sieving thread (lines 1166, 1233, 1271); no counts under RP_PHASE_COUNTS; no output under DEBUG.

Equations

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

def Ratpoints.Sieve.siftBitArrayByWords {σ : Type} (process : Int → Int → Int → σ → Answer σ) (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (checks : Thunk (List CheckSpec)) (cl : NumClass) (i : Int) (nums : Vector UInt64 rbaPack) (r : Delivery σ) (cnt : Counters) : Id (Delivery σ × Counters)

The arm of the second stage one word at a time, for the bit array that the first stage left nonzero with the word number i, from a copy nums of it, the points of its numerators delivered to the callback process on the delivery r: for each word κ of nums that is not zero, the second stage on that word (Ratpoints.Sieve.secondStageWord, with the moduli of specs, their reciprocals mgs and the test small) and the walk through its set bits (Ratpoints.Sieve.walkWord) from the first numerator of the word, after which it returns if the callback has stopped the search. For the stride 2 ^ k and the residue a₀ of the class cl of the denominator (Ratpoints.Sieve.NumClass), bit t of word κ stands for the numerator a₀ + 2 ^ k (rbaLength i + 64 κ + t), for the number rbaLength of bits of a bit array (Ratpoints.rbaLength): the first numerator of the bit array is a₀ + 2 ^ k rbaLength i, computed before the loop over the words, that of word κ is that plus κ times the step 64 2 ^ k from one word to the next, and the step from one bit to the next is 2 ^ k. Each numerator goes to the test of a candidate (Ratpoints.Sieve.accepted, with the thunk checks of the third stage) and, if it passes, to the exact check, with the thunk w of the products, the degree d, the denominator b and the flags fl. This is the arm that a build of ratpoints with USE_LONG_IN_PHASE_2 compiles.

C: sift.c:1126-1134, sift.c:1137-1139, sift.c:1154-1159, sift.c:1172-1173

Deviation: the stride, the first numerator and the steps as natural numbers and integers, the powers 2 ^ k for the shifts 1L << k, RBA_LENGTH << k and LONG_LENGTH << k, the last two of which stay ints, while the first numerators of the words, the numerators of bits of the bit arrays of a height bound below 2 ^ 63, stay longs (Ratpoints.Sieve.NumClass.fitsLong_numerator); the words of the bit array read as entries of the vector, for EXT; natural numbers and integers for the longs; the delivery r passed and returned, for the pointers info and wk->quit and the count total of _ratpoints_sift0, and the flag quit tested after each walk through the set bits of a word, where the C code returns from _ratpoints_sift0 within the walk (Ratpoints.Sieve.walkWord); no counts under RP_PHASE_COUNTS and no stop after a phase (RP_STOP_AFTER).

Equations

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

def Ratpoints.Sieve.siftBitArrayWhole {σ : Type} (process : Int → Int → Int → σ → Answer σ) (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (checks : Thunk (List CheckSpec)) (cl : NumClass) (i : Int) (nums : Vector UInt64 rbaPack) (r : Delivery σ) (cnt : Counters) : Id (Delivery σ × Counters)

The arm of the second stage on the whole bit array, for the bit array that the first stage left nonzero with the word number i, from a copy nums of it, the points of its numerators delivered to the callback process on the delivery r: the second stage on the whole bit array (Ratpoints.Sieve.secondStage, with the moduli of specs, their reciprocals mgs and the test small), and, if it is still nonzero, the set bits of its words walked through in turn (Ratpoints.Sieve.walkWord), the first word from the first numerator of the bit array and each further word from the first numerator of the word before it plus the step from one word to the next, both computed when the second stage has left the bit array nonzero; it returns after a walk at which the callback has stopped the search. For the stride 2 ^ k and the residue a₀ of the class cl of the denominator (Ratpoints.Sieve.NumClass), bit t of word κ stands for the numerator a₀ + 2 ^ k (rbaLength i + 64 κ + t), for the number rbaLength of bits of a bit array (Ratpoints.rbaLength): the first numerator of word κ is a₀ + 2 ^ k rbaLength i + κ 64 2 ^ k, and the step from one bit to the next 2 ^ k. Each numerator goes to the test of a candidate (Ratpoints.Sieve.accepted, with the thunk checks of the third stage) and, if it passes, to the exact check, with the thunk w of the products, the degree d, the denominator b and the flags fl. This is the arm that the default build of ratpoints compiles.

C: sift.c:1204-1210, sift.c:1213-1226, sift.c:1257-1264, sift.c:1293-1296, rp-private.h:135-136, rp-private.h:177-178, rp-private.h:238-239, rp-private.h:264-266, rp-private.h:288-289

Deviation: the stride, the first numerator and the steps as natural numbers and integers, the powers 2 ^ k for the shifts 1L << k, RBA_LENGTH << k and LONG_LENGTH << k, the last two of which stay ints, while the first numerators of the words, the numerators of bits of the bit arrays of a height bound below 2 ^ 63, stay longs (Ratpoints.Sieve.NumClass.fitsLong_numerator); the words of the bit array read as entries of the vector, for EXT0 and EXT; natural numbers and integers for the longs; the delivery r passed and returned, for the pointers info and wk->quit and the count total of _ratpoints_sift0, and the flag quit tested after each walk through the set bits of a word and the rest of the bit array left at a stop, where the C code returns from _ratpoints_sift0 within the walk (Ratpoints.Sieve.walkWord); no counts under RP_PHASE_COUNTS and no stop after a phase (RP_STOP_AFTER).

Equations

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

def Ratpoints.Sieve.siftBitArray {σ : Type} (process : Int → Int → Int → σ → Answer σ) (useLong : Bool) (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (checks : Thunk (List CheckSpec)) (cl : NumClass) (i : Int) (nums : Vector UInt64 rbaPack) (r : Delivery σ) (cnt : Counters) : Id (Delivery σ × Counters)

One bit array that the first stage left nonzero, with the word number i, from a copy nums of it, the points of its numerators delivered to the callback process on the delivery r, in the arm of the second stage that useLong chooses (Ratpoints.useLongInPhase2 in the run): the second stage on the whole bit array and then the walks through its words for useLong = false (Ratpoints.Sieve.siftBitArrayWhole), and for useLong = true the second stage on each word that is not zero and the walk through it (Ratpoints.Sieve.siftBitArrayByWords), with the moduli of specs, their reciprocals mgs and the test small, the thunk w of the products, the degree d, the denominator b, the flags fl, the thunk checks of the third stage and the packing of the class cl of the denominator. Both arms walk through the set bits of the same words, the words of nums and-ed with the rows of all the moduli of specs, in the same order, and return after a walk at which the callback has stopped the search.

C: sift.c:1094-1111

Deviation: the arm chosen by the argument useLong, so that the guards run both in the same build, for the arm that the build compiles (#ifdef USE_LONG_IN_PHASE_2), each arm a function of its own; a function of its own for the body of the loop of the scan over one bit array; no counts under RP_PHASE_COUNTS, no stop after a phase (RP_STOP_AFTER), and no output under DEBUG.

Equations

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

def Ratpoints.Sieve.scanPiece {σ : Type} (process : Int → Int → Int → σ → Answer σ) (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) (specs : List SieveSpec) (mgs : List Nat) (small : Bool) (checks : Thunk (List CheckSpec)) (cl : NumClass) (w0 : Int) (n : Nat) (surv : Vector UInt64 ((n + 1) * rbaPack)) (r : Delivery σ) (cnt : Counters) : Id (Delivery σ × Counters)

The scan over a piece, the bit arrays with the word numbers w0, …, w0 + n - 1, which are the first n bit arrays of surv, and the second stage and the extraction of the points of their numerators: a sentinel, a bit array of ones, is written into bit array n, just past the piece; then from bit array 0 on, the bit arrays that are zero (Ratpoints.Sieve.isZeroAt) are stepped over, the scan stops at the sentinel, and each of the other bit arrays pos is copied and goes, with its word number w0 + pos, through the second stage with the moduli, rows and offsets of specs, their reciprocals mgs and the test small, and the extraction in the packing of the class cl (Ratpoints.Sieve.siftBitArray, in the arm Ratpoints.useLongInPhase2, with the thunk w of the products, the degree d, the denominator b, the flags fl and the thunk checks of the third stage), which delivers the points of its numerators to the callback process on the delivery r; the scan returns when the callback has stopped the search.

C: sift.c:1061-1082, sift.c:1088-1092, sift.c:1298-1299, rp-private.h:133, rp-private.h:205, rp-private.h:236, rp-private.h:262, rp-private.h:286

Deviation: indices for the pointers into the survivors, and a scan that holds its position as an index, where ratpoints recovers the word number from a pointer difference; the copy nums of the bit array a vector of Ratpoints.rbaPack words; the sentinel ~zero of every build as Ratpoints.rbaPack words ~~~0, written one at a time; natural numbers and integers for the longs; the counters cnt passed and returned, for the field n_arrays of the sieving thread, which counts one up for each bit array that is not zero (line 1092); the delivery r passed and returned, for the pointers info and wk->quit and the count total of _ratpoints_sift0, and the flag quit tested after each bit array, where the C code returns from _ratpoints_sift0 within the walk through the set bits of a word (Ratpoints.Sieve.walkWord).

Equations

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

def Ratpoints.Sieve.siftPiece {σ : Type} (process : Int → Int → Int → σ → Answer σ) (w : Thunk (List Int)) (d b : Nat) (fl : CheckFlags) (sp1 : Nat) (specs : List SieveSpec) (mgs : List Nat) (checks : Thunk (List CheckSpec)) (cl : NumClass) (w0 : Int) (n maskLow maskHigh : Nat) (r : Delivery σ) (cnt : Counters) : Id (Delivery σ × Counters)

One piece, the bit arrays with the word numbers w0, …, w0 + n - 1, and the points of its numerators: whether the reductions of the row indices modulo the moduli of the first two stages can multiply by the reciprocals, small, when the word numbers lie between -Ratpoints.rowBias and Ratpoints.rowBias - 2 Ratpoints.maxPrimeEven, so that the sum of a word number and an offset, the least multiple of the modulus of at least Ratpoints.rowBias (below Ratpoints.rowBias plus the modulus) plus less than the modulus, is not negative and below 2 Ratpoints.rowBias, at most Ratpoints.mulModLimit; a fresh array of n + 1 bit arrays, the last one the place of the sentinel; the first stage with the first sp1 moduli of specs, their rows and offsets, and their reciprocals in mgs, from the pattern of the class cl of the denominator, in the arm that the chunk Ratpoints.chunk chooses as the conditional compilation of the C code does: chunk bit arrays at a time for a chunk from 2 to 16 (Ratpoints.Sieve.andRowsChunked), and one row at a time otherwise (Ratpoints.Sieve.andRows), which leave the same bit arrays; the lowest maskLow bits of the first bit array cleared if maskLow ≠ 0 (Ratpoints.Sieve.clearLowBits), and the highest maskHigh bits of the last bit array of the piece, n - 1, if maskHigh ≠ 0 (Ratpoints.Sieve.clearHighBits); and the scan with the second stage, with the other moduli of specs and their reciprocals, and the extraction in the packing of cl (Ratpoints.Sieve.scanPiece, with the thunk w of the products, the degree d, the denominator b, the flags fl and the thunk checks of the third stage), which delivers the points to the callback process on the delivery r and returns when the callback stops the search. This is _ratpoints_sift0 of the C code, with the allocation of the survivors array that it works in.

C: find_points.c:3119-3121, sift.c:498-531, sift.c:548, sift.c:1030-1041, sift.c:1056-1058, sift.c:1300-1305, rp-private.h:575, rp-private.h:610-614

Deviation: the arm of the first stage chosen by a test on the constant Ratpoints.chunk, for the conditional compilation #if (RATPOINTS_CHUNK > 1) && (RATPOINTS_CHUNK <= 16) (sift.c:452, sift.c:575, sift.c:943), which compiles one arm only, and tail_leg with the chunked one; a fresh array of zeros for each piece, for the survivors array of the sieving thread, which every piece reuses, with one bit array more for the alignment, and whose words malloc leaves uninitialized; the piece by its first word number w0 and its number n of bit arrays, for w_low and w_high, and an index for the pointer to its last bit array; the moduli of the first two stages with their rows and offsets as the list specs and the end sp1 of the first stage, for the sieve specs sieves and the number sp1 that the sieving thread keeps, the reciprocals of their moduli as the list mgs, for the array magics of the arguments, and the thunk checks, for the table checks of the third stage and its length nchecks = sp3 - sp2; the class cl as a value, for the pointer cls; integers for the longs of the test small, which stay longs, and a Boolean for its int; the counters cnt passed and returned, for the field n_words of the sieving thread, which counts the n Ratpoints.rbaPack words of the piece (line 548), the product of UInt64s as the C code multiplies the unsigned long by RBA_PACK; the thunk w of the products of the check as an argument, where _ratpoints_check_point computes the products when the first survivor of b reaches it; the delivery r passed and returned, for the pointers info and wk->quit and the count total that _ratpoints_sift0 keeps from zero and returns, and its returns at a stop within the walk through the set bits of a word passed on by the scan (Ratpoints.Sieve.scanPiece); natural numbers and integers for the longs; no measurements of the phases (RP_TIC, RP_TOC, RP_PHASE_TIMING) and no stop after one of them (RP_STOP_AFTER).

Equations

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

One denominator

def Ratpoints.Sieve.numeratorsToBits (low high : Int64) (cl : NumClass) (split : Bool) : Int64 × Int64

The bits of the numerators low, …, high in the packing of the class cl, whose bit t stands for the numerator a₀ + 2 ^ k t (Ratpoints.Sieve.NumClass): from ⌈(low - a₀) / 2 ^ k⌉ = -⌊(a₀ - low) / 2 ^ k⌋ to ⌊(high - a₀) / 2 ^ k⌋, by arithmetic shifts. With split clear, as the shifts of the differences a₀ - low and high - a₀, which stay in the range of a long for |low|, |high| ≤ 2 ^ 63 - 65; with split set, each end split into its multiple of 2 ^ k, the end shifted right by k, and its rest, the end and-ed with the mask 2 ^ k - 1, from which a₀ is taken, so that nothing leaves the range of a long also for an end within 2 ^ k of its bounds. Both forms give the same bits where both stay in range.

C: find_points.c:3355-3370

Deviation: Int64 for the longs, in two's complement, the representation on which the and with the mask acts, also on a negative end, and >>> on Int64 the arithmetic shift, for the >> of a negative long, both of which the C standard leaves to the implementation (the representation before C23) and gcc defines so; the arithmetic of Int64 wrapping where that of the longs overflows, which the C standard leaves undefined: the differences of the plain form for an end within a₀ of -2 ^ 63, so beyond 2 ^ 63 - 65 in absolute value, where neither the C code nor Ratpoints.Sieve.sift takes the plain form; the stride k and the residue a₀ of the class converted to Int64; the two ends returned as a pair, for the pointers low and high through which the function reads and writes them; a Boolean for the int split, an argument: clear on the path of the forms of the ends (Ratpoints.Sieve.intervalBits), which exact_bounds gives an interval only for H ≤ 2 ^ 63 - 65, and on the path of the products in 128 bits (Ratpoints.Sieve.intervalBitsExact) set exactly for the heights above 2 ^ 63 - 65.

Equations

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

def Ratpoints.Sieve.intervalBitsExact (b : Int64) (bd : IntervalBounds) (height : Int64) (cl : NumClass) : Nat × Int64 × Int64

The bits of the numerators of the search interval with the bounds bd (Ratpoints.Sieve.IntervalBounds) at the denominator b, for the height bound height and the class cl, from the products of b and the ends in 128 bits (Ratpoints.Sieve.exactScale), as interval_bits_exact computes them for an interval that is not taken inline: ⌈b l⌉, which is -⌊b |l|⌋ for l < 0, clipped to -height, and the code 2 when it is beyond height for l ≥ 0, so that neither this interval nor a later one holds a numerator within the bound; then ⌊b u⌋, which is -⌈b |u|⌉ for u < 0, and the code 1 when it is below -height, so that this interval holds none, and otherwise clipped to height; and the code 0 with the bits of ⌈b l⌉, …, ⌊b u⌋ (Ratpoints.Sieve.numeratorsToBits), in the form that splits the ends for the heights above 2 ^ 63 - 65.

C: find_points.c:3381-3406

Deviation: the code and the bits returned as a triple, for the int and the pointers low and high through which the C code writes the bits, the bits (0, 0) with the codes 1 and 2, for which the C code writes nothing; Int64 for the longs, the unsigned long products compared with the height bound converted to a 64-bit word, as the C code compares them; no output under DEBUG.

Equations

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

def Ratpoints.Sieve.intervalBits (b : Int64) (bd : IntervalBounds) (height : Int64) (cl : NumClass) : Nat × Int64 × Int64

The bits of the numerators of the search interval with the bounds bd (Ratpoints.Sieve.IntervalBounds) at the denominator b, for the height bound height and the class cl, as interval_bits computes them: lo = ⌈b l⌉ and hi = ⌊b u⌋ from the forms of the ends, (b M + C) >> sh, by arithmetic shifts; the code 2 for lo > height; for hi < -height the code 1 if the interval is taken inline, and otherwise what the products in 128 bits give (Ratpoints.Sieve.intervalBitsExact), the forms of an interval that is not taken inline being those of an empty one; and otherwise the code 0 with the bits of lo, …, hi clipped to -height, …, height (Ratpoints.Sieve.numeratorsToBits, in the form that does not split the ends). The code 0 comes also for an interval that holds no numerator, when lo > hi.

C: find_points.c:3410-3434

Deviation: the code and the bits returned as a triple, for the int and the pointers low and high through which the C code writes the bits, the bits (0, 0) with the codes 1 and 2, for which the C code writes nothing; Int64 for the longs, and >>> on Int64 the arithmetic shift, for the >> of a negative long, which the C standard leaves to the implementation and gcc defines so; the arithmetic of Int64 wrapping where that of the longs overflows, which it does not here, by the bound of Ratpoints.Sieve.endForm on the forms of an interval taken inline and the forms of an empty one otherwise; no output under DEBUG.

Equations

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

def Ratpoints.Sieve.setRows (store : RowStore) (es : List SieveEntry) (bp : List Nat) (cl : NumClass) (offsets : Array Nat) : List SieveSpec × Bool

The moduli of the first two stages with their rows and offsets for the denominator at hand, as set_rows makes the sieve specs, and whether a row is missing: for the n-th sieve entry e of es, its modulus p, the offset of the row of the packing of the class cl for the n-th modulus, at the position n after the start cl.offset of that row in the array offsets (Ratpoints.Sieve.classOffsets), the row of the residue bp[n], the denominator divided by the stride of its class modulo p (Ratpoints.Sieve.fillBpList), from the table of rows of the entry in the store store (Ratpoints.Sieve.RowStore.row?), the empty array when it is not built yet, the start 0, which the chunked first stage sets before it reads it (Ratpoints.Sieve.chunkStarts), and the end p of the walk of the chunked first stage through the row; a row is missing when one of them is not built yet, and Ratpoints.Sieve.buildRows builds it.

C: find_points.c:3149-3170

Deviation: a list of the moduli with their rows and offsets, for the array of sieve specs ssp that set_rows fills; the empty array for the null pointer of a row not built yet; the start set to 0, where the C code leaves the field as it is until the first stage sets it; the end p also for a row not built yet, where the C code adds p to the null pointer; the row read plainly, for the acquire load that the flag shared chooses when threads share the tables of rows; the store of the tables of rows of the run as an argument, for the arrays sieve of the entries that the pointers in sieve_list reach; the array of the row offsets of the run as an argument, which the C code reaches through the pointer offset of the class, and a class without a row of offsets (none, for NULL), which the run never sifts, reads the offsets from position 0; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.buildRows (missing : Bool) (es : List SieveEntry) (bp : List Nat) (specs : List SieveSpec) (store : RowStore) : Id (List SieveSpec × RowStore)

The rows that are missing from the sieve specs specs of the first two stages, built, when missing says that one is (Ratpoints.Sieve.setRows): for each spec whose row is not built yet, of the n-th sieve entry e of es and the residue bp[n], the row of bp[n] from the table of rows of its entry, read again, and otherwise built into it by the builder of the entry (Ratpoints.Sieve.SieveEntry.fetchRow), and the end p of the walk of the chunked first stage through the row; the specs and the store with the rows built.

C: find_points.c:3522-3554

Deviation: the specs and the store of the tables of rows of the run passed and returned, for the array of the sieve specs and the arrays sieve of the entries; the empty array for the null pointer of a row not built yet; no lock of the tables (rp_tables_lock, rp_tables_unlock), and the pointer read again plainly, for the acquire load, both for the threads that share the tables of rows, which the model does not have; no measurement of the construction (RP_INIT_TIC, RP_INIT_TOC) and no output under DEBUG.

Equations

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

def Ratpoints.Sieve.siftBits {σ : Type} (process : Int → Int → Int → σ → Answer σ) (w : Thunk (List Int)) (d b A : Nat) (fl : CheckFlags) (sp1 : Nat) (specs : List SieveSpec) (mgs : List Nat) (checks : Thunk (List CheckSpec)) (cl : NumClass) (low high : Int) (r : Delivery σ) (cnt : Counters) : Id (Delivery σ × Counters)

The points of the numerators of the bits low, …, high of the class cl of the denominator b (Ratpoints.Sieve.numeratorsToBits), delivered to the callback process on the delivery r, in pieces of at most A bit arrays, for A ≥ 1 (for A = 0 the loop does not end), with the moduli of the first two stages, their rows and offsets in specs and their reciprocals in mgs, the first stage ending after sp1 of them, the thunk checks of the third stage, the thunk w of the products of the check, the degree d and the flags fl; none if high < low. Otherwise, for the number rbaLength of bits of a bit array (Ratpoints.rbaLength), the bit arrays have the word numbers from wLow = ⌊low / rbaLength⌋ to wHigh - 1, for wHigh = ⌊high / rbaLength⌋ + 1; and while w0 < wHigh, the piece of the word numbers w0, …, w1 - 1, for w1 = min (w0 + A) wHigh, gives its points (Ratpoints.Sieve.siftPiece), with the low mask low - rbaLength wLow if it is the first piece and the high mask rbaLength - 1 - (high mod rbaLength) if it is the last, so that the bits that the masks leave lie end to end and make up low, …, high; after each piece the loop returns if the callback has stopped the search.

C: find_points.c:3563-3612

Deviation: a function of its own for the bits of one interval of the numerators, the part of the loop over the intervals of sift after the set-up; the size A of the pieces as an argument, for args->array_size (line 3571), which sift reads through the pointer args of the sieving thread; natural numbers and integers for the longs, the word numbers and the masks by the division and the remainder, rounding down, by Ratpoints.rbaLength, for the shift by RBA_SHIFT and the mask by RBA_LENGTH - 1 (with Ratpoints.rbaLength = 2 ^ Ratpoints.rbaShift), which gcc makes the floor division and the Euclidean remainder on a negative long too, the first bits of the bit arrays staying longs for the bits of a height bound below 2 ^ 63 (Ratpoints.Sieve.neg_two_pow_le_rbaLength_mul_ediv, Ratpoints.Sieve.rbaLength_mul_ediv_add_one_le_two_pow); the delivery r passed and returned, for the pointers info and wk->quit and the count total that sift keeps from zero and returns, and the counters cnt passed and returned, for those of the sieving thread; no test of the flag stop of a thread of the pool after a piece (line 3610), which is null on the calling thread (line 5129, with the pool excluded with the threads), and no measurement (RP_SIFT_TOC) on the return at a stop.

Equations

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

def Ratpoints.Sieve.sift {σ : Type} (process : Int → Int → Int → σ → Answer σ) (c : List Int) (d H A b : Nat) (fl : CheckFlags) (sp1 : Nat) (es : List SieveEntry) (mgs bp : List Nat) (cl : NumClass) (offsets : Array Nat) (es3 : List SieveEntry) (mgs3 : List Nat) (iv : Array IntervalBounds) (store : RowStore) (r : Delivery σ) (cnt : Counters) : Id (Delivery σ × RowStore × Counters)

The points of the denominator b, for H < 2 ^ 63, its numerators in the search intervals with the bounds iv (Ratpoints.Sieve.exactBounds, increasing and disjoint), delivered to the callback process on the delivery r, in pieces of at most A bit arrays, for A ≥ 1, in the packing of its class cl (Ratpoints.Sieve.NumClass), and the store of the tables of rows with the rows built for it. What the third stage needs of the sieve entries es3 of its primes, with the reciprocals mgs3 of their moduli, for b and H (Ratpoints.Sieve.fillChecks) is a thunk, and so are the products w of the coefficients cₖ with the powers b^(d - k) (Ratpoints.BruteForce.scaledCoeffs), both forced when the first numerator of b needs them. For each interval in turn, the bits of its numerators ⌈b l⌉, …, ⌊b u⌋ within the height bound (Ratpoints.Sieve.intervalBits): the code 2 returns, since no later interval holds a numerator within the bound, and the code 1 goes on to the next interval; at the first interval with the code 0, also one without numerators, the sieve specs of the moduli of the first two stages are made, of the sieve entries es, the row of the residue bp[n] of b divided by the stride of the class modulo the n-th modulus from the table of rows of its entry in store, and the offset of the row of the class for that modulus in offsets (Ratpoints.Sieve.setRows), with the rows that are not built yet built into their tables of rows (Ratpoints.Sieve.buildRows); and then the points of the bits of the interval (Ratpoints.Sieve.siftBits, with the reciprocals mgs of the moduli of the first two stages, the first stage ending after sp1 of them, the degree d and the flags fl), which returns when the callback stops the search. With the one interval [-h, h] of a search without search intervals, for h ≥ H, the numerators are -H, …, H.

C: find_points.c:3112-3114, find_points.c:3123-3124, find_points.c:3129-3130, find_points.c:3435-3440, find_points.c:3442-3488, find_points.c:3490-3521, find_points.c:3555-3561, find_points.c:3613-3617, rp-private.h:574, rp-private.h:577-578, rp-private.h:583, rp-private.h:585

Deviation: the height bound converted to Int64, which is exact for H < 2 ^ 63, and the denominator too, and the bits back to integers; the bounds of the search intervals an array, for the struct rp_intervals with its pointers bd and end, which sift reaches through the field iv of the sieving thread, which worker_init clears (line 3130) and run_block sets for each block (line 3913; here Ratpoints.Sieve.runBlock, which passes the array of the run on); one call of Ratpoints.Sieve.setRows, for the two calls with the flag shared a constant, between which the pool of threads chooses, which the model does not have; the store of the tables of rows passed and returned, for the arrays sieve of the entries of the arguments, which sift reaches through sieve_list and which keep the rows built for the rest of the run; the end sp1 of the first stage, the entries es and the reciprocals mgs of the first two stages, the entries es3 of the third stage and their reciprocals mgs3 as arguments, for the numbers sp1, sp2 and sp3 that the sieving thread keeps (worker_init), the entries sieve_list[0], …, sieve_list[sp2 - 1], the array magics of the arguments, which _ratpoints_sift0 reads, and the entries sieve_list[sp2], …, sieve_list[sp3 - 1] and the reciprocals magics[sp2], …, magics[sp3 - 1], which fill_checks reads, the cut points of the decision of the block (Ratpoints.Sieve.runBlock); the residues bp and the class cl as values, for the pointers bp_list and cls, and the array offsets of the row offsets of the run as an argument, which the C code reaches through the pointer offset of the class; the thunk of Ratpoints.Sieve.fillChecks, for the table checks of the sieving thread, which fill_checks fills, and its flag stage3_filled, which sift clears; the thunk of the products w, for the flag compute_bc, which sift sets and _ratpoints_check_point clears when it computes the products; the counters cnt passed and returned, for those of the sieving thread, the count sifts one up at the start (line 3461); the delivery r passed and returned, for the pointers info and wk->quit, which worker_init clears, and the count total that sift keeps from zero and returns; the arguments of the run passed explicitly, for the pointer args of the sieving thread (rp-private.h:574), which worker_init sets and through which sift reads them; no pool, slot and stop flag of a thread of the pool, the flag by which the pool of threads tells it to abandon its block (pool, slot, stop, rp-private.h:584, excluded with the threads); natural numbers and integers for the longs; no measurements of the phases (RP_SIFT_TIC, RP_SETUP_TIC and their TOC) and no output under DEBUG.

Equations

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

Examples