The contracts of the builders of the rows of a prime power and of a product #
The contracts of lay_out_pattern (Ratpoints.Sieve.repeatPattern,
Ratpoints.Sieve.layOutPattern), of the builder of the rows of a prime power
(Ratpoints.Sieve.sieveInitPower, with the patterns Ratpoints.Sieve.powerPatternUnit and
Ratpoints.Sieve.powerPatternNonunit), and of the blocks of the builder of the rows of a product
(Ratpoints.Sieve.productCopy, Ratpoints.Sieve.productAnd), as @[spec] theorems proved with
vcgen, the program logic of Lean core, with loop invariants that are named definitions: the row of
the residue b < m of a prime power m is the closed form of the row of b of its tables
(Ratpoints.Sieve.closedRow of Ratpoints.Sieve.Power.admits), stored into the table of rows of
its entry, and the blocks of the rows of the factors of a product, and-ed, are the and of the rows
of the factors.
Main definitions #
Ratpoints.Sieve.PatClear,Ratpoints.Sieve.PatZero: a pattern of periodmwith no bits frommon, and a cleared pattern.Ratpoints.Sieve.RepeatedBits: the words of the repeated pattern oflay_out_pattern.Ratpoints.Sieve.factorWord,Ratpoints.Sieve.productWord: a word of the row of a factor of a product read in the blocks of its length, and the and of those of the first factors.
Main statements #
Ratpoints.Sieve.repeatPattern_spec,Ratpoints.Sieve.layOutPattern_spec: the pattern repeated through the words, and laid out as a row of windows.Ratpoints.Sieve.sieveInitPower_spec: the rows of a prime power.Ratpoints.Sieve.productCopy_spec,Ratpoints.Sieve.productAnd_spec: the blocks of the rows of the factors of a product.Ratpoints.Sieve.toArray_eq_closedRow_of_productWord: the rows of the factors in closed form, and-ed in their blocks, are the closed form of the row of the product.
Implementation notes #
The file uses Lean core and Std only, as the contracts of the sieve do. The proofs use only that
Ratpoints.rbaPack and Ratpoints.chunk are positive, never their values. The bits of the words of
a pattern (Ratpoints.Sieve.bitAt_eq_getLsbD) are in Ratpoints.Proof.Rows, the contracts of the
builders of the rows of a prime in Ratpoints.Proof.PrimeRows, and those of the builders through
the tables of rows in Ratpoints.Proof.RowStore, and the row of a sieve entry as the and of the
rows of its factors in Ratpoints.Proof.Words (Ratpoints.Sieve.SieveEntry.admits_eq_all), with
the rows of a factor read at residues modulo its modulus (Ratpoints.Sieve.Factor.admits_congr).
The pattern repeated through words #
The pattern of period m in the words pat: bit j of word i < ⌈m / 64⌉ the bit of the
pattern at 64 i + j below m, clear from m on.
Equations
Instances For
The first or of word i of the copy of the pattern at the offset o = 64 q + s, a multiple of
m: word q + i gets the word shifted left by s.
The second or of word i of the copy at the offset o = 64 q + s, s ≠ 0: word q + i + 1
gets the word shifted right by 64 - s.
The invariant of the loop of Ratpoints.Sieve.repeatPattern over the copies of the pattern:
the offset o is a multiple of m, the words of rep hold the bits below it, and at the exit o
has reached 64 W.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The invariant of the loop over the words i of the copy at the offset o: the words of rep
hold the bits below o + 64 i (and below o + m), and at the exit the copy is done or cut at the
end of the words.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A word cleared, by the loop that clears the first words of rep.
A step of the loop over the words of a copy: the first or, and the second for s ≠ 0 when it
lies below W.
The copy at o done: the bits below o + m are in the words, the offset moves on by m.
The words of rep below words ≤ modWords + 2 hold the pattern of period m > 0 of the words
pat repeated from 0 on (Ratpoints.Sieve.RepeatedBits), for a pattern without bits from m
on.
The pattern laid out as a row #
The window of the repeated pattern at the offset o ≡ 64 x (mod m), o < m, is the window of
the pattern at 64 x.
The invariant of the loop of the words of the row of Ratpoints.Sieve.layOutPattern, after the
words below x: those words the windows of the pattern, and the offset o ≡ 64 x (mod m).
Equations
- Ratpoints.Sieve.RowLoopInvariant g m x st = (st.snd = 64 * x % m ∧ Ratpoints.Sieve.RowWords g m x st.fst)
Instances For
A step of the loop of the words of the row: word cur the window at the offset, which steps
on by 64 mod m modulo m.
A copy of word k to word m rbaPack + k, the window there being that at 64 k, since
m ∣ 64 m rbaPack.
The row of the pattern of period 0 < m ≤ 64 Ratpoints.modWords in the words pat, without
bits from m on, as lay_out_pattern lays it out: m + chunk - 1 bit arrays, word j the window
of the pattern at 64 j.
The rows of a prime power #
The words of a cleared pattern: Ratpoints.modWords words, every bit clear.
Equations
- Ratpoints.Sieve.PatZero pat = (pat.size = Ratpoints.modWords ∧ ∀ (y : Nat), Ratpoints.Sieve.bitAt pat y = false)
Instances For
The invariant of the loop of Ratpoints.Sieve.powerPatternUnit after the residues below x:
the residue r = x b⁻¹ mod m and the bits below x set where Ratpoints.Sieve.Power.fsq has the
bit of y b⁻¹.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bits of the pattern of a unit after the residue cur, its bit set when
Ratpoints.Sieve.Power.fsq has the bit of cur b⁻¹.
The pattern of the row of a unit b modulo the prime power m, from a cleared pattern: bit
x < m set when bit x b⁻¹ mod m of Ratpoints.Sieve.Power.fsq is, for the inverse of b below
m.
The invariant of the loop of Ratpoints.Sieve.powerPatternNonunit after the residues below
1 + c: the bits 1 ≤ y < 1 + c of the units y set where Ratpoints.Sieve.Power.gsq has the bit
of b y⁻¹.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pattern of the row of a residue b divisible by p modulo the prime power m, from a
cleared pattern: bit x of a unit x < m set when bit b x⁻¹ mod m of Ratpoints.Sieve.Power.gsq
is.
The pattern of a unit b < m read at the residue of a numerator is the row of b of the prime
power.
The pattern of a residue b < m divisible by p read at the residue of a numerator is the row
of b of the prime power.
The row laid out from the pattern of the residue b is the closed form of the row of b,
and so is what the builder stores.
The row of the residue b < m of the prime power m ≤ 64 Ratpoints.modWords with the tables
pw, for the inverse of b below m, is the closed form of the row of b of its tables, and the
builder stores it into the table of rows of the entry ref.
The blocks of the rows of a product #
Word y of the row of factor i of the product e, read in the blocks of the length q of
its modulus: word y mod rbaPack of bit array ⌊y / rbaPack⌋ mod q of the row frows[i].
Equations
Instances For
Word y of the row of the product e after its first K ≥ 1 factors: the and of their words
(Ratpoints.Sieve.factorWord).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The invariant of the loop of Ratpoints.Sieve.productCopy over the blocks of the first factor:
the bit arrays below x, a multiple of its modulus up to m, laid down.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A copy of bit array j of the first factor into bit array x + j.
The row of the first factor of the product e, of a modulus q ∣ m = e.p, laid down in the
blocks of its length: word y < m rbaPack of the row is word y of the factor read in those blocks
(Ratpoints.Sieve.factorWord).
The invariant of the loop of Ratpoints.Sieve.productAnd over the blocks of the factor
i ≥ 1: the bit arrays below x, a multiple of its modulus up to m, and-ed with it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An and of bit array j of the factor i into bit array x + j.
The rows of the factors i ≥ 1 of the product e, each of a positive modulus q ∣ m = e.p,
and-ed into the row in the blocks of their lengths: from the row of the first factor laid down,
word y < m rbaPack of the row is the and of the words of all the factors read in their blocks
(Ratpoints.Sieve.productWord).
The closed form of the rows of a product #
Bit t of word y of the row of the residue b mod q of factor i of a product, in closed
form, read in the blocks of the length q of its modulus: whether the factor admits 64 y + t.
The row of a product whose words are those of the rows of its factors, in closed form at the
residue b modulo their moduli, and-ed in the blocks of their lengths and repeated after the first
m bit arrays, is the closed form of the row of b of the product: the moduli of the factors
divide m, so each factor reads the numerators modulo its own modulus.