From 8882e339317ce2c69f2a84acad14e00f6d36da58 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Sun, 25 Oct 2026 13:17:27 +0000 Subject: [PATCH 1/2] CBMC: Only use name-only baselines for default configurations CI posts a CBMC runtime report on each PR. report.py compares the runtime of each proof configuration (proof name, `dm`, solver) with a baseline stored on the gh-pages branch. Baselines written before configurations existed have a single entry per proof name, timed with the default solver. classify_proof() fell back to that name-only entry for every configuration without an exact match. A secondary solver was therefore compared with the default solver's time and flagged as a regression. For example, poly_caddq_native with bitwuzla showed 112s against 3s, which is the time of the default z3 configuration. Use the name-only entry only for default configurations. Other configurations without an exact baseline entry are now reported as `new`. Signed-off-by: Hanno Becker --- .github/actions/cbmc/report.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/actions/cbmc/report.py b/.github/actions/cbmc/report.py index d4da70855d..045a038c34 100644 --- a/.github/actions/cbmc/report.py +++ b/.github/actions/cbmc/report.py @@ -120,7 +120,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" From de6cb3bdd97dfd87f9fae7b5e806613878cc5ef2 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Sun, 25 Oct 2026 14:09:59 +0000 Subject: [PATCH 2/2] CI: Publish CBMC baselines from merge queue runs PR reports compare CBMC runtimes with baselines on gh-pages (dev/cbmc[-reduce-ram]/mldsa-{44,65,87}.json). report.py wrote them in CI runs on main. Since 529a89dd ("CI: Do not run on pushes to main"), CI runs on PRs and in the merge queue only, and the baselines are still those of 2026-07-03, from before per-configuration timings. The merge queue tests the exact commit that main is then fast-forwarded to, so its timings are the right baseline. When a batch of PRs merges as one push, the run for the tip covers the whole batch. - Each CBMC job writes its result file at its gh-pages path under $RUNNER_TEMP/cbmc-results. In merge queue runs it uploads that tree as artifact cbmc-results-mldsa-[-reduce-ram]. A failing proof fails the step before the upload. - cbmc_publish.yml runs on each push to main. It finds the merge queue run of all.yml for the pushed commit, downloads its artifacts into a gh-pages checkout, and pushes them as one commit with the workflow token. If bench.yml pushed first, it rebases and retries once. For a commit that reached main outside the merge queue, it warns and skips. The workflow pushes with git instead of the Contents API that push_to_gh_pages() used. A result file now has 3010 entries (215 proofs, 2 data models, 7 solver profiles), about 570 KiB. Its base64 encoding is too long for the single `-F content=...` argument of `gh api`: Linux limits one argument to 128 KiB. Remove push_to_gh_pages() and the refs/heads/main branch of report.py main() that called it. Signed-off-by: Hanno Becker --- .github/actions/cbmc/action.yml | 17 ++++++++-- .github/actions/cbmc/report.py | 45 +------------------------- .github/workflows/cbmc_publish.yml | 51 ++++++++++++++++++++++++++++++ 3 files changed, 66 insertions(+), 47 deletions(-) create mode 100644 .github/workflows/cbmc_publish.yml diff --git a/.github/actions/cbmc/action.yml b/.github/actions/cbmc/action.yml index fa1d0a309e..44aea485f8 100644 --- a/.github/actions/cbmc/action.yml +++ b/.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,10 +72,13 @@ 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 \ @@ -83,3 +86,11 @@ runs: --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 diff --git a/.github/actions/cbmc/report.py b/.github/actions/cbmc/report.py index 045a038c34..c484238537 100644 --- a/.github/actions/cbmc/report.py +++ b/.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" @@ -341,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 @@ -392,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__": diff --git a/.github/workflows/cbmc_publish.yml b/.github/workflows/cbmc_publish.yml new file mode 100644 index 0000000000..d232c642e7 --- /dev/null +++ b/.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; }