The fast search on byte-array masks

Ratpoints.FastMask.fastPoints is Ratpoints.Fast.fastPoints with the bit masks and the rows of the families held in byte arrays (Ratpoints.Mask) instead of natural numbers: the ANDs of a chunk with the rows of a denominator are one call of the primitive Ratpoints.Mask.andRows, in place, without the copies and allocations of an AND of two GMP integers, and the survivors come from the primitive Ratpoints.Mask.nextSet. The reversal, the parameters, the families, the chunks, the order of the loops and the exact check are those of Ratpoints.Fast.fastPoints; only the order of the points in a chunk may differ. The shifts of the rows are multiples of 8 when the products of the moduli are odd, as they are for every even step (Ratpoints.Fast.Family.shift), so that Ratpoints.Mask.andRows reads whole bytes, and the rows of a denominator serve all its chunks in turn. The data of the exact check is made once per denominator, when a chunk first leaves candidates (Ratpoints.FastMask.pointsOfDenWith), and the mask of a part of a chunk is cut from that of the chunk, in whole 64-bit words.

Main definitions

• Ratpoints.FastMask.fastPoints: the points, by the sieve on byte-array masks.

def Ratpoints.FastMask.repeatBytes (a : ByteArray) : Nat → ByteArray

a repeated 2 ^ k times.

Equations

• Ratpoints.FastMask.repeatBytes a 0 = a
• Ratpoints.FastMask.repeatBytes a k.succ = Ratpoints.FastMask.repeatBytes a k ++ Ratpoints.FastMask.repeatBytes a k

def Ratpoints.FastMask.hornerRec : List Int → Int → Int

Horner's rule by plain recursion (Ratpoints.BruteForce.horner with List.foldr, which copies the list into an array at each call).

Equations

• Ratpoints.FastMask.hornerRec [] x✝ = 0
• Ratpoints.FastMask.hornerRec (a :: w) x✝ = a + x✝ * Ratpoints.FastMask.hornerRec w x✝

def Ratpoints.FastMask.pointsOfDenWith (w : List Int) (f z : Int) (xs : List Int) : List (Int × Int × Int)

The exact check of Ratpoints.BruteForce.pointsOfDen for the denominator z, with the scaled coefficients w of z and the factor f (z for odd degree, else 1) made beforehand, and Ratpoints.FastMask.hornerRec, and the gcd by Ratpoints.Fast.natGcd.

Equations

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

def Ratpoints.FastMask.pointsOfDen (c : List Int) (d : Nat) (z : Int) (xs : List Int) : List (Int × Int × Int)

Ratpoints.BruteForce.pointsOfDen with Ratpoints.FastMask.hornerRec.

Equations

• Ratpoints.FastMask.pointsOfDen c d z xs = Ratpoints.FastMask.pointsOfDenWith (Ratpoints.BruteForce.scaledCoeffs c d z) (if d % 2 = 1 then z else 1) z xs

def Ratpoints.FastMask.windowByte (q : ByteArray) (o : Nat) : UInt8

The byte of the bits q[o], …, q[o + 7] (each 0 or 1).

Equations

• Ratpoints.FastMask.windowByte q o = q[o]! ||| q[o + 1]! <<< 1 ||| q[o + 2]! <<< 2 ||| q[o + 3]! <<< 3 ||| q[o + 4]! <<< 4 ||| q[o + 5]! <<< 5 ||| q[o + 6]! <<< 6 ||| q[o + 7]! <<< 7

@[irreducible]

def Ratpoints.FastMask.patternBits (T' : Array Bool) (m g k i : Nat) (acc : ByteArray) : ByteArray

The bytes 1 or 0 of the entries T'[j g % m] for j from k to m + 7, pushed to acc, where i = k g % m is the index of the first of them, stepped by g < m without a division.

Equations

• Ratpoints.FastMask.patternBits T' m g k i acc = if k < m + 8 then Ratpoints.FastMask.patternBits T' m g (k + 1) (if i + g < m then i + g else i + g - m) (acc.push T'[i]!.toUInt8) else acc

@[irreducible]

def Ratpoints.FastMask.periodBytes (q : ByteArray) (m i o : Nat) (acc : ByteArray) : ByteArray

The bytes Ratpoints.FastMask.windowByte q o for i from i₀ to m - 1, with o = 8 i % m carried along, pushed to acc.

Equations

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

def Ratpoints.FastMask.baseRow (T : Array (Array Bool)) (m G nb r : Nat) : ByteArray

The row of the modulus m for the residue r of the denominator, for the numerators 0, G, 2G, …, as a mask of nb bytes: bit j is set when the residues G j and r modulo m allow a point (T = Ratpoints.Fast.admitTable c d m).

Equations

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

structure Ratpoints.FastMask.Family : Type

A family of moduli with product M: an inverse ginv of the step modulo M and the rows for the residues r < M of the denominator, as masks.

• M : Nat

  The product of the moduli.

• ginv : Nat

  An inverse of the step G modulo M.

• rows : Array ByteArray

  The rows, for the residues 0, …, M - 1 of the denominator.

def Ratpoints.FastMask.mkFamily (G L : Nat) (ts : List (Nat × Array (Array Bool))) : Option Family

The family of the moduli of the list ts of pairs (m, T), for the step G and chunks of at most L numerators, with rows of L + 8 M bits, M the product of the moduli.

Equations

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

def Ratpoints.FastMask.Family.shift (F : Family) (a₀ : Int) : Nat

The shift that aligns the rows of the family F with a chunk starting at a₀ (Ratpoints.Fast.Family.shift).

Equations

• F.shift a₀ = (a₀ * ↑F.ginv % ↑F.M).toNat + F.M * ((8 - (a₀ * ↑F.ginv % ↑F.M).toNat % 8) * F.M % 8)

def Ratpoints.FastMask.chunkPoints (G : Nat) (w : Thunk (List Int)) (f : Int) (rs : Array ByteArray) (sh : Array Nat) (o : Nat) (a₀ : Int) (mask : ByteArray) (b : Nat) : List (Int × Int × Int)

The points with the denominator b in the chunk of the numerators a₀, a₀ + G, … with the mask mask (one bit per numerator), by the sieve with the rows rs of b and the shifts sh moved by o (Ratpoints.Mask.andRows), and the exact check with the scaled coefficients w of b and the factor f (Ratpoints.FastMask.pointsOfDenWith), made when first needed.

Equations

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

def Ratpoints.FastMask.partPoints (G : Nat) (w : Thunk (List Int)) (f : Int) (rs : Array ByteArray) (sh : Array Nat) (lo hi a₀ : Int) (len : Nat) (mask : ByteArray) (b : Nat) : List (Int × Int × Int)

The points with the denominator b in the part of the chunk of the len numerators a₀, a₀ + G, … with the mask mask that holds those from lo to hi (as Ratpoints.Fast.partPoints): the chunk with its mask when the part is the whole chunk, else the part with the bytes of the mask from that of its first bit to the end of the 64-bit word of its last.

Equations

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

def Ratpoints.FastMask.denPoints (c : List Int) (d H G : Nat) (fams : Array Family) (reg : Option (Array (Option (Int × Nat) × Option (Int × Nat)))) (sl : List (Nat × Int × Nat × ByteArray × Array Nat)) (b : Nat) : List (Int × Int × Int)

The points with the denominator b in the chunks sl, each with its mask (as Ratpoints.Fast.denPoints: none when a row of b is zero); the scaled coefficients of b for the exact check are made once, when first needed.

Equations

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

def Ratpoints.FastMask.search (c : List Int) (d H G L : Nat) (fams : Array Family) (reg : Option (Array (Option (Int × Nat) × Option (Int × Nat)))) (dens : List Nat) : List (Int × Int × Int)

The points with the denominators dens, by the sieve with the region reg (as Ratpoints.Fast.search); each chunk carries its mask of len bits, all set, padded to whole 64-bit words.

Equations

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

structure Ratpoints.FastMask.Config : Type

The parameters of the search: step, chunk length, families.

• G : Nat

  The step.

• L : Nat

  The largest chunk length.

• fams : Array Family

  The families.

def Ratpoints.FastMask.choose (tu : Fast.Tuning) (c : List Int) (d H B : Nat) : Config

The parameters for the coefficients c of degree d, the height bound H and B denominators (as Ratpoints.Fast.choose).

Equations

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

def Ratpoints.FastMask.sievePoints (c : List Int) (H : Nat) (bLow bHigh : Int) (tu : Fast.Tuning := { }) : List (Int × Int × Int)

The points of height at most H with their denominator in the range of bLow and bHigh, each once, of the sieve on c itself (as Ratpoints.Fast.sievePoints).

Equations

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

def Ratpoints.FastMask.fastPoints (c : List Int) (H : Nat) (bLow bHigh : Int) (tu : Fast.Tuning := { }) : List (Int × Int × Int)

The points of height at most H with their denominator in the range of bLow and bHigh, each once (as Ratpoints.Fast.fastPoints, with the reversal of ratpoints (Ratpoints.Fast.reversed): only such points in any case, and all of them assuming Sturm's theorem).

Equations

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