Executing the native shared traversal layout

The controller copies computed parameters, doubles the actual magnitude, divides the common packed length into four-cell groups and computes the explicit stack reservation by instructions.

Main results

• setupTraversal_exec: actual nineteen-instruction layout setup and exact native controls.

The native layout and composition proof are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.setupTraversal_exec {κ n w : ℕ} (x : WordRAM.Data 128) (hs : Saved κ n x) (hc : x.regs (primeRegisters PrimeTable.count) = (ThreeSum.ChanHe.mPar n (2 * (n + 2) ^ κ)).primesLE.card) (hfit : WordRAM.Fits w ((arena κ n x.mem).floor + (arena κ n x.mem).U + (arena κ n x.mem).N + (arena κ n x.mem).fuel + 16)) : ∃ (y : WordRAM.Data 128), WordRAM.Exec w setupTraversal x y 19 ∧ Saved κ n y ∧ (arena κ n x.mem).Controls y ∧ y.regs Traversal.outputCount = 0 ∧ y.regs power = 1 ∧ y.regs remaining = ThreeSum.ChanHe.fuel n + 1 ∧ y.regs scalar = 3 ∧ y.mem = x.mem

Execute all shared traversal arguments, constants and explicit-stack reservations.