Initialized-input native distinct-position frontend

The ABI has 128 registers. Radix uses 0–15; frontend locals use 16–63; the existing parameter program uses 64–87. Registers 88–90 return descriptor base, descriptor count and heap end. Each descriptor has six words (length, pointer) for its three compact injective arrays. Each array has capacity n+1, including the singleton zeros required when n=0.

Main definitions

• Arrays.program: native enumeration and descriptor construction.
• program: parameters, explicit-bit radix deduplication, and all frontend arrays.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.inputLen : Fin 48

Original input length and label-bit budget.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.digits : Fin 48

Original input length and label-bit budget.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.splits : Fin 48

Number of split triples, total triple count and total array count.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.triples : Fin 48

Number of split triples, total triple count and total array count.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.arrays : Fin 48

Number of split triples, total triple count and total array count.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.capacity : Fin 48

Capacity per compact array.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.heap : Fin 48

Next payload address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.descriptors : Fin 48

Descriptor table base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.current : Fin 48

Current array index, current triple and slot.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.triple : Fin 48

Current array index, current triple and slot.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.slot : Fin 48

Current array index, current triple and slot.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.temp : Fin 48

Arithmetic temporary and final heap endpoint.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.heapEnd : Fin 48

Arithmetic temporary and final heap endpoint.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.singleton : WordRAM.Code WordRAM.Basis.standard 48

Write the singleton-zero array, including on empty input.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.extra : WordRAM.Code WordRAM.Basis.standard 48

Compute the exact array selection mode for the two multiplicity triples.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.splitSetup : WordRAM.Code WordRAM.Basis.standard 48

Decode β, then β', then [false,true], and scan the indicated one of three arrays.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.split : WordRAM.Code WordRAM.Basis.standard 48

Split setup followed by the complete compacting scan.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.pick : WordRAM.Code WordRAM.Basis.standard 48

Native choice between the split prefix and the two multiplicity triples.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.writeDescriptor : WordRAM.Code WordRAM.Basis.standard 48

Write a compact array's two descriptor words and advance the allocation cursor.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.body : WordRAM.Code WordRAM.Basis.standard 48

One complete array and its two descriptor words.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.setup : WordRAM.Code WordRAM.Basis.standard 48

Initialize every constant, layout and cursor, then enumerate every array, including empties.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.program : WordRAM.Code WordRAM.Basis.standard 48

Setup and all array iterations.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.parameterRegisters (i : Fin 24) : Fin 128

Embed the 24-register parameter program above both native kernels.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.radixRegisters (i : Fin 16) : Fin 128

Embed the 16-register radix program in the low registers.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.arrayRegisters (i : Fin 48) : Fin 128

Embed the 48-register frontend program between radix and parameters.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.descriptorBase : Fin 128

Final descriptor base, descriptor count and one-past-end payload address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.descriptorCount : Fin 128

Final descriptor base, descriptor count and one-past-end payload address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.heapEnd : Fin 128

Final descriptor base, descriptor count and one-past-end payload address.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.radixSetup : WordRAM.Code WordRAM.Basis.standard 128

Setup for the lower-level sorter with the magnitude-derived bit bound, never physical width.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.arraySetup : WordRAM.Code WordRAM.Basis.standard 128

Transfer actual parameters and radix outputs into the concrete frontend ABI.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.finish : WordRAM.Code WordRAM.Basis.standard 128

Return metadata while preserving parameter outputs and full radix key/count arrays.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.construct : WordRAM.Code WordRAM.Basis.standard 128

Native frontend after the existing complete parameter program.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.program (κ : ℕ) : WordRAM.Code WordRAM.Basis.standard 128

One finite native program for each fixed polynomial magnitude exponent.