Charged timestamp insertion for native child queries

Main results

• PrunedQuery.exec_emit: one native membership test and optional unique suffix insertion, within nine instructions, with the complete memory update and register frame.

This kernel does not assume that a child request set was computed elsewhere. The surrounding native scan supplies each tested suffix and uses the returned timestamp/list updates.

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

Exactly the registers a timestamp insertion can modify.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableEmitLocal (i : Fin registers) : Decidable (EmitLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_emit {w : ℕ} (x : WordRAM.Data registers) (h1 : x.regs one = 1) (hs : WordRAM.Fits w (x.regs stamps + x.regs suffix)) (hl : WordRAM.Fits w (x.regs childList + x.regs childCount)) (hn : WordRAM.Fits w (x.regs childCount + 1)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w emit x y 9 ∧ (y.regs childCount = if x.mem (x.regs stamps + x.regs suffix) = x.regs epoch then x.regs childCount else x.regs childCount + 1) ∧ (y.mem = if x.mem (x.regs stamps + x.regs suffix) = x.regs epoch then x.mem else Function.update (Function.update x.mem (x.regs childList + x.regs childCount) (x.regs suffix)) (x.regs stamps + x.regs suffix) (x.regs epoch)) ∧ ∀ (i : Fin registers), ¬EmitLocal i → y.regs i = x.regs i

Timestamp insertion performs its real load, comparison, optional stores and increment. The result states the exact memory update even before a caller supplies array separation.