Round-six lemma `hdr_in`
ProvedJ6Seg.JK.hdr_inAn auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.
The following holds (Lean statement, in the scope of module Solutions.J6SegILJKer14):
theorem J6Seg.JK.hdr_in {s : IState HS} {F : Fin HS → List ℤ} {h body : List ℤ} {B : ℕ}
(hl : h.length = 8) (hT : F dTJ = h ++ body) (hR : ∀ X ∈ hdrRegs, F X = [])
(hB : Bnd B h) :
Sp hdrIn (encK s F) (encK s (hdrSt F h body)) (8 * (10000 * (B + 2)))
Context. B-line IL, the J kernel (B4), part 14: the kernel states
kS B z0 re im v w tmp wr wi: the managed state B (registers loaded, table body on dTJ)
with the stacks 0, RE, IM, V, W, TMP, WR, WI replaced; lookup and update lemmas.
The header moves hdrIn / hdrOut.
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_Defs66 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.JK open IntMul NLogN NLogN.KIL NLogN.KFB Function Finset
theorem J6Seg.JK.hdr_in {s : IState HS} {F : Fin HS → List ℤ} {h body : List ℤ} {B : ℕ}
(hl : h.length = 8) (hT : F dTJ = h ++ body) (hR : ∀ X ∈ hdrRegs, F X = [])
(hB : Bnd B h) :
Sp hdrIn (encK s F) (encK s (hdrSt F h body)) (8 * (10000 * (B + 2))) := by sorry