The rows of the moduli

The rows of the sieve entries as words, built as the C code builds them in init.c and in the generators of the headers of the build, and the tables in which the C code keeps them: every row of the modulus m has m + chunk - 1 bit arrays of Ratpoints.rbaPack words, for the chunk Ratpoints.chunk, m bit arrays and copies of the first chunk - 1 of them, which the chunked first stage reads past the first m (Ratpoints.Sieve.andRowsChunked); word j of the row of the residue b has bit t set exactly when the row admits the numerator 64 j + t (Ratpoints.Sieve.Entry.admits, the reference of the rows of a prime). The row of 0 of a prime of the table is the pattern sieves0 that the build generates, from the words of the forbidden divisor p (Ratpoints.Sieve.sieves0, Ratpoints.Sieve.forbiddenRow); the rows of the other residues of a prime are built by the function that the build generates for the prime, from the code CODE_INIT_SIEVE1 for a prime below 64 (Ratpoints.Sieve.sieveInit1) and CODE_INIT_SIEVE2 for a prime above 64 (Ratpoints.Sieve.sieveInit2), which compute the pattern of the row four bits at a time (Ratpoints.Sieve.initFourDecl, Ratpoints.Sieve.initFourLoop, Ratpoints.Sieve.initBit), rotate it through the words and copy them (Ratpoints.Sieve.initReplicate). The row of a prime power is laid out from its pattern (Ratpoints.Sieve.sieveInitPower, Ratpoints.Sieve.layOutPattern), and the row of a product is the and of the rows of its factors, laid down in blocks of the length of each factor (Ratpoints.Sieve.sieveInitProduct), which builds the rows of its factors that are absent first (Ratpoints.Sieve.factorRows). The rows are kept in tables, one for each entry of the C code, by the residue (Ratpoints.Sieve.RowStore): the table of rows of a prime starts with its row of 0 (Ratpoints.Sieve.primeRows), the others with no rows (Ratpoints.Sieve.SieveEntry.addTables), and each builder stores the row that it builds into the table of rows of its entry (Ratpoints.Sieve.RowStore.publish); the row of a sieve entry is read from its table of rows or built into it by the builder of its kind (Ratpoints.Sieve.SieveEntry.fetchRow, Ratpoints.Sieve.SieveEntry.initRow, Ratpoints.Sieve.initFactorRow). The loop of the tables and the end of the choice of the moduli make the tables of rows of a run (Ratpoints.examineInLoop, Ratpoints.choiceEnd), and the run reads the rows of each denominator from them and builds those that are missing into them (Ratpoints.Sieve.setRows, Ratpoints.Sieve.buildRows).

Main definitions

• Ratpoints.Sieve.forbiddenRow, Ratpoints.Sieve.sieves0: the words of a forbidden divisor, and the row of 0 of a prime of the table.
• Ratpoints.Sieve.RowStore, Ratpoints.Sieve.RowStore.row?, Ratpoints.Sieve.RowStore.publish: the tables of rows, a row read from them, and a row stored into them.
• Ratpoints.Sieve.primeRows, Ratpoints.Sieve.Factor.newRows, Ratpoints.Sieve.SieveEntry.addTables: the table of rows of a prime, that of the entry of a factor, and the tables of rows of a sieve entry made in the store.
• Ratpoints.Sieve.initBit, Ratpoints.Sieve.initFourDecl, Ratpoints.Sieve.initFourLoop, Ratpoints.Sieve.initReplicate: the macros of init.c with which the rows of the primes are built.
• Ratpoints.Sieve.sieveInit1, Ratpoints.Sieve.sieveInit2: the rows of a prime below 64 and above 64, each stored into the table of rows of its entry.
• Ratpoints.Sieve.window, Ratpoints.Sieve.repeatPattern, Ratpoints.Sieve.layOutPattern: the 64 bits of packed words from a position on, and a pattern of period m repeated through words and laid out as a row.
• Ratpoints.Sieve.powerPatternUnit, Ratpoints.Sieve.powerPatternNonunit, Ratpoints.Sieve.sieveInitPower: the patterns of the rows of a prime power, and its rows, each stored into the table of rows of its entry.
• Ratpoints.Sieve.initFactorRow, Ratpoints.Sieve.factorRows, Ratpoints.Sieve.productCopy, Ratpoints.Sieve.productAnd, Ratpoints.Sieve.sieveInitProduct: the builder of the entry of a factor by its kind, the rows of the factors of a product, built into their tables of rows when absent, the blocks of the rows of the factors, and the rows of a product, each stored into the table of rows of its entry.
• Ratpoints.Sieve.SieveEntry.initRow, Ratpoints.Sieve.SieveEntry.fetchRow: the row of a sieve entry built by the builder of its kind, and read from its table of rows or built into it.

The row of 0 of a prime

def Ratpoints.Sieve.forbiddenRow (p : Nat) : Array UInt64

The words of the forbidden divisor p, and of the row of 0 of a prime p of the table: p words, word r with bit j clear exactly when p ∣ 64 r + j, made as the generator of the tables of the build makes its array work and as sieving_info makes the words of a forbidden divisor beyond the table: all ones, then for i < 64 the bit of the position p i cleared, the position N being bit N mod 64 of word ⌊N / 64⌋. The pattern sieves0 repeats them (Ratpoints.Sieve.sieves0).

C: find_points.c:2773-2777, gen_find_points_h.c:118-120

Deviation: one function for the two codes that make these words, the array work of the generator of find_points.h, for the primes of the table, and the words that sieving_info makes in the buffer forb_words for the forbidden divisors beyond the table (Ratpoints.Sieve.forbidden), with the positions p i for i < 64, for the positions m = 0, p, 2 p, … below 64 p there; a fresh array of p words, for the array work of RATPOINTS_MAX_PRIME words and for the space in the buffer; divisions and remainders for the shifts and masks by LONG_SHIFT and LONG_MASK.

Equations

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

def Ratpoints.Sieve.sieves0 (p : Nat) : Array UInt64

The row of 0 of the prime p of the table, the pattern sieves0[pn] that the generator of the tables of the build writes for the prime p = prime[pn]: the p words work of the forbidden divisor p (Ratpoints.Sieve.forbiddenRow) written Ratpoints.rbaPack times, the first p bit arrays, and then the rbaPack (chunk - 1) words work[i mod p], the copies of the first Ratpoints.chunk - 1 bit arrays, so that word x is word x mod p of work for x < (p + chunk - 1) rbaPack. Bit t of word x is set exactly when p ∤ 64 x + t. The forbidden divisors that are primes of the table read its first p words (Ratpoints.Sieve.forbiddenOfPrime, Ratpoints.Sieve.forbidden); the table of rows of a prime has it as its row of 0 (Ratpoints.Sieve.primeRows), as the sieve entry of a prime of the table has it in the C code, and the run reads it from there (Ratpoints.Sieve.setRows).

C: find_points.c:37, gen_find_points_h.c:102-116, gen_find_points_h.c:122-134

Deviation: a function of p, computed when it is called, for the row of p in the table sieves0 that the build generates and that find_points.c includes; its first (p + chunk - 1) rbaPack words, for the row of RBA_PACK (RATPOINTS_MAX_PRIME_EVEN + RATPOINTS_CHUNK - 1) words whose other words are 0 and never read.

Equations

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

The tables of rows

@[reducible, inline]

abbrev Ratpoints.Sieve.RowStore : Type

The tables of rows of the entries of a run: for the reference to an entry (Ratpoints.Sieve.EntryRef), the table of its rows by the residue of the denominator modulo its modulus, m of them for the modulus m, each none until it is built. These are the arrays sieve of the sieve entries of ratpoints, which the C code reaches through the pointers to the entries (sieve_list[n], and the field factor of the entry of a product), with none for NULL. A table of rows is made, with the row of 0 of a prime from the build and the others absent, where the C code makes the entry (Ratpoints.examineInLoop, Ratpoints.Sieve.SieveEntry.addTables), and the builders store the rows that they build into the table of their entry (Ratpoints.Sieve.RowStore.publish); the run reads the rows of a denominator from the tables of rows and builds the missing ones into them (Ratpoints.Sieve.setRows, Ratpoints.Sieve.buildRows), and hands the store on from one denominator to the next (Ratpoints.Sieve.sieveRun).

Equations

• Ratpoints.Sieve.RowStore = Std.HashMap Ratpoints.Sieve.EntryRef (Array (Option (Array UInt64)))

def Ratpoints.Sieve.RowStore.row? (s : RowStore) (ref : EntryRef) (r : Nat) : Option (Array UInt64)

The row of the residue r in the table of rows of the entry ref, the pointer se->sieve[r]: none when the row is not built yet, or when there is no such table or row.

Equations

• s.row? ref r = (Std.HashMap.getD s ref #[]).getD r none

def Ratpoints.Sieve.RowStore.publish (s : RowStore) (ref : EntryRef) (r : Nat) (row : Array UInt64) : RowStore

The store with the row row of the residue r in the table of rows of the entry ref, the store RP_PUBLISH(&se->sieve[b], row) of the row into its entry with which each builder ends (Ratpoints.Sieve.sieveInit1, Ratpoints.Sieve.sieveInit2, Ratpoints.Sieve.sieveInitPower, Ratpoints.Sieve.sieveInitProduct); the store as it is when it has no table of ref.

Equations

• s.publish ref r row = Std.HashMap.modify s ref fun (x : Array (Option (Array UInt64))) => x.set! r (some row)

def Ratpoints.Sieve.primeRows (p : Nat) : Array (Option (Array UInt64))

The table of rows of the prime p as examine_prime makes it: the row of 0 the pattern sieves0 of the build (Ratpoints.Sieve.sieves0), and the rows of the residues 1, …, p - 1 absent until they are built.

C: find_points.c:1820-1821

Deviation: the table returned, for the array sieve of the entry, which examine_prime fills; the row of 0 the words of the pattern, for the pointer to them.

Equations

• Ratpoints.Sieve.primeRows p = #[some (Ratpoints.Sieve.sieves0 p)] ++ Array.replicate (p - 1) none

def Ratpoints.Sieve.Factor.newRows : Factor → Array (Option (Array UInt64))

The table of rows that the entry of the factor f starts with: for a prime that of examine_prime (Ratpoints.Sieve.primeRows), and for a prime power m the m rows absent, as make_power makes them (Ratpoints.Sieve.SieveEntry.addTables).

Equations

• (Ratpoints.Sieve.Factor.prime t).newRows = Ratpoints.Sieve.primeRows t.p
• (Ratpoints.Sieve.Factor.power pw).newRows = Array.replicate pw.m none

def Ratpoints.Sieve.SieveEntry.addTables (e : SieveEntry) (s : RowStore) : RowStore

The store s with the tables of rows of the sieve entry e of a modulus, each made only when its reference is absent: the table of rows of the entry of each factor (Ratpoints.Sieve.Factor.newRows), that of a prime with its row of 0 (Ratpoints.Sieve.primeRows) and that of a prime power m with its m rows absent, as make_power makes it, and for a product the m rows absent of its own entry, as make_modulus makes them.

C: find_points.c:2427, find_points.c:2471

Deviation: the tables of rows made in the store of the run, by the reference to the entry (Ratpoints.Sieve.EntryRef), for the arrays sieve of the entries, after the choice for every entry, the reserve included (Ratpoints.choiceEnd), where make_power and make_modulus make them with the entry; a table of rows made only when its reference is absent, for the test of power_se (lines 2444 and 2466) by which the entry of a prime power is made once, and for the entry of a prime, which examine_prime makes once, with its table of rows, in the loop of the tables (Ratpoints.examineInLoop) or in the third stage (lines 2994-2995), where the model makes the table of a prime of the third stage after the choice, and none for a prime that the third stage examines and passes over, whose table nothing reads.

Equations

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

The rows of a prime

def Ratpoints.Sieve.initBit (w : UInt64) (v : Bool) (i : Nat) : UInt64

The word w with bit i < 64 or-ed with the Boolean v, RP_INIT_BIT in its form without a branch, w | v << i.

C: init.c:42-46

Deviation: the form of the production builds, where RP_INIT_BRANCH is not set; a Boolean for the int entry of is_f_square, which is 0 or 1.

Equations

• Ratpoints.Sieve.initBit w v i = w ||| v.toUInt64 <<< i.toUInt64

def Ratpoints.Sieve.initFourDecl (p d : Nat) : Nat × Nat × Nat × Nat

RP_INIT_FOUR_DECL: from the inverse d < p of the residue of the denominator, the residues ab1 = d, ab2 = 2 d mod p and ab3 = 3 d mod p of the second, third and fourth of the four lanes that compute the pattern of a row of the prime p four bits at a time, and their step d4 = 4 d mod p, each by one conditional subtraction of p.

C: init.c:62-63, init.c:65-70

Deviation: the form of the production builds, where RP_INIT_ONEWAY is not set; the residues returned, for the variables that the macro declares in its caller; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.initFourLoop (isfs : Array Bool) (p d4 : Nat) (w : UInt64) (lo hi ab ab1 ab2 ab3 : Nat) : Id (UInt64 × Nat × Nat × Nat × Nat × Nat)

RP_INIT_FOUR_LOOP: the bits of the word w from bit i = lo on, four at a time while i + 4 ≤ hi, bit i + k the entry of the table isfs at the residue of lane k (ab, ab1, ab2, ab3), each lane then stepped by d4 modulo p by a conditional subtraction; the word, the bit i reached and the residues of the lanes, with which the caller goes on.

C: init.c:64, init.c:72-83

Deviation: the form of the production builds, where RP_INIT_ONEWAY is not set; the table, the prime, the step, the word, the residues and the bounds as arguments and the word, the bit and the residues returned, for the variables of its caller that the macro reads and writes; Booleans for the int entries of is_f_square; the steps ab += d4; if (ab >= p) ab -= p; as conditional values.

Equations

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

def Ratpoints.Sieve.initReplicate {n : Nat} (p : Nat) (si : Vector UInt64 n) : Id (Vector UInt64 n)

RP_INIT_REPLICATE for the prime p: the first p words of the row si repeated through the words of its first p bit arrays, word a + k p set to word a for a < p and 1 ≤ k < Ratpoints.rbaPack; then the copies of the first (chunk - 1) rbaPack words after the first p rbaPack, word p rbaPack + k set to word k, in this order, so that they copy words already copied when p < chunk - 1 (Ratpoints.chunk). Word j of the result is word j mod p of si for j < (p + chunk - 1) rbaPack.

C: init.c:99-111

Deviation: the row passed and returned, for the pointer si of its caller.

Equations

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

def Ratpoints.Sieve.sieve1Pattern (t : Entry) (b : Nat) : Id UInt64

The pattern of the row of the residue b of the prime p = t.p < 64 in CODE_INIT_SIEVE1: the word help0 whose bit a < p is the entry of the table of t at a d mod p, for the inverse d of b modulo p from the table of inverses of t: four bits at a time from the four lanes of the residues a d mod p (Ratpoints.Sieve.initFourDecl, Ratpoints.Sieve.initFourLoop), and the bits left over, p mod 4 of them, one at a time from the first lane (Ratpoints.Sieve.initBit), its residue stepped by d modulo p.

C: init.c:131-143

Deviation: the steps ab += d; if (ab >= p) ab -= p; as conditional values; the results of the loop of four bits read as the components of its tuple; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.sieve1Rows (p : Nat) (help0 help1 : UInt64) : Id (Vector UInt64 ((p + chunk - 1) * rbaPack))

The first p words of the row of a prime p < 64 in CODE_INIT_SIEVE1, from the word help0, the pattern of the row repeated through the word, and the word help1, the pattern shifted right by 64 mod p: word 0 of the row help0, and for a = 1, …, p - 1 word a the rotation help1 | help0 << diff_shift, for diff_shift = (⌊64 / p⌋ + 1) p mod 64, with help1 then the bits of the old help0 shifted out by diff = 64 - diff_shift.

C: init.c:126-129, init.c:160-177

Deviation: ldp, p1, diff_shift and diff computed here, for the variables at the head of the function; the mask p1 & LONG_MASK as the remainder by 64; a fresh vector of (p + chunk - 1) rbaPack words, for the space that the builder takes from the buffer of the tables (ba_next); natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.sieveInit1 (t : Entry) (ref : EntryRef) (b : Nat) (store : RowStore) : Id (Vector UInt64 ((t.p + chunk - 1) * rbaPack) × RowStore)

The row of the residue b of the prime p = t.p < 64 with the tables t, as the function that the build generates for p from CODE_INIT_SIEVE1 builds it, p + chunk - 1 bit arrays, and the store store with the row stored into the table of rows of the entry ref (Ratpoints.Sieve.RowStore.publish): the pattern of p bits in help0 (Ratpoints.Sieve.sieve1Pattern); help1 the pattern shifted right by 64 mod p; the pattern repeated in help0 by or-ing in help0 shifted left by i for i = p, 2 p, 4 p, … below 64; the first p words of the row rotated out of help0 and help1 (Ratpoints.Sieve.sieve1Rows); then the copies (Ratpoints.Sieve.initReplicate).

C: init.c:118-125, init.c:130, init.c:144-159, init.c:178-183

Deviation: one function for every prime below 64, the prime that of its tables, for the function that the build generates for each prime with the prime a constant (init_sieve.h); the tables of the prime and the reference to its entry (Ratpoints.Sieve.EntryRef) as arguments, for the sieve entry se from which the C code reads them and into which it stores the row, and the store of the tables of the rows of the run passed and returned, for the arrays sieve of the entries; the row stored plainly, for the release store of RP_PUBLISH in a build with threads, which the model does not have; no copy pattern of help0, which the C code shifts for help1.

Equations

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

def Ratpoints.Sieve.sieve2Word (t : Entry) (d d4 n ab ab1 ab2 ab3 : Nat) : Id (UInt64 × Nat × Nat × Nat × Nat)

Word n ≤ ⌊p / 64⌋ of the pattern of the row of the prime p = t.p > 64 in CODE_INIT_SIEVE2: the bits i below m, 64 for n < ⌊p / 64⌋ and p mod 64 for the last word, four at a time from the four lanes (Ratpoints.Sieve.initFourLoop) and the bits left over one at a time from the first lane (Ratpoints.Sieve.initBit), its residue stepped by d modulo p; the word and the residues of the lanes, which go on to the next word.

C: init.c:209-216

Deviation: the residues of the lanes passed and returned, for the variables of the function; the steps ab += d; if (ab >= p) ab -= p; as conditional values; the results of the loop of four bits read as the components of its tuple; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.sieve2Pattern (t : Entry) (b : Nat) (help : Vector UInt64 (t.p / 64 + 2)) : Id (Vector UInt64 (t.p / 64 + 2))

The pattern of the row of the residue b of the prime p = t.p > 64 in CODE_INIT_SIEVE2, in the words help[0], …, help[⌊p / 64⌋]: word n the bits 64 n, … of the pattern, bit a < p the entry of the table of t at a d mod p for the inverse d of b modulo p, each word from Ratpoints.Sieve.sieve2Word, the four lanes (Ratpoints.Sieve.initFourDecl) going on from word to word.

C: init.c:204-208, init.c:217-219

Deviation: the words help passed and returned, for the array of the function; ⌊p / 64⌋ computed where it is used, for the variable wp; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.sieve2Rows (p : Nat) (help : Vector UInt64 (p / 64 + 2)) : Id (Vector UInt64 ((p + chunk - 1) * rbaPack))

The first p words of the row of a prime p > 64 in CODE_INIT_SIEVE2, from the words help[0], …, help[wp] of its pattern, wp = ⌊p / 64⌋, p = 64 wp + ds with 0 < ds < 64: words a < wp the words of the pattern; then for a = wp, …, p - 1, with the cursor a1 from wp on and the next position t after it in the ring of the wp + 1 words: help[a1] |= help[t] << ds, word a of the row help[a1], the cursor moved on to t and help[t] >>= 64 - ds.

C: init.c:195-196, init.c:220-238

Deviation: the words help passed, for the array of the function; diff_shift and diff computed here, for the variables at the head of the function, and wp where it is used, for the variable of the function; a fresh vector of (p + chunk - 1) rbaPack words, for the space that the builder takes from the buffer of the tables (ba_next); the shift by LONG_SHIFT and the mask by LONG_MASK as the division and the remainder by 64.

Equations

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

def Ratpoints.Sieve.sieveInit2 (t : Entry) (ref : EntryRef) (b : Nat) (store : RowStore) : Id (Vector UInt64 ((t.p + chunk - 1) * rbaPack) × RowStore)

The row of the residue b of the prime p = t.p > 64 with the tables t, as the function that the build generates for p from CODE_INIT_SIEVE2 builds it, p + chunk - 1 bit arrays, and the store store with the row stored into the table of rows of the entry ref (Ratpoints.Sieve.RowStore.publish): the ⌊p / 64⌋ + 2 words help cleared from the last, the pattern of the row in them (Ratpoints.Sieve.sieve2Pattern), the first p words of the row rotated out of them (Ratpoints.Sieve.sieve2Rows), and the copies (Ratpoints.Sieve.initReplicate).

C: init.c:186-194, init.c:197-203, init.c:239-244

Deviation: one function for every prime above 64, the prime that of its tables, for the function that the build generates for each prime with the prime a constant (init_sieve.h); the tables of the prime and the reference to its entry (Ratpoints.Sieve.EntryRef) as arguments, for the sieve entry se from which the C code reads them and into which it stores the row, and the store of the tables of the rows of the run passed and returned, for the arrays sieve of the entries; the words help a fresh vector, which the loop clears from the last, for the array whose words the function leaves unset until it clears them; the row stored plainly, for the release store of RP_PUBLISH in a build with threads, which the model does not have.

Equations

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

The rows of a prime power

def Ratpoints.Sieve.window (E : Array UInt64) (s : Nat) : UInt64

The 64 bits of the packed words E from position s on, where bit t of word q is at position 64 q + t: word s / 64 shifted right by r = s % 64, and for r ≠ 0 the lowest r bits of the next word above them, as lay_out_pattern cuts each word of a row out of the repeated pattern at line 291 of init.c (Ratpoints.Sieve.layOutPattern).

Equations

• Ratpoints.Sieve.window E s = if s % 64 = 0 then E[s / 64]! else E[s / 64]! >>> (s % 64).toUInt64 ||| E[s / 64 + 1]! <<< (64 - s % 64).toUInt64

def Ratpoints.Sieve.repeatPattern (pat : Array UInt64) (m words : Nat) (rep : Vector UInt64 (modWords + 2)) : Id (Vector UInt64 (modWords + 2))

The words rep of lay_out_pattern: its first words words cleared, and the pattern pat of period m or-ed in at the bit offsets o = 0, m, 2 m, … below 64 words, at each offset the ⌈m / 64⌉ words of the pattern, shifted left by o mod 64 into the words from ⌊o / 64⌋ on and, for a nonzero shift, right by 64 - o mod 64 into the next words, those beyond the first words words cut. For a pattern without bits from m on, bit N < 64 words of the result is bit N mod m of the pattern.

C: init.c:268-279

Deviation: the words rep passed and returned, for the array of lay_out_pattern; the two loops as while loops, for the for loops that step o by m and test i against two bounds; the or-ing into the next word as a conditional value; the shifts by LONG_SHIFT and the masks by LONG_MASK as divisions and remainders by 64.

Equations

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

def Ratpoints.Sieve.layOutPattern (pat : Array UInt64) (m : Nat) : Id (Vector UInt64 ((m + chunk - 1) * rbaPack))

The row of the pattern pat of period m, as lay_out_pattern lays it out, m + chunk - 1 bit arrays: the pattern repeated through words = ⌊(m + 127) / 64⌋ words, 64 words ≥ m + 64 (Ratpoints.Sieve.repeatPattern); for x < m rbaPack, word x of the row the 64 bits of the repeated pattern from the offset o = 64 x mod m on (Ratpoints.Sieve.window), the offset stepped by 64 mod m modulo m; then the copies of the first (chunk - 1) rbaPack words after the first m rbaPack. For 0 < m ≤ 64 Ratpoints.modWords and a pattern without bits from m on, bit t of word j of the row is bit (64 j + t) mod m of the pattern.

C: init.c:259-267, init.c:280-297

Deviation: the words rep a fresh vector of RP_MODWORDS + 2 zeros, for the array whose first words words lay_out_pattern clears and whose other words it leaves unset and never reads; a fresh vector of (m + chunk - 1) rbaPack words for the row, for the space that it takes from the buffer of the tables (ba_next); the step of the offset as a conditional value; the shifts by LONG_SHIFT and the masks by LONG_MASK as divisions and remainders by 64.

Equations

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

def Ratpoints.Sieve.powerPatternUnit (pw : Power) (b : Nat) (pat : Array UInt64) : Id (Array UInt64)

The pattern of the row of a unit b modulo the prime power m with the tables pw, in _ratpoints_sieve_init_power: for x < m, bit x of pat set (Ratpoints.Sieve.setBitAt) when bit r of fsq is (Ratpoints.Sieve.bitAt), for the residue r = x b⁻¹ mod m, stepped by the inverse of b modulo m from the table of inverses.

C: init.c:369-375

Deviation: the pattern passed and returned, for the array of the function; the step r += binv; if (r >= m) r -= m; as a conditional value; natural numbers for the longs.

Equations

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

def Ratpoints.Sieve.powerPatternNonunit (pw : Power) (b : Nat) (pat : Array UInt64) : Id (Array UInt64)

The pattern of the row of a residue b divisible by p modulo the prime power m = p ^ e with the tables pw, in _ratpoints_sieve_init_power: for the units x below m, bit x of pat set (Ratpoints.Sieve.setBitAt) when bit b x⁻¹ mod m of gsq is (Ratpoints.Sieve.bitAt), with the inverse of x modulo m from the table of inverses.

C: init.c:378-385

Deviation: the pattern passed and returned, for the array of the function; natural numbers for the longs and unsigned longs, the product b inv[x] below m ^ 2.

Equations

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

def Ratpoints.Sieve.sieveInitPower (pw : Power) (ref : EntryRef) (b : Nat) (store : RowStore) : Id (Vector UInt64 ((pw.m + chunk - 1) * rbaPack) × RowStore)

The row of the residue b of the prime power m = p ^ e with the tables pw, as _ratpoints_sieve_init_power builds it, and the store store with the row stored into the table of rows of the entry ref (Ratpoints.Sieve.RowStore.publish): the pattern pat of Ratpoints.modWords words cleared; for a unit b, bit x set when f(x b⁻¹) is a square modulo m (Ratpoints.Sieve.powerPatternUnit), and for p ∣ b, bit x of a unit x set when frev(b x⁻¹) is a square modulo m (Ratpoints.Sieve.powerPatternNonunit); then the pattern laid out as a row of m + chunk - 1 bit arrays (Ratpoints.Sieve.layOutPattern).

C: init.c:359-368, init.c:376-377, init.c:386-387, init.c:391-393, rp-private.h:592

Deviation: the tables of the prime power and the reference to its entry (Ratpoints.Sieve.EntryRef) as arguments, for the sieve entry se whose field pw points to the tables and into which the C code stores the row, and the store of the tables of rows of the run passed and returned, for the arrays sieve of the entries; the pattern a fresh array, which the loop clears, for the array whose words the function leaves unset until it clears them; the row stored plainly, for the release store of RP_PUBLISH in a build with threads, which the model does not have.

Equations

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

The rows of a product

def Ratpoints.Sieve.initFactorRow (init : RowInit) (ref : EntryRef) (f : Factor) (b : Nat) (store : RowStore) : Id (Array UInt64 × RowStore)

The row of the residue b built by the builder of the kind init on the tables of the factor f, whose entry is ref, and the store with the row that the builder stores into the table of rows of that entry: the call (*(se->init))(se, b, args) for the entry of a prime or a prime power, the function that the build generates for a prime below 64 (Ratpoints.Sieve.sieveInit1) or above 64 (Ratpoints.Sieve.sieveInit2), and the builder of the rows of a prime power (Ratpoints.Sieve.sieveInitPower). A kind that does not fit the factor, which the entries of the model never have (Ratpoints.Sieve.SieveEntry.refInit, Ratpoints.primeEntry, Ratpoints.makeModulus), gives the empty row and the store as it is. The row of 0 of a prime is never built: it is in the table of rows of the prime from the start, the pattern sieves0 that examine_prime installs (Ratpoints.Sieve.sieves0).

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.Sieve.initFactorRow init ref f b store = pure (#[], store)

def Ratpoints.Sieve.factorRows (e : SieveEntry) (b : Nat) (store : RowStore) : Id (Array (Array UInt64) × RowStore)

The rows of the factors of the product e for the residue b modulo their moduli, as _ratpoints_sieve_init_product takes them, and the store: for each factor f with the modulus q, the row of b mod q in the table of rows of its entry (Ratpoints.Sieve.RowStore.row?), and when it is absent the row that the builder of the entry of the factor builds and stores into that table (Ratpoints.Sieve.initFactorRow with Ratpoints.Sieve.Factor.init and Ratpoints.Sieve.Factor.ref).

C: init.c:407-414

Deviation: the rows of the factors an array returned with the store, for the array frow of the function and the tables of rows in the entries of the factors; the row read plainly, for the acquire load RP_ACQUIRE of a build with threads, which the model does not have; the number of the factors the length of their list, for the count nf.

Equations

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

def Ratpoints.Sieve.productCopy {n : Nat} (row : Vector UInt64 n) (e : SieveEntry) (frows : Array (Array UInt64)) : Id (Vector UInt64 n)

The row of a product m laid down from the row frows[0] of its first factor, of the modulus q, in _ratpoints_sieve_init_product: for x = 0, q, 2 q, … below m and j < q, bit array x + j of row set to bit array j of the row of the factor (Ratpoints.Sieve.storeBitArray).

C: init.c:419-423

Deviation: the row passed and returned, for the pointer of the function; the loop over x as a while loop, for the for loop that steps x by q; the row of the factor as the vector of its words, which the store of a bit array reads.

Equations

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

def Ratpoints.Sieve.productAnd {n : Nat} (row : Vector UInt64 n) (e : SieveEntry) (frows : Array (Array UInt64)) : Id (Vector UInt64 n)

The rows frows[i] of the other factors of the product m = e.p, each of the modulus q of its factor, and-ed into the row, in _ratpoints_sieve_init_product: for each factor i ≥ 1, for x = 0, q, 2 q, … below m and j < q, bit array x + j of row and-ed with bit array j of the row of the factor (Ratpoints.Sieve.andBitArray).

C: init.c:424-429

Deviation: the row passed and returned, for the pointer of the function; the loop over x as a while loop, for the for loop that steps x by q; the number of the factors the length of their list, for the count nf.

Equations

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

def Ratpoints.Sieve.sieveInitProduct (e : SieveEntry) (b : Nat) (store : RowStore) : Id (Vector UInt64 ((e.p + chunk - 1) * rbaPack) × RowStore)

The row of the residue b of the product m = e.p of the sieve entry e, as _ratpoints_sieve_init_product builds it, m + chunk - 1 bit arrays, and the store store with the rows of the factors that it builds and with the row stored into the table of rows of the entry (Ratpoints.Sieve.RowStore.publish): the rows of the factors for b modulo their moduli, from the tables of rows of their entries or built into them (Ratpoints.Sieve.factorRows); the row of the first factor laid down in blocks of its length (Ratpoints.Sieve.productCopy), the rows of the others and-ed in, in blocks of theirs (Ratpoints.Sieve.productAnd), and the copies of the first chunk - 1 bit arrays after the first m (Ratpoints.Sieve.storeBitArray). Since the moduli of the factors divide m, bit array y < m + chunk - 1 of the row is the and of the bit arrays y mod q of the rows of the factors.

C: init.c:399-406, init.c:415-418, init.c:430, init.c:443-445, rp-private.h:593

Deviation: the store of the tables of rows passed and returned, for the entries of the factors that the C code reaches through the pointers factor and for the entry se into which it stores the row; a fresh vector of (m + chunk - 1) rbaPack words, for the space that the builder takes from the buffer of the tables (ba_next) after the rows of the factors; the row stored plainly, for the release store of RP_PUBLISH in a build with threads, which the model does not have; the number of the factors the length of their list, for the count nf.

Equations

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

The rows of the entries of a run

def Ratpoints.Sieve.SieveEntry.initRow (e : SieveEntry) (b : Nat) (store : RowStore) : Id (Array UInt64 × RowStore)

The row of the residue b < e.p of the sieve entry e built by its builder, the call (*(se->init))(se, b, args) of the run, and the store with the row that the builder stores into the table of rows of the entry: for a product the builder of the rows of a product (Ratpoints.Sieve.sieveInitProduct), which builds the rows of its factors that are absent into their tables of rows first, and for a prime or a prime power the builder of its kind on the tables of its one factor, with the reference to the entry (Ratpoints.Sieve.initFactorRow).

Equations

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

def Ratpoints.Sieve.SieveEntry.fetchRow (e : SieveEntry) (b : Nat) (store : RowStore) : Id (Array UInt64 × RowStore)

The row of the residue b < e.p of the sieve entry e and the store: the row in the table of rows of its entry (Ratpoints.Sieve.RowStore.row?) when it is there, and otherwise the row that its builder builds into that table of rows (Ratpoints.Sieve.SieveEntry.initRow). This is the body of the loop of sift that builds the rows that are missing, which reads the pointer to the row again before it calls the builder (Ratpoints.Sieve.buildRows).

Equations

• e.fetchRow b store = match store.row? e.ref b with | some row => pure (row, store) | none => e.initRow b store

Examples