Copying the final encoding to its fixed output block

Main results

• Encoding.exec_copyOut: reuse the native array copy, including equal blocks and both possible disjoint address orders, with its charged 7n+4 bound.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.exec_copyOut {w : ℕ} (x : WordRAM.Data 32) (h1 : WordRAM.Fits w 1) (hs : WordRAM.Fits w (x.regs src + x.regs capacity)) (hd : WordRAM.Fits w (x.regs output + x.regs capacity)) (hdisj : x.regs src + x.regs capacity ≤ x.regs output ∨ x.regs output + x.regs capacity ≤ x.regs src ∨ x.regs src = x.regs output) : ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin w copyOut x y (7 * x.regs capacity + 4) ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem (x.regs src) (x.regs output) (x.regs capacity) ∧ ∀ (i : Fin 32), i ≠ cell → i ≠ address → i ≠ accumulator → i ≠ one → y.regs i = x.regs i

The final copy uses seven instructions per output word plus four instructions of setup and loop termination. Equal source/output blocks are permitted, so odd and even depths use the same fixed program. All other registers retain their values.