Actual native leaf multiplication

Main results

• PrunedQuery.exec_leafProduct: load the two encoded leaf words and store their exact signed product, within nineteen native instructions.
• PrunedQuery.exec_leaf: take the actual empty/nonempty branch and return to the parent.

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

The existing signed workspace and the indexed-load address register.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableLeafLocal (i : Fin registers) : Decidable (LeafLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_leafProduct {w : ℕ} {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) (hleft : x.mem (x.regs arrayA + x.regs leafPrefix) = WordRAM.Signed.encode a) (hright : x.mem (x.regs arrayB + x.regs leafPrefix) = WordRAM.Signed.encode b) (hp : WordRAM.Fits (w + 2) (x.regs arrayA + x.regs leafPrefix)) (hq : WordRAM.Fits (w + 2) (x.regs arrayB + x.regs leafPrefix)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin (w + 2) leafProduct x y 19 ∧ y.mem = Function.update x.mem (x.regs valueBase) (WordRAM.Signed.encode (a * b)) ∧ ∀ (i : Fin registers), ¬LeafLocal i → y.regs i = x.regs i

Both loads, the existing fourteen-instruction signed multiplication kernel and the store are charged. The ordinary mathematical product must fit the source signed width.

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

Registers used by the full leaf phase, including its actual parent-return decision.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableLeafReturnLocal (i : Fin registers) : Decidable (LeafReturnLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_leaf {w : ℕ} {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) (hleft : x.mem (x.regs arrayA + x.regs leafPrefix) = WordRAM.Signed.encode a) (hright : x.mem (x.regs arrayB + x.regs leafPrefix) = WordRAM.Signed.encode b) (hp : WordRAM.Fits (w + 2) (x.regs arrayA + x.regs leafPrefix)) (hq : WordRAM.Fits (w + 2) (x.regs arrayB + x.regs leafPrefix)) (hd : WordRAM.Fits (w + 2) (x.regs level + 2)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin (w + 2) leaf x y 24 ∧ (y.mem = if x.regs count = 0 then x.mem else Function.update x.mem (x.regs valueBase) (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 x.regs mode else 2) ∧ (y.regs active = if x.regs level = 0 then 0 else x.regs active) ∧ ∀ (i : Fin registers), ¬LeafReturnLocal i → y.regs i = x.regs i

The empty leaf performs no operand loads or multiplication. A requested leaf computes its signed product. Both execute the real return branch; root termination and parent accumulation are decided by the stored depth register, not by an external call rule.