Charged native suffix selection

Main results

• PrunedQuery.exec_suffix: one real quotient computation and timestamp insertion, within ten native instructions, with its complete memory and register frame.

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

Registers changed by shortening a query and attempting its insertion.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableSuffixLocal (i : Fin registers) : Decidable (SuffixLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_suffix {w : ℕ} (child : Bool) (x : WordRAM.Data registers) (q : ℕ) (hq : x.regs query = q) (h1 : x.regs one = 1) (h10 : x.regs ten = 10) (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)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w (putSuffix child) x y 10 ∧ y.regs suffix = shortened child q ∧ (y.regs childCount = if x.mem (x.regs stamps + shortened child q) = x.regs epoch then x.regs childCount else x.regs childCount + 1) ∧ (y.mem = if x.mem (x.regs stamps + shortened child q) = x.regs epoch then x.mem else Function.update (Function.update x.mem (x.regs childList + x.regs childCount) (shortened child q)) (x.regs stamps + shortened child q) (x.regs epoch)) ∧ ∀ (i : Fin registers), ¬SuffixLocal i → y.regs i = x.regs i

The selected suffix is divided from the actual loaded query, then deduplicated by its actual memory timestamp. No query-set computation is supplied as a hypothesis.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_scanDispatch {w : ℕ} (child : Bool) (x : WordRAM.Data registers) (q : ℕ) (hq : x.regs query = q) (hdigit : x.regs digit = q % 10) (h1 : x.regs one = 1) (h10 : x.regs ten = 10) (h9 : x.regs nine = 9) (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)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w (scanDispatch child) x y 14 ∧ (y.regs childCount = if selected child (x.regs term) q ∧ x.mem (x.regs stamps + shortened child q) ≠ x.regs epoch then x.regs childCount + 1 else x.regs childCount) ∧ (y.mem = if selected child (x.regs term) q ∧ x.mem (x.regs stamps + shortened child q) ≠ x.regs epoch then Function.update (Function.update x.mem (x.regs childList + x.regs childCount) (shortened child q)) (x.regs stamps + shortened child q) (x.regs epoch) else x.mem) ∧ ∀ (i : Fin registers), ¬SuffixLocal i → y.regs i = x.regs i

Execute the actual query filter and unique insertion. The numerical selection is proved from the two real digit comparisons; it is not a supplied child-set certificate.

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

All scan-step scratch registers; caller pointers, counts and the current epoch are kept.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableScanStepLocal (i : Fin registers) : Decidable (ScanStepLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_scanStep {w : ℕ} (child : Bool) (x : WordRAM.Data registers) (q : ℕ) (hq : x.mem (x.regs listBase + x.regs index) = q) (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 ∧ x.mem (x.regs stamps + shortened child q) ≠ x.regs epoch then x.regs childCount + 1 else x.regs childCount) ∧ (y.mem = if selected child (x.regs term) q ∧ x.mem (x.regs stamps + shortened child q) ≠ x.regs epoch then Function.update (Function.update x.mem (x.regs childList + x.regs childCount) (shortened child q)) (x.regs stamps + shortened child q) (x.regs epoch) else x.mem) ∧ ∀ (i : Fin registers), ¬ScanStepLocal i → y.regs i = x.regs i

One complete native scan step includes source indexing, the actual load and digit computation, conditional deduplicated insertion, and the loop-counter increment.