One instruction (round six, `ins1`)
ProvedJ6Seg.PJ.Rn.ins1One instruction.
The following holds (Lean statement, in the scope of module Solutions.J6SegILPreJ10):
theorem J6Seg.PJ.Rn.ins1 {W N : ℕ} (hN : N ≤ 2 ^ W) {v : Vr} {c : Cs} (hv : BV W v) :
∀ i : Ins, i.ok W N (v, c) →
Rn i.p v c (fun v' => v' = (i.run (v, c)).1 ∧ BV W v') (i.run (v, c)).2 (i.cost W N)
Context. B-line IL, J pre-table (B5-J), part 10: straight-line instruction lists
Ins: a (register assignment), rd (random read dst := X[e]), pu (push), po (pop), en
(d := expNeg n k j, the library program through PreT.callC). Ins.run is the effect on
(v, c), Ins.ok W N the side conditions (values ≤ 2^W, read lists of length ≤ N), and
Rn.insL: a list of instructions runs as its runL, at cost costL W N.
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_Defs69 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.PJ open IntMul NLogN NLogN.KIL NLogN.RS Function IntMul.HvdH
theorem J6Seg.PJ.Rn.ins1 {W N : ℕ} (hN : N ≤ 2 ^ W) {v : Vr} {c : Cs} (hv : BV W v) :
∀ i : Ins, i.ok W N (v, c) →
Rn i.p v c (fun v' => v' = (i.run (v, c)).1 ∧ BV W v') (i.run (v, c)).2 (i.cost W N) := by sorry