A call of a number program (round six, `callX`)

A call of a number program.

The following holds (Lean statement, in the scope of module Solutions.J6AIL7):

theorem J6A.PA.Rn.callX {v : Vr} {c : Cs} {W : ℕ} {d : Fin HS} (hd : d ∈ rg)
    {e16 e17 e18 e27 : Ex HS} (h16 : OnRg e16) (h17 : OnRg e17) (h18 : OnRg e18)
    (h27 : OnRg e27) (o16 : okR v c e16) (o17 : okR v c e17) (o18 : okR v c e18)
    (o27 : okR v c e27) (t16 : Tame (2 ^ W) e16) (t17 : Tame (2 ^ W) e17)
    (t18 : Tame (2 ^ W) e18) (t27 : Tame (2 ^ W) e27) (hv : BV W v)
    {a16 a17 a18 a27 : ℕ} (v16 : ev v c e16 = a16) (v17 : ev v c e17 = a17)
    (v18 : ev v c e18 = a18) (v27 : ev v c e27 = a27)
    (b16 : (a16 : ℤ) < 2 ^ W) (b17 : (a17 : ℤ) < 2 ^ W) (b18 : (a18 : ℤ) < 2 ^ W)
    (b27 : (a27 : ℤ) < 2 ^ W)
    {prog : RS} {r : ℤ} {C : ℕ}
    (hprog : ∀ (t : IState HS) (L16 L17 L18 L27 : List Item), t.G 16 = .int a16 :: L16 →
      t.G 17 = .int a17 :: L17 → t.G 18 = .int a18 :: L18 → t.G 27 = .int a27 :: L27 →
      prog.ok t ∧ prog.run t = t.upd 19 (.int r :: t.G 19) ∧ prog.cost t ≤ C)
    (hr : |r| < 2 ^ W) :
    Rn (J6A.PA.callX d e16 e17 e18 e27 prog) v c (· = Function.update v d r) c
      (cCallX e16 e17 e18 e27 W C)

Context. A lines, IL side 7: register-file helpers and the parameter block

On the register file RF v c of J6SegILPreJ* (Rn runs):

• Rn.asgR, Rn.pushR: assignments / pushes of expressions reading only registers of rg;
• Rn.callX: a call of a number program with inputs on 16, 17, 18, 27 and result on 19 (callC of J6SegILPre3), and Rn.enX / Rn.epX: v d := expNeg n k j / expPos n k j σ;
• parA: from the axis descriptor [k, pre, post, s, t, p, α, d] on dA = 31, the registers 1 … 12 become pre, post, s, t, p, α, m = sWidth p α, H = 2^⌊log₂ m⌋, W = H + m + 3, M = t / 16H, win = 8H, f = ⌊log₂ m⌋ + 3 (Rn.parA).

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*).