The search for the points

Ratpoints.findPointsWith c H s o process info is the model of the library function find_points of ratpoints, with the options s of the sieve (Ratpoints.SieveOptions), the options o of the library that change the refusals, the order of the output or what is delivered (Ratpoints.Options), the callback process of the caller and its data info: it refuses, as the program does (Ratpoints.Refusal), more than Ratpoints.maxDegree + 1 coefficients, fewer than two, the height bound 0 and the heights that are not longs, and then the binary forms that are not squarefree as the set-up of the library finds them: when the leading zeros of the n + 1 coefficients lower ⌈n / 2⌉, in the reversal check (Ratpoints.Setup.reversal), which may also reverse the polynomial, and with the Sturm step on, by the remainder chain (Ratpoints.Sturm.chain); between the last two it refuses malformed search intervals (Ratpoints.searchIntervals). The options are normalized first (Ratpoints.Options.normalize), the search intervals are [-h, h] when none are given, and the Sturm step (Ratpoints.sturmRegion, Ratpoints.Sturm.computeSturm) narrows them to the intervals that it keeps, where the polynomial may be ≥ 0, or returns at once when it keeps no part of them, so that the polynomial is negative on them within ±2 ^ 63, and there is no point at infinity (at the depth of the step it may also keep intervals on which the polynomial is negative). Otherwise it runs the search of the polynomial that the set-up hands on (Ratpoints.searchPoints), which delivers no points when no class of the denominators modulo 64 admits a numerator and there is no point at infinity, or when the curve has none modulo one of the primes looked at by the choice of the moduli, and otherwise the points of height at most H on y ^ 2 = F(x, z) in the search region (the denominators in the range of the options and x / z in a search interval) to the callback (Ratpoints.Delivery), the points at infinity first and then, unless the Sturm step has left no interval, those of the denominators in the order of the loop of the search (Ratpoints.Sieve.Shape), increasing unless it runs over the divisors of the leading coefficient, found by the sieve on the bit arrays of words with the moduli, primes, prime powers and products of them, that the search chooses from the curve as find_points does (Ratpoints.sievingInfo) and corrects between the blocks of the run (Ratpoints.Sieve.sieveRun), and the array size of s, each mapped back to the caller's curve after a reversal, until a call of the callback stops the search, and returns the data of the callback, the count, the sum of the values that the calls returned, the bits of the flags that the program reads after the search, the search intervals as the search leaves them and the numbers of the moduli used (Ratpoints.Outcome). Under the options of the output it delivers only the points with y ≥ 0 (RATPOINTS_NO_Y), or, each with y = 0, the candidate at infinity and every numerator that passes the sieve, the test for common factors and the third stage (RATPOINTS_NO_CHECK). Under the bit RATPOINTS_VERBOSE of the flags the library prints a report of the search (Ratpoints.Report) on the standard output, between the points that the callback of the program prints there: Ratpoints.findPointsVerbose c H s o process info print is the search with a print channel print, through which it prints the report into the data of the callback where the C code prints it, and which returns the data also with a refusal, since the report may come before it; Ratpoints.findPointsWith is that search with the refusal alone, and with the print channel that prints nothing by default. Ratpoints.findPoints c H s o is the list of what it delivers, by the callback that appends each point to an array (Ratpoints.appendPoint).

Main definitions

• Ratpoints.Options, Ratpoints.Options.normalize: the options of a search, and as the search normalizes them.
• Ratpoints.Outcome: what a search returns and writes back.
• Ratpoints.searchIntervals, Ratpoints.sturmRegion: the search intervals of a search, the default one or the caller's checked, and the Sturm step on them.
• Ratpoints.sieving, Ratpoints.chooseAndSearch, Ratpoints.searchPoints: the sieving of a search, the choice of the moduli with the search after it, and the search of the polynomial that the set-up hands on.
• Ratpoints.findPointsWork, Ratpoints.findPointsVerbose: the search after the test of the leading zeros, and the search with a callback and the print channel.
• Ratpoints.findPointsWith: the search with a callback.
• Ratpoints.findPoints: the points, as a list.

structure Ratpoints.Options : Type

The options of a search that change the refusals, the order of the output or what is delivered, with the defaults of a run of the program without options: whether the set-up may reverse the polynomial (Ratpoints.Setup.reversal), the depth of the Sturm step, negative for none, the two options of the output, whether the numerators that pass the sieve are delivered without the exact check (RATPOINTS_NO_CHECK) and whether only the point with y ≥ 0 of a pair is delivered (RATPOINTS_NO_Y), and the search region: the search intervals and the range of the denominators. Unlike the options of the sieve (Ratpoints.SieveOptions), which change neither the points nor their order, these change the order of the output (the reversal, and the range of the denominators, which also decides the shape of the divisors), the refusals (the Sturm step, the search intervals, and without the Sturm step the reversal check), what is delivered (the options of the output and the search region; under the first of the output, the reversal, the options of the sieve and the Sturm step change it too), and with its intervals what the search writes back (Ratpoints.Outcome).

C: main.c:348, main.c:352, ratpoints.h:359, ratpoints.h:363-364, ratpoints.h:369, ratpoints.h:403-405

Deviation: a structure for the fields of ratpoints_args that hold these options: Booleans for the bits RATPOINTS_NO_CHECK, RATPOINTS_NO_Y and RATPOINTS_NO_REVERSE of the flags, noCheck and noY true when their bits are set, reverse true when RATPOINTS_NO_REVERSE is clear, so that all three defaults are those of the cleared flags (main.c, line 352); of the other bits of the flags, which main.c clears with these, the Jacobi switch is that of the options of the sieve (Ratpoints.SieveOptions.jacobi), and RATPOINTS_VERBOSE is the print channel of the search (Ratpoints.findPointsVerbose), which the program makes from Ratpoints.Cli.Output.verbose; an integer for args->sturm; a list of pairs of doubles (Ratpoints.Double) for the array domain of the type ratpoints_interval with the number num_inter of its intervals, the empty list for num_inter = 0, so that no number of intervals is negative and the room in the array for the intervals of the Sturm step is no concern of the caller; integers for the longs b_low and b_high; of the fields that share their lines in ratpoints.h, sp1, sp2, num_primes and max_forbidden are read by the options of the sieve (Ratpoints.SieveOptions), and sp3 is the end of the third stage of the choice (Ratpoints.Params.sp3), corrected during the run (Ratpoints.Sieve.Correction).

• reverse : Bool

  Whether the set-up may reverse the polynomial: the bit RATPOINTS_NO_REVERSE of the flags clear, which the option -k of the program sets and -K clears.

• sturm : Int

  args->sturm, the depth of the Sturm step, negative for none: Ratpoints.defaultSturm unless the option -s of the program sets -1 or -S a depth; a depth above Ratpoints.Double.mantDig + 2 = 55 is taken as 55 (Ratpoints.Options.normalize).

• noCheck : Bool

  The bit RATPOINTS_NO_CHECK of the flags, which the option -x of the program sets and -X clears: every numerator that passes the sieve is delivered, with y = 0, without the exact check.

• noY : Bool

  The bit RATPOINTS_NO_Y of the flags, which the option -y of the program sets and -Y clears: of a pair of points (x : ±y : z) only the one with y ≥ 0 is delivered.

• domain : List (Double × Double)

  args->domain with args->num_inter, the search intervals [l, u] of the caller, which the options -l and -u of the program give, and [] for none, the whole line: they must have l ≤ u, be increasing and strictly apart and have no NaN end, and may have infinite ends.

• bLow : Int

  args->b_low, the least denominator, which the option -dl of the program gives; values below 1 stand for 1.

• bHigh : Int

  args->b_high, the largest denominator, which the option -du of the program gives; values below 1 and above the height bound stand for the height bound.

def Ratpoints.Options.normalize (o : Options) (H : Nat) : Options

The options o as find_points_work_1 normalizes the fields of the arguments that hold them, for the height bound H ≥ 1: the least denominator 1 for one below 1, the largest denominator H for one below 1 or above H, the depth of the Sturm step capped at Ratpoints.Double.mantDig + 2 = 55, beyond which the ends of the intervals that the step keeps would not all be doubles, and the switch of the reversal off (RATPOINTS_NO_REVERSE_AUTO) when the caller gives search intervals or the range of the denominators is not 1, …, H.

C: find_points.c:4640-4641, find_points.c:4659-4661, find_points.c:4678-4689, ratpoints.h:421-424

Deviation: the normalized options returned, for the fields of the arguments that the C code normalizes in place and restores in find_points_work (lines 4542-4545 and 4560-4563), which the caller does not see either; no clamp of the number of the search intervals, which a list cannot make negative; the bit RATPOINTS_NO_REVERSE_AUTO, which the C code sets in the flags and the reversal check tests with RATPOINTS_NO_REVERSE (line 4739), as the switch reverse cleared; integers for the longs.

Equations

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

structure Ratpoints.Outcome (σ : Type) : Type

What a search gives its caller, find_points with the callback process and its data info: the data info that the callback leaves, the count total of the search, the sum of the values that the calls of the callback returned, which find_points returns, and the bits of the flags of the arguments that the search writes back and the program ratpoints reads after it (its message 7): RATPOINTS_REVERSED, set when the reversal check has reversed the polynomial, RATPOINTS_USE_SQUARES, set for odd degree and |c_d| = 1, when the denominators are the squares, and RATPOINTS_USE_SQUARES1, set for odd degree otherwise when the divisor set-up has succeeded (Ratpoints.Setup.setupUs1), when the denominators are divisors of c_d times squares; the search sets the last two before its exits after the Sturm step and before the points at infinity, and the return after the Sturm step (find_points.c:4889) comes only for an even degree, where neither is set, so that they are written back on every path that does not refuse the input; and the search intervals as the search leaves them, which the program prints after the search (its message 8): [-h, h] when the caller gives none (Ratpoints.searchIntervals), narrowed by the Sturm step to the intervals it leaves, in the coordinates of the polynomial searched (Ratpoints.sturmRegion), and none when it leaves none; and the numbers of the moduli used, which the program prints after the search (its message 4): those of the first stage, of the first two and of all three stages, as the last block of the run was sifted with them (Ratpoints.Sieve.sieveRun), and 0 for each when the search returns before the sieve.

C: ratpoints.h:377-383, ratpoints.h:414, ratpoints.h:416-417

Deviation: a structure for what the C code returns and writes back into the arguments: the data of the callback, which the caller has behind its pointer info, the count, which find_points returns as a long that also carries its error codes (Ratpoints.findPointsWith returns the refusals apart), Booleans for three bits of args->flags, and the search intervals as a list, for the array args->domain and the number args->num_inter that the search writes back and the program reads after it; nothing else written back: neither the reversed coefficients and the degree (args->cof, args->degree), which nothing reads after the search; nor the other internal bits of the flags, RATPOINTS_CHECK_DENOM, RATPOINTS_USE_JACOBI and RATPOINTS_NO_REVERSE_AUTO, which the program does not read either, the bits of the input coming back as the caller set them (find_points.c:4606), which the program takes from its own options and settings (Ratpoints.Options, Ratpoints.SieveOptions.jacobi, Ratpoints.Cli.Output.verbose); nor args->sp3, which find_points_work zeroes on entry (line 4551) and leaves as the search leaves it, unlike sp2, which it restores (line 4561): the end of the third stage of the last block sifted (line 5163), that of the choice after the returns between the choice and the sieve, where sp3_used stays 0, and 0 after the returns before the choice and after the exits of the choice when the curve has no points modulo a prime (find_points.c:2614, find_points.c:2998), which come before line 3017 sets it; nor the private fields that sieving_info and adapt_primes write, adapt_at, run_words, run_denoms, sp3_max and check_rel, which nothing reads before sieving_info sets them again in the next search; natural numbers for the longs sp1_used, sp2_used and sp3_used.

• info : σ

  The data of the callback after the search.

• total : Int

  The count, the sum of the values that the calls of the callback returned.

• reversed : Bool

  RATPOINTS_REVERSED: the reversal check has reversed the polynomial.

• useSquares : Bool

  RATPOINTS_USE_SQUARES: the denominators are the squares.

• useSquares1 : Bool

  RATPOINTS_USE_SQUARES1: the denominators are divisors of c_d times squares.

• domain : List (Double × Double)

  args->domain with args->num_inter: the search intervals as the search leaves them.

• sp1Used : Nat

  sp1_used: the moduli used in the first stage.

• sp2Used : Nat

  sp2_used: the moduli used in the first two stages.

• sp3Used : Nat

  sp3_used: the moduli used in the three stages.

def Ratpoints.searchIntervals (H : Nat) (domain : List (Double × Double)) : Id (Option (List (Double × Double)))

The search intervals of a search for the height bound H ≥ 1 and the intervals domain of the caller, as find_points_work_1 deals with them, or none for intervals that it refuses (RATPOINTS_BAD_ARGS): for none given, the default interval [-h, h], h the double of H (Ratpoints.Double.ofInt64), moved up to the next double (Ratpoints.Double.nextUp) when it is below 2 ^ 63 and below H, so that it holds every x = a / b of the search; otherwise the intervals given, refused when an interval has not l ≤ u or does not begin above the end of the one before it, the comparisons of doubles (Ratpoints.Double.le, Ratpoints.Double.lt), so that a NaN end is refused too.

C: find_points.c:4829, find_points.c:4831-4855

Deviation: the intervals returned as a list, for the array domain and the number num_inter of the arguments, which the C code sets to the default interval in place; none for the code RATPOINTS_BAD_ARGS that the C code returns (Ratpoints.Refusal.badArgs); the test of a null pointer domain (line 4830) excluded, the interface of the library; natural numbers for the long index.

Equations

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

def Ratpoints.sturmRegion (c : List Int) (d : Nat) (sturm : Int) (dom : List (Double × Double)) : Id (Except Refusal (Option (List (Double × Double) × Bool)))

The Sturm step of find_points_work_1 on the polynomial f with the coefficient list c of degree d that the reversal check hands on, with the depth sturm, for the search intervals dom (Ratpoints.searchIntervals): with the step off, sturm < 0, the intervals as they are; with it on, the refusal Ratpoints.Refusal.notSquarefree when the remainder chain of f is none (Ratpoints.Sturm.computeSturm), and otherwise the intervals that the step leaves, when there are some; when there are none, f negative on them within ±2 ^ 63, none for an even d whose leading coefficient is not a square (Ratpoints.Setup.isSquare), when there is no point at infinity either, so that the search returns at once, and otherwise no intervals with the flag sturm_empty set, so that the search delivers the points at infinity only.

C: find_points.c:4857-4859, find_points.c:4862-4863, find_points.c:4879-4892

Deviation: the result as a refusal, none, or the intervals with the flag sturm_empty, for the codes that the C code returns at lines 4879 and 4889, the intervals that it leaves in domain with their number num_inter, and its local flag sturm_empty; the square test lcfsq made on the polynomial searched (Ratpoints.Setup.isSquare), where the C code computes it before the reversal check (line 4634) and clears it in case 2 (line 4770): the same value for an even degree, the only one that reads it; no failure for lack of memory (RATPOINTS_NO_MEMORY), which the model cannot meet; the report under RATPOINTS_VERBOSE printed by the caller from the result (Ratpoints.Report.sturmStep).

Equations

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

def Ratpoints.sieving {σ : Type} (process : Int → Int → Int → σ → Answer σ) (c : List Int) (d H : Nat) (s : SieveOptions) (P : Params) (fl : CheckFlags) (useSquares : Bool) (us1 : Option (List Setup.DenInfo × List Nat)) (checkDenom useJacobi : Bool) (forb : List Sieve.ForbiddenEntry) (forbVal : List Sieve.ForbiddenVal) (entries : List Sieve.SieveEntry) (magics : Array Nat) (cls : Vector Sieve.NumClass 64) (db : UInt64) (store : Sieve.RowStore) (bLow bHigh : Nat) (domain : List (Double × Double)) (r : Delivery σ) : Id (Delivery σ × Nat × Nat)

The sieving of the search of the polynomial with the coefficient list c of degree d, for the height H, the options s, the result P of the choice of the moduli and the flags fl, delivered to the callback process on the delivery r, whose flag quit is clear, with the sieve entries entries of the moduli and their reciprocals magics, the classes cls of the denominators modulo 64 with the word db of those that admit a numerator, and the store store of the tables of rows, from the choice (Ratpoints.sievingInfo): an array of Ratpoints.Sieve.numPackings rows of one offset for each sieve entry, and the row offsets of the classes in it, with the inverses of the strides in the entries (Ratpoints.Sieve.classOffsets); the shape of the run and the bounds of the search intervals domain (Ratpoints.Sieve.runSetup, with the flags of the denominators useSquares, us1, checkDenom and useJacobi, the forbidden divisors forb and forbVal and the largest denominator bHigh); and the points of the denominators bLow, …, bHigh of the shape in the search intervals (Ratpoints.Sieve.sieveRun), in blocks, with the cut points of the choice P as the first decision, the options s, which the correction reads, and pieces of at most Ratpoints.Params.arraySizeAt P H bit arrays, which returns when the callback stops the search, with the ends of the second and the third stage of its last block. This is the block that the C code introduces as "now do the sieving".

C: find_points.c:4573, find_points.c:5116, find_points.c:5119, find_points.c:5132, find_points.c:5137-5139, find_points.c:5167

Deviation: a function of its own for the block of the sieving in find_points_work_1; the range of the denominators and the search intervals as arguments, for the fields b_low, b_high, domain and num_inter of the arguments that run_setup and the run read; the flags of the denominators as Booleans and an option, for the bits of args->flags and the arrays args->den_info and args->divisors that run_setup reads; the array of the row offsets made with zeros, for the array on the stack, whose entries the C code leaves unset until class_offsets writes them, with one offset in each row for each of the sp3_max sieve entries of the run, the reserve of the correction included; the delivery passed and returned, for the pointers info and wk.quit and the count total, and the ends of the second and the third stage of the last block returned with it, for the fields sp2 and sp3 of the arguments that the run writes; no sieving thread made (worker_init, worker_clear), whose fields the components that the run calls take as arguments, and no pool of threads (excluded with the threads); no failure for lack of memory, which the model cannot meet.

Equations

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

def Ratpoints.chooseAndSearch {σ : Type} (process : Int → Int → Int → σ → Answer σ) (c : List Int) (d : Nat) (s : SieveOptions) (mayExtend : Bool) (fl : CheckFlags) (us1 : Option (List Setup.DenInfo × List Nat)) (a : ShapeArgs) (bpw : Float) (sturmEmpty : Bool) (print : String → σ → σ) (r : Delivery σ) : Id (Delivery σ × Nat × Nat × Nat)

The choice of the moduli and the search after it, for the polynomial with the coefficient list c of degree d that the set-up hands on, the normalized options s of the sieve, whether the caller left the number of primes to the library (mayExtend), the flags fl, the divisor set-up us1 (Ratpoints.Setup.setupUs1), the shape a of the run (Ratpoints.ShapeArgs: the height bound, the flags of the denominators, the range of the denominators, the search intervals that the Sturm step leaves and the classes of the denominators modulo 64), the mean bits per word bpw of its bit arrays and the flag sturmEmpty of the Sturm step, delivered to the callback process on the delivery r, whose flag quit is clear, with the print channel print: the choice of the moduli from the curve (Ratpoints.sievingInfo), with the flag of the longs (Ratpoints.Setup.useCLong), and nothing delivered when the curve has no points modulo one of the primes looked at, after the message of the exit (Ratpoints.Report.noPoints); the report of the choice and of its moduli (Ratpoints.Report.choice, Ratpoints.Report.moduli); the points at infinity (Ratpoints.Sieve.pointsAtInfinity), after the line before them when there are some (Ratpoints.Report.atInfinity), after which it returns if the callback has stopped the search; the lines after them (Ratpoints.Report.sieving), after which it returns if the Sturm step has left no interval; and the sieving (Ratpoints.sieving) with the result of the choice. It returns the delivery with the numbers of the moduli used, the end of the first stage of the choice and the ends of the second and the third stage of the last block of the run, after the sieving, and 0 for each after the returns before it.

C: find_points.c:4996-5006, find_points.c:5010-5012, find_points.c:5100-5103, find_points.c:5105-5106, find_points.c:5210-5213

Deviation: a function of its own for the part of find_points_work_1 from the call of sieving_info on; the shape of the run as an argument, for the fields of the arguments and the local variables of find_points_work_1 that the C code passes on (the range of the denominators, the search intervals, the flags of the denominators, the classes and the word den_bits); the exit returns the delivery with the message, nothing delivered, where sieving_info returns the prime and find_points_work_1 the count 0; the delivery passed and returned, for the pointer info, the local flag quit of find_points_work_1 and the count total, and the numbers of the moduli used returned with it, for the fields sp1_used, sp2_used and sp3_used of the arguments, which find_points_work zeroes on entry; the report under RATPOINTS_VERBOSE printed through the print channel, that of the choice after it returns, where sieving_info prints it at its end; no failure for lack of memory, which the model cannot meet; no output under DEBUG.

Equations

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

def Ratpoints.searchPoints {σ : Type} (process : Int → Int → Int → σ → Answer σ) (c : List Int) (d H : Nat) (s : SieveOptions) (mayExtend : Bool) (fl : CheckFlags) (bLow bHigh : Nat) (domain : List (Double × Double)) (sturmEmpty : Bool) (print : String → σ → σ) (r : Delivery σ) : Id (Outcome σ)

The search of the polynomial with the coefficient list c of degree d that the set-up hands on, for the height bound H, the normalized options s of the sieve (Ratpoints.SieveOptions.normalize), whether the caller left the number of primes to the library (mayExtend), and the flags fl, over the denominators bLow, …, bHigh and the search intervals domain that the Sturm step leaves, with its flag sturmEmpty (Ratpoints.sturmRegion), delivered to the callback process on the delivery r, whose flag quit is clear, with the print channel print. First the flags of the tests on the denominators: the checked loop for even degree, which the choice of the moduli switches off when nothing comes of it; the Jacobi test for even degree, c_d not a square (Ratpoints.Setup.isSquare) and the switch s.jacobi; the squares for odd degree and |c_d| = 1; and for odd degree otherwise the divisors of c_d up to bHigh (Ratpoints.Setup.setupUs1); with their report (Ratpoints.Report.setup). Then the 2-adic information (Ratpoints.Sieve.twoAdic) with the packings of the classes of the denominators modulo 64 and the word den_bits of the classes that admit a numerator (Ratpoints.Sieve.numClasses), and nothing delivered when no class admits a numerator and there is no point at infinity, as there is for odd degree or c_d a square, after the message of the exit (Ratpoints.Report.noClasses). Then the report of the packing (Ratpoints.Report.packing) and the choice of the moduli and the search after it (Ratpoints.chooseAndSearch), with the mean bits per word of the bit arrays of the run (Ratpoints.meanBitsPerWord) and the shape of the run (Ratpoints.ShapeArgs), each point mapped by Ratpoints.Sieve.swapPoint when fl.reversed is set. It returns the data and the count of the delivery with the bits of the flags of the search that the program reads, the search intervals and the numbers of the moduli used (Ratpoints.Outcome): fl.reversed, the squares, the success of the divisor set-up, domain, and the numbers that the search after the choice returns, 0 for each after the 2-adic exit. For 1 ≤ H < 2 ^ 63, 1 ≤ bLow, bHigh ≤ H, d the degree of c and 1 ≤ d, the flags of the output clear, a callback that does not stop the search, well-formed search intervals and sturmEmpty false, the calls are those of the points at infinity followed by the points of the brute-force reference over the denominators of the search from bLow to bHigh (Ratpoints.searchDens) whose x / z lies in a search interval, in the order of its loop, increasing unless the shape is that of the divisors, each mapped when fl.reversed is set, also when an exit is taken; with sturmEmpty set, only the points at infinity.

C: find_points.c:4588-4589, find_points.c:4595-4596, find_points.c:4602, find_points.c:4603-4604, find_points.c:4607, find_points.c:4900-4914, find_points.c:4919-4920, find_points.c:4927, find_points.c:4942-4943, find_points.c:4948, find_points.c:4954-4959, find_points.c:4962-4963, find_points.c:4992-4995, ratpoints.h:415, ratpoints.h:418

Deviation: the range of the denominators, the search intervals and the flag sturm_empty as arguments, for the fields b_low, b_high, domain and num_inter of the arguments and the local flag of find_points_work_1; the flags of the denominators as Booleans, for the bits of args->flags; the divisors of the leading coefficient with their records as lists, for the arrays args->den_info and args->divisors of the arguments; the square test lcfsq of line 4906 made on the polynomial searched (Ratpoints.Setup.isSquare), where the C code computes it before the reversal check (line 4634) and clears it in case 2 (line 4770): the same value for an even degree, the only one that reads it; the array size normalized for the height bound where the estimate of the run reads it (Ratpoints.arraySizeAt); the test on point_at_infty of the 2-adic exit recomputed, as Ratpoints.Sieve.pointsAtInfinity decides it; the 2-adic exit returns the delivery with the message, nothing delivered, where find_points_work_1 returns the count 0; the delivery passed, for the pointer info, the local flag quit of find_points_work_1 and the count total, and the result with the bits of the flags written back, the search intervals and the numbers of the moduli used (Ratpoints.Outcome), for the bits that find_points_work_1 sets in args->flags, the intervals that it leaves in args->domain and the fields sp1_used, sp2_used and sp3_used that the part after the choice sets (Ratpoints.chooseAndSearch); the report under RATPOINTS_VERBOSE printed through the print channel, the lines of the tests on the denominators together after the divisor set-up, which prints nothing; no output under DEBUG.

Equations

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

def Ratpoints.findPointsWork {σ : Type} (c : List Int) (d H : Nat) (s : SieveOptions) (o : Options) (process : Int → Int → Int → σ → Answer σ) (info : σ) (print : String → σ → σ) : Id (Except (Refusal × σ) (Outcome σ))

The search of find_points_work_1 for the coefficient list c of degree d, the leading zeros dropped, after the checks of the coefficients, the height bound H and the leading zeros, with the options s of the sieve and the options o, delivered to the callback process from its data info, with the print channel print: the options normalized (Ratpoints.Options.normalize) and the report of the arguments as the search normalizes them (Ratpoints.Report.arguments, with Ratpoints.SieveOptions.normalize); the reversal check (Ratpoints.Setup.reversal), with its report (Ratpoints.Report.reversal), which may refuse the form or reverse the polynomial; the search intervals (Ratpoints.searchIntervals), [-h, h] for none, and the refusal Ratpoints.Refusal.badArgs for malformed ones; the Sturm step (Ratpoints.sturmRegion), with its report (Ratpoints.Report.sturmStep), which may refuse the form, return at once with nothing delivered and no interval when it keeps no interval and the polynomial searched has no point at infinity, or narrow the search intervals; and otherwise the search of the polynomial that the reversal check hands on (Ratpoints.searchPoints), with the options of the sieve normalized (Ratpoints.SieveOptions.normalize), whether the caller left the number of primes to the library (np_is_default, a negative value of s.numPrimes), the flag of the reversal and the options of the output o.noCheck and o.noY (Ratpoints.CheckFlags), the normalized range of the denominators and the search intervals that the Sturm step leaves, from the data info, the count 0 and the flag quit clear. A refusal comes with the data of the callback as the report has left it.

C: find_points.c:4577-4585

Deviation: a function of its own for the part of find_points_work_1 after the test of the leading zeros; the refusals returned apart from the outcome, with the data of the callback, for the negative codes that the C code returns, the caller keeping its data behind the pointer info; the outcome of the return of line 4889, which leaves the flags of the squares clear and no interval, with the data info, the count 0, the flag of the reversal, no interval and no moduli used, the flag being in fact clear there (the cases 1 and 3 of the reversal check leave an odd degree, and in case 2 the reversed polynomial takes the value c_d > 0 at 0, in the default interval, which the Sturm step keeps); the test of the longs (Ratpoints.Setup.useCLong), which the C code makes between the reversal check and the search intervals, made by the search, where it is used; the report under RATPOINTS_VERBOSE printed through the print channel, that of the reversal check and of the Sturm step after them, from their results, where the C code prints in their course; no failure for lack of memory, which the model cannot meet.

Equations

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

def Ratpoints.findPointsVerbose {σ : Type} (c : List Int) (H : Nat) (s : SieveOptions) (o : Options) (process : Int → Int → Int → σ → Answer σ) (info : σ) (print : String → σ → σ) : Except (Refusal × σ) (Outcome σ)

The search of find_points with the callback process and its data info, and with the print channel print, through which the library prints its report under RATPOINTS_VERBOSE (Ratpoints.Report) into the data of the callback: the points of height at most H on y ^ 2 = F(x, z) for the coefficient list c in the search region of the options o, found by the sieve with the moduli that the search chooses from the curve and the array size of the options s of the sieve, delivered to process, with the report between them, or a refusal with the data of the callback as the report has left it. More than Ratpoints.maxDegree + 1 coefficients, fewer than two, and the height bound 0 or one of 2 ^ 63 or more, which is not a long (Ratpoints.fitsLong), are refused, in the order of the program (errors 3, 5 and 4); then, as not squarefree (error 8), a list whose leading zeros lower ⌈n / 2⌉, where n + 1 is its length, that is ⌈d / 2⌉ < ⌈n / 2⌉ for the degree d = Ratpoints.BruteForce.degree c; these refusals come before the report, with the data info. Otherwise the search of find_points_work_1 (Ratpoints.findPointsWork): the options normalized (Ratpoints.Options.normalize: the range of the denominators within 1, …, H, the depth of the Sturm step at most 55, and the switch of the reversal off for a search region) and the report of the arguments; the reversal check, which may refuse the form too or reverse the polynomial; the search intervals, [-h, h] for none, and the refusal Ratpoints.Refusal.badArgs (error 9) for intervals without l ≤ u, not increasing and strictly apart, or with a NaN end; the Sturm step, which with 0 ≤ o.sturm refuses the form when the remainder chain of the polynomial searched is none (Ratpoints.Sturm.chain), that is when that polynomial has a repeated factor, returns at once, with nothing delivered and no interval, when it keeps no interval (at its exit for a polynomial without a real root and with a negative constant term, or when the intervals of its bisection miss the search intervals), so that that polynomial is negative on the search intervals within ±2 ^ 63, and that polynomial has no point at infinity, and otherwise narrows the search intervals to the intervals that it keeps, where it may be ≥ 0; and the search of the polynomial that the reversal check hands on (Ratpoints.searchPoints), with the flag of the reversal and the options of the output o.noCheck and o.noY (Ratpoints.CheckFlags), which delivers the points to process (under o.noCheck the candidate at infinity and the numerators that pass the sieve, the test for common factors and the third stage, each with y = 0), none when no class of the denominators modulo 64 admits a numerator and there is no point at infinity, or when the curve has no points modulo one of the primes looked at, and else the points at infinity first, then, unless the Sturm step has left no interval, those of the denominators in the order of the loop of the search (Ratpoints.Sieve.sieveRun) whose x / z lies in a search interval, each mapped back to the caller's curve after a reversal, until a call of process stops the search; it returns the data that process and print leave, the count, the bits of the flags that the program reads after the search, the search intervals as the search leaves them and the numbers of the moduli used (Ratpoints.Outcome).

C: find_points.c:4523-4528, find_points.c:4546, find_points.c:4551-4552, find_points.c:4557-4559, find_points.c:4564-4565, find_points.c:4567-4571, find_points.c:4606, find_points.c:4624-4633, find_points.c:4658, find_points.c:5219-5220, find_points.c:5226-5229, find_points.c:5235, find_points.c:5241-5242, ratpoints.h:362, ratpoints.h:399-400, ratpoints.h:409-411, ratpoints.h:427-430, ratpoints.h:436-437, ratpoints.h:441-442

Deviation: one function for find_points, find_points_work and the start of find_points_work_1, which the library calls in turn, and the rest of which is Ratpoints.findPointsWork. The refusals of the program, in its order and with its errors (Ratpoints.Refusal), returned apart from the outcome with the data of the callback, for the negative codes of the library (RATPOINTS_NON_SQUAREFREE and RATPOINTS_BAD_ARGS; RATPOINTS_WORK_LENGTH_TOO_SMALL and RATPOINTS_NO_MEMORY cannot arise), which share the long that find_points returns with the count, the caller keeping its data behind the pointer info: fewer than two coefficients are refused on the length of c, as the program refuses them, where the library refuses an empty list as a negative degree and one coefficient as the degree 0 (a longer list of degree 0 fails the test of the leading zeros first); and the height bound, which the program checks before it calls the library, comes before the test of the leading zeros, which the library makes first, so that 5 0 with H = 0 is error 4, as the program gives it. The degree with the leading zeros dropped is Ratpoints.BruteForce.degree c. A natural number H for the long height of the arguments (ratpoints.h:362), so that H = 0 stands for the heights below 1 that line 4658 refuses; a height that is not a long, 2 ^ 63 or more, is refused with error 4, as the program refuses it when it reads the height (Ratpoints.Cli.heightBound), where the library cannot be given one, its height being a long. The end of the type ratpoints_args (ratpoints.h:399-400) with its first fields, whose other fields are those of the options, the parameters, the result of the choice of the moduli and the outcome (Ratpoints.Options, Ratpoints.SieveOptions, Ratpoints.Params, Ratpoints.SievingInfo, Ratpoints.Outcome), of the divisor set-up (Ratpoints.Setup.setupUs1), or excluded. A list for the array of GMP integers and its scratch integers work, with nothing written back to the caller but the data of the callback, the count, three bits of the flags, the search intervals and the numbers of the moduli used (Ratpoints.Outcome), which are 0 unless the search sets them, as find_points_work zeroes them on entry with the working field sp3, so that there is no state between calls and the reset of the flags clears nothing; the callback a function that returns what the call gives (Ratpoints.Answer), and its data a value, for the pointer info; the bit RATPOINTS_VERBOSE of the flags as the print channel print, a function that prints a text into the data of the callback, which holds the standard output of the caller, so that the text comes between the points as on the standard output of the C program, and which prints nothing when the bit is clear; the options of the output as fields of the options (Ratpoints.Options), copied into the flags of the check (Ratpoints.CheckFlags) with the flag of the reversal, for the bits of args->flags that the mask of line 4606 keeps; the points at infinity and the square test of the leading coefficient are decided where they are used (Ratpoints.Sieve.pointsAtInfinity, Ratpoints.Setup.reversal, Ratpoints.sturmRegion, Ratpoints.searchPoints); no failure for lack of memory, which the model cannot meet.

Equations

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

def Ratpoints.findPointsWith {σ : Type} (c : List Int) (H : Nat) (s : SieveOptions) (o : Options) (process : Int → Int → Int → σ → Answer σ) (info : σ) (print : String → σ → σ := fun (x : String) (s : σ) => s) : Except Refusal (Outcome σ)

The search of find_points with the callback process and its data info, with the print channel print, which prints nothing by default, as without RATPOINTS_VERBOSE: the outcome of the search of Ratpoints.findPointsVerbose, or its refusal alone. With the default print channel, these are the points of height at most H on y ^ 2 = F(x, z) for the coefficient list c in the search region of the options o, found by the sieve with the moduli that the search chooses from the curve and the array size of the options s of the sieve, delivered to process, or the refusals of the program (errors 3, 5 and 4 for the coefficients and the height bound, error 8 for a form that is not squarefree, by the leading zeros, the reversal check or the Sturm step, and error 9 for malformed search intervals). It models no C code of its own: it is Ratpoints.findPointsVerbose with the data of the callback dropped from a refusal.

Equations

• Ratpoints.findPointsWith c H s o process info print = Except.mapError (fun (x : Ratpoints.Refusal × σ) => x.fst) (Ratpoints.findPointsVerbose c H s o process info print)

def Ratpoints.findPoints (c : List Int) (H : Nat) (s : SieveOptions := { }) (o : Options := { }) : Except Refusal (List (Int × Int × Int))

The points that the search with the options s of the sieve and the options o, by default those of a run of the program without options, delivers for the coefficient list c and the height H, as a list in their order: the search of Ratpoints.findPointsWith with the callback that appends each point (x, y, z) to an array and never stops the search (Ratpoints.appendPoint), from the empty array, or its refusal. With the options of the output clear these are the points of height at most H on y ^ 2 = F(x, z) in the search region of o (z = 0, or bLow ≤ z ≤ bHigh after the normalization and x / z in a search interval): the points at infinity first, then those of the denominators in the order of the loop of the search, each mapped back to the caller's curve after a reversal; with o.noY those of them with y ≥ 0; and with o.noCheck, where there are points at infinity, (a, 0, b) for the candidate at infinity, then the numerators that pass the sieve, the test for common factors and the third stage, of the denominators of the same range and with x / z in a search interval as the Sturm step leaves them, each as (x, 0, z), mapped back after a reversal. It models no C code: it is Ratpoints.findPointsWith with the appending callback of the model.

Equations

• Ratpoints.findPoints c H s o = Except.map (fun (x : Ratpoints.Outcome (Array (Int × Int × Int))) => x.info.toList) (Ratpoints.findPointsWith c H s o Ratpoints.appendPoint #[])

Examples

The points that ratpoints c H -q prints at the pinned commit, in the same order, also after a reversal and in the divisor shape, and with -k ({ reverse := false }); the list of the brute-force reference Ratpoints.bruteForce for other parameters, among them pieces of a few bit arrays; the refusals of forms that are not squarefree as the program makes them, with and without -s ({ sturm := -1 }) and -k, and the points of such forms that it searches; the search with the flag of the reversal, for polynomials to which ratpoints reverses others, and on curves without points modulo 3, 5 and 7, where it takes an exit, and without points modulo 64, where it takes the 2-adic exit; composite moduli, prime powers and products of them, in any order and with primes beyond the loop of the tables, made as the choice of the moduli makes them; the sieve entries of each kind, and the exit of the loop of the tables; the packing of -2 0 0 1 as the build of ratpoints with DEBUG prints it, with its classes, the word of the classes that admit a numerator, its seven packings, the biases of its moduli and the residues and row offsets of four denominators; the row offsets of the packing and the inverses of the strides against their rule (Ratpoints.Sieve.classOffsets); the sieve of one denominator in the packing of its class, with the residues of the denominator divided by the stride and the row offsets of the class, against the plain sieve of the numerators that the word of the class admits, also for words whose bits of the heights 1 to 3 can be none or end below 0, with either flag of the reversal; the tables of inverses and squares (Ratpoints.Sieve.inversesMod, Ratpoints.Sieve.squaresMod) of the Ratpoints.numPrimes primes among which the moduli are chosen; the search with a callback (Ratpoints.findPointsWith), with a callback that stops at its k-th call for every k, a stop at the first point at infinity at the heights 10 ^ 12 and 2 ^ 63 - 1, and the bits of the flags written back as ratpoints reports them; the options of the output ({ noY := true }, { noCheck := true }), against the output of ratpoints under -y, and under -x the survivors as normalized pairs among which are those of the points, whatever moduli the choice makes; the search region and the Sturm step against find_points of the pinned library, with the search intervals that it leaves, and the refusals of malformed search intervals; and the refusals in the order of the program, the coefficients before the height bound and the height bound before the leading zeros, for the height bound 0 and for 2 ^ 63, the least height that is not a long, while 2 ^ 63 - 1 passes on to the test of the leading zeros.