Saving the actual frontend and parameter outputs

The outer controller retains every shared scalar in registers outside the complete root program's write set. These are copies of computed frontend results, not inputs supplied by a caller.

Main definitions

• Saved: exact native outer metadata after the snapshot instructions.

Main results

• snapshot_exec: execute all thirteen scalar copies and constant initializations.

The native ABI and composition proof are original.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.Saved (κ n : ℕ) (x : WordRAM.Data 128) : Prop

Exact computed metadata retained outside the root program's register bank.

• base : x.regs descriptors = (Frontend.layout κ n).descriptors

  Descriptor table and count produced by the frontend.

• count : x.regs roots = (Frontend.layout κ n).count
• fuel : x.regs levels = ThreeSum.ChanHe.fuel n

  Exact numeric parameter outputs.

• magnitude : x.regs inputMagnitude = (n + 2) ^ κ
• limit : x.regs candidateLimit = ThreeSum.ChanHe.mPar n (2 * (n + 2) ^ κ)
• digits : x.regs labels = (Frontend.layout κ n).digits
• length : x.regs packedLength = 8 * ThreeSum.ChanHe.mPar n (2 * (n + 2) ^ κ) ^ 2
• endpoint : x.regs firstFree = (Frontend.layout κ n).endpoint
• index : x.regs current = 0

  Actual index and small constants.

• stride : x.regs Preprocessing.stride = 6
• one : x.regs Preprocessing.one = 1
• zero : x.regs Preprocessing.zero = 0
• four : x.regs Preprocessing.four = 4

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.Saved.congr {κ n : ℕ} {x y : WordRAM.Data 128} (h : Saved κ n x) (hr : ∀ (i : Fin 128), 109 ≤ ↑i → ↑i ≤ 120 ∨ ↑i = 126 → y.regs i = x.regs i) : Saved κ n y

Programs restricted to lower registers retain all computed outer metadata.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.snapshot_exec {κ n w : ℕ} (x : WordRAM.Data 128) (hp : Parameters.Output n ((n + 2) ^ κ) (WordRAM.Data.comap Frontend.parameterRegisters x)) (hb : x.regs Frontend.descriptorBase = (Frontend.layout κ n).descriptors) (hc : x.regs Frontend.descriptorCount = (Frontend.layout κ n).count) (he : x.regs Frontend.heapEnd = (Frontend.layout κ n).endpoint) (h6 : WordRAM.Fits w 6) : ∃ (y : WordRAM.Data 128), WordRAM.Exec w snapshot x y 13 ∧ Saved κ n y ∧ y.mem = x.mem

Saving computed scalars and initializing the outer constants changes no memory.