The output slab pass (pass 7) (round six, `slabOut_runs`)

The output slab pass (pass 7).

The following holds (Lean statement, in the scope of module Solutions.J6SegILSlab8):

theorem J6Seg.Slab.slabOut_runs {pM : Fin P} (hMul : MulOK I iprog pM NLogN.KFUU.MS) (s : IState HS)
    (F : Fin HS → List ℤ) {N post pre : ℕ} (hnp : 0 < N * post) (p P' s' t α : ℕ)
    (Y Y₂ : List GI) (l l₂ : List ℤ) (hY : Y.length = pre * (N * post))
    (hY₂ : Y₂.length = pre * (N * post)) {Bu Ba : ℕ} (hBa : 1 ≤ Ba)
    (hBu : ∀ u ∈ gflat Y, zsz u ≤ Bu) (hBu₂ : ∀ u ∈ gflat Y₂, zsz u ≤ Bu)
    (harg : ∀ l, zsz (argO p s' t α l) ≤ Ba)
    (hF0 : F 0 = gflat Y ++ l) (hFZ : F rZ = gflat Y₂ ++ l₂)
    {l1 l2 : List ℤ} (hK1 : F rK1 = (2 : ℤ) ^ (P' - p) :: l1) (hK2 : F rK2 = (2 : ℤ) ^ p :: l2)
    (hA : F lA = []) (hC : F lC = []) (hD : F lD = []) (RC : List ℤ)
    (hFC : F rC = flatC (ctlOf N N (fun l => some l) (argO p s' t α)) ++ RC) (hACC : F rACC = [])
    {LM : List ℤ} (hM : F rM = ((2 * post : ℕ) : ℤ) :: LM) {LN : List ℤ}
    (hN : F rNC = ((ctlOf N N (fun l => some l) (argO p s' t α)).length : ℤ) :: LN) {LB : List ℤ}
    (hB : F rNB = (pre : ℤ) :: LB) {LT : List ℤ}
    (hT : F rTOT = ((pre * (N * (2 * post)) : ℕ) : ℤ) :: LT) :
    IRuns I iprog (J6Seg.Slab.passP drP rdP (itO pM) bkP) (encK s F)
      (encK s (update (update F 0
        (gflat (slabPass N N post (fun l => some l) (J6Seg.outH p P' s' t α) (List.zip Y Y₂)) ++ l))
        rZ l₂))
      (passC pre (ctlOf N N (fun l => some l) (argO p s' t α)).length (2 * post) Ba
        (2 * (2 * Bu + 2) + 2 * (2 * moveCost Bu + 19) + cItO (Bu + Ba + 2) (P' - p) p +
          2 * (2 * moveCost Bu + 19))
        (pre * (N * (2 * post))) (Bu + Ba + 1))

Context. B-line IL, B1 (streaming slab pass) §8: the slab passes of axisPipe on GI arrays

The three IL slab passes, on gflat arrays (post GI entries = m = 2 post integers per slab):

• slabId_runs (passes 3, 5: h = fun _ z => z; control ctlOf n n' src (fun _ => 0)),
• slabSc_runs (pass 1: h = selH p P; control ctlOf n n' src (fun _ => 2^(P-p-1))),
• slabOut_runs (pass 7: h = outH p P s t α on zip Y Y₂, source some l; control ctlOf N N some argO with argO l = d̃_l for l < s, else 0; the two arrays on stacks 0 and rZ; constants 2^(P-p), 2^p on rK1, rK2; multiplication MulOK pM).

Each takes the skeleton inputs (rC = flatC cs ++ RC, rACC = [], rNB = pre, rNC = |cs|, rM = 2 post, rTOT = pre · n' · 2 post, the rptX counters empty) and leaves gflat (slabPass …) ++ l on stack 0, everything else unchanged. The cost is passC …; with passC_le and |cs| ≤ n + n' (length_ctlOf_le) it is, per block, O((n + n' + 1) (post + 1) (cu + Ba + 1)) with cu = O(Bu + 1) (identity), O(Bu + P + 1) (scale), O(cU (Bu + Ba + 2) + P) (output: one multiplication per entry).

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).