Native frontend descriptor layout

Descriptors have six words, three consecutive (length,pointer) pairs. Arrays occupy disjoint blocks of capacity n+1; unused capacity is outside the compact enumeration. The first four n-word blocks remain reserved for radix sorting and full multiplicities.

Main definitions

• Layout: concrete descriptor and payload addresses.
• array: the compact list represented by one array slot.
• Output: exact descriptor words and payload readback, including empty arrays.

structure Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Layout : Type

Concrete layout at input length n and runtime label-bit budget Λ.

• n : ℕ

  Input length.

• digits : ℕ

  Number of label bits.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Layout.splits (l : Layout) : ℕ

Number of bit-split triples.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Layout.count (l : Layout) : ℕ

Total descriptor count, including the two multiplicity triples.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Layout.arrays (l : Layout) : ℕ

Total compact array count.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Layout.capacity (l : Layout) : ℕ

Capacity allows singleton zero even when the original input is empty.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Layout.descriptors (l : Layout) : ℕ

Descriptor table follows all four radix buffers.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Layout.payloads (l : Layout) : ℕ

Payload blocks follow the complete descriptor table.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Layout.pointer (l : Layout) (j : ℕ) : ℕ

Pointer for array slot j.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Layout.endpoint (l : Layout) : ℕ

One-past-end address of all allocated blocks.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Layout.pointer_succ (l : Layout) (j : ℕ) : l.pointer (j + 1) = l.pointer j + l.capacity

Payload pointers advance by the full reserved capacity.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Layout.pointer_mono (l : Layout) {i j : ℕ} (h : i ≤ j) : l.pointer i ≤ l.pointer j

Payload blocks occur in allocation order.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Layout.descriptor_before (l : Layout) {j : ℕ} (hj : j < l.arrays) (i : ℕ) : l.descriptors + 2 * j + 2 ≤ l.pointer i

Every descriptor word precedes every payload block.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.mode (Λ j : ℕ) : ℕ

Selection mode for a physical array slot.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.beta (Λ j : ℕ) : ℕ

Bit coordinates of a physical slot in the split part of the table.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.beta' (Λ j : ℕ) : ℕ

Bit coordinates of a physical slot in the split part of the table.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.digit (j : ℕ) : ℕ

Bit coordinates of a physical slot in the split part of the table.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.array (U Λ : ℕ) (rs : List (ℕ × ℕ)) (j : ℕ) : List ℕ

Compact encoded list for one physical array slot.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.select_extra (U β β' v mode : ℕ) (rs : List (ℕ × ℕ)) (hm : 3 ≤ mode) : select U β β' v mode rs = select U 0 0 0 mode rs

The two bit coordinates are irrelevant in the three nonsplitting scan modes.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.array_split (U Λ : ℕ) (rs : List (ℕ × ℕ)) (t s : ℕ) (ht : t < 2 * Λ ^ 2) (hs : s < 3) : array U Λ rs (3 * t + s) = select U (t / 2 / Λ) (t / 2 % Λ) (t % 2) s rs

Physical array slots within a split triple follow A, B₀, B₁ order.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.root (U Λ : ℕ) (rs : List (ℕ × ℕ)) (t : ℕ) : List ℕ × List ℕ × List ℕ

Read the three array specifications belonging to a descriptor.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.root_split (U Λ : ℕ) (rs : List (ℕ × ℕ)) (t : ℕ) (ht : t < 2 * Λ ^ 2) : root U Λ rs t = (select U (t / 2 / Λ) (t / 2 % Λ) (t % 2) 0 rs, select U (t / 2 / Λ) (t / 2 % Λ) (t % 2) 1 rs, select U (t / 2 / Λ) (t / 2 % Λ) (t % 2) 2 rs)

A descriptor in the split prefix has exactly the requested three compact selections.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.root_extras (U Λ : ℕ) (rs : List (ℕ × ℕ)) : root U Λ rs (2 * Λ ^ 2) = (select U 0 0 0 3 rs, [0], select U 0 0 0 5 rs) ∧ root U Λ rs (2 * Λ ^ 2 + 1) = (select U 0 0 0 4 rs, [0], [0])

The two final descriptors retain their singleton zeros and exact multiplicity scans.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.length_array_le (U Λ : ℕ) (rs : List (ℕ × ℕ)) (j : ℕ) : (array U Λ rs j).length ≤ rs.length + 1

Every array fits in its n+1 capacity, including empty-input singleton zeros.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.array_nodup (U Λ : ℕ) {rs : List (ℕ × ℕ)} (h : (List.map Prod.fst rs).Nodup) (j : ℕ) : (array U Λ rs j).Nodup

Every descriptor represents an injective enumeration.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.array_values {input : List ℤ} {rs : List (ℕ × ℕ)} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (U Λ j u : ℕ) (hu : u ∈ array U Λ rs j) : u = 0 ∨ ∃ z ∈ input, u = WordRAM.Signed.encode z ∨ u = WordRAM.Signed.encode (2 * z)

Each output word is canonical zero, an original input key, or the key of twice an input.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.array_canonical {input : List ℤ} {rs : List (ℕ × ℕ)} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (U Λ j u : ℕ) (hu : u ∈ array U Λ rs j) : WordRAM.Signed.encode (WordRAM.Signed.decode u) = u

Every compact output word is a canonical signed encoding.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.array_decoded_nodup {input : List ℤ} {rs : List (ℕ × ℕ)} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (h : (List.map Prod.fst rs).Nodup) (U Λ j : ℕ) : (List.map WordRAM.Signed.decode (array U Λ rs j)).Nodup

Injectivity holds for the represented integer array, as well as its native keys.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.array_magnitude {input : List ℤ} {rs : List (ℕ × ℕ)} {U : ℕ} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (hvalues : ∀ z ∈ input, |z| ≤ ↑U) (Λ j u : ℕ) (hu : u ∈ array U Λ rs j) : |WordRAM.Signed.decode u| ≤ ↑(2 * U)

Every decoded payload integer has the exact reduction's common magnitude bound 2U.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.roots (U : ℕ) (rs : List (ℕ × ℕ)) : List (List ℕ × List ℕ × List ℕ)

The compact root lists before their native layout is assigned.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.decodeRoot (T : List ℕ × List ℕ × List ℕ) : Finset ℤ × Finset ℤ × Finset ℤ

Decode a compact triple to the finite sets used by the existing reduction.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.roots_decoded {input : List ℤ} {rs : List (ℕ × ℕ)} {U : ℕ} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (hcounts : ∀ p ∈ rs, List.count p.1 (List.map WordRAM.Signed.encode input) = p.2) (hvalues : ∀ z ∈ input, |z| ≤ ↑U) : List.map decodeRoot (roots U rs) = ThreeSum.inputs U fun (i : Fin input.length) => input[i]

Exact list equality with ThreeSum.inputs, preserving root order and every empty array.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.roots_indexed (U : ℕ) (rs : List (ℕ × ℕ)) : have Λ := ThreeSum.labelBits (2 * U); List.map (root U Λ rs) (List.range (2 * Λ ^ 2 + 2)) = roots U rs

Physical descriptor indices have exactly the nested order of the finite root list.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Output (l : Layout) (U : ℕ) (rs : List (ℕ × ℕ)) (mem : ℕ → ℕ) : Prop

Exact descriptor and compact payload readback. Unused capacity is unrestricted.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.readArray (mem : ℕ → ℕ) (a : ℕ) : List ℕ

Follow one (length,pointer) pair in native memory. This is output interpretation, not an instruction or an assumed computation by the frontend.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.readRoots (l : Layout) (mem : ℕ → ℕ) : List (Finset ℤ × Finset ℤ × Finset ℤ)

Follow all six-word descriptors in order and decode their represented sets.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Output.read_array {l : Layout} {U : ℕ} {rs : List (ℕ × ℕ)} {mem : ℕ → ℕ} (h : Output l U rs mem) {j : ℕ} (hj : j < l.arrays) : readArray mem (l.descriptors + 2 * j) = Math.array U l.digits rs j

Exact slot readback includes zero-length arrays and ignores unused capacity.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Output.readback {n U : ℕ} {input : List ℤ} {rs : List (ℕ × ℕ)} {mem : ℕ → ℕ} (h : Output { n := n, digits := ThreeSum.labelBits (2 * U) } U rs mem) (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (hcounts : ∀ p ∈ rs, List.count p.1 (List.map WordRAM.Signed.encode input) = p.2) (hvalues : ∀ z ∈ input, |z| ≤ ↑U) : readRoots { n := n, digits := ThreeSum.labelBits (2 * U) } mem = ThreeSum.inputs U fun (i : Fin input.length) => input[i]

The descriptor table reads back as exactly the existing finite frontend list, in order.