Forward push step (round six, `fsIs`)
ProvedJ6Seg.PJ.Rn.fsIsForward push step.
The following holds (Lean statement, in the scope of module Solutions.J6SegILPreJD4):
theorem J6Seg.PJ.Rn.fsIs (hF : Fx Q kk m mw cB u) (hS : StS m L Mf c) (hB : BdS W m L Mf)
(hLm : L.length = m) (hv : BV W u) {r cw i : ℕ} (h5 : u 5 = r) (h3 : u 3 = cw) (h2 : u 2 = i)
(hi : i < cw) (hcw : cw ≤ r) (hr : r < m) (h4 : u 4 = Lg L r) :
Rn (progL fsI) u c (fun u' => (∀ i ∉ ([6, 7, 8, 29] : List (Fin HS)), u' i = u i) ∧ BV W u')
(update c 41 ((if bandS mw cB (Lg L r) (Lg L (r - cw + i)) then
fdiv Q (Mf r (r - cw + i)) (Mf (r - cw + i) (r - cw + i)) else 0) :: c 41))
(costL W (m * m + m) fsI)
Context. B-line IL, J pre-table (B5-J), jTab part D4: the straight-line pieces of serP
For each instruction list of serP (bHead, czI, czT, bMid, wbI, cbI, bTail,
fHead, cnI, fMid, fsI, fTail): its run on the register file, as an Rn with the
registers it sets, the stack it pushes onto (41), and the registers it leaves alone.
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_Defs71
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg J6Seg.PJ
open IntMul NLogN NLogN.KIL NLogN.RS Function J6Seg.PJ.E
variable {Q kk m mw cB W : ℕ} {L : List ℕ} {Mf : ℕ → ℕ → ℤ} {u : Vr} {c : Cs}
theorem J6Seg.PJ.Rn.fsIs (hF : Fx Q kk m mw cB u) (hS : StS m L Mf c) (hB : BdS W m L Mf)
(hLm : L.length = m) (hv : BV W u) {r cw i : ℕ} (h5 : u 5 = r) (h3 : u 3 = cw) (h2 : u 2 = i)
(hi : i < cw) (hcw : cw ≤ r) (hr : r < m) (h4 : u 4 = Lg L r) :
Rn (progL fsI) u c (fun u' => (∀ i ∉ ([6, 7, 8, 29] : List (Fin HS)), u' i = u i) ∧ BV W u')
(update c 41 ((if bandS mw cB (Lg L r) (Lg L (r - cw + i)) then
fdiv Q (Mf r (r - cw + i)) (Mf (r - cw + i) (r - cw + i)) else 0) :: c 41))
(costL W (m * m + m) fsI) := by sorry