Complete native Chan–He node construction

The parent supplies three injective signed-encoded input arrays ending before a fresh allocation base, a positive modulus M, N ≥ 2M, and magnitude bound U. The fixed native program computes all residues/histograms, the three exact compact heavy arrays and the existing Node.oneArray in 4N cells. Initialization, tags, address calculations, all called code and count stores are charged. A single polynomial envelope derives every arithmetic/address fit.

Main results

• NodePacking.exec: complete native execution in 66(n₀+n₁+n₂)+15M+12N+228 instructions.
• NodePacking.time_le_linear: a uniform linear instruction bound.

Prime selection, the frontend, recursion, global State.init composition and the global width and preprocessing asymptotics remain the responsibility of the parent construction.

References

• T. M. Chan and Q. He, Reducing 3SUM to Convolution-3SUM

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.exec {w : ℕ} (x : WordRAM.Data 64) (values : Fin 3 → ℕ → ℤ) (hM : 0 < (layout x).M) (hN : 2 * (layout x).M ≤ (layout x).N) (hwidth : GenericRAM.Signed.Fits w ↑(layout x).budget) (hsrc : ∀ (j : Fin 3), x.regs (source j) + (layout x).n j ≤ (layout x).base) (hbdd : ∀ (j : Fin 3), ∀ i < (layout x).n j, (values j i).natAbs ≤ (layout x).U) (hinput : ∀ (j : Fin 3), ∀ i < (layout x).n j, x.mem (x.regs (source j) + i) = WordRAM.Signed.encode (values j i)) (hinj : ∀ (j : Fin 3), Set.InjOn (values j) ↑(Finset.range ((layout x).n j))) : ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin (w + 2) program x y (66 * (layout x).total + 15 * (layout x).M + 12 * (layout x).N + 228) ∧ y.mem = memory (layout x) values x.mem ∧ Parameters x y

Complete node work, with only actual supplied array contents and one explicit polynomial width envelope as premises. The instruction bound excludes the final halt.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.time_le_linear (L : Layout) : 66 * L.total + 15 * L.M + 12 * L.N + 228 ≤ 256 * (L.total + L.M + L.N + 1)

The complete charged bound is uniformly linear in input lengths, modulus and output length.