fix(ci): run cold translation when protected-base evidence is missing

[bordumb]

Summary

formal translation no longer fails a pull request when the base commit has no protected-base translation evidence. The job runs the same two clean reproductions a cold plan runs. Every digest and binding check is unchanged.

Why (a) cold fallback, not (b) broader reuse

• (b) fixes only one cause of missing evidence; (a) fixes all of them. Evidence is missing when the base run failed in another job (chore(formal): refresh assurance-manifest digests on main #172's case: 8b96f2ca failed formal Lean authoritative after formal translation passed), was cancelled by a newer push (cancel-in-progress on main), is still running, or its artifact expired. Of the last eight main push runs, six were cancelled, one failed, and one is in progress. Under (b), every PR based on the cancelled or in-progress commits would still fail.
• The spec asks for (a). AP-SPEC-050 §8.3 item 9 says the consumer MUST "fall back to a clean run on any mismatch or absence", and §14.3 lists "absent reuse falls back to two clean reproductions" as a required test. §8.1 permits (b), but (b) does not meet §8.3 item 9.
• (a) accepts nothing new. The fallback produces the strongest evidence the job has: two byte-identical reproductions from source. (b) would widen which reused evidence is accepted.
• Cost. The fallback costs one cold translation, and only when evidence is missing. The phase baseline is 28 runner-minutes. The reuse path is unchanged.

Changes

1. .github/workflows/ci.yml, job formal-translation-run:
   • Locate step. "Locate protected-base translation evidence" now runs before the cold steps and has id: protected-base-translation. It writes found=false first. It writes found=true only after downloading exactly one evidence file. Every absence ends the step with exit 0 and a summary line naming the reason: no base SHA, no successful CI push run on main, no unexpired artifact, a failed lookup or download, or a malformed artifact.
   • Bind step. "Verify and bind protected-base translation evidence" runs only when found == 'true'. Its command is unchanged, and a binding failure still fails the job. There is no fallback on mismatch.
   • Cold steps. Disk reclaim, Nix, Aeneas/Charon, and "Reproduce translation twice" run when reused != 'true' && found != 'true', that is, unless a reuse step found evidence.
   • Packaging (the fail-closed part). "Package a bounded translation update" now uses the same condition, plus pull_request. In update mode, the reproduction rewrites drifted generated files in place. Without the packaging step, drift found by the fallback would qualify. With it, the update is packaged and "Stop qualification…" fails the job.
   • Timing label. The phase timing labels the fallback executed-cold-without-base-evidence.
2. xtask/src/formal_qualification.rs: validate_ci_workflow_gates now reads the conditions of the translation job's steps. The bind step must require found == 'true'. Reproduction and packaging must share the fallback condition. New tests:
   • three mutation tests, each rejected: the old hard-failure condition, packaging that skips the fallback, and binding without found evidence;
   • one test that validates the committed ci.yml.
3. Docs:
   • new docs/ci/formal-translation-evidence.md, covering how evidence is chosen, the fallback, and the manual recovery (dispatch ci.yml on the branch);
   • a link to it from formal-artifact-regeneration.md;
   • a decision row in docs/PROGRAM_BOARD.md §4.
4. Regenerated files: the source closure (xtask changed), the assurance-manifest digests, and the semantic freeze. Freeze versions: source-closure 74, assurance-manifest 35, evolution-contract 72, public-surface 314, freezeVersion 314.

Overlap with #172

main is red because of stale assurance-manifest digests. This PR can't pass formal Lean authoritative without refreshing them, so it carries the same refresh. Its manifest diff matches #172's line for line except for the source-closure digest, which differs because this PR changes xtask.

• If this PR lands first, chore(formal): refresh assurance-manifest digests on main #172 is redundant.
• If chore(formal): refresh assurance-manifest digests on main #172 lands first, this PR needs a rebase and another freeze bump.

Verification

• Hosted CI passed on 8110261b. Run 36218032591: all 26 checks pass, including CI qualified, formal Lean authoritative, and formal evidence.

  • The four new tests ran in authoritative implementation and passed.
  • This PR changes the evidence closure, so CI planned a cold translation (formal_closure_changed). That run exercised the new conditions: Locate and Verify were skipped, disk, Nix, Aeneas, reproduction, and packaging ran, the two reproductions were byte-identical, and there was no drift.
  • formal Lean authoritative produced no assurance update, so the recomputed manifest digests are exact. The updater made no bot commit.

• The lookup script, tested against real runs. The fallback only runs for a PR whose closures match its base, which can happen only after this merges. So I ran the step's exact script locally against real main runs with a simulated GITHUB_OUTPUT, GITHUB_ENV, and step summary. For the success case, macOS bash 3.2 has no mapfile, so the local copy replaced that one unchanged line with an equivalent loop; the runners have bash 5.

  Base commit	Its CI push run	Result
  c1dd5517 (current main)	in progress	found=false; summary: no successful CI push run on main
  256e113f	cancelled	found=false; same reason
  8b96f2ca (chore(formal): refresh assurance-manifest digests on main #172's base)	failed in Lean	found=false; same reason
  8bf2970c	succeeded (the last success, two days ago)	found=true; auths-formal-translation-36056135924-1 downloaded, and AUTHS_REUSED_TRANSLATION_EVIDENCE set
  none	—	found=false; no base commit

• Local runs, used only to build the change:

  • actionlint: no new findings (its two reports also appear on main);
  • bash -n on the lookup script;
  • cargo fmt;
  • the xtask build;
  • auths-ci-plan formal-source-closure update;
  • cargo xtask semantic-freeze --update.

  Following the GitHub-first policy, no tests were run locally.

• Commit is unsigned. The headless signing agent is not on this host, so re-signing is left to the maintainer.