Native setup of the two Chan–He prime searches

The first search uses thresholds 3Λ|Sⱼ|². After saving its selected prime, native counting at that prime provides the second thresholds 3Λ coll Sⱼ p. Both searches use the complete prime scan and collision queries, including explicit positive signed-modulus encoding.

Main definitions

• Modulus.firstSetup: compute the first search's three thresholds.
• Modulus.secondSetup: compute the second thresholds from native counts.
• Modulus.program: compute the existing Chan–He modulus using two native minimum searches.

Main results

• Modulus.exec: exact modulus, input frame and charged cost from explicit local fits.
• Modulus.not_readsWidth: the program does not inspect the physical word width.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.digits : Fin 64

Collision divisor bound Λ.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.first : Fin 64

First selected candidate, or one if none qualifies.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.multiplier : Fin 64

Three times the collision divisor bound.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.output : Fin 64

Unsigned product of the two selections, each defaulting to one.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.firstSetup : WordRAM.Code WordRAM.Basis.standard 64

Charge all six square/threshold multiplications and the three scalar setup instructions.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.secondSetup : WordRAM.Code WordRAM.Basis.standard 64

Charge all three second-threshold multiplications and their scalar setup.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.program : WordRAM.Code WordRAM.Basis.standard 64

Run both concrete searches and compute their product. The prime table and its count are shared by all nodes and are supplied in the search ABI.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.firstState (x : WordRAM.Data 64) : WordRAM.Data 64

The exact data after the first setup; memory is unchanged.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.exec_firstSetup {w : ℕ} (x : WordRAM.Data 64) (h3 : WordRAM.Fits w 3) (htriple : WordRAM.Fits w (3 * x.regs digits)) (hsq : ∀ (j : Fin 3), WordRAM.Fits w (x.regs (CountCall.length j) ^ 2)) (hcut : ∀ (j : Fin 3), WordRAM.Fits w (3 * x.regs digits * x.regs (CountCall.length j) ^ 2)) : WordRAM.ExecWithin w firstSetup x (firstState x) 9

First-search thresholds are computed by nine actual native instructions.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.secondState (x : WordRAM.Data 64) : WordRAM.Data 64

The exact data after the second setup; memory is unchanged.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.exec_secondSetup {w : ℕ} (x : WordRAM.Data 64) (h3 : WordRAM.Fits w 3) (htriple : WordRAM.Fits w (3 * x.regs digits)) (hcut : ∀ (j : Fin 3), WordRAM.Fits w (3 * x.regs digits * x.regs (CountCall.result j))) : WordRAM.ExecWithin w secondSetup x (secondState x) 6

Second-search thresholds are computed by six actual native instructions.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.budget (x : WordRAM.Data 64) : ℕ

One polynomial bound for selector counters, thresholds and memory addresses.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.searchTime (x : WordRAM.Data 64) : ℕ

One search with its factor bounded by the largest candidate.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.cost (x : WordRAM.Data 64) : ℕ

Both searches, a baseline collision count, scalar setup and the final product.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.exec {w : ℕ} (x : WordRAM.Data 64) (values : Fin 3 → ℕ → ℤ) (hm : 2 ≤ x.regs Search.limit) (hmod : GenericRAM.Signed.Fits w ↑(x.regs Search.limit ^ 2)) (hbudget : WordRAM.Fits (w + 2) (budget x)) (hcard : x.regs CollisionTest.card = (x.regs Search.limit).primesLE.card) (hbefore : x.regs Search.primes + (x.regs Search.limit + 1) ≤ x.regs CountCall.scratch) (hbitmap : ∀ q ≤ x.regs Search.limit, x.mem (x.regs Search.primes + q) = if Nat.Prime q then 1 else 0) (hvalues : ∀ (j : Fin 3), ∀ i < x.regs (CountCall.length j), GenericRAM.Signed.Fits w (values j i)) (hsk : ∀ (j : Fin 3), x.regs (CountCall.source j) + x.regs (CountCall.length j) ≤ x.regs CountCall.scratch) (hkd : ∀ (j : Fin 3), x.regs CountCall.scratch + x.regs (CountCall.length j) ≤ x.regs CountCall.histogram) (hinput : ∀ (j : Fin 3), ∀ i < x.regs (CountCall.length j), x.mem (x.regs (CountCall.source j) + i) = WordRAM.Signed.encode (values j i)) (hinj : ∀ (j : Fin 3), Set.InjOn (values j) ↑(Finset.range (x.regs (CountCall.length j)))) : ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin (w + 2) program x y (cost x) ∧ (∀ (i : Fin 64), 28 ≤ ↑i ∧ ↑i ≤ 35 ∨ 40 ≤ ↑i ∧ ↑i ≤ 42 ∨ i = digits → y.regs i = x.regs i) ∧ (∀ a < x.regs CountCall.scratch, y.mem a = x.mem a) ∧ y.regs first = ThreeSum.ChanHe.firstP (x.regs Search.limit).primesLE (x.regs digits) (Finset.image (values 0) (Finset.range (x.regs (CountCall.length 0)))) (Finset.image (values 1) (Finset.range (x.regs (CountCall.length 1)))) (Finset.image (values 2) (Finset.range (x.regs (CountCall.length 2)))) ∧ y.regs output = ThreeSum.ChanHe.modulus (x.regs Search.limit).primesLE (x.regs digits) (Finset.image (values 0) (Finset.range (x.regs (CountCall.length 0)))) (Finset.image (values 1) (Finset.range (x.regs (CountCall.length 1)))) (Finset.image (values 2) (Finset.range (x.regs (CountCall.length 2))))

Compute exactly the existing Chan–He modulus with two complete native prime searches. The prime bitmap/count is a shared input built by PrimeTable.program. A single polynomial budget bounds selector counters, thresholds and addresses; input values and the maximum modulus fit the source width. The final halt is excluded.

The interface requires m ≥ 2 for a nonempty candidate-prime window. The intended preprocessing caller uses mPar n U = (wPar n U + 1) * (2 * log₂(wPar n U + 1) + 4) ≥ 4. The default-only window m = 1 is outside this interface, although the selector bounds extend to it; m = 0 fails the default-selector upper bound.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus.not_readsWidth : ¬program.ReadsWidth

The finite selector program never reads the word width.