Disjoint memory layout for complete native Chan–He node construction

Three supplied signed input arrays precede base. The allocated block consists of three count-prefixed heavy arrays (capacities n₀,n₁,n₂), the 4N packed cells, a reusable residue array of capacity n₀+n₁+n₂, and M histogram cells. Empty arrays still have a count cell.

Main definitions

• NodePacking.Layout: concrete bases and a polynomial resource envelope.

References

This memory layout is an original implementation choice.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout : Type

Runtime sizes and the fresh allocation base for one complete node.

• base : ℕ

  The input arrays end no later than this address.

• n : Fin 3 → ℕ

  The three supplied input lengths.

• N : ℕ

  Common number of groups; the packed output has 4N cells.

• M : ℕ

  Positive modulus, supplied by the parent prime search.

• U : ℕ

  Bound on the magnitudes of this node's inputs.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.total (L : Layout) : ℕ

Total input capacity, shared by the reusable residue workspace.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.descriptor (L : Layout) (j : Fin 3) : ℕ

Count cell immediately preceding a compact heavy array.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.heavy (L : Layout) (j : Fin 3) : ℕ

Compact heavy output data starts one cell after its count.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.packed (L : Layout) : ℕ

All three compact output capacities precede the packed array.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.scratch (L : Layout) : ℕ

A reusable residue array, after every permanent output.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.hist (L : Layout) : ℕ

A reusable histogram, after the full residue capacity.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.endpoint (L : Layout) : ℕ

One-past-end address of the complete allocated block.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.gap (L : Layout) : ℕ

The ordinary one-array tag, 3(2U+1)+1.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.tag (L : Layout) (j : Fin 3) : ℕ

Positive tag for the selected packed column.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.budget (L : Layout) : ℕ

Polynomial envelope for all addresses, signed values, encodings and histogram counters. Its fixed constant also covers code labels and all setup constants.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.n_le_total (L : Layout) (j : Fin 3) : L.n j ≤ L.total

Each input fits the reusable residue capacity.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.heavy_end_le_packed (L : Layout) (j : Fin 3) : L.heavy j + L.n j ≤ L.packed

All three compact arrays and their count cells are disjoint, with the packed array next.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.base_le_descriptor (L : Layout) (j : Fin 3) : L.base ≤ L.descriptor j

Every descriptor is inside its allocated output prefix.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.descriptor_lt_packed (L : Layout) (j : Fin 3) : L.descriptor j < L.packed

Every descriptor precedes the packed array, including for empty inputs.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.endpoint_eq (L : Layout) : L.endpoint = L.base + 3 + 2 * L.total + 4 * L.N + L.M

The allocated endpoint has a linear size formula.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.next_descriptor (L : Layout) : L.heavy 0 + L.n 0 = L.descriptor 1 ∧ L.heavy 1 + L.n 1 = L.descriptor 2 ∧ L.heavy 2 + L.n 2 = L.packed

Descriptor/capacity blocks end where the next one begins.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.bounds (L : Layout) : L.endpoint ≤ L.budget ∧ 120 * L.U + 80 ≤ L.budget ∧ L.base + L.total + L.M + L.N + L.U + 16 ≤ L.budget

Every address and padding/tag value is covered by one polynomial envelope.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.count_budget_le (L : Layout) (j : Fin 3) (src t : ℕ) (hs : src ≤ L.base) (ht : t ≤ 4 * L.gap) : src + L.scratch + L.hist + L.heavy j + L.packed + L.n j * L.n j + 2 * L.n j + L.M + 4 * L.N + 2 * t + 2 * L.U + 64 ≤ L.budget

The complete counting/placement call's budget is derived from the concrete node layout.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Layout.tag_bounds (L : Layout) (j : Fin 3) : L.U ≤ L.tag j ∧ L.tag j ≤ 4 * L.gap

All three tags are positive, dominate the input magnitude, and fit the common tag bound.