GTR012 — UpgradeToLatest: the iterative upgrade orchestrator
Contract: structural-only by composition; behaviourally capped by the gate’s ceiling when one is passed.
The transform
Loop: declare the newest valid profile (GTR007); if still below
the target (the latest profile, or the behaviour gate’s ceiling;
behavior-gate), apply the registered single-step
upgrade_vN codemod for the sticking version (GTR008,
GTR093, GTR009, GTR010,
GTR011); revalidate; repeat until the target or stuck.
Proof
Every constituent step is individually proven (each step’s own document); the
loop adds only validity-gated sequencing — it advances exactly when
newest_valid_profile strictly improves, so it can never apply a step whose
precondition (stuck at that version) doesn’t hold, and it terminates (the
profile is strictly increasing over a finite vendored set). A ceiling
threads through every declaration site (the capped newest_valid_profile
scan and UpdateProfile(ceiling=…)), so no round can declare past it; a
stall at the ceiling is deliberate and never reported as a missing
upgrade_vN. Runtime deltas surface via the gate’s stop report, the credited
auto_fixed_codes, behavior_preserving, and the §23 warnings, per the
upgrade contract.