The blocks of the run and the correction of the moduli

The loop over the denominators of find_points_work_1, in blocks, on the calling thread: the steps of the shape of the run (Ratpoints.Sieve.Shape), the k of the squares k ^ 2, the k of each divisor s of the divisor shape, one segment of steps per divisor, the words of 64 denominators, or the denominators themselves, are cut into blocks of consecutive steps of one length (Ratpoints.Sieve.Shape.segments, Ratpoints.Sieve.Shape.blockPlan), about Ratpoints.blocksWanted blocks of at least Ratpoints.blockMin steps, the steps of a block found from the segment that holds it (Ratpoints.Sieve.BlockPlan.steps); the loop of each shape goes over the steps of a block (Ratpoints.Sieve.Shape.blockLoop), its denominators in the order of the loop, each that passes the tests of the shape handed to a step, which sifts it (Ratpoints.Sieve.siftDen), and returns when the callback has stopped the search; each block is sifted as a whole, with the moduli of the decision of the correction of the moduli in force for it (Ratpoints.Sieve.findDecision), its counters from zero, and reports its counters and that decision (Ratpoints.Sieve.runBlock). The counters of the blocks are added to those of the run (Ratpoints.Sieve.RunCounts, Ratpoints.Sieve.runFold), from which the search corrects its choice of the end of the second stage and of the third stage once the run has swept enough words (Ratpoints.Sieve.adaptPrimes): a decision made at the fold of block j is for the blocks from j + Ratpoints.adaptLag + 1 on (Ratpoints.Sieve.Decision, Ratpoints.Sieve.Correction). The run sifts the blocks in turn, each folded after it, and returns the ends of the second and the third stage of the last block folded, which the search reports as used (Ratpoints.Sieve.sieveRun). The pool of threads that ratpoints may sieve the blocks with is not modelled: with it, the blocks are sifted apart and delivered in their order, and the decision of a block is the same, since it depends only on the folds of the blocks at least Ratpoints.adaptLag + 1 before it.

Main definitions

• Ratpoints.Sieve.Shape.segments, Ratpoints.Sieve.BlockPlan, Ratpoints.Sieve.blockLength, Ratpoints.Sieve.Shape.blockPlan, Ratpoints.Sieve.BlockPlan.steps: the segments of steps of the shape of the run, the length of the blocks, the first block of each segment, and the steps of a block.
• Ratpoints.Sieve.squaresBlock, Ratpoints.Sieve.squares1Block, Ratpoints.Sieve.wordsBlock, Ratpoints.Sieve.allBlock, with Ratpoints.Sieve.forbStarts, Ratpoints.Sieve.denWord and Ratpoints.Sieve.walkDens: the loops of the four shapes over the steps of a block, and their dispatch Ratpoints.Sieve.Shape.blockLoop.
• Ratpoints.Sieve.siftDen: one denominator of a block sifted.
• Ratpoints.Sieve.Decision, Ratpoints.Sieve.findDecision, Ratpoints.Sieve.BlockStat, Ratpoints.Sieve.runBlock: the decisions of the correction, the one in force for a block, and the sieve of one block with what it reports.
• Ratpoints.Sieve.adaptRates, Ratpoints.Sieve.adaptUp, Ratpoints.Sieve.adaptDown, Ratpoints.Sieve.adaptSecond, Ratpoints.Sieve.adaptThird, Ratpoints.Sieve.adaptPrimes: the correction of the end of the second stage and of the third stage from the counters of the run.
• Ratpoints.Sieve.RunCounts, Ratpoints.Sieve.Correction, Ratpoints.Sieve.RunCounts.fold, Ratpoints.Sieve.Correction.start, Ratpoints.Sieve.runFold: the counters of the run, the state of the correction, its start, and the fold of a block into them.
• Ratpoints.Sieve.sieveRun: the blocks of the run, sifted in turn, each folded after it, and the ends of the second and the third stage of the last block folded.

The blocks

def Ratpoints.Sieve.Shape.segments (s : Shape) (bLow bHigh : Nat) : Id (Array (Nat × Nat) × Nat)

The segments of steps of the shape s for the denominators bLow, …, bHigh, each from its first step lo to its last hi, both included, and the number of the steps of all of them: the k with bLow ≤ k ^ 2 ≤ bHigh for the squares, from ⌈√bLow⌉ to ⌊√bHigh⌋ (Ratpoints.Sieve.ceilSqrt, Ratpoints.Sieve.floorSqrt); for each divisor s of the divisor shape in turn, a segment of its own, the k with bLow ≤ s k ^ 2 ≤ bHigh, from ⌈√(⌊(bLow - 1) / s⌋ + 1)⌉ to ⌊√⌊bHigh / s⌋⌋; the words ⌊bLow / 64⌋ to ⌊bHigh / 64⌋ of 64 denominators for the word shape; and bLow, …, bHigh otherwise. A segment with hi < lo has no steps.

C: find_points.c:3812-3837

Deviation: the segments as an array of pairs, for the arrays seg_lo and seg_hi of the run; quotients by 64 for the shifts by LONG_SHIFT; natural numbers for the longs, the steps of a segment counted only when lo ≤ hi, as the C code counts them; the count of the segments read from the shape, for nseg, which run_setup counts before (line 3794).

Equations

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

structure Ratpoints.Sieve.BlockPlan : Type

The blocks of a run: its segments of steps, each from its first step to its last (Ratpoints.Sieve.Shape.segments), the length of the blocks (Ratpoints.Sieve.blockLength), and the first block of each segment, with the number of the blocks at the end (Ratpoints.Sieve.Shape.blockPlan): segment s holds the blocks from segBlock[s] to segBlock[s + 1] - 1, the last of them possibly shorter.

C: find_points.c:3750-3754

Deviation: the segments as an array of pairs, for the pointers seg_lo and seg_hi; the first blocks with the number of the blocks at the end of the array, for seg_block and nblocks, which the C code keeps apart with the same value; no count nseg of the segments, an array having its size; natural numbers for the longs.

• segs : Array (Nat × Nat)

  The segments, each from its first step to its last.

• len : Nat

  The length of the blocks, in steps.

• segBlock : Array Nat

  The first block of each segment, and at the end the number of the blocks.

def Ratpoints.Sieve.BlockPlan.nblocks (plan : BlockPlan) : Nat

The number of the blocks of the run.

Equations

• plan.nblocks = plan.segBlock.back!

def Ratpoints.Sieve.blockLength (steps : Nat) : Nat

The length of the blocks of a run of steps steps: steps / Ratpoints.blocksWanted + 1, at least Ratpoints.blockMin, and the fixed length of Ratpoints.blockLen when the build sets one.

C: find_points.c:3838-3842

Deviation: the conditional compilation #ifdef RP_BLOCK_LEN a constant of type Option Nat (Ratpoints.blockLen), none in the default build.

Equations

• Ratpoints.Sieve.blockLength steps = Ratpoints.blockLen.getD (if steps / Ratpoints.blocksWanted + 1 < Ratpoints.blockMin then Ratpoints.blockMin else steps / Ratpoints.blocksWanted + 1)

def Ratpoints.Sieve.Shape.blockPlan (s : Shape) (bLow bHigh : Nat) : Id BlockPlan

The blocks of the run of the shape s for the denominators bLow, …, bHigh: its segments (Ratpoints.Sieve.Shape.segments), the length of the blocks for the number of its steps (Ratpoints.Sieve.blockLength), and the first block of each segment, each segment with steps holding ⌊(hi - lo) / len⌋ + 1 blocks, with the number of the blocks at the end.

C: find_points.c:3843-3850

Deviation: the blocks returned as a structure (Ratpoints.Sieve.BlockPlan), for the fields of the run that run_setup fills; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.BlockPlan.steps (plan : BlockPlan) (i : Nat) : Id (Nat × Nat × Nat)

The steps of block i < plan.nblocks of the run with the blocks plan: the segment seg that holds it, the first with i < segBlock[seg + 1], and its first and last steps a and e, the block being the (i - segBlock[seg])-th of its segment, of len steps or up to the end of the segment.

C: find_points.c:3900-3904

Deviation: the segment and the steps returned, for the locals of run_block; natural numbers for the longs, the difference hi - a truncated at 0, where the C code compares a long that is not negative for a block of the run.

Equations

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

The loops of the shapes over a block

@[reducible, inline]

abbrev Ratpoints.Sieve.BlockState (σ : Type) : Type

What the loop over the denominators of a block carries from one denominator to the next: the delivery of the search (Ratpoints.Delivery), the store of the tables of rows (Ratpoints.Sieve.RowStore) and the counters of the block (Ratpoints.Sieve.Counters).

Equations

• Ratpoints.Sieve.BlockState σ = (Ratpoints.Delivery σ × Ratpoints.Sieve.RowStore × Ratpoints.Sieve.Counters)

def Ratpoints.Sieve.siftDen {σ : Type} (process : Int → Int → Int → σ → Answer σ) (c : List Int) (d H A : Nat) (fl : CheckFlags) (sp1 : Nat) (es : List SieveEntry) (mgs : List Nat) (es3 : List SieveEntry) (mgs3 : List Nat) (cls : Vector NumClass 64) (offsets : Array Nat) (iv : Array IntervalBounds) (b : Nat) (st : BlockState σ) : Id (BlockState σ)

One denominator b of a block, on the state st of the block: the residues of b divided by the stride of its class cls[b mod 64] modulo the moduli of the first two stages, the entries es with the reciprocals mgs (Ratpoints.Sieve.fillBpList), and its points (Ratpoints.Sieve.sift, with the entries es3 and the reciprocals mgs3 of the third stage, the row offsets offsets of the classes, the bounds iv of the search intervals, the height H, pieces of at most A bit arrays, the end sp1 of the first stage and the flags fl), delivered to the callback process.

C: find_points.c:3926-3927, find_points.c:3955-3956, find_points.c:4042-4043, find_points.c:4066-4067

Deviation: a function of its own for the two calls that each shape makes for a denominator, the residues a list for the array bp_list, which sift reads through its pointer; the state of the block passed and returned (Ratpoints.Sieve.BlockState), for the pointers info and wk->quit, the count total that run_block keeps, the arrays sieve of the entries and the counters of the sieving thread.

Equations

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

def Ratpoints.Sieve.squaresBlock {σ : Type} (step : Nat → BlockState σ → Id (BlockState σ)) (cls : Vector NumClass 64) (a e : Nat) (st : BlockState σ) : Id (BlockState σ)

The steps a, …, e of a block of the square shape, on the state st of the block: for each k, the denominator k ^ 2, sifted by step when the pattern of its class modulo 64 among the classes cls is not 0, after which the loop returns if the callback has stopped the search.

C: find_points.c:3919-3925, find_points.c:3928-3935

Deviation: the denominator sifted by the argument step, for the two calls of each shape (Ratpoints.Sieve.siftDen); the pattern of the class read as its one word, for EXT0(cl->bits); the state of the block passed and returned (Ratpoints.Sieve.BlockState); natural numbers for the longs, the denominators k ^ 2 being at most b_high and so longs for a long b_high (Ratpoints.Sieve.fitsLong_of_mem_squaresDens); no output under DEBUG.

Equations

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

def Ratpoints.Sieve.squares1Block {σ : Type} (step : Nat → BlockState σ → Id (BlockState σ)) (cls : Vector NumClass 64) (info : List Setup.DenInfo) (dv a e : Nat) (st : BlockState σ) : Id (BlockState σ)

The steps a, …, e of a block of the segment of the divisor dv of the divisor shape, on the state st of the block: for each k, the denominator dv k ^ 2, sifted by step when the pattern of its class modulo 64 among the classes cls is not 0 and it passes the valuation test with the primes info (Ratpoints.Sieve.denInfoTest), after which the loop returns if the callback has stopped the search.

C: find_points.c:3937-3943, find_points.c:3954, find_points.c:3957-3965

Deviation: the denominator sifted by the argument step, for the two calls of each shape (Ratpoints.Sieve.siftDen); the valuation test a function of its own; the pattern of the class read as its one word; the state of the block passed and returned (Ratpoints.Sieve.BlockState); natural numbers for the longs, the denominators dv k ^ 2 being at most b_high and so longs for a long b_high (Ratpoints.Sieve.fitsLong_of_mem_squares1Dens); no output under DEBUG.

Equations

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

def Ratpoints.Sieve.forbStarts (forb : Array ForbiddenEntry) (a : Nat) : Array Nat

The positions of the forbidden divisors forb tested with words at the first word a of a block: a mod p for each p, by a multiplication with the reciprocal of p (Ratpoints.Sieve.mulMod) when a ≤ Ratpoints.mulModLimit, and by the helper mod of the C code otherwise (Ratpoints.Sieve.modLong).

C: find_points.c:3981, find_points.c:3983-3988

Deviation: indices into the words of the divisors, for the pointers cur into the arrays from start to end; a Boolean for the int small; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.denWord (db : UInt64) (forb : Array ForbiddenEntry) (cur : Array Nat) (lo0 hi0 bLow bHigh w : Nat) : Id (UInt64 × Array Nat)

The word of the denominators 64 w + j of the word w that pass the class test and the forbidden divisors tested with words, with the positions cur of these divisors at w: the word db of the classes that admit a numerator (Ratpoints.Sieve.denBits), and-ed with the word at the position of each divisor of forb, whose position steps on by one, back to 0 at its prime p; in the first word lo0 of the run the bits below bLow mod 64 cleared, and in its last word hi0 those above bHigh mod 64. Returns the word and the positions at the next word.

C: find_points.c:3990, find_points.c:3993-4006

Deviation: indices into the words of the divisors, for the pointers cur, and the end of the words of a divisor its prime p, for the pointer end; the remainders by 64 for the masks by LONG_MASK; the positions returned with the word; natural numbers for the longs; no output under DEBUG.

Equations

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

def Ratpoints.Sieve.walkDens {σ : Type} (step : Nat → BlockState σ → Id (BlockState σ)) (test : Nat → Id Bool) (x : UInt64) (base : Nat) (st : BlockState σ) : Id (BlockState σ)

The set bits j of the word x of the denominators base + j, lowest first (Ratpoints.Sieve.ctz), on the state st of the block: each bit cleared, and its denominator sifted by step when it passes the tests test of the word shape (Ratpoints.Sieve.wordsTest), after which the walk returns if the callback has stopped the search.

C: find_points.c:4007-4009, find_points.c:4012, find_points.c:4044-4053

Deviation: the denominator sifted by the argument step, for the two calls of each shape (Ratpoints.Sieve.siftDen), and the tests of the word shape the argument test, for the code of Ratpoints.Sieve.wordsTest in the loop; the lowest set bit by the loop of RP_CTZL (Ratpoints.Sieve.ctz); the class of the denominator read by Ratpoints.Sieve.siftDen; the state of the block passed and returned (Ratpoints.Sieve.BlockState); natural numbers for the longs, the denominators base + j being at most b_high and so longs for a long b_high (Ratpoints.Sieve.fitsLong_of_mem_wordsDens); no output under DEBUG.

Equations

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

def Ratpoints.Sieve.wordsBlock {σ : Type} (step : Nat → BlockState σ → Id (BlockState σ)) (forb : Array ForbiddenEntry) (test : Nat → Id Bool) (db : UInt64) (lo0 hi0 bLow bHigh a e : Nat) (st : BlockState σ) : Id (BlockState σ)

The steps a, …, e of a block of the word shape, the words of 64 denominators, on the state st of the block: the positions of the forbidden divisors forb tested with words at the first word a (Ratpoints.Sieve.forbStarts); then for each word w, the word of its denominators that pass the class test and those divisors, with the masks of the first and the last word lo0 and hi0 of the run for the denominators bLow, …, bHigh (Ratpoints.Sieve.denWord, with the word db of the classes that admit a numerator), and the walk through its set bits, the denominators that pass the tests test sifted by step (Ratpoints.Sieve.walkDens), after which the loop returns if the callback has stopped the search.

C: find_points.c:3967-3980, find_points.c:3982, find_points.c:3989, find_points.c:3991-3992, find_points.c:4054-4058

Deviation: the denominator sifted by the argument step, for the two calls of each shape, and the tests of the word shape the argument test (Ratpoints.Sieve.wordsTest); the forbidden divisors an array, for the pointer run->forb_ba and their count nfb; the product 64 w for the shift by LONG_SHIFT; the state of the block passed and returned (Ratpoints.Sieve.BlockState); natural numbers for the longs, the products 64 w and the denominators being at most b_high and so longs for a long b_high (Ratpoints.Sieve.fitsLong_of_mem_wordsDens).

Equations

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

def Ratpoints.Sieve.allBlock {σ : Type} (step : Nat → BlockState σ → Id (BlockState σ)) (cls : Vector NumClass 64) (a e : Nat) (st : BlockState σ) : Id (BlockState σ)

The steps a, …, e of a block of the shape of every denominator, on the state st of the block: each denominator b, sifted by step when the pattern of its class modulo 64 among the classes cls is not 0, after which the loop returns if the callback has stopped the search.

C: find_points.c:4060-4065, find_points.c:4068-4074

Deviation: the denominator sifted by the argument step, for the two calls of each shape (Ratpoints.Sieve.siftDen); the pattern of the class read as its one word; the state of the block passed and returned (Ratpoints.Sieve.BlockState); natural numbers for the longs; no output under DEBUG.

Equations

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

def Ratpoints.Sieve.Shape.blockLoop {σ : Type} (shape : Shape) (step : Nat → BlockState σ → Id (BlockState σ)) (cls : Vector NumClass 64) (db : UInt64) (plan : BlockPlan) (seg a e bLow bHigh : Nat) (st : BlockState σ) : Id (BlockState σ)

The loop of the shape shape over the steps a, …, e of a block in the segment seg of the blocks plan, each denominator handed to the step step with the state st: the squares (Ratpoints.Sieve.squaresBlock), the divisors times squares with the divisor of the segment (Ratpoints.Sieve.squares1Block), the words of 64 denominators with the tests of Ratpoints.Sieve.wordsTest (Ratpoints.Sieve.wordsBlock), or every denominator (Ratpoints.Sieve.allBlock), with the classes cls, the word db of the classes that admit a numerator and the range bLow, …, bHigh of the denominators.

C: find_points.c:3917-3918, find_points.c:3936, find_points.c:3966, find_points.c:4059, find_points.c:4075-4076

Deviation: a function of its own for the switch of run_block over the shapes, the step an argument, for the two lines of each shape that sift a denominator (Ratpoints.Sieve.siftDen); the first and last words of the run, which the masks of the word shape compare with, read from the first segment of plan, as the C code reads seg_lo[0] and seg_hi[0]; natural numbers for the longs.

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.Sieve.Shape.squares.blockLoop step cls db plan seg a e bLow bHigh st = Ratpoints.Sieve.squaresBlock step cls a e st
• (Ratpoints.Sieve.Shape.squares1 info divisors).blockLoop step cls db plan seg a e bLow bHigh st = Ratpoints.Sieve.squares1Block step cls info divisors[seg]! a e st
• Ratpoints.Sieve.Shape.all.blockLoop step cls db plan seg a e bLow bHigh st = Ratpoints.Sieve.allBlock step cls a e st

One block

structure Ratpoints.Sieve.Decision : Type

A decision of the correction of the moduli: the first block block that it is for, and the ends sp2 and sp3 of the second and the third stage that the blocks from it on are sifted with, up to the next decision. The first is that of the choice, for block 0 (Ratpoints.Sieve.Correction.start).

It models no C code of its own: a structure for the entries of the arrays dec_block, dec_sp2 and dec_sp3 of the run (find_points.c:3761, Ratpoints.Sieve.Correction), with natural numbers for the longs.

• block : Nat

  The first block that the decision is for.

• sp2 : Nat

  The end of the second stage.

• sp3 : Nat

  The end of the third stage.

@[instance_reducible]

instance Ratpoints.Sieve.instInhabitedDecision : Inhabited Decision

Equations

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

def Ratpoints.Sieve.findDecision (decs : Array Decision) (i : Nat) : Id Nat

The decision in force for block i, among the decisions decs, whose first is for block 0: the last whose first block is at most i, found from the last decision back.

C: find_points.c:3908-3910, find_points.c:3912

Deviation: the decisions an array of structures (Ratpoints.Sieve.Decision), for the three arrays dec_block, dec_sp2 and dec_sp3 and their count ndec, which the C code reads with an acquire load, for the threads that publish their decisions (RP_ACQUIRE), here a plain read; the index returned, for the local d; natural numbers for the longs.

Equations

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

structure Ratpoints.Sieve.BlockStat : Type

What the sieve of one block reports to the fold of the run (Ratpoints.Sieve.runFold): its counters (Ratpoints.Sieve.Counters), the index dec of the decision that it was sifted with and the ends sp2 and sp3 of the second and the third stage of that decision.

C: find_points.c:4082-4086

Deviation: the counters as a structure, for the six fields; natural numbers for the longs.

• cnt : Counters

  The counters of the block.

• dec : Nat

  The index of the decision that the block was sifted with.

• sp2 : Nat

  The end of the second stage of that decision.

• sp3 : Nat

  The end of the third stage of that decision.

def Ratpoints.Sieve.runBlock {σ : Type} (process : Int → Int → Int → σ → Answer σ) (c : List Int) (d H A : Nat) (fl : CheckFlags) (sp1 : Nat) (entries : List SieveEntry) (magics : Array Nat) (cls : Vector NumClass 64) (offsets : Array Nat) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh : Nat) (plan : BlockPlan) (decs : Array Decision) (i : Nat) (store : RowStore) (r : Delivery σ) : Id (Delivery σ × RowStore × BlockStat)

Block i of the run with the blocks plan of the shape shape, for the polynomial of degree d with the coefficient list c, delivered to the callback process on the delivery r, with the store store of the tables of rows: its segment and its steps a, …, e (Ratpoints.Sieve.BlockPlan.steps), the decision in force for it among decs (Ratpoints.Sieve.findDecision), whose ends sp2 and sp3 cut the sieve entries entries and their reciprocals magics into the first two stages, the first ending at sp1, and the third stage; the counters from zero; and the loop of the shape over the steps (Ratpoints.Sieve.Shape.blockLoop, with the word db of the classes that admit a numerator and the range bLow, …, bHigh of the denominators), each denominator sifted by Ratpoints.Sieve.siftDen with the classes cls, the row offsets offsets, the bounds iv of the search intervals, the height H, pieces of at most A bit arrays and the flags fl. Returns the delivery, the store and the report of the block (Ratpoints.Sieve.BlockStat).

C: find_points.c:3127-3128, find_points.c:3889-3898, find_points.c:3911, find_points.c:3913-3915, find_points.c:4077-4078, find_points.c:4088-4093, rp-private.h:582

Deviation: the decision's entries and reciprocals cut as lists for each block, for the numbers sp2 and sp3 that the sieving thread keeps and through which sift and fill_bp_list read the arrays sieve_list and magics; the report returned with the delivery and the store, for the fields of the sieving thread that worker_stat copies into it after the block; the counters and the index of the decision, which worker_init clears before the run (lines 3127-3128), set only here, for each block (lines 3911 and 3914-3915), before they are read; the arguments of the run passed explicitly, for the fields of the run and of the arguments that run_block reads; the delivery r passed and returned, for the pointers info and wk->quit and the count total that run_block keeps from zero and returns; the array bp_list of sp3_max entries on the stack, of which fill_bp_list fills the first sp2, a list made by Ratpoints.Sieve.siftDen; natural numbers for the longs.

Equations

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

The correction of the moduli

structure Ratpoints.Sieve.RunCountsextends Ratpoints.Sieve.Counters : Type

The counters of the run, the sums of those of the blocks folded so far in the order of the blocks (Ratpoints.Sieve.RunCounts.fold), with the words swept when the counters of the second stage on were last restarted, words2, and the end sp2 of the second stage that those were counted under: they restart when a block sifted with another sp2 is folded.

C: find_points.c:1363-1367

Deviation: the six counters of the sieving thread extended (Ratpoints.Sieve.Counters), for the six fields; a UInt64 for the unsigned long n_words_2 and a natural number for the long sp2.

• words : UInt64
• arrays : UInt64
• bits : UInt64
• coprime : UInt64
• checks : UInt64
• sifts : UInt64
• words2 : UInt64

  n_words_2: the words swept when the counters of the second stage on last restarted.

• sp2 : Nat

  The end of the second stage that those counters were counted under.

def Ratpoints.Sieve.RunCounts.fold (c : RunCounts) (sp2 : Nat) (k : Counters) : RunCounts

The counters of the run c after the fold of a block that was sifted with the end sp2 of the second stage and counted k: when sp2 is not the end that the counters of the run were counted under, those of the second stage on (bits, coprime, checks, sifts) restart from zero, with the words swept so far as words2 and sp2 as the end; then the counters of the block are added.

C: find_points.c:4107-4113

Deviation: a function of its own for this part of run_fold; the end sp2 passed, for the entry dec_sp2[st->dec] that run_fold reads; the sums of UInt64s, wrapping as the unsigned longs do.

Equations

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

def Ratpoints.Sieve.adaptRates (es : Array SieveEntry) (c : RunCounts) (sp1 : Nat) : Id (Option (Float × Float × Float × Float))

The rates that the run has shown, from its counters c with the end c.sp2 of the second stage that they were counted under, the densities of the sieve entries es and the end sp1 of the first stage, or none when there is too little data: none unless the run swept words, sp1 ≥ 1, sp1 < c.sp2, the run counted Ratpoints.adaptArrays bit arrays that survived the first stage and Ratpoints.adaptBits numerators that survived the second, and words since the counters of the second stage restarted; and otherwise the survivors of the first stage per word s1, those of the second per word since the restart s2, the product r1 of the densities of the first stage and the product r2 of those of the first two, none unless r2 < r1 and s2 < s1.

C: find_points.c:1389, find_points.c:1400-1420

Deviation: a function of its own for this part of adapt_primes, its returns the result none; Floats for the doubles, in the order of the C code, the conversions of the UInt64 counters to Float as the C code converts the unsigned longs to doubles, and the words since the restart the difference of the UInt64s, wrapping, converted, as the C code computes it; the densities read from the entries, for sieve_list[n]->r; natural numbers for the longs, so that sp1 ≤ 0 is sp1 = 0.

Equations

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

def Ratpoints.Sieve.adaptUp (es : Array SieveEntry) (start : Nat) (level chance rate s costSurv ct U D : Float) : Id (Nat × Float × Float)

The walk of the correction up from the end start of the second stage: for each further sieve entry of es in turn, of the modulus p and the density r, the survivors per word next with it, level + chance rate r, and its cost (Ratpoints.primeCost with Ratpoints.costPhase2 s per word, the cost ct of a row and the estimates U and D of the run); the walk stops at the first entry whose survivors removed, s - next, times the cost costSurv of a survivor, are not above its cost, and otherwise takes it: rate times r, s the new survivors per word. Returns the new end of the second stage, the rate and the survivors per word.

C: find_points.c:1449-1457

Deviation: a function of its own for this loop of adapt_primes; the entries an array, for sieve_list up to sp3_max, its size; Floats for the doubles, in the order of the C code; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.adaptDown (es : Array SieveEntry) (sp1 sp2 : Nat) (level chance rate s costSurv ct U D : Float) : Id (Nat × Float)

The walk of the correction down from the end sp2 of the second stage, when it takes nothing more: for the entries of es below sp2 in turn, from the last down, while the position is above sp1 and the entry is a prime (its count nf of factors 0), the survivors per word prev without it, level + chance rate / r, and its cost (Ratpoints.primeCost with Ratpoints.costPhase2 prev per word); the walk stops at the first entry whose survivors removed, prev - s, times the cost costSurv of a survivor, are above its cost, and otherwise drops it: rate divided by r, s the survivors per word without it. Returns the new end of the second stage and the survivors per word.

C: find_points.c:1460-1472

Deviation: a function of its own for this loop of adapt_primes; the entries an array, for sieve_list; Floats for the doubles, in the order of the C code; natural numbers for the longs, n stepping down from sp2 - 1 while it is above sp1.

Equations

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

def Ratpoints.Sieve.adaptSecond (es : Array SieveEntry) (c : RunCounts) (sp1 : Nat) (level chance r2 checkRel ct U D : Float) : Id (Nat × Float)

The correction of the end of the second stage, from the counters c of the run with the end c.sp2 that they were counted under, the floor level and the slope chance of the survivors per word against the product of the densities, the product r2 of the densities of the first two stages, the cost checkRel of one exact check, the cost ct of a row and the estimates U and D of the run: the cost of a survivor, Ratpoints.costSurvivor plus the share of the survivors that reach the exact check times Ratpoints.costCheck (checkRel - 1); the walk up (Ratpoints.Sieve.adaptUp), and when it takes nothing, the walk down (Ratpoints.Sieve.adaptDown) from c.sp2, never below the end sp1 of the first stage. Returns the new end of the second stage and the survivors per word with it.

C: find_points.c:1439-1448, find_points.c:1458-1459, find_points.c:1473-1476

Deviation: a function of its own for this part of adapt_primes; Floats for the doubles, in the order of the C code; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.adaptThird (es : Array SieveEntry) (c : RunCounts) (sp2 : Nat) (q checkRel level chance r2 s : Float) : Id Nat

The correction of the third stage, which starts at the end sp2 of the second, for the value q of -Q, the cost checkRel of one exact check, the floor level and the slope chance of the survivors per word against the product of the densities, the product r2 of the densities of the first two stages and the survivors per word s with the new second stage: the costs of a prime of the stage per denominator, q when q ≥ 0 and Ratpoints.sp3PerDenom otherwise, and per survivor, Ratpoints.sp3PerSurvivor, each divided by checkRel; the survivors that a denominator brings to the stage, S, the share of the run's survivors that pass the test for common factors per denominator sifted, carried over to the new second stage by the ratio of s to the survivors per word with the old one, old = level + chance r2 (when old > 0); for the entries of es from sp2 on in turn, the stage stops at the first of density r with S (1 - perSurv - r) ≤ perDenom, and otherwise takes it, S times r. Returns the end of the third stage.

C: find_points.c:1487-1505

Deviation: a function of its own for this part of adapt_primes, the fields sp3_per_denom (its double read by its bits by the caller) and check_rel of the arguments that it reads and the local variables level, chance, r2 and s of adapt_primes passed as arguments; the end of the third stage returned, for the field sp3 of the arguments that it writes; Floats for the doubles, in the order of the C code; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.adaptPrimes (s : SieveOptions) (P : Params) (es : Array SieveEntry) (c : RunCounts) (sp2 sp3 : Nat) : Id (Nat × Nat × UInt64)

The correction of the choice of the moduli from the counters c of the run, with the options s (Ratpoints.SieveOptions), the result P of the choice (Ratpoints.Params: its end sp1 of the first stage, its estimates of the run and its cost of a check) and the sieve entries es, its reserve included, when the ends of the second and the third stage are sp2 and sp3, the latest decision: the next correction when twice the words swept so far have been swept, wrapping as the unsigned long does; nothing more when the rates of the run do not tell (Ratpoints.Sieve.adaptRates); otherwise the floor and the slope of the survivors per word, then with -A 2 or more the end of the second stage corrected (Ratpoints.Sieve.adaptSecond), and unless -P gives the third stage, when the run sifted denominators, the end of the third stage (Ratpoints.Sieve.adaptThird, with the value of -Q and the cost of a check), and otherwise the end of the third stage at least that of the second. Returns the ends of the second and the third stage and the words of the next correction.

C: find_points.c:1383-1388, find_points.c:1390-1398, find_points.c:1421-1438, find_points.c:1477-1486, find_points.c:1506-1509, find_points.c:1515

Deviation: the fields of the arguments that adapt_primes reads passed as the options, the result of the choice and the entries, and those that it writes, sp2, sp3 and adapt_at, returned; the doubles of the options by their bits; Floats for the doubles, in the order of the C code; integers for the longs adapt and sp3_extra and natural numbers for the others; no output under RP_PRIME_STATS.

Equations

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

structure Ratpoints.Sieve.Correction : Type

The state of the correction of the moduli during the run: the counters of the run (Ratpoints.Sieve.RunCounts), the number of the blocks folded, the decisions made (Ratpoints.Sieve.Decision), the ends of the second and the third stage of the last block folded, and the latest decision of the correction with the words of the next one, which the C code keeps in the arguments.

C: find_points.c:3755-3762

Deviation: the decisions an array of structures, for the three arrays dec_block, dec_sp2 and dec_sp3 and their count ndec; the fields sp2, sp3 and adapt_at of the arguments, which adapt_primes writes and run_fold reads, kept here, since they are read only within the run, by run_fold and adapt_primes, after which line 5163 overwrites sp2 and sp3 with the ends of the last block folded; natural numbers for the longs and a UInt64 for the unsigned long.

• cnt : RunCounts

  The counters of the run.

• folded : Nat

  nfolded: the number of the blocks folded.

• decisions : Array Decision

  The decisions, the first for block 0.

• lastSp2 : Nat

  last_sp2: the end of the second stage of the last block folded.

• lastSp3 : Nat

  last_sp3: the end of the third stage of the last block folded.

• sp2 : Nat

  args->sp2: the end of the second stage of the latest decision.

• sp3 : Nat

  args->sp3: the end of the third stage of the latest decision.

• adaptAt : UInt64

  args->adapt_at: the words swept at which the next correction is made.

def Ratpoints.Sieve.Correction.start (sp2 sp3 : Nat) (adaptAt : UInt64) : Correction

The correction at the start of the run, for the ends sp2 and sp3 of the second and the third stage of the choice and the words adaptAt of the first correction: nothing counted, the counters of the second stage on counted under sp2, no block folded, one decision, that of the choice for block 0, and the ends of the choice as those of the last block folded.

C: find_points.c:3853-3856, find_points.c:3861-3863

Deviation: the state returned, for the fields of the run that run_setup sets.

Equations

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

def Ratpoints.Sieve.runFold (s : SieveOptions) (P : Params) (es : Array SieveEntry) (st : Correction) (b : BlockStat) : Id Correction

The fold of the next block of the run, with the report b (Ratpoints.Sieve.BlockStat), into the state st of the correction, with the options s, the result P of the choice and the sieve entries es: the block is the j-th folded; its counters added to those of the run (Ratpoints.Sieve.RunCounts.fold, with the end of the second stage of its decision); its ends as those of the last block folded; and when the run has swept the words of the next correction, the correction (Ratpoints.Sieve.adaptPrimes), whose result, when it changes an end, is a decision for the blocks from j + Ratpoints.adaptLag + 1 on.

C: find_points.c:4102-4106, find_points.c:4114-4127

Deviation: the state of the correction passed and returned (Ratpoints.Sieve.Correction), for the fields of the run and of the arguments; the decision appended to the array, for the store into the three arrays and the release store of their count (RP_PUBLISH), for the threads that read them, here a plain store; natural numbers for the longs.

Equations

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

The run

def Ratpoints.Sieve.sieveRun {σ : Type} (process : Int → Int → Int → σ → Answer σ) (c : List Int) (d H A : Nat) (fl : CheckFlags) (s : SieveOptions) (P : Params) (entries : List SieveEntry) (magics : Array Nat) (cls : Vector NumClass 64) (offsets : Array Nat) (db : UInt64) (shape : Shape) (iv : Array IntervalBounds) (bLow bHigh : Nat) (store : RowStore) (r : Delivery σ) : Id (Delivery σ × Nat × Nat)

The points of the denominators from bLow to bHigh of the shape shape, for the polynomial of degree d with the coefficient list c, delivered to the callback process on the delivery r, whose flag quit is clear, with the sieve entries entries of the moduli, the reserve of the correction included, and the reciprocals magics of their moduli in their order, as the result P of the choice (Ratpoints.sievingInfo) gives them for the options s: the blocks of the run (Ratpoints.Sieve.Shape.blockPlan); the correction from the choice (Ratpoints.Sieve.Correction.start, with the ends P.sp2 and P.sp3 and the words P.adaptAt); then for each block in turn its points (Ratpoints.Sieve.runBlock, with the decision in force for it, the end P.sp1 of the first stage, the classes cls with their row offsets offsets, the word db of the classes that admit a numerator, the bounds iv of the search intervals and pieces of at most A bit arrays), the rows that it builds into the store store going on to the next block, and the fold of its report (Ratpoints.Sieve.runFold), after which the run returns if the callback has stopped the search. Returns the delivery and the ends of the second and the third stage of the last block folded, which the search reports as used.

C: find_points.c:5120, find_points.c:5152-5160, find_points.c:5163

Deviation: the blocks on the calling thread alone, without the pool of threads, which sifts them apart and delivers them in the same order, the decision of each block depending only on the folds of the blocks at least Ratpoints.adaptLag + 1 before it (excluded with the threads); the ends of the last block returned, for the fields sp2 and sp3 of the arguments that line 5163 writes; the store of the tables of rows passed from one block to the next, for the arrays sieve of the entries of the arguments, its last state not returned, as nothing reads the tables of rows after the run; the delivery r passed and returned, for the pointers info and wk.quit and the count total; natural numbers for the longs.

Equations

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

Examples

The blocks, the decision in force, the fold of the counters, the correction and the denominators that the blocks visit against their rule; the shape and the denominators that the run sifts 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 dump); and the blocks and the run of the divisor shape against the points that ratpoints prints.