Complete record-to-original-input preparation

All runtime metadata is read by the real descriptor code. The logarithm, five original-header stores and three native array copies compose to linear preparation work. The readback premises here are internal; the producer client derives them from the actual prepared instance.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.exec_prepare {W b m n i out rho piece s t q : ℕ} (X : Matrix (Fin n) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin n) ℤ) (qs : List (Fin n × Fin n)) (x : WordRAM.Data 320) (hD : x.mem 1 = MatrixMultiplication.Schonhage.D m) (hn : x.mem 3 = n) (hi : x.regs Reg.ordinal = i) (hout : x.regs 39 = out) (hb : x.regs 42 = b) (hrec : out + i * (6 + 2 * (n * MatrixMultiplication.Schonhage.D m)) + 6 ≤ b) (hrecord : { base := out + i * (6 + 2 * (n * MatrixMultiplication.Schonhage.D m)), length := 6 }.Realizes x.mem ![rho, piece, q, qs.length, s, t]) (hsb : s + n * MatrixMultiplication.Schonhage.D m ≤ b) (htb : t + n * MatrixMultiplication.Schonhage.D m ≤ b) (hqb : q + 2 * qs.length ≤ b) (hleft : ∀ a < n * MatrixMultiplication.Schonhage.D m, x.mem (s + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem (5 + a)) (hright : ∀ a < n * MatrixMultiplication.Schonhage.D m, x.mem (t + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem (5 + n * MatrixMultiplication.Schonhage.D m + a)) (hqueries : ∀ a < 2 * qs.length, x.mem (q + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem (5 + 2 * (n * MatrixMultiplication.Schonhage.D m) + a)) (hfit : WordRAM.Fits W (2 * b + 2 * (n * MatrixMultiplication.Schonhage.D m) + 2 * qs.length + 20 * m + MatrixMultiplication.Schonhage.D m + n + 256)) : ∃ (y : WordRAM.Data 320), WordRAM.ExecWithin W prepare x y (8 * m + 14 * (n * MatrixMultiplication.Schonhage.D m) + 14 * qs.length + 69) ∧ y.regs Reg.base = b ∧ (∀ a < MatrixMultiplication.Schonhage.QueriedProduct.inputEnd m n qs.length, y.mem (b + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem a) ∧ (∀ (a : ℕ), a < b ∨ b + MatrixMultiplication.Schonhage.QueriedProduct.inputEnd m n qs.length ≤ a → y.mem a = x.mem a) ∧ ∀ (j : Fin 320), ↑j < 65 → y.regs j = x.regs j

Complete native preparation from a selected record and its actual three source spans. No source execution, encoded matrix or routing table is supplied.