Stage one (round six, `stage1`)
ProvedIntMul.Kappa.R6.Cx.NetEff.stage1Stage one: y_S += x_S; x and the dirty scratch a are restored (temporaries m clean).
The following holds (Lean statement, in the scope of module Solutions.R6CxNetEff):
theorem IntMul.Kappa.R6.Cx.NetEff.stage1 (hg : GOK (d.gates.flatMap gq)) (hlen : d.pieces.length = NV) (hsrc : ∀ t < NV, d.src t < NR)
(hR : RdOK d) (hM : MaskOK d) (Λ : ℕ → Vt) (hm : ∀ j < 24, Λ (mw j) = 0) :
(∀ S < NV, runL ((specs1 d).flatMap Spec.ops) Λ (yw S) = Λ (yw S) + Λ (xw S)) ∧
(∀ q < NR, runL ((specs1 d).flatMap Spec.ops) Λ (aw q) = Λ (aw q)) ∧
(∀ t < NV, runL ((specs1 d).flatMap Spec.ops) Λ (xw t) = Λ (xw t))
Context. The scalar effect of the two stage programs
For the local wires (x_t = t, y_S = 2024 + S, a_q = 4048 + q, m_j = 53256 + j) and any state
Λ with clean temporaries (Λ (m_j) = 0), the ops of specs1 give y_S ↦ y_S + x_S and those of
specs2 give y_S ↦ y_S − x_S, while x and the dirty scratch a are restored. The data enter
through DatOK (checked by the kernel) and the mask identity MaskOK (R6CxNetMaskAll).
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_R6_Defs24
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Cx IntMul.Kappa.R6.Cx.NetEff
open IntMul.Kappa.R6.Cx.NetSpec IntMul.Kappa.R6.Cx.NetMask IntMul.Kappa.R6.Cx.NetScal IntMul.Kappa.R6.Cx.NetLoc Finset
variable {Vt : Type*} [AddCommGroup Vt] [Module ℂ Vt]
variable (d : Dat)
theorem IntMul.Kappa.R6.Cx.NetEff.stage1 (hg : GOK (d.gates.flatMap gq)) (hlen : d.pieces.length = NV) (hsrc : ∀ t < NV, d.src t < NR)
(hR : RdOK d) (hM : MaskOK d) (Λ : ℕ → Vt) (hm : ∀ j < 24, Λ (mw j) = 0) :
(∀ S < NV, runL ((specs1 d).flatMap Spec.ops) Λ (yw S) = Λ (yw S) + Λ (xw S)) ∧
(∀ q < NR, runL ((specs1 d).flatMap Spec.ops) Λ (aw q) = Λ (aw q)) ∧
(∀ t < NV, runL ((specs1 d).flatMap Spec.ops) Λ (xw t) = Λ (xw t)) := by sorry