Actual record selection and depth recovery #
These internal lemmas account for the actual original-header and six descriptor loads, every stride/address calculation, and the existing floor-logarithm loop. The final producer client derives each loaded word from its actual readback theorem.
theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.exec_logarithm {W m : ℕ} (x : WordRAM.Data 320) (hD : x.regs Reg.source = 4 ^ m) (hfit : WordRAM.Fits W (4 ^ m + 2 * m + 3)) :
The computed logarithm is read from the actual existing loop, with no logarithm input
certificate. Its charge is 8m+5 at a power of four.
theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.exec_readRecord {W n D i out b : ℕ} (x : WordRAM.Data 320) (v : Fin 6 → ℕ) (hD : x.mem 1 = D) (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 * D)) + 6 ≤ b) (hv : ∀ (k : Fin 6), x.mem (out + i * (6 + 2 * (n * D)) + ↑k) = v k) (hfit : WordRAM.Fits W (b + 2 * (n * D) + D + n + 128)) :
∃ (y : WordRAM.Data 320),
WordRAM.ExecWithin W readRecord x y 28 ∧ y.mem = x.mem ∧ y.regs Reg.dimension = D ∧ y.regs Reg.size = n ∧ y.regs Reg.area = n * D ∧ y.regs Reg.twiceArea = 2 * (n * D) ∧ y.regs Reg.base = b ∧ y.regs Reg.record = out + i * (6 + 2 * (n * D)) ∧ y.regs Reg.rho = v 0 ∧ y.regs Reg.piece = v 1 ∧ y.regs Reg.queries = v 2 ∧ y.regs Reg.count = v 3 ∧ y.regs Reg.left = v 4 ∧ y.regs Reg.right = v 5 ∧ y.regs Reg.source = D ∧ y.regs Reg.one = 1 ∧ y.regs Reg.two = 2 ∧ y.regs Reg.nineteen = 19 ∧ y.regs Reg.four = 4
Read an actual six-word producer record at its computed ordinal. The input memory is unchanged; arbitrary source words are loaded, rather than supplied as predecoded registers.