Returning from a completed native internal node

Main results

• PrunedQuery.exec_progress_finish: the native exhausted-term branch returns the existing pruned values and all frame, cursor and timestamp conclusions used by the parent.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_progress_finish {w L f a0 b0 n d p E : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ) (x y : WordRAM.Data registers) (hx : NodeReady L f a0 b0 (n + 1) d p E S x) (hy : NodeProgress L f a0 b0 n d p E S a b x 10 y) (hfit : WordRAM.Fits w (nodeBudget L f a0 b0 E (n + 1))) : ∃ (z : WordRAM.Data registers), WordRAM.ExecWithin w step y z 26 ∧ NodeResult L f a0 b0 (n + 1) d E S a b x z

All ten stored partial sums give the existing Pruned.result. The native final dispatch and pop change registers only, stopping at the root and resuming accumulation at a parent.