Computed child-frame writes

Main results

• PrunedQuery.exec_push: compute the next stack address, prefix and stride, store all four child-frame words, and enter that frame in fifteen native instructions.

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

Registers changed while constructing and entering one child frame.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidablePushLocal (i : Fin registers) : Decidable (PushLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_push {w : ℕ} (x : WordRAM.Data registers) (h0 : x.regs nil = 0) (h1 : x.regs one = 1) (h4 : x.regs frameWidth = 4) (h10 : x.regs ten = 10) (hw : WordRAM.Fits w (x.regs frames + x.regs nextLevel * 4 + x.regs leafPrefix + x.regs term * x.regs stride + x.regs stride * 10 + 8)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w push x y 15 ∧ y.regs level = x.regs nextLevel ∧ y.regs mode = 0 ∧ y.regs childFrame = x.regs frames + x.regs nextLevel * 4 ∧ y.regs childPrefix = x.regs leafPrefix + x.regs term * x.regs stride ∧ y.regs childStride = x.regs stride * 10 ∧ y.mem = Function.update (Function.update (Function.update (Function.update x.mem (x.regs frames + x.regs nextLevel * 4) (x.regs childCount)) (x.regs frames + x.regs nextLevel * 4 + 1) (x.regs leafPrefix + x.regs term * x.regs stride)) (x.regs frames + x.regs nextLevel * 4 + 2) (x.regs stride * 10)) (x.regs frames + x.regs nextLevel * 4 + 3) 0 ∧ WordRAM.Modifies { base := x.regs frames + x.regs nextLevel * 4, length := 4 }.footprint x.mem y.mem ∧ ∀ (i : Fin registers), ¬PushLocal i → y.regs i = x.regs i

The child list's actual count is written to the computed frame, followed by the new leaf prefix, stride and zero term counter. All scalar fit premises follow from the displayed budget.