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

.github/workflows/ci.yml

@@ -395,23 +395,63 @@ jobs:
             fi
           done < <(jq -r --arg repo "$GITHUB_REPOSITORY" --argjson pr "$AUTHS_PR_NUMBER" '.workflow_runs | map(select(.name == "CI" and .head_repository.full_name == $repo and any(.pull_requests[]?; .number == $pr))) | .[:10][] | [.id, .run_attempt, .head_sha] | @tsv' <<< "$runs")
           echo 'No applicable successful same-PR translation; using two clean reproductions.' >> "$GITHUB_STEP_SUMMARY"
+      # Protected-base evidence is an optimization, never a precondition. The
+      # base commit's run may have failed in another job, been cancelled by a
+      # newer push, still be running, or have expired; `found` then stays false
+      # and the two clean reproductions below run instead. Located evidence
+      # that does not bind to this checkout still fails the job.
+      - id: protected-base-translation
+        name: Locate protected-base translation evidence
+        if: needs.ci-plan.outputs.formal_cold_required != 'true'
+        env:
+          GH_TOKEN: ${{ github.token }}
+          AUTHS_BASE_SHA: ${{ github.event.pull_request.base.sha }}
+        shell: bash
+        run: |
+          set -euo pipefail
+          echo 'found=false' >> "$GITHUB_OUTPUT"
+          no_evidence() {
+            echo "Translation: no protected-base evidence for base ${AUTHS_BASE_SHA:-unknown} ($1); executing two clean reproductions." >> "$GITHUB_STEP_SUMMARY"
+            exit 0
+          }
+          [[ "$AUTHS_BASE_SHA" =~ ^[0-9a-f]{40}$ ]] || no_evidence 'no base commit'
+          run_id="$(gh api --method GET "repos/${GITHUB_REPOSITORY}/actions/runs" -f head_sha="$AUTHS_BASE_SHA" -f status=success -f per_page=50 --jq '.workflow_runs | map(select(.name == "CI" and .event == "push" and .head_branch == "main")) | first | .id')" || no_evidence 'run lookup failed'
+          [[ -n "$run_id" && "$run_id" != null ]] || no_evidence 'no successful CI push run on main'
+          artifact_name="$(gh api --method GET "repos/${GITHUB_REPOSITORY}/actions/runs/${run_id}/artifacts" --jq '.artifacts | map(select(.expired == false and (.name | startswith("auths-formal-translation-")))) | first | .name')" || no_evidence "run ${run_id} artifact lookup failed"
+          [[ -n "$artifact_name" && "$artifact_name" != null ]] || no_evidence "run ${run_id} has no unexpired translation artifact"
+          mkdir -p target/reused-formal
+          gh run download "$run_id" --name "$artifact_name" --dir target/reused-formal || no_evidence "artifact ${artifact_name} could not be downloaded"
+          mapfile -t evidence < <(find target/reused-formal -type f -name aeneas-qualification.json)
+          [[ "${#evidence[@]}" == 1 ]] || no_evidence "artifact ${artifact_name} does not hold exactly one evidence file"
+          echo "AUTHS_REUSED_TRANSLATION_EVIDENCE=${evidence[0]}" >> "$GITHUB_ENV"
+          echo 'found=true' >> "$GITHUB_OUTPUT"
+          echo "Translation: protected-base run ${run_id}, artifact ${artifact_name}" >> "$GITHUB_STEP_SUMMARY"
+      - name: Verify and bind protected-base translation evidence
+        if: steps.protected-base-translation.outputs.found == 'true'
+        env:
+          AUTHS_FORMAL_PHASE_CLOSURE_SHA256: ${{ needs.ci-plan.outputs.formal_translation_digest }}
+          AUTHS_FORMAL_TOOLCHAIN_CLOSURE_SHA256: ${{ needs.ci-plan.outputs.formal_toolchain_digest }}
+          AUTHS_FORMAL_EVIDENCE_CLOSURE_SHA256: ${{ needs.ci-plan.outputs.formal_evidence_digest }}
+        run: cargo xtask ci formal-translation-reuse
+      # Two clean reproductions run unless a reuse step above located evidence:
+      # for a cold plan, a same-PR miss, and absent protected-base evidence.
       - name: Reclaim disk for cold translation
-        if: needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true'
+        if: steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true'
         shell: bash
         run: |
           set -euo pipefail
           sudo rm -rf /opt/ghc /opt/hostedtoolcache/CodeQL /usr/local/.ghcup /usr/local/lib/android /usr/share/dotnet
           sudo docker system prune --all --force
           sudo apt-get clean
       - name: Install pinned Nix with the public Aeneas Cachix substitute
-        if: needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true'
+        if: steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true'
         uses: cachix/install-nix-action@ab739621df7a23f52766f9ccc97f38da6b7af14f # v31.10.5
         with:
           extra_nix_config: |
             extra-substituters = https://hacl.cachix.org
             extra-trusted-public-keys = hacl.cachix.org-1:FzsZ2xsByOwKwIWNPII7yMOelJNDZ12mDAj3d1eGX0c=
       - name: Acquire pinned Aeneas and Charon
-        if: needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true'
+        if: steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true'
         run: >-
           nix build
           --print-build-logs
@@ -420,7 +460,7 @@ jobs:
           github:AeneasVerif/aeneas/3a8586facab25b31bdb1e1f5f45acd60d1cc5ff0#aeneas
           --out-link target/formal-tools
       - name: Reproduce translation twice
-        if: needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true'
+        if: steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true'
         env:
           AUTHS_AENEAS_BIN: ${{ github.workspace }}/target/formal-tools/bin/aeneas
           AUTHS_CHARON_BIN: ${{ github.workspace }}/target/formal-tools/bin/charon
@@ -431,7 +471,7 @@ jobs:
         run: cargo xtask ci formal-translation-reproduce
       - id: formal-update
         name: Package a bounded translation update
-        if: github.event_name == 'pull_request' && needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true'
+        if: github.event_name == 'pull_request' && steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true'
         env:
           AUTHS_BASE_SHA: ${{ github.event.pull_request.base.sha }}
         run: |
@@ -461,31 +501,6 @@ jobs:
         run: |
           echo "Generated Aeneas output drifted; the bounded updater will commit the reviewed artifact set."
           exit 1
-      - name: Locate protected-base translation evidence
-        if: needs.ci-plan.outputs.formal_cold_required != 'true'
-        env:
-          GH_TOKEN: ${{ github.token }}
-          AUTHS_BASE_SHA: ${{ github.event.pull_request.base.sha }}
-        shell: bash
-        run: |
-          set -euo pipefail
-          run_id="$(gh api --method GET "repos/${GITHUB_REPOSITORY}/actions/runs" -f head_sha="$AUTHS_BASE_SHA" -f status=success -f per_page=50 --jq '.workflow_runs | map(select(.name == "CI" and .event == "push" and .head_branch == "main")) | first | .id')"
-          [[ -n "$run_id" && "$run_id" != null ]]
-          artifact_name="$(gh api --method GET "repos/${GITHUB_REPOSITORY}/actions/runs/${run_id}/artifacts" --jq '.artifacts | map(select(.expired == false and (.name | startswith("auths-formal-translation-")))) | first | .name')"
-          [[ -n "$artifact_name" && "$artifact_name" != null ]]
-          mkdir -p target/reused-formal
-          gh run download "$run_id" --name "$artifact_name" --dir target/reused-formal
-          mapfile -t evidence < <(find target/reused-formal -type f -name aeneas-qualification.json)
-          [[ "${#evidence[@]}" == 1 ]]
-          echo "AUTHS_REUSED_TRANSLATION_EVIDENCE=${evidence[0]}" >> "$GITHUB_ENV"
-          echo "Translation: protected-base run ${run_id}, artifact ${artifact_name}" >> "$GITHUB_STEP_SUMMARY"
-      - name: Verify and bind protected-base translation evidence
-        if: needs.ci-plan.outputs.formal_cold_required != 'true'
-        env:
-          AUTHS_FORMAL_PHASE_CLOSURE_SHA256: ${{ needs.ci-plan.outputs.formal_translation_digest }}
-          AUTHS_FORMAL_TOOLCHAIN_CLOSURE_SHA256: ${{ needs.ci-plan.outputs.formal_toolchain_digest }}
-          AUTHS_FORMAL_EVIDENCE_CLOSURE_SHA256: ${{ needs.ci-plan.outputs.formal_evidence_digest }}
-        run: cargo xtask ci formal-translation-reuse
       - name: Preserve reusable translation evidence
         if: steps.formal-update.outputs.update_required != 'true'
         uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7
@@ -508,7 +523,7 @@ jobs:
         with:
           phase: translation
           started-at: ${{ env.AUTHS_FORMAL_STARTED_AT }}
-          execution: ${{ steps.prior-pr-translation.outputs.reused == 'true' && 'reused-pr-run' || needs.ci-plan.outputs.formal_cold_required == 'true' && 'executed-cold' || 'reused-protected-base' }}
+          execution: ${{ steps.prior-pr-translation.outputs.reused == 'true' && 'reused-pr-run' || steps.protected-base-translation.outputs.found == 'true' && 'reused-protected-base' || steps.protected-base-translation.outputs.found == 'false' && 'executed-cold-without-base-evidence' || 'executed-cold' }}
 
   formal-kani-run:
     name: formal Kani

docs/PROGRAM_BOARD.md

@@ -202,6 +202,7 @@ gates do not shrink.
 | 2026-09-25 | Owner direction: the 2026-09-24 review pass is implemented as PRs in priority order, without filing public issues; a security weakness goes to a private advisory first. Decisions inside that work that the owner has not taken follow rule 8 (narrower reading, logged PROVISIONAL). | §3 "Review pass 2026-09-24"; `docs/audit/settled.md` |
 | 2026-09-25 | PROVISIONAL, taken unattended as the narrower readings for package 2.5 (kernel conformance) of the 2026-09-24 review, whose check-precedence decision the owner delegated: native's current order is codified, and only the attachment-limit line changes in Rust. (1) The canonical action is decoded, with its input, body, and detached-attachment bounds, before the proof, and a failure there carries no plan digest. The Go and TypeScript verifiers decode it the same way and return the native codes: fields read in key order, each bound checked as its field is read, the canonical encoding checked last. (2) Detached attachments are bounded by the aggregate attachment limit, as the spec and CDDL already said; native used the bundle limit, which denied attachments between the two limits and ignored a lowered attachment limit in process. (3) One check precedence, native's: decode (context, canonical action, proof), reference resolution, principal control (registry manifest and configuration first), action binding before any branch, authority branches, then plan and composition. Binding runs the carried body, each action's fields, profile, audience, challenge, evaluation time, channel, shared meaning, extensions, and observation attachments, then attachments, then the profile policy. Each branch runs root control, anchor acceptance, statuses (the anchor, then each grant's status and subject), the resource matcher, namespaces, the budget chain, the delegation walk, terminal coverage, the action's control, assurance, and observation. A statement's control failure is deferred to the branch that needs it. (4) Every grant permission's resource, not only the action's, must lie inside the anchor's namespaces, as native requires. (5) A budget algebra is resolved only where a bounded ceiling is compared, and a value in another algebra is local-policy-denied, the algebra rejecting its input; Go and TypeScript had resolved every algebra up front, including those of unrelated anchors, and returned indeterminate. (6) For a grant after the first, the observation-requirement drop check and the attenuation laws run before any handler evaluates the grant's extensions, so a malformed or over-limit child payload is `observation-requirement-dropped` under a parent with requirements and `delegation-expanded` otherwise, never the handler's code; `protocol.md` now defers to the per-extension laws instead of byte-for-byte preservation. | `core/spec/v1/verification-algorithm.md` "Stages"; `core/spec/v1/registry.md` "Attenuation laws"; `core/spec/v1/protocol.md` "Trust anchor", "Grant"; `core/spec/v1/error-codes.md`; `docs/LIMIT_COVERAGE.md` |
 | 2026-09-25 | PROVISIONAL, taken unattended as the narrower readings for package 2.6 (status statements) of the 2026-09-24 review, whose `purpose` decision the owner left open: (1) `purpose` is removed from principal-status statements rather than given purpose-scoped selection, which would add role semantics no spec defines. The wire loses key 3 and the later keys move down one, one direct cutover with no reader for the old shape (a ten-entry statement is `malformed-proof`); the carried-status rollback check keys on the principal alone, as selection does; the Python and WASM authoring APIs and the TypeScript engine contract drop the argument. (2) The accepted-extension rule covers every statement about a principal or grant whose status a branch evaluates, whatever its method or issuer and whether or not selection would pick it, checked after the statement's control and before selection; statements about subjects the branch does not evaluate are not checked. (3) As for actions and grants, the first extension in canonical order decides: an identifier the context does not accept is `critical-extension-unknown`, an accepted one `unsupported-critical-extension`. (4) No registered extension, `exact-marker-v1` included, has a status handler, so an accepted extension on an evaluated status statement is never evaluated and is always `unsupported-critical-extension`; a status extension needs a protocol review, an executable model, and a new manifest. | `core/spec/v1/protocol.md` "Evidence and status"; `core/spec/v1/verification-algorithm.md` "Principal status", "Grant status"; `core/spec/v1/registry.md` "Status-statement extensions"; `core/spec/v1/auths-proof.cddl` |
+| 2026-09-26 | The owner delegated the choice between two fixes. Taken: when protected-base translation evidence is missing, `formal translation` runs two clean reproductions in the same job, rather than also reusing base runs where only the translation job succeeded. Six of the last eight `main` push runs were cancelled by newer merges, which the second fix cannot cover. Evidence that is found but fails binding still fails the job, and every pull-request reproduction still packages generated drift. | `docs/ci/formal-translation-evidence.md`; `.github/workflows/ci.yml` |
 | 2026-09-26 | The owner delegated whether `formal Lean authoritative` fails when it packages an assurance update. Taken: it fails, as `formal translation` does, so the job that found the drift is the red one; the `formal-translation` gate and `CI qualified` were already red, and the updater keys off the update artifact, not job status. The job now declares the `update_required` output that `formal evidence` gates on, so aggregation is skipped instead of failing on a missing Lean artifact, and xtask requires both. | `.github/workflows/ci.yml`; `xtask/src/formal_qualification.rs` |
 
 ## 5. Not doing

docs/ci/formal-artifact-regeneration.md

@@ -13,6 +13,10 @@ Fork pull requests get the same downloadable artifact and diagnostic summary, bu
 never receive automatic writeback. A rejected artifact names the violated boundary
 (for example, an unexpected path, symlink, deletion, stale SHA, or size limit).
 
+[Formal translation evidence](formal-translation-evidence.md) describes when the
+translation job reproduces and when it reuses evidence, and how to recover a
+pull request by dispatching `ci.yml` on its branch.
+
 ## Architecture
 
 ```text

docs/ci/formal-translation-evidence.md

@@ -0,0 +1,62 @@
+# Formal translation evidence
+
+## How the job chooses its evidence
+
+The `formal translation` job qualifies the Aeneas translation of the exact head
+commit in one of three ways.
+
+| Path | When | Evidence |
+| --- | --- | --- |
+| Two clean reproductions | The plan requires a cold run: every push, schedule, and dispatch event, and every pull request that changes the translation, toolchain, or evidence closure. Also whenever no reusable evidence was located. | Aeneas and Charon run twice from source; the outputs must be byte-identical and match the committed generated files. |
+| Same pull request, earlier run | A pull request with a cold plan whose earlier run's `formal translation` job succeeded with the same closure digests. | That run's result, bound to this checkout. |
+| Protected base | A pull request that changes none of those closures, when a successful `CI` push run on `main` for the base commit published translation evidence. | The base run's evidence, bound to this checkout by `cargo xtask ci formal-translation-reuse`. |
+
+Reuse saves time; it is never required. The ci-plan summary line "reuse
+protected-base evidence" states the plan. The translation job decides at run
+time whether evidence exists.
+
+## Missing protected-base evidence
+
+The base commit often has no successful run. Its run may have failed in another
+job, been cancelled by a newer push to `main`, still be running, or have
+expired. The job then runs the two clean reproductions itself, and its summary
+says why:
+
+```text
+Translation: no protected-base evidence for base <sha> (no successful CI push run on main); executing two clean reproductions.
+```
+
+The phase timing records the execution as `executed-cold-without-base-evidence`.
+The fallback checks nothing less than a cold plan does. A pull-request
+reproduction runs in update mode: output that differs from the committed files
+is packaged for the [formal artifact updater](formal-artifact-regeneration.md)
+and the job fails until the regenerated files are committed.
+
+Evidence that is found but does not bind to this checkout fails the job. There
+is no fallback for that case. It means the committed generated artifacts or the
+translation source closure differ from what the base run qualified, although
+the plan saw no closure change. Look for hand-edited generated files or a file
+missing from the planner's closures.
+
+## Manual recovery
+
+Dispatch `ci.yml` on the pull request's branch:
+
+```bash
+gh workflow run ci.yml --repo auths-dev/auths-proof --ref <branch>
+```
+
+`workflow_dispatch` is a comprehensive event in
+`.github/ci/phase-ownership.toml`. The dispatched run plans every phase, runs
+two clean reproductions, and qualifies the branch head. Its checks are recorded
+on the same head commit as the pull-request run. The formal artifact updater
+starts CI the same way after it pushes regenerated artifacts. A dispatched run
+is not a pull-request event, so it never packages generated updates: drift makes
+it fail.
+
+A missing base run no longer needs this. Use it when:
+
+- found base evidence failed to bind, and the head should be qualified from
+  source instead of from the base run; or
+- a pull-request head needs a complete cold qualification without a new
+  commit.