The set-up of the run

The shape of the run that Ratpoints.Sieve.runSetup chooses from the flags of the search, and the bounds of the search intervals that it makes, which the contract of the search reads.

Main statements

• Ratpoints.Sieve.fst_run_runSetup, Ratpoints.Sieve.snd_run_runSetup: the shape that Ratpoints.Sieve.runSetup chooses from the flags of the search, and the bounds of the search intervals that it makes.

theorem Ratpoints.Sieve.fst_run_runSetup (useSquares : Bool) (us1 : Option (List Setup.DenInfo × List Nat)) (checkDenom useJacobi : Bool) (forb : List ForbiddenEntry) (forbVal : List ForbiddenVal) (lcf : Int) (H bHigh : Nat) (domain : List (Double × Double)) : (runSetup useSquares us1 checkDenom useJacobi forb forbVal lcf H bHigh domain).run.fst = if useSquares = true then Shape.squares else match us1 with | some (info, divisors) => Shape.squares1 info divisors | none => if checkDenom = true then Shape.words forb forbVal useJacobi (if useJacobi = true then (jacobiSetup lcf bHigh).run else none) lcf else Shape.all

The shape that Ratpoints.Sieve.runSetup chooses from the flags of the search.

theorem Ratpoints.Sieve.snd_run_runSetup (useSquares : Bool) (us1 : Option (List Setup.DenInfo × List Nat)) (checkDenom useJacobi : Bool) (forb : List ForbiddenEntry) (forbVal : List ForbiddenVal) (lcf : Int) (H bHigh : Nat) (domain : List (Double × Double)) : (runSetup useSquares us1 checkDenom useJacobi forb forbVal lcf H bHigh domain).run.snd = (exactBounds domain H.toInt64 bHigh.toInt64).run

The bounds of the search intervals of the run that Ratpoints.Sieve.runSetup makes.