Native frontend array and descriptor execution

Main results

The compact scan contract is composed with every array setup and descriptor store.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.budget (l : Layout) (U : ℕ) : ℕ

Local arithmetic budget covers array addresses, native labels and loop setup.

structure Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.ScanReady (w : ℕ) (rs : List (ℕ × ℕ)) (x : WordRAM.Data 48) : Prop

The hypotheses of a concrete compact scan, before choosing its bit coordinates and mode.

• length : x.regs Scan.len = rs.length

  The source length is the distinct-key count.

• 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

  Native small constants.

• keys : WordRAM.Block.HoldsList (x.regs Scan.keys) (List.map Prod.fst rs) x.mem

  Both radix arrays have exact contents.

• counts : WordRAM.Block.HoldsList (x.regs Scan.counts) (List.map Prod.snd rs) x.mem
• words (p : ℕ × ℕ) : p ∈ rs → WordRAM.Fits w p.1

  Every key and the native label arithmetic fit.

• absolute (p : ℕ × ℕ) : p ∈ rs → p.1 / 2 ≤ 2 * x.regs Select.magnitude
• double (p : ℕ × ℕ) : p ∈ rs → WordRAM.Fits w (2 * p.1)
• labels : WordRAM.Fits w (4 * x.regs Select.magnitude + 2)
• small : WordRAM.Fits w 5
• keyAddress : WordRAM.Fits w (x.regs Scan.keys + rs.length)

  Source and output endpoints fit.

• countAddress : WordRAM.Fits w (x.regs Scan.counts + rs.length)
• outputAddress : WordRAM.Fits w (x.regs Scan.dst + rs.length + 1)
• keysBefore : x.regs Scan.keys + rs.length ≤ x.regs Scan.dst

  Both source blocks precede the output.

• countsBefore : x.regs Scan.counts + rs.length ≤ x.regs Scan.dst

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.ScanParametersPreserved (x y : WordRAM.Data 48) : Prop

Parameters changed by split/mode setup.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.ScanReady.transfer {w : ℕ} {rs : List (ℕ × ℕ)} {x y : WordRAM.Data 48} (h : ScanReady w rs x) (he : ScanParametersPreserved x y) : ScanReady w rs y

A mode/bit setup preserves every actual scan precondition.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.ScanReady.exec {w : ℕ} {rs : List (ℕ × ℕ)} {x : WordRAM.Data 48} (h : ScanReady w rs x) : ∃ (y : WordRAM.Data 48), WordRAM.ExecWithin w Scan.program x y (43 * rs.length + 4) ∧ WordRAM.Block.HoldsList (x.regs Scan.dst) (Math.select (x.regs Select.magnitude) (x.regs Select.beta) (x.regs Select.beta') (x.regs Select.digit) (x.regs Select.mode) rs) y.mem ∧ y.regs Scan.out = (Math.select (x.regs Select.magnitude) (x.regs Select.beta) (x.regs Select.beta') (x.regs Select.digit) (x.regs Select.mode) rs).length ∧ WordRAM.Modifies { base := x.regs Scan.dst, length := rs.length }.footprint x.mem y.mem ∧ ∀ (j : Fin 48), WordRAM.Code.Preserves j Scan.body → y.regs j = x.regs j

Invoke the proved native scan from its actual arithmetic/layout context.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.pick_exec {w U Λ j : ℕ} (x : WordRAM.Data 48) (rs : List (ℕ × ℕ)) (h : ScanReady w rs x) (hU : x.regs Select.magnitude = U) (hΛ : x.regs digits = Λ) (hs : x.regs splits = 2 * Λ ^ 2) (ht : x.regs triple = j / 3) (hslot : x.regs slot = j % 3) (hjfit : WordRAM.Fits w j) : ∃ (y : WordRAM.Data 48), WordRAM.ExecWithin w pick x y (43 * rs.length + 20) ∧ WordRAM.Block.HoldsList (x.regs Scan.dst) (Math.array U Λ rs j) y.mem ∧ y.regs Scan.out = (Math.array U Λ rs j).length ∧ WordRAM.Modifies { base := x.regs Scan.dst, length := rs.length + 1 }.footprint x.mem y.mem

Select exactly the array named by one physical slot. Every split/multiplicity setup is executed; the width and label budget are scalar runtime values, independent of code size.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Arrays.body_exec {w U Λ j : ℕ} (x : WordRAM.Data 48) (rs : List (ℕ × ℕ)) (hready : ScanReady w rs (x.set Scan.dst (x.regs heap))) (hU : x.regs Select.magnitude = U) (hΛ : x.regs digits = Λ) (hs : x.regs splits = 2 * Λ ^ 2) (hj : x.regs current = j) (hcap : rs.length + 1 ≤ x.regs capacity) (hbefore : x.regs descriptors + 2 * j + 2 ≤ x.regs heap) (ha : WordRAM.Fits w (x.regs descriptors + 2 * j + 2)) (hh : WordRAM.Fits w (x.regs heap + x.regs capacity)) (hi : WordRAM.Fits w (j + 1)) : ∃ (y : WordRAM.Data 48), WordRAM.ExecWithin w body x y (43 * rs.length + 30) ∧ y.regs current = j + 1 ∧ y.regs heap = x.regs heap + x.regs capacity ∧ y.mem (x.regs descriptors + 2 * j) = (Math.array U Λ rs j).length ∧ y.mem (x.regs descriptors + 2 * j + 1) = x.regs heap ∧ WordRAM.Block.HoldsList (x.regs heap) (Math.array U Λ rs j) y.mem ∧ ∀ (a : ℕ), a < x.regs heap ∨ x.regs heap + x.regs capacity ≤ a → a ≠ x.regs descriptors + 2 * j → a ≠ x.regs descriptors + 2 * j + 1 → y.mem a = x.mem a

One complete array, its exact descriptor words, allocation advance and local frame.