Query-set meaning of an actual native scan step

Main results

• PrunedQuery.exec_scanInsert: the native filter and timestamp comparisons compute exactly a finite-set insertion, preserving the list/directory invariant and the outside memory frame.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_scanInsert {w capacity : ℕ} (child : Bool) (x : WordRAM.Data registers) (S : Finset ℕ) (q : ℕ) (hq : x.mem (x.regs listBase + x.regs index) = q) (hcount : x.regs childCount = S.card) (htable : ScanMemory x.mem (x.regs childList) (x.regs stamps) (x.regs epoch) capacity S) (hcode : shortened child q < capacity) (hsep : x.regs childList + capacity ≤ x.regs stamps ∨ x.regs stamps + capacity ≤ x.regs childList) (h1 : x.regs one = 1) (h10 : x.regs ten = 10) (h9 : x.regs nine = 9) (h10fit : WordRAM.Fits w 10) (hread : WordRAM.Fits w (x.regs listBase + x.regs index)) (hs : WordRAM.Fits w (x.regs stamps + shortened child q)) (hl : WordRAM.Fits w (x.regs childList + x.regs childCount)) (hn : WordRAM.Fits w (x.regs childCount + 1)) (hi : WordRAM.Fits w (x.regs index + 1)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w (scanStep child) x y 18 ∧ y.regs index = x.regs index + 1 ∧ y.regs childCount = (if selected child (x.regs term) q then insert (shortened child q) S else S).card ∧ ScanMemory y.mem (x.regs childList) (x.regs stamps) (x.regs epoch) capacity (if selected child (x.regs term) q then insert (shortened child q) S else S) ∧ (∀ (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), ¬ScanStepLocal i → y.regs i = x.regs i

One charged native step computes its set insertion from the loaded source word and the actual timestamp. S describes the current memory, rather than supplying a decision oracle.