Soundness: what “safe” guarantees (and what it doesn’t)

TL;DR. format never changes behaviour. upgrade is minimal-bump by default: profile= moves only when strictly needed for validity, and a tool that validates where it sits is kept byte-untouched. upgrade --modernize is the behavior-preserving walk: it advances the profile only as far as it can prove no applicable breaking (must_fix) Galaxy behaviour change is crossed un-fixed, stops there with an actionable report, and the result is structurally valid at the profile it declares. Going further is an explicit choice (--modernize --allow-behavior-change). Behaviour-affecting edits are applied only where the tool can prove them safe; everything else is reported, not changed. That conservatism is the point: it’s what makes the automation trustworthy.

Two different promises

Formatting is behaviour-preserving by construction. Indentation, blank lines, attribute/element order, empty-element shorthand, and CDATA-wrapping a pure-text body change bytes, not meaning. format is safe and idempotent and never touches profile=.

Upgrading is semantic, and its guarantee is two-part. Bumping a tool’s profile= can change how Galaxy interprets it. Structurally, the oracle is XSD validity at the target profile: the engine only advances a tool to a profile where it still validates. Validity is a sound oracle for structural changes, not a behaviour oracle, so a second, behavioural gate caps the walk: the engine computes every Galaxy-catalogued behaviour change the bump would cross, detects per tool which actually apply, and stops below the first applicable must_fix change it cannot provably fix on that tool. A fix is credited only by execution (applied, then re-detected); the stop report names the blocking code and links to docs/profile_boundaries.md, the per-boundary what-changed-and-what-to-do reference. Advisory (consider) changes are warned about, never crossed silently. The full argument is behavior-gate.md, part of the published rule proofs.

How we know format is behaviour-preserving: the audit

“Behaviour-preserving by construction” is a strong claim, so it is adversarially audited, not just asserted. Every fixable rule’s behaviour-preservation claim was stress-tested by independent skeptics that try to execute a counterexample breaking it; each “refuted” verdict was then re-verified by execution on the current code and against Galaxy’s own source before being acted on (adversarial agents over-claim). The result is recorded, rule by rule, in docs/behavior_preservation.md, the proof ledger.

This is an honest process, and it found real bugs in formatting rules once assumed safe, all now fixed, each pinned by a regression fixture so a future change can’t silently reintroduce the break:

  • a whitespace-only <configfile>/<command>/<token> body was collapsed, dropping template content (GTR004); a carriage return was lost through a CDATA wrap (GTR018.1/GTR019.1); a multi-flag <option value="-b -h"> select was single-quoted into one token (GTR020.1); a deprecated interpreter= rewrite duplicated a flag in a mixed-content <command> (GTR016).

Two of the eight refuted findings turned out to be over-claims by the audit itself, confirmed harmless by reading Galaxy’s source (e.g. Galaxy evaluates an output <filter> via eval(filter.text.strip()), so a comment-tail clause is dead at runtime either way). They were documented, not “fixed”. The point: the format guarantee is backed by executed evidence and a living ledger, not by assertion.

Reference and rename operations read Cheetah faithfully. find-references and rename-param resolve $param references through a faithful CT3 Cheetah lexer (a base dependency), so a $var inside a #raw block, a comment, or behind an escaped \$ is classified exactly as Galaxy would, correct for novel tool XML, not a regex approximation tuned to the current corpus.

How the boundary is enforced

  • By default the profile moves only to the minimum valid profile at or above the tool’s baseline, and only when the tool does not validate where it sits; a valid tool is byte-untouched and an undeclared tool stays undeclared. An unresolvable @PROFILE@ baseline fails closed (no advance), and the profile is never lowered.

  • Under --modernize the profile is advanced only to the newest profile the tool structurally reaches, capped by the behaviour ceiling (the newest vendored profile below the first applicable, un-fixed must_fix change) and by the deployment ceiling (the newest profile every major public Galaxy server runs, vendored from a committed server-poll snapshot; a newer declaration could not install everywhere yet). Only an explicit --target-profile exceeds the deployment ceiling.

  • For profile bumps that carry behaviour-affecting Galaxy changes, the engine runs per-tool detection and only applies an automated repair where it can prove the change is safe for that tool. Where it can’t, it stops and reports (for must_fix changes) or warns (for consider changes) instead of silently changing behaviour; --modernize --allow-behavior-change is the explicit opt-out.

  • The runtime-gated repairs are exactly as wide as their proofs (widened 2026-06-10 when source archaeology extended the proofs):

    • GTR016 (interpreter=) rewrites any non-empty interpreter value, Galaxy interpolates it verbatim in every composition form it ever shipped, provided the command’s first token is a literal script (“bucket A”); a Cheetah-leading command is left to detect/warn.

    • GTR015 (format="input") fixes the sole-data-input case, top-level or conditional/section-nested (qualified format_source); multi-input and repeat-nested cases are genuinely undecidable and stay reported.

    • GTR014 guards format_source.

  • Imported-macro write-back is locate-in-source (the construct is found in its defining file), not provenance-driven. Three consumers exist: the @PROFILE@ token (addressed by name, only when every importer agrees on the target profile); literal format/ftype normalization (the opt-in normalize-macros, validity-safe so no consensus gate); and cross-file parameter rename (rename-param rewrites a $param reference found in an imported macro, gated by sole-ownership within a --repo-root, or by importer consensus with --across-importers). There is no general mechanism to edit arbitrary macro-defined content yet, sizing that residual found 0 further tools, so the provenance layer stays deferred (docs/macro_handling_architecture.md).

You can see the verdict

upgrade reports a behavior_preserving flag for the bump:

  • true: it crossed no behaviour-affecting platform change that applies to this tool, or every applicable breaking change was provably fixed (each credited fix is named in a “fixed automatically” note);

  • false: at least one applies un-fixed (under the modernize walk’s gate this can only be an advisory consider change; breaking changes stop the walk instead); look before accepting;

  • null: undetermined (the profile is a macro token that resolves to no version; the upgrade then changes nothing).

Alongside it: stopped_at (where the gate capped the walk), blocking_codes (the full review list), and auto_fixed_codes. The CLI, library, and MCP server all surface these, so automation can auto-accept the safe case and escalate the rest, rather than trusting the bump blindly.

What this means for you

  • Trust format unconditionally.

  • Treat upgrade as “advance to the newest valid profile, plus the repairs proven safe”, and read its report for anything it chose to flag rather than fix.

  • Treat check findings as advisory: they’re best-practice signals, not failures.

Authoritative references

  • docs/profile_upgrades.md: the per-profile upgrade map and the validity-as-oracle boundary.

  • galaxy-tool-codemod/docs/decisions.md: the canonical_codemods() / AUTO_UPGRADE_CODEMODS split, per-tool warning detection, and the soundness limits of raw-tree vs macro-expanded detection.

  • docs/macro_handling_architecture.md: why macro write-back is locate-in-source today (the @PROFILE@ token + literal format/ftype), and the deferred, sized-to-zero provenance layer that would generalise it to arbitrary content.