The swap with expression parameters (round six, `swE_spec`)
ProvedNLogN.KFX.swE_specThe swap with expression parameters. Stack 0 is enc2 xs ++ R; the expressions
evaluate (with ≤ zsz V + 3 bits) to vol Pre, vol G, vol Suf, u; the two [2^u] fields are
interchanged at cost ≤ K (V+1) u^τ.
The following holds (Lean statement, in the scope of module Solutions.KFX1Sw):
theorem NLogN.KFX.swE_spec :
∃ T q₀ : ℕ, ∀ q, q.Prime → q₀ < q → ∃ K : ℝ, 0 ≤ K ∧
∀ (u : ℕ) (Pre G Suf : Shape), 1 ≤ u →
(∀ a ∈ Pre, 1 ≤ a) → (∀ a ∈ G, 1 ≤ a) → (∀ a ∈ Suf, 1 ≤ a) →
∀ (I : List Sym) (t : IState HS) (xs : List (ZMod 2)) (R : List Item),
t.G 0 = ints (enc2 xs) ++ R →
xs.length = vol (binShape Pre G Suf (2 ^ u)) →
∀ (eP eG eS eU : Ex HS) (Bb : ℕ), Bb ≤ zsz (vol (binShape Pre G Suf (2 ^ u)) : ℤ) + 3 →
eP.size + eG.size + eS.size + eU.size ≤ 50 →
NoK eP → NoK eG → NoK eS → NoK eU →
ESp eP t Bb (vol Pre : ℤ) → ESp eG t Bb (vol G : ℤ) → ESp eS t Bb (vol Suf : ℤ) →
ESp eU t Bb (u : ℤ) →
∃ c : ℕ, IRuns I l12prog (swE q eP eG eS eU) t
(t.upd 0 (ints (pull (binShape Pre G Suf (2 ^ u)) (binShape Pre G Suf (2 ^ u))
(swapPos Pre.length (Pre.length + 1 + G.length)) 0 (enc2 xs)) ++ R)) c ∧
(c : ℝ) ≤ K * ((vol (binShape Pre G Suf (2 ^ u)) : ℝ) + 1) *
(u : ℝ) ^ (1 - (2 : ℝ)⁻¹ ^ 50)
Context. KFX §1: the Lemma 12 swap wrapper with expression parameters
swE q eP eG eS eU pushes the four Lemma 12 parameters as the values of arbitrary expressions
(read from registers at run time), runs l12F, pops. swE_spec is KFL.swI_spec with the
literals replaced by expressions (KFL.ESp facts), and swE_geo gives the three slot swaps
rixT g (swT i) on the 8-axis geometry.
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_K_Defs33 import Definitions.Def_IntMul_Kappa_R6_Defs1 import Mathlib import Definitions.Def_IntMul_HvdH_M_Defs8 import Definitions.Def_IntMul_MultitapeModel set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open NLogN NLogN.KFX open IntMul NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL AModel AModelL12 NetProp7
theorem NLogN.KFX.swE_spec :
∃ T q₀ : ℕ, ∀ q, q.Prime → q₀ < q → ∃ K : ℝ, 0 ≤ K ∧
∀ (u : ℕ) (Pre G Suf : Shape), 1 ≤ u →
(∀ a ∈ Pre, 1 ≤ a) → (∀ a ∈ G, 1 ≤ a) → (∀ a ∈ Suf, 1 ≤ a) →
∀ (I : List Sym) (t : IState HS) (xs : List (ZMod 2)) (R : List Item),
t.G 0 = ints (enc2 xs) ++ R →
xs.length = vol (binShape Pre G Suf (2 ^ u)) →
∀ (eP eG eS eU : Ex HS) (Bb : ℕ), Bb ≤ zsz (vol (binShape Pre G Suf (2 ^ u)) : ℤ) + 3 →
eP.size + eG.size + eS.size + eU.size ≤ 50 →
NoK eP → NoK eG → NoK eS → NoK eU →
ESp eP t Bb (vol Pre : ℤ) → ESp eG t Bb (vol G : ℤ) → ESp eS t Bb (vol Suf : ℤ) →
ESp eU t Bb (u : ℤ) →
∃ c : ℕ, IRuns I l12prog (swE q eP eG eS eU) t
(t.upd 0 (ints (pull (binShape Pre G Suf (2 ^ u)) (binShape Pre G Suf (2 ^ u))
(swapPos Pre.length (Pre.length + 1 + G.length)) 0 (enc2 xs)) ++ R)) c ∧
(c : ℝ) ≤ K * ((vol (binShape Pre G Suf (2 ^ u)) : ℝ) + 1) *
(u : ℝ) ^ (1 - (2 : ℝ)⁻¹ ^ 50) := by sorry