The plan of the blocks of the run

The run cuts the steps of its shape into segments (Ratpoints.Sieve.Shape.segments), one for each divisor of the divisor shape and one otherwise, and each segment into blocks of one length (Ratpoints.Sieve.Shape.blockPlan), the first block of each segment recorded with the number of the blocks at the end; the steps of block i are found from the segment that holds it (Ratpoints.Sieve.BlockPlan.steps). The plan that the run makes is well-formed (Ratpoints.Sieve.BlockPlan.WF): blocks of at least one step, the first blocks of the segments the running sums of the numbers of their blocks (Ratpoints.Sieve.numBlocks); for a well-formed plan the search for the segment of a block ends, the steps of the block are those of Ratpoints.Sieve.blockRange, its first step at most its last, and the blocks in order cover the steps of the segments in order. A decision of the correction of the moduli is well-formed for the entries of the run (Ratpoints.Sieve.DecisionWF) when its cut points are in order within the entries and the entries from its second cut point on count no factor.

Main definitions

• Ratpoints.Sieve.numBlocks, Ratpoints.Sieve.blockRange: the number of the blocks of a segment and the first and last steps of each.
• Ratpoints.Sieve.Shape.numSegs, Ratpoints.Sieve.Shape.segment: the segments of a shape.
• Ratpoints.Sieve.BlockPlan.WF: a well-formed plan of the blocks.
• Ratpoints.Sieve.BlockPlan.blockSteps, Ratpoints.Sieve.BlockPlan.blockSeg: the steps and the segment of a block.
• Ratpoints.Sieve.DecisionWF: a decision whose cut points the blocks can use.

Main statements

• Ratpoints.Sieve.flatMap_blockRange: the blocks of a segment cover its steps in order.
• Ratpoints.Sieve.Shape.segments_spec, Ratpoints.Sieve.Shape.blockPlan_spec: the segments of a shape, and the plan of its blocks well-formed over them.
• Ratpoints.Sieve.one_le_blockLength: a block has at least one step.
• Ratpoints.Sieve.BlockPlan.WF.steps_spec, Ratpoints.Sieve.BlockPlan.WF.run_steps_eq: the steps of a block of a well-formed plan, from its segment.
• Ratpoints.Sieve.BlockPlan.WF.flatMap_blockSteps: the blocks of a well-formed plan, in order, cover the steps of its segments in order.
• Ratpoints.Sieve.BlockPlan.WF.run_steps_le: the first step of a block is at most its last, which the loops of the blocks need to end.
• Ratpoints.Sieve.DecisionWF.mk_sp2, Ratpoints.Sieve.DecisionWF.map_dinv: a well-formed decision stays well-formed with no third stage, and for the entries with the inverses of the strides that Ratpoints.Sieve.classOffsets sets.

Implementation notes

The file uses Lean core and Std only, as the contracts of the sieve do.

The blocks of a segment

def Ratpoints.Sieve.numBlocks (lo hi len : Nat) : Nat

The number of the blocks of len steps of the segment of the steps lo, …, hi, the last possibly shorter: ⌊(hi - lo) / len⌋ + 1, and none for an empty segment, hi < lo.

Equations

• Ratpoints.Sieve.numBlocks lo hi len = if lo ≤ hi then (hi - lo) / len + 1 else 0

def Ratpoints.Sieve.blockRange (lo hi len j : Nat) : Nat × Nat

The first and last steps of block j of len steps of the segment of the steps lo, …, hi: from lo + j len, len steps or up to hi.

Equations

• Ratpoints.Sieve.blockRange lo hi len j = (lo + j * len, if hi - (lo + j * len) < len then hi else lo + j * len + len - 1)

theorem Ratpoints.Sieve.blockRange_succ (lo hi len j : Nat) : blockRange lo hi len (j + 1) = blockRange (lo + len) hi len j

theorem Ratpoints.Sieve.numBlocks_of_le {lo hi len : Nat} (hlen : 1 ≤ len) (h : lo + len ≤ hi) : numBlocks lo hi len = numBlocks (lo + len) hi len + 1

theorem Ratpoints.Sieve.blockRange_le {lo hi len j : Nat} (hlen : 1 ≤ len) (hj : j < numBlocks lo hi len) : lo ≤ (blockRange lo hi len j).fst ∧ (blockRange lo hi len j).fst ≤ (blockRange lo hi len j).snd ∧ (blockRange lo hi len j).snd ≤ hi

A block of a segment has its first step at most its last, both within the segment.

theorem Ratpoints.Sieve.flatMap_blockRange {len : Nat} (hlen : 1 ≤ len) {β : Type} (g : Nat → List β) (lo hi : Nat) : List.flatMap (fun (j : Nat) => List.flatMap g (List.range' (blockRange lo hi len j).fst ((blockRange lo hi len j).snd + 1 - (blockRange lo hi len j).fst))) (List.range (numBlocks lo hi len)) = List.flatMap g (List.range' lo (hi + 1 - lo))

The blocks of a segment, in order, cover its steps in order.

The plan of the blocks

def Ratpoints.Sieve.Shape.numSegs : Shape → Nat

The number of the segments of steps of the shape s: one for each divisor of the divisor shape, and one otherwise.

Equations

• (Ratpoints.Sieve.Shape.squares1 info divisors).numSegs = divisors.length
• x✝.numSegs = 1

def Ratpoints.Sieve.Shape.segment (s : Shape) (bLow bHigh n : Nat) : Nat × Nat

The first and last steps of segment n of the shape s for the denominators bLow, …, bHigh (Ratpoints.Sieve.Shape.segments).

Equations

• Ratpoints.Sieve.Shape.squares.segment bLow bHigh n = (Ratpoints.Sieve.ceilSqrt bLow, Ratpoints.Sieve.floorSqrt bHigh)
• (Ratpoints.Sieve.Shape.squares1 info divisors).segment bLow bHigh n = (Ratpoints.Sieve.ceilSqrt ((bLow - 1) / divisors[n]! + 1), Ratpoints.Sieve.floorSqrt (bHigh / divisors[n]!))
• (Ratpoints.Sieve.Shape.words forb forbVal useJacobi fast lcf).segment bLow bHigh n = (bLow / 64, bHigh / 64)
• Ratpoints.Sieve.Shape.all.segment bLow bHigh n = (bLow, bHigh)

theorem Ratpoints.Sieve.Shape.segments_spec (s : Shape) (bLow bHigh : Nat) : ⦃ True ⦄ s.segments bLow bHigh ⦃ fun (r : Array (Nat × Nat) × Nat) => r.fst.toList = List.map (s.segment bLow bHigh) (List.range s.numSegs) ⦄

The segments of steps of the shape s, one for each of its segments in order.

theorem Ratpoints.Sieve.Shape.toList_fst_run_segments (s : Shape) (bLow bHigh : Nat) : (s.segments bLow bHigh).run.fst.toList = List.map (s.segment bLow bHigh) (List.range s.numSegs)

structure Ratpoints.Sieve.BlockPlan.WF (plan : BlockPlan) : Prop

The blocks plan are well-formed: blocks of at least one step, and the first block of each segment the number of the blocks of the segments before it (Ratpoints.Sieve.numBlocks), the number of all the blocks at the end.

• one_le_len : 1 ≤ plan.len

  The blocks have at least one step.

• segBlock_eq : plan.segBlock.toList = List.map (fun (j : Nat) => (List.map (fun (sg : Nat × Nat) => numBlocks sg.fst sg.snd plan.len) (List.take j plan.segs.toList)).sum) (List.range (plan.segs.size + 1))

  The first block of each segment, and the number of all the blocks at the end.

theorem Ratpoints.Sieve.one_le_blockLength (steps : Nat) : 1 ≤ blockLength steps

A block has at least one step: the length that a build sets is positive (Ratpoints.blockLen_pos), and otherwise the length is at least 1.

theorem Ratpoints.Sieve.Shape.blockPlan_spec (s : Shape) (bLow bHigh : Nat) : ⦃ True ⦄ s.blockPlan bLow bHigh ⦃ fun (plan : BlockPlan) => plan.WF ∧ plan.segs = (s.segments bLow bHigh).run.fst ⦄

The blocks that Ratpoints.Sieve.Shape.blockPlan makes are well-formed, over the segments of Ratpoints.Sieve.Shape.segments.

theorem Ratpoints.Sieve.BlockPlan.WF.size_segBlock {plan : BlockPlan} (h : plan.WF) : plan.segBlock.size = plan.segs.size + 1

theorem Ratpoints.Sieve.BlockPlan.WF.getElem!_segBlock {plan : BlockPlan} (h : plan.WF) {j : Nat} (hj : j ≤ plan.segs.size) : plan.segBlock[j]! = (List.map (fun (sg : Nat × Nat) => numBlocks sg.fst sg.snd plan.len) (List.take j plan.segs.toList)).sum

theorem Ratpoints.Sieve.BlockPlan.WF.segBlock_succ {plan : BlockPlan} (h : plan.WF) {j : Nat} (hj : j < plan.segs.size) : plan.segBlock[j + 1]! = plan.segBlock[j]! + numBlocks plan.segs[j]!.fst plan.segs[j]!.snd plan.len

theorem Ratpoints.Sieve.BlockPlan.WF.nblocks_eq {plan : BlockPlan} (h : plan.WF) : plan.nblocks = plan.segBlock[plan.segs.size]!

theorem Ratpoints.Sieve.BlockPlan.WF.segBlock_mono {plan : BlockPlan} (h : plan.WF) {j k : Nat} (hjk : j ≤ k) (hk : k ≤ plan.segs.size) : plan.segBlock[j]! ≤ plan.segBlock[k]!

theorem Ratpoints.Sieve.BlockPlan.WF.segBlock_zero {plan : BlockPlan} (h : plan.WF) : plan.segBlock[0]! = 0

def Ratpoints.Sieve.SegmentSearchInvariant (plan : BlockPlan) (i : Nat) : Std.WP.WhileInvariant Nat Prop

The invariant of the search of Ratpoints.Sieve.BlockPlan.steps for the segment of block i, whose state is the segment seg: a segment of the blocks whose first block is at most i, and at the exit the segment whose blocks hold i.

Equations

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

theorem Ratpoints.Sieve.BlockPlan.WF.steps_spec {plan : BlockPlan} (h : plan.WF) (i : Nat) : ⦃ i < plan.nblocks ⦄ plan.steps i ⦃ fun (r : Nat × Nat × Nat) => r.fst < plan.segs.size ∧ plan.segBlock[r.fst]! ≤ i ∧ i < plan.segBlock[r.fst + 1]! ∧ r.snd = blockRange plan.segs[r.fst]!.fst plan.segs[r.fst]!.snd plan.len (i - plan.segBlock[r.fst]!) ⦄

The steps of block i < plan.nblocks of well-formed blocks: its segment, the one whose blocks hold it, and its first and last steps (Ratpoints.Sieve.blockRange). The search for the segment ends, since the first block after the last segment is the number of the blocks.

theorem Ratpoints.Sieve.BlockPlan.WF.run_steps {plan : BlockPlan} (h : plan.WF) {i : Nat} (hi : i < plan.nblocks) : ∃ (seg : Nat), seg < plan.segs.size ∧ plan.segBlock[seg]! ≤ i ∧ i < plan.segBlock[seg + 1]! ∧ (plan.steps i).run = (seg, blockRange plan.segs[seg]!.fst plan.segs[seg]!.snd plan.len (i - plan.segBlock[seg]!))

The steps of block i < plan.nblocks of well-formed blocks, from the segment whose blocks hold it (Ratpoints.Sieve.BlockPlan.WF.steps_spec).

theorem Ratpoints.Sieve.BlockPlan.WF.run_steps_eq {plan : BlockPlan} (h : plan.WF) {i seg : Nat} (hs : seg < plan.segs.size) (h1 : plan.segBlock[seg]! ≤ i) (h2 : i < plan.segBlock[seg + 1]!) : (plan.steps i).run = (seg, blockRange plan.segs[seg]!.fst plan.segs[seg]!.snd plan.len (i - plan.segBlock[seg]!))

The steps of a block of well-formed blocks that lies in the segment seg: the block i - segBlock[seg] of the segment (Ratpoints.Sieve.blockRange).

def Ratpoints.Sieve.BlockPlan.blockSteps (plan : BlockPlan) (i : Nat) : List Nat

The steps of block i of the blocks plan, in order.

Equations

• plan.blockSteps i = List.range' (plan.steps i).run.snd.fst ((plan.steps i).run.snd.snd + 1 - (plan.steps i).run.snd.fst)

def Ratpoints.Sieve.BlockPlan.blockSeg (plan : BlockPlan) (i : Nat) : Nat

The segment of block i of the blocks plan.

Equations

• plan.blockSeg i = (plan.steps i).run.fst

theorem Ratpoints.Sieve.BlockPlan.WF.flatMap_blockSteps {plan : BlockPlan} (h : plan.WF) {β : Type} (g : Nat → Nat → List β) : List.flatMap (fun (i : Nat) => List.flatMap (g (plan.blockSeg i)) (plan.blockSteps i)) (List.range plan.nblocks) = List.flatMap (fun (seg : Nat) => List.flatMap (g seg) (List.range' plan.segs[seg]!.fst (plan.segs[seg]!.snd + 1 - plan.segs[seg]!.fst))) (List.range plan.segs.size)

The blocks of well-formed blocks, in order, cover the steps of their segments in order, and so the lists g seg k of the steps k of each segment seg, in order.

theorem Ratpoints.Sieve.BlockPlan.WF.run_steps_le {plan : BlockPlan} (h : plan.WF) {i : Nat} (hi : i < plan.nblocks) : (plan.steps i).run.snd.fst ≤ (plan.steps i).run.snd.snd

The steps of a block of well-formed blocks run from its first to its last, which is not before it.

Well-formed decisions

structure Ratpoints.Sieve.DecisionWF (es : List SieveEntry) (sp1 : Nat) (d : Decision) : Prop

A decision d of the correction of the moduli is well-formed for the sieve entries es of the run and the end sp1 of the first stage: sp1 ≤ d.sp2 ≤ d.sp3 ≤ |es|, and every entry from the position d.sp2 on, those of the third stage and the reserve, counts no factor (Ratpoints.Sieve.SieveEntry.nf zero), so that, for the entries of the choice of the moduli, it is a prime of the table, as the third stage needs.

• sp1_le_sp2 : sp1 ≤ d.sp2

  The end of the second stage is at least that of the first.

• sp2_le_sp3 : d.sp2 ≤ d.sp3

  The end of the third stage is at least that of the second.

• sp3_le_length : d.sp3 ≤ es.length

  The end of the third stage is at most the number of the entries.

• nf_eq_zero (e : SieveEntry) : e ∈ List.drop d.sp2 es → e.nf = 0

  Every entry from the end of the second stage on counts no factor.

theorem Ratpoints.Sieve.DecisionWF.mk_sp2 {l : List SieveEntry} {sp1 : Nat} {d : Decision} (h : DecisionWF l sp1 d) (b : Nat) : DecisionWF l sp1 { block := b, sp2 := d.sp2, sp3 := d.sp2 }

A well-formed decision gives a well-formed decision with its end of the second stage and no third stage, for any first block.

theorem Ratpoints.Sieve.DecisionWF.map_dinv {es : List SieveEntry} {sp1 : Nat} {d : Decision} (h : DecisionWF es sp1 d) (dinv : SieveEntry → Array Nat) : DecisionWF (List.map (fun (e : SieveEntry) => { p := e.p, factors := e.factors, magic := e.magic, bias := e.bias, rbainv := e.rbainv, dinv := dinv e, ref := e.ref, init := e.init, r := e.r, nf := e.nf }) es) sp1 d

A well-formed decision stays well-formed for the sieve entries with the inverses of the strides that Ratpoints.Sieve.classOffsets sets.