Three charged original-input copies

The left and right raw matrices and every interleaved query occurrence are copied separately. Sources lie below the actual producer heap end. Only the destination spans are written; no caller catalogue, virtual window or unrelated allocation is cleared or copied.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.exec_copyInputs {W b A Q s t q : ℕ} (x : WordRAM.Data 320) (hb : x.regs Reg.base = b) (hA : x.regs Reg.area = A) (hQ : x.regs Reg.count = Q) (hs : x.regs Reg.left = s) (ht : x.regs Reg.right = t) (hq : x.regs Reg.queries = q) (hsb : s + A ≤ b) (htb : t + A ≤ b) (hqb : q + 2 * Q ≤ b) (hfit : WordRAM.Fits W (2 * b + 2 * A + 2 * Q + 64)) : ∃ (y : WordRAM.Data 320), WordRAM.ExecWithin W copyInputs x y (14 * A + 14 * Q + 21) ∧ (∀ a < A, y.mem (b + 5 + a) = x.mem (s + a)) ∧ (∀ a < A, y.mem (b + 5 + A + a) = x.mem (t + a)) ∧ (∀ a < 2 * Q, y.mem (b + 5 + 2 * A + a) = x.mem (q + a)) ∧ (∀ (a : ℕ), a < b + 5 ∨ b + 5 + 2 * A + 2 * Q ≤ a → y.mem a = x.mem a) ∧ ∀ (i : Fin 320), ↑i < 96 → i ≠ Reg.address → y.regs i = x.regs i

All three original arrays are copied with native loops, at fourteen instructions per matrix cell/query pair plus constant argument and loop overhead.