Complete descriptor-table execution

The invariant retains every completed descriptor and compact payload, both full radix arrays, and all memory outside the allocated frontend region.

Main results

The enumeration loop charges each native array scan, descriptor store and allocation advance.

structure Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.Registers (l : Layout) (U k : ℕ) (x : WordRAM.Data 48) : Prop

Immutable registers of the complete enumeration loop.

• magnitude : x.regs Select.magnitude = U

  Original magnitude promise.

• inputLen : x.regs Arrays.inputLen = l.n

  Original input length and explicit bit budget.

• digits : x.regs Arrays.digits = l.digits
• keys : x.regs Scan.keys = 1 + 2 * l.n

  Exact radix key/count pointers and distinct-key length.

• counts : x.regs Scan.counts = 1 + 3 * l.n
• len : x.regs Scan.len = k
• splits : x.regs Arrays.splits = l.splits

  Computed layout values.

• triples : x.regs Arrays.triples = l.count
• arrays : x.regs Arrays.arrays = l.arrays
• capacity : x.regs Arrays.capacity = l.capacity
• descriptors : x.regs Arrays.descriptors = l.descriptors
• heapEnd : x.regs Arrays.heapEnd = l.endpoint
• constants : x.regs Select.zero = 0 ∧ x.regs Select.one = 1 ∧ x.regs Select.two = 2 ∧ x.regs Select.three = 3 ∧ x.regs Select.four = 4 ∧ x.regs Select.five = 5

  All small constants are real native registers.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.Registers.transfer {l : Layout} {U k : ℕ} {x y : WordRAM.Data 48} (h : Registers l U k x) (hr : ∀ (i : Fin 48), WordRAM.Code.Preserves i body → y.regs i = x.regs i) : Registers l U k y

The body preserves every immutable layout and source register.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.layout_bounds (l : Layout) (U : ℕ) : l.n + 1 ≤ budget l U ∧ l.digits * l.digits ≤ budget l U ∧ l.splits ≤ budget l U ∧ l.count ≤ budget l U ∧ l.arrays ≤ budget l U ∧ 2 * l.arrays ≤ budget l U ∧ l.payloads ≤ budget l U ∧ l.arrays * l.capacity ≤ budget l U ∧ l.endpoint ≤ budget l U ∧ 4 * U + 2 ≤ budget l U ∧ 5 ≤ budget l U

Every layout scalar and partial allocation is below the explicit arithmetic budget.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.setup_exec {w U : ℕ} (l : Layout) (k : ℕ) (x : WordRAM.Data 48) (hU : x.regs Select.magnitude = U) (hn : x.regs inputLen = l.n) (hΛ : x.regs digits = l.digits) (hk : x.regs Scan.keys = 1 + 2 * l.n) (hc : x.regs Scan.counts = 1 + 3 * l.n) (hlen : x.regs Scan.len = k) (hd : x.regs descriptors = l.descriptors) (hfit : WordRAM.Fits w (budget l U)) : ∃ (y : WordRAM.Data 48), WordRAM.ExecWithin w setup x y 19 ∧ Registers l U k y ∧ y.regs current = 0 ∧ y.regs heap = l.pointer 0 ∧ y.mem = x.mem

Setup computes all constants and addresses with actual instructions, preserving all memory.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.loop_exec {w U : ℕ} (l : Layout) (rs : List (ℕ × ℕ)) (x : WordRAM.Data 48) (hr : Registers l U rs.length x) (hidx : x.regs current = 0) (hheap : x.regs heap = l.pointer 0) (hlen : rs.length ≤ l.n) (hk : WordRAM.Block.HoldsList (1 + 2 * l.n) (List.map Prod.fst rs) x.mem) (hc : WordRAM.Block.HoldsList (1 + 3 * l.n) (List.map Prod.snd rs) x.mem) (hkeys : ∀ p ∈ rs, p.1 ≤ 2 * U + 1 ∧ p.1 / 2 ≤ U) (hfit : WordRAM.Fits w (budget l U)) : ∃ (y : WordRAM.Data 48), WordRAM.ExecWithin w (WordRAM.Code.loop (WordRAM.Cond.lt current arrays) body) x y (l.arrays * (43 * rs.length + 32) + 2) ∧ Output l U rs y.mem ∧ y.regs current = l.arrays ∧ y.regs heap = l.endpoint ∧ Registers l U rs.length y ∧ WordRAM.Block.HoldsList (1 + 2 * l.n) (List.map Prod.fst rs) y.mem ∧ WordRAM.Block.HoldsList (1 + 3 * l.n) (List.map Prod.snd rs) y.mem ∧ WordRAM.Modifies { base := l.descriptors, length := l.endpoint - l.descriptors }.footprint x.mem y.mem

All compact arrays and six-word descriptors are produced by the complete native loop.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.exec {w U : ℕ} (l : Layout) (rs : List (ℕ × ℕ)) (x : WordRAM.Data 48) (hU : x.regs Select.magnitude = U) (hn : x.regs inputLen = l.n) (hΛ : x.regs digits = l.digits) (hkreg : x.regs Scan.keys = 1 + 2 * l.n) (hcreg : x.regs Scan.counts = 1 + 3 * l.n) (hlenreg : x.regs Scan.len = rs.length) (hd : x.regs descriptors = l.descriptors) (hlen : rs.length ≤ l.n) (hk : WordRAM.Block.HoldsList (1 + 2 * l.n) (List.map Prod.fst rs) x.mem) (hc : WordRAM.Block.HoldsList (1 + 3 * l.n) (List.map Prod.snd rs) x.mem) (hkeys : ∀ p ∈ rs, p.1 ≤ 2 * U + 1 ∧ p.1 / 2 ≤ U) (hfit : WordRAM.Fits w (budget l U)) : ∃ (y : WordRAM.Data 48), WordRAM.ExecWithin w program x y (l.arrays * (43 * rs.length + 32) + 21) ∧ Output l U rs y.mem ∧ Registers l U rs.length y ∧ y.regs heap = l.endpoint ∧ WordRAM.Block.HoldsList (1 + 2 * l.n) (List.map Prod.fst rs) y.mem ∧ WordRAM.Block.HoldsList (1 + 3 * l.n) (List.map Prod.snd rs) y.mem ∧ WordRAM.Modifies { base := l.descriptors, length := l.endpoint - l.descriptors }.footprint x.mem y.mem

Complete array/descriptor construction, including all native constant and layout setup.