Complete fixed native program for one Chan–He node

The source comparator is NodeArray.lean at anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5. The layout, native code and proofs are original. The source's Light machine is not imported.

Main definitions

• NodePacking.program: computes the layout and tags, pads every output cell, then performs three actual residue/histogram/extraction/placement calls, including all three count stores.

References

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

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.source (j : Fin 3) : Fin 64

The three supplied signed input bases.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.length (j : Fin 3) : Fin 64

The three supplied input lengths.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.base : Fin 64

Fresh allocation base after all input arrays.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.groups : Fin 64

Common number of four-cell groups.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.magnitude : Fin 64

Node input magnitude bound.

@[reducible, inline]

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

Positive modulus.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.scratch : Fin 64

Computed residue workspace base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.histogram : Fin 64

Computed histogram workspace base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.packed : Fin 64

Computed packed output base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.gap : Fin 64

Twice the gap G=6U+4, ready for sign-and-magnitude tagging.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.padding : Fin 64

Twice the padding magnitude W=2U+1.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.temporary : Fin 64

Setup scratch.

@[reducible, inline]

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

Constant one, retained across the complete calls.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.four : Fin 64

Constant four, retained across the complete calls.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.layout (x : WordRAM.Data 64) : Layout

The mathematical layout determined by the runtime parameters.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.paddingRegisters (i : Fin 10) : Fin 64

Padding workspace embedded below all persistent node parameters.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.pdst : Fin 64

Packed output base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.plen : Fin 64

Number of four-cell groups.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.pad0 : Fin 64

Padding word for column zero.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.pad1 : Fin 64

Padding word for column one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.pad2 : Fin 64

Padding word for column two.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.pad3 : Fin 64

Padding word for column three.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.layoutCode : WordRAM.Code WordRAM.Basis.standard 64

Compute every permanent and scratch block address in twelve native instructions.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.constantsCode : WordRAM.Code WordRAM.Basis.standard 64

Compute the exact positive encoded padding pattern, including all signed-negation/tag work. The third padding word uses subtraction because its integer contribution is -W.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.descriptorCode (j : Fin 3) : WordRAM.Code WordRAM.Basis.standard 64

Compute the selected heavy-array descriptor address. The choice is one of three fixed pieces of code, never a program whose size depends on an input length.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.tagCode (j : Fin 3) : WordRAM.Code WordRAM.Basis.standard 64

Deliver the exact encoded tag for one fixed column.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.distanceCode (j : Fin 3) : WordRAM.Code WordRAM.Basis.standard 64

Deliver the duplicated-Z distance; the other columns perform two coincident stores.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.prepare (j : Fin 3) : WordRAM.Code WordRAM.Basis.standard 64

Every runtime input and output parameter is explicitly delivered to the complete call.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.round (j : Fin 3) : WordRAM.Code WordRAM.Basis.standard 64

Complete one-set native round with charged setup and a written heavy count.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.initializeCode : WordRAM.Code WordRAM.Basis.standard 64

Complete charged address/tag/padding initialization.

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

Complete one-node preprocessing. This code is independent of n,w,M,N,U.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.preserves_parameters (i : Fin 64) (hi : 46 ≤ ↑i ∧ ↑i ≤ 55) : WordRAM.Code.Preserves i program

The original three input bases/lengths and base, length, magnitude and modulus parameters are preserved by the complete program.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.size_program_le : program.size ≤ 4096

The assembled code length has a fixed bound, independent of every runtime parameter.

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

The complete program is deterministic and never reads the word width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.isRandFree : program.IsRandFree

No instruction samples randomness or invokes an oracle.