ci: Set bencher measure slug as source of truth

.github/workflows/bench-main.yml

@@ -308,7 +308,7 @@ jobs:
       # and throughput are phase-scoped by the CELL (execute vs prove
       # testbed), and prove-time/verify-time/proof-size exist only on the
       # prove testbed — a threshold naming an absent measure just sits
-      # empty there. The per-phase `phase:<span>` measures (witness gen,
+      # empty there. The per-phase `phase-<span>` measures (witness gen,
       # stage commits, quotient, …) are uploaded for trend visibility but
       # intentionally left un-thresholded (noisy and dynamically named;
       # the PR-comment drill-down does the phase-level comparison).

.github/workflows/bench-pr.yml

@@ -654,18 +654,27 @@ jobs:
         env:
           PARSE_ERROR: ${{ needs.build.outputs.parse-error }}
         run: |
-          {
-            echo "## ❌ benchmark run failed"
-            if [ -n "$PARSE_ERROR" ]; then
+          if [ -f comment-body.md ]; then
+            # A report exists: some job failed but results came through.
+            # Soft note on top; the report's own footer links the logs.
+            {
+              echo "> ⚠️ Some benchmark jobs failed — results may be partial."
               echo
-              echo "> $PARSE_ERROR"
-            fi
-            echo
-            if [ -f comment-body.md ]; then cat comment-body.md; fi
-            echo
-            echo "[Workflow logs](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})"
-          } > body-with-header.md
-          mv body-with-header.md comment-body.md
+              cat comment-body.md
+            } > body-with-note.md
+            mv body-with-note.md comment-body.md
+          else
+            # No report at all: the run itself failed.
+            {
+              echo "## ❌ benchmark run failed"
+              if [ -n "$PARSE_ERROR" ]; then
+                echo
+                echo "> $PARSE_ERROR"
+              fi
+              echo
+              echo "[Workflow logs](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})"
+            } > comment-body.md
+          fi
       - name: Generate token to write PR comment
         id: app-token
         uses: actions/create-github-app-token@v3

Ix/Cli/BenchCmd.lean

@@ -17,7 +17,7 @@
      ONE PROCESS PER CONSTANT: a kill costs exactly that constant (its row
      is marked `status: oom`, keeping whatever the tool flushed), and each
      spawn's texray window (`<out>.spans`) belongs wholly to it, folded
-     into the row as flat `phase:<span>` fields — independent bencher
+     into the row as flat `phase-<span>` fields — independent bencher
      measures with no attribution machinery;
   4. gates the cell on the row contract (`Ix.Benchmark.Results`): exit 3
      when any row is `rejected`, exit 1 when NO rows were produced, else 0.
@@ -237,8 +237,20 @@ def readSpans (path : String) : IO (Array (String × Float)) := do
         | none => acc := acc.push (s, v)
   return acc
 
+/-- A span name as a bencher-legal measure slug: lowercase alphanumerics
+    with every other character folded to `-` (`stark/stage1_commit` →
+    `stark-stage1-commit`). Row keys ARE bencher measure slugs — the slug
+    is the one identity uploads and `fetch-main` agree on — so they must
+    be born slug-shaped. -/
+def slugify (s : String) : String :=
+  let dashed := s.toList.map fun c => if c.isAlphanum then c.toLower else '-'
+  -- Collapse runs so `a__b` and `a_b` can't alias two spellings apart.
+  let folded := dashed.foldl (init := []) fun acc c =>
+    if c == '-' && acc.head? == some '-' then acc else c :: acc
+  String.ofList folded.reverse
+
 /-- Fold a spawn's texray window (`<out>.spans`) into its constant's row as
-    flat `phase:<span>` fields — the aiur prover's tracing spans and the
+    flat `phase-<span>` fields — the aiur prover's tracing spans and the
     zkVM hosts' `record_manual` entries alike — then drop the window file.
     The keys pass straight through `bmf` as independent bencher measures
     and come back from `fetch-main` in the same shape. No row (the tool
@@ -250,7 +262,7 @@ def mergeSpans (out : String) (name : String) : IO Unit := do
     let rows ← readRows out
     if let some row := (rows.getObjVal? name).toOption then
       let row := spans.foldl (init := row) fun r (s, v) =>
-        r.setObjVal! s!"phase:{s}" (jsonRound 6 v)
+        r.setObjVal! s!"phase-{slugify s}" (jsonRound 6 v)
       writeEntry out name row
   if ← FilePath.pathExists spansPath then
     IO.FS.removeFile spansPath

Ix/Cli/BenchReport.lean

@@ -36,7 +36,7 @@ namespace Ix.Cli.BenchReport
 def metricKind (metric : String) : String :=
   if ["peak-rss", "file-size", "proof-size"].contains metric
   then "bytes"
-  else if metric.startsWith "phase:" then "seconds"
+  else if metric.startsWith "phase-" then "seconds"
   else if ["execute-time", "prove-time", "verify-time", "check-time",
            "compile-time"].contains metric then "seconds"
   else if ["fft-cost", "cycles", "steps", "max-shard-cycles",
@@ -135,11 +135,11 @@ def rowNames (rows : Json) : Array String :=
   | .obj kvs => kvs.toArray.map (·.1)
   | _ => #[]
 
-/-- The `phase:<span>` field names of one row (flat keys — same shape on
+/-- The `phase-<span>` field names of one row (flat keys — same shape on
     the PR side, in local baselines, and coming back from bencher). -/
 def rowPhaseKeys (rows : Json) (name : String) : Array String :=
   match (rows.getObjVal? name).toOption with
-  | some (.obj kvs) => kvs.toArray.map (·.1) |>.filter (·.startsWith "phase:")
+  | some (.obj kvs) => kvs.toArray.map (·.1) |>.filter (·.startsWith "phase-")
   | _ => #[]
 
 /-! ## compare -/
@@ -253,7 +253,7 @@ def renderCompare (a : CompareArgs) : String := Id.run do
     out := out.push "" |>.push
       "_⚠️ no PR-side results (see the workflow logs)._"
   -- Per-phase drill-down: the main table above carries every constant's
-  -- high-level row; below it, each constant with `phase:<span>` fields
+  -- high-level row; below it, each constant with `phase-<span>` fields
   -- (aiur witness/commit/quotient breakdowns, zkVM coarse phases) gets its
   -- own collapsed mini-table (`phase | main | PR | Δ%`), opened as
   -- desired.
@@ -370,7 +370,7 @@ def shardMeasure (k : String) : String :=
 
 /-- Rows JSON → Bencher Metric Format. Rows with `status ≠ ok` are dropped
     whole — a rejected or OOM'd constant must never become a bencher data
-    point. Numeric fields (`phase:<span>` included) pass through as
+    point. Numeric fields (`phase-<span>` included) pass through as
     measures. Nested per-shard objects (`shard-cycles: {"0": …}`) become
     per-shard BENCHMARKS (`<name>/shard-0`) sharing the parent's measure
     slugs — multiplicity belongs in bencher's benchmark dimension, not as
@@ -499,12 +499,16 @@ def runFetchMainCmd (p : Cli.Parsed) : IO UInt32 := do
         let ms := (bench.getObjVal? "measures").toOption.bind (·.getArr?.toOption)
           |>.getD #[]
         for m in ms do
-          let mName := (m.getObjVal? "measure").toOption.bind fun x =>
-            (x.getObjVal? "name").toOption.bind (·.getStr?.toOption)
+          -- The SLUG is the source of truth: row keys are born
+          -- slug-shaped (see the registry metric lists and
+          -- `BenchCmd.slugify`), uploads attach to measures by it, and
+          -- the console-editable display name is never consulted.
+          let mSlug := (m.getObjVal? "measure").toOption.bind fun x =>
+            (x.getObjVal? "slug").toOption.bind (·.getStr?.toOption)
           let mVal := (m.getObjVal? "metric").toOption.bind fun x =>
             (x.getObjVal? "value").toOption
-          if let (some mn, some mv) := (mName, mVal) then
-            metrics := metrics.push (mn, mv)
+          if let (some ms, some mv) := (mSlug, mVal) then
+            metrics := metrics.push (ms, mv)
         if metrics.size > 1 then
           seen := seen.push name
           rows := rows.push (name, Json.mkObj metrics.toList)

docs/benchmarking.md

@@ -21,7 +21,7 @@ and one exit-code convention (Rust: `crates/bench`; Lean:
 `Ix/Benchmark/Results.lean`):
 
 ```json
-{ "<name>": { "status": "ok", "<metric>": 123, "phase:<span>": 1.5 } }
+{ "<name>": { "status": "ok", "<metric>": 123, "phase-<span>": 1.5 } }
 ```
 
 - Rows are flushed after every name, so a killed run keeps its completed rows.
@@ -100,7 +100,7 @@ With `--texray`, tools write per-phase span timings (`aiur/prove_ixvm`,
 `aiur/witness`, `stark/*`, `zisk/execute`, …) to `<json>.spans`. The
 per-constant backends run **one process per constant**, so each spawn's
 window belongs wholly to its constant: `ix bench run` folds it into the
-row as flat `phase:<span>` fields, which flow to bencher as independent
+row as flat `phase-<span>` fields, which flow to bencher as independent
 measures (witness gen, stage commits, quotient, … each get a trend line)
 and render in the PR comment as a collapsible per-constant drill-down.