Complete native collision queries for Chan–He prime searches

A query computes all three collision counts and tests their scaled thresholds. No count or acceptance test is supplied as advice: all counting and comparison instructions are charged.

Main definitions

• Query.program: the complete native collision-count and threshold query.

Main results

• Query.exec: exact three-inequality acceptance, input frame and instruction bound.

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

Count collisions and test all three inequalities.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Query.exec {w M : ℕ} (x : WordRAM.Data 64) (values : Fin 3 → ℕ → ℤ) (hM : 0 < M) (hmod : GenericRAM.Signed.Fits w ↑M) (hmodreg : x.regs CountCall.modulus = WordRAM.Signed.encode ↑M) (hfit : ∀ (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 + M)) (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)) (hz : x.regs CollisionTest.zero = 0) (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 (34 * (x.regs (CountCall.length 0) + x.regs (CountCall.length 1) + x.regs (CountCall.length 2)) + 15 * M + 85) ∧ (y.regs CollisionTest.good = if ThreeSum.ChanHe.coll (Finset.image (values 0) (Finset.range (x.regs (CountCall.length 0)))) M * x.regs CollisionTest.card ≤ x.regs (CollisionTest.threshold 0) ∧ ThreeSum.ChanHe.coll (Finset.image (values 1) (Finset.range (x.regs (CountCall.length 1)))) M * x.regs CollisionTest.card ≤ x.regs (CollisionTest.threshold 1) ∧ ThreeSum.ChanHe.coll (Finset.image (values 2) (Finset.range (x.regs (CountCall.length 2)))) M * x.regs CollisionTest.card ≤ x.regs (CollisionTest.threshold 2) then 1 else 0) ∧ (∀ (i : Fin 64), 28 ≤ ↑i ∧ ↑i < 37 ∨ 40 ≤ ↑i → i ≠ CollisionTest.scaled → i ≠ CollisionTest.good → y.regs i = x.regs i) ∧ ∀ a < x.regs CountCall.scratch, y.mem a = x.mem a

Execute a complete three-set collision query within 34(n₀+n₁+n₂)+15M+85 instructions. Multiplication fits are bounded by nⱼ²·card, independently of the actual input collision count. The final halt is excluded.