The behavior gate: the modernize walk’s soundness argument

Scope (2026-06-12): upgrade’s default is now the minimal bump (keep profile= when the repaired tool validates at its baseline, else the minimum valid profile; codemod decisions §50, GTR097). The gate proven here bounds the opt-in --modernize walk; read “the walk” below as that mode. The minimal default crosses a boundary only when validity strictly requires it, and any boundary a needed bump does cross still receives the same runtime-gated fixes and reporting. The walk is additionally capped by the deployment ceiling (registry decisions D23), an orthogonal installability bound outside this document’s behaviour claim: a lower cap can only shrink the set of crossed boundaries, never grow it.

Contract: the modernize walk crosses no Galaxy must_fix behaviour boundary whose change applies to the tool, except boundaries whose change it provably fixed on that tool. Holds by construction for novel tools; the corpus sweep is evidence, never the argument.

Mechanism: galaxy_tool_codemod/behavior_gate.py; policy and mode selection: the registry facade’s upgrade. Per-step structural soundness is the separate GTR012 composition (validity-gated sequencing); this document is the behavioural half that caps it.

The claim, decomposed

The gate computes a ceiling before the walk starts and the walk cannot exceed it. The claim reduces to five sub-claims:

  1. The boundary catalogue is Galaxy’s own. PROFILE_UPGRADE_CODES is vendored verbatim from Galaxy’s upgrade advisor (lib/galaxy/tool_util/upgrade/upgrade_codes.json @ b45c58a2). What counts as a profile behaviour change, and its must_fix/consider severity, is Galaxy’s authoritative enumeration, not ours. Scope limitation, stated plainly: a behaviour change Galaxy itself has not catalogued is invisible to the gate; we hold the same epistemic position as Galaxy’s advisor.

  2. Applicability detection never under-reports. Each code’s per-tool detector ports the corresponding ProfileMigration.advise predicate (codemod decisions §25), runs on the macro-expanded view (matching Galaxy’s advisors, which parse post-expansion), and falls back to the raw tree when expansion fails, the conservative direction (over-report, never silent). Detector tightenings are one-directional: they only suppress cases provably unaffected by the change (e.g. §28’s single-simple-command set -e suppression, and the 24.2 test-case detector’s own provably-clean checker, codemod §47), so a tightening can remove a false block but never admit a false pass. The 24.2 checker is itself parity-gated against Galaxy’s real validator with zero unsound suppressions (docs/galaxy_reimplementations.md touchpoint 3).

  3. Auto-fix credit is proof by execution, per tool. A crossed, applicable must_fix code stops being a blocker only when its mapped RuntimeGatedFix, each individually proven behaviour-preserving in its own document (GTR014 21_09_fix_from_work_dir_whitespace, GTR015 16_04_fix_output_format, GTR016 16_04_fix_interpreter, GTR096 24_2_fix_test_case_validation), is applied to a throwaway copy of this tool and the code’s detector no longer fires (code_cleared_by_autofix). There is no static “fixable codes” set: a fix’s partial coverage (GTR015’s sole-data-input subset, GTR016’s bucket A) and macro-supplied constructs the raw-tree fix cannot reach are handled exactly, because the probe re-detects on the expanded view. The live run re-verifies: the facade credits a fix in auto_fixed_codes only when post-apply re-detection shows the code quiet.

  4. The ceiling arithmetic cannot cross a blocker. A code at version V is crossed by a from -> to bump iff from < V <= to (upgrade_codes_crossed). The ceiling is the newest vendored profile strictly below the lowest surviving blocker’s V (behavior_ceiling), so declaring the ceiling crosses no blocked boundary, by the range inequality. Fail-closed branches: no vendored profile below the lowest blocker means no profile advance at all (blocked_below_baseline); an unplaceable baseline (an unresolved @PROFILE@ token) means the crossings cannot be ranged, so the walk does not run; and the gate never lowers a declared profile.

  5. The walk respects the ceiling by construction. The ceiling threads through every declaration site: newest_valid_profile(…, ceiling=…) skips newer profiles, UpdateProfile(ceiling=…) caps profile= (and the inline-token rewrite), and UpgradeToLatest(ceiling=…) targets the ceiling instead of latest. The shared-macro @PROFILE@ path computes each importer’s target through the same gate, and the consensus rule (every importer agrees) makes the shared bump the minimum every importer’s gate allows. Pinned by test_behavior_gate.py, the ceiling tests in test_binding.py / test_update_profile.py / test_upgrades.py, and the facade gate tests.

What the walk does NOT claim

Applicable consider-level changes do not stop the walk by default, a deliberate, documented policy choice (blocking on them would freeze nearly every tool at 16.04 because Galaxy emits one such code unconditionally; see docs/upgrade_behavior_block_stats.md). They are surfaced in the crossed-boundary warning and an honest behavior_preserving=False, never silently. Two opt-in flags adjust the gate, in opposite directions: --allow-behavior-change lifts it entirely and restores the historical structural walk, with the same reporting, and --block-consider tightens it to stop at applicable consider-level changes too (the review-everything mode; registry docs/decisions.md D28). The mechanism is the same blocking_codes(levels=…) in both cases; only the policy set changes.

Evidence (not the argument)

uv run python -m scripts.corpus_check upgrade --mode modernize runs the gated walk over every corpus tool and asserts this contract per tool (fail-closed, gate cap, no un-fixed must_fix crossing recomputed independently, validity preservation, byte idempotence), retaining every violation as a regression fixture (the default --mode both also sweeps the minimal default’s own contract). scripts.measure upgrade-behavior-blocks reports where the walk stops, computed with these same gate functions.

Coverage guard

test_proof_documents.py asserts every RuntimeGatedFix (its GTR code and its Galaxy upgrade_code) is named in this document, so a new auto-fix cannot join the gate without extending this argument.