Charged copies across the producer/consumer boundary

Main results

• QueriedProduct.exec_copyCall: real argument setup and the unchanged dynamic native copy, with both address orders, equality, complete memory meaning and caller-register frame.

These are internal execution interfaces. Complete product clients derive the numerical fits and separation from the original input and the explicit computed layout.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.bank_injective : Function.Injective bank

Each existing 96-register callee has exactly its original register semantics.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_copyCall {w : ℕ} (x : WordRAM.Data 160) (h1 : WordRAM.Fits w 1) (hs : WordRAM.Fits w (x.regs source + x.regs length)) (hd : WordRAM.Fits w (x.regs destination + x.regs length)) (hsep : x.regs source + x.regs length ≤ x.regs destination ∨ x.regs destination + x.regs length ≤ x.regs source ∨ x.regs source = x.regs destination) : ∃ (y : WordRAM.Data 160), WordRAM.ExecWithin w copyCall x y (7 * x.regs length + 7) ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem (x.regs source) (x.regs destination) (x.regs length) ∧ ∀ (i : Fin 160), 7 ≤ ↑i → y.regs i = x.regs i

Dynamic native argument setup and every copy instruction are charged. The caller's source/destination/length registers, and every register beyond the seven-register callee, are preserved. Source and destination separation is a numerical layout obligation.