Exact output contract for complete native Chan–He node construction

The output uses the existing mathematical heavy subsets and Node.oneArray. A heavy array contains each selected integer once, preceded by its exact cardinality. The packed array has 4N cells, including every sentinel and padded cell. Memory outside the explicit allocation and caller registers 46–55 are preserved.

Main results

• NodePacking.exec_spec: complete native execution and exact semantic readback.
• NodePacking.Output.packed_square: exact native readback at the common 8m² length.
• NodePacking.abs_oneArray_le: the node magnitude bound is 60U+40.

These programs and composition proofs are original. The mathematical comparator is the existing Chan–He development; no host-level output is substituted for native execution.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Output (L : Layout) (values : Fin 3 → ℕ → ℤ) (before after : ℕ → ℕ) : Prop

Exact semantic readback from the concrete native allocation.

• heavy (j : Fin 3) : ∃ (zs : List ℤ), zs.Nodup ∧ zs.toFinset = ThreeSum.ChanHe.heavy (Finset.image (values j) (Finset.range (L.n j))) L.M ∧ after (L.descriptor j) = zs.length ∧ ∀ (k : ℕ) (hk : k < zs.length), after (L.heavy j + k) = WordRAM.Signed.encode zs[k]

  Each compact list enumerates precisely the existing heavy set, without duplicates.

• packed (u : ℕ) : u < 4 * L.N → after (L.packed + u) = WordRAM.Signed.encode ((node L values).oneArray L.U u)

  Every packed cell equals the existing mathematical node array.

• frame (a : ℕ) : a < L.base ∨ L.endpoint ≤ a → after a = before a

  All memory outside the fresh allocation retains its old contents.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.memory_output (L : Layout) (values : Fin 3 → ℕ → ℤ) (mem : ℕ → ℕ) (hM : 0 < L.M) (hN : 2 * L.M ≤ L.N) (hinj : ∀ (j : Fin 3), Set.InjOn (values j) ↑(Finset.range (L.n j))) : Output L values mem (memory L values mem)

Exact readback of the fully composed memory theorem.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Output.heavy_card {L : Layout} {values : Fin 3 → ℕ → ℤ} {before after : ℕ → ℕ} (h : Output L values before after) (j : Fin 3) : after (L.descriptor j) = (ThreeSum.ChanHe.heavy (Finset.image (values j) (Finset.range (L.n j))) L.M).card

The native descriptor is the cardinality of the existing heavy set.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.exec_spec {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 (256 * ((layout x).total + (layout x).M + (layout x).N + 1)) ∧ Output (layout x) values x.mem y.mem ∧ Parameters x y

The complete fixed native program constructs all three exact heavy outputs and the exact packed node array, charging setup, clearing, padding, signed tags, every address and count store, and every actual residue/histogram call. Initial output and scratch contents are arbitrary.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.bdd_image (L : Layout) (values : Fin 3 → ℕ → ℤ) (hbdd : ∀ (j : Fin 3), ∀ i < L.n j, (values j i).natAbs ≤ L.U) (j : Fin 3) : ThreeSum.Bdd L.U (Finset.image (values j) (Finset.range (L.n j)))

The supplied magnitude bound transfers to the existing finite-set notion.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.abs_oneArray_le (L : Layout) (values : Fin 3 → ℕ → ℤ) (hbdd : ∀ (j : Fin 3), ∀ i < L.n j, (values j i).natAbs ≤ L.U) (u : ℕ) : |(node L values).oneArray L.U u| ≤ 60 * ↑L.U + 40

The existing mathematical output bound applies to every native packed value.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Output.packed_square {L : Layout} {values : Fin 3 → ℕ → ℤ} {before after : ℕ → ℕ} (h : Output L values before after) {m : ℕ} (hN : L.N = 2 * m ^ 2) {u : ℕ} (hu : u < 8 * m ^ 2) : after (L.packed + u) = WordRAM.Signed.encode ((node L values).oneArray L.U u)

Exact readback at the full preprocessing's common length, with no extra padding assumption.