Native least-prime collision searches

The search scans the prime bitmap in increasing order. A candidate runs the complete native three-set collision query. Its first acceptance is retained while the remaining candidates are visited without further bitmap reads. If no candidate is accepted, the answer is one, matching ChanHe.minOrOne.

Main definitions

• Search.program: a fixed native prime search using charged collision queries.

Main results

• Search.exec: exact minimum/default selection with native fits, frames and charged cost.
• Search.preserves_caller: the upper five caller registers are preserved.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.limit : Fin 64

Largest candidate prime.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.primes : Fin 64

Prime bitmap base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.factor : Fin 64

Factor multiplied by the candidate prime.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.cursor : Fin 64

Current candidate.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.stop : Fin 64

One past the largest candidate.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.answer : Fin 64

Selected prime, or the default one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.found : Fin 64

Whether an acceptance has already occurred.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.one : Fin 64

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.zero : Fin 64

Constant zero.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.two : Fin 64

Constant two, for positive signed encoding.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.rawModulus : Fin 64

Unencoded candidate modulus.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.addr : Fin 64

Bitmap address scratch.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.bit : Fin 64

Loaded primality bit.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.modulus : Fin 64

Encoded candidate modulus.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.good : Fin 64

Acceptance flag returned by the collision query.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.query : WordRAM.Code WordRAM.Basis.standard 64

Compute and encode the candidate modulus, then run the full collision query.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.pick : WordRAM.Code WordRAM.Basis.standard 64

Record an accepted candidate, or retain the previous answer.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.nop : WordRAM.Code WordRAM.Basis.standard 64

A charged instruction that retains the answer.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.load : WordRAM.Code WordRAM.Basis.standard 64

Load a bitmap entry.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.inner : WordRAM.Code WordRAM.Basis.standard 64

Before the first acceptance, run the query exactly on prime candidates.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.body : WordRAM.Code WordRAM.Basis.standard 64

One candidate and its charged cursor increment.

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

Initialize the selector and scan the entire bounded candidate range.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.preserves_caller (i : Fin 64) (hi : 59 ≤ ↑i) : WordRAM.Code.Preserves i program

The five upper caller registers survive the complete native search.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search.exec {w : ℕ} (x : WordRAM.Data 64) (values : Fin 3 → ℕ → ℤ) (hfactor : 0 < x.regs factor) (hmod : GenericRAM.Signed.Fits w ↑(x.regs factor * x.regs limit)) (hfit : WordRAM.Fits (w + 2) (x.regs limit + 3)) (haddr : WordRAM.Fits (w + 2) (x.regs primes + (x.regs limit + 1))) (hbefore : x.regs primes + (x.regs limit + 1) ≤ x.regs CountCall.scratch) (hbitmap : ∀ q ≤ x.regs limit, x.mem (x.regs 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)) (hs : ∀ (j : Fin 3), WordRAM.Fits (w + 2) (x.regs (CountCall.source j) + x.regs (CountCall.length j))) (hk : ∀ (j : Fin 3), WordRAM.Fits (w + 2) (x.regs CountCall.scratch + x.regs (CountCall.length j))) (hd : WordRAM.Fits (w + 2) (x.regs CountCall.histogram + x.regs factor * x.regs limit)) (ht : ∀ (j : Fin 3), WordRAM.Fits (w + 2) (x.regs (CountCall.length j) * x.regs (CountCall.length j) + x.regs (CountCall.length j) + 1)) (hproduct : ∀ (j : Fin 3), WordRAM.Fits (w + 2) (x.regs (CountCall.length j) * x.regs (CountCall.length j) * x.regs CollisionTest.card)) (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 ((x.regs limit + 1) * (34 * (x.regs (CountCall.length 0) + x.regs (CountCall.length 1) + x.regs (CountCall.length 2)) + 15 * (x.regs factor * x.regs limit) + 102) + 9) ∧ (∀ (i : Fin 64), 28 ≤ ↑i ∧ ↑i ≤ 35 ∨ 40 ≤ ↑i ∧ ↑i ≤ 46 → y.regs i = x.regs i) ∧ (∀ a < x.regs CountCall.scratch, y.mem a = x.mem a) ∧ y.regs answer = ThreeSum.ChanHe.minOrOne ({q ∈ (x.regs limit).primesLE | ∀ (j : Fin 3), ThreeSum.ChanHe.coll (Finset.image (values j) (Finset.range (x.regs (CountCall.length j)))) (x.regs factor * q) * x.regs CollisionTest.card ≤ x.regs (CollisionTest.threshold j)})

The least prime whose three actual collision counts satisfy the supplied thresholds. Every candidate query is executed by Query.program; the hypotheses only constrain native input values, layout and word fits. All instructions, including the scan after acceptance, are charged. The final halt is excluded.