CBMC: Push performance data to gh-pages

.github/actions/cbmc/action.yml

@@ -61,7 +61,7 @@ runs:
           GH_TOKEN: ${{ inputs.gh_token }}
           PARAMETER_SET: ${{ inputs.mldsa_parameter_set }}
           REDUCE_RAM: ${{ inputs.reduce_ram }}
-          WORKSPACE: ${{ github.workspace }}
+          RESULTS_DIR: ${{ runner.temp }}/cbmc-results
         run: |
           echo "::group::cbmc_$PARAMETER_SET"
           reduce_ram_flag=""
@@ -72,14 +72,25 @@ runs:
             data_dir="dev/cbmc-reduce-ram"
             variant="reduce-ram"
           fi
-          tests cbmc --mldsa-parameter-set "$PARAMETER_SET" --dm all --solver all --per-proof-timeout 1800 --output-result-json "$WORKSPACE/cbmc_result_$PARAMETER_SET.json" $reduce_ram_flag || cbmc_failed=true
+          # Write the results at their gh-pages path; see cbmc_publish.yml.
+          result="$RESULTS_DIR/$data_dir/mldsa-$PARAMETER_SET.json"
+          mkdir -p "$(dirname "$result")"
+          tests cbmc --mldsa-parameter-set "$PARAMETER_SET" --dm all --solver all --per-proof-timeout 1800 --output-result-json "$result" $reduce_ram_flag || cbmc_failed=true
           echo "::endgroup::"
           python3 "$ACTION_PATH/report.py" \
-            --results-json "$WORKSPACE/cbmc_result_$PARAMETER_SET.json" \
+            --results-json "$result" \
             --mldsa-parameter-set "$PARAMETER_SET" \
             --min-runtime 20 \
             --regression-threshold 1.5 \
             --gh-pages-branch gh-pages \
             --data-dir "$data_dir" \
             --variant "$variant"
           if [ "$cbmc_failed" = "true" ]; then exit 1; fi
+      - name: Upload CBMC results for publishing
+        if: ${{ github.event_name == 'merge_group' }}
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
+        with:
+          name: cbmc-results-mldsa-${{ inputs.mldsa_parameter_set }}${{ inputs.reduce_ram == 'true' && '-reduce-ram' || '' }}
+          path: ${{ runner.temp }}/cbmc-results/
+          if-no-files-found: error
+          retention-days: 7

.github/actions/cbmc/report.py

@@ -5,7 +5,6 @@
 """CBMC proof results reporter for GitHub Actions."""
 
 import argparse
-import base64
 import json
 import os
 import subprocess
@@ -14,8 +13,6 @@
 
 # GitHub context
 GITHUB_REPOSITORY = os.environ.get("GITHUB_REPOSITORY", "")
-GITHUB_REF = os.environ.get("GITHUB_REF", "")
-GITHUB_SHA = os.environ.get("GITHUB_SHA", "")[:7]
 
 COMMENT_TAG = "cbmc-report"
 
@@ -120,7 +117,11 @@ def index_baseline(baseline):
 def classify_proof(r, baseline_by_config, baseline_by_name, cfg):
     """Classify a single proof result, returning (ProofResult, is_alert)."""
     name, dm, solver = config_key(r)
-    base = baseline_by_config.get((name, dm, solver), baseline_by_name.get(name, {}))
+    base = baseline_by_config.get((name, dm, solver))
+    if base is None:
+        # Legacy baselines have one entry per proof, timed with the default
+        # configuration. Comparing other configurations with it is misleading.
+        base = baseline_by_name.get(name, {}) if r.get("default", False) else {}
     base_val, base_failed = base.get("value"), base.get("status") == "failed"
     base_omitted = base.get("status") == "omitted"
     base_inconclusive = base.get("status") == "inconclusive"
@@ -337,44 +338,6 @@ def post_or_update_comment(pr_number, body, cfg):
         os.unlink(tmp_path)
 
 
-def push_to_gh_pages(current, cfg):
-    """Push results to gh-pages branch using GitHub Contents API."""
-    file_path = f"{cfg.data_dir}/mldsa-{cfg.param_set}.json"
-    content_b64 = base64.b64encode(json.dumps(current, indent=2).encode()).decode()
-
-    result = subprocess.run(
-        [
-            "gh",
-            "api",
-            f"repos/{GITHUB_REPOSITORY}/contents/{file_path}?ref={cfg.gh_pages_branch}",
-            "--jq",
-            ".sha",
-        ],
-        capture_output=True,
-        text=True,
-    )
-    sha = result.stdout.strip() if result.returncode == 0 else ""
-
-    cmd = [
-        "gh",
-        "api",
-        f"repos/{GITHUB_REPOSITORY}/contents/{file_path}",
-        "-X",
-        "PUT",
-        "-F",
-        f"message=Update CBMC results for ML-DSA-{cfg.param_set} ({GITHUB_SHA})",
-        "-F",
-        f"content={content_b64}",
-        "-F",
-        f"branch={cfg.gh_pages_branch}",
-    ]
-    if sha:
-        cmd.extend(["-F", f"sha={sha}"])
-
-    subprocess.run(cmd, check=True)
-    print(f"Pushed results to {cfg.gh_pages_branch}")
-
-
 def main():
     args = get_args()
     args.param_set = args.mldsa_parameter_set
@@ -388,10 +351,8 @@ def main():
     pr_number = get_pr_number()
     if pr_number:
         post_or_update_comment(pr_number, build_comment(current, baseline, args), args)
-    elif GITHUB_REF in ("refs/heads/main", "refs/heads/master"):
-        push_to_gh_pages(current, args)
     else:
-        print(f"Not a PR and not main branch ({GITHUB_REF}), skipping")
+        print("Not a PR, skipping")
 
 
 if __name__ == "__main__":

.github/workflows/cbmc_publish.yml

@@ -0,0 +1,51 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+# When a commit lands on main, copy the CBMC results from its merge queue
+# run to gh-pages. PR reports use them as the baseline.
+
+name: CBMC publish
+permissions:
+  contents: read
+on:
+  push:
+    branches: ["main"]
+
+concurrency: cbmc-publish
+
+jobs:
+  publish:
+    name: Publish CBMC baselines
+    if: ${{ github.repository_owner == 'pq-code-package' }}
+    runs-on: ubuntu-latest
+    permissions:
+      actions: read
+      contents: write
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          ref: gh-pages
+          persist-credentials: false
+      - name: Publish CBMC results to gh-pages
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          # The merge queue fast-forwards main to the commit it tested.
+          run_id=$(gh api "repos/$GITHUB_REPOSITORY/actions/workflows/all.yml/runs?event=merge_group&head_sha=$GITHUB_SHA" \
+            --jq '.workflow_runs | max_by(.created_at) | .id // empty')
+          if [ -z "$run_id" ]; then
+            echo "::warning::$GITHUB_SHA has no merge queue run; skipping"
+            exit 0
+          fi
+
+          # Each artifact holds one result file under its gh-pages path.
+          gh run download "$run_id" -R "$GITHUB_REPOSITORY" --pattern 'cbmc-results-*' --dir "$RUNNER_TEMP/cbmc-results"
+          cp -r "$RUNNER_TEMP"/cbmc-results/*/dev .
+
+          git config user.name "github-actions[bot]"
+          git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
+          git add dev
+          git diff --cached --quiet || git commit -m "Update CBMC results (${GITHUB_SHA::7})"
+          # Rebase and retry once if bench.yml pushed first.
+          remote="https://x-access-token:$GH_TOKEN@github.com/$GITHUB_REPOSITORY"
+          git push "$remote" HEAD:gh-pages || { git pull --rebase origin gh-pages && git push "$remote" HEAD:gh-pages; }