Charged native return and term-advance transitions

Main results

• PrunedQuery.exec_pop: return to the parent's accumulation phase or terminate the root.
• PrunedQuery.exec_advance: store the incremented term counter in the actual parent frame.

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

Registers changed by a return transition.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidablePopLocal (i : Fin registers) : Decidable (PopLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_pop {w : ℕ} (x : WordRAM.Data registers) (h0 : x.regs nil = 0) (h1 : x.regs one = 1) (hw : WordRAM.Fits w (x.regs level + 2)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w pop x y 4 ∧ y.mem = x.mem ∧ (y.regs level = if x.regs level = 0 then 0 else x.regs level - 1) ∧ (y.regs mode = if x.regs level = 0 then x.regs mode else 2) ∧ (y.regs active = if x.regs level = 0 then 0 else x.regs active) ∧ ∀ (i : Fin registers), ¬PopLocal i → y.regs i = x.regs i

The return decision is the program's real comparison with zero. Both branches preserve memory and all registers outside the three controller fields.

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

Registers changed by advancing and storing a term counter.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableAdvanceLocal (i : Fin registers) : Decidable (AdvanceLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_storeTerm {w : ℕ} (x : WordRAM.Data registers) (h1 : x.regs one = 1) (h4 : x.regs frameWidth = 4) (hf : WordRAM.Fits w (x.regs frame + 4)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w storeTerm x y 4 ∧ y.regs mode = 1 ∧ y.mem = Function.update x.mem (x.regs frame + 3) (x.regs term) ∧ ∀ (i : Fin registers), i ≠ address → i ≠ mode → y.regs i = x.regs i

Store a term already in its register and switch to dispatch, charging all four operations.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_advance {w : ℕ} (x : WordRAM.Data registers) (h1 : x.regs one = 1) (h4 : x.regs frameWidth = 4) (ht : WordRAM.Fits w (x.regs term + 1)) (hf : WordRAM.Fits w (x.regs frame + 4)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w advance x y 5 ∧ y.regs term = x.regs term + 1 ∧ y.regs mode = 1 ∧ y.mem = Function.update x.mem (x.regs frame + 3) (x.regs term + 1) ∧ ∀ (i : Fin registers), ¬AdvanceLocal i → y.regs i = x.regs i

The term increment, frame-word address computation, store and phase assignment take five instructions. Only the fourth frame word changes in memory.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_clearValuesFinish {w : ℕ} (x : WordRAM.Data registers) (h1 : x.regs one = 1) (h4 : x.regs frameWidth = 4) (hf : WordRAM.Fits w (x.regs frame + 4)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w clearValuesFinish x y 5 ∧ y.regs term = 0 ∧ y.regs mode = 1 ∧ y.mem = Function.update x.mem (x.regs frame + 3) 0 ∧ ∀ (i : Fin registers), ¬AdvanceLocal i → y.regs i = x.regs i

Initialization uses the same actual frame store as advancement, with a zero term counter.