The program on the stream table (round six, `netH_runs`)

The program on the stream table.

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

theorem IntMul.Kappa.R6.IL.netH_runs {G0 : Fin HS → List Item} {v : ℕ} (E : Bit.Edge m → IStmt HS Pp)
    (impl : Bit.Edge m → List (ZMod 2) → List (ZMod 2)) (cE : Bit.Edge m → ℕ)
    (s : IState HS) (hs : Inv G0 s) (rest : List ℤ) {Bb : ℕ} (hB : TabB (T + W) v Bb)
    (hv1 : 1 ≤ v) :
    ∀ (prog : List (Bit.Instr (Fin W ⊕ Fin T) (ZMod 2) m)),
      (∀ e ∈ Bit.progEdges prog, ∀ ys : List (ZMod 2), ys.length = v → (impl e ys).length = v) →
      (∀ e ∈ Bit.progEdges prog, ∀ ys : List (ZMod 2), ys.length = v →
        ∀ (t : IState HS) (R : List Item), Inv G0 t →
        IRuns I iprog (E e) (t.upd 0 (ints (enc2 ys) ++ R)) (t.upd 0 (ints (enc2 (impl e ys)) ++ R))
          (cE e)) →
      ∀ (st : Fin W ⊕ Fin T → List (ZMod 2)) (f : Fin HS → List ℤ), (∀ x, (st x).length = v) →
      (∀ r, Prot r → f r = []) → RegS s f (T + W) v →
      f 0 = tabR 0 (T + W) (tabS st) ++ rest → f 21 = [] →
      IRuns I iprog (netH E prog) (encK s f)
        (encK s (Function.update f 0 (tabR 0 (T + W) (tabS (Bit.netRunH v impl prog st)) ++ rest)))
        ((prog.map (instrHC cE ((T + W) * v) Bb)).sum + 1)

Context. Round six, item language: a QHNet program on a table of T + W streams

The wires Fin W ⊕ Fin T of a round-six network are laid out as a table of T + W streams of length v on stack 0 (temporaries first: inr t ↦ t, inl w ↦ T + w, eqv).

• gateH_fsp: a gate (g, S) is one fine rebuild rebuildCU (T + W) (srcT (ngOf g S)) (frozen KIL3/KFD table code), with denotation gateApply;
• instrH, netH: the code of an instruction / of a program, an edge (x, e) being run in place by applyCF with an edge code E e;
• netH_runs: the program code computes netRunH v impl prog whenever every edge code computes impl e on single streams (under the invariant Inv G0).

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*).