The terminal case of the actual pruned-query controller #
Main results #
PrunedQuery.exec_leafStep: load the stored frame, select the leaf phase and return.PrunedQuery.exec_controller_leaf: prepend this real iteration to the controller's remaining execution, with its charged loop test.
These use the existing native ExecWithin semantics throughout. The continuation is a
conclusion of the execution proof, rather than a hypothesis supplying a solver or its cost.
def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.LeafStepLocal (i : Fin registers) :
Registers written by frame loading and a terminal controller phase.
Instances For
@[instance_reducible]
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_leafStep {w p : ℕ} {a b : ℤ} (ha : GenericRAM.Signed.Fits w a) (hb : GenericRAM.Signed.Fits w b) (hab : GenericRAM.Signed.Fits w (a * b)) (x : WordRAM.Data registers) (h0 : x.regs nil = 0) (h1 : x.regs one = 1) (h4 : x.regs frameWidth = 4) (hm : x.regs mode = 0) (hd : x.regs level = x.regs inputDepth) (hpref : x.mem (x.regs frames + 4 * x.regs level + 1) = p) (hleft : x.mem (x.regs arrayA + p) = WordRAM.Signed.encode a) (hright : x.mem (x.regs arrayB + p) = WordRAM.Signed.encode b) (hw :
WordRAM.Fits (w + 2)
(x.regs frames + 4 * (x.regs level + 1) + x.regs lists + x.regs values + (x.regs level + 1) * x.regs span + x.regs level + x.regs arrayA + p + x.regs arrayB + p + 12)) :
∃ (y : WordRAM.Data registers),
WordRAM.ExecWithin (w + 2) step x y 43 ∧ (y.mem = if x.mem (x.regs frames + 4 * x.regs level) = 0 then x.mem
else Function.update x.mem (x.regs values + x.regs level * x.regs span) (WordRAM.Signed.encode (a * b))) ∧ (y.regs level = if x.regs level = 0 then 0 else x.regs level - 1) ∧ (y.regs mode = if x.regs level = 0 then 0 else 2) ∧ (y.regs active = if x.regs level = 0 then 0 else x.regs active) ∧ ∀ (i : Fin registers), ¬LeafStepLocal i → y.regs i = x.regs i
The actual controller reads its frame and takes both real entry/leaf comparisons. The only possible store is the requested product at this depth's value-row base.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_controller_leaf {w p : ℕ} {a b : ℤ} (ha : GenericRAM.Signed.Fits w a) (hb : GenericRAM.Signed.Fits w b) (hab : GenericRAM.Signed.Fits w (a * b)) (x : WordRAM.Data registers) (h0 : x.regs nil = 0) (h1 : x.regs one = 1) (h4 : x.regs frameWidth = 4) (hm : x.regs mode = 0) (hd : x.regs level = x.regs inputDepth) (hactive : x.regs active = 1) (hpref : x.mem (x.regs frames + 4 * x.regs level + 1) = p) (hleft : x.mem (x.regs arrayA + p) = WordRAM.Signed.encode a) (hright : x.mem (x.regs arrayB + p) = WordRAM.Signed.encode b) (hw :
WordRAM.Fits (w + 2)
(x.regs frames + 4 * (x.regs level + 1) + x.regs lists + x.regs values + (x.regs level + 1) * x.regs span + x.regs level + x.regs arrayA + p + x.regs arrayB + p + 12)) :
∃ (y : WordRAM.Data registers),
(y.mem = if x.mem (x.regs frames + 4 * x.regs level) = 0 then x.mem
else Function.update x.mem (x.regs values + x.regs level * x.regs span) (WordRAM.Signed.encode (a * b))) ∧ (y.regs level = if x.regs level = 0 then 0 else x.regs level - 1) ∧ (y.regs mode = if x.regs level = 0 then 0 else 2) ∧ (y.regs active = if x.regs level = 0 then 0 else 1) ∧ (∀ (i : Fin registers), ¬LeafStepLocal i → y.regs i = x.regs i) ∧ ∀ (z : WordRAM.Data registers) (U : ℕ),
WordRAM.ExecWithin (w + 2) controller y z U → WordRAM.ExecWithin (w + 2) controller x z (45 + U)
A terminal node is one actual iteration of the existing native loop. Its 43 body instructions plus the two loop instructions are charged before any continuation.