The choice of the moduli #
Ratpoints.sievingInfo is the model of sieving_info of ratpoints: the loop of the tables over
the primes looked at, which ranks the primes that say something by their keys for the first stage
(Ratpoints.phase1Key), records the forbidden divisors of the denominators and, when the caller
left the number of primes to the library, looks at further primes while the first two stages would
be short of moduli (Ratpoints.tablesLoop); the further forbidden divisors; the composite moduli,
the prime powers and products of them below RATPOINTS_COMPOSITE_MAX whose tables the run can pay
for (Ratpoints.addModuli); the first stage by its rule and the second by its offset, each taking
the candidates in the order of their keys and passing over one that shares a prime with one taken
(Ratpoints.takeEntries, Ratpoints.firstStages); the sieve entries of the composite moduli taken
(Ratpoints.makeModulus); the third stage by its cost rule, which may look at further primes
(Ratpoints.thirdStage); and the reserve of the correction of the moduli during the run, the
primes left, sorted with the third stage by their densities. It returns the first prime looked at
modulo which the curve has no points, if there is one, and otherwise the result of the choice
(Ratpoints.Params) with the sieve entries of all the moduli, their reciprocals, the forbidden
divisors, the store of the tables of rows and the switch of the checked loop of the denominators.
The search makes the choice after the 2-adic information (Ratpoints.chooseAndSearch).
Main definitions #
Ratpoints.primeEntry,Ratpoints.ModulusCandidate.ofPrime: the sieve entry and the candidate of a prime.Ratpoints.addModuli: the composite moduli offered.Ratpoints.makeModulus: the sieve entry of a composite modulus taken.Ratpoints.takeEntries,Ratpoints.firstStages: the candidates that a stage takes, and the first two stages.Ratpoints.tablesLoop: the loop of the tables.Ratpoints.thirdStage,Ratpoints.thirdOf: the third stage.Ratpoints.SievingInfo,Ratpoints.sievingInfo: the result ofsieving_info, and the function.
The candidates of the primes #
The sieve entry of the prime p of the table t with the density r, as examine_prime makes
it: its one factor, its reciprocal (Ratpoints.Sieve.magic), the bias p ⌈Ratpoints.rowBias / p⌉,
the inverse of Ratpoints.rbaLength modulo p from its table of inverses at the remainder of
Ratpoints.rbaLength by the multiplication with the reciprocal, the inverses of the strides empty,
the reference to its own table of rows, the builder of the build for p
(Ratpoints.Sieve.sieveInit), the density and the count 0 of factors.
It models no C code of its own: it is the part of examine_prime that makes the sieve entry
(find_points.c:1795-1819, in the range of Ratpoints.Sieve.examinePrime?), as a value.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The candidate of the prime of the table t, at the position pn of Ratpoints.primeTable,
with the density r and the code code of its examination (Ratpoints.Sieve.examinePrime?): the
density, the prime, the mask 2 ^ pn for pn < 64 and 0 otherwise, the count -1 of factors for
the code 2, when the prime says only that numerator and denominator are coprime, and 0
otherwise, and its sieve entry (Ratpoints.primeEntry); the key and the cost are set by the caller.
C: find_points.c:1782-1785
Deviation: the record returned, for the record prec_entry that examine_prime fills, its key and
cost 0.0 until the caller sets them, where the C code leaves them as they are; the count -1 read
from the code, which is 2 exactly when np ≥ p.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The composite moduli #
The prime powers examined so far by add_moduli: the records of the useful ones, by their index
(pws), and for each prime power p ^ e examined, by the position pn of p and the exponent
e, its index, or none when it says nothing (pw_idx).
C: find_points.c:2350, find_points.c:2352-2354, find_points.c:2358-2359
Deviation: a structure for the buffer pws, the count npw of its records and the array pw_idx
of indices with its markers -1 (not examined) and -2 (useless): an array of the records, and a
list of the pairs examined with an option, none for -2, a pair not in the list for -1.
- pws : Array Sieve.Power
The records of the useful prime powers, by their index.
The prime powers examined, by the position of their prime and their exponent: the index of the record, or none when it says nothing.
Instances For
The index of the prime power p ^ e, p at the position pn of the table, among the useful
prime powers of tab, examining it when it is examined for the first time
(Ratpoints.Sieve.examinePower, with pinf whether denominators divisible by p occur), and none
when it says nothing (Ratpoints.Sieve.Power.useful).
C: find_points.c:2387-2394
Deviation: the table passed and returned, for the buffer pws, the count npw and the array
pw_idx of add_moduli; no test of room in the buffer (line 2390), which never fails, since
add_moduli examines each prime power at most once and num_powers counts them all.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The state of the factorization of a candidate modulus in add_moduli: the cofactor left, the
position of the next prime, whether the candidate is still possible, the product of the densities
of the factors, the mask of their primes, their codes and the table of the prime powers examined.
C: find_points.c:2362, find_points.c:2364-2365
Deviation: a structure for the local variables of the loop over the candidates.
- rest : Nat
The cofactor left.
- pn : Nat
The position of the next prime of the table.
- ok : Bool
Whether the candidate is still possible.
- r : Float
The product of the densities of the factors.
- mask : UInt64
The mask of the primes of the factors.
The codes of the factors.
- tab : PowerTable
The prime powers examined.
Instances For
The state st of the factorization with the factor p ^ e, p at the position st.pn:
refused when Ratpoints.maxFactors factors are taken already, or p is beyond the first 64 primes;
for e = 1 the density of the prime from the loop of the tables (primeSe), refused when the prime
says nothing; for e > 1 that of the prime power (Ratpoints.powerIndex), refused when it says
nothing; the code of the factor and the bit of its prime.
C: find_points.c:2381-2386, find_points.c:2395-2398
Deviation: the densities of the primes from the array primeSe of the tables and densities of the
loop of the tables, for the entries prime_se and their fields r.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The factorization of the candidate m over the first pnLim primes of the table, from the
state st (Ratpoints.FacState), as add_moduli makes it: for the primes p in turn, while the
candidate is possible and the cofactor above 1, a cofactor below p ^ 2, a prime, is looked up
among the primes from p on and refused when it is not among the first pnLim; a prime that does
not divide the cofactor is passed over; else it is divided off as often as it divides and taken as
a factor (Ratpoints.takeFactor).
C: find_points.c:2370-2380, find_points.c:2399
Deviation: a while loop with the position of the prime in the state, for the loop for whose
variable pn the search for the prime below p ^ 2 advances; natural numbers for the longs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The candidate of the odd composite m, as add_moduli offers it, or none, with the table of
the prime powers examined: none when its table alone is too dear for the run of U words and D
denominators (ct m min(D, m) / U above Ratpoints.modulusTableMax), when it does not factor over
the primes looked at into factors that say something (Ratpoints.factorCandidate), when it is a
prime, and when the product of the densities of its factors is not below 1; else its density, its
mask and the codes of its factors, and its count of factors.
C: find_points.c:2363, find_points.c:2368, find_points.c:2400-2402, find_points.c:2404-2406
Deviation: the candidate returned, for the record prec[pnp] that add_moduli fills, with the key
and the cost 0.0, which the caller sets, and no sieve entry.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pool pool of the candidates with the composite moduli offered (Ratpoints.offerModulus),
the odd m from 9 below Ratpoints.maxPrimeEven and up to Ratpoints.compositeMax, each keyed for
the first stage (Ratpoints.phase1Key), until the pool holds Ratpoints.numPrimes + Ratpoints.maxModuli candidates; with the useful prime powers examined, by their index.
C: find_points.c:2346-2349, find_points.c:2351, find_points.c:2355-2356, find_points.c:2361,
find_points.c:2403, find_points.c:2407-2411
Deviation: the pool passed and returned, for the array prec and the count pnp, and the records
of the prime powers returned, for the buffer pws of the arguments; the tables and the densities of
the primes of the loop of the tables (primeSe) and whether denominators divisible by them occur
(pinf) as arrays by their positions; the estimates of the run as arguments, for the fields of the
arguments; a while loop over the candidates; natural numbers for the longs; no bound npw_max
(num_powers, line 2351), which never binds.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sieve entry of the composite modulus e, at the position n of the moduli, as make_power
and make_modulus make it from the codes of its factors: a code below Ratpoints.numPrimes the
table of the prime at that position from the loop of the tables (primeSe), another the record of
the prime power of its index (pws); a prime power, one factor, with the reference to its own table
of rows and the builder of a prime power; a product with the reference to its own table of rows by
its position and the builder of a product; the reciprocal, the bias, the inverse of
Ratpoints.rbaLength by the extended Euclidean algorithm (Ratpoints.Sieve.modinv), the density of
the candidate and its count of factors.
C: find_points.c:2414-2426, find_points.c:2428-2429, find_points.c:2434-2470,
find_points.c:2472-2475
Deviation: the entry returned as a fresh value, for the space that make_power and make_modulus
take from the buffer of the sieve entries, and the entry of a prime power made for each modulus that
needs it, where make_modulus makes it once and keeps it by its index (power_se), with the
density of the first modulus that makes it, the density of the prime power in both cases; the
factors as a list (Ratpoints.Sieve.Factor), the tables of a prime from the loop of the tables and
the records of the prime powers, for the pointers factor to their entries; the tables of rows,
which make_power (line 2427) and make_modulus (line 2471) clear, made in the store of the run
after the choice (Ratpoints.Sieve.SieveEntry.addTables).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The stages #
The pool pool with the candidates whose mask meets used dropped from the position start
on, in their order.
C: find_points.c:2509-2518
Equations
- One or more equations did not get rendered due to their size.
Instances For
The candidates that one stage takes from the pool pool, from the position start on, in the
order they are in, with the mask used of the primes of the moduli taken and the product rate of
their densities: a candidate that shares a prime with one taken is dropped from the pool; with
want ≥ 0 that many are taken, and with want < 0 the rule of the first stage decides
(Ratpoints.phase1Wants, with the bits per word bpw, the target and the offset extra of the
second stage); then every later candidate that shares a prime with one taken is dropped
(Ratpoints.dropUsed). Returns the pool, the mask, the product of the densities and the number
taken.
C: find_points.c:2490-2508, find_points.c:2519-2520
Deviation: the pool, the mask and the product passed and returned, for the pointers prec, pnp,
used and rate; an integer for the long want and natural numbers for the other longs; the
candidate dropped by Array.eraseIdxIfInBounds, for the loop that moves the rest down.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pool pool keyed again for the second stage from the position sp1 on, when there are
candidates left: the product rate of the densities of the first stage times the bits per word
swept bpws, and the key of each candidate left (Ratpoints.primeKey with the cost COST_PHASE2 rate per word, its table and the run of U words and D denominators), then those sorted by
their keys; with the product.
C: find_points.c:2853-2863
Deviation: the sort by qsort with compare_entries as Lean's stable merge sort
(Ratpoints.sortFrom), which gives the order of glibc's qsort, stable when it can allocate its
buffer, as always in the model, also on ties, since the keys are finite or +∞.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pool pool with the candidates from the position sp2 on that are not primes that say more
than coprimality dropped (count of factors not 0): the composite moduli not taken and the primes
that say only that numerator and denominator are coprime.
C: find_points.c:2879-2890
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pool pool with the sieve entries of the composite moduli among its first sp2 candidates
made (Ratpoints.makeModulus), each at its position.
C: find_points.c:2894-2900
Deviation: the entries kept in the candidates, for the array sieve_list into which sieving_info
puts them (line 2898), which the caller reads from the candidates.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The first two stages of the choice on the pool pool, sorted by keys, for the options s, the
target, the cost ct of a row, the estimate est, the bits per word swept bpws and the offset
sp2e of the second stage: the first stage takes the value of -n candidates when given, and
otherwise as many as its rule wants (Ratpoints.takeEntries); the rest keyed again
(Ratpoints.rankSecond); the second takes the value of -N minus the first when given, else
sp2e, at least 0; then the composite moduli and the primes that say only coprimality dropped
from the end of the second stage on (Ratpoints.dropComposites). Returns the pool and the two cut
points.
C: find_points.c:2843-2846, find_points.c:2864-2871
Deviation: integers for the longs that may be negative.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The loop of the tables #
The tuning of the choice that the options s give: the target of the first stage, the value of
-r when positive and Ratpoints.survivorsPerWord otherwise; the offset of the second stage in a
long run, the value of -R when ≥ 0 and Ratpoints.sp2Extra otherwise; its scale, the value of
-U when ≥ 0 and Ratpoints.sp2U0 otherwise; and the cost of a row of a table, the value of -C
when ≥ 0 and Ratpoints.costTable otherwise.
C: find_points.c:2569-2575
Deviation: the four values as a quadruple, for the local variables of sieving_info; the doubles of
the options by their bits (Ratpoints.Double.toFloat).
Equations
- One or more equations did not get rendered due to their size.
Instances For
What the choice derives from an estimate est of the run (Ratpoints.runShape), the mean bits
per word bpw, the scale u0 and the offset extra of a long run: the estimate, the cost of the
calls of the sieve per word COST_CALL calls / U, the bits per word swept bpw (U - pad) / U, and
the offset of the second stage (Ratpoints.phase2Offset).
C: find_points.c:2597-2599, find_points.c:2813-2815
Deviation: one function for the two places of the C code, the values returned.
Equations
Instances For
The state of the loop of the tables: the pool of the candidates, the number of primes to look at, the primes among the candidates that say only coprimality, the table and the density of each prime that says something by its position, whether denominators divisible by each prime occur, the forbidden divisors found and the store of the tables of rows.
C: find_points.c:2537-2539, find_points.c:2545, find_points.c:2547, find_points.c:2566-2567
Deviation: a structure for the local variables of sieving_info that the loop changes: arrays, for
prec with its count pnp, prime_se, pinf and the arrays of the forbidden divisors with their
counts; the tables and the densities of the primes, for the entries prime_se; the store of the
tables of rows, for the arrays sieve of the entries.
- pool : Array ModulusCandidate
The pool of the candidates.
- pnLim : Nat
The number of primes to look at,
pn_lim. - nWeak : Nat
The candidates that say only coprimality,
n_weak. - primeSe : Array (Option (Sieve.Entry × Float))
The table and the density of each prime that says something, by its position.
Whether denominators divisible by each prime occur, by its position.
The forbidden divisors tested with words.
- val : Array Sieve.ForbiddenVal
The forbidden divisors tested by their valuations.
- store : Sieve.RowStore
The store of the tables of rows.
Instances For
The state st of the loop of the tables after the prime at the position pn: its table
(Ratpoints.Sieve.examinePrime?), none when the curve has no points modulo it; whether denominators
divisible by it occur; when it says something, its candidate keyed for the first stage
(Ratpoints.ModulusCandidate.ofPrime, Ratpoints.phase1Key, for the cost ct of a row, the
estimate est and the cost cc of the calls), its table and density, the count of the primes that
say only coprimality, and its table of rows in the store (Ratpoints.Sieve.primeRows); and its
forbidden divisor for the checked loop, while fewer than maxForbidden are found
(Ratpoints.Sieve.forbiddenOfPrime).
C: find_points.c:2606-2626, find_points.c:2677
Deviation: the exit as none, for the prime that sieving_info returns, which the loop of the
tables returns (Ratpoints.tablesLoop); the store with the table of rows of the prime, for the
array sieve of its entry.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The state st of the loop of the tables after the decision whether to look at one more prime,
when the caller left the number of primes to the library and the last prime to look at has been
looked at: the pool sorted by keys; the end s1 of the first stage, the value of -n when given
and else what its rule would take (Ratpoints.primesForPhase1, with the bits per word swept bpws,
the target and the offset sp2e of the second stage), at most Ratpoints.numPrimes; the end of the
second stage it wants, the value of -N when given and else s1 + sp2e; one more prime when the
candidates that say more than coprimality are fewer.
C: find_points.c:2694-2705
Deviation: the sort by qsort with compare_entries as Lean's stable merge sort
(Ratpoints.sortFrom), which gives the order of glibc's qsort, stable when it can allocate its
buffer, as always in the model, also on ties, since the keys are finite or +∞; integers for the
longs that may be negative or large.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The loop of the tables over the primes of Ratpoints.primeTable from the first on, while fewer
than the number to look at have been looked at, that number being the normalized value of -p at
first: each prime examined in the loop (Ratpoints.examineInLoop), with an exit when the curve has
no points modulo one of them; and when the caller left the number to the library (mayExtend) and
the last prime to look at has just been looked at, while fewer than Ratpoints.numPrimes are, the
decision to look at one more (Ratpoints.raiseLimit). The exit returns the prime.
C: find_points.c:2601-2605, find_points.c:2693, find_points.c:2707
Deviation: a loop over the first Ratpoints.numPrimes positions that ends when the position reaches
the number to look at, for the loop for whose bound the body raises, which never passes
Ratpoints.numPrimes; no clearing of the arrays prime_se, power_se and pinf (lines
2601-2602), which the state starts empty.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The third stage #
The mean density of the candidates of the pool that say more than coprimality (count of factors
≥ 0), 1 when there are none, the quality of a prime that the third stage expects to find.
C: find_points.c:2982-2991
Equations
- One or more equations did not get rendered due to their size.
Instances For
The state of the third stage: the pool, the end sp3 of the stage, the survivors S expected
per denominator, and the number of primes looked at.
C: find_points.c:2922, find_points.c:2933
Deviation: a structure for the local variables of the stage.
- pool : Array ModulusCandidate
The pool of the candidates.
- sp3 : Nat
The end of the third stage.
- S : Float
The survivors expected per denominator.
- pnLim : Nat
The number of primes looked at.
Instances For
The third stage with one more prime looked at, the prime at the position st.pnLim of the
table, when the stage finds no prime in the pool that pays for itself: none when the curve has no
points modulo it; the pool as it is when it says nothing or only coprimality; else its candidate
with its density as its key and the cost 0.
C: find_points.c:2976-2978, find_points.c:2994-3008
Equations
- One or more equations did not get rendered due to their size.
Instances For
The third stage from the state st, up to sp3Want primes in all, with the costs perSurv and
perDenom of a prime per survivor and per denominator: while the stage has fewer, the prime of
least density not yet taken (Ratpoints.bestByR) is taken, moved to the end of the stage, and the
survivors multiplied by its density, unless there is none or, with -P absent (sp3Extra < 0), it
does not pay for itself, S (1 - perSurv - r) ≤ perDenom; then, when the caller left the number of
primes to the library (mayExtend) and fewer than Ratpoints.numPrimes have been looked at, unless
with -P absent a prime of the mean density of the pool (Ratpoints.rTyp) would not pay for itself
either, one more prime is looked at (Ratpoints.lookFurther); otherwise the stage ends. The exit,
when the curve has no points modulo a prime looked at, returns that prime.
C: find_points.c:2949-2950, find_points.c:2973-2975, find_points.c:2980-2981,
find_points.c:2992-2993, find_points.c:3009-3016
Deviation: a while loop over the state, the candidates swapped by Array.swapIfInBounds; the
sieve entry of the prime taken kept in its candidate, for the array sieve_list (line 3014).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The survivors per denominator that the third stage expects at its start, for the estimate est
of the run, the mean bits per word bpw and the densities of the moduli of the first two stages:
the numerators per denominator (U - pad) 64 / D, times the bits per word bpw / 64, times the
densities of the moduli of the first two stages, times Ratpoints.sp3Coprime for the test for
common factors.
C: find_points.c:2941-2947
Deviation: 64 for LONG_LENGTH.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The third stage of the choice after the first two, which end at sp2, for the options s, the
cost checkRel of a check, the estimate est and the bits per word bpw: it wants sp2 + P
primes for the value P of -P when that is given and below Ratpoints.numPrimes - sp2, and
Ratpoints.numPrimes otherwise; its costs per denominator, the value of -Q when ≥ 0 and
Ratpoints.sp3PerDenom otherwise, and per survivor Ratpoints.sp3PerSurvivor, each divided by
checkRel; the survivors at its start (Ratpoints.survivorsAtThird); then the stage
(Ratpoints.thirdStage).
C: find_points.c:2926-2932
Deviation: integers for the comparison of the longs; the double of -Q by its bits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The choice #
What the choice of the moduli gives the search: its result (Ratpoints.Params), the sieve
entries of all its moduli in their order, the reserve included, their reciprocals, the forbidden
divisors tested with words and by their valuations, the store of the tables of rows, and the switch
of the checked loop of the denominators, cleared when there is no forbidden divisor and no Jacobi
test.
C: ratpoints.h:389, ratpoints.h:391
Deviation: a structure for what sieving_info writes into the arguments, the arrays sieve_list
and magics (line 389) and forb_ba and forbidden (line 391) as lists, for the arrays with their
counts, the bit RATPOINTS_CHECK_DENOM of the flags as a Boolean and the fields of the result
(Ratpoints.Params), and into the entries, the arrays sieve as the store of the tables of rows;
no field for the array stage3_list (line 389), the buffer of the table of the third stage that
the sieving thread fills for each denominator (find_points.c:5127), which the model replaces by
the thunk of the checks (Ratpoints.Sieve.fillChecks, Ratpoints.Sieve.sift).
- params : Params
The result of the choice.
- entries : List Sieve.SieveEntry
The sieve entries of the moduli.
Their reciprocals.
- forb : List Sieve.ForbiddenEntry
The forbidden divisors tested with words.
- forbVal : List Sieve.ForbiddenVal
The forbidden divisors tested by their valuations.
- store : Sieve.RowStore
The store of the tables of rows.
- checkDenom : Bool
The switch of the checked loop of the denominators.
Instances For
The cost of one exact check relative to Ratpoints.checkReference: that of the curve
(Ratpoints.checkCost, with the value of -W) divided by it, and 1 when that is not positive.
C: find_points.c:2587-2588
Deviation: the value returned, for the field check_rel of the arguments; the double of -W by its
bits.
Equations
- Ratpoints.checkRelOf c d H s = do let __do_lift ← Ratpoints.checkCost c d H s.checkCost.toFloat have x : Float := __do_lift / Ratpoints.checkReference pure (if x ≤ 0.0 then 1.0 else x)
Instances For
The number of words at which the first correction of the moduli is made: Ratpoints.adaptWords
when the options s let the search correct its choice, -A not 0 and neither -n nor -N
given, and 2 ^ 64 - 1, which no run reaches, otherwise.
C: find_points.c:2580-2581
Deviation: a UInt64 for the unsigned long, 2 ^ 64 - 1 for ULONG_MAX.
Equations
Instances For
The end of the choice of the moduli, from the pool pool after the third stage t, which
starts at sp2: the third stage and the reserve sorted by their densities from sp2 on
(Ratpoints.ModulusCandidate.rLe), the sieve entries of all the candidates in their order, their
reciprocals and the store with the tables of rows of every entry and its factors
(Ratpoints.Sieve.SieveEntry.addTables). Every candidate has its sieve entry by then: a prime from
its examination (Ratpoints.ModulusCandidate.ofPrime), a composite modulus of the first two stages
from Ratpoints.stageEntries, and the composite moduli from the end of the second stage on have
been dropped (Ratpoints.dropComposites), so that the entries are those of the pool, position by
position.
C: find_points.c:3017, find_points.c:3024-3034, find_points.c:3064-3070
Deviation: the sort by qsort with compare_by_r as Lean's stable merge sort
(Ratpoints.sortFrom), from the end of the second stage on, as the C code sorts, which gives the
order of glibc's qsort, stable when it can allocate its buffer, as always in the model; the
entries, the reciprocals and the store returned, for the arrays sieve_list and magics of the
arguments and the arrays sieve of the entries; sp3_max the length of the list of the entries,
the larger of sp3 and the size of the pool, which is never smaller; no enlargement of the buffer
of the rows (lines 3042-3061), which the model does not have.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The choice of the moduli after the loop of the tables, which leaves the state st, for the
coefficient list c of degree d, the options s, the shape a of the run, the bits per word
bpw, the cost checkRel of a check, the switch checkDenom of the checked loop and the forbidden
divisors forb and forbVal: the estimate of the run again, now with the forbidden divisors
(Ratpoints.runShape, Ratpoints.choiceEstimate); the candidates keyed again; the composite moduli
(Ratpoints.addModuli); the pool sorted by keys; the first two stages (Ratpoints.firstStages);
the sieve entries of the composite moduli taken (Ratpoints.stageEntries); the third stage
(Ratpoints.thirdOf); and the end of the choice (Ratpoints.choiceEnd). The exit of the third
stage, when the curve has no points modulo a prime that it looks at, returns that prime.
C: find_points.c:2808-2812, find_points.c:2816-2823, find_points.c:2826
Deviation: the sort by qsort with compare_entries as Lean's stable merge sort
(Ratpoints.sortFrom), which gives the order of glibc's qsort, stable when it can allocate its
buffer, as always in the model, also on ties, since the keys are finite or +∞; the result returned
as a structure (Ratpoints.SievingInfo), for the fields of the arguments that sieving_info
sets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
What sieving_info computes for the search of the polynomial with the coefficient list c of
degree d, with the flag useCLong of the longs, the switch checkDenom of the checked loop of
the denominators, whether the caller left the number of primes to the library (mayExtend), the
normalized options s (Ratpoints.SieveOptions.normalize), the shape a of the run and the mean
bits per word bpw of its bit arrays (Ratpoints.meanBitsPerWord): the tuning
(Ratpoints.SieveOptions.tuning); the cost of one check (Ratpoints.checkRelOf); the first
estimate of the run, without the forbidden divisors (Ratpoints.runShape); the loop of the tables
(Ratpoints.tablesLoop), with an exit that returns the prime when the curve has no points modulo a
prime looked at; for the checked loop, the further forbidden divisors (Ratpoints.Sieve.forbidden);
the switch of the checked loop cleared when there is no forbidden divisor and no Jacobi test; and
the rest of the choice (Ratpoints.choiceTail).
C: find_points.c:2522-2532, find_points.c:2546, find_points.c:2548-2559,
find_points.c:2595-2596, find_points.c:2794-2795, find_points.c:3102-3103
Deviation: the result as the prime that sieving_info returns when the curve has no points modulo
it, the error of the result, and as a structure (Ratpoints.SievingInfo) otherwise, for the code
0 that it returns and the fields of the arguments that it sets; the arrays prime_se, power_se
and pinf of the loop of the tables in its state (Ratpoints.TableLoop), the entries of the prime
powers made where a modulus needs them (Ratpoints.makeModulus); no failure for lack of memory
(lines 2801 and 3061), which the model cannot meet; no output under RP_PRIME_STATS or DEBUG, and
the report under RATPOINTS_VERBOSE at its end (lines 3089-3095) printed by the search after it
returns (Ratpoints.Report.choice).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Examples #
The forbidden divisors 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 against their rule; the
stages, the composite moduli, the third stage and the end of the choice against their rule.