The exact bounds of the search intervals

The search intervals of a run in the form in which the sieve of one denominator reads them, made once per run from the doubles of the search region (Ratpoints.Sieve.exactBounds): for the denominator b the numerators of an interval [l, u] are ⌈b l⌉, …, ⌊b u⌋ within the height bound, computed exactly. An end x is an exact binary fraction, |x| = m 2 ^ (-s) (Ratpoints.Sieve.ExactEnd, made by Ratpoints.Sieve.exactEnd from the bits of the double), and b |x| rounded as the end wants it is computed in 128 bits (Ratpoints.Sieve.exactScale); mostly, though, the sieve computes ⌈b l⌉ and ⌊b u⌋ in a long from a form (b M + C) >> sh of each end (Ratpoints.Sieve.endForm), which is exact for an end with a short mantissa and for an end beyond the height bound on its side. The intervals with both forms are taken inline (fast), the others by the products in 128 bits (Ratpoints.Sieve.IntervalBounds). The functions that turn the bounds of an interval into the bits of the numerators of a class, interval_bits and interval_bits_exact of the C code, are Ratpoints.Sieve.intervalBits and Ratpoints.Sieve.intervalBitsExact in Ratpoints.Model.Sieve, next to the conversion of numerators to bits that they end with (Ratpoints.Sieve.numeratorsToBits). The bounds are made once for the run (Ratpoints.Sieve.runSetup) and read by the sieve of one denominator (Ratpoints.Sieve.sift).

Main definitions

• Ratpoints.Sieve.ExactEnd, Ratpoints.Sieve.exactEnd: an end of a search interval as an exact binary fraction with the rounding of its side.
• Ratpoints.Sieve.exactScale: b |x| rounded as the end wants it, in 128 bits, capped at 2 ^ 64 - 1.
• Ratpoints.Sieve.endForm: the form (b M + C) >> sh of an end.
• Ratpoints.Sieve.IntervalBounds, Ratpoints.Sieve.exactBounds: the bounds of the search intervals of a run.

structure Ratpoints.Sieve.ExactEnd : Type

An end x = ±m 2 ^ (-s) of a search interval as exact_end makes it (Ratpoints.Sieve.exactEnd), with the rounding r = rh 2 ^ 64 + rl that Ratpoints.Sieve.exactScale adds to b m, 2 ^ s - 1 when the end wants b |x| rounded up and 0 when it wants it rounded down, and whether x < 0.

C: find_points.c:3217-3218

Deviation: a natural number for the int s, which is from 0 to 127, and a Boolean for the int neg.

• m : UInt64

  The mantissa: odd, or s = 0.

• rl : UInt64

  The low 64 bits of the rounding.

• rh : UInt64

  The high 64 bits of the rounding.

• s : Nat

  The exponent: |x| = m 2 ^ (-s).

• neg : Bool

  Whether x < 0.

@[instance_reducible]

instance Ratpoints.Sieve.instInhabitedExactEnd : Inhabited ExactEnd

Equations

• Ratpoints.Sieve.instInhabitedExactEnd = { default := Ratpoints.Sieve.instInhabitedExactEnd.default }

@[instance_reducible]

instance Ratpoints.Sieve.instReprExactEnd : Repr ExactEnd

Equations

• Ratpoints.Sieve.instReprExactEnd = { reprPrec := Ratpoints.Sieve.instReprExactEnd.repr }

def Ratpoints.Sieve.instReprExactEnd.repr : ExactEnd → Nat → Std.Format

Equations

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

structure Ratpoints.Sieve.IntervalBounds : Type

The bounds of a search interval as the sieve of one denominator reads them, rp_bounds: the forms (b lM + lC) >> lsh of the lower end and (b uM + uC) >> ush of the upper end (Ratpoints.Sieve.endForm), whether the interval is taken inline (fast), and both ends as exact binary fractions (Ratpoints.Sieve.ExactEnd). An interval that is not taken inline has the forms of an empty one, 0 at the lower end and -2 ^ 63 at the upper end.

C: find_points.c:3219-3221

Deviation: natural numbers for the int shifts lsh and ush, which are from 0 to 63, and a Boolean for the int fast.

• lM : Int64

  The multiplier of the form of the lower end.

• lC : Int64

  The constant of the form of the lower end.

• uM : Int64

  The multiplier of the form of the upper end.

• uC : Int64

  The constant of the form of the upper end.

• lsh : Nat

  The shift of the form of the lower end.

• ush : Nat

  The shift of the form of the upper end.

• fast : Bool

  Whether the interval is taken inline, from the forms of its ends.

• low : ExactEnd

  The lower end.

• up : ExactEnd

  The upper end.

@[instance_reducible]

instance Ratpoints.Sieve.instInhabitedIntervalBounds : Inhabited IntervalBounds

Equations

• Ratpoints.Sieve.instInhabitedIntervalBounds = { default := Ratpoints.Sieve.instInhabitedIntervalBounds.default }

def Ratpoints.Sieve.instReprIntervalBounds.repr : IntervalBounds → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Ratpoints.Sieve.instReprIntervalBounds : Repr IntervalBounds

Equations

• Ratpoints.Sieve.instReprIntervalBounds = { reprPrec := Ratpoints.Sieve.instReprIntervalBounds.repr }

def Ratpoints.Sieve.exactScale (b : Int64) (e : ExactEnd) : UInt64

min (2 ^ 64 - 1) ⌊(b m + r) / 2 ^ s⌋ for the end e = ±m 2 ^ (-s) with the rounding r (Ratpoints.Sieve.ExactEnd) and the denominator b, which is b |x| rounded as the end wants it, unless that does not fit 64 bits. The product b m in two 64-bit halves, the low half the product of the words and the high half by Ratpoints.Sieve.mulHi; r added with the carry from the low half; the 128-bit sum shifted right by s, from 0 to 127, in its halves; and 2 ^ 64 - 1 when the high half of the quotient is not 0. As b m < 2 ^ 126 and r < 2 ^ 127, the sum is below 2 ^ 128 and nothing is lost.

C: find_points.c:3231-3238, find_points.c:3257

Deviation: the 128-bit product, sum and shift on two 64-bit halves, the high half of the product by Ratpoints.Sieve.mulHi, for the unsigned __int128 of the arm that the modelled builds compile (the compiler defines __SIZEOF_INT128__, and RP_NO_INT128 is not set), which Lean core does not have; the other arm (lines 3239-3256), for a build without a 128-bit type, is excluded; the long b converted to a 64-bit word, as the C code converts it to an unsigned long.

Equations

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

def Ratpoints.Sieve.exactMantissa (ax : Double) : Id (UInt64 × Nat)

The mantissa m and the exponent s of a double ax with 0 ≤ ax < 2 ^ 63, the absolute value of an end, as exact_end makes them: ax = f 2 ^ ex with 1/2 ≤ f < 1 (Ratpoints.Double.frexp), m = f 2 ^ 53 (Ratpoints.Double.ldexp, converted by Ratpoints.Double.toUInt64) and s = 53 - ex, so that ax = m 2 ^ (-s); then s = 0 for m = 0, and else, while s > 0, the trailing zero bits of m dropped (Ratpoints.Sieve.ctz), at most s of them; m shifted up by -s when s < 0; and s capped at 127, which leaves ⌊b m 2 ^ (-s)⌋ = 0 and ⌈b m 2 ^ (-s)⌉ = 1 for every 1 ≤ b < 2 ^ 63, as they are for s = 127.

C: find_points.c:3272-3291

Deviation: an integer for the int s while it is computed, and a natural number when it is returned; the lowest set bit by the loop of RP_CTZL (Ratpoints.Sieve.ctz), where gcc and clang take __builtin_ctzl; the mantissa and the exponent returned, for the fields m and s of the rp_end that the C code writes.

Equations

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

def Ratpoints.Sieve.exactEnd (x : Double) (lower : Bool) : Id ExactEnd

The end x of a search interval, at its lower end if lower and at its upper end otherwise, as exact_end makes it (Ratpoints.Sieve.ExactEnd): neg for x < 0 (Ratpoints.Double.lt, so that -0.0 is not negative); m = 2 ^ 63 and s = 0 when |x| < 2 ^ 63 fails, an infinity included, which is beyond every numerator, and otherwise the mantissa and the exponent of |x| (Ratpoints.Sieve.exactMantissa); and the rounding 2 ^ s - 1, in two halves for s ≥ 64, when the end wants b |x| rounded up, which is when lower and neg differ (the lower end wants ⌈b x⌉, which is b |x| rounded up for x ≥ 0 and minus b |x| rounded down for x < 0, and the upper end the other way round), and 0 otherwise.

C: find_points.c:3264-3271, find_points.c:3292-3299

Deviation: the double as its bits, with fabs and the comparisons of the C language on them (Ratpoints.Double.fabs, Ratpoints.Double.lt); a Boolean for the int lower; the end returned, for the rp_end that the C code writes through its pointer.

Equations

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

def Ratpoints.Sieve.endForm (e : ExactEnd) (lower : Bool) (height bHigh : Int64) : Option (Int64 × Int64 × Nat)

The form w = (b M + C) >> sh of the end e of a search interval, at its lower end if lower and at its upper end otherwise, for the height bound height and the denominators up to bHigh ≥ 1, as end_form makes it, or none: for an end that can lie beyond the bound on its side (x < 0 at the lower end, x ≥ 0 at the upper end), whose |x| is rounded down, with Ratpoints.Sieve.exactScale at b = 1 at least height, so that |x| ≥ height, the form (0, -height, 0) at the lower end and (0, height, 0) at the upper end; and for s < 64 and m ≤ ⌊(2 ^ 63 - 1 - C) / bHigh⌋ the form (±m, C, s), the sign of x, with C = 2 ^ s - 1 at the lower end and 0 at the upper end, for which b M + C stays within the longs for every b ≤ bHigh.

C: find_points.c:3304-3318

Deviation: the form returned as an option, for the pointers M, C and sh through which the C code writes it and the int that says whether it has one; Int64 for the longs, with the division of Int64, which truncates as the C division does, on the non-negative longs LONG_MAX - c and b_high; a Boolean for the int lower; a natural number for the int sh.

Equations

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

def Ratpoints.Sieve.exactBounds (domain : List (Double × Double)) (height bHigh : Int64) : Id (Array IntervalBounds)

The bounds of the search intervals domain, increasing, disjoint and without a NaN, for the height bound height and the denominators up to bHigh ≥ 1, as exact_bounds makes them (Ratpoints.Sieve.IntervalBounds): for each interval [l, u] in turn, its ends (Ratpoints.Sieve.exactEnd, l as a lower end and u as an upper end), and the interval taken inline when height ≤ 2 ^ 63 - 65, so that Ratpoints.Sieve.numeratorsToBits needs no split form, and both ends have a form (Ratpoints.Sieve.endForm), with these forms; otherwise the forms of an empty interval, 0 at the lower end and -2 ^ 63 at the upper end.

C: find_points.c:3323-3340

Deviation: the search intervals and the bounds as arguments, for the fields domain, num_inter, height and b_high of the arguments, and the array of the bounds returned, for the array that run_setup allocates and exact_bounds fills through its pointer; Int64 for the longs; the conjunction of the tests, whose && makes the form of the upper end only when the lower end has one, as a bind of options, and the forms as the options that Ratpoints.Sieve.endForm returns, for the fields that end_form writes.

Equations

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

Examples

The ends that exact_end makes and the values of exact_scale for them, against a C program that runs these functions of the pinned commit verbatim, on doubles of every kind (both zeros, the subnormals, the infinities, 2 ^ 63 and its neighbours, integers and fractions of either sign); the numerator intervals of the search intervals of a run are in the examples of Ratpoints.Model.Sieve, against the build of ratpoints with DEBUG.