`ljP` (round six, `ljP_sp`)
ProvedJ6Seg.Src.ljP_spljP, on any state.
The following holds (Lean statement, in the scope of module Solutions.J6SegILSrc5):
theorem J6Seg.Src.ljP_sp (s0 : IState HS) (F : Fin HS → List ℤ) {iS iT iL iW : Fin HS} (fS : Free iS)
(fT : Free iT) (fL : Free iL) (fW : Free iW) {s t lam w A : ℕ} {LS LT LL LW : List ℤ}
(hGS : F iS = (s : ℤ) :: LS) (hGT : F iT = (t : ℤ) :: LT) (hGL : F iL = (lam : ℤ) :: LL)
(hGW : F iW = (w : ℤ) :: LW) (hs : 0 < s) (hl : 0 < lam)
(hsA : s ≤ 2 ^ A) (htA : t ≤ 2 ^ A) (hlA : lam ≤ 2 ^ A) (hwA : w ≤ 2 ^ A) (hA : 2 ≤ A) :
Sp (ljP iS iT iL iW) (encK s0 F) (encK s0 (ljOut F s t lam w)) (ljCost s A)
Context. B-line IL, source-table producers, part 5: ljP assembled
ljP iS iT iL iW is a plain RS program (no mulC calls).
Inputs (tops of the named stacks, which must be Free, i.e. < 56 and not one of
13, 14, 15, 30, 31, 32, 33, 43, 44): s on iS, t on iT, λ on iL, w on iW;
0 < s, 0 < λ, and s, t, λ, w ≤ 2^A with 2 ≤ A.
Outputs (prepended, head = index 0):
30:LJ = Jlist (mkBlocks s t λ w)(= J6Seg.LJ s t λ w), increasing;31:|LJ|;32:STL = (range s).map (stF s t λ);33:LNL = (range s).map (fun i => 1 + enF s t λ (stF s t λ i)).
Scratch 14, 15, 43 is pushed and popped; every other stack is unchanged; nothing ≥ 56
other than expression scratch is touched. Theorem ljP_sp, cost ljCost s A.
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_Defs65 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.Src set_option maxRecDepth 20000 open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg.PreT J6Seg
theorem J6Seg.Src.ljP_sp (s0 : IState HS) (F : Fin HS → List ℤ) {iS iT iL iW : Fin HS} (fS : Free iS)
(fT : Free iT) (fL : Free iL) (fW : Free iW) {s t lam w A : ℕ} {LS LT LL LW : List ℤ}
(hGS : F iS = (s : ℤ) :: LS) (hGT : F iT = (t : ℤ) :: LT) (hGL : F iL = (lam : ℤ) :: LL)
(hGW : F iW = (w : ℤ) :: LW) (hs : 0 < s) (hl : 0 < lam)
(hsA : s ≤ 2 ^ A) (htA : t ≤ 2 ^ A) (hlA : lam ≤ 2 ^ A) (hwA : w ≤ 2 ^ A) (hA : 2 ≤ A) :
Sp (ljP iS iT iL iW) (encK s0 F) (encK s0 (ljOut F s t lam w)) (ljCost s A) := by sorry