Returning queried values in the actual input order

Main results

• PrunedQuery.exec_report: the native reporting loop preserves duplicate requests and writes their corresponding values in order, charging every load, address, store and loop test.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.ReportLocal (i : Fin registers) : Prop

Registers used while reporting the explicitly supplied query list.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableReportLocal (i : Fin registers) : Decidable (ReportLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_report {w N capacity : ℕ} (x : WordRAM.Data registers) (codes : ℕ → ℕ) (hN : x.regs queryCount = N) (hinput : ∀ i < N, x.mem (x.regs queries + i) = codes i) (hcodes : ∀ i < N, codes i < capacity) (hsrc : x.regs queries + N ≤ x.regs output ∨ x.regs output + N ≤ x.regs queries) (hvals : x.regs values + capacity ≤ x.regs output ∨ x.regs output + N ≤ x.regs values) (h1 : x.regs one = 1) (hw : WordRAM.Fits w (x.regs queries + N + x.regs values + capacity + x.regs output + N + N + 12)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w report x y (9 * N + 3) ∧ y.regs index = N ∧ (∀ i < N, y.mem (x.regs output + i) = x.mem (x.regs values + codes i)) ∧ WordRAM.Modifies { base := x.regs output, length := N }.footprint x.mem y.mem ∧ ∀ (i : Fin registers), ¬ReportLocal i → y.regs i = x.regs i

The finite native loop reads the original requests, including duplicates. Its only writes are the N output cells; the value directory and original requests remain unchanged.