The contracts of the pieces and the bits of one interval #
The contracts of the components of the model on words from one piece on up to the bits of one
interval in pieces, as @[spec] theorems proved with vcgen, the program logic of Lean core, with
loop invariants that are named definitions. Each component hands the points it finds to the
callback of the caller on a delivery (Ratpoints.Delivery), whose flag of the stop is clear at the
start, and returns as soon as a call sets it; its contract says that the delivery it returns is the
reference of the delivery (Ratpoints.Delivery.deliver) of the list of the points it finds, which
passes over the points after the stop. The contracts speak of the bits j of the packing of a class
cl (Ratpoints.Sieve.NumClass), each standing for the numerator a₀ + 2 ^ k j
(Ratpoints.Sieve.NumClass.numerator), and of the tests of the bits that the rows of the moduli
read at their offsets (Ratpoints.Sieve.SieveSpec.Reads); the points of a numerator are those that
the exact check delivers with the flags of the search (Ratpoints.Sieve.acceptedPoints).
Main definitions #
Ratpoints.Sieve.IsMasked: the words of a piece with the masks at its two ends applied.Ratpoints.Sieve.arraysWith,Ratpoints.Sieve.bitsCounts: the number of the bit arrays that hold a bit that passes a test, and the counts that the bits of one interval add to the counters.Ratpoints.Sieve.lowMask,Ratpoints.Sieve.highMask,Ratpoints.Sieve.bitsBefore,Ratpoints.Sieve.pieceBits: the masks ofRatpoints.Sieve.siftBitsat the two ends of a piece, the bits of the pieces before a word number, and the bits of a piece that its masks leave.Ratpoints.Sieve.PieceResult: what a piece returns, as the two contracts ofRatpoints.Sieve.siftPiecestate it.Ratpoints.Sieve.SiftBitsInvariant,Ratpoints.Sieve.SiftBitsWhileInvariant: the invariant of the loop ofRatpoints.Sieve.siftBitsover the pieces, of the delivery and of the counters.
Main statements #
Ratpoints.Sieve.siftPiece_spec: one piece with rows that read tests of the bits delivers, in either arm of the first stage, the points of the numerators of the bits that the masks at its two ends leave and that pass the pattern of the class (Ratpoints.Sieve.classBit) and the tests of the rows, in increasing order.Ratpoints.Sieve.siftPiece_counters_spec: when the callback does not stop the search, one piece adds to the counters its words, its bit arrays that hold a bit that passes the pattern of the class, the tests of the first stage and the masks, and the counts of the tests of a candidate of the numerators whose points it delivers.Ratpoints.Sieve.siftBits_spec: the bits fromlowtohighin pieces deliver the points of the numerators of those that pass the pattern of the class and the tests of the rows, and, when the callback does not stop the search, add the counts ofRatpoints.Sieve.bitsCounts, independent of the size of the pieces.
Implementation notes #
The file uses Lean core and Std only, as Ratpoints.Proof.Words, Ratpoints.Proof.FirstStage,
Ratpoints.Proof.Stages, Ratpoints.Proof.Packing, Ratpoints.Proof.Delivery and
Ratpoints.Proof.Scan do, whose lemmas on bit arrays, rows, classes and the delivery and whose
contracts of both arms of the first stage and of the scan of a piece it builds on. The contracts
read the test of a candidate as its value (Ratpoints.Sieve.acceptedPoints), so that they need
nothing of the numerators and the denominator. The loop over the pieces returns at a stop: its
invariant holds the delivery of the points found so far with the flag clear before a return, and
the value returned after it, the delivery of all the points, since the reference passes over the
points after the first call that sets the flag (Ratpoints.Delivery.deliver_eq_of_prefix); its
verification conditions are closed by lemmas in their shape. A piece has a contract of the delivery
and one of the counters, as the scan has (Ratpoints.Proof.ScanCounts), whose proofs name the
contracts of the counters of the components they call; the loop over the pieces holds the delivery
and the counters in one invariant, and the contract of the bits of one interval states both. The
counts of the tests of a candidate, of the bit arrays and of the bits of one interval are
irreducible in their verification conditions. The contract of the sieve of one denominator, which
calls Ratpoints.Sieve.siftBits for each search interval, is in Ratpoints.Proof.Sift.
The masks and one piece #
The words v of a piece of n bit arrays are the words surv with the masks at its two ends
applied, as far as the bits t < 64 of the words y < n rbaPack go: bit t of word y is set in
v exactly when it is set in surv, maskLow ≤ 64 y + t and 64 y + t + maskHigh < rbaLength n,
for the number rbaPack of words of a bit array (Ratpoints.rbaPack).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bits of the words v of a piece of n bit arrays from the word number w0 on, the words
of its first stage with the first sp1 moduli of specs from the class word cw on (hand, as
Ratpoints.Sieve.andRows_spec states it) with the masks at its two ends applied, when the rows of
the moduli read the tests sf.2 of the bits (Ratpoints.Sieve.SieveSpec.Reads): bit t of word
y stands for the bit rbaLength w0 + 64 y + t, which is set when it passes the class word, the
tests of the first stage and the masks.
The words of the scan of a piece of n bit arrays from the word number w0 on, the words v
of its first stage with the first sp1 moduli of specs from the class word cw on (hand) with
the masks at its two ends applied, and-ed with the rows of the other moduli, when the rows of the
moduli read the tests sf.2 of the bits (Ratpoints.Sieve.SieveSpec.Reads): bit t of word y
stands for the bit rbaLength w0 + 64 y + t, which is set when it passes the class word, the tests
of all the moduli and the masks.
The points of a piece of n bit arrays from the word number w0 on, given the contracts of its
first stage with the first sp1 moduli of specs from the class word cw on the words surv
(hand, as Ratpoints.Sieve.andRows_spec states it) and of its scan with the other moduli on the
words v (hout, as Ratpoints.Sieve.scanPiece_spec states it, with the points g j of a bit
j), when v is surv with the masks applied and the rows of the moduli read the tests sf.2 of
the bits (Ratpoints.Sieve.SieveSpec.Reads): the points of the bits from rbaLength w0 + maskLow
to rbaLength (w0 + n) - 1 - maskHigh that pass the class word (Ratpoints.Sieve.classBit) and
all the tests.
The rows of the moduli, read at their offsets, are given by the tests sf.2 of the bits that
they read (Ratpoints.Sieve.SieveSpec.Reads), quantified in the postcondition since the program
does not mention them; the first sp1 moduli go to the first stage, in the chunked arm
(Ratpoints.Sieve.andRowsChunked_spec) for 1 < chunk ≤ 16 and in the other otherwise
(Ratpoints.Sieve.andRows_spec), the others to the second, with their reciprocals and the test
small, which keeps the values that the reductions by the reciprocals see in range
(Ratpoints.Sieve.SieveSpec.Fits); the bound on maskHigh is that of the high mask
(Ratpoints.Sieve.getLsbD_clearHighBits), and the low mask needs none.
The counters of one piece #
The number of the bit arrays with the word numbers w0, …, w0 + n - 1, of
Ratpoints.rbaLength bits each, that hold a bit that passes keep.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The counters of a piece of n bit arrays from the word number w0 on, given the contracts of
its first stage with the first sp1 moduli of specs from the class word cw on the words surv
(hand) and of the counters of its scan with the other moduli on the words v (hout, as
Ratpoints.Sieve.scanPiece_counters_spec states it), when v is surv with the masks applied and
the rows of the moduli read the tests sf.2 of the bits: the bit arrays that hold a bit that the
masks leave and that passes the class word and the tests of the first stage, and the counts of the
tests of a candidate of the numerators of the bits from rbaLength w0 + maskLow to
rbaLength (w0 + n) - 1 - maskHigh that pass the class word and all the tests.
When the callback does not stop the search, one piece of n bit arrays adds to the counters its
n Ratpoints.rbaPack words, in words, the number of its bit arrays that hold a bit that the masks
leave and that passes the pattern of the class (Ratpoints.Sieve.classBit) and the tests of the
rows of the first stage, the first sp1 moduli of specs, in arrays, and the counts of the tests
of a candidate (Ratpoints.Sieve.testedCounts) of the numerators of the bits that the masks leave
and that pass the pattern of the class and the tests of the rows of all the moduli; the tests
sf.2 that the rows read (Ratpoints.Sieve.SieveSpec.Reads) are quantified in the postcondition.
The bits of one interval #
The low mask of Ratpoints.Sieve.siftBits on the piece from the word number w0 on: the number
of the bits of the first piece below low, 0 on the others.
Equations
- Ratpoints.Sieve.lowMask low w0 = if w0 = low / ↑Ratpoints.rbaLength then (low - ↑Ratpoints.rbaLength * (low / ↑Ratpoints.rbaLength)).toNat else 0
Instances For
The high mask of Ratpoints.Sieve.siftBits on the piece that ends at the word number w1: the
number of the bits of the last piece above high, 0 on the others.
Equations
- Ratpoints.Sieve.highMask high w1 = if w1 = high / ↑Ratpoints.rbaLength + 1 then Ratpoints.rbaLength - 1 - (high % ↑Ratpoints.rbaLength).toNat else 0
Instances For
The bits from that of low up to the word number w0 that lie in low, …, high: those of the
pieces of Ratpoints.Sieve.siftBits before w0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bits of a piece of n bit arrays from the word number w0 on that the masks maskLow and
maskHigh at its two ends leave.
Equations
- Ratpoints.Sieve.pieceBits w0 n maskLow maskHigh = List.map (fun (k : Nat) => ↑Ratpoints.rbaLength * w0 + ↑maskLow + ↑k) (List.range (n * Ratpoints.rbaLength - maskLow - maskHigh))
Instances For
The bits up to the word number w0 and those of the next piece of r bit arrays, with the low
mask of Ratpoints.Sieve.siftBits and a high mask mH, the number of its bits above high, that
pass keep, with their points g: those up to the word number w1' = w0 + r.
The bits up to the word number w0 come first among those up to w0' ≥ w0.
The bits from that of low up to the word number one past that of high that lie in
low, …, high are the bits low, …, high.
On the words of a piece from the word number w0 ≥ ⌊low / rbaLength⌋ on that ends at
w1' = w0 + rr, with the low mask of Ratpoints.Sieve.siftBits and a high mask mH, the number of
its bits above high, the masks leave the bits in low, …, high.
The counts that the bits low, …, high of the class cl of the denominator b add to the
counters when they go through the sieve in pieces (Ratpoints.Sieve.siftBits), for the tests
keep1 and keep of the bits that the rows of the first stage and of the first two stages read,
with the thunk checks of the third stage: none if high < low, and otherwise the
Ratpoints.rbaPack words of each of the bit arrays from that of low to that of high, in
words, the number of these bit arrays that hold one of the bits that passes the pattern of the
class (Ratpoints.Sieve.classBit) and keep1, in arrays, and the counts of the tests of a
candidate (Ratpoints.Sieve.testedCounts) of the numerators of the bits that pass the pattern of
the class and keep, each as a UInt64, wrapping.
Equations
- One or more equations did not get rendered due to their size.
Instances For
What a piece of n bit arrays from the word number w0 on with the masks mL and mH at its
two ends returns in the loop of Ratpoints.Sieve.siftBits over the pieces of the class cl, from
the delivery r and the counters c, for the tests keep1 and keep of the bits that the rows of
the first stage and of the first two stages read and the points g of the bits: the delivery r'
of the points of its bits that the masks leave and that pass the pattern of the class and keep,
and, when the callback does not stop the search in it, the counters c' with its words, the number
of its bit arrays that hold a bit that the masks leave and that passes the pattern of the class and
keep1, and the counts of the tests of a candidate, with the thunk checks of the third stage over
the denominator b, of the numerators whose points it delivers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The invariant of the loop of Ratpoints.Sieve.siftBits over the pieces, for the bits from
low to high of the packing of the class cl, the tests keep1 and keep of the bits that the
rows of the first stage and of the first two stages read and the points g of the bits, from the
delivery r0 and the counters cnt0, at the exit of the loop or not: the bit arrays from that of
low up to the word number w0 are done, the callback has not stopped the search, the delivery is
that of the points of their bits in low, …, high that pass the pattern of the class and keep,
and the counters are cnt0 plus their words, the number of them that hold a bit in
low, …, high that passes the pattern of the class and keep1, and the counts of the tests of a
candidate, with the thunk checks of the third stage over the denominator b, of the numerators
whose points are delivered.
The next piece starts at the word number
w0, not below that oflow.The word number
w0is at most one past that ofhigh.At the exit,
w0is one past the word number ofhigh.The next piece ends at the word number
w1,rangebit arrays afterw0.A piece has at least one bit array.
The callback has not stopped the search.
- eq_deliver : r = Delivery.deliver process r0 (List.flatMap g (List.filter (fun (j : Int) => classBit cl.bits j && keep j) (bitsBefore low high w0)))
The delivery is that of the points of the bits up to
w0that pass the pattern of the class andkeep, in increasing order. - eq_counts : c = cnt0 + { words := ((w0 - low / ↑rbaLength).toNat * rbaPack).toUInt64 } + { arrays := (arraysWith (fun (j : Int) => classBit cl.bits j && keep1 j && decide (low ≤ j ∧ j ≤ high)) (low / ↑rbaLength) (w0 - low / ↑rbaLength).toNat).toUInt64 } + testedCounts b checks (List.map cl.numerator (List.filter (fun (j : Int) => classBit cl.bits j && keep j) (bitsBefore low high w0)))
The counters of the bit arrays from that of
lowup tow0.
Instances For
Ratpoints.Sieve.SiftBitsInvariant as the invariant of the while loop of
Ratpoints.Sieve.siftBits, with the value of a return at a stop: the delivery of the points of all
the bits low, …, high that pass the pattern of the class and keep, whose flag of the stop is
set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A piece of rr ≥ 1 bit arrays from the word number w0 on, which ends at
w1' ≤ high / rbaLength + 1, with the low mask of Ratpoints.Sieve.siftBits and a high mask mH,
the number of its bits above high, when the callback does not stop the search in it.
A piece that ends at w1' ≤ high / rbaLength + 1, when the callback stops the search in it: the
delivery is that of all the bits low, …, high that pass the pattern of the class and keep.
The pieces advance: the measure high / rbaLength + 1 - w0 of the loop of
Ratpoints.Sieve.siftBits decreases from one piece to the next.
The loop of Ratpoints.Sieve.siftBits ends at the word number one past that of high.
A middle piece, which ends at the word number w1 ≤ high / rbaLength + 1, when the callback
does not stop the search in it, in the shape of the verification condition.
The last piece, which ends at the word number high / rbaLength + 1, when the callback does not
stop the search in it, in the shape of the verification condition.
A middle piece, when the callback stops the search in it, in the shape of the verification
condition: the delivery is that of all the bits low, …, high that pass the pattern of the class
and keep.
The last piece, when the callback stops the search in it, in the shape of the verification
condition: the delivery is that of all the bits low, …, high that pass the pattern of the class
and keep.
What the piece of the verification condition needs of the invariant: the callback has not stopped the search.
At the exit of the loop of Ratpoints.Sieve.siftBits, the delivery is that of the points of the
bits low, …, high that pass the pattern of the class and keep, and the counters are those of
Ratpoints.Sieve.bitsCounts.
An empty interval of bits delivers nothing and counts nothing.
The bits from low to high in pieces of A ≥ 1 bit arrays, with the moduli specs and their
reciprocals, deliver the points of the numerators of the bits that pass the class word of cl and
the tests sf.2 that the rows of the moduli read (Ratpoints.Sieve.SieveSpec.Reads), quantified in
the postcondition since the program does not mention them, and, when the callback does not stop the
search, add to the counters the counts of Ratpoints.Sieve.bitsCounts, with the tests of the first
sp1 moduli for the first stage; an empty interval delivers and counts nothing; the loop over the
pieces ends by the measure high / rbaLength + 1 - w0, since every piece has at least one bit
array, or at a stop.