diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7e29ec1c5..1e01e93e4 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -395,8 +395,48 @@ 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 @@ -404,14 +444,14 @@ jobs: 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 diff --git a/docs/PROGRAM_BOARD.md b/docs/PROGRAM_BOARD.md index cb0469b65..3debb47df 100644 --- a/docs/PROGRAM_BOARD.md +++ b/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 diff --git a/docs/ci/formal-artifact-regeneration.md b/docs/ci/formal-artifact-regeneration.md index 4d9b08292..4b030a201 100644 --- a/docs/ci/formal-artifact-regeneration.md +++ b/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 diff --git a/docs/ci/formal-translation-evidence.md b/docs/ci/formal-translation-evidence.md new file mode 100644 index 000000000..d2281813d --- /dev/null +++ b/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 (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 +``` + +`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. diff --git a/formal/assurance-manifest-v1.toml b/formal/assurance-manifest-v1.toml index 99475d9f5..bc5a29c7f 100644 --- a/formal/assurance-manifest-v1.toml +++ b/formal/assurance-manifest-v1.toml @@ -7184,7 +7184,7 @@ sha256 = "2bb401ffca0136622cd79bb14a5a38852061649a06cc46100503870c22d300c7" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-055" @@ -7291,7 +7291,7 @@ sha256 = "2bb401ffca0136622cd79bb14a5a38852061649a06cc46100503870c22d300c7" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-056" @@ -7412,7 +7412,7 @@ sha256 = "2bb401ffca0136622cd79bb14a5a38852061649a06cc46100503870c22d300c7" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-104" @@ -13544,7 +13544,7 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-189" @@ -13626,7 +13626,7 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-190" @@ -13708,7 +13708,7 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-191" @@ -13790,7 +13790,7 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-192" @@ -13871,7 +13871,7 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-193" @@ -13956,7 +13956,7 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-194" @@ -14041,7 +14041,7 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-195" @@ -14128,7 +14128,7 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-196" @@ -14218,7 +14218,7 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-197" @@ -14309,7 +14309,7 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-198" @@ -14391,7 +14391,7 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-199" @@ -14482,7 +14482,7 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-200" @@ -14563,7 +14563,7 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" [[claims]] claim_id = "AP-FORMAL-RICH-201" @@ -14644,4 +14644,4 @@ sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "39d75f8959dbb54c510cb17c7141c4d27a7ef388faa6d3ec232cb756a97b7a1d" +sha256 = "1b181fec646f4fe74a38081b6c347a27b792b69766709cc6e4cc9a1ecadb3773" diff --git a/formal/qualification/aeneas/source-closure.json b/formal/qualification/aeneas/source-closure.json index df87024c2..995832d97 100644 --- a/formal/qualification/aeneas/source-closure.json +++ b/formal/qualification/aeneas/source-closure.json @@ -1,6 +1,6 @@ { "schema": "auths-proof-translation-source-closure/v2", - "digest": "44e814dc02211e4c058560c80dc2aa3a04a8dcaac329b3c9eb41633c38cfab41", + "digest": "ab8a52b5cd6b01b3e22dab8529b0046ee06a024799f1c0c4147f65458c2b17f7", "files": [ { "path": ".cargo/config.toml", @@ -261,7 +261,7 @@ }, { "path": "xtask/src/formal_qualification.rs", - "sha256": "2247ffe9417de5abe0553fd56d65a4809c31d950975bd8388f6407f013ddd7ee" + "sha256": "085f9c6dae1beb23e2f0e8500a823fef7a360ea86507601e370a8cf57d375c07" }, { "path": "xtask/src/fuzz.rs", diff --git a/release/semantic-freeze-versions.toml b/release/semantic-freeze-versions.toml index 0737b673d..96a9f2a70 100644 --- a/release/semantic-freeze-versions.toml +++ b/release/semantic-freeze-versions.toml @@ -1,4 +1,4 @@ -freeze_version = 318 +freeze_version = 319 # Semantic identity counters live outside the xtask source tree deliberately. # The formal source closure binds xtask's executable code, while the semantic @@ -16,10 +16,10 @@ freeze_version = 318 "auths.frozen-bytes/core/fixtures/v1/manifest.json" = 13 "auths.frozen-bytes/core/formal-vectors/v1/manifest.json" = 1 "auths.frozen-bytes/demos/benchmarks/profiles/release.toml" = 1 -"auths.frozen-bytes/formal/assurance-manifest-v1.toml" = 37 +"auths.frozen-bytes/formal/assurance-manifest-v1.toml" = 38 "auths.frozen-bytes/formal/qualification/aeneas/generated" = 13 "auths.frozen-bytes/formal/qualification/aeneas/qualification.toml" = 9 -"auths.frozen-bytes/formal/qualification/aeneas/source-closure.json" = 76 +"auths.frozen-bytes/formal/qualification/aeneas/source-closure.json" = 77 "auths.frozen-bytes/product/conformance/v1/mechanism-profile-conformance.json" = 1 "auths.frozen-bytes/product/conformance/v1/simplified-product-waist.json" = 3 "auths.frozen-bytes/product/fixtures/v1/bounded-policy/manifest.json" = 3 @@ -67,5 +67,5 @@ freeze_version = 318 "auths.product.simplified-waist" = 17 "auths.product.vocabulary" = 20 "auths.release.benchmark-contract" = 1 -"auths.release.evolution-contract" = 72 -"auths.release.public-surface" = 318 +"auths.release.evolution-contract" = 73 +"auths.release.public-surface" = 319 diff --git a/release/semantic-freeze.json b/release/semantic-freeze.json index 821c5db3e..edb3925e2 100644 --- a/release/semantic-freeze.json +++ b/release/semantic-freeze.json @@ -1,6 +1,6 @@ { "schema": "auths.semantic-freeze/1", - "freezeVersion": 318, + "freezeVersion": 319, "publicSurface": { "rustRoots": [ "auths", @@ -202,7 +202,7 @@ }, { "id": "auths.frozen-bytes/formal/assurance-manifest-v1.toml", - "version": 37, + "version": 38, "classification": "frozen-bytes", "categories": [ "canonical-generated-evidence" @@ -210,7 +210,7 @@ "owners": [ "formal/assurance-manifest-v1.toml" ], - "sha256": "9a832a6b731368cfad9d9d39aa4dcfbbe8ae72009d80b49e19803525f50038af" + "sha256": "f572820f17c56208002802f9594045e7da16500e044ff728d1a714c6c7dd428c" }, { "id": "auths.frozen-bytes/formal/qualification/aeneas/generated", @@ -238,7 +238,7 @@ }, { "id": "auths.frozen-bytes/formal/qualification/aeneas/source-closure.json", - "version": 76, + "version": 77, "classification": "frozen-bytes", "categories": [ "canonical-generated-evidence" @@ -246,7 +246,7 @@ "owners": [ "formal/qualification/aeneas/source-closure.json" ], - "sha256": "586fe3aaaec69f1ccbe0cda7c8a2ca7790ca6143416611911f822889054aea4a" + "sha256": "b2bee1b1e65ced8e3b7042f4d64897fac2cf9d2912be3a3ec98ac643225d66da" }, { "id": "auths.frozen-bytes/product/conformance/v1/mechanism-profile-conformance.json", @@ -1019,7 +1019,7 @@ }, { "id": "auths.release.evolution-contract", - "version": 72, + "version": 73, "classification": "frozen-meaning", "categories": [ "version-axes", @@ -1040,11 +1040,11 @@ "release/fixtures/evolution", "xtask/src/evolution_policy.rs" ], - "sha256": "5b3fc0bce975a7c05be2e002d52f3002650b5777de5ef591b61703f95021489a" + "sha256": "b5be11aac2717b99d2a699ba23a163b42f5fb0cd54c2850a49b0b219269f5303" }, { "id": "auths.release.public-surface", - "version": 318, + "version": 319, "classification": "release-metadata", "categories": [ "package-names", @@ -1136,7 +1136,7 @@ "xtask/src/release_control.rs", "xtask/src/semantic_freeze.rs" ], - "sha256": "a3fbb18e8c356429c97ca88690c634abc1211a29839e537c16d44b4494cc3459" + "sha256": "8f6be22755727f1b65a62ce600e30e494f7569e961c0a954b35594fcd6113988" } ] } diff --git a/xtask/src/formal_qualification.rs b/xtask/src/formal_qualification.rs index 8a0b96d1d..cc0b880c9 100644 --- a/xtask/src/formal_qualification.rs +++ b/xtask/src/formal_qualification.rs @@ -1388,6 +1388,7 @@ fn validate_ci_workflow_gates(ci: &str) -> Result<(), String> { .to_owned(), ); } + validate_translation_evidence_selection(formal_job)?; for job_name in [ "authoritative-run", "compliance-run", @@ -1499,6 +1500,70 @@ fn validate_ci_workflow_gates(ci: &str) -> Result<(), String> { Ok(()) } +/// Condition of every step on the two-reproduction path: it runs unless a +/// reuse step located evidence, so a cold plan, a same-PR miss, and absent +/// protected-base evidence all reach it. +const TRANSLATION_REPRODUCTION_CONDITION: &str = "steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true'"; + +/// 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; the job then executes the same two +/// clean reproductions as a cold plan. A pull-request reproduction runs in +/// update mode and rewrites drifted outputs in place, so the packaging step +/// must share its condition, or drift would qualify instead of stopping the +/// job. Located evidence is reused only through the binding step, whose +/// failure fails the job rather than falling back. +fn validate_translation_evidence_selection(job: &str) -> Result<(), String> { + let locate = workflow_step_source(job, "Locate protected-base translation evidence")?; + let bind = workflow_step_source(job, "Verify and bind protected-base translation evidence")?; + let reproduce = workflow_step_source(job, "Reproduce translation twice")?; + let package = workflow_step_source(job, "Package a bounded translation update")?; + if !locate.contains("- id: protected-base-translation\n") + || !bind.contains("\n if: steps.protected-base-translation.outputs.found == 'true'\n") + || !reproduce.contains(&format!( + "\n if: {TRANSLATION_REPRODUCTION_CONDITION}\n" + )) + || !package.contains(&format!( + "\n if: github.event_name == 'pull_request' && {TRANSLATION_REPRODUCTION_CONDITION}\n" + )) + { + return Err( + "hosted translation must reuse protected-base evidence only once located and bound, and otherwise execute two clean reproductions that package generated drift" + .to_owned(), + ); + } + Ok(()) +} + +/// One step of a workflow job, from its list marker to the next step's, so a +/// condition is read from the step it gates rather than from anywhere in the +/// job. +fn workflow_step_source<'a>(job: &'a str, step_name: &str) -> Result<&'a str, String> { + let name = format!("name: {step_name}"); + let starts: Vec<_> = job + .match_indices("\n - ") + .map(|(index, _)| index) + .collect(); + let ends = starts + .iter() + .skip(1) + .copied() + .chain(std::iter::once(job.len())); + starts + .iter() + .copied() + .zip(ends) + .map(|(start, end)| &job[start..end]) + .find(|step| { + step.lines().any(|line| { + line.strip_prefix(" - ") + .or_else(|| line.strip_prefix(" ")) + == Some(name.as_str()) + }) + }) + .ok_or_else(|| format!("hosted CI omits the `{step_name}` step")) +} + fn workflow_job_source<'a>(workflow: &'a str, job_name: &str) -> Result<&'a str, String> { let marker = format!("\n {job_name}:"); let tail = workflow @@ -2289,12 +2354,24 @@ cargo xtask ci formal-proof-fast needs: [ci-plan, formal-update-gate, repository-preflight] needs.repository-preflight.result == 'success' compiler-cache: "false" -AUTHS_FORMAL_UPDATE_MODE -formal-update-artifact create -Preserve the bounded translation update -Stop qualification until generated translation is committed -cargo xtask ci formal-translation-reproduce -cargo xtask ci formal-translation-reuse + - id: protected-base-translation + name: Locate protected-base translation evidence + if: needs.ci-plan.outputs.formal_cold_required != 'true' + run: echo 'found=false' >> "$GITHUB_OUTPUT" + - name: Verify and bind protected-base translation evidence + if: steps.protected-base-translation.outputs.found == 'true' + run: cargo xtask ci formal-translation-reuse + - name: Reproduce translation twice + if: steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true' + env: + AUTHS_FORMAL_UPDATE_MODE: ${{ github.event_name == 'pull_request' && 'true' || 'false' }} + run: cargo xtask ci formal-translation-reproduce + - id: formal-update + name: Package a bounded translation update + if: github.event_name == 'pull_request' && steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true' + run: cargo run --locked -p auths-ci-plan -- formal-update-artifact create + - name: Preserve the bounded translation update + - name: Stop qualification until generated translation is committed formal-kani-run: needs: [ci-plan, formal-update-gate, repository-preflight] needs.repository-preflight.result == 'success' @@ -2379,6 +2456,47 @@ needs.formal-kani.result validate_ci_workflow_gates(CI_GATES).expect("hosted CI gates must satisfy formal policy"); } + #[test] + fn committed_hosted_ci_satisfies_formal_policy() { + validate_ci_workflow_gates(include_str!("../../.github/workflows/ci.yml")) + .expect("the committed hosted CI workflow must satisfy formal policy"); + } + + #[test] + fn missing_protected_base_evidence_executes_two_clean_reproductions() { + let base_run_required = CI_GATES.replace( + "name: Reproduce translation twice\n if: steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true'\n", + "name: Reproduce translation twice\n if: needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true'\n", + ); + let error = validate_ci_workflow_gates(&base_run_required).expect_err( + "a base commit without successful CI must not fail every pull request on it", + ); + assert!(error.contains("otherwise execute two clean reproductions")); + } + + #[test] + fn every_update_mode_reproduction_packages_its_drift() { + let unpackaged = CI_GATES.replace( + "if: github.event_name == 'pull_request' && steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true'\n", + "if: github.event_name == 'pull_request' && needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true'\n", + ); + let error = validate_ci_workflow_gates(&unpackaged).expect_err( + "a fallback reproduction that rewrote drifted outputs must still stop the job", + ); + assert!(error.contains("that package generated drift")); + } + + #[test] + fn protected_base_reuse_requires_located_evidence() { + let unlocated = CI_GATES.replace( + "if: steps.protected-base-translation.outputs.found == 'true'\n", + "if: needs.ci-plan.outputs.formal_cold_required != 'true'\n", + ); + let error = validate_ci_workflow_gates(&unlocated) + .expect_err("binding must not run when no evidence was located"); + assert!(error.contains("only once located and bound")); + } + #[test] fn hosted_ci_cannot_omit_pinned_lean_setup() { let error = validate_ci_workflow_gates(