Complete charged native query scans

Main results

• PrunedQuery.exec_scan: the fixed native loop reads, filters and deduplicates its source list in at most 20 N + 5 instructions, without clearing a dense directory.

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

Registers changed by the whole scan, including its fresh-epoch initialization.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableScanLocal (i : Fin registers) : Decidable (ScanLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_scan {w N capacity : ℕ} (child : Bool) (x : WordRAM.Data registers) (input : ℕ → ℕ) (hN : x.regs count = N) (hinput : ∀ i < N, x.mem (x.regs listBase + i) = input i) (hcodes : ∀ i < N, shortened child (input i) < capacity) (hsep : x.regs childList + capacity ≤ x.regs stamps ∨ x.regs stamps + capacity ≤ x.regs childList) (hsrcOut : x.regs listBase + N ≤ x.regs childList ∨ x.regs childList + capacity ≤ x.regs listBase) (hsrcStamp : x.regs listBase + N ≤ x.regs stamps ∨ x.regs stamps + capacity ≤ x.regs listBase) (hmarks : ∀ q < capacity, x.mem (x.regs stamps + q) ≤ x.regs epoch) (h1 : x.regs one = 1) (h10 : x.regs ten = 10) (h9 : x.regs nine = 9) (hwidth : WordRAM.Fits w (x.regs listBase + N + x.regs childList + capacity + x.regs stamps + capacity + N + capacity + x.regs epoch + 12)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w (scan child) x y (20 * N + 5) ∧ y.regs index = N ∧ y.regs epoch = x.regs epoch + 1 ∧ y.regs childCount = (scanSet child (x.regs term) input N).card ∧ ScanMemory y.mem (x.regs childList) (x.regs stamps) (x.regs epoch + 1) capacity (scanSet child (x.regs term) input N) ∧ (∀ i < N, y.mem (x.regs listBase + i) = input i) ∧ (∀ (a : ℕ), ¬{ base := x.regs childList, length := capacity }.Owns a → ¬{ base := x.regs stamps, length := capacity }.Owns a → y.mem a = x.mem a) ∧ ∀ (i : Fin registers), ¬ScanLocal i → y.regs i = x.regs i

The actual native scan constructs a distinct query list and its membership timestamps. All width premises concern ordinary addresses, lengths and the incoming epoch. Source/output/ directory separation is checked on concrete intervals. No child list is supplied in advance.