From bb1080ca4724d81f9696b108fa7dda2ec1b1df1a Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 00:40:17 +0000
Subject: [PATCH 01/29] Add self-hosted CI: tests and A/B benches on PRs

Workflow runs on the self-hosted runner: a test job (release build,
cargo test with default and arena_compact+random features, docs) and a
bench job that benchmarks the PR head against its base on the same
machine.  bench_ab.sh builds both sides once, runs them in alternating
order pinned to one core, averages the rounds with bench_avg_files.py
and posts the bench_cmp.py table to the step summary and the PR.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/bench_ab.sh |  85 ++++++++++++++++++++++++++++
 .github/workflows/ci.yml    | 109 ++++++++++++++++++++++++++++++++++++
 2 files changed, 194 insertions(+)
 create mode 100755 .github/scripts/bench_ab.sh
 create mode 100644 .github/workflows/ci.yml

diff --git a/.github/scripts/bench_ab.sh b/.github/scripts/bench_ab.sh
new file mode 100755
index 00000000..bfc29627
--- /dev/null
+++ b/.github/scripts/bench_ab.sh
@@ -0,0 +1,85 @@
+#!/usr/bin/env bash
+# A/B benchmark of two commits on the same machine.
+#
+# Builds the bench binaries for BASE and HEAD once each (separate target
+# dirs), then runs them for ROUNDS rounds, alternating which side goes first
+# and pinning every run to one core.  Per-bench results are averaged over the
+# rounds with benches/bench_avg_files.py and compared with benches/bench_cmp.py.
+#
+# usage: bench_ab.sh <base-sha> <head-sha>
+#
+# env:  BENCH_ROUNDS       rounds per side                (default 3)
+#       BENCHES            space separated bench targets  (default: the set used in BENCH_BUGFIXES)
+#       BENCH_CPU          core to pin to                 (default 3)
+#       BENCH_OUT          output directory               (default ./bench-out)
+#       DIVAN_SAMPLE_COUNT sample count for benches that do not set their own (default 40)
+#       CARGO_TARGET_DIR   parent of the two per-side target dirs (default ./target)
+set -euo pipefail
+
+BASE_SHA=${1:?usage: bench_ab.sh <base-sha> <head-sha>}
+HEAD_SHA=${2:?usage: bench_ab.sh <base-sha> <head-sha>}
+ROUNDS=${BENCH_ROUNDS:-3}
+BENCHES=${BENCHES:-"shakespeare cities sparse_keys binary_keys superdense_keys act_paths zipper_head_owned product_zipper"}
+CPU=${BENCH_CPU:-3}
+OUT=$(realpath -m "${BENCH_OUT:-$PWD/bench-out}")
+TARGET=$(realpath -m "${CARGO_TARGET_DIR:-$PWD/target}")
+export DIVAN_SAMPLE_COUNT=${DIVAN_SAMPLE_COUNT:-40}
+
+repo=$PWD
+base_src=$OUT/src-base
+mkdir -p "$OUT"
+rm -f "$OUT"/*.txt "$OUT"/*.log
+
+cleanup() { git -C "$repo" worktree remove --force "$base_src" 2>/dev/null || true; }
+trap cleanup EXIT
+cleanup
+git worktree add --detach "$base_src" "$BASE_SHA" >/dev/null
+
+# build_side <side> <src-dir> : writes "<bench> <executable>" lines to $OUT/bins-<side>.txt
+build_side() {
+    local side=$1 src=$2 args=()
+    for b in $BENCHES; do args+=(--bench "$b"); done
+    echo "== building $side ($(git -C "$src" rev-parse --short HEAD)) into $TARGET/ab-$side"
+    (cd "$src" && cargo bench --no-run --message-format=json "${args[@]}" \
+        --target-dir "$TARGET/ab-$side" 2>"$OUT/build-$side.log") \
+    | python3 -c '
+import json, sys
+for line in sys.stdin:
+    m = json.loads(line)
+    if m.get("reason") == "compiler-artifact" and m.get("executable") and "bench" in m["target"]["kind"]:
+        print(m["target"]["name"], m["executable"])
+' > "$OUT/bins-$side.txt"
+    for b in $BENCHES; do
+        grep -q "^$b " "$OUT/bins-$side.txt" || { echo "no executable for bench $b on $side" >&2; exit 1; }
+    done
+}
+
+build_side base "$base_src"
+build_side head "$repo"
+
+exe_for() { awk -v n="$2" '$1 == n { print $2 }' "$OUT/bins-$1.txt"; }
+
+for ((r = 1; r <= ROUNDS; r++)); do
+    if (( r % 2 )); then order="base head"; else order="head base"; fi
+    for b in $BENCHES; do
+        for side in $order; do
+            echo "== round $r/$ROUNDS $b $side"
+            taskset -c "$CPU" "$(exe_for "$side" "$b")" --bench \
+                > "$OUT/$side-$b-r$r.txt" 2>> "$OUT/run-$side.log"
+        done
+    done
+done
+
+strip_ansi() { sed 's/\x1b\[[0-9;]*m//g'; }
+: > "$OUT/compare.txt"
+for b in $BENCHES; do
+    for side in base head; do
+        python3 "$repo/benches/bench_avg_files.py" "$OUT/$side-$b-r"*.txt -o "$OUT/$side-$b-avg.txt"
+    done
+    {
+        echo "$b  (base $(git rev-parse --short "$BASE_SHA")  head $(git rev-parse --short "$HEAD_SHA")  rounds $ROUNDS  median ns)"
+        python3 "$repo/benches/bench_cmp.py" --base "$OUT/base-$b-avg.txt" --other "$OUT/head-$b-avg.txt" | strip_ansi
+        echo
+    } >> "$OUT/compare.txt"
+done
+cat "$OUT/compare.txt"
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 00000000..31c55c95
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,109 @@
+name: CI
+
+on:
+  pull_request:
+  push:
+    branches: [master]
+  workflow_dispatch:
+    inputs:
+      base:
+        description: base ref to benchmark against
+        default: master
+      rounds:
+        description: bench rounds per side
+        default: "3"
+      benches:
+        description: space separated bench targets (empty = default set)
+        default: ""
+
+permissions:
+  contents: read
+
+# One workflow run per PR / branch; a new push cancels the one in progress.
+concurrency:
+  group: ci-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+env:
+  CARGO_TERM_COLOR: never
+  # Persistent across jobs on the runner (outside its _work dir), so builds are incremental.
+  CARGO_TARGET_DIR: /home/gh-runner/cache/target
+
+jobs:
+  test:
+    name: tests
+    runs-on: [self-hosted, linux, x64]
+    timeout-minutes: 120
+    steps:
+      - uses: actions/checkout@v4
+      - name: toolchain
+        run: |
+          rustup toolchain install stable --profile minimal
+          rustup default stable
+          rustc --version && cargo --version
+      - name: build
+        run: cargo build --release --all-targets
+      - name: unit + integration tests
+        run: cargo test --release
+      - name: tests with arena_compact + random
+        run: cargo test --release --features arena_compact,random
+      - name: doc tests + docs
+        run: cargo doc --no-deps
+
+  bench:
+    name: bench A/B vs base
+    # PRs and manual runs only; a push to master has nothing to compare against.
+    if: github.event_name == 'pull_request' || github.event_name == 'workflow_dispatch'
+    runs-on: [self-hosted, linux, x64, bench]
+    timeout-minutes: 300
+    permissions:
+      contents: read
+      pull-requests: write
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+      - name: toolchain
+        run: |
+          rustup toolchain install stable --profile minimal
+          rustup default stable
+      - name: resolve base
+        id: base
+        run: |
+          if [ "${{ github.event_name }}" = pull_request ]; then
+            sha=${{ github.event.pull_request.base.sha }}
+          else
+            sha=$(git rev-parse "origin/${{ inputs.base }}" 2>/dev/null || git rev-parse "${{ inputs.base }}")
+          fi
+          echo "sha=$sha" >> "$GITHUB_OUTPUT"
+      - name: A/B bench
+        env:
+          BENCH_ROUNDS: ${{ inputs.rounds || '3' }}
+          BENCHES: ${{ inputs.benches }}
+          BENCH_OUT: ${{ runner.temp }}/bench-out
+        run: |
+          # an empty BENCHES must fall through to the script's default set
+          [ -n "$BENCHES" ] || unset BENCHES
+          .github/scripts/bench_ab.sh "${{ steps.base.outputs.sha }}" "${{ github.sha }}"
+      - name: summary
+        if: always()
+        run: |
+          out="${{ runner.temp }}/bench-out"
+          if [ -s "$out/compare.txt" ]; then
+            { echo '```'; cat "$out/compare.txt"; echo '```'; } > "$out/compare.md"
+            cat "$out/compare.md" >> "$GITHUB_STEP_SUMMARY"
+          fi
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: bench-out
+          path: ${{ runner.temp }}/bench-out/*.txt
+          if-no-files-found: ignore
+      - name: comment on PR
+        # The token is read-only for PRs from forks, so only comment on same-repo PRs.
+        if: github.event_name == 'pull_request' && github.event.pull_request.head.repo.full_name == github.repository
+        continue-on-error: true
+        uses: marocchino/sticky-pull-request-comment@v2
+        with:
+          header: bench
+          path: ${{ runner.temp }}/bench-out/compare.md

From 7e3fa339bbe2723a4d97440e2b707d5a11e5e041 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 12:32:04 +0000
Subject: [PATCH 02/29] CI bench: pass required-features, report progress to
 the PR while running

bench_ab.sh failed on the runner with exit 101 because act_paths declares
required-features (arena_compact, serialization) and the script built
without them.  It now reads each side's Cargo.toml and passes the features
the requested benches need, and prints the cargo error into the step log
when a build fails instead of leaving it in a temp file.

The script also appends to progress.txt after every run and rewrites
compare.txt after every completed round.  The workflow runs it in the
background and, once a minute, posts progress plus the compare table of
the rounds finished so far to one PR comment via pr_comment.py (stdlib
only).  The comment is found by a marker so re-runs and later pushes
reuse it, and its id is cached per run so the periodic updates skip the
lookup.  This replaces the sticky-comment action.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/bench_ab.sh   | 75 ++++++++++++++++++++++++++---------
 .github/scripts/pr_comment.py | 71 +++++++++++++++++++++++++++++++++
 .github/workflows/ci.yml      | 20 +++++-----
 3 files changed, 137 insertions(+), 29 deletions(-)
 create mode 100755 .github/scripts/pr_comment.py

diff --git a/.github/scripts/bench_ab.sh b/.github/scripts/bench_ab.sh
index bfc29627..95940a19 100755
--- a/.github/scripts/bench_ab.sh
+++ b/.github/scripts/bench_ab.sh
@@ -14,6 +14,10 @@
 #       BENCH_OUT          output directory               (default ./bench-out)
 #       DIVAN_SAMPLE_COUNT sample count for benches that do not set their own (default 40)
 #       CARGO_TARGET_DIR   parent of the two per-side target dirs (default ./target)
+#
+# Progress is appended to $BENCH_OUT/progress.txt after every run, and
+# $BENCH_OUT/compare.txt is rewritten after every completed round, so a watcher
+# (see pr_comment.sh) can show partial results while the script runs.
 set -euo pipefail
 
 BASE_SHA=${1:?usage: bench_ab.sh <base-sha> <head-sha>}
@@ -28,33 +32,74 @@ export DIVAN_SAMPLE_COUNT=${DIVAN_SAMPLE_COUNT:-40}
 repo=$PWD
 base_src=$OUT/src-base
 mkdir -p "$OUT"
-rm -f "$OUT"/*.txt "$OUT"/*.log
+rm -f "$OUT"/*.txt "$OUT"/*.log "$OUT"/*.json
+
+progress() { echo "$(date -u +%H:%M:%S) $*" >> "$OUT/progress.txt"; }
+strip_ansi() { sed 's/\x1b\[[0-9;]*m//g'; }
+
+# compare_rounds <n> : average the rounds finished so far per bench and side, then compare; writes $OUT/compare.txt
+compare_rounds() {
+    local tmp=$OUT/compare.tmp
+    : > "$tmp"
+    for b in $BENCHES; do
+        for side in base head; do
+            python3 "$repo/benches/bench_avg_files.py" "$OUT/$side-$b-r"*.txt -o "$OUT/$side-$b-avg.txt"
+        done
+        {
+            echo "$b  (base $(git rev-parse --short "$BASE_SHA")  head $(git rev-parse --short "$HEAD_SHA")  rounds $1  median ns)"
+            python3 "$repo/benches/bench_cmp.py" --base "$OUT/base-$b-avg.txt" --other "$OUT/head-$b-avg.txt" | strip_ansi
+            echo
+        } >> "$tmp"
+    done
+    mv "$tmp" "$OUT/compare.txt"
+}
 
 cleanup() { git -C "$repo" worktree remove --force "$base_src" 2>/dev/null || true; }
 trap cleanup EXIT
 cleanup
 git worktree add --detach "$base_src" "$BASE_SHA" >/dev/null
+progress "plan: $ROUNDS round(s) x base/head x [$BENCHES], core $CPU"
 
 # build_side <side> <src-dir> : writes "<bench> <executable>" lines to $OUT/bins-<side>.txt
 build_side() {
-    local side=$1 src=$2 args=()
+    local side=$1 src=$2 args=() feats
     for b in $BENCHES; do args+=(--bench "$b"); done
-    echo "== building $side ($(git -C "$src" rev-parse --short HEAD)) into $TARGET/ab-$side"
-    (cd "$src" && cargo bench --no-run --message-format=json "${args[@]}" \
-        --target-dir "$TARGET/ab-$side" 2>"$OUT/build-$side.log") \
-    | python3 -c '
+    # features the requested benches declare via required-features (only those the side's Cargo.toml has)
+    feats=$(cd "$src" && python3 - "$BENCHES" <<'PY'
+import sys, tomllib
+t = tomllib.load(open('Cargo.toml', 'rb'))
+want = set(sys.argv[1].split())
+have = set(t.get('features', {}))
+need = set()
+for b in t.get('bench', []):
+    if b.get('name') in want:
+        need |= set(b.get('required-features', []))
+print(','.join(sorted(need & have)))
+PY
+)
+    [[ -n $feats ]] && args+=(--features "$feats")
+    echo "== building $side ($(git -C "$src" rev-parse --short HEAD)) into $TARGET/ab-$side${feats:+ with features $feats}"
+    if ! (cd "$src" && cargo bench --no-run --message-format=json "${args[@]}" --target-dir "$TARGET/ab-$side" \
+            > "$OUT/build-$side.json" 2> "$OUT/build-$side.log"); then
+        echo "build of $side failed; tail of $OUT/build-$side.log:" >&2
+        tail -30 "$OUT/build-$side.log" >&2
+        exit 1
+    fi
+    python3 -c '
 import json, sys
 for line in sys.stdin:
     m = json.loads(line)
     if m.get("reason") == "compiler-artifact" and m.get("executable") and "bench" in m["target"]["kind"]:
         print(m["target"]["name"], m["executable"])
-' > "$OUT/bins-$side.txt"
+' < "$OUT/build-$side.json" > "$OUT/bins-$side.txt"
     for b in $BENCHES; do
         grep -q "^$b " "$OUT/bins-$side.txt" || { echo "no executable for bench $b on $side" >&2; exit 1; }
     done
 }
 
+progress "building base $(git rev-parse --short "$BASE_SHA")"
 build_side base "$base_src"
+progress "building head $(git rev-parse --short "$HEAD_SHA")"
 build_side head "$repo"
 
 exe_for() { awk -v n="$2" '$1 == n { print $2 }' "$OUT/bins-$1.txt"; }
@@ -64,22 +109,14 @@ for ((r = 1; r <= ROUNDS; r++)); do
     for b in $BENCHES; do
         for side in $order; do
             echo "== round $r/$ROUNDS $b $side"
+            t0=$SECONDS
             taskset -c "$CPU" "$(exe_for "$side" "$b")" --bench \
                 > "$OUT/$side-$b-r$r.txt" 2>> "$OUT/run-$side.log"
+            progress "round $r/$ROUNDS $b $side $((SECONDS - t0))s"
         done
     done
+    compare_rounds "$r"
+    progress "round $r/$ROUNDS done, compare.txt refreshed"
 done
 
-strip_ansi() { sed 's/\x1b\[[0-9;]*m//g'; }
-: > "$OUT/compare.txt"
-for b in $BENCHES; do
-    for side in base head; do
-        python3 "$repo/benches/bench_avg_files.py" "$OUT/$side-$b-r"*.txt -o "$OUT/$side-$b-avg.txt"
-    done
-    {
-        echo "$b  (base $(git rev-parse --short "$BASE_SHA")  head $(git rev-parse --short "$HEAD_SHA")  rounds $ROUNDS  median ns)"
-        python3 "$repo/benches/bench_cmp.py" --base "$OUT/base-$b-avg.txt" --other "$OUT/head-$b-avg.txt" | strip_ansi
-        echo
-    } >> "$OUT/compare.txt"
-done
 cat "$OUT/compare.txt"
diff --git a/.github/scripts/pr_comment.py b/.github/scripts/pr_comment.py
new file mode 100755
index 00000000..d26d4a7d
--- /dev/null
+++ b/.github/scripts/pr_comment.py
@@ -0,0 +1,71 @@
+#!/usr/bin/env python3
+"""Create or update the single bench comment on a pull request.
+
+One comment per pull request, edited in place.  The first call of a run finds
+the PR's existing bench comment by the hidden marker on its first line (so a
+re-run or a new push reuses it) or creates it, and records the id in
+$BENCH_OUT/comment_id; later calls in the same run go straight to that id.
+Standard library only.
+
+usage: pr_comment.py <pr-number> <status text>
+env:   GITHUB_TOKEN GITHUB_REPOSITORY   (provided by Actions)
+       BENCH_OUT                        dir holding progress.txt / compare.txt from bench_ab.sh
+       GITHUB_SERVER_URL GITHUB_RUN_ID  for the run link, optional
+"""
+import json, os, sys, time, urllib.request
+from pathlib import Path
+
+MARKER = '<!-- pathmap-bench-ab -->'
+LIMIT = 65536            # GitHub's comment body cap
+PROGRESS_LINES = 40
+
+pr, status = sys.argv[1], sys.argv[2] if len(sys.argv) > 2 else ''
+out = Path(os.environ['BENCH_OUT'])
+repo = os.environ['GITHUB_REPOSITORY']
+api = f'https://api.github.com/repos/{repo}'
+headers = {'Authorization': f"Bearer {os.environ['GITHUB_TOKEN']}",
+           'Accept': 'application/vnd.github+json', 'Content-Type': 'application/json'}
+run_url = f"{os.environ.get('GITHUB_SERVER_URL', 'https://github.com')}/{repo}/actions/runs/{os.environ.get('GITHUB_RUN_ID', '')}"
+
+
+def call(method, url, data=None):
+    req = urllib.request.Request(url, method=method, headers=headers,
+                                 data=json.dumps(data).encode() if data is not None else None)
+    with urllib.request.urlopen(req, timeout=30) as r:
+        return json.load(r)
+
+
+def read(name):
+    p = out / name
+    return p.read_text() if p.is_file() else ''
+
+
+parts = [MARKER, f'### Bench A/B vs base: {status}', '',
+         f"[run log]({run_url}) · updated {time.strftime('%Y-%m-%d %H:%M:%S', time.gmtime())} UTC"]
+progress = read('progress.txt').splitlines()
+if progress:
+    parts += ['', f'<details><summary>progress (last {PROGRESS_LINES} lines)</summary>', '', '```',
+              *progress[-PROGRESS_LINES:], '```', '</details>']
+compare = read('compare.txt')
+if compare:
+    head = '\n'.join(parts)
+    room = LIMIT - len(head) - 200
+    if len(compare) > room:
+        compare = compare[:room] + '\n… truncated; the full table is in the bench-out artifact\n'
+    parts += ['', '```', compare.rstrip(), '```']
+body = '\n'.join(parts)
+
+id_file = out / 'comment_id'
+if id_file.is_file():
+    cid = id_file.read_text().strip()
+    how = 'updated'
+else:
+    found = [c['id'] for c in call('GET', f'{api}/issues/{pr}/comments?per_page=100') if c['body'].startswith(MARKER)]
+    cid = found[0] if found else None
+    how = 'reused' if found else 'created'
+if cid is None:
+    cid = call('POST', f'{api}/issues/{pr}/comments', {'body': body})['id']
+else:
+    call('PATCH', f'{api}/issues/comments/{cid}', {'body': body})
+id_file.write_text(str(cid))
+print(f'comment {cid} {how}: {len(body)} chars')
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 31c55c95..084aa170 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -58,7 +58,7 @@ jobs:
     timeout-minutes: 300
     permissions:
       contents: read
-      pull-requests: write
+      pull-requests: write   # for the progress comment; read-only on fork PRs, where commenting is skipped
     steps:
       - uses: actions/checkout@v4
         with:
@@ -81,10 +81,18 @@ jobs:
           BENCH_ROUNDS: ${{ inputs.rounds || '3' }}
           BENCHES: ${{ inputs.benches }}
           BENCH_OUT: ${{ runner.temp }}/bench-out
+          GITHUB_TOKEN: ${{ github.token }}
+          # Only same-repo PRs get a writable token; on fork PRs the comment calls fail and are ignored.
+          PR: ${{ github.event.pull_request.number }}
         run: |
           # an empty BENCHES must fall through to the script's default set
           [ -n "$BENCHES" ] || unset BENCHES
-          .github/scripts/bench_ab.sh "${{ steps.base.outputs.sha }}" "${{ github.sha }}"
+          mkdir -p "$BENCH_OUT"
+          comment() { [ -z "$PR" ] || python3 .github/scripts/pr_comment.py "$PR" "$1" || true; }
+          .github/scripts/bench_ab.sh "${{ steps.base.outputs.sha }}" "${{ github.sha }}" & bench=$!
+          # refresh the PR comment once a minute while the bench runs: progress + the compare table of finished rounds
+          while kill -0 $bench 2>/dev/null; do comment "running"; sleep 60; done
+          if wait $bench; then comment "done"; else comment "failed, see run log"; exit 1; fi
       - name: summary
         if: always()
         run: |
@@ -99,11 +107,3 @@ jobs:
           name: bench-out
           path: ${{ runner.temp }}/bench-out/*.txt
           if-no-files-found: ignore
-      - name: comment on PR
-        # The token is read-only for PRs from forks, so only comment on same-repo PRs.
-        if: github.event_name == 'pull_request' && github.event.pull_request.head.repo.full_name == github.repository
-        continue-on-error: true
-        uses: marocchino/sticky-pull-request-comment@v2
-        with:
-          header: bench
-          path: ${{ runner.temp }}/bench-out/compare.md

From dd8b7997e34a289c54115301abde1006007c0f21 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 12:38:28 +0000
Subject: [PATCH 03/29] CI bench: comment once at start with the job link, once
 at the end with results

The per-minute progress updates duplicated the job log.  The comment now
carries a link to the specific job (looked up from the run's jobs as the
one in progress on this runner, falling back to the run link) and, when
the bench finishes, the compare table.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/pr_comment.py | 44 +++++++++++++++++++++++------------
 .github/workflows/ci.yml      | 10 ++++----
 2 files changed, 35 insertions(+), 19 deletions(-)

diff --git a/.github/scripts/pr_comment.py b/.github/scripts/pr_comment.py
index d26d4a7d..2f7024c7 100755
--- a/.github/scripts/pr_comment.py
+++ b/.github/scripts/pr_comment.py
@@ -1,23 +1,23 @@
 #!/usr/bin/env python3
 """Create or update the single bench comment on a pull request.
 
-One comment per pull request, edited in place.  The first call of a run finds
-the PR's existing bench comment by the hidden marker on its first line (so a
-re-run or a new push reuses it) or creates it, and records the id in
-$BENCH_OUT/comment_id; later calls in the same run go straight to that id.
-Standard library only.
+One comment per pull request, edited in place: a status line, a link to the
+job that produced it, and bench_ab.sh's compare table once it exists.  The
+first call of a run finds the PR's existing bench comment by the hidden marker
+on its first line (so a re-run or a new push reuses it) or creates it, and
+records the id in $BENCH_OUT/comment_id; later calls in the same run go
+straight to that id.  Standard library only.
 
 usage: pr_comment.py <pr-number> <status text>
-env:   GITHUB_TOKEN GITHUB_REPOSITORY   (provided by Actions)
-       BENCH_OUT                        dir holding progress.txt / compare.txt from bench_ab.sh
-       GITHUB_SERVER_URL GITHUB_RUN_ID  for the run link, optional
+env:   GITHUB_TOKEN GITHUB_REPOSITORY GITHUB_RUN_ID RUNNER_NAME   (provided by Actions)
+       BENCH_OUT                        dir holding compare.txt from bench_ab.sh
+       GITHUB_SERVER_URL                optional
 """
 import json, os, sys, time, urllib.request
 from pathlib import Path
 
 MARKER = '<!-- pathmap-bench-ab -->'
 LIMIT = 65536            # GitHub's comment body cap
-PROGRESS_LINES = 40
 
 pr, status = sys.argv[1], sys.argv[2] if len(sys.argv) > 2 else ''
 out = Path(os.environ['BENCH_OUT'])
@@ -25,7 +25,8 @@
 api = f'https://api.github.com/repos/{repo}'
 headers = {'Authorization': f"Bearer {os.environ['GITHUB_TOKEN']}",
            'Accept': 'application/vnd.github+json', 'Content-Type': 'application/json'}
-run_url = f"{os.environ.get('GITHUB_SERVER_URL', 'https://github.com')}/{repo}/actions/runs/{os.environ.get('GITHUB_RUN_ID', '')}"
+run_id = os.environ.get('GITHUB_RUN_ID', '')
+run_url = f"{os.environ.get('GITHUB_SERVER_URL', 'https://github.com')}/{repo}/actions/runs/{run_id}"
 
 
 def call(method, url, data=None):
@@ -40,12 +41,25 @@ def read(name):
     return p.read_text() if p.is_file() else ''
 
 
+def job_url():
+    """Link to this job's log: the job in progress on this runner within the run.  Cached per run."""
+    cache = out / 'job_url'
+    if cache.is_file():
+        return cache.read_text().strip()
+    url = run_url
+    try:
+        jobs = call('GET', f'{api}/actions/runs/{run_id}/jobs?per_page=100')['jobs']
+        mine = [j for j in jobs if j.get('runner_name') == os.environ.get('RUNNER_NAME') and j.get('status') == 'in_progress']
+        if mine:
+            url = mine[0]['html_url']
+            cache.write_text(url)
+    except Exception as e:                       # the run link is a fine fallback
+        print(f'job lookup failed, using run link: {e}', file=sys.stderr)
+    return url
+
+
 parts = [MARKER, f'### Bench A/B vs base: {status}', '',
-         f"[run log]({run_url}) · updated {time.strftime('%Y-%m-%d %H:%M:%S', time.gmtime())} UTC"]
-progress = read('progress.txt').splitlines()
-if progress:
-    parts += ['', f'<details><summary>progress (last {PROGRESS_LINES} lines)</summary>', '', '```',
-              *progress[-PROGRESS_LINES:], '```', '</details>']
+         f"[job log]({job_url()}) · {time.strftime('%Y-%m-%d %H:%M:%S', time.gmtime())} UTC"]
 compare = read('compare.txt')
 if compare:
     head = '\n'.join(parts)
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 084aa170..ef353406 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -89,10 +89,12 @@ jobs:
           [ -n "$BENCHES" ] || unset BENCHES
           mkdir -p "$BENCH_OUT"
           comment() { [ -z "$PR" ] || python3 .github/scripts/pr_comment.py "$PR" "$1" || true; }
-          .github/scripts/bench_ab.sh "${{ steps.base.outputs.sha }}" "${{ github.sha }}" & bench=$!
-          # refresh the PR comment once a minute while the bench runs: progress + the compare table of finished rounds
-          while kill -0 $bench 2>/dev/null; do comment "running"; sleep 60; done
-          if wait $bench; then comment "done"; else comment "failed, see run log"; exit 1; fi
+          comment "running"
+          if .github/scripts/bench_ab.sh "${{ steps.base.outputs.sha }}" "${{ github.sha }}"; then
+            comment "done"
+          else
+            comment "failed, see the job log"; exit 1
+          fi
       - name: summary
         if: always()
         run: |

From ed83cc00a0e42798b938a61b7a3e48fefc29fec7 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 12:49:44 +0000
Subject: [PATCH 04/29] CI bench: print each bench's compare table as soon as
 both sides have run

The table for a bench is averaged over the rounds finished so far and
saved as cmp-<bench>.txt; compare.txt is the concatenation, rewritten at
the end of every round.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/bench_ab.sh | 41 ++++++++++++++++++++++---------------
 1 file changed, 25 insertions(+), 16 deletions(-)

diff --git a/.github/scripts/bench_ab.sh b/.github/scripts/bench_ab.sh
index 95940a19..559a7605 100755
--- a/.github/scripts/bench_ab.sh
+++ b/.github/scripts/bench_ab.sh
@@ -15,9 +15,11 @@
 #       DIVAN_SAMPLE_COUNT sample count for benches that do not set their own (default 40)
 #       CARGO_TARGET_DIR   parent of the two per-side target dirs (default ./target)
 #
-# Progress is appended to $BENCH_OUT/progress.txt after every run, and
-# $BENCH_OUT/compare.txt is rewritten after every completed round, so a watcher
-# (see pr_comment.sh) can show partial results while the script runs.
+# As soon as both sides of a bench have run in a round, its compare table
+# (averaged over the rounds finished so far) is printed and saved as
+# $BENCH_OUT/cmp-<bench>.txt; $BENCH_OUT/compare.txt, the concatenation, is
+# rewritten after every completed round.  Progress lines go to
+# $BENCH_OUT/progress.txt.  pr_comment.py posts compare.txt to the PR.
 set -euo pipefail
 
 BASE_SHA=${1:?usage: bench_ab.sh <base-sha> <head-sha>}
@@ -37,20 +39,26 @@ rm -f "$OUT"/*.txt "$OUT"/*.log "$OUT"/*.json
 progress() { echo "$(date -u +%H:%M:%S) $*" >> "$OUT/progress.txt"; }
 strip_ansi() { sed 's/\x1b\[[0-9;]*m//g'; }
 
-# compare_rounds <n> : average the rounds finished so far per bench and side, then compare; writes $OUT/compare.txt
+# compare_bench <bench> <rounds-so-far> : average each side over the rounds run so far and
+# compare; writes $OUT/cmp-<bench>.txt and prints it
+compare_bench() {
+    local b=$1
+    for side in base head; do
+        python3 "$repo/benches/bench_avg_files.py" "$OUT/$side-$b-r"*.txt -o "$OUT/$side-$b-avg.txt"
+    done
+    {
+        echo "$b  (base $(git rev-parse --short "$BASE_SHA")  head $(git rev-parse --short "$HEAD_SHA")  rounds $2  median ns)"
+        python3 "$repo/benches/bench_cmp.py" --base "$OUT/base-$b-avg.txt" --other "$OUT/head-$b-avg.txt" | strip_ansi
+        echo
+    } > "$OUT/cmp-$b.txt"
+    cat "$OUT/cmp-$b.txt"
+}
+
+# compare_rounds : concatenate the per-bench tables into $OUT/compare.txt
 compare_rounds() {
     local tmp=$OUT/compare.tmp
     : > "$tmp"
-    for b in $BENCHES; do
-        for side in base head; do
-            python3 "$repo/benches/bench_avg_files.py" "$OUT/$side-$b-r"*.txt -o "$OUT/$side-$b-avg.txt"
-        done
-        {
-            echo "$b  (base $(git rev-parse --short "$BASE_SHA")  head $(git rev-parse --short "$HEAD_SHA")  rounds $1  median ns)"
-            python3 "$repo/benches/bench_cmp.py" --base "$OUT/base-$b-avg.txt" --other "$OUT/head-$b-avg.txt" | strip_ansi
-            echo
-        } >> "$tmp"
-    done
+    for b in $BENCHES; do cat "$OUT/cmp-$b.txt" >> "$tmp"; done
     mv "$tmp" "$OUT/compare.txt"
 }
 
@@ -114,9 +122,10 @@ for ((r = 1; r <= ROUNDS; r++)); do
                 > "$OUT/$side-$b-r$r.txt" 2>> "$OUT/run-$side.log"
             progress "round $r/$ROUNDS $b $side $((SECONDS - t0))s"
         done
+        compare_bench "$b" "$r"
     done
-    compare_rounds "$r"
+    compare_rounds
     progress "round $r/$ROUNDS done, compare.txt refreshed"
 done
 
-cat "$OUT/compare.txt"
+echo "== final compare over $ROUNDS round(s): $OUT/compare.txt"

From 945e87d10f4be301a45d93e098cfd0ef54b7891b Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 12:58:50 +0000
Subject: [PATCH 05/29] CI: run the bench job after the test job passes

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/workflows/ci.yml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index ef353406..b1b42326 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -52,7 +52,9 @@ jobs:
 
   bench:
     name: bench A/B vs base
-    # PRs and manual runs only; a push to master has nothing to compare against.
+    # Runs after the tests pass (skipped when they fail), on PRs and manual runs only;
+    # a push to master has nothing to compare against.
+    needs: test
     if: github.event_name == 'pull_request' || github.event_name == 'workflow_dispatch'
     runs-on: [self-hosted, linux, x64, bench]
     timeout-minutes: 300

From 8d9c35582a7cea817bee0425759644bda6667f99 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 13:08:28 +0000
Subject: [PATCH 06/29] CI: differential fuzz job as a regression gate against
 the base commit

The crate on master has 44 new divergences from the Lean model on the
seed-7 corpus, so "zero divergences" cannot be the bar.  fuzz_ab.sh runs
head and base on identical inputs (model vs crate, 20000; ACT read side,
5000) and fails only when head diverges on an input base did not.  Both
sides use head's differential/ and lean/, so only the crate under test
differs; if base cannot be built with head's harness its own is tried,
and with no baseline at all the job reports that and does not gate.

Two enabling fixes: the differential harness did not compile since the
ZipperValues/ZipperValuesAt split (ReadSource now requires
ZipperValuesAt<u64>), and differential.py accepts PATHMAP_TRACE /
PATHMAP_ACT_TRACE to find binaries built into another target dir.

The fuzz job runs after the tests, on PRs and manual runs.  Lean is
installed through elan for the runner user; lake's build dir is kept in
the runner's cache since checkout wipes ignored files.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/fuzz_ab.sh  | 151 ++++++++++++++++++++++++++++++++++++
 .github/workflows/ci.yml    |  53 +++++++++++++
 differential/src/harness.rs |   2 +-
 lean/differential.py        |   8 +-
 4 files changed, 210 insertions(+), 4 deletions(-)
 create mode 100755 .github/scripts/fuzz_ab.sh

diff --git a/.github/scripts/fuzz_ab.sh b/.github/scripts/fuzz_ab.sh
new file mode 100755
index 00000000..37799723
--- /dev/null
+++ b/.github/scripts/fuzz_ab.sh
@@ -0,0 +1,151 @@
+#!/usr/bin/env bash
+# Differential fuzz of two commits against the Lean model, as a regression gate.
+#
+# The crate at HEAD has known divergences from the model, so "zero divergences"
+# cannot be the bar.  Instead both commits are run on identical inputs and the
+# job fails only when HEAD diverges on an input BASE did not.  The harness
+# (differential/) and the model (lean/) are taken from HEAD for both sides, so
+# the only thing that differs is the crate under test in src/.  If BASE cannot
+# be built with HEAD's harness, BASE's own harness is tried; if that fails too
+# there is no baseline, which is reported loudly and does not fail the job.
+#
+# usage: fuzz_ab.sh <base-sha> <head-sha>
+#
+# env:  FUZZ_INPUTS        random programs, model vs crate        (default 20000)
+#       FUZZ_ACT_INPUTS    random programs with the ACT read side (default 5000; 0 skips)
+#       FUZZ_SEED          (default 7)
+#       FUZZ_JOBS          worker processes                        (default 16)
+#       FUZZ_OUT           output dir                              (default ./fuzz-out)
+#       CARGO_TARGET_DIR   parent of the per-side target dirs      (default ./target)
+#       LAKE_CACHE         optional dir to keep lean's .lake build dirs across runs
+set -euo pipefail
+
+BASE_SHA=${1:?usage: fuzz_ab.sh <base-sha> <head-sha>}
+HEAD_SHA=${2:?usage: fuzz_ab.sh <base-sha> <head-sha>}
+INPUTS=${FUZZ_INPUTS:-20000}
+ACT_INPUTS=${FUZZ_ACT_INPUTS:-5000}
+SEED=${FUZZ_SEED:-7}
+JOBS=${FUZZ_JOBS:-16}
+OUT=$(realpath -m "${FUZZ_OUT:-$PWD/fuzz-out}")
+TARGET=$(realpath -m "${CARGO_TARGET_DIR:-$PWD/target}")
+LAKE_CACHE=${LAKE_CACHE:-}
+
+repo=$PWD
+base_src=$OUT/src-base
+mkdir -p "$OUT"
+rm -f "$OUT"/*.txt "$OUT"/*.log "$OUT"/*.md
+
+cleanup() { git -C "$repo" worktree remove --force "$base_src" 2>/dev/null || true; }
+trap cleanup EXIT
+cleanup
+git worktree add --detach "$base_src" "$BASE_SHA" >/dev/null
+
+# build_side <side> <src-dir> : lake build + cargo build into this side's target dir
+build_side() {
+    local side=$1 src=$2
+    if [[ -n $LAKE_CACHE ]]; then
+        mkdir -p "$LAKE_CACHE/$side"
+        rm -rf "$src/lean/.lake"; ln -sfn "$LAKE_CACHE/$side" "$src/lean/.lake"
+    fi
+    (cd "$src/lean" && lake build) > "$OUT/lake-$side.log" 2>&1 || { tail -30 "$OUT/lake-$side.log" >&2; return 1; }
+    (cd "$src" && cargo build --release -p differential --target-dir "$TARGET/fuzz-$side") > "$OUT/build-$side.log" 2>&1 \
+        || { tail -30 "$OUT/build-$side.log" >&2; return 1; }
+}
+
+echo "== building head ($(git rev-parse --short "$HEAD_SHA"))"
+build_side head "$repo"
+
+echo "== building base ($(git rev-parse --short "$BASE_SHA")) with head's differential/ and lean/"
+rm -rf "$base_src/differential" "$base_src/lean"
+cp -r "$repo/differential" "$base_src/differential"
+cp -r "$repo/lean" "$base_src/lean" && rm -rf "$base_src/lean/.lake"   # head's model and harness, not its build dir
+baseline=head-harness
+if ! build_side base "$base_src"; then
+    echo "== head's harness does not build against base; trying base's own"
+    git -C "$base_src" checkout -- differential lean
+    git -C "$base_src" clean -fdq -- differential lean
+    if build_side base "$base_src"; then baseline=base-harness; else baseline=none; fi
+fi
+
+# run_side <side> <src-dir> <label> <inputs> [--act]
+run_side() {
+    local side=$1 src=$2 label=$3 n=$4; shift 4
+    export TMPDIR=$OUT/fails-$side-$label
+    export PATHMAP_TRACE=$TARGET/fuzz-$side/release/pathmap_trace PATHMAP_ACT_TRACE=$TARGET/fuzz-$side/release/act_trace
+    mkdir -p "$TMPDIR"
+    echo "== fuzz $label $side: $n inputs, seed $SEED"
+    (cd "$src" && ./lean/differential.py --random "$n" --seed "$SEED" --maxlen 300 --max-fails 0 -j "$JOBS" "$@") \
+        > "$OUT/fuzz-$label-$side.txt" 2>&1 || true
+    grep -E "inputs agree|child restart" "$OUT/fuzz-$label-$side.txt" || { tail -5 "$OUT/fuzz-$label-$side.txt"; }
+}
+
+modes=("crate:$INPUTS:")
+(( ACT_INPUTS > 0 )) && modes+=("act:$ACT_INPUTS:--act")
+for m in "${modes[@]}"; do
+    IFS=: read -r label n flag <<< "$m"
+    run_side head "$repo" "$label" "$n" $flag
+    [[ $baseline != none ]] && run_side base "$base_src" "$label" "$n" $flag
+done
+
+python3 - "$OUT" "$baseline" "$(git rev-parse --short "$BASE_SHA")" "$(git rev-parse --short "$HEAD_SHA")" "$SEED" "${modes[@]}" <<'PY'
+import re, sys
+from pathlib import Path
+out, baseline, base, head, seed, *modes = sys.argv[1:]
+out = Path(out)
+fail_re = re.compile(r'^FAIL (\S+) \[saved [^\]]*\]: (.*)$')
+sum_re = re.compile(r'^(\d+)/(\d+) inputs agree \((\d+) hit known bugs, (\d+) new divergences\)')
+
+def parse(p):
+    fails, summary = {}, None
+    if not p.is_file():
+        return fails, summary
+    for line in p.read_text().splitlines():
+        m = fail_re.match(line)
+        if m:
+            fails[m.group(1)] = m.group(2)
+        m = sum_re.match(line)
+        if m:
+            summary = tuple(map(int, m.groups()))
+    return fails, summary
+
+lines = [f'# Differential fuzz: head {head} vs base {base}', '']
+if baseline == 'none':
+    lines += ['**No baseline**: base could not be built with either harness, so only head was run and nothing is gated.', '']
+elif baseline == 'base-harness':
+    lines += ["Base was built with its own harness and model (head's did not build against it), so harness changes may show up as differences.", '']
+bad = 0
+for m in modes:
+    label, n, _ = m.split(':')
+    hf, hs = parse(out / f'fuzz-{label}-head.txt')
+    bf, bs = parse(out / f'fuzz-{label}-base.txt')
+    lines += [f'## {label}: {n} inputs, seed {seed}', '',
+              '| side | agree | known | new divergences |', '|---|---:|---:|---:|']
+    for side, s in (('head', hs), ('base', bs)):
+        if s:
+            lines.append(f'| {side} | {s[0]}/{s[1]} | {s[2]} | {s[3]} |')
+        elif side == 'head' or baseline != 'none':
+            lines.append(f'| {side} | run did not finish, see fuzz-{label}-{side}.txt | | |')
+            bad += 1
+    if baseline != 'none' and hs and bs:
+        new = sorted(set(hf) - set(bf))
+        fixed = sorted(set(bf) - set(hf))
+        lines += ['', f'{len(new)} input(s) diverge on head but not on base; {len(fixed)} diverge on base but not on head.']
+        if new:
+            bad += len(new)
+            lines += ['', '### Newly diverging inputs (head only)', '']
+            for name in new[:50]:
+                lines.append(f'- `{name}`: {hf[name][:200]}')
+            if len(new) > 50:
+                lines.append(f'- … and {len(new) - 50} more, see fuzz-{label}-head.txt')
+        if fixed:
+            lines += ['', f'<details><summary>{len(fixed)} input(s) fixed on head</summary>', '']
+            lines += [f'- `{name}`' for name in fixed[:50]]
+            lines += ['', '</details>']
+    lines.append('')
+verdict = 'FAIL: new divergences relative to base, or a run did not finish' if bad else 'OK: no new divergences relative to base'
+lines.insert(2, f'**{verdict}**')
+lines.insert(3, '')
+(out / 'summary.md').write_text('\n'.join(lines) + '\n')
+print('\n'.join(lines))
+sys.exit(1 if bad else 0)
+PY
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b1b42326..b0d5c647 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -12,6 +12,9 @@ on:
       rounds:
         description: bench rounds per side
         default: "3"
+      fuzz_inputs:
+        description: random programs for the differential fuzzer
+        default: "20000"
       benches:
         description: space separated bench targets (empty = default set)
         default: ""
@@ -111,3 +114,53 @@ jobs:
           name: bench-out
           path: ${{ runner.temp }}/bench-out/*.txt
           if-no-files-found: ignore
+
+  fuzz:
+    name: differential fuzz vs Lean model
+    # Regression gate: head and base run on identical inputs, and the job fails only when
+    # head diverges from the model on an input base did not (master has known divergences).
+    needs: test
+    if: github.event_name == 'pull_request' || github.event_name == 'workflow_dispatch'
+    runs-on: [self-hosted, linux, x64]
+    timeout-minutes: 90
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+      - name: toolchains
+        run: |
+          rustup toolchain install stable --profile minimal
+          rustup default stable
+          # elan reads lean/lean-toolchain and fetches the pinned Lean on first use
+          [ -x "$HOME/.elan/bin/elan" ] || curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none --no-modify-path
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: resolve base
+        id: base
+        run: |
+          if [ "${{ github.event_name }}" = pull_request ]; then
+            sha=${{ github.event.pull_request.base.sha }}
+          else
+            sha=$(git rev-parse "origin/${{ inputs.base }}" 2>/dev/null || git rev-parse "${{ inputs.base }}")
+          fi
+          echo "sha=$sha" >> "$GITHUB_OUTPUT"
+      - name: fuzz head and base
+        env:
+          FUZZ_INPUTS: ${{ inputs.fuzz_inputs || '20000' }}
+          FUZZ_OUT: ${{ runner.temp }}/fuzz-out
+          LAKE_CACHE: /home/gh-runner/cache/lean-lake   # checkout wipes ignored files such as lean/.lake
+        run: |
+          .github/scripts/fuzz_ab.sh "${{ steps.base.outputs.sha }}" "${{ github.sha }}"
+      - name: summary
+        if: always()
+        run: |
+          f="${{ runner.temp }}/fuzz-out/summary.md"
+          [ -s "$f" ] && cat "$f" >> "$GITHUB_STEP_SUMMARY" || true
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: fuzz-out
+          path: |
+            ${{ runner.temp }}/fuzz-out/*.txt
+            ${{ runner.temp }}/fuzz-out/*.md
+            ${{ runner.temp }}/fuzz-out/fails-*
+          if-no-files-found: ignore
diff --git a/differential/src/harness.rs b/differential/src/harness.rs
index e0e47ca6..bb168798 100644
--- a/differential/src/harness.rs
+++ b/differential/src/harness.rs
@@ -175,7 +175,7 @@ pub fn dump<Z: ZipperMoving + ZipperPath + ZipperValues<u64>>(z: &mut Z) -> Stri
 /// Keeping this behind a trait means there is still exactly one operation table,
 /// so the two front ends cannot drift apart.
 pub trait ReadSource:
-    Zipper + ZipperMoving + ZipperPath + ZipperValues<u64> + ZipperAbsolutePath + ZipperIteration
+    Zipper + ZipperMoving + ZipperPath + ZipperValues<u64> + ZipperValuesAt<u64> + ZipperAbsolutePath + ZipperIteration
 {
     /// Depth-first dump of everything below the focus (`fork_read_zipper` + walk).
     fn dump_fork(&self) -> String;
diff --git a/lean/differential.py b/lean/differential.py
index 3f66934a..a7129a72 100755
--- a/lean/differential.py
+++ b/lean/differential.py
@@ -31,11 +31,13 @@
 
 ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
 ORACLE = os.path.join(ROOT, "lean", ".lake", "build", "bin", "pathmap-oracle")
-TRACE_CANDIDATES = [
+# PATHMAP_TRACE / PATHMAP_ACT_TRACE override the search, for builds that live
+# in another target dir (CI builds two commits side by side).
+TRACE_CANDIDATES = [os.environ.get("PATHMAP_TRACE", "")] + [
     os.path.join(ROOT, "target", "release", "pathmap_trace"),
     os.path.join(ROOT, "target", "debug", "pathmap_trace"),
 ]
-ACT_CANDIDATES = [
+ACT_CANDIDATES = [os.environ.get("PATHMAP_ACT_TRACE", "")] + [
     os.path.join(ROOT, "target", "release", "act_trace"),
     os.path.join(ROOT, "target", "debug", "act_trace"),
 ]
@@ -48,7 +50,7 @@
 
 def find_trace_bin(act):
     for c in (ACT_CANDIDATES if act else TRACE_CANDIDATES):
-        if os.path.exists(c):
+        if c and os.path.exists(c):
             return c
     if act:
         sys.exit("build the ACT side first: "

From 1a4c285fdcd187dc1d7d046ca54690d372c31bdc Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 13:13:11 +0000
Subject: [PATCH 07/29] CI: rewrite bench_ab and fuzz_ab in Python

Same inputs, env vars and output files as the bash versions, which were
mostly embedded Python anyway.  bench_ab.py imports the divan helpers
from benches/ instead of shelling out to bench_avg_files.py and
bench_cmp.py.  Standard library only.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/bench_ab.py | 159 ++++++++++++++++++++++++++++++
 .github/scripts/bench_ab.sh | 131 -------------------------
 .github/scripts/fuzz_ab.py  | 191 ++++++++++++++++++++++++++++++++++++
 .github/scripts/fuzz_ab.sh  | 151 ----------------------------
 .github/workflows/ci.yml    |   4 +-
 5 files changed, 352 insertions(+), 284 deletions(-)
 create mode 100755 .github/scripts/bench_ab.py
 delete mode 100755 .github/scripts/bench_ab.sh
 create mode 100755 .github/scripts/fuzz_ab.py
 delete mode 100755 .github/scripts/fuzz_ab.sh

diff --git a/.github/scripts/bench_ab.py b/.github/scripts/bench_ab.py
new file mode 100755
index 00000000..ade18086
--- /dev/null
+++ b/.github/scripts/bench_ab.py
@@ -0,0 +1,159 @@
+#!/usr/bin/env python3
+"""A/B benchmark of two commits on the same machine.
+
+Builds the bench binaries for BASE and HEAD once each (separate target dirs),
+then runs them for ROUNDS rounds, alternating which side goes first and
+pinning every run to one core.  As soon as both sides of a bench have run in
+a round, its compare table (per-round divan medians averaged over the rounds
+finished so far, via benches/divan_fmt.py) is printed and saved as
+$BENCH_OUT/cmp-<bench>.txt; $BENCH_OUT/compare.txt, the concatenation, is
+rewritten after every completed round.  Progress lines go to
+$BENCH_OUT/progress.txt.  pr_comment.py posts compare.txt to the PR.
+
+usage: bench_ab.py <base-sha> <head-sha>
+
+env:  BENCH_ROUNDS       rounds per side                (default 3)
+      BENCHES            space separated bench targets  (default: the set used in BENCH_BUGFIXES)
+      BENCH_CPU          core to pin to                 (default 3)
+      BENCH_OUT          output directory               (default ./bench-out)
+      DIVAN_SAMPLE_COUNT sample count for benches that do not set their own (default 40)
+      CARGO_TARGET_DIR   parent of the two per-side target dirs (default ./target)
+"""
+import json, os, re, subprocess, sys, time, tomllib
+from pathlib import Path
+
+DEFAULT_BENCHES = 'shakespeare cities sparse_keys binary_keys superdense_keys act_paths zipper_head_owned product_zipper'
+
+
+def log(*a, **kw):
+    print(*a, flush=True, **kw)
+
+
+def git(*args, cwd=None):
+    return subprocess.run(['git', *args], cwd=cwd, check=True, text=True, capture_output=True).stdout.strip()
+
+
+class Bench:
+    def __init__(self, base, head):
+        self.repo = Path.cwd()
+        self.base_sha, self.head_sha = base, head
+        self.rounds = int(os.environ.get('BENCH_ROUNDS', 3))
+        self.benches = os.environ.get('BENCHES', DEFAULT_BENCHES).split()
+        self.cpu = os.environ.get('BENCH_CPU', '3')
+        self.out = Path(os.environ.get('BENCH_OUT', self.repo / 'bench-out')).resolve()
+        self.target = Path(os.environ.get('CARGO_TARGET_DIR', self.repo / 'target')).resolve()
+        self.base_src = self.out / 'src-base'
+        self.bins = {}
+        os.environ.setdefault('DIVAN_SAMPLE_COUNT', '40')
+        sys.path.insert(0, str(self.repo / 'benches'))
+        import divan_fmt
+        self.fmt = divan_fmt
+
+    def progress(self, msg):
+        with open(self.out / 'progress.txt', 'a') as f:
+            f.write(f'{time.strftime("%H:%M:%S", time.gmtime())} {msg}\n')
+
+    def short(self, sha):
+        return git('rev-parse', '--short', sha, cwd=self.repo)
+
+    def cleanup(self):
+        subprocess.run(['git', 'worktree', 'remove', '--force', str(self.base_src)], cwd=self.repo,
+                       capture_output=True)
+
+    def required_features(self, src):
+        """Features the requested benches declare via required-features, limited to those the tree has."""
+        t = tomllib.loads((src / 'Cargo.toml').read_text())
+        have = set(t.get('features', {}))
+        need = set()
+        for b in t.get('bench', []):
+            if b.get('name') in self.benches:
+                need |= set(b.get('required-features', []))
+        return sorted(need & have)
+
+    def build_side(self, side, src):
+        feats = self.required_features(src)
+        target = self.target / f'ab-{side}'
+        log(f'== building {side} ({self.short(git("rev-parse", "HEAD", cwd=src))}) into {target}'
+            + (f' with features {",".join(feats)}' if feats else ''))
+        cmd = ['cargo', 'bench', '--no-run', '--message-format=json', '--target-dir', str(target)]
+        for b in self.benches:
+            cmd += ['--bench', b]
+        if feats:
+            cmd += ['--features', ','.join(feats)]
+        with open(self.out / f'build-{side}.log', 'w') as err:
+            p = subprocess.run(cmd, cwd=src, stdout=subprocess.PIPE, stderr=err, text=True)
+        if p.returncode:
+            sys.exit(f'build of {side} failed:\n' + tail(self.out / f'build-{side}.log'))
+        exes = {}
+        for line in p.stdout.splitlines():
+            m = json.loads(line)
+            if m.get('reason') == 'compiler-artifact' and m.get('executable') and 'bench' in m['target']['kind']:
+                exes[m['target']['name']] = m['executable']
+        (self.out / f'bins-{side}.txt').write_text(''.join(f'{k} {v}\n' for k, v in exes.items()))
+        missing = [b for b in self.benches if b not in exes]
+        if missing:
+            sys.exit(f'no executable for bench(es) {missing} on {side}')
+        self.bins[side] = exes
+
+    def run(self, side, bench, rnd):
+        t0 = time.time()
+        with open(self.out / f'{side}-{bench}-r{rnd}.txt', 'w') as out, open(self.out / f'run-{side}.log', 'a') as err:
+            subprocess.run(['taskset', '-c', self.cpu, self.bins[side][bench], '--bench'],
+                           cwd=self.repo, stdout=out, stderr=err, check=True)
+        self.progress(f'round {rnd}/{self.rounds} {bench} {side} {time.time() - t0:.0f}s')
+
+    def compare_bench(self, bench, rounds_so_far):
+        """Average each side's rounds so far, compare medians, save and print the table."""
+        avg = {}
+        for side in ('base', 'head'):
+            files = sorted(self.out.glob(f'{side}-{bench}-r*.txt'))
+            data = [self.fmt.parse_divan_output(f.read_text()) for f in files]
+            avg[side] = self.fmt.average_fields(data)
+            (self.out / f'{side}-{bench}-avg.txt').write_text(self.fmt.render_divan_table(avg[side]) + '\n')
+        table = self.fmt.render_divan_table(self.fmt.compare_fields(avg['base'], avg['head'], 'median_ns'))
+        table = re.sub(r'\x1b\[[0-9;]*m', '', table)
+        text = (f'{bench}  (base {self.short(self.base_sha)}  head {self.short(self.head_sha)}'
+                f'  rounds {rounds_so_far}  median ns)\n{table}\n\n')
+        (self.out / f'cmp-{bench}.txt').write_text(text)
+        log(text, end='')
+
+    def compare_rounds(self):
+        tmp = self.out / 'compare.tmp'
+        tmp.write_text(''.join((self.out / f'cmp-{b}.txt').read_text() for b in self.benches))
+        tmp.rename(self.out / 'compare.txt')
+
+    def main(self):
+        self.out.mkdir(parents=True, exist_ok=True)
+        for f in self.out.iterdir():
+            if f.suffix in ('.txt', '.log', '.json'):
+                f.unlink()
+        self.cleanup()
+        try:
+            git('worktree', 'add', '--detach', str(self.base_src), self.base_sha, cwd=self.repo)
+            self.progress(f'plan: {self.rounds} round(s) x base/head x [{" ".join(self.benches)}], core {self.cpu}')
+            self.progress(f'building base {self.short(self.base_sha)}')
+            self.build_side('base', self.base_src)
+            self.progress(f'building head {self.short(self.head_sha)}')
+            self.build_side('head', self.repo)
+            for rnd in range(1, self.rounds + 1):
+                order = ('base', 'head') if rnd % 2 else ('head', 'base')
+                for bench in self.benches:
+                    for side in order:
+                        log(f'== round {rnd}/{self.rounds} {bench} {side}')
+                        self.run(side, bench, rnd)
+                    self.compare_bench(bench, rnd)
+                self.compare_rounds()
+                self.progress(f'round {rnd}/{self.rounds} done, compare.txt refreshed')
+            log(f'== final compare over {self.rounds} round(s): {self.out / "compare.txt"}')
+        finally:
+            self.cleanup()
+
+
+def tail(path, n=30):
+    return '\n'.join(Path(path).read_text().splitlines()[-n:])
+
+
+if __name__ == '__main__':
+    if len(sys.argv) != 3:
+        sys.exit('usage: bench_ab.py <base-sha> <head-sha>')
+    Bench(sys.argv[1], sys.argv[2]).main()
diff --git a/.github/scripts/bench_ab.sh b/.github/scripts/bench_ab.sh
deleted file mode 100755
index 559a7605..00000000
--- a/.github/scripts/bench_ab.sh
+++ /dev/null
@@ -1,131 +0,0 @@
-#!/usr/bin/env bash
-# A/B benchmark of two commits on the same machine.
-#
-# Builds the bench binaries for BASE and HEAD once each (separate target
-# dirs), then runs them for ROUNDS rounds, alternating which side goes first
-# and pinning every run to one core.  Per-bench results are averaged over the
-# rounds with benches/bench_avg_files.py and compared with benches/bench_cmp.py.
-#
-# usage: bench_ab.sh <base-sha> <head-sha>
-#
-# env:  BENCH_ROUNDS       rounds per side                (default 3)
-#       BENCHES            space separated bench targets  (default: the set used in BENCH_BUGFIXES)
-#       BENCH_CPU          core to pin to                 (default 3)
-#       BENCH_OUT          output directory               (default ./bench-out)
-#       DIVAN_SAMPLE_COUNT sample count for benches that do not set their own (default 40)
-#       CARGO_TARGET_DIR   parent of the two per-side target dirs (default ./target)
-#
-# As soon as both sides of a bench have run in a round, its compare table
-# (averaged over the rounds finished so far) is printed and saved as
-# $BENCH_OUT/cmp-<bench>.txt; $BENCH_OUT/compare.txt, the concatenation, is
-# rewritten after every completed round.  Progress lines go to
-# $BENCH_OUT/progress.txt.  pr_comment.py posts compare.txt to the PR.
-set -euo pipefail
-
-BASE_SHA=${1:?usage: bench_ab.sh <base-sha> <head-sha>}
-HEAD_SHA=${2:?usage: bench_ab.sh <base-sha> <head-sha>}
-ROUNDS=${BENCH_ROUNDS:-3}
-BENCHES=${BENCHES:-"shakespeare cities sparse_keys binary_keys superdense_keys act_paths zipper_head_owned product_zipper"}
-CPU=${BENCH_CPU:-3}
-OUT=$(realpath -m "${BENCH_OUT:-$PWD/bench-out}")
-TARGET=$(realpath -m "${CARGO_TARGET_DIR:-$PWD/target}")
-export DIVAN_SAMPLE_COUNT=${DIVAN_SAMPLE_COUNT:-40}
-
-repo=$PWD
-base_src=$OUT/src-base
-mkdir -p "$OUT"
-rm -f "$OUT"/*.txt "$OUT"/*.log "$OUT"/*.json
-
-progress() { echo "$(date -u +%H:%M:%S) $*" >> "$OUT/progress.txt"; }
-strip_ansi() { sed 's/\x1b\[[0-9;]*m//g'; }
-
-# compare_bench <bench> <rounds-so-far> : average each side over the rounds run so far and
-# compare; writes $OUT/cmp-<bench>.txt and prints it
-compare_bench() {
-    local b=$1
-    for side in base head; do
-        python3 "$repo/benches/bench_avg_files.py" "$OUT/$side-$b-r"*.txt -o "$OUT/$side-$b-avg.txt"
-    done
-    {
-        echo "$b  (base $(git rev-parse --short "$BASE_SHA")  head $(git rev-parse --short "$HEAD_SHA")  rounds $2  median ns)"
-        python3 "$repo/benches/bench_cmp.py" --base "$OUT/base-$b-avg.txt" --other "$OUT/head-$b-avg.txt" | strip_ansi
-        echo
-    } > "$OUT/cmp-$b.txt"
-    cat "$OUT/cmp-$b.txt"
-}
-
-# compare_rounds : concatenate the per-bench tables into $OUT/compare.txt
-compare_rounds() {
-    local tmp=$OUT/compare.tmp
-    : > "$tmp"
-    for b in $BENCHES; do cat "$OUT/cmp-$b.txt" >> "$tmp"; done
-    mv "$tmp" "$OUT/compare.txt"
-}
-
-cleanup() { git -C "$repo" worktree remove --force "$base_src" 2>/dev/null || true; }
-trap cleanup EXIT
-cleanup
-git worktree add --detach "$base_src" "$BASE_SHA" >/dev/null
-progress "plan: $ROUNDS round(s) x base/head x [$BENCHES], core $CPU"
-
-# build_side <side> <src-dir> : writes "<bench> <executable>" lines to $OUT/bins-<side>.txt
-build_side() {
-    local side=$1 src=$2 args=() feats
-    for b in $BENCHES; do args+=(--bench "$b"); done
-    # features the requested benches declare via required-features (only those the side's Cargo.toml has)
-    feats=$(cd "$src" && python3 - "$BENCHES" <<'PY'
-import sys, tomllib
-t = tomllib.load(open('Cargo.toml', 'rb'))
-want = set(sys.argv[1].split())
-have = set(t.get('features', {}))
-need = set()
-for b in t.get('bench', []):
-    if b.get('name') in want:
-        need |= set(b.get('required-features', []))
-print(','.join(sorted(need & have)))
-PY
-)
-    [[ -n $feats ]] && args+=(--features "$feats")
-    echo "== building $side ($(git -C "$src" rev-parse --short HEAD)) into $TARGET/ab-$side${feats:+ with features $feats}"
-    if ! (cd "$src" && cargo bench --no-run --message-format=json "${args[@]}" --target-dir "$TARGET/ab-$side" \
-            > "$OUT/build-$side.json" 2> "$OUT/build-$side.log"); then
-        echo "build of $side failed; tail of $OUT/build-$side.log:" >&2
-        tail -30 "$OUT/build-$side.log" >&2
-        exit 1
-    fi
-    python3 -c '
-import json, sys
-for line in sys.stdin:
-    m = json.loads(line)
-    if m.get("reason") == "compiler-artifact" and m.get("executable") and "bench" in m["target"]["kind"]:
-        print(m["target"]["name"], m["executable"])
-' < "$OUT/build-$side.json" > "$OUT/bins-$side.txt"
-    for b in $BENCHES; do
-        grep -q "^$b " "$OUT/bins-$side.txt" || { echo "no executable for bench $b on $side" >&2; exit 1; }
-    done
-}
-
-progress "building base $(git rev-parse --short "$BASE_SHA")"
-build_side base "$base_src"
-progress "building head $(git rev-parse --short "$HEAD_SHA")"
-build_side head "$repo"
-
-exe_for() { awk -v n="$2" '$1 == n { print $2 }' "$OUT/bins-$1.txt"; }
-
-for ((r = 1; r <= ROUNDS; r++)); do
-    if (( r % 2 )); then order="base head"; else order="head base"; fi
-    for b in $BENCHES; do
-        for side in $order; do
-            echo "== round $r/$ROUNDS $b $side"
-            t0=$SECONDS
-            taskset -c "$CPU" "$(exe_for "$side" "$b")" --bench \
-                > "$OUT/$side-$b-r$r.txt" 2>> "$OUT/run-$side.log"
-            progress "round $r/$ROUNDS $b $side $((SECONDS - t0))s"
-        done
-        compare_bench "$b" "$r"
-    done
-    compare_rounds
-    progress "round $r/$ROUNDS done, compare.txt refreshed"
-done
-
-echo "== final compare over $ROUNDS round(s): $OUT/compare.txt"
diff --git a/.github/scripts/fuzz_ab.py b/.github/scripts/fuzz_ab.py
new file mode 100755
index 00000000..7a6e2b5c
--- /dev/null
+++ b/.github/scripts/fuzz_ab.py
@@ -0,0 +1,191 @@
+#!/usr/bin/env python3
+"""Differential fuzz of two commits against the Lean model, as a regression gate.
+
+The crate at HEAD has known divergences from the model, so "zero divergences"
+cannot be the bar.  Instead both commits are run on identical inputs and the
+job fails only when HEAD diverges on an input BASE did not.  The harness
+(differential/) and the model (lean/) are taken from HEAD for both sides, so
+the only thing that differs is the crate under test in src/.  If BASE cannot
+be built with HEAD's harness, BASE's own harness is tried; if that fails too
+there is no baseline, which is reported loudly and does not fail the job.
+
+usage: fuzz_ab.py <base-sha> <head-sha>
+
+env:  FUZZ_INPUTS        random programs, model vs crate        (default 20000)
+      FUZZ_ACT_INPUTS    random programs with the ACT read side (default 5000; 0 skips)
+      FUZZ_SEED          (default 7)
+      FUZZ_JOBS          worker processes                        (default 16)
+      FUZZ_OUT           output dir                              (default ./fuzz-out)
+      CARGO_TARGET_DIR   parent of the per-side target dirs      (default ./target)
+      LAKE_CACHE         optional dir to keep lean's .lake build dirs across runs
+"""
+import os, re, shutil, subprocess, sys
+from pathlib import Path
+
+FAIL_RE = re.compile(r'^FAIL (\S+) \[saved [^\]]*\]: (.*)$')
+SUMMARY_RE = re.compile(r'^(\d+)/(\d+) inputs agree \((\d+) hit known bugs, (\d+) new divergences\)')
+
+
+def log(*a, **kw):
+    print(*a, flush=True, **kw)
+
+
+def git(*args, cwd=None, check=True):
+    return subprocess.run(['git', *args], cwd=cwd, check=check, text=True, capture_output=True).stdout.strip()
+
+
+def tail(path, n=30):
+    return '\n'.join(Path(path).read_text().splitlines()[-n:])
+
+
+class Fuzz:
+    def __init__(self, base, head):
+        self.repo = Path.cwd()
+        self.base_sha, self.head_sha = base, head
+        self.inputs = int(os.environ.get('FUZZ_INPUTS', 20000))
+        self.act_inputs = int(os.environ.get('FUZZ_ACT_INPUTS', 5000))
+        self.seed = os.environ.get('FUZZ_SEED', '7')
+        self.jobs = os.environ.get('FUZZ_JOBS', '16')
+        self.out = Path(os.environ.get('FUZZ_OUT', self.repo / 'fuzz-out')).resolve()
+        self.target = Path(os.environ.get('CARGO_TARGET_DIR', self.repo / 'target')).resolve()
+        self.lake_cache = os.environ.get('LAKE_CACHE')
+        self.base_src = self.out / 'src-base'
+        self.modes = [('crate', self.inputs, [])]
+        if self.act_inputs > 0:
+            self.modes.append(('act', self.act_inputs, ['--act']))
+
+    def short(self, sha):
+        return git('rev-parse', '--short', sha, cwd=self.repo)
+
+    def cleanup(self):
+        subprocess.run(['git', 'worktree', 'remove', '--force', str(self.base_src)], cwd=self.repo,
+                       capture_output=True)
+
+    def build_side(self, side, src):
+        """lake build + cargo build into this side's target dir.  Returns False on failure."""
+        if self.lake_cache:
+            cache = Path(self.lake_cache) / side
+            cache.mkdir(parents=True, exist_ok=True)
+            lake = src / 'lean' / '.lake'
+            if lake.is_symlink() or lake.exists():
+                lake.unlink() if lake.is_symlink() else shutil.rmtree(lake)
+            lake.symlink_to(cache)
+        for name, cmd, cwd in (('lake', ['lake', 'build'], src / 'lean'),
+                               ('build', ['cargo', 'build', '--release', '-p', 'differential',
+                                          '--target-dir', str(self.target / f'fuzz-{side}')], src)):
+            logf = self.out / f'{name}-{side}.log'
+            with open(logf, 'w') as f:
+                p = subprocess.run(cmd, cwd=cwd, stdout=f, stderr=subprocess.STDOUT)
+            if p.returncode:
+                log(f'{name} for {side} failed:\n{tail(logf)}')
+                return False
+        return True
+
+    def prepare_base(self):
+        """Build base with head's harness and model; fall back to base's own.  Returns the baseline kind."""
+        log(f"== building base ({self.short(self.base_sha)}) with head's differential/ and lean/")
+        for d in ('differential', 'lean'):
+            shutil.rmtree(self.base_src / d)
+            shutil.copytree(self.repo / d, self.base_src / d, symlinks=True,
+                            ignore=shutil.ignore_patterns('.lake'))
+        if self.build_side('base', self.base_src):
+            return 'head-harness'
+        log("== head's harness does not build against base; trying base's own")
+        git('checkout', '--', 'differential', 'lean', cwd=self.base_src)
+        git('clean', '-fdq', '--', 'differential', 'lean', cwd=self.base_src)
+        return 'base-harness' if self.build_side('base', self.base_src) else 'none'
+
+    def run_side(self, side, src, label, n, flags):
+        env = dict(os.environ,
+                   TMPDIR=str(self.out / f'fails-{side}-{label}'),
+                   PATHMAP_TRACE=str(self.target / f'fuzz-{side}' / 'release' / 'pathmap_trace'),
+                   PATHMAP_ACT_TRACE=str(self.target / f'fuzz-{side}' / 'release' / 'act_trace'))
+        Path(env['TMPDIR']).mkdir(parents=True, exist_ok=True)
+        log(f'== fuzz {label} {side}: {n} inputs, seed {self.seed}')
+        outf = self.out / f'fuzz-{label}-{side}.txt'
+        with open(outf, 'w') as f:
+            subprocess.run([str(src / 'lean' / 'differential.py'), '--random', str(n), '--seed', self.seed,
+                            '--maxlen', '300', '--max-fails', '0', '-j', self.jobs, *flags],
+                           cwd=src, env=env, stdout=f, stderr=subprocess.STDOUT)
+        text = outf.read_text()
+        info = [l for l in text.splitlines() if SUMMARY_RE.match(l) or 'child restart' in l]
+        log('\n'.join(info) if info else tail(outf, 5))
+
+    def parse(self, label, side):
+        fails, summary = {}, None
+        p = self.out / f'fuzz-{label}-{side}.txt'
+        if p.is_file():
+            for line in p.read_text().splitlines():
+                if m := FAIL_RE.match(line):
+                    fails[m.group(1)] = m.group(2)
+                if m := SUMMARY_RE.match(line):
+                    summary = tuple(map(int, m.groups()))
+        return fails, summary
+
+    def summarize(self, baseline):
+        """Write summary.md; return the number of problems (new divergences or unfinished runs)."""
+        L = [f'# Differential fuzz: head {self.short(self.head_sha)} vs base {self.short(self.base_sha)}', '', '', '']
+        if baseline == 'none':
+            L += ['**No baseline**: base could not be built with either harness, so only head was run and nothing is gated.', '']
+        elif baseline == 'base-harness':
+            L += ["Base was built with its own harness and model (head's did not build against it), "
+                  'so harness changes may show up as differences.', '']
+        bad = 0
+        for label, n, _ in self.modes:
+            hf, hs = self.parse(label, 'head')
+            bf, bs = self.parse(label, 'base')
+            L += [f'## {label}: {n} inputs, seed {self.seed}', '',
+                  '| side | agree | known | new divergences |', '|---|---:|---:|---:|']
+            for side, s in (('head', hs), ('base', bs)):
+                if s:
+                    L.append(f'| {side} | {s[0]}/{s[1]} | {s[2]} | {s[3]} |')
+                elif side == 'head' or baseline != 'none':
+                    L.append(f'| {side} | run did not finish, see fuzz-{label}-{side}.txt | | |')
+                    bad += 1
+            if baseline != 'none' and hs and bs:
+                new = sorted(set(hf) - set(bf))
+                fixed = sorted(set(bf) - set(hf))
+                L += ['', f'{len(new)} input(s) diverge on head but not on base; {len(fixed)} diverge on base but not on head.']
+                if new:
+                    bad += len(new)
+                    L += ['', '### Newly diverging inputs (head only)', '']
+                    L += [f'- `{name}`: {hf[name][:200]}' for name in new[:50]]
+                    if len(new) > 50:
+                        L.append(f'- … and {len(new) - 50} more, see fuzz-{label}-head.txt')
+                if fixed:
+                    L += ['', f'<details><summary>{len(fixed)} input(s) fixed on head</summary>', '']
+                    L += [f'- `{name}`' for name in fixed[:50]]
+                    L += ['', '</details>']
+            L.append('')
+        L[2] = ('**FAIL: new divergences relative to base, or a run did not finish**' if bad
+                else '**OK: no new divergences relative to base**')
+        text = '\n'.join(L) + '\n'
+        (self.out / 'summary.md').write_text(text)
+        log(text, end='')
+        return bad
+
+    def main(self):
+        self.out.mkdir(parents=True, exist_ok=True)
+        for f in self.out.iterdir():
+            if f.suffix in ('.txt', '.log', '.md'):
+                f.unlink()
+        self.cleanup()
+        try:
+            git('worktree', 'add', '--detach', str(self.base_src), self.base_sha, cwd=self.repo)
+            log(f'== building head ({self.short(self.head_sha)})')
+            if not self.build_side('head', self.repo):
+                sys.exit(1)
+            baseline = self.prepare_base()
+            for label, n, flags in self.modes:
+                self.run_side('head', self.repo, label, n, flags)
+                if baseline != 'none':
+                    self.run_side('base', self.base_src, label, n, flags)
+            return 1 if self.summarize(baseline) else 0
+        finally:
+            self.cleanup()
+
+
+if __name__ == '__main__':
+    if len(sys.argv) != 3:
+        sys.exit('usage: fuzz_ab.py <base-sha> <head-sha>')
+    sys.exit(Fuzz(sys.argv[1], sys.argv[2]).main())
diff --git a/.github/scripts/fuzz_ab.sh b/.github/scripts/fuzz_ab.sh
deleted file mode 100755
index 37799723..00000000
--- a/.github/scripts/fuzz_ab.sh
+++ /dev/null
@@ -1,151 +0,0 @@
-#!/usr/bin/env bash
-# Differential fuzz of two commits against the Lean model, as a regression gate.
-#
-# The crate at HEAD has known divergences from the model, so "zero divergences"
-# cannot be the bar.  Instead both commits are run on identical inputs and the
-# job fails only when HEAD diverges on an input BASE did not.  The harness
-# (differential/) and the model (lean/) are taken from HEAD for both sides, so
-# the only thing that differs is the crate under test in src/.  If BASE cannot
-# be built with HEAD's harness, BASE's own harness is tried; if that fails too
-# there is no baseline, which is reported loudly and does not fail the job.
-#
-# usage: fuzz_ab.sh <base-sha> <head-sha>
-#
-# env:  FUZZ_INPUTS        random programs, model vs crate        (default 20000)
-#       FUZZ_ACT_INPUTS    random programs with the ACT read side (default 5000; 0 skips)
-#       FUZZ_SEED          (default 7)
-#       FUZZ_JOBS          worker processes                        (default 16)
-#       FUZZ_OUT           output dir                              (default ./fuzz-out)
-#       CARGO_TARGET_DIR   parent of the per-side target dirs      (default ./target)
-#       LAKE_CACHE         optional dir to keep lean's .lake build dirs across runs
-set -euo pipefail
-
-BASE_SHA=${1:?usage: fuzz_ab.sh <base-sha> <head-sha>}
-HEAD_SHA=${2:?usage: fuzz_ab.sh <base-sha> <head-sha>}
-INPUTS=${FUZZ_INPUTS:-20000}
-ACT_INPUTS=${FUZZ_ACT_INPUTS:-5000}
-SEED=${FUZZ_SEED:-7}
-JOBS=${FUZZ_JOBS:-16}
-OUT=$(realpath -m "${FUZZ_OUT:-$PWD/fuzz-out}")
-TARGET=$(realpath -m "${CARGO_TARGET_DIR:-$PWD/target}")
-LAKE_CACHE=${LAKE_CACHE:-}
-
-repo=$PWD
-base_src=$OUT/src-base
-mkdir -p "$OUT"
-rm -f "$OUT"/*.txt "$OUT"/*.log "$OUT"/*.md
-
-cleanup() { git -C "$repo" worktree remove --force "$base_src" 2>/dev/null || true; }
-trap cleanup EXIT
-cleanup
-git worktree add --detach "$base_src" "$BASE_SHA" >/dev/null
-
-# build_side <side> <src-dir> : lake build + cargo build into this side's target dir
-build_side() {
-    local side=$1 src=$2
-    if [[ -n $LAKE_CACHE ]]; then
-        mkdir -p "$LAKE_CACHE/$side"
-        rm -rf "$src/lean/.lake"; ln -sfn "$LAKE_CACHE/$side" "$src/lean/.lake"
-    fi
-    (cd "$src/lean" && lake build) > "$OUT/lake-$side.log" 2>&1 || { tail -30 "$OUT/lake-$side.log" >&2; return 1; }
-    (cd "$src" && cargo build --release -p differential --target-dir "$TARGET/fuzz-$side") > "$OUT/build-$side.log" 2>&1 \
-        || { tail -30 "$OUT/build-$side.log" >&2; return 1; }
-}
-
-echo "== building head ($(git rev-parse --short "$HEAD_SHA"))"
-build_side head "$repo"
-
-echo "== building base ($(git rev-parse --short "$BASE_SHA")) with head's differential/ and lean/"
-rm -rf "$base_src/differential" "$base_src/lean"
-cp -r "$repo/differential" "$base_src/differential"
-cp -r "$repo/lean" "$base_src/lean" && rm -rf "$base_src/lean/.lake"   # head's model and harness, not its build dir
-baseline=head-harness
-if ! build_side base "$base_src"; then
-    echo "== head's harness does not build against base; trying base's own"
-    git -C "$base_src" checkout -- differential lean
-    git -C "$base_src" clean -fdq -- differential lean
-    if build_side base "$base_src"; then baseline=base-harness; else baseline=none; fi
-fi
-
-# run_side <side> <src-dir> <label> <inputs> [--act]
-run_side() {
-    local side=$1 src=$2 label=$3 n=$4; shift 4
-    export TMPDIR=$OUT/fails-$side-$label
-    export PATHMAP_TRACE=$TARGET/fuzz-$side/release/pathmap_trace PATHMAP_ACT_TRACE=$TARGET/fuzz-$side/release/act_trace
-    mkdir -p "$TMPDIR"
-    echo "== fuzz $label $side: $n inputs, seed $SEED"
-    (cd "$src" && ./lean/differential.py --random "$n" --seed "$SEED" --maxlen 300 --max-fails 0 -j "$JOBS" "$@") \
-        > "$OUT/fuzz-$label-$side.txt" 2>&1 || true
-    grep -E "inputs agree|child restart" "$OUT/fuzz-$label-$side.txt" || { tail -5 "$OUT/fuzz-$label-$side.txt"; }
-}
-
-modes=("crate:$INPUTS:")
-(( ACT_INPUTS > 0 )) && modes+=("act:$ACT_INPUTS:--act")
-for m in "${modes[@]}"; do
-    IFS=: read -r label n flag <<< "$m"
-    run_side head "$repo" "$label" "$n" $flag
-    [[ $baseline != none ]] && run_side base "$base_src" "$label" "$n" $flag
-done
-
-python3 - "$OUT" "$baseline" "$(git rev-parse --short "$BASE_SHA")" "$(git rev-parse --short "$HEAD_SHA")" "$SEED" "${modes[@]}" <<'PY'
-import re, sys
-from pathlib import Path
-out, baseline, base, head, seed, *modes = sys.argv[1:]
-out = Path(out)
-fail_re = re.compile(r'^FAIL (\S+) \[saved [^\]]*\]: (.*)$')
-sum_re = re.compile(r'^(\d+)/(\d+) inputs agree \((\d+) hit known bugs, (\d+) new divergences\)')
-
-def parse(p):
-    fails, summary = {}, None
-    if not p.is_file():
-        return fails, summary
-    for line in p.read_text().splitlines():
-        m = fail_re.match(line)
-        if m:
-            fails[m.group(1)] = m.group(2)
-        m = sum_re.match(line)
-        if m:
-            summary = tuple(map(int, m.groups()))
-    return fails, summary
-
-lines = [f'# Differential fuzz: head {head} vs base {base}', '']
-if baseline == 'none':
-    lines += ['**No baseline**: base could not be built with either harness, so only head was run and nothing is gated.', '']
-elif baseline == 'base-harness':
-    lines += ["Base was built with its own harness and model (head's did not build against it), so harness changes may show up as differences.", '']
-bad = 0
-for m in modes:
-    label, n, _ = m.split(':')
-    hf, hs = parse(out / f'fuzz-{label}-head.txt')
-    bf, bs = parse(out / f'fuzz-{label}-base.txt')
-    lines += [f'## {label}: {n} inputs, seed {seed}', '',
-              '| side | agree | known | new divergences |', '|---|---:|---:|---:|']
-    for side, s in (('head', hs), ('base', bs)):
-        if s:
-            lines.append(f'| {side} | {s[0]}/{s[1]} | {s[2]} | {s[3]} |')
-        elif side == 'head' or baseline != 'none':
-            lines.append(f'| {side} | run did not finish, see fuzz-{label}-{side}.txt | | |')
-            bad += 1
-    if baseline != 'none' and hs and bs:
-        new = sorted(set(hf) - set(bf))
-        fixed = sorted(set(bf) - set(hf))
-        lines += ['', f'{len(new)} input(s) diverge on head but not on base; {len(fixed)} diverge on base but not on head.']
-        if new:
-            bad += len(new)
-            lines += ['', '### Newly diverging inputs (head only)', '']
-            for name in new[:50]:
-                lines.append(f'- `{name}`: {hf[name][:200]}')
-            if len(new) > 50:
-                lines.append(f'- … and {len(new) - 50} more, see fuzz-{label}-head.txt')
-        if fixed:
-            lines += ['', f'<details><summary>{len(fixed)} input(s) fixed on head</summary>', '']
-            lines += [f'- `{name}`' for name in fixed[:50]]
-            lines += ['', '</details>']
-    lines.append('')
-verdict = 'FAIL: new divergences relative to base, or a run did not finish' if bad else 'OK: no new divergences relative to base'
-lines.insert(2, f'**{verdict}**')
-lines.insert(3, '')
-(out / 'summary.md').write_text('\n'.join(lines) + '\n')
-print('\n'.join(lines))
-sys.exit(1 if bad else 0)
-PY
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b0d5c647..3269b8f1 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -95,7 +95,7 @@ jobs:
           mkdir -p "$BENCH_OUT"
           comment() { [ -z "$PR" ] || python3 .github/scripts/pr_comment.py "$PR" "$1" || true; }
           comment "running"
-          if .github/scripts/bench_ab.sh "${{ steps.base.outputs.sha }}" "${{ github.sha }}"; then
+          if .github/scripts/bench_ab.py "${{ steps.base.outputs.sha }}" "${{ github.sha }}"; then
             comment "done"
           else
             comment "failed, see the job log"; exit 1
@@ -149,7 +149,7 @@ jobs:
           FUZZ_OUT: ${{ runner.temp }}/fuzz-out
           LAKE_CACHE: /home/gh-runner/cache/lean-lake   # checkout wipes ignored files such as lean/.lake
         run: |
-          .github/scripts/fuzz_ab.sh "${{ steps.base.outputs.sha }}" "${{ github.sha }}"
+          .github/scripts/fuzz_ab.py "${{ steps.base.outputs.sha }}" "${{ github.sha }}"
       - name: summary
         if: always()
         run: |

From 15ec363685bf0a05ac495dd1dedce6aba761c705 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 13:20:04 +0000
Subject: [PATCH 08/29] CI: move to checkout@v5 and upload-artifact@v5, which
 run on Node 24

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/workflows/ci.yml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 3269b8f1..7c12f1c4 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -38,7 +38,7 @@ jobs:
     runs-on: [self-hosted, linux, x64]
     timeout-minutes: 120
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v5
       - name: toolchain
         run: |
           rustup toolchain install stable --profile minimal
@@ -65,7 +65,7 @@ jobs:
       contents: read
       pull-requests: write   # for the progress comment; read-only on fork PRs, where commenting is skipped
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v5
         with:
           fetch-depth: 0
       - name: toolchain
@@ -108,7 +108,7 @@ jobs:
             { echo '```'; cat "$out/compare.txt"; echo '```'; } > "$out/compare.md"
             cat "$out/compare.md" >> "$GITHUB_STEP_SUMMARY"
           fi
-      - uses: actions/upload-artifact@v4
+      - uses: actions/upload-artifact@v5
         if: always()
         with:
           name: bench-out
@@ -124,7 +124,7 @@ jobs:
     runs-on: [self-hosted, linux, x64]
     timeout-minutes: 90
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v5
         with:
           fetch-depth: 0
       - name: toolchains
@@ -155,7 +155,7 @@ jobs:
         run: |
           f="${{ runner.temp }}/fuzz-out/summary.md"
           [ -s "$f" ] && cat "$f" >> "$GITHUB_STEP_SUMMARY" || true
-      - uses: actions/upload-artifact@v4
+      - uses: actions/upload-artifact@v5
         if: always()
         with:
           name: fuzz-out

From 927309cdeff587bfd343a343136a0f3629be15b1 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 13:23:57 +0000
Subject: [PATCH 09/29] CI bench: post a per-bench summary to the PR instead of
 the full tables

bench_ab.py now also writes summary.md and summary.json after every
round: one row per bench (cases, geometric mean, largest gain and loss,
counts beyond 5%) and a collapsed list of the cases that moved more than
5%.  The PR comment and the run summary use it; the full per-bench
tables stay in the job log and the bench-out artifact.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/bench_ab.py   | 58 ++++++++++++++++++++++++++++++-----
 .github/scripts/pr_comment.py | 14 ++++-----
 .github/workflows/ci.yml      | 11 +++----
 3 files changed, 63 insertions(+), 20 deletions(-)

diff --git a/.github/scripts/bench_ab.py b/.github/scripts/bench_ab.py
index ade18086..f917dffc 100755
--- a/.github/scripts/bench_ab.py
+++ b/.github/scripts/bench_ab.py
@@ -7,8 +7,10 @@
 a round, its compare table (per-round divan medians averaged over the rounds
 finished so far, via benches/divan_fmt.py) is printed and saved as
 $BENCH_OUT/cmp-<bench>.txt; $BENCH_OUT/compare.txt, the concatenation, is
-rewritten after every completed round.  Progress lines go to
-$BENCH_OUT/progress.txt.  pr_comment.py posts compare.txt to the PR.
+rewritten after every completed round, as are $BENCH_OUT/summary.md (one row
+per bench plus the cases that moved more than THRESH, which is what
+pr_comment.py posts to the PR) and summary.json.  Progress lines go to
+$BENCH_OUT/progress.txt.
 
 usage: bench_ab.py <base-sha> <head-sha>
 
@@ -19,10 +21,11 @@
       DIVAN_SAMPLE_COUNT sample count for benches that do not set their own (default 40)
       CARGO_TARGET_DIR   parent of the two per-side target dirs (default ./target)
 """
-import json, os, re, subprocess, sys, time, tomllib
+import json, math, os, re, statistics, subprocess, sys, time, tomllib
 from pathlib import Path
 
 DEFAULT_BENCHES = 'shakespeare cities sparse_keys binary_keys superdense_keys act_paths zipper_head_owned product_zipper'
+THRESH = 0.05          # a case is listed in the summary when |change| exceeds this
 
 
 def log(*a, **kw):
@@ -44,6 +47,7 @@ def __init__(self, base, head):
         self.target = Path(os.environ.get('CARGO_TARGET_DIR', self.repo / 'target')).resolve()
         self.base_src = self.out / 'src-base'
         self.bins = {}
+        self.results = {}      # bench -> {'group/case': {'base': ns, 'head': ns, 'pct': float}}
         os.environ.setdefault('DIVAN_SAMPLE_COUNT', '40')
         sys.path.insert(0, str(self.repo / 'benches'))
         import divan_fmt
@@ -110,17 +114,57 @@ def compare_bench(self, bench, rounds_so_far):
             data = [self.fmt.parse_divan_output(f.read_text()) for f in files]
             avg[side] = self.fmt.average_fields(data)
             (self.out / f'{side}-{bench}-avg.txt').write_text(self.fmt.render_divan_table(avg[side]) + '\n')
-        table = self.fmt.render_divan_table(self.fmt.compare_fields(avg['base'], avg['head'], 'median_ns'))
-        table = re.sub(r'\x1b\[[0-9;]*m', '', table)
+        cmp = self.fmt.compare_fields(avg['base'], avg['head'], 'median_ns')
+        self.results[bench] = {f'{g}/{c}': {'base': r['base'], 'head': r['other'], 'pct': r['pct']} for (g, c), r in cmp.items()}
+        table = re.sub(r'\x1b\[[0-9;]*m', '', self.fmt.render_divan_table(cmp))
         text = (f'{bench}  (base {self.short(self.base_sha)}  head {self.short(self.head_sha)}'
                 f'  rounds {rounds_so_far}  median ns)\n{table}\n\n')
         (self.out / f'cmp-{bench}.txt').write_text(text)
         log(text, end='')
 
-    def compare_rounds(self):
+    def compare_rounds(self, rounds_so_far):
         tmp = self.out / 'compare.tmp'
         tmp.write_text(''.join((self.out / f'cmp-{b}.txt').read_text() for b in self.benches))
         tmp.rename(self.out / 'compare.txt')
+        (self.out / 'summary.json').write_text(json.dumps(
+            {'base': self.short(self.base_sha), 'head': self.short(self.head_sha), 'rounds': rounds_so_far,
+             'benches': self.results}))
+        (self.out / 'summary.md').write_text(self.render_summary(rounds_so_far))
+
+    def render_summary(self, rounds_so_far):
+        """One row per bench, then the cases beyond THRESH, collapsed."""
+        def pct(v):
+            return f'{v:+.1%}'
+        L = [f'base {self.short(self.base_sha)} → head {self.short(self.head_sha)}, {rounds_so_far} round(s), '
+             f'median of each run averaged; negative is faster', '',
+             '| bench | cases | geomean | largest gain | largest loss | >5% faster | >5% slower |',
+             '|---|---:|---:|---|---|---:|---:|']
+        movers = []
+        for b in self.benches:
+            cases = self.results.get(b, {})
+            if not cases:
+                L.append(f'| {b} | 0 | | | | | |')
+                continue
+            ratios = [r['head'] / r['base'] for r in cases.values() if r['base']]
+            geo = math.exp(statistics.fmean(map(math.log, ratios))) - 1 if ratios else 0.0
+            lo = min(cases.items(), key=lambda kv: kv[1]['pct'])
+            hi = max(cases.items(), key=lambda kv: kv[1]['pct'])
+            faster = sum(r['pct'] < -THRESH for r in cases.values())
+            slower = sum(r['pct'] > THRESH for r in cases.values())
+            L.append(f'| {b} | {len(cases)} | {pct(geo)} | {pct(lo[1]["pct"])} `{lo[0]}` | {pct(hi[1]["pct"])} `{hi[0]}` '
+                     f'| {faster} | {slower} |')
+            movers += [(b, name, r) for name, r in cases.items() if abs(r['pct']) > THRESH]
+        movers.sort(key=lambda m: -abs(m[2]['pct']))
+        if movers:
+            L += ['', f'<details><summary>{len(movers)} case(s) moved more than {THRESH:.0%}</summary>', '',
+                  '| bench | case | base | head | change |', '|---|---|---:|---:|---:|']
+            L += [f'| {b} | `{name}` | {self.fmt.format_ns(r["base"])} | {self.fmt.format_ns(r["head"])} | {pct(r["pct"])} |'
+                  for b, name, r in movers[:60]]
+            if len(movers) > 60:
+                L.append(f'| | … and {len(movers) - 60} more, see compare.txt in the bench-out artifact | | | |')
+            L += ['', '</details>']
+        L += ['', 'Full tables per bench are in the job log and the bench-out artifact.']
+        return '\n'.join(L) + '\n'
 
     def main(self):
         self.out.mkdir(parents=True, exist_ok=True)
@@ -142,7 +186,7 @@ def main(self):
                         log(f'== round {rnd}/{self.rounds} {bench} {side}')
                         self.run(side, bench, rnd)
                     self.compare_bench(bench, rnd)
-                self.compare_rounds()
+                self.compare_rounds(rnd)
                 self.progress(f'round {rnd}/{self.rounds} done, compare.txt refreshed')
             log(f'== final compare over {self.rounds} round(s): {self.out / "compare.txt"}')
         finally:
diff --git a/.github/scripts/pr_comment.py b/.github/scripts/pr_comment.py
index 2f7024c7..098ca7e5 100755
--- a/.github/scripts/pr_comment.py
+++ b/.github/scripts/pr_comment.py
@@ -2,7 +2,7 @@
 """Create or update the single bench comment on a pull request.
 
 One comment per pull request, edited in place: a status line, a link to the
-job that produced it, and bench_ab.sh's compare table once it exists.  The
+job that produced it, and bench_ab.py's summary.md once it exists.  The
 first call of a run finds the PR's existing bench comment by the hidden marker
 on its first line (so a re-run or a new push reuses it) or creates it, and
 records the id in $BENCH_OUT/comment_id; later calls in the same run go
@@ -10,7 +10,7 @@
 
 usage: pr_comment.py <pr-number> <status text>
 env:   GITHUB_TOKEN GITHUB_REPOSITORY GITHUB_RUN_ID RUNNER_NAME   (provided by Actions)
-       BENCH_OUT                        dir holding compare.txt from bench_ab.sh
+       BENCH_OUT                        dir holding summary.md from bench_ab.py
        GITHUB_SERVER_URL                optional
 """
 import json, os, sys, time, urllib.request
@@ -60,13 +60,13 @@ def job_url():
 
 parts = [MARKER, f'### Bench A/B vs base: {status}', '',
          f"[job log]({job_url()}) · {time.strftime('%Y-%m-%d %H:%M:%S', time.gmtime())} UTC"]
-compare = read('compare.txt')
-if compare:
+summary = read('summary.md')
+if summary:
     head = '\n'.join(parts)
     room = LIMIT - len(head) - 200
-    if len(compare) > room:
-        compare = compare[:room] + '\n… truncated; the full table is in the bench-out artifact\n'
-    parts += ['', '```', compare.rstrip(), '```']
+    if len(summary) > room:
+        summary = summary[:room] + '\n\n… truncated; see the bench-out artifact\n'
+    parts += ['', summary.rstrip()]
 body = '\n'.join(parts)
 
 id_file = out / 'comment_id'
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 7c12f1c4..19295bda 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -103,16 +103,15 @@ jobs:
       - name: summary
         if: always()
         run: |
-          out="${{ runner.temp }}/bench-out"
-          if [ -s "$out/compare.txt" ]; then
-            { echo '```'; cat "$out/compare.txt"; echo '```'; } > "$out/compare.md"
-            cat "$out/compare.md" >> "$GITHUB_STEP_SUMMARY"
-          fi
+          f="${{ runner.temp }}/bench-out/summary.md"
+          [ -s "$f" ] && cat "$f" >> "$GITHUB_STEP_SUMMARY" || true
       - uses: actions/upload-artifact@v5
         if: always()
         with:
           name: bench-out
-          path: ${{ runner.temp }}/bench-out/*.txt
+          path: |
+            ${{ runner.temp }}/bench-out/*.txt
+            ${{ runner.temp }}/bench-out/summary.*
           if-no-files-found: ignore
 
   fuzz:

From 078e190525d77e91ebedb0b333f7dede0e85860a Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 13:36:39 +0000
Subject: [PATCH 10/29] CI: run the bench job after the fuzz gate as well as
 the tests

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/workflows/ci.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 19295bda..8f77fb64 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -55,9 +55,9 @@ jobs:
 
   bench:
     name: bench A/B vs base
-    # Runs after the tests pass (skipped when they fail), on PRs and manual runs only;
-    # a push to master has nothing to compare against.
-    needs: test
+    # Runs last, after the tests and the fuzz gate pass (skipped when either fails), on PRs
+    # and manual runs only; a push to master has nothing to compare against.
+    needs: [test, fuzz]
     if: github.event_name == 'pull_request' || github.event_name == 'workflow_dispatch'
     runs-on: [self-hosted, linux, x64, bench]
     timeout-minutes: 300

From 6d0dd4280c143a9a81df314a7af9b884e1fec66c Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 13:43:17 +0000
Subject: [PATCH 11/29] CI: upload-artifact@v7; v5 still runs on Node 20

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/workflows/ci.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 8f77fb64..32ff4479 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -105,7 +105,7 @@ jobs:
         run: |
           f="${{ runner.temp }}/bench-out/summary.md"
           [ -s "$f" ] && cat "$f" >> "$GITHUB_STEP_SUMMARY" || true
-      - uses: actions/upload-artifact@v5
+      - uses: actions/upload-artifact@v7
         if: always()
         with:
           name: bench-out
@@ -154,7 +154,7 @@ jobs:
         run: |
           f="${{ runner.temp }}/fuzz-out/summary.md"
           [ -s "$f" ] && cat "$f" >> "$GITHUB_STEP_SUMMARY" || true
-      - uses: actions/upload-artifact@v5
+      - uses: actions/upload-artifact@v7
         if: always()
         with:
           name: fuzz-out

From 42d5eebb88fd64e30629be511761d7791b59d5dd Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 13:52:13 +0000
Subject: [PATCH 12/29] CI fuzz: report new divergences as a warning
 annotation, not a failure

The job stays green; the run shows the annotation and the summary names
the inputs.  FUZZ_STRICT=1 restores the hard failure (with an error
annotation).  A run that does not finish still fails the job.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .../__pycache__/fuzz_ab.cpython-314.pyc       | Bin 0 -> 17811 bytes
 .github/scripts/fuzz_ab.py                    |  31 ++++++++++++------
 .github/workflows/ci.yml                      |   5 +--
 3 files changed, 24 insertions(+), 12 deletions(-)
 create mode 100644 .github/scripts/__pycache__/fuzz_ab.cpython-314.pyc

diff --git a/.github/scripts/__pycache__/fuzz_ab.cpython-314.pyc b/.github/scripts/__pycache__/fuzz_ab.cpython-314.pyc
new file mode 100644
index 0000000000000000000000000000000000000000..0d806eb34fbed4ed5acf8d169904bd9861c5c561
GIT binary patch
literal 17811
zcmb_^ZB!dqmSB}WkkAL8;v1X7U>orv%tvgDZEOtKV9bXLEGG^|7D#|>kd!J3Y{f}D
zy=Qm8-96xRdMs};$MST~Sl)D>knN9<-R={5PbTqf&z>nFFzQ<Nbk6SnnSYMmebSS&
zKla{NDoGF}ozp#q_3G8D``)|nzWeUG_r6=M$uR0DxW47Mf91PX6!m}bLB2Gx%(MSY
zQ`Ak0rF_&V#nL^rk0y78PeJZVpOV~FJ{7sEeQLNXdeXWzK1~^QNimouH<`GXQ>?NX
z+QrM4{*^GQIE;=}7f?Puo5s?thSk<9*z^KwTH!OWnXC?Sw9lAFL96-#iZwJVVl8J}
z%4Cf#&r_7cPf?}RrL1!5l6r8D^foz_`x#ZX%mH*RfmRPzCc{X1=p#dhhS7Zm%%zO4
z>S>g&El#wW8k<o?GK@T$!TpJPa;`a+Nnpg%6);N`lsU`3pr)u!*TjUAbGm&l`!qA*
z4+I#`1mm0YFyo$?8JCY|?2~qvoA)ukDJOH*X?HU-9*1+fma)SthI3AGPM&vp+{~oi
z=d|c_!vHqUL7uVunC`CjPG$-quev>RZpPu7b#jwV_qda1COFRwX*1Rw?_u@?oSY{a
zXpe5(?sj{8%$Spaj@da2!}I_)PP>B{^Z2F`SaME=^Sc>9#O1)zjKgqTZm-|R1FCKZ
z{B-0I8Un;(nD7WskR0>-80-n2Pqq(rF)kj)=JjwsCsf6eo_6`V{bS6WopZa~lRAQz
z-G>9OLdsn6j4`~=ew}B4AWpZL@o=@woC`2Kb^hW-+t4uE(=mLkp_ZAjyQX<E8mI!J
zY1bjz5>g(Z3nDS$a=Z8`#y&lV4eqRg6rKV!fbO~~N7D4wo5@HK9YR#5Y8vJXOMy5(
z`&Fk~qB<Gygol$T$OFBAM!ZLd6+Q0h>wpamQ6?0!2aoi?*V4@T-3}+m_?*BME;qw-
z<MlW#6B6a5DbvA}jrm>EK8Xm}<$hj9yOu!0GcrYND5M9@<#ZfjT)==hNwI-@2xc$@
zz`^Zd#_YUv+U0fvd8b_CQ`=^0+T(Ws{y5)`I5C0X1b3vjPUq+Clg?Jc={EbA#e1DO
ziY?ahQ}#CI=oBy($?9}Y_iQU8&0bIc;Q8SpCU$YqJn*iU^GtH~86cfR>{&iWofue^
z!#QF10|6Qjz-87+#e^H$JBDqEHg~iq5e$h9V8DdH={QA9yuIh3xg*R0hQI3a^4r=S
z>gwv0v1Aez4s8QEGjK9K6o#4ea93e2VKA^LdEmdVxZ=Gx9NgBL#MpAB2Id&!cFxJm
zOIqkj^apm4)-K4H*h)&Ext&G>=ZEE1;qLMKU@1epTvB0*Y#dEXJ<75=s3)V_(axS8
zunj}nHEiqbVWGAc7KR(vJo1~9@jAIWLTR5JgcRv4MvkObrFU|hXWM(bY#r?#-Cc29
zJYEzEAbb#4pNF~Xbb1+FhrsTZX;_40Spa{!U{%@2IS&t##_#5J{bpKJ4cdKEfr`;n
z?LB9is*#}@Gc)ocZ=VGr^y28qrAyT#ms*)BOSQQ&&@);!;;1p#lQbsjKvskBVMeN?
z!YP+8CV0pElfb7^>5lmsF^|i81>Rvtpfch2jDh4PH4@u`Dar~PJWJQpR{A8ZqRL<c
zhb=@YswbxX{M0Zaul8~-x6iB)X}hSnI>+N4TU{$Q)X&<vdWYR-ub%;CtH&Ys*}e6a
zNsx~Iv3h=-b9sF{nJ;NYipptNTIo<7k>E{`+@!Wt>GKVOs%)tflHkd8RoOErr$puW
zoI_NPPdUf04#!7=U2EZoD$28INMIz8O4nd)^Ov9T4x2V*p{<Gm`T`9K1kEZAAtm4%
zR7v;bbWm1(k_zRGmQY0rV;eTBI6VMx21rDe&w0%!W{lgtK0oKQN&IY9i8|gt7F&Fx
z68Jz&<9!ZzE2?=P(8a7wZUgv|=atZ0Wo0#o<Kr^qq!KcG9V9?0ecoc*t+wEEK})DP
zXbF$64ht7Y*Y&nd{luDnVpBi8rk{@J-Ga)^p>{W(Ob;A2_V8?$w8c_`aSnij*foL>
z<g!w-Vlfz_m;46rGEKgYURK%+d_~9G0r~+4!D>*6sw*Csn?vlxbd-ZOLPH(zop$+f
z2jBrx<pp*UX*c1veftPifY=~&xLr^YbXJN#0Le`%s?S_Jym0u9;b7(WE^g+T*YeDf
zyqe9tgKK#QBY7<=<tsTWxkBEth`vowwMmqLit$UP!!s)s*`dKpl#d3bS20@aQ|411
z7zHSxDpmohnpHxY#;PFI5XDr>ra?ZP)j+CawUFvjK?U_x=QCO<Uk0m(ksCzSDG*!Z
zar#16$ZPPdeRe|iP54-*xs`Iq=k-F4UjfhYRv`~<N!JMSD7i+EQOPxkY_;PW%-&G|
zk0=pj<x}PZXd729x&ExS6<`3wMv&AtF-NfRKLJ}6tCm{?EdQKwr?Hx(mg00vNXtI~
zJFPXPtYOn@<CwyV+Ch=Q5{c5uX%Yv-=kd?NO!pO->HiGOaE~F^pFk-?5<kRE$3LMR
zBN%Eida{`<-MGiO<6I77E|qai+}W(;F#~*#{Ep3r8u2H&l%gzDlM;3o$_*x?bOD@6
z&L{4pRLdJ+Sk|Ip2@v}dZ{*ydS<WTyY)<Od*jx+U6gQw@w>E*%2S0P3s3$6@q<*@X
zeh{viJCst_Jm4y(ONI-mlp=j7_Jq2lsAxDSYROB`(E?go&l0nCYFJ{Lq%DcMgq{@Z
zUQ!!H`hZ9`1him5)S(g%`#4&TqS8L@3#jYr;MQ->BRc@u21OOxWTF;fZJ@A=TGZD`
zP6?`qsPOQj2K06p=W&Zl(BZ^1$pjR2(3CBfSMg4#12>m3fClT;Gd&Ak!k)_^fkhoE
zX|{1Ys1&#vbFOip+#@$Gs!`eJ#WcIu>vTIn0fN@1CqxxNUxnz94SJuv6=`kIt;=V#
ziAI#{7WomkYTgEW3hdXW!aLoscYp89yy`pY(fu`owi0s2CEpvbY~>fdwdY>--RgUm
zyO!{-6?LSzEs}p6UhB7tcfB=s@5<dP_uO~gLS5UcDzdvPQhW;DWp0`B@0_`P=1%|Z
z{?L(SWyI8sO>Zw%MNH3;(%gc#6!&y@b@wvvW`qLE&F>w4_wY(!qp2rScqWqDyO}$*
zmOB*5JrBUzt^DG*8t=8<ZN1law@s)%y5ji2^}g#-)kYf|DH)374{zp=tmThH@<#z0
zP%Mq(UK%Mr2xXaD`Gt3`+`e+hecK(nwA>NNZ&~SBlSULREWM|_s|~eo6xIQ#F<P)Y
zq<WyguMe|A{sAGc0Sa}viyvP&9z3_M-yJn%EuL98vuW71X4n<<ha3+)_dP3`<?F)k
z_Q!^kpD8Ir*_Sn(_<q_5Q;@9T;%;^!E0uN#+F)$IMC~pB%E)XT*bclips53E5xfKs
zX~Ljpg`|<8#sT@0$WKaO)NR^{n$!?=gda%$7&1d1L1!y7XX!{NJ>2wO&$~VAnQekL
zri#ew2S8D{!4j3=2C4JMRa;bOS>;GvMFXLch7E1MWU*>d!+TUOcU&xNpod~g1c;P0
zAclsFSJa{z=>ywCOyit0o>@W|@Gy)!hk*=43r0cRZ&q_CU^$eNKo}p#9mhvPE}D>w
z$8pBgIL$cPO@6OvAf$>todAHCO1GuWS<JYV5mW~Q;g;nWK2)xDe%$w~zQ_qyC>Ro6
zxU~7g*xCzY(S6mQE9vxFi522X5Hw?iA3PhLjY4`8#V!==y!OWm9PguOPF8(WLCZ9>
z(#aczS7}wIQjlY&Mr;!*qpUDX$@N%O@{?C(RehZ*En_-aKsFK8U|bPPj7e4wWLO9A
z9&9+@s9gul9f3_!NaU8~cKh<aej_f2zGND~cvY#?N^A1QrDoM^nnkgbGEGYG^lIRz
zWz$(5s~`Cz+be6Z(gvzgkxWk+4~xdCXi_#QvZzzA1<wI5a8|DdxFKI2UE*$48z|O@
zZLt}R+h<2RQY6D!wQQ!WS{$Kmv|r&@+T!MrH+>}T;Z3Dvlv5Wbt;sOE<#rQyHcJ*s
zULBi_f6Xz@E~B2;4KfKxIVaEfB*2wYz2L<jsgU21QRR?P<&Nx)muh7S0p-+kz6_0j
zP$kl--5@Y4D2A$`;%x&bmr^c88MO<b@bB#DBg$Qri#F#429vxWHOx2|v*64F7oh{Z
z7vLxXrz1~1UEnB5cwoS>$U4DfcJs_B`!tUZO5zs;Bib_jP$6n09}X{So!4Bv&*r%*
zs!(ctp(f52c!1qpRFi%{y}(Wb>2-CS6M#T|E9yYHB>PYUhPpbb_d4*<e4!@VjY!vh
zp|XHeLZs(piyZll80$`s>kp_I^rr^W32shDtL~IJmqW2GnXl@ZtI(RLbMZF*`V82v
zSH(1fFK7~exAe?U`F*Zw5TG+ekm_Q9HlK$Zz=lvc;f`XjDi7!$NrE(OXt)zpF;T}6
zN{xetLcAx$0ygWVZAgW#Es(jW!w}_$gHsP^%Wa>5;_(?rOv8dvPKY%8^YXaNL6MPN
zTas<9Bc!yE)-s7)P84)P1^xx1)O?Ej^y2aP<DlIHP4~*~mPJhFaOZ~Uz<gKKkiFQu
z&>K>Pee=ERhURE)elY+0M??EJa?SId(ahY%*A`ye%w#^vWI~+}dhho>==<BgX!+g;
zW%tWA%Nsu_Z(LH{(cjj;Vf;nf2gd(mTy;cRdjEjhz`(*luxs70C(7&#=PwrsRfkua
zR`Y*(R4D6?GW)~(mk+J<J~BOeHCo;BiwaO)uD*Zuky99cUKo1eQU6BU#YpRmPn2}^
zB|184hYT}LKT|5o9P~o}eCHDXB#i=9t>t!0$P`Ko*~6;PY<O7M-MEq4IN!OIowwu&
zcHAj@qb$_EW!inG|MmV*(+d4z_2$W;wUa~Zrr{;}b0w8i{%K~`;*G@{w{C1@<u3V_
zCW2j|%20kN@YBj=-%qNSO9fNgde(8Vp!BnB?EAAED$De_9xC1``+`SX^TX$=PL*mt
zD%GE=)sLsp3k=UDU>$B#ZNLB-jL8RRAbvq<OtFa<K}KHbAmbE`$+9>HBxHc1y!1$1
zdq|}xfQ+XG<A!>o<?VZ-+)Eji)LPt>PShf;#SPg+`S#YnNsp{LsVCG&c3j{DOp~!<
zHL`pyqk2KjLTLwm#CMrQRTd5R6r+{pzbqRaMDDWb6-iE2RwwrdR6qrgT&$iouu4{y
zx?R>NyC%2Q$$)dtudfxGGuU<iEyj@r24yyAfVqLulSGK41tgtapcRxj>>;Ny<cQ=5
zNXO}EIKUadik@+-Ae{jv33+tH;|uifF;`t~hb546?3lDq;Gq=hr7E!3ysfKb30_Y+
z#66&%dlBf#p}%gJy8tQp3$-z^3WC=)>Gp6=t^-~K4CLS^b`%vj0X^;*MEp33NW1u<
zD57(O@p0E>+@t}CTH=rfn-X@IIu2Y56i8jfDWIyGaJ=+|0V~$U`U4^CaXUd#j-v}g
z8+AAC3?>bjI5C;P1T|)8-{ZZG`vlRQ#Y|}|HgJaeoUm7NJVN54k*yHgA=w~|B*hJ0
zu%zMi!-jZ>*+h;f7vbK(e+tP>>i=r>LIx8uJt)3k9PWIl?_po0yj5V12uCgp2K%~p
z?0;sP=i9doIg5R_`hu1B>h9Ks%QuQ^)(y2-IB;tq*m<w#Zcmv0o4#=KJI5X#TWQ#+
zIlAiGsxWU>9R8%@@XG#3#Ys@njh*yoYAUDtiIxIcj#l2mQ1gRh_m6Gr8$QuD{3f@2
z3ve;?uWJV&Gk+$i3cAA+E0rJAy<fMX?Z&dxOV;3UsBQV+itmG0-hX97EAJc2`75Rm
zcD=uAv;6cY<)`Og6|_T-tdK}XL0p`{h|x0zOI7=<5kzCM5FLrB>8Z~IMl?{5T(G=S
z8BY{ZuV||hl&NisqbvfpwU9!fu!=9MuwQ2`{2R8bPNg=pX|jm)rj4K}C5;}`@@>Hh
zu?=c4?(vf$!GEkp_5D!X{24*xkX)<|>BQ;@%?wr*QMyz5*MORFHI<0ARJ2!+*5K@l
zsO{TE<JBYtuT}H4YP)tMZV(I>%9tkZ<y6uPDz<wH+3b`Q%t@*dH;dR@;Gh(qMApRS
zvH5HPTL|yt21KHNi{7e+^Q(Q<WIRg~@8uj@l-NMnV*E>(4pz-znGBb>%f_8I-I_jF
zo+y`d^7}06yw0z%P=3WJ&{n;=kv%fRVBDyXOTgP2-~8k)auT?{lwwP)y2Ah#GgRQE
zRoAcRt&uiiuO8Zs^NCe2*LA>*K;6<*K`>UmycXm;m@vh#5u;8`E~{oVem1Zj=8u>+
zcO~=24<?Ua;nle)^R7S|30$b-E<w{AI%m+$NbC*Kh{shkcCXFH*~gt?I=UrE7Ceb*
z!+nErE-e}d+lRaR+6QgJY<owSm@PkI)Bq{s{ynrg%nd;r(85-QHVPxs%omDQ=8KHj
zSujL&fSZ#6yTy0S$Jr1S+z11i$$KS)KLoU}L6L}tKpHr+pbnPI*so1H!H3#(;6Ol6
z9_z@UIPgzXu%}&#9d3$BaJO=(6>*m#=?@skr_iDUw<=gsJ`Ow)=yO&%z>CTun{dxz
zLJS(TWhAQx1psHqgzS1a`P>vHIM2jc#I<71g$Wwj9J0Tt8#>?D*Ur9RW4pjFYxj*$
zakwlcv&TTp9_}g@Oe3^<+CJu-=5RsaskMEQ=e~=173|Uz+)D_DB1)vEMU~4v;UTIv
zm_Km~NZL8Ia7ZgzKaxXNe#E_*|2YUdaOh^_ywP~4^>!=xXoHS>Q+KDr2bU|C^Os**
z$y?C~<`WycPeh8_x5_I+!w+7(|KjrbmFAUw%WWHb+gE!w_Vx*bwvD~ENcrWhy;Wh;
zJ0%ZGpq_7KV)@k#bJwHv4f8o+*tTJ|MfP6)okp2CM$apMr=`-3^FvF8-@O#kmTYRv
z*R<u~$`zBKEnnBR;m$a<<X@T$o(uYd6QPr#mqO#=-7BgO(%(;CepxVdtZRwgb#38V
zuq(7TR1l`amErubPbhBQ$OP~4mN9#&GN@d%ea9A}w+#7<{kQtx>If-A6MttA>Q8Ji
zCnBZotF8aU3q!-do)s?G1iN$7er3&mC0e>KtPa1jGQQgU$n?)e|5yZeRp|&FJ%3Tk
zd|I|=x&0ScHroc)+6I2FRv6Erm6Wjylz=SL;;Rd<Ml#FhRnd~Nd&ln{UoWYRWR9$r
z)Gpb7s@ptpV(q|*)$Gj!9iJTNSba^n_~P2>7w^zZGyu%2gv=2b_dVZy=VH%7&ywTY
z1CO<beq;(emfPRn1=-Jy(95Fj|2@@FS(j)Y#omW$?bY41`lI5qZj<VxRu!ZlE7Kr-
zMC-e=)3+VV;x<Fng#Sk7ydDlixegG_P`vYErHu!CSg`#l8@F#iYO6YxWhRT%xOjUT
z#T&q?ceeh`j@iL-n+K7cHWJ?+2hqIWaarT`&k@?IiT7PW`qm7_H~B=hQH3lnFC0qw
zo|fP5gGwWDJMNqJ9@_>$JS4<^!rM1ul5v5p3#HADOQxf2jmg+}RlT>Q4dp^}6Na*=
z`iZEPg!Z?g6|+I|wrId<GvS(cCJ7!5#^-?4;g$eSR8Mjqzn5Did7s}q4gM4m@mv!Y
zq>-1rSu2U7+fYVi5{MuS1Qa#Ae`dzcUFSH2R-xG=(lb2Hk}P;6xuYfr4zW`MlAi?_
zei;&oZ73=U4$se_3#5CYJD3;r2PZ@4LcY*MxKk)-*f2EA(^0(v;~y4}+&U61EV`$^
ztAEqDS$JTr@WA6jaHwn*mfbVnHHI9K!WtpBW~t$EZcVhx{Ep_KW|@9lx72lS|K0te
z@;9s3OnbKq_iPqctrdcFiWFLeT+33!W-i{hc31qc<44Nyxp$s_`25=!Bb6<Y-G^U4
z{aHFy)bs?_Ssp6hyS{uTgMt?pli}Gu4GsquOv<<uD2?mjP$PE9Qwoa<q8w7it3atr
zhECiQ^%_-RZo{8N<pmv^Rgr*TV0Kt=3UEIwEsEMC*7qv<z*Wko5h!q25Gc);p++Gb
znuvsC>mt^D7S*LV1zeWoY{so`$7NNsTA6X@VC38aj3hN&`Zl<?0dE~~>gug&Ko<kl
zOJPxf?wkhWhI4R>YWoPmsgd3UA=FlVlY%(LZvw7}!T+!t<6_~2H1<@>p3Srxpx-R3
zag<872B0h(%C?0#$KbYwG{?%6JL={%#x*%`%bW$x(7<YO9wg0?%pEwkV<H1oFRS8f
zu*)SBG7(Jk8Z|OM;IRZ?m^|aE-fzWRK*$}?Ll^A`lF_Hj)PNF@0Kf}zjTB1$1D1>+
zcatk2z^rkbC8;c~57#Emm5h})BV{}BI!W!s+fLa|CLX0E1gJG0tPV8KPb$xpdxr9Y
zM%B(WV9k(6?)Z?5J7t^OsHjX>T42NAK}u0lf5~_hTQk1IH~I^IwY@BvH`tQoryVvS
zSS0L$f$cM@c)`M!Cf5PmB`apTfQISKVs}}y0K?r@tu-qdjx9@mLR%he6Nth=2O(Gh
zS=&aeNHxCEMiS{^CR9t!pG@j{$@2-gl@l87Nj{pfX2xfwTWTNHcSTZb$+KG7h%!&P
z9pe}3zmhH>dE#{0+o*(bg9?#)+{k0>zAy1i>d_{-n7b6ce-&G4s`yAWI1+ZhRWYhS
zC8Ez_RmR`#A@8a{zQt|x*kXfQ918XpXu;e^v(-R1J@E$AG^*n*s@YmO&(;m1g|XwZ
z#?>6Q4ox8W@?z8v8Y4R{){<=R5ANFW8Xm3L^7=}4<65(UZuJR|h@_mvtjjDHa2T;O
zA!lv~9KFD~d`>2&L0D!WbY40EVyboo`PMRixAai~n1mQ@Y_<f7E11rtj|Yeq*-G4=
zc#Z|p?8Mb7QrydcZD6Xpx<3(nUtQfQy&m`Y!P<*`qJgf_SiHXzVtXO1Jm%oUuM4Cv
z3(%{|%-MPJtp<kaLsjyz0i6Be2P6&)7r^dbI|+VC0+`e&evOj+#Q@fiedrML);e4<
zWQa#v{&L0TGZPHtFAc`0?Cwbjb)T_cXCVG!j`4f(8xPqqhCp}=*9lliu3=?G1;Z`i
zBPfhip!$Xsj(;N-Y<(jZVtwOFf$uj0rW<v2b@*#dN&<=-OhC!p0E@jopkQtU7|6q%
zK>rf*(nJyaolJ`4NC@cAkOxrs3)DzPeid(qTI8D=JQpRzP5O`pC-4XpC{KnVlbQsB
zbu593)>b(j-v_a^&SPKV45lieG`F?}j(@r5?O*bI6(Y5a(=uscTKoUyuYrvHaL4$Y
z{(!QMxg1blZpAl`u*8p>Umf$mZ~i@T<Oi}~jyd?+16&glIpF-3U=8F5<Q#Q4G1!-H
zI~rRCZ7^OE=!L|Ya9sn2kCEnRy$mAKmjk+^^>WofMRhf5^sS6t@}+!vHma)wit1{J
z&IK@0bD^E>@994s*t=uSu}kpuz-K|T@WG9=T%cx6b@f1RD}KAOV_BvECLWUjM1>Qp
z0M;}F)`O1)BF(tJ2f76IRRBBoJLljl7is44;6Vy(W2y)P;1@h*0&LEd4iJ#g(ka3T
z%>4ip;$vxt9Gqd3ubkj$7~<uW;PsK5Fl`7$+$rd%5p{DYYe)pPIY&BCCSiDz!E#ni
zhoQkywa-2+>JqYsBlZq)xzILIF*N}{UQ~?1eT<jvAetAIP#5eWoGZ?a-J-(8qX#r`
z_`LlPI$ffVE8r9}$k|2w`7f~QTOjXmQlDm;!<Fw;KdfFJe(%z|mm<|2g1K|G=aJ)|
zul(Z`5*;+L_QFJ@e^Th15{xe4>WtudN#Om0VHT~W+@;xd{jR9NDCFFDLQ${L?FzW%
zoK*ZC0*6j27TTl6yx{J2<9+~nLeaS$bhPsn_%w35>EBbdv74T6|CA{YH7vEF^P=@{
zS{HifyO!+HyrMf7Z(j_lL$i@Q%fhMolPO9J#-)y+dTA~=7Rm-EOWShgd**k|%Oyh2
zu@x?w(<Yp-Vo%SLo}R~^c2$Jf;92l9HHK>=C5LWnmQ=sZHAPK%ce-zP2RU-W%!eDo
z=YHHA-nUFImoK;f3|&(EO2f*zUxNE-Rk_-}YX67M)q{_6gk5JJoB9B+p!JQ>(6!}*
zkM|$m)|9aS^dt4^+#|a%IQ(c<IByenU0yfYqo&=V^6wA4e&#bhRoe2zKxGvM4{l_Z
zKNt&*y~Bptt^CrrhC(@SUicv&Zv4UA#x6@FzkW%%Rk-^tKGgW;+>dg@?Arw!Wd|aK
z4NK~1R`${uz~{dCeDI90@7y|jUa-CxVMl~>mxN2N3dOI%eB`&|d}OyPmgwK+=0{Dt
zewZ5?`a$7_$-LCFWhxMgkF7XYF06L^lk!o=ueGZIm?@TSh&D7YpZi(<vUWwW(zsgw
z%ZXpMt~xf3^a`zKfv!dU^zSG-Z-D;Pl=n$d?}n*&sU3#@sN$okNYTKrrdHsbKcouI
zhK9m9;m#iyE?53|w@}p*DL(wGskNek4b#9<`&L15u<3i(LVMnL1+8ro*Z8CH<%+kb
zR&stk6SfIQ&ptZ;=(I32B9vcRFC6`CZXt9L+#@iJKW$p}|D<)fR%o*cyDtl44xz}o
zVR8~2Rw{meCQ@|#-813N7!K#&tb6y&TG8<h({Tb3+!LG@ifT4YHSlOKqCa4XT|E2Q
zA*yuW=Pi^WKbqSz-#%}@)%javel)KjRQaIhK~1RUZrbu;q2SmGyPCf8vT(*D<a#Br
zPjgRTW`Q^euP<B=W`Fxe(6N!Z2fT9W#>K*g!lknt>CC3Kc1>Fw9$wcrqPwwkX>3DV
z6wNFYGAkjV^<SS>P{o7vzk;)^_ykQ{tB=~s`qQ<))@Al*Xj4ToXrKKjvW!8&f;GMK
zO64<y08VfnB$TJGsQEP>H1LvvhUo==U8?v<R*zCMW?X{02~a7FaoOVp25MDIm8DX7
zyAp6ERO0vy<1|@S!qkH?WbGV#B0>Y+qL|!qL22A8mUsoRn`zP$D4cOm8Jh;ssTAIn
zYOSoYf)cGsjtqe|QmD8jG9m>gva3Q?&!u?9k$9BbAd|pa&XrT6aZe&S=Btq3B<?ar
z!HGi+Rwl~j9L#QS%;nPT#TZu^0T}@9Uxo99W~;h6#yQYGxJJ+o5aWe9;Dyw!;inTR
z=5Kpzy?t>$0i$r|l`uVs17^}1_sdR#*$EB@YOs1|og~u-Of-N=lZPrrp^Vaf@Qr>6
z)`j;wFPV;I6h`+A{}C7$6^rmQNJml}j0S>x?GAE~ggO?S%YZRTZ4cxix=NKun<Z5n
zjSQl1gQD|o%#UIXB`QGq#1Bi(heQo1AsmL%rSbj=&=@!e!lHnX0<Q-!hY=EzzH<O`
zxJHu{Aq<TGW#>9Csvrc<$GwKHPhf(IDfa;;sQkz-TXHh=6D*A@Gu-R=_%lp?4vFNg
zjcF*7w^lU+AI-x@6BzQ3*>@4_G);W9TEn7tLA#i-kP-BS9rGFM+NNlB-krkRg`3&s
zYuV+Gvn%G?qYxwpr!hiF<KxUm*a`1wZ)^Wrhv5;G5QYYF*RWvtPR0|3F}-BVkh!FT
zW1H3=@esX#?A>FL`u5f4kB|N8m|(rQX|=6cZ5xKm043z$fz!qN7nfD<8Q(QV_O=O?
z$5&nwvf9@TC!@IqcaGma9y$my8iyYq-pqaOlicSZLhX+Bb!{;F4SlqrWV4`Zt)MDW
zP(9xrt=Rvd^@pvuGndrCz0oYw9ph~y94t8=xbC}_^H!c)&uWk6mIP-X=kAR{%v|5?
zzR*5U#_Ar{t>mpf_t@0)nTD#gz!}e8^Mn5T{mU(p%A;$B^7)?M7VZi89=!bE<<QIT
zUBBJ1`jTMi{uJEWXBW<XxBm}tmP0aM@C*?2S4|zIrzz?mOzjzP`=~;LX^j%nkExu~
zIZCsUYXLBc6$n!_;^QGqS}`F3nkO)aIxY#NkrZR1{Nh^dH)o3Q2?qvA!Y3R$n+@zu
z|1{<eHrq>n`*iG0rVY*rIG%i#==RubTo*QY1{1=Z$aE5?5hf!lIN>xjdBi-M4US9U
z|17XU{0`>=^UTRZ7uh!3__Uqp@$huqIX!K&fiYlADuimlQq&2;b6gqrfeAV&cpTs#
z{u0#Sr-}@92mO?x)yJQvDb%%3wK;0j(<*~{n0{KCp>BD~q^oy7&9|ucetwzGRhK-W
zAR#V#(ijdOIoM_k?Ei+}&YS6fL0N7#i5i>D;TZ>VphyuF5N+jzjC8E~5f(xCu5W7E
zH7140YQ{Y?UOZ~~j|c_s)Y#(1QzLS!D~<8L<0GypQDx^QXSt8@843B2lJM5zJMB?v
zuG+ZYz$4O$|F4jMen-=vsq$&n=N5|Ize(+jQ2YKDRrsmSuvmSoTF5&R(H*_1i5fE(
zFW$N+6gnbC=S|(yG@53fXldF*FExV>3HP86ltj4y4oZ)Iu6<rXmwZNH`ear`sSNXh
zb!E|SG`jhw#g>JZfA>m|Ue^>wwfaTvEv=B<x~@GERcZdR`&-=$!%G!+s%}>W8@^u?
j<nLX(dkrF`UXB=RHjM|?j0Ymd#>c8AST3q!GPwT_cd%Y0

literal 0
HcmV?d00001

diff --git a/.github/scripts/fuzz_ab.py b/.github/scripts/fuzz_ab.py
index 7a6e2b5c..8a20ecee 100755
--- a/.github/scripts/fuzz_ab.py
+++ b/.github/scripts/fuzz_ab.py
@@ -2,8 +2,10 @@
 """Differential fuzz of two commits against the Lean model, as a regression gate.
 
 The crate at HEAD has known divergences from the model, so "zero divergences"
-cannot be the bar.  Instead both commits are run on identical inputs and the
-job fails only when HEAD diverges on an input BASE did not.  The harness
+cannot be the bar.  Instead both commits are run on identical inputs, and an
+input that diverges on HEAD but not on BASE is reported as a GitHub warning
+annotation (the job stays green) or, with FUZZ_STRICT=1, fails the job.  A
+run that does not finish always fails the job.  The harness
 (differential/) and the model (lean/) are taken from HEAD for both sides, so
 the only thing that differs is the crate under test in src/.  If BASE cannot
 be built with HEAD's harness, BASE's own harness is tried; if that fails too
@@ -15,6 +17,7 @@
       FUZZ_ACT_INPUTS    random programs with the ACT read side (default 5000; 0 skips)
       FUZZ_SEED          (default 7)
       FUZZ_JOBS          worker processes                        (default 16)
+      FUZZ_STRICT        1 = new divergences fail the job instead of warning (default 0)
       FUZZ_OUT           output dir                              (default ./fuzz-out)
       CARGO_TARGET_DIR   parent of the per-side target dirs      (default ./target)
       LAKE_CACHE         optional dir to keep lean's .lake build dirs across runs
@@ -49,6 +52,7 @@ def __init__(self, base, head):
         self.out = Path(os.environ.get('FUZZ_OUT', self.repo / 'fuzz-out')).resolve()
         self.target = Path(os.environ.get('CARGO_TARGET_DIR', self.repo / 'target')).resolve()
         self.lake_cache = os.environ.get('LAKE_CACHE')
+        self.strict = os.environ.get('FUZZ_STRICT', '0') == '1'
         self.base_src = self.out / 'src-base'
         self.modes = [('crate', self.inputs, [])]
         if self.act_inputs > 0:
@@ -123,14 +127,14 @@ def parse(self, label, side):
         return fails, summary
 
     def summarize(self, baseline):
-        """Write summary.md; return the number of problems (new divergences or unfinished runs)."""
+        """Write summary.md; return (new divergences, unfinished runs)."""
         L = [f'# Differential fuzz: head {self.short(self.head_sha)} vs base {self.short(self.base_sha)}', '', '', '']
         if baseline == 'none':
             L += ['**No baseline**: base could not be built with either harness, so only head was run and nothing is gated.', '']
         elif baseline == 'base-harness':
             L += ["Base was built with its own harness and model (head's did not build against it), "
                   'so harness changes may show up as differences.', '']
-        bad = 0
+        new_total, unfinished = 0, 0
         for label, n, _ in self.modes:
             hf, hs = self.parse(label, 'head')
             bf, bs = self.parse(label, 'base')
@@ -141,13 +145,15 @@ def summarize(self, baseline):
                     L.append(f'| {side} | {s[0]}/{s[1]} | {s[2]} | {s[3]} |')
                 elif side == 'head' or baseline != 'none':
                     L.append(f'| {side} | run did not finish, see fuzz-{label}-{side}.txt | | |')
-                    bad += 1
+                    unfinished += 1
             if baseline != 'none' and hs and bs:
                 new = sorted(set(hf) - set(bf))
                 fixed = sorted(set(bf) - set(hf))
                 L += ['', f'{len(new)} input(s) diverge on head but not on base; {len(fixed)} diverge on base but not on head.']
                 if new:
-                    bad += len(new)
+                    new_total += len(new)
+                    log(f'::{"error" if self.strict else "warning"} title=Differential fuzz ({label})::{len(new)} input(s) diverge from the model on head '
+                        f'but not on base, e.g. {new[0]}: {hf[new[0]][:150]}')
                     L += ['', '### Newly diverging inputs (head only)', '']
                     L += [f'- `{name}`: {hf[name][:200]}' for name in new[:50]]
                     if len(new) > 50:
@@ -157,12 +163,16 @@ def summarize(self, baseline):
                     L += [f'- `{name}`' for name in fixed[:50]]
                     L += ['', '</details>']
             L.append('')
-        L[2] = ('**FAIL: new divergences relative to base, or a run did not finish**' if bad
-                else '**OK: no new divergences relative to base**')
+        if unfinished:
+            L[2] = '**FAIL: a fuzz run did not finish**'
+        elif new_total:
+            L[2] = f'**{"FAIL" if self.strict else "WARNING"}: {new_total} new divergence(s) relative to base**'
+        else:
+            L[2] = '**OK: no new divergences relative to base**'
         text = '\n'.join(L) + '\n'
         (self.out / 'summary.md').write_text(text)
         log(text, end='')
-        return bad
+        return new_total, unfinished
 
     def main(self):
         self.out.mkdir(parents=True, exist_ok=True)
@@ -180,7 +190,8 @@ def main(self):
                 self.run_side('head', self.repo, label, n, flags)
                 if baseline != 'none':
                     self.run_side('base', self.base_src, label, n, flags)
-            return 1 if self.summarize(baseline) else 0
+            new_total, unfinished = self.summarize(baseline)
+            return 1 if unfinished or (self.strict and new_total) else 0
         finally:
             self.cleanup()
 
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 32ff4479..02aeeb6f 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -116,8 +116,9 @@ jobs:
 
   fuzz:
     name: differential fuzz vs Lean model
-    # Regression gate: head and base run on identical inputs, and the job fails only when
-    # head diverges from the model on an input base did not (master has known divergences).
+    # Regression check: head and base run on identical inputs; an input on which head diverges
+    # from the model but base did not is reported as a warning annotation (master has known
+    # divergences).  Set FUZZ_STRICT=1 below to make that fail the job instead.
     needs: test
     if: github.event_name == 'pull_request' || github.event_name == 'workflow_dispatch'
     runs-on: [self-hosted, linux, x64]

From 46c5445be30bbc6d232b6cda085a106105884055 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 13:58:51 +0000
Subject: [PATCH 13/29] CI fuzz: shrink the first new divergences and emit Rust
 reproducers

For up to FUZZ_REPROS (3) newly diverging inputs with distinct
first-differing operations, fuzz_ab.py runs lean/shrink.py on the saved
input and `pathmap_trace --repro` on the result.  The summary gets a
collapsed block per input with the differing trace lines and the Rust
program; the .min.bin and .rs files go to fuzz-out/repro/ in the
artifact.  shrink.py accepts PATHMAP_ORACLE / PATHMAP_TRACE /
PATHMAP_ACT_TRACE like differential.py.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/fuzz_ab.py | 77 ++++++++++++++++++++++++++++++++++----
 .github/workflows/ci.yml   |  1 +
 lean/shrink.py             |  8 ++--
 3 files changed, 75 insertions(+), 11 deletions(-)

diff --git a/.github/scripts/fuzz_ab.py b/.github/scripts/fuzz_ab.py
index 8a20ecee..9f527f34 100755
--- a/.github/scripts/fuzz_ab.py
+++ b/.github/scripts/fuzz_ab.py
@@ -5,7 +5,10 @@
 cannot be the bar.  Instead both commits are run on identical inputs, and an
 input that diverges on HEAD but not on BASE is reported as a GitHub warning
 annotation (the job stays green) or, with FUZZ_STRICT=1, fails the job.  A
-run that does not finish always fails the job.  The harness
+run that does not finish always fails the job.  For the first REPROS newly
+diverging inputs with distinct first-differing operations, the input is
+shrunk with lean/shrink.py and a standalone Rust reproducer is emitted with
+`pathmap_trace --repro` into the summary and $FUZZ_OUT/repro/.  The harness
 (differential/) and the model (lean/) are taken from HEAD for both sides, so
 the only thing that differs is the crate under test in src/.  If BASE cannot
 be built with HEAD's harness, BASE's own harness is tried; if that fails too
@@ -18,6 +21,7 @@
       FUZZ_SEED          (default 7)
       FUZZ_JOBS          worker processes                        (default 16)
       FUZZ_STRICT        1 = new divergences fail the job instead of warning (default 0)
+      FUZZ_REPROS        newly diverging inputs to shrink and turn into Rust (default 3)
       FUZZ_OUT           output dir                              (default ./fuzz-out)
       CARGO_TARGET_DIR   parent of the per-side target dirs      (default ./target)
       LAKE_CACHE         optional dir to keep lean's .lake build dirs across runs
@@ -25,7 +29,7 @@
 import os, re, shutil, subprocess, sys
 from pathlib import Path
 
-FAIL_RE = re.compile(r'^FAIL (\S+) \[saved [^\]]*\]: (.*)$')
+FAIL_RE = re.compile(r'^FAIL (\S+) \[saved ([^\]]*)\]: (.*)$')
 SUMMARY_RE = re.compile(r'^(\d+)/(\d+) inputs agree \((\d+) hit known bugs, (\d+) new divergences\)')
 
 
@@ -53,6 +57,7 @@ def __init__(self, base, head):
         self.target = Path(os.environ.get('CARGO_TARGET_DIR', self.repo / 'target')).resolve()
         self.lake_cache = os.environ.get('LAKE_CACHE')
         self.strict = os.environ.get('FUZZ_STRICT', '0') == '1'
+        self.repros = int(os.environ.get('FUZZ_REPROS', 3))
         self.base_src = self.out / 'src-base'
         self.modes = [('crate', self.inputs, [])]
         if self.act_inputs > 0:
@@ -116,18 +121,62 @@ def run_side(self, side, src, label, n, flags):
         log('\n'.join(info) if info else tail(outf, 5))
 
     def parse(self, label, side):
-        fails, summary = {}, None
+        """fails: name -> {'path', 'msg', 'detail'}; summary: (agree, total, known, new)."""
+        fails, summary, last = {}, None, None
         p = self.out / f'fuzz-{label}-{side}.txt'
         if p.is_file():
             for line in p.read_text().splitlines():
                 if m := FAIL_RE.match(line):
-                    fails[m.group(1)] = m.group(2)
+                    last = fails[m.group(1)] = {'path': m.group(2), 'msg': m.group(3), 'detail': []}
+                elif line.startswith('  ') and last is not None:
+                    last['detail'].append(line.strip())      # the "lean: ..." / "crate: ..." trace lines
+                else:
+                    last = None
                 if m := SUMMARY_RE.match(line):
                     summary = tuple(map(int, m.groups()))
         return fails, summary
 
+    @staticmethod
+    def kind(f):
+        """What diverged: the first-differing op from the model's trace line, else the message shape."""
+        for d in f['detail']:
+            if d.startswith('lean:'):
+                parts = d.split()
+                if len(parts) > 2:
+                    return parts[2]
+        return re.sub(r'\d+', 'N', f['msg'])
+
+    def repro(self, label, name, f, flags):
+        """Shrink one newly diverging input and emit a Rust reproducer.  Returns markdown."""
+        rdir = self.out / 'repro'
+        rdir.mkdir(exist_ok=True)
+        stem = rdir / f'{label}-{name.replace("#", "_")}'
+        env = dict(os.environ,
+                   PATHMAP_ORACLE=os.environ.get('PATHMAP_ORACLE') or str(self.repo / 'lean' / '.lake' / 'build' / 'bin' / 'pathmap-oracle'),
+                   PATHMAP_TRACE=str(self.target / 'fuzz-head' / 'release' / 'pathmap_trace'),
+                   PATHMAP_ACT_TRACE=str(self.target / 'fuzz-head' / 'release' / 'act_trace'))
+        small = stem.with_suffix('.min.bin')
+        note = ''
+        try:
+            r = subprocess.run([str(self.repo / 'lean' / 'shrink.py'), f['path'], '-o', str(small), *flags],
+                               cwd=self.repo, env=env, capture_output=True, text=True, timeout=600)
+            sizes = next((l for l in r.stdout.splitlines() if ' -> ' in l and 'bytes' in l), None)
+            if r.returncode or not small.is_file():
+                raise RuntimeError((r.stdout + r.stderr).strip().splitlines()[-1:] or ['shrink failed'])
+            note = sizes.split(', written')[0] if sizes else 'shrunk'
+        except (subprocess.TimeoutExpired, RuntimeError) as e:
+            shutil.copy(f['path'], small)
+            note = f'not shrunk ({e}); reproducer is for the full input'
+        r = subprocess.run([env['PATHMAP_TRACE'], '--repro', str(small)], capture_output=True, text=True)
+        code = r.stdout if r.returncode == 0 else f'// pathmap_trace --repro failed:\n// {r.stderr.strip()}'
+        stem.with_suffix('.rs').write_text(code)
+        act_note = ' (act mode: the harness reads map1 through an ArenaCompactTree; the reproducer uses a PathMap read zipper)' if flags else ''
+        log(f'== repro {label} {name}: {self.kind(f)}, {note}\n{code}')
+        return '\n'.join([f'<details><summary><code>{name}</code>: first differs at <code>{self.kind(f)}</code>, {note}{act_note}</summary>', '',
+                           f"{f['msg']}", *[f'    {d}' for d in f['detail']], '', '```rust', code.rstrip(), '```', '', '</details>', ''])
+
     def summarize(self, baseline):
-        """Write summary.md; return (new divergences, unfinished runs)."""
+        """Write summary.md (with reproducers for the first few new divergences); return (new divergences, unfinished runs)."""
         L = [f'# Differential fuzz: head {self.short(self.head_sha)} vs base {self.short(self.base_sha)}', '', '', '']
         if baseline == 'none':
             L += ['**No baseline**: base could not be built with either harness, so only head was run and nothing is gated.', '']
@@ -147,17 +196,28 @@ def summarize(self, baseline):
                     L.append(f'| {side} | run did not finish, see fuzz-{label}-{side}.txt | | |')
                     unfinished += 1
             if baseline != 'none' and hs and bs:
-                new = sorted(set(hf) - set(bf))
+                new = sorted(set(hf) - set(bf))          # names are random#NNNNN, so this is input order
                 fixed = sorted(set(bf) - set(hf))
                 L += ['', f'{len(new)} input(s) diverge on head but not on base; {len(fixed)} diverge on base but not on head.']
                 if new:
                     new_total += len(new)
                     log(f'::{"error" if self.strict else "warning"} title=Differential fuzz ({label})::{len(new)} input(s) diverge from the model on head '
-                        f'but not on base, e.g. {new[0]}: {hf[new[0]][:150]}')
+                        f'but not on base, e.g. {new[0]}: {hf[new[0]]["msg"][:150]}')
                     L += ['', '### Newly diverging inputs (head only)', '']
-                    L += [f'- `{name}`: {hf[name][:200]}' for name in new[:50]]
+                    L += [f'- `{name}`: {hf[name]["msg"][:200]} ({self.kind(hf[name])})' for name in new[:50]]
                     if len(new) > 50:
                         L.append(f'- … and {len(new) - 50} more, see fuzz-{label}-head.txt')
+                    picked, seen = [], set()
+                    for name in new:
+                        k = self.kind(hf[name])
+                        if k not in seen:
+                            seen.add(k); picked.append(name)
+                        if len(picked) >= self.repros:
+                            break
+                    if picked:
+                        flags = next(fl for lb, _, fl in self.modes if lb == label)
+                        L += ['', f'### Reproducers: first {len(picked)} distinct kind(s), shrunk', '']
+                        L += [self.repro(label, name, hf[name], flags) for name in picked]
                 if fixed:
                     L += ['', f'<details><summary>{len(fixed)} input(s) fixed on head</summary>', '']
                     L += [f'- `{name}`' for name in fixed[:50]]
@@ -179,6 +239,7 @@ def main(self):
         for f in self.out.iterdir():
             if f.suffix in ('.txt', '.log', '.md'):
                 f.unlink()
+        shutil.rmtree(self.out / 'repro', ignore_errors=True)
         self.cleanup()
         try:
             git('worktree', 'add', '--detach', str(self.base_src), self.base_sha, cwd=self.repo)
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 02aeeb6f..b4d7a875 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -163,4 +163,5 @@ jobs:
             ${{ runner.temp }}/fuzz-out/*.txt
             ${{ runner.temp }}/fuzz-out/*.md
             ${{ runner.temp }}/fuzz-out/fails-*
+            ${{ runner.temp }}/fuzz-out/repro
           if-no-files-found: ignore
diff --git a/lean/shrink.py b/lean/shrink.py
index 7afc4fa9..65f23f64 100755
--- a/lean/shrink.py
+++ b/lean/shrink.py
@@ -9,13 +9,15 @@
 import argparse, os, re, subprocess, sys
 
 ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
-ORACLE = os.path.join(ROOT, "lean", ".lake", "build", "bin", "pathmap-oracle")
+# PATHMAP_ORACLE / PATHMAP_TRACE / PATHMAP_ACT_TRACE override the defaults, for
+# builds that live in another target dir (CI builds two commits side by side).
+ORACLE = os.environ.get("PATHMAP_ORACLE") or os.path.join(ROOT, "lean", ".lake", "build", "bin", "pathmap-oracle")
 # Release by default, matching differential.py: a debug build turns several
 # known bugs into panics, and the shrinker would then collapse every input onto
 # whichever panic it hits first.  `--debug` shrinks toward a panic on purpose.
-TRACE_RELEASE = os.path.join(ROOT, "target", "release", "pathmap_trace")
+TRACE_RELEASE = os.environ.get("PATHMAP_TRACE") or os.path.join(ROOT, "target", "release", "pathmap_trace")
 TRACE_DEBUG = os.path.join(ROOT, "target", "debug", "pathmap_trace")
-ACT_RELEASE = os.path.join(ROOT, "target", "release", "act_trace")
+ACT_RELEASE = os.environ.get("PATHMAP_ACT_TRACE") or os.path.join(ROOT, "target", "release", "act_trace")
 ACT_DEBUG = os.path.join(ROOT, "target", "debug", "act_trace")
 TRACE = TRACE_RELEASE
 ORACLE_ARGS = []

From 9c088b3f40ca500c482a792c8cb478b300d641a2 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 13:59:02 +0000
Subject: [PATCH 14/29] Drop a committed __pycache__ and ignore them

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .../scripts/__pycache__/fuzz_ab.cpython-314.pyc | Bin 17811 -> 0 bytes
 .gitignore                                      |   1 +
 2 files changed, 1 insertion(+)
 delete mode 100644 .github/scripts/__pycache__/fuzz_ab.cpython-314.pyc

diff --git a/.github/scripts/__pycache__/fuzz_ab.cpython-314.pyc b/.github/scripts/__pycache__/fuzz_ab.cpython-314.pyc
deleted file mode 100644
index 0d806eb34fbed4ed5acf8d169904bd9861c5c561..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 17811
zcmb_^ZB!dqmSB}WkkAL8;v1X7U>orv%tvgDZEOtKV9bXLEGG^|7D#|>kd!J3Y{f}D
zy=Qm8-96xRdMs};$MST~Sl)D>knN9<-R={5PbTqf&z>nFFzQ<Nbk6SnnSYMmebSS&
zKla{NDoGF}ozp#q_3G8D``)|nzWeUG_r6=M$uR0DxW47Mf91PX6!m}bLB2Gx%(MSY
zQ`Ak0rF_&V#nL^rk0y78PeJZVpOV~FJ{7sEeQLNXdeXWzK1~^QNimouH<`GXQ>?NX
z+QrM4{*^GQIE;=}7f?Puo5s?thSk<9*z^KwTH!OWnXC?Sw9lAFL96-#iZwJVVl8J}
z%4Cf#&r_7cPf?}RrL1!5l6r8D^foz_`x#ZX%mH*RfmRPzCc{X1=p#dhhS7Zm%%zO4
z>S>g&El#wW8k<o?GK@T$!TpJPa;`a+Nnpg%6);N`lsU`3pr)u!*TjUAbGm&l`!qA*
z4+I#`1mm0YFyo$?8JCY|?2~qvoA)ukDJOH*X?HU-9*1+fma)SthI3AGPM&vp+{~oi
z=d|c_!vHqUL7uVunC`CjPG$-quev>RZpPu7b#jwV_qda1COFRwX*1Rw?_u@?oSY{a
zXpe5(?sj{8%$Spaj@da2!}I_)PP>B{^Z2F`SaME=^Sc>9#O1)zjKgqTZm-|R1FCKZ
z{B-0I8Un;(nD7WskR0>-80-n2Pqq(rF)kj)=JjwsCsf6eo_6`V{bS6WopZa~lRAQz
z-G>9OLdsn6j4`~=ew}B4AWpZL@o=@woC`2Kb^hW-+t4uE(=mLkp_ZAjyQX<E8mI!J
zY1bjz5>g(Z3nDS$a=Z8`#y&lV4eqRg6rKV!fbO~~N7D4wo5@HK9YR#5Y8vJXOMy5(
z`&Fk~qB<Gygol$T$OFBAM!ZLd6+Q0h>wpamQ6?0!2aoi?*V4@T-3}+m_?*BME;qw-
z<MlW#6B6a5DbvA}jrm>EK8Xm}<$hj9yOu!0GcrYND5M9@<#ZfjT)==hNwI-@2xc$@
zz`^Zd#_YUv+U0fvd8b_CQ`=^0+T(Ws{y5)`I5C0X1b3vjPUq+Clg?Jc={EbA#e1DO
ziY?ahQ}#CI=oBy($?9}Y_iQU8&0bIc;Q8SpCU$YqJn*iU^GtH~86cfR>{&iWofue^
z!#QF10|6Qjz-87+#e^H$JBDqEHg~iq5e$h9V8DdH={QA9yuIh3xg*R0hQI3a^4r=S
z>gwv0v1Aez4s8QEGjK9K6o#4ea93e2VKA^LdEmdVxZ=Gx9NgBL#MpAB2Id&!cFxJm
zOIqkj^apm4)-K4H*h)&Ext&G>=ZEE1;qLMKU@1epTvB0*Y#dEXJ<75=s3)V_(axS8
zunj}nHEiqbVWGAc7KR(vJo1~9@jAIWLTR5JgcRv4MvkObrFU|hXWM(bY#r?#-Cc29
zJYEzEAbb#4pNF~Xbb1+FhrsTZX;_40Spa{!U{%@2IS&t##_#5J{bpKJ4cdKEfr`;n
z?LB9is*#}@Gc)ocZ=VGr^y28qrAyT#ms*)BOSQQ&&@);!;;1p#lQbsjKvskBVMeN?
z!YP+8CV0pElfb7^>5lmsF^|i81>Rvtpfch2jDh4PH4@u`Dar~PJWJQpR{A8ZqRL<c
zhb=@YswbxX{M0Zaul8~-x6iB)X}hSnI>+N4TU{$Q)X&<vdWYR-ub%;CtH&Ys*}e6a
zNsx~Iv3h=-b9sF{nJ;NYipptNTIo<7k>E{`+@!Wt>GKVOs%)tflHkd8RoOErr$puW
zoI_NPPdUf04#!7=U2EZoD$28INMIz8O4nd)^Ov9T4x2V*p{<Gm`T`9K1kEZAAtm4%
zR7v;bbWm1(k_zRGmQY0rV;eTBI6VMx21rDe&w0%!W{lgtK0oKQN&IY9i8|gt7F&Fx
z68Jz&<9!ZzE2?=P(8a7wZUgv|=atZ0Wo0#o<Kr^qq!KcG9V9?0ecoc*t+wEEK})DP
zXbF$64ht7Y*Y&nd{luDnVpBi8rk{@J-Ga)^p>{W(Ob;A2_V8?$w8c_`aSnij*foL>
z<g!w-Vlfz_m;46rGEKgYURK%+d_~9G0r~+4!D>*6sw*Csn?vlxbd-ZOLPH(zop$+f
z2jBrx<pp*UX*c1veftPifY=~&xLr^YbXJN#0Le`%s?S_Jym0u9;b7(WE^g+T*YeDf
zyqe9tgKK#QBY7<=<tsTWxkBEth`vowwMmqLit$UP!!s)s*`dKpl#d3bS20@aQ|411
z7zHSxDpmohnpHxY#;PFI5XDr>ra?ZP)j+CawUFvjK?U_x=QCO<Uk0m(ksCzSDG*!Z
zar#16$ZPPdeRe|iP54-*xs`Iq=k-F4UjfhYRv`~<N!JMSD7i+EQOPxkY_;PW%-&G|
zk0=pj<x}PZXd729x&ExS6<`3wMv&AtF-NfRKLJ}6tCm{?EdQKwr?Hx(mg00vNXtI~
zJFPXPtYOn@<CwyV+Ch=Q5{c5uX%Yv-=kd?NO!pO->HiGOaE~F^pFk-?5<kRE$3LMR
zBN%Eida{`<-MGiO<6I77E|qai+}W(;F#~*#{Ep3r8u2H&l%gzDlM;3o$_*x?bOD@6
z&L{4pRLdJ+Sk|Ip2@v}dZ{*ydS<WTyY)<Od*jx+U6gQw@w>E*%2S0P3s3$6@q<*@X
zeh{viJCst_Jm4y(ONI-mlp=j7_Jq2lsAxDSYROB`(E?go&l0nCYFJ{Lq%DcMgq{@Z
zUQ!!H`hZ9`1him5)S(g%`#4&TqS8L@3#jYr;MQ->BRc@u21OOxWTF;fZJ@A=TGZD`
zP6?`qsPOQj2K06p=W&Zl(BZ^1$pjR2(3CBfSMg4#12>m3fClT;Gd&Ak!k)_^fkhoE
zX|{1Ys1&#vbFOip+#@$Gs!`eJ#WcIu>vTIn0fN@1CqxxNUxnz94SJuv6=`kIt;=V#
ziAI#{7WomkYTgEW3hdXW!aLoscYp89yy`pY(fu`owi0s2CEpvbY~>fdwdY>--RgUm
zyO!{-6?LSzEs}p6UhB7tcfB=s@5<dP_uO~gLS5UcDzdvPQhW;DWp0`B@0_`P=1%|Z
z{?L(SWyI8sO>Zw%MNH3;(%gc#6!&y@b@wvvW`qLE&F>w4_wY(!qp2rScqWqDyO}$*
zmOB*5JrBUzt^DG*8t=8<ZN1law@s)%y5ji2^}g#-)kYf|DH)374{zp=tmThH@<#z0
zP%Mq(UK%Mr2xXaD`Gt3`+`e+hecK(nwA>NNZ&~SBlSULREWM|_s|~eo6xIQ#F<P)Y
zq<WyguMe|A{sAGc0Sa}viyvP&9z3_M-yJn%EuL98vuW71X4n<<ha3+)_dP3`<?F)k
z_Q!^kpD8Ir*_Sn(_<q_5Q;@9T;%;^!E0uN#+F)$IMC~pB%E)XT*bclips53E5xfKs
zX~Ljpg`|<8#sT@0$WKaO)NR^{n$!?=gda%$7&1d1L1!y7XX!{NJ>2wO&$~VAnQekL
zri#ew2S8D{!4j3=2C4JMRa;bOS>;GvMFXLch7E1MWU*>d!+TUOcU&xNpod~g1c;P0
zAclsFSJa{z=>ywCOyit0o>@W|@Gy)!hk*=43r0cRZ&q_CU^$eNKo}p#9mhvPE}D>w
z$8pBgIL$cPO@6OvAf$>todAHCO1GuWS<JYV5mW~Q;g;nWK2)xDe%$w~zQ_qyC>Ro6
zxU~7g*xCzY(S6mQE9vxFi522X5Hw?iA3PhLjY4`8#V!==y!OWm9PguOPF8(WLCZ9>
z(#aczS7}wIQjlY&Mr;!*qpUDX$@N%O@{?C(RehZ*En_-aKsFK8U|bPPj7e4wWLO9A
z9&9+@s9gul9f3_!NaU8~cKh<aej_f2zGND~cvY#?N^A1QrDoM^nnkgbGEGYG^lIRz
zWz$(5s~`Cz+be6Z(gvzgkxWk+4~xdCXi_#QvZzzA1<wI5a8|DdxFKI2UE*$48z|O@
zZLt}R+h<2RQY6D!wQQ!WS{$Kmv|r&@+T!MrH+>}T;Z3Dvlv5Wbt;sOE<#rQyHcJ*s
zULBi_f6Xz@E~B2;4KfKxIVaEfB*2wYz2L<jsgU21QRR?P<&Nx)muh7S0p-+kz6_0j
zP$kl--5@Y4D2A$`;%x&bmr^c88MO<b@bB#DBg$Qri#F#429vxWHOx2|v*64F7oh{Z
z7vLxXrz1~1UEnB5cwoS>$U4DfcJs_B`!tUZO5zs;Bib_jP$6n09}X{So!4Bv&*r%*
zs!(ctp(f52c!1qpRFi%{y}(Wb>2-CS6M#T|E9yYHB>PYUhPpbb_d4*<e4!@VjY!vh
zp|XHeLZs(piyZll80$`s>kp_I^rr^W32shDtL~IJmqW2GnXl@ZtI(RLbMZF*`V82v
zSH(1fFK7~exAe?U`F*Zw5TG+ekm_Q9HlK$Zz=lvc;f`XjDi7!$NrE(OXt)zpF;T}6
zN{xetLcAx$0ygWVZAgW#Es(jW!w}_$gHsP^%Wa>5;_(?rOv8dvPKY%8^YXaNL6MPN
zTas<9Bc!yE)-s7)P84)P1^xx1)O?Ej^y2aP<DlIHP4~*~mPJhFaOZ~Uz<gKKkiFQu
z&>K>Pee=ERhURE)elY+0M??EJa?SId(ahY%*A`ye%w#^vWI~+}dhho>==<BgX!+g;
zW%tWA%Nsu_Z(LH{(cjj;Vf;nf2gd(mTy;cRdjEjhz`(*luxs70C(7&#=PwrsRfkua
zR`Y*(R4D6?GW)~(mk+J<J~BOeHCo;BiwaO)uD*Zuky99cUKo1eQU6BU#YpRmPn2}^
zB|184hYT}LKT|5o9P~o}eCHDXB#i=9t>t!0$P`Ko*~6;PY<O7M-MEq4IN!OIowwu&
zcHAj@qb$_EW!inG|MmV*(+d4z_2$W;wUa~Zrr{;}b0w8i{%K~`;*G@{w{C1@<u3V_
zCW2j|%20kN@YBj=-%qNSO9fNgde(8Vp!BnB?EAAED$De_9xC1``+`SX^TX$=PL*mt
zD%GE=)sLsp3k=UDU>$B#ZNLB-jL8RRAbvq<OtFa<K}KHbAmbE`$+9>HBxHc1y!1$1
zdq|}xfQ+XG<A!>o<?VZ-+)Eji)LPt>PShf;#SPg+`S#YnNsp{LsVCG&c3j{DOp~!<
zHL`pyqk2KjLTLwm#CMrQRTd5R6r+{pzbqRaMDDWb6-iE2RwwrdR6qrgT&$iouu4{y
zx?R>NyC%2Q$$)dtudfxGGuU<iEyj@r24yyAfVqLulSGK41tgtapcRxj>>;Ny<cQ=5
zNXO}EIKUadik@+-Ae{jv33+tH;|uifF;`t~hb546?3lDq;Gq=hr7E!3ysfKb30_Y+
z#66&%dlBf#p}%gJy8tQp3$-z^3WC=)>Gp6=t^-~K4CLS^b`%vj0X^;*MEp33NW1u<
zD57(O@p0E>+@t}CTH=rfn-X@IIu2Y56i8jfDWIyGaJ=+|0V~$U`U4^CaXUd#j-v}g
z8+AAC3?>bjI5C;P1T|)8-{ZZG`vlRQ#Y|}|HgJaeoUm7NJVN54k*yHgA=w~|B*hJ0
zu%zMi!-jZ>*+h;f7vbK(e+tP>>i=r>LIx8uJt)3k9PWIl?_po0yj5V12uCgp2K%~p
z?0;sP=i9doIg5R_`hu1B>h9Ks%QuQ^)(y2-IB;tq*m<w#Zcmv0o4#=KJI5X#TWQ#+
zIlAiGsxWU>9R8%@@XG#3#Ys@njh*yoYAUDtiIxIcj#l2mQ1gRh_m6Gr8$QuD{3f@2
z3ve;?uWJV&Gk+$i3cAA+E0rJAy<fMX?Z&dxOV;3UsBQV+itmG0-hX97EAJc2`75Rm
zcD=uAv;6cY<)`Og6|_T-tdK}XL0p`{h|x0zOI7=<5kzCM5FLrB>8Z~IMl?{5T(G=S
z8BY{ZuV||hl&NisqbvfpwU9!fu!=9MuwQ2`{2R8bPNg=pX|jm)rj4K}C5;}`@@>Hh
zu?=c4?(vf$!GEkp_5D!X{24*xkX)<|>BQ;@%?wr*QMyz5*MORFHI<0ARJ2!+*5K@l
zsO{TE<JBYtuT}H4YP)tMZV(I>%9tkZ<y6uPDz<wH+3b`Q%t@*dH;dR@;Gh(qMApRS
zvH5HPTL|yt21KHNi{7e+^Q(Q<WIRg~@8uj@l-NMnV*E>(4pz-znGBb>%f_8I-I_jF
zo+y`d^7}06yw0z%P=3WJ&{n;=kv%fRVBDyXOTgP2-~8k)auT?{lwwP)y2Ah#GgRQE
zRoAcRt&uiiuO8Zs^NCe2*LA>*K;6<*K`>UmycXm;m@vh#5u;8`E~{oVem1Zj=8u>+
zcO~=24<?Ua;nle)^R7S|30$b-E<w{AI%m+$NbC*Kh{shkcCXFH*~gt?I=UrE7Ceb*
z!+nErE-e}d+lRaR+6QgJY<owSm@PkI)Bq{s{ynrg%nd;r(85-QHVPxs%omDQ=8KHj
zSujL&fSZ#6yTy0S$Jr1S+z11i$$KS)KLoU}L6L}tKpHr+pbnPI*so1H!H3#(;6Ol6
z9_z@UIPgzXu%}&#9d3$BaJO=(6>*m#=?@skr_iDUw<=gsJ`Ow)=yO&%z>CTun{dxz
zLJS(TWhAQx1psHqgzS1a`P>vHIM2jc#I<71g$Wwj9J0Tt8#>?D*Ur9RW4pjFYxj*$
zakwlcv&TTp9_}g@Oe3^<+CJu-=5RsaskMEQ=e~=173|Uz+)D_DB1)vEMU~4v;UTIv
zm_Km~NZL8Ia7ZgzKaxXNe#E_*|2YUdaOh^_ywP~4^>!=xXoHS>Q+KDr2bU|C^Os**
z$y?C~<`WycPeh8_x5_I+!w+7(|KjrbmFAUw%WWHb+gE!w_Vx*bwvD~ENcrWhy;Wh;
zJ0%ZGpq_7KV)@k#bJwHv4f8o+*tTJ|MfP6)okp2CM$apMr=`-3^FvF8-@O#kmTYRv
z*R<u~$`zBKEnnBR;m$a<<X@T$o(uYd6QPr#mqO#=-7BgO(%(;CepxVdtZRwgb#38V
zuq(7TR1l`amErubPbhBQ$OP~4mN9#&GN@d%ea9A}w+#7<{kQtx>If-A6MttA>Q8Ji
zCnBZotF8aU3q!-do)s?G1iN$7er3&mC0e>KtPa1jGQQgU$n?)e|5yZeRp|&FJ%3Tk
zd|I|=x&0ScHroc)+6I2FRv6Erm6Wjylz=SL;;Rd<Ml#FhRnd~Nd&ln{UoWYRWR9$r
z)Gpb7s@ptpV(q|*)$Gj!9iJTNSba^n_~P2>7w^zZGyu%2gv=2b_dVZy=VH%7&ywTY
z1CO<beq;(emfPRn1=-Jy(95Fj|2@@FS(j)Y#omW$?bY41`lI5qZj<VxRu!ZlE7Kr-
zMC-e=)3+VV;x<Fng#Sk7ydDlixegG_P`vYErHu!CSg`#l8@F#iYO6YxWhRT%xOjUT
z#T&q?ceeh`j@iL-n+K7cHWJ?+2hqIWaarT`&k@?IiT7PW`qm7_H~B=hQH3lnFC0qw
zo|fP5gGwWDJMNqJ9@_>$JS4<^!rM1ul5v5p3#HADOQxf2jmg+}RlT>Q4dp^}6Na*=
z`iZEPg!Z?g6|+I|wrId<GvS(cCJ7!5#^-?4;g$eSR8Mjqzn5Did7s}q4gM4m@mv!Y
zq>-1rSu2U7+fYVi5{MuS1Qa#Ae`dzcUFSH2R-xG=(lb2Hk}P;6xuYfr4zW`MlAi?_
zei;&oZ73=U4$se_3#5CYJD3;r2PZ@4LcY*MxKk)-*f2EA(^0(v;~y4}+&U61EV`$^
ztAEqDS$JTr@WA6jaHwn*mfbVnHHI9K!WtpBW~t$EZcVhx{Ep_KW|@9lx72lS|K0te
z@;9s3OnbKq_iPqctrdcFiWFLeT+33!W-i{hc31qc<44Nyxp$s_`25=!Bb6<Y-G^U4
z{aHFy)bs?_Ssp6hyS{uTgMt?pli}Gu4GsquOv<<uD2?mjP$PE9Qwoa<q8w7it3atr
zhECiQ^%_-RZo{8N<pmv^Rgr*TV0Kt=3UEIwEsEMC*7qv<z*Wko5h!q25Gc);p++Gb
znuvsC>mt^D7S*LV1zeWoY{so`$7NNsTA6X@VC38aj3hN&`Zl<?0dE~~>gug&Ko<kl
zOJPxf?wkhWhI4R>YWoPmsgd3UA=FlVlY%(LZvw7}!T+!t<6_~2H1<@>p3Srxpx-R3
zag<872B0h(%C?0#$KbYwG{?%6JL={%#x*%`%bW$x(7<YO9wg0?%pEwkV<H1oFRS8f
zu*)SBG7(Jk8Z|OM;IRZ?m^|aE-fzWRK*$}?Ll^A`lF_Hj)PNF@0Kf}zjTB1$1D1>+
zcatk2z^rkbC8;c~57#Emm5h})BV{}BI!W!s+fLa|CLX0E1gJG0tPV8KPb$xpdxr9Y
zM%B(WV9k(6?)Z?5J7t^OsHjX>T42NAK}u0lf5~_hTQk1IH~I^IwY@BvH`tQoryVvS
zSS0L$f$cM@c)`M!Cf5PmB`apTfQISKVs}}y0K?r@tu-qdjx9@mLR%he6Nth=2O(Gh
zS=&aeNHxCEMiS{^CR9t!pG@j{$@2-gl@l87Nj{pfX2xfwTWTNHcSTZb$+KG7h%!&P
z9pe}3zmhH>dE#{0+o*(bg9?#)+{k0>zAy1i>d_{-n7b6ce-&G4s`yAWI1+ZhRWYhS
zC8Ez_RmR`#A@8a{zQt|x*kXfQ918XpXu;e^v(-R1J@E$AG^*n*s@YmO&(;m1g|XwZ
z#?>6Q4ox8W@?z8v8Y4R{){<=R5ANFW8Xm3L^7=}4<65(UZuJR|h@_mvtjjDHa2T;O
zA!lv~9KFD~d`>2&L0D!WbY40EVyboo`PMRixAai~n1mQ@Y_<f7E11rtj|Yeq*-G4=
zc#Z|p?8Mb7QrydcZD6Xpx<3(nUtQfQy&m`Y!P<*`qJgf_SiHXzVtXO1Jm%oUuM4Cv
z3(%{|%-MPJtp<kaLsjyz0i6Be2P6&)7r^dbI|+VC0+`e&evOj+#Q@fiedrML);e4<
zWQa#v{&L0TGZPHtFAc`0?Cwbjb)T_cXCVG!j`4f(8xPqqhCp}=*9lliu3=?G1;Z`i
zBPfhip!$Xsj(;N-Y<(jZVtwOFf$uj0rW<v2b@*#dN&<=-OhC!p0E@jopkQtU7|6q%
zK>rf*(nJyaolJ`4NC@cAkOxrs3)DzPeid(qTI8D=JQpRzP5O`pC-4XpC{KnVlbQsB
zbu593)>b(j-v_a^&SPKV45lieG`F?}j(@r5?O*bI6(Y5a(=uscTKoUyuYrvHaL4$Y
z{(!QMxg1blZpAl`u*8p>Umf$mZ~i@T<Oi}~jyd?+16&glIpF-3U=8F5<Q#Q4G1!-H
zI~rRCZ7^OE=!L|Ya9sn2kCEnRy$mAKmjk+^^>WofMRhf5^sS6t@}+!vHma)wit1{J
z&IK@0bD^E>@994s*t=uSu}kpuz-K|T@WG9=T%cx6b@f1RD}KAOV_BvECLWUjM1>Qp
z0M;}F)`O1)BF(tJ2f76IRRBBoJLljl7is44;6Vy(W2y)P;1@h*0&LEd4iJ#g(ka3T
z%>4ip;$vxt9Gqd3ubkj$7~<uW;PsK5Fl`7$+$rd%5p{DYYe)pPIY&BCCSiDz!E#ni
zhoQkywa-2+>JqYsBlZq)xzILIF*N}{UQ~?1eT<jvAetAIP#5eWoGZ?a-J-(8qX#r`
z_`LlPI$ffVE8r9}$k|2w`7f~QTOjXmQlDm;!<Fw;KdfFJe(%z|mm<|2g1K|G=aJ)|
zul(Z`5*;+L_QFJ@e^Th15{xe4>WtudN#Om0VHT~W+@;xd{jR9NDCFFDLQ${L?FzW%
zoK*ZC0*6j27TTl6yx{J2<9+~nLeaS$bhPsn_%w35>EBbdv74T6|CA{YH7vEF^P=@{
zS{HifyO!+HyrMf7Z(j_lL$i@Q%fhMolPO9J#-)y+dTA~=7Rm-EOWShgd**k|%Oyh2
zu@x?w(<Yp-Vo%SLo}R~^c2$Jf;92l9HHK>=C5LWnmQ=sZHAPK%ce-zP2RU-W%!eDo
z=YHHA-nUFImoK;f3|&(EO2f*zUxNE-Rk_-}YX67M)q{_6gk5JJoB9B+p!JQ>(6!}*
zkM|$m)|9aS^dt4^+#|a%IQ(c<IByenU0yfYqo&=V^6wA4e&#bhRoe2zKxGvM4{l_Z
zKNt&*y~Bptt^CrrhC(@SUicv&Zv4UA#x6@FzkW%%Rk-^tKGgW;+>dg@?Arw!Wd|aK
z4NK~1R`${uz~{dCeDI90@7y|jUa-CxVMl~>mxN2N3dOI%eB`&|d}OyPmgwK+=0{Dt
zewZ5?`a$7_$-LCFWhxMgkF7XYF06L^lk!o=ueGZIm?@TSh&D7YpZi(<vUWwW(zsgw
z%ZXpMt~xf3^a`zKfv!dU^zSG-Z-D;Pl=n$d?}n*&sU3#@sN$okNYTKrrdHsbKcouI
zhK9m9;m#iyE?53|w@}p*DL(wGskNek4b#9<`&L15u<3i(LVMnL1+8ro*Z8CH<%+kb
zR&stk6SfIQ&ptZ;=(I32B9vcRFC6`CZXt9L+#@iJKW$p}|D<)fR%o*cyDtl44xz}o
zVR8~2Rw{meCQ@|#-813N7!K#&tb6y&TG8<h({Tb3+!LG@ifT4YHSlOKqCa4XT|E2Q
zA*yuW=Pi^WKbqSz-#%}@)%javel)KjRQaIhK~1RUZrbu;q2SmGyPCf8vT(*D<a#Br
zPjgRTW`Q^euP<B=W`Fxe(6N!Z2fT9W#>K*g!lknt>CC3Kc1>Fw9$wcrqPwwkX>3DV
z6wNFYGAkjV^<SS>P{o7vzk;)^_ykQ{tB=~s`qQ<))@Al*Xj4ToXrKKjvW!8&f;GMK
zO64<y08VfnB$TJGsQEP>H1LvvhUo==U8?v<R*zCMW?X{02~a7FaoOVp25MDIm8DX7
zyAp6ERO0vy<1|@S!qkH?WbGV#B0>Y+qL|!qL22A8mUsoRn`zP$D4cOm8Jh;ssTAIn
zYOSoYf)cGsjtqe|QmD8jG9m>gva3Q?&!u?9k$9BbAd|pa&XrT6aZe&S=Btq3B<?ar
z!HGi+Rwl~j9L#QS%;nPT#TZu^0T}@9Uxo99W~;h6#yQYGxJJ+o5aWe9;Dyw!;inTR
z=5Kpzy?t>$0i$r|l`uVs17^}1_sdR#*$EB@YOs1|og~u-Of-N=lZPrrp^Vaf@Qr>6
z)`j;wFPV;I6h`+A{}C7$6^rmQNJml}j0S>x?GAE~ggO?S%YZRTZ4cxix=NKun<Z5n
zjSQl1gQD|o%#UIXB`QGq#1Bi(heQo1AsmL%rSbj=&=@!e!lHnX0<Q-!hY=EzzH<O`
zxJHu{Aq<TGW#>9Csvrc<$GwKHPhf(IDfa;;sQkz-TXHh=6D*A@Gu-R=_%lp?4vFNg
zjcF*7w^lU+AI-x@6BzQ3*>@4_G);W9TEn7tLA#i-kP-BS9rGFM+NNlB-krkRg`3&s
zYuV+Gvn%G?qYxwpr!hiF<KxUm*a`1wZ)^Wrhv5;G5QYYF*RWvtPR0|3F}-BVkh!FT
zW1H3=@esX#?A>FL`u5f4kB|N8m|(rQX|=6cZ5xKm043z$fz!qN7nfD<8Q(QV_O=O?
z$5&nwvf9@TC!@IqcaGma9y$my8iyYq-pqaOlicSZLhX+Bb!{;F4SlqrWV4`Zt)MDW
zP(9xrt=Rvd^@pvuGndrCz0oYw9ph~y94t8=xbC}_^H!c)&uWk6mIP-X=kAR{%v|5?
zzR*5U#_Ar{t>mpf_t@0)nTD#gz!}e8^Mn5T{mU(p%A;$B^7)?M7VZi89=!bE<<QIT
zUBBJ1`jTMi{uJEWXBW<XxBm}tmP0aM@C*?2S4|zIrzz?mOzjzP`=~;LX^j%nkExu~
zIZCsUYXLBc6$n!_;^QGqS}`F3nkO)aIxY#NkrZR1{Nh^dH)o3Q2?qvA!Y3R$n+@zu
z|1{<eHrq>n`*iG0rVY*rIG%i#==RubTo*QY1{1=Z$aE5?5hf!lIN>xjdBi-M4US9U
z|17XU{0`>=^UTRZ7uh!3__Uqp@$huqIX!K&fiYlADuimlQq&2;b6gqrfeAV&cpTs#
z{u0#Sr-}@92mO?x)yJQvDb%%3wK;0j(<*~{n0{KCp>BD~q^oy7&9|ucetwzGRhK-W
zAR#V#(ijdOIoM_k?Ei+}&YS6fL0N7#i5i>D;TZ>VphyuF5N+jzjC8E~5f(xCu5W7E
zH7140YQ{Y?UOZ~~j|c_s)Y#(1QzLS!D~<8L<0GypQDx^QXSt8@843B2lJM5zJMB?v
zuG+ZYz$4O$|F4jMen-=vsq$&n=N5|Ize(+jQ2YKDRrsmSuvmSoTF5&R(H*_1i5fE(
zFW$N+6gnbC=S|(yG@53fXldF*FExV>3HP86ltj4y4oZ)Iu6<rXmwZNH`ear`sSNXh
zb!E|SG`jhw#g>JZfA>m|Ue^>wwfaTvEv=B<x~@GERcZdR`&-=$!%G!+s%}>W8@^u?
j<nLX(dkrF`UXB=RHjM|?j0Ymd#>c8AST3q!GPwT_cd%Y0

diff --git a/.gitignore b/.gitignore
index b845d407..790fe2ad 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,3 +10,4 @@ whisper_benches/logs
 # Lean build output and shrink.py scratch file
 /lean/.lake
 /lean/.shrink.bin
+__pycache__/

From 63604ded1168fd12d44bef21cb9ebad7732d0d79 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 14:08:13 +0000
Subject: [PATCH 15/29] CI fuzz: show the Lean toolchain and build steps in the
 job log

The toolchain step resolves lean/lean-toolchain through elan (which
downloads it when missing) and prints the versions; fuzz_ab.py reports
each lake and cargo build with its duration instead of only on failure.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/fuzz_ab.py | 4 +++-
 .github/workflows/ci.yml   | 6 +++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/.github/scripts/fuzz_ab.py b/.github/scripts/fuzz_ab.py
index 9f527f34..5c6856d9 100755
--- a/.github/scripts/fuzz_ab.py
+++ b/.github/scripts/fuzz_ab.py
@@ -26,7 +26,7 @@
       CARGO_TARGET_DIR   parent of the per-side target dirs      (default ./target)
       LAKE_CACHE         optional dir to keep lean's .lake build dirs across runs
 """
-import os, re, shutil, subprocess, sys
+import os, re, shutil, subprocess, sys, time
 from pathlib import Path
 
 FAIL_RE = re.compile(r'^FAIL (\S+) \[saved ([^\]]*)\]: (.*)$')
@@ -83,11 +83,13 @@ def build_side(self, side, src):
                                ('build', ['cargo', 'build', '--release', '-p', 'differential',
                                           '--target-dir', str(self.target / f'fuzz-{side}')], src)):
             logf = self.out / f'{name}-{side}.log'
+            t0 = time.time()
             with open(logf, 'w') as f:
                 p = subprocess.run(cmd, cwd=cwd, stdout=f, stderr=subprocess.STDOUT)
             if p.returncode:
                 log(f'{name} for {side} failed:\n{tail(logf)}')
                 return False
+            log(f'   {" ".join(cmd[:2])} for {side}: ok in {time.time() - t0:.0f}s (log: {logf.name})')
         return True
 
     def prepare_base(self):
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b4d7a875..091efe86 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -131,9 +131,13 @@ jobs:
         run: |
           rustup toolchain install stable --profile minimal
           rustup default stable
-          # elan reads lean/lean-toolchain and fetches the pinned Lean on first use
+          # elan (installed once per runner user) reads lean/lean-toolchain and fetches the pinned
+          # Lean when it is missing; resolving the version here makes that happen in this step
           [ -x "$HOME/.elan/bin/elan" ] || curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none --no-modify-path
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+          export PATH="$HOME/.elan/bin:$PATH"
+          elan --version
+          (cd lean && lean --version && lake --version)
       - name: resolve base
         id: base
         run: |

From 92d96190f696397f917bf8f2bc38bcca7936ac69 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 14:09:19 +0000
Subject: [PATCH 16/29] CI: provision rustup and elan per runner user when
 missing

A clean runner has neither.  Every job's toolchain step now installs
rustup into $HOME if absent and puts it on the PATH; the fuzz job does
the same for elan and resolves lean/lean-toolchain there, which fetches
the pinned Lean.  Verified from an empty home with a bare PATH: rustup,
stable Rust, elan and Lean 4.33.1 all arrive in about 20 seconds.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/workflows/ci.yml | 23 +++++++++++++++++------
 1 file changed, 17 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 091efe86..60402a5c 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -40,7 +40,11 @@ jobs:
     steps:
       - uses: actions/checkout@v5
       - name: toolchain
+        # rustup is installed per runner user on first use
         run: |
+          [ -x "$HOME/.cargo/bin/rustup" ] || curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal --default-toolchain none --no-modify-path
+          echo "$HOME/.cargo/bin" >> "$GITHUB_PATH"
+          export PATH="$HOME/.cargo/bin:$PATH"
           rustup toolchain install stable --profile minimal
           rustup default stable
           rustc --version && cargo --version
@@ -69,7 +73,11 @@ jobs:
         with:
           fetch-depth: 0
       - name: toolchain
+        # rustup is installed per runner user on first use
         run: |
+          [ -x "$HOME/.cargo/bin/rustup" ] || curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal --default-toolchain none --no-modify-path
+          echo "$HOME/.cargo/bin" >> "$GITHUB_PATH"
+          export PATH="$HOME/.cargo/bin:$PATH"
           rustup toolchain install stable --profile minimal
           rustup default stable
       - name: resolve base
@@ -128,16 +136,19 @@ jobs:
         with:
           fetch-depth: 0
       - name: toolchains
+        # Everything is installed per runner user on first use: rustup and elan into $HOME,
+        # then the Rust toolchain and the Lean pinned by lean/lean-toolchain.
         run: |
-          rustup toolchain install stable --profile minimal
-          rustup default stable
-          # elan (installed once per runner user) reads lean/lean-toolchain and fetches the pinned
-          # Lean when it is missing; resolving the version here makes that happen in this step
+          [ -x "$HOME/.cargo/bin/rustup" ] || curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal --default-toolchain none --no-modify-path
           [ -x "$HOME/.elan/bin/elan" ] || curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none --no-modify-path
+          export PATH="$HOME/.cargo/bin:$HOME/.elan/bin:$PATH"
+          echo "$HOME/.cargo/bin" >> "$GITHUB_PATH"
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-          export PATH="$HOME/.elan/bin:$PATH"
+          rustup toolchain install stable --profile minimal
+          rustup default stable
+          rustc --version && cargo --version
           elan --version
-          (cd lean && lean --version && lake --version)
+          (cd lean && lean --version && lake --version)   # fetches the pinned Lean when it is missing
       - name: resolve base
         id: base
         run: |

From 7def6e340cc3759a32ae78ac656e3ee7d45028c6 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 14:17:34 +0000
Subject: [PATCH 17/29] CI bench: run bench pairs in parallel, one per core

Each bench's base and head runs still share one core back to back, but
different benches run at the same time on different cores from
BENCH_CPUS (default: one SMT thread per physical core, every other core,
at most 16, which spreads them over the L3 complexes).  A round's wall
time is now that of its slowest bench pair rather than the sum.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/bench_ab.py | 76 +++++++++++++++++++++++++++----------
 1 file changed, 57 insertions(+), 19 deletions(-)

diff --git a/.github/scripts/bench_ab.py b/.github/scripts/bench_ab.py
index f917dffc..bfed60a2 100755
--- a/.github/scripts/bench_ab.py
+++ b/.github/scripts/bench_ab.py
@@ -2,9 +2,10 @@
 """A/B benchmark of two commits on the same machine.
 
 Builds the bench binaries for BASE and HEAD once each (separate target dirs),
-then runs them for ROUNDS rounds, alternating which side goes first and
-pinning every run to one core.  As soon as both sides of a bench have run in
-a round, its compare table (per-round divan medians averaged over the rounds
+then runs them for ROUNDS rounds.  Benches run in parallel, each on its own
+core from BENCH_CPUS (the base and head runs of a bench share that core, back
+to back, alternating which side goes first each round).  As soon as both
+sides of a bench have run in a round, its compare table (per-round divan medians averaged over the rounds
 finished so far, via benches/divan_fmt.py) is printed and saved as
 $BENCH_OUT/cmp-<bench>.txt; $BENCH_OUT/compare.txt, the concatenation, is
 rewritten after every completed round, as are $BENCH_OUT/summary.md (one row
@@ -16,13 +17,16 @@
 
 env:  BENCH_ROUNDS       rounds per side                (default 3)
       BENCHES            space separated bench targets  (default: the set used in BENCH_BUGFIXES)
-      BENCH_CPU          core to pin to                 (default 3)
+      BENCH_CPUS         cores to pin to, e.g. "0,2,4-8"; one bench pair runs per core at a time
+                         (default: one SMT thread per physical core, every other core, at most 16)
       BENCH_OUT          output directory               (default ./bench-out)
       DIVAN_SAMPLE_COUNT sample count for benches that do not set their own (default 40)
       CARGO_TARGET_DIR   parent of the two per-side target dirs (default ./target)
 """
-import json, math, os, re, statistics, subprocess, sys, time, tomllib
+import json, math, os, re, statistics, subprocess, sys, threading, time, tomllib
+from concurrent.futures import ThreadPoolExecutor
 from pathlib import Path
+from queue import Queue
 
 DEFAULT_BENCHES = 'shakespeare cities sparse_keys binary_keys superdense_keys act_paths zipper_head_owned product_zipper'
 THRESH = 0.05          # a case is listed in the summary when |change| exceeds this
@@ -36,13 +40,33 @@ def git(*args, cwd=None):
     return subprocess.run(['git', *args], cwd=cwd, check=True, text=True, capture_output=True).stdout.strip()
 
 
+def parse_cpus(spec):
+    cpus = []
+    for part in spec.replace(' ', '').split(','):
+        a, _, b = part.partition('-')
+        cpus += list(range(int(a), int(b or a) + 1))
+    return cpus
+
+
+def default_cpus(limit=16):
+    """One SMT thread per physical core, every other core (spreads over the L3 complexes), at most `limit`."""
+    cores = {}
+    for d in sorted(Path('/sys/devices/system/cpu').glob('cpu[0-9]*'), key=lambda d: int(d.name[3:])):
+        core = (d / 'topology' / 'core_id')
+        if core.is_file():
+            cores.setdefault(int(core.read_text()), int(d.name[3:]))
+    first = [cpu for _, cpu in sorted(cores.items())]
+    return (first[::2] or [0])[:limit]
+
+
 class Bench:
     def __init__(self, base, head):
         self.repo = Path.cwd()
         self.base_sha, self.head_sha = base, head
         self.rounds = int(os.environ.get('BENCH_ROUNDS', 3))
         self.benches = os.environ.get('BENCHES', DEFAULT_BENCHES).split()
-        self.cpu = os.environ.get('BENCH_CPU', '3')
+        self.cpus = parse_cpus(os.environ['BENCH_CPUS']) if os.environ.get('BENCH_CPUS') else default_cpus()
+        self.lock = threading.Lock()   # serialises log/progress output from the workers
         self.out = Path(os.environ.get('BENCH_OUT', self.repo / 'bench-out')).resolve()
         self.target = Path(os.environ.get('CARGO_TARGET_DIR', self.repo / 'target')).resolve()
         self.base_src = self.out / 'src-base'
@@ -54,7 +78,7 @@ def __init__(self, base, head):
         self.fmt = divan_fmt
 
     def progress(self, msg):
-        with open(self.out / 'progress.txt', 'a') as f:
+        with self.lock, open(self.out / 'progress.txt', 'a') as f:
             f.write(f'{time.strftime("%H:%M:%S", time.gmtime())} {msg}\n')
 
     def short(self, sha):
@@ -99,12 +123,24 @@ def build_side(self, side, src):
             sys.exit(f'no executable for bench(es) {missing} on {side}')
         self.bins[side] = exes
 
-    def run(self, side, bench, rnd):
+    def run(self, side, bench, rnd, cpu):
         t0 = time.time()
-        with open(self.out / f'{side}-{bench}-r{rnd}.txt', 'w') as out, open(self.out / f'run-{side}.log', 'a') as err:
-            subprocess.run(['taskset', '-c', self.cpu, self.bins[side][bench], '--bench'],
+        with open(self.out / f'{side}-{bench}-r{rnd}.txt', 'w') as out, open(self.out / f'run-{side}-{bench}.log', 'a') as err:
+            subprocess.run(['taskset', '-c', str(cpu), self.bins[side][bench], '--bench'],
                            cwd=self.repo, stdout=out, stderr=err, check=True)
-        self.progress(f'round {rnd}/{self.rounds} {bench} {side} {time.time() - t0:.0f}s')
+        self.progress(f'round {rnd}/{self.rounds} {bench} {side} {time.time() - t0:.0f}s cpu {cpu}')
+
+    def run_pair(self, bench, rnd, free):
+        """Both sides of one bench, back to back on one core taken from the pool, then its compare table."""
+        cpu = free.get()
+        try:
+            for side in (('base', 'head') if rnd % 2 else ('head', 'base')):
+                with self.lock:
+                    log(f'== round {rnd}/{self.rounds} {bench} {side} (cpu {cpu})')
+                self.run(side, bench, rnd, cpu)
+            self.compare_bench(bench, rnd)
+        finally:
+            free.put(cpu)
 
     def compare_bench(self, bench, rounds_so_far):
         """Average each side's rounds so far, compare medians, save and print the table."""
@@ -120,7 +156,8 @@ def compare_bench(self, bench, rounds_so_far):
         text = (f'{bench}  (base {self.short(self.base_sha)}  head {self.short(self.head_sha)}'
                 f'  rounds {rounds_so_far}  median ns)\n{table}\n\n')
         (self.out / f'cmp-{bench}.txt').write_text(text)
-        log(text, end='')
+        with self.lock:
+            log(text, end='')
 
     def compare_rounds(self, rounds_so_far):
         tmp = self.out / 'compare.tmp'
@@ -174,18 +211,19 @@ def main(self):
         self.cleanup()
         try:
             git('worktree', 'add', '--detach', str(self.base_src), self.base_sha, cwd=self.repo)
-            self.progress(f'plan: {self.rounds} round(s) x base/head x [{" ".join(self.benches)}], core {self.cpu}')
+            self.progress(f'plan: {self.rounds} round(s) x base/head x [{" ".join(self.benches)}], '
+                          f'{min(len(self.cpus), len(self.benches))} at a time on cpus {",".join(map(str, self.cpus))}')
             self.progress(f'building base {self.short(self.base_sha)}')
             self.build_side('base', self.base_src)
             self.progress(f'building head {self.short(self.head_sha)}')
             self.build_side('head', self.repo)
+            free = Queue()
+            for cpu in self.cpus:
+                free.put(cpu)
             for rnd in range(1, self.rounds + 1):
-                order = ('base', 'head') if rnd % 2 else ('head', 'base')
-                for bench in self.benches:
-                    for side in order:
-                        log(f'== round {rnd}/{self.rounds} {bench} {side}')
-                        self.run(side, bench, rnd)
-                    self.compare_bench(bench, rnd)
+                with ThreadPoolExecutor(min(len(self.cpus), len(self.benches))) as pool:
+                    for r in pool.map(lambda b: self.run_pair(b, rnd, free), self.benches):
+                        pass                     # re-raises a worker's exception
                 self.compare_rounds(rnd)
                 self.progress(f'round {rnd}/{self.rounds} done, compare.txt refreshed')
             log(f'== final compare over {self.rounds} round(s): {self.out / "compare.txt"}')

From 33f40a23eb505e970a19bb12a83265efbe2c94f2 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 14:32:51 +0000
Subject: [PATCH 18/29] CI bench: build both sides at the same path and target
 dir

An A/A run (same commit on both sides) reported 5-25% differences on
superdense_keys and binary_keys cases, consistent across rounds, with
the two sides pinned to the same core.  The sides were different
binaries: built at different paths into different target dirs, they got
different crate hashes and code layout.  Now one worktree is used for
both: check out base, build, copy the bench executables out; check out
head, build, copy out.  The historical bench run did the same and had a
round-to-round CV under 1% on those benches.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/bench_ab.py | 41 ++++++++++++++++++++++++-------------
 1 file changed, 27 insertions(+), 14 deletions(-)

diff --git a/.github/scripts/bench_ab.py b/.github/scripts/bench_ab.py
index bfed60a2..bf8f96a9 100755
--- a/.github/scripts/bench_ab.py
+++ b/.github/scripts/bench_ab.py
@@ -1,8 +1,12 @@
 #!/usr/bin/env python3
 """A/B benchmark of two commits on the same machine.
 
-Builds the bench binaries for BASE and HEAD once each (separate target dirs),
-then runs them for ROUNDS rounds.  Benches run in parallel, each on its own
+Builds the bench binaries for BASE and HEAD once each, both from the same
+worktree path and target dir (checkout base, build, copy the executables
+out; checkout head, build, copy out) so the two sides differ only in the
+change under test: building the sides at different paths or into different
+target dirs changes crate hashes and code layout, which alone moved cases by
+5-25% in an A/A run.  Then runs them for ROUNDS rounds.  Benches run in parallel, each on its own
 core from BENCH_CPUS (the base and head runs of a bench share that core, back
 to back, alternating which side goes first each round).  As soon as both
 sides of a bench have run in a round, its compare table (per-round divan medians averaged over the rounds
@@ -21,9 +25,9 @@
                          (default: one SMT thread per physical core, every other core, at most 16)
       BENCH_OUT          output directory               (default ./bench-out)
       DIVAN_SAMPLE_COUNT sample count for benches that do not set their own (default 40)
-      CARGO_TARGET_DIR   parent of the two per-side target dirs (default ./target)
+      CARGO_TARGET_DIR   parent of the shared bench target dir  (default ./target)
 """
-import json, math, os, re, statistics, subprocess, sys, threading, time, tomllib
+import json, math, os, re, shutil, statistics, subprocess, sys, threading, time, tomllib
 from concurrent.futures import ThreadPoolExecutor
 from pathlib import Path
 from queue import Queue
@@ -69,7 +73,7 @@ def __init__(self, base, head):
         self.lock = threading.Lock()   # serialises log/progress output from the workers
         self.out = Path(os.environ.get('BENCH_OUT', self.repo / 'bench-out')).resolve()
         self.target = Path(os.environ.get('CARGO_TARGET_DIR', self.repo / 'target')).resolve()
-        self.base_src = self.out / 'src-base'
+        self.src = self.out / 'src'          # one worktree for both sides
         self.bins = {}
         self.results = {}      # bench -> {'group/case': {'base': ns, 'head': ns, 'pct': float}}
         os.environ.setdefault('DIVAN_SAMPLE_COUNT', '40')
@@ -85,7 +89,7 @@ def short(self, sha):
         return git('rev-parse', '--short', sha, cwd=self.repo)
 
     def cleanup(self):
-        subprocess.run(['git', 'worktree', 'remove', '--force', str(self.base_src)], cwd=self.repo,
+        subprocess.run(['git', 'worktree', 'remove', '--force', str(self.src)], cwd=self.repo,
                        capture_output=True)
 
     def required_features(self, src):
@@ -98,10 +102,13 @@ def required_features(self, src):
                 need |= set(b.get('required-features', []))
         return sorted(need & have)
 
-    def build_side(self, side, src):
+    def build_side(self, side, sha):
+        """Check `sha` out in the shared worktree, build, and copy the bench executables to bins/<side>/."""
+        src = self.src
+        git('checkout', '--detach', '-f', sha, cwd=src)
         feats = self.required_features(src)
-        target = self.target / f'ab-{side}'
-        log(f'== building {side} ({self.short(git("rev-parse", "HEAD", cwd=src))}) into {target}'
+        target = self.target / 'ab'
+        log(f'== building {side} ({self.short(sha)}) in {src} into {target}'
             + (f' with features {",".join(feats)}' if feats else ''))
         cmd = ['cargo', 'bench', '--no-run', '--message-format=json', '--target-dir', str(target)]
         for b in self.benches:
@@ -117,11 +124,16 @@ def build_side(self, side, src):
             m = json.loads(line)
             if m.get('reason') == 'compiler-artifact' and m.get('executable') and 'bench' in m['target']['kind']:
                 exes[m['target']['name']] = m['executable']
-        (self.out / f'bins-{side}.txt').write_text(''.join(f'{k} {v}\n' for k, v in exes.items()))
         missing = [b for b in self.benches if b not in exes]
         if missing:
             sys.exit(f'no executable for bench(es) {missing} on {side}')
-        self.bins[side] = exes
+        bindir = self.out / 'bins' / side
+        bindir.mkdir(parents=True, exist_ok=True)
+        self.bins[side] = {}
+        for b in self.benches:
+            shutil.copy2(exes[b], bindir / b)
+            self.bins[side][b] = str(bindir / b)
+        (self.out / f'bins-{side}.txt').write_text(''.join(f'{b} {exes[b]}\n' for b in self.benches))
 
     def run(self, side, bench, rnd, cpu):
         t0 = time.time()
@@ -209,14 +221,15 @@ def main(self):
             if f.suffix in ('.txt', '.log', '.json'):
                 f.unlink()
         self.cleanup()
+        shutil.rmtree(self.out / 'bins', ignore_errors=True)
         try:
-            git('worktree', 'add', '--detach', str(self.base_src), self.base_sha, cwd=self.repo)
+            git('worktree', 'add', '--detach', str(self.src), self.base_sha, cwd=self.repo)
             self.progress(f'plan: {self.rounds} round(s) x base/head x [{" ".join(self.benches)}], '
                           f'{min(len(self.cpus), len(self.benches))} at a time on cpus {",".join(map(str, self.cpus))}')
             self.progress(f'building base {self.short(self.base_sha)}')
-            self.build_side('base', self.base_src)
+            self.build_side('base', self.base_sha)
             self.progress(f'building head {self.short(self.head_sha)}')
-            self.build_side('head', self.repo)
+            self.build_side('head', self.head_sha)
             free = Queue()
             for cpu in self.cpus:
                 free.put(cpu)

From 04d1d1e98d62006c64886c925034ff1e29c8ad98 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 15:21:30 +0000
Subject: [PATCH 19/29] CI: Lean job that builds the model and checks its
 proofs and guards

`lake build` type-checks the theorems in Spec.lean and evaluates every
#guard in Check.lean, so a broken law or regression fixture fails the
job.  Lean only warns on sorry, so the job greps the build log and the
model sources for it (and for axioms) separately.  Lake's build dir is
kept in the runner's cache; a warm run takes seconds.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/workflows/ci.yml | 49 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 60402a5c..d09625b8 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -122,6 +122,55 @@ jobs:
             ${{ runner.temp }}/bench-out/summary.*
           if-no-files-found: ignore
 
+  lean:
+    name: Lean model, proofs and checks
+    # `lake build` type-checks the theorems in lean/PathMapModel/Spec.lean and evaluates every
+    # `#guard` (the metamorphic laws over the fixture battery and the regression fixtures), so
+    # a broken law or fixture fails the build.  Lean only warns on `sorry`, so that is checked
+    # for separately.
+    runs-on: [self-hosted, linux, x64]
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@v5
+      - name: toolchain
+        # elan is installed per runner user on first use and fetches the Lean pinned by lean/lean-toolchain
+        run: |
+          [ -x "$HOME/.elan/bin/elan" ] || curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none --no-modify-path
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+          export PATH="$HOME/.elan/bin:$PATH"
+          (cd lean && lean --version && lake --version)
+      - name: build the model, check proofs and guards
+        run: |
+          # checkout wipes ignored files, so keep lake's build dir in the persistent cache
+          mkdir -p /home/gh-runner/cache/lean-lake/proofs
+          ln -sfn /home/gh-runner/cache/lean-lake/proofs lean/.lake
+          cd lean
+          lake build 2>&1 | tee ../lake.log
+          test "${PIPESTATUS[0]}" -eq 0
+      - name: no sorry, no unexpected axioms
+        run: |
+          if grep -n 'declaration uses .sorry.' lake.log; then
+            echo "::error::a declaration uses sorry"; exit 1
+          fi
+          if grep -rn "\bsorry\b\|^axiom " lean/PathMapModel lean/Main.lean; then
+            echo "::error::sorry or axiom in the model sources"; exit 1
+          fi
+      - name: summary
+        if: always()
+        run: |
+          {
+            echo "### Lean model"
+            echo
+            echo "| file | theorems | guards |"
+            echo "|---|---:|---:|"
+            for f in lean/PathMapModel/*.lean; do
+              t=$(grep -c '^theorem\|^lemma' "$f" || true); g=$(grep -c '#guard' "$f" || true)
+              [ "$t$g" = "00" ] || echo "| $(basename "$f") | $t | $g |"
+            done
+            echo
+            echo "$(grep -c 'declaration uses' lake.log || true) declaration(s) use sorry; $(grep -c '^warning' lake.log || true) warning(s) from lake build."
+          } >> "$GITHUB_STEP_SUMMARY"
+
   fuzz:
     name: differential fuzz vs Lean model
     # Regression check: head and base run on identical inputs; an input on which head diverges

From 9b0fbad019e0404951600660d3d78ec319354013 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 15:40:49 +0000
Subject: [PATCH 20/29] CI fuzz: post its own PR comment with new failure modes
 and reproducers

pr_comment.py takes --id / --title / --dir so each job owns one comment
per PR (bench keeps its marker and defaults).  The fuzz job posts its
summary after every run: verdict, per-mode tables, the inputs that
diverge on head but not on base, and the shrunk Rust reproducers in
collapsed blocks.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/pr_comment.py | 39 ++++++++++++++++++++++-------------
 .github/workflows/ci.yml      | 14 +++++++++++++
 2 files changed, 39 insertions(+), 14 deletions(-)

diff --git a/.github/scripts/pr_comment.py b/.github/scripts/pr_comment.py
index 098ca7e5..9817737e 100755
--- a/.github/scripts/pr_comment.py
+++ b/.github/scripts/pr_comment.py
@@ -1,26 +1,35 @@
 #!/usr/bin/env python3
-"""Create or update the single bench comment on a pull request.
+"""Create or update one job's comment on a pull request.
 
-One comment per pull request, edited in place: a status line, a link to the
-job that produced it, and bench_ab.py's summary.md once it exists.  The
-first call of a run finds the PR's existing bench comment by the hidden marker
-on its first line (so a re-run or a new push reuses it) or creates it, and
-records the id in $BENCH_OUT/comment_id; later calls in the same run go
-straight to that id.  Standard library only.
+One comment per pull request and job id, edited in place: a title with a
+status, a link to the job that produced it, and the job's summary.md once it
+exists.  The first call of a run finds the PR's existing comment by the hidden
+marker on its first line (so a re-run or a new push reuses it) or creates it,
+and records the id in <dir>/comment_id; later calls in the same run go straight
+to that id.  Standard library only.
 
-usage: pr_comment.py <pr-number> <status text>
+usage: pr_comment.py [--id ID] [--title TITLE] [--dir DIR] <pr-number> <status text>
+       --id     comment identity, one per job          (default bench-ab)
+       --title  heading before the status              (default "Bench A/B vs base")
+       --dir    dir holding summary.md, comment_id     (default $BENCH_OUT)
 env:   GITHUB_TOKEN GITHUB_REPOSITORY GITHUB_RUN_ID RUNNER_NAME   (provided by Actions)
-       BENCH_OUT                        dir holding summary.md from bench_ab.py
        GITHUB_SERVER_URL                optional
 """
-import json, os, sys, time, urllib.request
+import argparse, json, os, sys, time, urllib.request
 from pathlib import Path
 
-MARKER = '<!-- pathmap-bench-ab -->'
 LIMIT = 65536            # GitHub's comment body cap
 
-pr, status = sys.argv[1], sys.argv[2] if len(sys.argv) > 2 else ''
-out = Path(os.environ['BENCH_OUT'])
+ap = argparse.ArgumentParser()
+ap.add_argument('--id', default='bench-ab')
+ap.add_argument('--title', default='Bench A/B vs base')
+ap.add_argument('--dir', default=os.environ.get('BENCH_OUT'))
+ap.add_argument('pr')
+ap.add_argument('status', nargs='?', default='')
+args = ap.parse_args()
+pr, status = args.pr, args.status
+MARKER = f'<!-- pathmap-{args.id} -->'
+out = Path(args.dir)
 repo = os.environ['GITHUB_REPOSITORY']
 api = f'https://api.github.com/repos/{repo}'
 headers = {'Authorization': f"Bearer {os.environ['GITHUB_TOKEN']}",
@@ -58,9 +67,11 @@ def job_url():
     return url
 
 
-parts = [MARKER, f'### Bench A/B vs base: {status}', '',
+parts = [MARKER, f'### {args.title}: {status}', '',
          f"[job log]({job_url()}) · {time.strftime('%Y-%m-%d %H:%M:%S', time.gmtime())} UTC"]
 summary = read('summary.md')
+if summary.startswith('# '):                 # the comment has its own heading
+    summary = summary.split('\n', 1)[1].lstrip('\n') if '\n' in summary else ''
 if summary:
     head = '\n'.join(parts)
     room = LIMIT - len(head) - 200
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index d09625b8..081788fd 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -180,6 +180,9 @@ jobs:
     if: github.event_name == 'pull_request' || github.event_name == 'workflow_dispatch'
     runs-on: [self-hosted, linux, x64]
     timeout-minutes: 90
+    permissions:
+      contents: read
+      pull-requests: write   # for the fuzz comment; read-only on fork PRs, where commenting is skipped
     steps:
       - uses: actions/checkout@v5
         with:
@@ -208,12 +211,23 @@ jobs:
           fi
           echo "sha=$sha" >> "$GITHUB_OUTPUT"
       - name: fuzz head and base
+        id: fuzz
         env:
           FUZZ_INPUTS: ${{ inputs.fuzz_inputs || '20000' }}
           FUZZ_OUT: ${{ runner.temp }}/fuzz-out
           LAKE_CACHE: /home/gh-runner/cache/lean-lake   # checkout wipes ignored files such as lean/.lake
         run: |
           .github/scripts/fuzz_ab.py "${{ steps.base.outputs.sha }}" "${{ github.sha }}"
+      - name: comment on the PR
+        # One comment per PR for this job (separate from the bench one): verdict, per-mode tables,
+        # newly diverging inputs and their shrunk Rust reproducers.  Skipped when there is no PR;
+        # fails silently on fork PRs, whose token is read-only.
+        if: always() && github.event.pull_request.number
+        env:
+          GITHUB_TOKEN: ${{ github.token }}
+        run: |
+          python3 .github/scripts/pr_comment.py --id fuzz --title "Differential fuzz vs Lean model" \
+            --dir "${{ runner.temp }}/fuzz-out" "${{ github.event.pull_request.number }}" "${{ steps.fuzz.outcome }}" || true
       - name: summary
         if: always()
         run: |

From 4556c84c987c0626067f7db3bea4919655dd6c52 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 15:48:13 +0000
Subject: [PATCH 21/29] CI: run the fuzz job even when the tests fail

Its findings are warnings, and a PR with failing tests is one whose
divergences are worth seeing.  The bench job still needs both to pass.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/workflows/ci.yml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 081788fd..6f3fc2f0 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -176,8 +176,10 @@ jobs:
     # Regression check: head and base run on identical inputs; an input on which head diverges
     # from the model but base did not is reported as a warning annotation (master has known
     # divergences).  Set FUZZ_STRICT=1 below to make that fail the job instead.
+    # Ordered after the tests but not gated on them: findings are warnings, and a PR whose
+    # tests fail is exactly one whose divergences are worth seeing.
     needs: test
-    if: github.event_name == 'pull_request' || github.event_name == 'workflow_dispatch'
+    if: ${{ !cancelled() && (github.event_name == 'pull_request' || github.event_name == 'workflow_dispatch') }}
     runs-on: [self-hosted, linux, x64]
     timeout-minutes: 90
     permissions:

From a65e8a23d4d737d6e0e7c2f305ff3fe933ac43b3 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 15:51:21 +0000
Subject: [PATCH 22/29] CI fuzz: list new divergences by kind, at most 10 lines

One row per first-differing operation (or final-state mismatch) with
the input count and a first example, instead of up to 50 inputs.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/fuzz_ab.py | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/.github/scripts/fuzz_ab.py b/.github/scripts/fuzz_ab.py
index 5c6856d9..d901aec7 100755
--- a/.github/scripts/fuzz_ab.py
+++ b/.github/scripts/fuzz_ab.py
@@ -144,6 +144,8 @@ def kind(f):
         for d in f['detail']:
             if d.startswith('lean:'):
                 parts = d.split()
+                if len(parts) > 1 and parts[1].startswith(('MAP', 'ROOT')):
+                    return f'{parts[1]} (final state)'
                 if len(parts) > 2:
                     return parts[2]
         return re.sub(r'\d+', 'N', f['msg'])
@@ -205,17 +207,16 @@ def summarize(self, baseline):
                     new_total += len(new)
                     log(f'::{"error" if self.strict else "warning"} title=Differential fuzz ({label})::{len(new)} input(s) diverge from the model on head '
                         f'but not on base, e.g. {new[0]}: {hf[new[0]]["msg"][:150]}')
-                    L += ['', '### Newly diverging inputs (head only)', '']
-                    L += [f'- `{name}`: {hf[name]["msg"][:200]} ({self.kind(hf[name])})' for name in new[:50]]
-                    if len(new) > 50:
-                        L.append(f'- … and {len(new) - 50} more, see fuzz-{label}-head.txt')
-                    picked, seen = [], set()
+                    kinds = {}                                # first-differing op -> [input names], input order
                     for name in new:
-                        k = self.kind(hf[name])
-                        if k not in seen:
-                            seen.add(k); picked.append(name)
-                        if len(picked) >= self.repros:
-                            break
+                        kinds.setdefault(self.kind(hf[name]), []).append(name)
+                    L += ['', f'### Newly diverging inputs (head only): {len(new)} input(s), {len(kinds)} kind(s)', '',
+                          '| first differs at | inputs | first example |', '|---|---:|---|']
+                    for k, names in list(kinds.items())[:10]:
+                        L.append(f'| `{k}` | {len(names)} | `{names[0]}`: {hf[names[0]]["msg"][:80]} |')
+                    if len(kinds) > 10:
+                        L.append(f'| … {len(kinds) - 10} more kind(s) | | see fuzz-{label}-head.txt |')
+                    picked = [names[0] for names in kinds.values()][:self.repros]
                     if picked:
                         flags = next(fl for lb, _, fl in self.modes if lb == label)
                         L += ['', f'### Reproducers: first {len(picked)} distinct kind(s), shrunk', '']

From b8ee5861d0ebc1722a3140304543cd615072d713 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 15:57:54 +0000
Subject: [PATCH 23/29] CI fuzz: post the PR comment only when there is
 something to report

fuzz_ab.py writes a findings file when head has new divergences or a
run did not finish; pr_comment.py --create-only-if creates the comment
only then.  An existing comment is still updated by a clean run, so it
does not keep showing stale findings.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/fuzz_ab.py    | 4 ++++
 .github/scripts/pr_comment.py | 6 ++++++
 .github/workflows/ci.yml      | 8 +++++---
 3 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/.github/scripts/fuzz_ab.py b/.github/scripts/fuzz_ab.py
index d901aec7..622040a1 100755
--- a/.github/scripts/fuzz_ab.py
+++ b/.github/scripts/fuzz_ab.py
@@ -234,6 +234,10 @@ def summarize(self, baseline):
             L[2] = '**OK: no new divergences relative to base**'
         text = '\n'.join(L) + '\n'
         (self.out / 'summary.md').write_text(text)
+        findings = self.out / 'findings'                  # exists only when there is something to report
+        findings.unlink(missing_ok=True)
+        if new_total or unfinished:
+            findings.write_text(f'{new_total} new divergences, {unfinished} unfinished runs\n')
         log(text, end='')
         return new_total, unfinished
 
diff --git a/.github/scripts/pr_comment.py b/.github/scripts/pr_comment.py
index 9817737e..5b685dbb 100755
--- a/.github/scripts/pr_comment.py
+++ b/.github/scripts/pr_comment.py
@@ -12,6 +12,8 @@
        --id     comment identity, one per job          (default bench-ab)
        --title  heading before the status              (default "Bench A/B vs base")
        --dir    dir holding summary.md, comment_id     (default $BENCH_OUT)
+       --create-only-if FILE  create the comment only when FILE exists; an existing comment is
+                              always updated (so a clean run clears earlier findings)
 env:   GITHUB_TOKEN GITHUB_REPOSITORY GITHUB_RUN_ID RUNNER_NAME   (provided by Actions)
        GITHUB_SERVER_URL                optional
 """
@@ -24,6 +26,7 @@
 ap.add_argument('--id', default='bench-ab')
 ap.add_argument('--title', default='Bench A/B vs base')
 ap.add_argument('--dir', default=os.environ.get('BENCH_OUT'))
+ap.add_argument('--create-only-if')
 ap.add_argument('pr')
 ap.add_argument('status', nargs='?', default='')
 args = ap.parse_args()
@@ -88,6 +91,9 @@ def job_url():
     found = [c['id'] for c in call('GET', f'{api}/issues/{pr}/comments?per_page=100') if c['body'].startswith(MARKER)]
     cid = found[0] if found else None
     how = 'reused' if found else 'created'
+if cid is None and args.create_only_if and not Path(args.create_only_if).exists():
+    print(f'no comment yet and {args.create_only_if} is absent: nothing to report')
+    sys.exit(0)
 if cid is None:
     cid = call('POST', f'{api}/issues/{pr}/comments', {'body': body})['id']
 else:
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 6f3fc2f0..7c04aae5 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -222,14 +222,16 @@ jobs:
           .github/scripts/fuzz_ab.py "${{ steps.base.outputs.sha }}" "${{ github.sha }}"
       - name: comment on the PR
         # One comment per PR for this job (separate from the bench one): verdict, per-mode tables,
-        # newly diverging inputs and their shrunk Rust reproducers.  Skipped when there is no PR;
-        # fails silently on fork PRs, whose token is read-only.
+        # newly diverging inputs and their shrunk Rust reproducers.  Created only when there is
+        # something to report; an existing comment is updated by a clean run.  Skipped when there
+        # is no PR; fails silently on fork PRs, whose token is read-only.
         if: always() && github.event.pull_request.number
         env:
           GITHUB_TOKEN: ${{ github.token }}
         run: |
           python3 .github/scripts/pr_comment.py --id fuzz --title "Differential fuzz vs Lean model" \
-            --dir "${{ runner.temp }}/fuzz-out" "${{ github.event.pull_request.number }}" "${{ steps.fuzz.outcome }}" || true
+            --dir "${{ runner.temp }}/fuzz-out" --create-only-if "${{ runner.temp }}/fuzz-out/findings" \
+            "${{ github.event.pull_request.number }}" "${{ steps.fuzz.outcome }}" || true
       - name: summary
         if: always()
         run: |

From 09d5aa5643b3f4e29184bb300ebac0c2bd23e1e1 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Wed, 9 Sep 2026 16:15:14 +0000
Subject: [PATCH 24/29] CI fuzz: explain the columns and show known-class
 counts that changed

The comparison diffs only the unclassified divergences, so inputs that
moved between the known-bug bucket and agreement were invisible: a base
with 826 known hits and a head with 221 showed 44 new on both sides and
nothing fixed.  The summary now has a legend and a table of known
classes whose hit counts differ between base and head.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
---
 .github/scripts/fuzz_ab.py | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

diff --git a/.github/scripts/fuzz_ab.py b/.github/scripts/fuzz_ab.py
index 622040a1..a867fbf1 100755
--- a/.github/scripts/fuzz_ab.py
+++ b/.github/scripts/fuzz_ab.py
@@ -31,6 +31,7 @@
 
 FAIL_RE = re.compile(r'^FAIL (\S+) \[saved ([^\]]*)\]: (.*)$')
 SUMMARY_RE = re.compile(r'^(\d+)/(\d+) inputs agree \((\d+) hit known bugs, (\d+) new divergences\)')
+KNOWN_RE = re.compile(r'^  known x(\d+): (.*)$')
 
 
 def log(*a, **kw):
@@ -123,8 +124,8 @@ def run_side(self, side, src, label, n, flags):
         log('\n'.join(info) if info else tail(outf, 5))
 
     def parse(self, label, side):
-        """fails: name -> {'path', 'msg', 'detail'}; summary: (agree, total, known, new)."""
-        fails, summary, last = {}, None, None
+        """fails: name -> {'path', 'msg', 'detail'}; summary: (agree, total, known, new); known: class -> count."""
+        fails, summary, last, known = {}, None, None, {}
         p = self.out / f'fuzz-{label}-{side}.txt'
         if p.is_file():
             for line in p.read_text().splitlines():
@@ -136,7 +137,9 @@ def parse(self, label, side):
                     last = None
                 if m := SUMMARY_RE.match(line):
                     summary = tuple(map(int, m.groups()))
-        return fails, summary
+                if m := KNOWN_RE.match(line):
+                    known[m.group(2)] = int(m.group(1))
+        return fails, summary, known
 
     @staticmethod
     def kind(f):
@@ -189,9 +192,11 @@ def summarize(self, baseline):
                   'so harness changes may show up as differences.', '']
         new_total, unfinished = 0, 0
         for label, n, _ in self.modes:
-            hf, hs = self.parse(label, 'head')
-            bf, bs = self.parse(label, 'base')
+            hf, hs, hk = self.parse(label, 'head')
+            bf, bs, bk = self.parse(label, 'base')
             L += [f'## {label}: {n} inputs, seed {self.seed}', '',
+                  'agree = model and crate match; known = the divergence matches a classified bug in '
+                  'differential.py; new = it matches none.  Only the new set is compared input by input below.', '',
                   '| side | agree | known | new divergences |', '|---|---:|---:|---:|']
             for side, s in (('head', hs), ('base', bs)):
                 if s:
@@ -203,6 +208,13 @@ def summarize(self, baseline):
                 new = sorted(set(hf) - set(bf))          # names are random#NNNNN, so this is input order
                 fixed = sorted(set(bf) - set(hf))
                 L += ['', f'{len(new)} input(s) diverge on head but not on base; {len(fixed)} diverge on base but not on head.']
+                changed = sorted(((bk.get(k, 0), hk.get(k, 0), k) for k in set(bk) | set(hk) if bk.get(k, 0) != hk.get(k, 0)),
+                                 key=lambda t: -abs(t[0] - t[1]))
+                if changed:
+                    L += ['', '### Known-class hits that changed', '', '| known class | base | head |', '|---|---:|---:|']
+                    L += [f'| {k[:100]} | {b} | {h} |' for b, h, k in changed[:10]]
+                    if len(changed) > 10:
+                        L.append(f'| … {len(changed) - 10} more | | |')
                 if new:
                     new_total += len(new)
                     log(f'::{"error" if self.strict else "warning"} title=Differential fuzz ({label})::{len(new)} input(s) diverge from the model on head '

From 5ec50ce832ea7750f57d5bb08774783cceea761c Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Tue, 15 Sep 2026 22:51:53 +0000
Subject: [PATCH 25/29] Fuzz: count agreement over the inputs that actually ran

differential.py derived the agreement count by subtracting from the
requested input count, so when --max-fails stopped the run early every
input that was never executed was scored as agreeing.  The error grows
with the number of divergences, which is backwards: over 3000 inputs at
seed 7, --max-fails 3 classified 846 inputs and reported 2987/3000
agree -- more than the 2959/3000 an exhaustive run finds over the same
set.  --max-fails defaults to 10, so hand-run invocations were all
affected; fuzz_ab.py passes --max-fails 0 and was exact.

Count the inputs actually classified and report against that, naming
the shortfall on a line of its own so the summary line's format, which
fuzz_ab.py parses with SUMMARY_RE, is unchanged.

A denominator below the requested count now counts as an unfinished run
in fuzz_ab.py, which fails the job.  A truncated run previously still
printed a summary line and passed as OK, even though the two sides stop
after their own scheduling-dependent prefix of the inputs: comparing
failure sets drawn from different input populations is not a gate.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 .github/scripts/fuzz_ab.py | 10 ++++++++--
 lean/differential.py       | 11 +++++++++--
 2 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/.github/scripts/fuzz_ab.py b/.github/scripts/fuzz_ab.py
index a867fbf1..25dedaa8 100755
--- a/.github/scripts/fuzz_ab.py
+++ b/.github/scripts/fuzz_ab.py
@@ -199,7 +199,13 @@ def summarize(self, baseline):
                   'differential.py; new = it matches none.  Only the new set is compared input by input below.', '',
                   '| side | agree | known | new divergences |', '|---|---:|---:|---:|']
             for side, s in (('head', hs), ('base', bs)):
-                if s:
+                if s and s[1] < n:
+                    # differential.py reports against the inputs it actually ran, so a denominator
+                    # below the requested count means the run stopped early (--max-fails).  The two
+                    # sides then covered different inputs and the comparison below is not a gate.
+                    L.append(f'| {side} | {s[0]}/{s[1]} — **stopped early, {n - s[1]} input(s) not run** | {s[2]} | {s[3]} |')
+                    unfinished += 1
+                elif s:
                     L.append(f'| {side} | {s[0]}/{s[1]} | {s[2]} | {s[3]} |')
                 elif side == 'head' or baseline != 'none':
                     L.append(f'| {side} | run did not finish, see fuzz-{label}-{side}.txt | | |')
@@ -239,7 +245,7 @@ def summarize(self, baseline):
                     L += ['', '</details>']
             L.append('')
         if unfinished:
-            L[2] = '**FAIL: a fuzz run did not finish**'
+            L[2] = '**FAIL: a fuzz run did not cover every input**'
         elif new_total:
             L[2] = f'**{"FAIL" if self.strict else "WARNING"}: {new_total} new divergence(s) relative to base**'
         else:
diff --git a/lean/differential.py b/lean/differential.py
index a7129a72..ef6d658d 100755
--- a/lean/differential.py
+++ b/lean/differential.py
@@ -505,12 +505,14 @@ def save(idx):
 
     fails = 0
     known = {}
+    done = 0              # inputs actually classified; < n_inputs when --max-fails stops the run
     restarts = 0
     reports = []          # (idx, name, msg) for failures, so -j output is ordered
 
     def record(idx, msg):
         """Classify one result.  Returns True when the run should stop."""
-        nonlocal fails
+        nonlocal fails, done
+        done += 1
         name = source.name(idx)
         if not msg:
             if args.verbose:
@@ -567,8 +569,13 @@ def record(idx, msg):
     if restarts:
         print("(%d child restart(s) after a timeout or crash)" % restarts)
     hit = sum(known.values())
+    # Against `done`, not `n_inputs`: when --max-fails stops the run the remaining
+    # inputs were never executed, and counting them in the denominator would score
+    # every one of them as agreeing.
     print("%d/%d inputs agree (%d hit known bugs, %d new divergences)"
-          % (n_inputs - fails - hit, n_inputs, hit, fails))
+          % (done - fails - hit, done, hit, fails))
+    if done < n_inputs:
+        print("(%d of %d inputs were not run)" % (n_inputs - done, n_inputs))
     for note, n in sorted(known.items()):
         print("  known x%d: %s" % (n, note))
     return 1 if fails else 0

From 19908883d91a2583f6f81c6dec7bd5a0945da4f6 Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Tue, 15 Sep 2026 23:10:29 +0000
Subject: [PATCH 26/29] Fuzz: name the reason an operation was skipped

Every skip rendered as a bare `skip`, so a trace said that something
declined the operation but not what: the ACT read source refusing to be
a merge source, a degenerate `k = 0`, an empty focus and a quarantined
op were all the same token.  Each site now emits `skip:<reason>` from a
vocabulary defined once on each side -- `SKIP_*` in harness.rs, `skip*`
in Fuzz.lean -- and the two must agree exactly, since a token that
differs makes every input that skips diverge.

Naming them turned up an ordering bug the bare token had hidden.  For
`restricting` the model tested ACT mode first and the harness tested the
empty focus first, so in ACT mode with an empty focus the two took
different branches and agreed only because both printed `skip`.  The
model now checks the guards in the harness's order; the harness reaches
its ACT skip only by calling `do_restricting`, which it does not do once
the empty-focus guard has fired, so that is the order that can be
matched.  `meet_k_path_into` splits `meetKPathUnspecified` into its two
disjuncts on both sides for the same reason.

Behaviour is otherwise unchanged: 20000 crate inputs and 5000 ACT inputs
at seed 7 give the same agree, known and new counts as before.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 differential/src/harness.rs |  70 +++++++++++++++++-------
 lean/PathMapModel/Fuzz.lean | 103 ++++++++++++++++++++++++------------
 lean/README.md              |  36 ++++++++-----
 3 files changed, 143 insertions(+), 66 deletions(-)

diff --git a/differential/src/harness.rs b/differential/src/harness.rs
index bb168798..0b0d72d9 100644
--- a/differential/src/harness.rs
+++ b/differential/src/harness.rs
@@ -82,10 +82,13 @@ pub fn show_val(v: Option<&u64>) -> String {
 }
 
 /// Render a status the read source may have declined to produce.
+///
+/// Only the default `ReadSource` impls return `None`, and only the ACT zipper
+/// uses them, so the reason is always ACT mode.  See `SKIP_REASONS`.
 pub fn show_status_opt(s: Option<AlgebraicStatus>) -> String {
     match s {
         Some(s) => show_status(s).to_string(),
-        None => "skip".to_string(),
+        None => SKIP_ACT.to_string(),
     }
 }
 
@@ -134,6 +137,33 @@ pub fn fingerprint<Z: ZipperMoving + ZipperPath + ZipperValues<u64> + ZipperAbso
     )
 }
 
+/// Why an operation was skipped.  Every `skip` in the trace carries one of
+/// these, so a skipped op says which rule declined it rather than just that
+/// something declined it.  `lean/PathMapModel/Fuzz.lean` emits the same
+/// tokens; the two must agree exactly or every input with a skip diverges.
+///
+/// * `skip:act` — the ACT read source cannot be a merge source
+///   (`ZipperInfallibleSubtries` is not implemented for it) or does not
+///   implement the trait the op needs.
+/// * `skip:at-root` — `to_next`/`to_prev_sibling_byte` at the zipper root,
+///   where the native read zipper escapes its own root.
+/// * `skip:k0` — a degenerate `k = 0`.
+/// * `skip:empty-focus` — the focus has nothing below it, where the op's
+///   behaviour is a function of node materialisation rather than trie state.
+/// * `skip:empty-path` — `insert_prefix("")`, which destroys the subtrie.
+/// * `skip:off-root-prune` — a prune on a write zipper not rooted at the map
+///   root, where the depth pruned is a function of internal node layout.
+/// * `skip:quarantined` — the op is disabled outright (op 54).
+///
+/// Each is recorded in lean/FINDINGS.md and commented at its site.
+pub const SKIP_ACT: &str = "skip:act";
+pub const SKIP_AT_ROOT: &str = "skip:at-root";
+pub const SKIP_K0: &str = "skip:k0";
+pub const SKIP_EMPTY_FOCUS: &str = "skip:empty-focus";
+pub const SKIP_EMPTY_PATH: &str = "skip:empty-path";
+pub const SKIP_OFF_ROOT_PRUNE: &str = "skip:off-root-prune";
+pub const SKIP_QUARANTINED: &str = "skip:quarantined";
+
 /// Does the focus have no descendants at all?
 ///
 /// Several return values (`remove_branches`, `restricting`, `join_map_into`,
@@ -523,7 +553,7 @@ pub fn run_ops<R: ReadSource>(
                     // Skipped at the zipper root: the native ReadZipper escapes
                     // its own root there. See `Zip.toNextSiblingByte`.
                     if tgt!(t, wz, *rz, z, z.at_root()) {
-                        ("to_next_sibling_byte", "skip".to_string())
+                        ("to_next_sibling_byte", SKIP_AT_ROOT.to_string())
                     } else {
                         let r = tgt!(t, wz, *rz, z, z.to_next_sibling_byte());
                         ("to_next_sibling_byte", show_byte_opt(r))
@@ -532,7 +562,7 @@ pub fn run_ops<R: ReadSource>(
                 12 => {
                     let t = get!(d.modn(2));
                     if tgt!(t, wz, *rz, z, z.at_root()) {
-                        ("to_prev_sibling_byte", "skip".to_string())
+                        ("to_prev_sibling_byte", SKIP_AT_ROOT.to_string())
                     } else {
                         let r = tgt!(t, wz, *rz, z, z.to_prev_sibling_byte());
                         ("to_prev_sibling_byte", show_byte_opt(r))
@@ -555,7 +585,7 @@ pub fn run_ops<R: ReadSource>(
                     let k = get!(d.modn(4));
                     // k == 0 is degenerate; see Fuzz.lean.
                     if k == 0 {
-                        ("descend_first_k_path", "skip".to_string())
+                        ("descend_first_k_path", SKIP_K0.to_string())
                     } else {
                         let r = (*rz).descend_first_k_path(k);
                         ("descend_first_k_path", show_bool(r).to_string())
@@ -570,7 +600,7 @@ pub fn run_ops<R: ReadSource>(
                     let mut v: Vec<String> = Vec::new();
                     if k == 0 {
                         let _ = writeln!(out, 
-                            "{step} k_path_walk ret=skip W={} R={}",
+                            "{step} k_path_walk ret={SKIP_K0} W={} R={}",
                             fingerprint(&wz, root0), fingerprint(rz, root1));
                         step += 1;
                         continue;
@@ -639,7 +669,7 @@ pub fn run_ops<R: ReadSource>(
                     };
                     match n {
                         Some(n) => ("make_map_val_count", format!("{n}")),
-                        None => ("make_map_val_count", "skip".to_string()),
+                        None => ("make_map_val_count", SKIP_ACT.to_string()),
                     }
                 }
                 26 => {
@@ -664,14 +694,14 @@ pub fn run_ops<R: ReadSource>(
                     if pruneable {
                         ("prune_path", format!("{}", wz.prune_path()))
                     } else {
-                        ("prune_path", "skip".to_string())
+                        ("prune_path", SKIP_OFF_ROOT_PRUNE.to_string())
                     }
                 }
                 31 => {
                     if pruneable {
                         ("prune_ascend", format!("{}", wz.prune_ascend()))
                     } else {
-                        ("prune_ascend", "skip".to_string())
+                        ("prune_ascend", SKIP_OFF_ROOT_PRUNE.to_string())
                     }
                 }
                 32 => {
@@ -693,7 +723,7 @@ pub fn run_ops<R: ReadSource>(
                     ("remove_unmasked_branches", hex_path(&canon))
                 }
                 34 => {
-                    let s = if (*rz).do_graft(&mut wz) { "-" } else { "skip" };
+                    let s = if (*rz).do_graft(&mut wz) { "-" } else { SKIP_ACT };
                     ("graft", s.to_string())
                 }
                 35 => {
@@ -701,7 +731,7 @@ pub fn run_ops<R: ReadSource>(
                     let s = if (*rz).do_graft_src_at(&mut wz, &p) {
                         hex_path(&p)
                     } else {
-                        "skip".to_string()
+                        SKIP_ACT.to_string()
                     };
                     ("graft_src_at", s)
                 }
@@ -741,11 +771,11 @@ pub fn run_ops<R: ReadSource>(
                     // Skipped when either side has nothing below its focus; see
                     // Fuzz.lean and lean/FINDINGS.md #8.
                     if focus_node_empty(&wz) || focus_node_empty(rz) {
-                        ("restricting", "skip".to_string())
+                        ("restricting", SKIP_EMPTY_FOCUS.to_string())
                     } else {
                         match (*rz).do_restricting(&mut wz) {
                             Some(b) => ("restricting", show_bool(b).to_string()),
-                            None => ("restricting", "skip".to_string()),
+                            None => ("restricting", SKIP_ACT.to_string()),
                         }
                     }
                 }
@@ -754,7 +784,7 @@ pub fn run_ops<R: ReadSource>(
                     let _pr = get!(d.boolean()); // decoded for stream alignment; see `no_prune`
                     // `join_k_path_into(0)` destroys the subtrie in pathmap 0.3.1.
                     if k == 0 {
-                        ("join_k_path_into", "skip".to_string())
+                        ("join_k_path_into", SKIP_K0.to_string())
                     } else {
                         // The bool leaks node materialisation; see FINDINGS.md #8.
                         let r = wz.join_k_path_into(k, no_prune);
@@ -770,7 +800,7 @@ pub fn run_ops<R: ReadSource>(
                     let p = get!(d.path(6));
                     // `insert_prefix("")` destroys the subtrie in pathmap 0.3.1.
                     if p.is_empty() {
-                        ("insert_prefix", "skip".to_string())
+                        ("insert_prefix", SKIP_EMPTY_PATH.to_string())
                     } else {
                         ("insert_prefix", show_bool(wz.insert_prefix(&p)).to_string())
                     }
@@ -797,8 +827,10 @@ pub fn run_ops<R: ReadSource>(
                     // `meet_k_path_into` spins forever when the focus has no
                     // children, and escapes the focus subtree when k == 0.
                     // See `Zip.meetKPathUnspecified`.
-                    if k == 0 || wz.child_count() == 0 {
-                        ("meet_k_path_into", "skip".to_string())
+                    if k == 0 {
+                        ("meet_k_path_into", SKIP_K0.to_string())
+                    } else if wz.child_count() == 0 {
+                        ("meet_k_path_into", SKIP_EMPTY_FOCUS.to_string())
                     } else {
                         (
                             "meet_k_path_into",
@@ -869,7 +901,7 @@ pub fn run_ops<R: ReadSource>(
                             show_bool(agree)
                         ),
                     ),
-                    None => ("to_next_get_val", "skip".to_string()),
+                    None => ("to_next_get_val", SKIP_ACT.to_string()),
                 },
                 53 => {
                     let n = get!(d.modn(4));
@@ -882,7 +914,7 @@ pub fn run_ops<R: ReadSource>(
                     let s = if (*rz).do_graft_masked(&mut wz, mask, ru) {
                         format!("{}:{}", hex_path(&canon), show_bool(ru))
                     } else {
-                        "skip".to_string()
+                        SKIP_ACT.to_string()
                     };
                     ("graft_masked_branches", s)
                 }
@@ -899,7 +931,7 @@ pub fn run_ops<R: ReadSource>(
                     // leaves behind degrade the AlgebraicStatus that *later*
                     // operations report, contaminating the rest of the run.
                     let _ = (mask, ru, &canon);
-                    ("graft_child_maps", "skip".to_string())
+                    ("graft_child_maps", SKIP_QUARANTINED.to_string())
                 }
                 55 => {
                     let p = get!(d.path(6));
diff --git a/lean/PathMapModel/Fuzz.lean b/lean/PathMapModel/Fuzz.lean
index b1fcc938..de6c88e7 100644
--- a/lean/PathMapModel/Fuzz.lean
+++ b/lean/PathMapModel/Fuzz.lean
@@ -50,6 +50,36 @@ abbrev V := UInt64
 /-- The `Lattice`/`DistributiveLattice` instance `pathmap` provides for `u64`. -/
 def ops : ValOps V := u64Ops
 
+/-! ## Skip reasons
+
+Why an operation was skipped.  Every `skip` in the trace carries one of these,
+so a skipped op says which rule declined it rather than just that something
+declined it.  `differential/src/harness.rs` emits the same tokens; the two must
+agree exactly or every input with a skip diverges.
+
+* `skip:act` — the ACT read source cannot be a merge source
+  (`ZipperInfallibleSubtries` is not implemented for it) or does not implement
+  the trait the op needs.
+* `skip:at-root` — `to_next`/`to_prev_sibling_byte` at the zipper root, where
+  the native read zipper escapes its own root.
+* `skip:k0` — a degenerate `k = 0`.
+* `skip:empty-focus` — the focus has nothing below it, where the op's behaviour
+  is a function of node materialisation rather than trie state.
+* `skip:empty-path` — `insert_prefix("")`, which destroys the subtrie.
+* `skip:off-root-prune` — a prune on a write zipper not rooted at the map root,
+  where the depth pruned is a function of internal node layout.
+* `skip:quarantined` — the op is disabled outright (op 54).
+
+Each is recorded in FINDINGS.md and commented at its site. -/
+
+def skipAct : String := "skip:act"
+def skipAtRoot : String := "skip:at-root"
+def skipK0 : String := "skip:k0"
+def skipEmptyFocus : String := "skip:empty-focus"
+def skipEmptyPath : String := "skip:empty-path"
+def skipOffRootPrune : String := "skip:off-root-prune"
+def skipQuarantined : String := "skip:quarantined"
+
 /-! ## Rendering -/
 
 def hexDigit (n : Nat) : Char :=
@@ -262,12 +292,12 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
   | 11 => do let (t, d) ← d.mod 2
              -- Skipped at the zipper root: `ReadZipper::to_next_sibling_byte`
              -- escapes its own root there (see the notes in `Zip.toNextSiblingByte`).
-             if (getTarget s t).atRoot then some (emit s "to_next_sibling_byte" "skip", d)
+             if (getTarget s t).atRoot then some (emit s "to_next_sibling_byte" skipAtRoot, d)
              else
                let (r, s) := onTarget s t (fun z => z.toNextSiblingByte)
                some (emit s "to_next_sibling_byte" (showByteOpt r), d)
   | 12 => do let (t, d) ← d.mod 2
-             if (getTarget s t).atRoot then some (emit s "to_prev_sibling_byte" "skip", d)
+             if (getTarget s t).atRoot then some (emit s "to_prev_sibling_byte" skipAtRoot, d)
              else
                let (r, s) := onTarget s t (fun z => z.toPrevSiblingByte)
                some (emit s "to_prev_sibling_byte" (showByteOpt r), d)
@@ -283,7 +313,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
              -- `k = 0` is degenerate: `k_path_internal` treats "already at depth
              -- base+0" as a hit and reports success without moving, then
              -- `to_next_k_path(0)` reports success forever.  Skipped.
-             if k == 0 then some (emit s "descend_first_k_path" "skip", d)
+             if k == 0 then some (emit s "descend_first_k_path" skipK0, d)
              else
                let (r, z) := s.rz.descendFirstKPath k
                some (emit { s with rz := z } "descend_first_k_path" (showBool r), d)
@@ -292,7 +322,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
              -- `descend_first_k_path` iteration -- `k_path_internal` carries
              -- iteration state, and calling it cold is flagged by pathmap's own
              -- debug assertions.  So the op is the whole walk, not one step.
-             if k == 0 then some (emit s "k_path_walk" "skip", d)
+             if k == 0 then some (emit s "k_path_walk" skipK0, d)
              else
                let (ps, z) := kWalk s.rz k
                some (emit { s with rz := z } "k_path_walk"
@@ -324,7 +354,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
              let z := getTarget s t
              some (emit s "val_at" (showVal (z.valAt p)), d)
   | 25 => do let (t, d) ← d.mod 2
-             if s.act && t == 1 then some (emit s "make_map_val_count" "skip", d)
+             if s.act && t == 1 then some (emit s "make_map_val_count" skipAct, d)
              else
                let z := getTarget s t
                some (emit s "make_map_val_count" (toString (z.makeMap.valCount [])), d)
@@ -342,11 +372,11 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
   | 30 => do if pruneable s then
                let (n, z) := s.wz.prunePath
                some (emit { s with wz := z } "prune_path" (toString n), d)
-             else some (emit s "prune_path" "skip", d)
+             else some (emit s "prune_path" skipOffRootPrune, d)
   | 31 => do if pruneable s then
                let (n, z) := s.wz.pruneAscend
                some (emit { s with wz := z } "prune_ascend" (toString n), d)
-             else some (emit s "prune_ascend" "skip", d)
+             else some (emit s "prune_ascend" skipOffRootPrune, d)
   | 32 => do let (_pr, d) ← d.bool
              let leaky := s.wz.focusNodeIsEmpty
              let (r, z) := s.wz.removeBranches noPrune
@@ -355,56 +385,59 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
   | 33 => do let (n, d) ← d.mod 4; let (m, d) ← d.pathN n; let (_pr, d) ← d.bool
              let z := s.wz.removeUnmaskedBranches (ByteMask.ofList m) noPrune
              some (emit { s with wz := z } "remove_unmasked_branches" (hexPath (ByteMask.ofList m)), d)
-  | 34 => do if s.act then some (emit s "graft" "skip", d) else
+  | 34 => do if s.act then some (emit s "graft" skipAct, d) else
              do
                let z := s.wz.graft s.rz
                some (emit { s with wz := z } "graft" "-", d)
   | 35 => do let (p, d) ← d.path
-             if s.act then some (emit s "graft_src_at" "skip", d)
+             if s.act then some (emit s "graft_src_at" skipAct, d)
              else
                let z := s.wz.graftSrcAt s.rz p
                some (emit { s with wz := z } "graft_src_at" (hexPath p), d)
-  | 36 => do if s.act then some (emit s "join_into" "skip", d) else
+  | 36 => do if s.act then some (emit s "join_into" skipAct, d) else
              do
                let (st, z) := s.wz.joinInto ops s.rz
                some (emit { s with wz := z } "join_into" (toString st), d)
-  | 37 => do if s.act then some (emit s "join_map_into" "skip", d) else
+  | 37 => do if s.act then some (emit s "join_map_into" skipAct, d) else
              do
                let leaky := s.wz.focusNodeIsEmpty
                let (st, z) := s.wz.joinMapInto ops s.rz.makeMap
                some (emit { s with wz := z } "join_map_into"
                  (if leaky then "?" else toString st), d)
   | 38 => do let (_pr, d) ← d.bool
-             if s.act then some (emit s "meet_into" "skip", d)
+             if s.act then some (emit s "meet_into" skipAct, d)
              else
                let (st, z) := s.wz.meetInto ops s.rz noPrune
                some (emit { s with wz := z } "meet_into" (toString st), d)
   | 39 => do let (_pr, d) ← d.bool
-             if s.act then some (emit s "subtract_into" "skip", d)
+             if s.act then some (emit s "subtract_into" skipAct, d)
              else
                let (st, z) := s.wz.subtractInto ops s.rz noPrune
                some (emit { s with wz := z } "subtract_into" (toString st), d)
-  | 40 => do if s.act then some (emit s "restrict" "skip", d) else
+  | 40 => do if s.act then some (emit s "restrict" skipAct, d) else
              do
                let leaky := s.wz.focusNodeIsEmpty
                let (st, z) := s.wz.restrict ops s.rz
                some (emit { s with wz := z } "restrict"
                  (if leaky then "?" else toString st), d)
-  | 41 => do if s.act then some (emit s "restricting" "skip", d) else
-             do
-               -- Skipped, not merely masked, when either side has nothing below
-               -- its focus: there `restricting` branches on whether an empty node
-               -- happens to be materialised, and the two branches differ in
-               -- *effect*, not just in the reported bool.  See FINDINGS.md #8.
-               if s.wz.focusNodeIsEmpty || s.rz.focusNodeIsEmpty then
-                 some (emit s "restricting" "skip", d)
-               else
-                 let (r, z) := s.wz.restricting s.rz
-                 some (emit { s with wz := z } "restricting" (showBool r), d)
+             -- Skipped, not merely masked, when either side has nothing below
+             -- its focus: there `restricting` branches on whether an empty node
+             -- happens to be materialised, and the two branches differ in
+             -- *effect*, not just in the reported bool.  See FINDINGS.md #8.
+             -- This guard is checked *before* the ACT one because the harness
+             -- reaches the ACT skip only by calling `do_restricting`, which it
+             -- does not do once this guard has fired; the two orders were
+             -- indistinguishable while both reasons rendered as a bare `skip`.
+  | 41 => do if s.wz.focusNodeIsEmpty || s.rz.focusNodeIsEmpty then
+               some (emit s "restricting" skipEmptyFocus, d)
+             else if s.act then some (emit s "restricting" skipAct, d)
+             else
+               let (r, z) := s.wz.restricting s.rz
+               some (emit { s with wz := z } "restricting" (showBool r), d)
   | 42 => do let (k, d) ← d.mod 4; let (_pr, d) ← d.bool
              -- `join_k_path_into(0)` should be the identity but destroys the
              -- subtrie in pathmap 0.3.1; see `Zip.joinKPathInto`.
-             if k == 0 then some (emit s "join_k_path_into" "skip", d)
+             if k == 0 then some (emit s "join_k_path_into" skipK0, d)
              else
                -- The bool is another `AbstractNodeRef` leak: an empty node still
                -- comes back as `Some(...)` from `into_option()` for some
@@ -418,7 +451,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
              -- `insert_prefix("")` destroys the subtrie in pathmap 0.3.1; see
              -- `Zip.insertPrefix`.  Skipped so the known bug does not mask others.
              if p.isEmpty then
-               some (emit s "insert_prefix" "skip", d)
+               some (emit s "insert_prefix" skipEmptyPath, d)
              else
                let (r, z) := s.wz.insertPrefix p
                some (emit { s with wz := z } "insert_prefix" (showBool r), d)
@@ -437,9 +470,11 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
              | none => some (emit { s with wz := z } "take_map_restore" "0", d)
   | 46 => do let (k, d) ← d.mod 4; let (_pr, d) ← d.bool
              -- `meet_k_path_into` is not implementable for these arguments; see
-             -- `Zip.meetKPathUnspecified`.  The Rust side applies the same guard.
-             if s.wz.meetKPathUnspecified k then
-               some (emit s "meet_k_path_into" "skip", d)
+             -- `Zip.meetKPathUnspecified`, whose two disjuncts are split out here
+             -- so the skip names which one fired.  The Rust side matches.
+             if k == 0 then some (emit s "meet_k_path_into" skipK0, d)
+             else if s.wz.focusNodeIsEmpty then
+               some (emit s "meet_k_path_into" skipEmptyFocus, d)
              else
                let (r, z) := s.wz.meetKPathInto ops k noPrune
                some (emit { s with wz := z } "meet_k_path_into" (showBool r), d)
@@ -477,14 +512,14 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
   | 52 => do -- `ZipperReadOnlyIteration::to_next_get_val` must advance exactly as
              -- `to_next_val` does and hand back the value at the new focus.
              -- ACT does not implement the trait, so the op is unavailable there.
-             if s.act then some (emit s "to_next_get_val" "skip", d) else
+             if s.act then some (emit s "to_next_get_val" skipAct, d) else
              do
              let (moved, z) := s.rz.toNextVal
              let v := if moved then z.val else none
              some (emit { s with rz := z } "to_next_get_val"
                (showBool moved ++ ":" ++ showVal v ++ ":1"), d)
   | 53 => do let (n, d) ← d.mod 4; let (m, d) ← d.pathN n; let (ru, d) ← d.bool
-             if s.act then some (emit s "graft_masked_branches" "skip", d) else
+             if s.act then some (emit s "graft_masked_branches" skipAct, d) else
              do
                let z := s.wz.graftMaskedBranches s.rz (ByteMask.ofList m) ru
                some (emit { s with wz := z } "graft_masked_branches"
@@ -496,7 +531,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
              -- broken three ways (FINDINGS.md #15) and the node representations
              -- it leaves behind degrade the `AlgebraicStatus` that *later*
              -- operations report, which would contaminate the whole run.
-             if true then some (emit s "graft_child_maps" "skip", d) else
+             if true then some (emit s "graft_child_maps" skipQuarantined, d) else
              do
                let mask := ByteMask.ofList m
                let maps := mask.map (fun b => ([b], s.rz.trie.subtrie (s.rz.focus ++ [b])))
@@ -505,7 +540,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
                  (hexPath mask ++ ":" ++ showBool ru), d)
   | 55 => do let (p, d) ← d.path
              -- `meet_2` takes two sources; the second is the first moved to `p`.
-             if s.act then some (emit s "meet_2" "skip", d) else
+             if s.act then some (emit s "meet_2" skipAct, d) else
              do
                let b := { s.rz with path := s.rz.path ++ p }
                let (st, z) := s.wz.meet2 ops s.rz b
diff --git a/lean/README.md b/lean/README.md
index 71906dc4..ea58b529 100644
--- a/lean/README.md
+++ b/lean/README.md
@@ -319,19 +319,29 @@ not, the maps it ends with match the trace's `MAP0`/`MAP1`.
 A handful of argument combinations are skipped by both sides, each because the
 crate's behaviour there is a confirmed bug that would otherwise mask everything
 downstream.  Each is recorded in [FINDINGS.md](FINDINGS.md) and each skip is
-commented at its site:
-
-* `meet_k_path_into` when the focus has no children, or `k = 0` — it does not
-  terminate.
-* `insert_prefix("")` and `join_k_path_into(0)` — both should be the identity and
-  both destroy the subtrie.
-* `descend_first_k_path(0)` / `to_next_k_path(0)` — degenerate; report success
-  without moving, forever.
-* `to_next_sibling_byte` / `to_prev_sibling_byte` at the zipper root — the native
-  read zipper leaves its own root there.
-* `prune_path` / `prune_ascend`, and the `prune` flag on every other operation,
-  for a write zipper not rooted at the map root — the depth pruned is a function
-  of internal node layout, so there is nothing to specify.
+commented at its site.
+
+A skip is named in the trace — `ret=skip:<reason>`, never a bare `skip` — so a
+skipped op says which rule declined it.  The vocabulary is defined once on each
+side (`SKIP_*` in `differential/src/harness.rs`, `skip*` in
+`PathMapModel/Fuzz.lean`) and the two must agree exactly, or every input that
+skips diverges:
+
+| token | what it means |
+|---|---|
+| `skip:k0` | `meet_k_path_into(0)`, `join_k_path_into(0)`, `descend_first_k_path(0)` / `to_next_k_path(0)` — degenerate; the first two should be the identity and destroy the subtrie, the last reports success without moving, forever. |
+| `skip:empty-focus` | `meet_k_path_into` with no children (it does not terminate), and `restricting` when either side has nothing below its focus (the two branches differ in *effect*, not just in the reported bool). |
+| `skip:empty-path` | `insert_prefix("")` — should be the identity, destroys the subtrie. |
+| `skip:at-root` | `to_next_sibling_byte` / `to_prev_sibling_byte` at the zipper root — the native read zipper leaves its own root there. |
+| `skip:off-root-prune` | `prune_path` / `prune_ascend`, and the `prune` flag on every other operation, for a write zipper not rooted at the map root — the depth pruned is a function of internal node layout, so there is nothing to specify. |
+| `skip:quarantined` | `graft_child_maps` (op 54), disabled outright: it is broken three ways (FINDINGS.md #15) and the node representations it leaves behind degrade the `AlgebraicStatus` that *later* operations report. |
+| `skip:act` | ACT mode only — the read source cannot be a merge source (`ZipperInfallibleSubtries` is not implemented for it) or does not implement the trait the op needs. |
+
+Naming these turned up an ordering bug the bare token had hidden: for
+`restricting` the model tested ACT mode first and the harness tested the empty
+focus first, so in ACT mode with an empty focus the two took different branches
+and agreed only because both printed `skip`.  The model now checks the guards in
+the harness's order.
 
 `to_next_k_path` is also only exercised as the continuation of a
 `descend_first_k_path` iteration (the `k_path_walk` op), because

From 6af7e80e645239a807ffa1a4d643a55d9450b4ec Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Tue, 15 Sep 2026 23:10:46 +0000
Subject: [PATCH 27/29] Fuzz: classify the remaining divergence classes by
 shape

At seed 7 the run reported 44 unclassified divergences on 20000 crate
inputs and 3 on 5000 ACT inputs.  All of them are instances of five
defects the 2026-09-11 triage had already shrunk into lean/corpus/ but
that were never added to KNOWN, so every run rediscovered them and a
genuinely new defect would have had to be spotted among them.

They resisted the existing op-name keys because the op that reports one
is not the op that caused it: value bias is introduced by a merge but
observed by whichever of `dump`, `val_at` or the final map dump next
reads the location, and it turned up under six different op names.  So
`divergence_shape` keys them on which fields of the trace line moved --
status only, a child count that grew, a value count that shrank, a value
that changed, the focus value returned for a path the model says is
empty -- and the KNOWN entries match those tags.  They are tested last,
so every op-specific entry above still wins.

Returning "no familiar shape" is the case that matters, and the shapes
are deliberately narrow: a value appearing or vanishing is not value
bias, a location moving in a dump is not, and a bool return flipping is
not, which is why the value-bias rule for `ret` is confined to the ops
whose return is a value rather than a flag.  A compound divergence on
seed 10 (`meet_k_path_into` flips its bool, drops a value and gains a
child at once) is still reported as new, which is correct.

Also fixes a misattribution: the ACT val_count shape entry sat below the
op-name entries, so a val_count-only difference landing on a
`to_next_val` line was blamed on the `to_next_val` class -- 131 of 5000
ACT inputs at seed 7.  It is tested first now.

Seed 7 goes from 44 and 3 new to 0 and 0 with the agree counts
unchanged, seeds 0-3, 11 and 99 from 1-2 new to 0, and all 14 corpus
reproducers classify as the class their filenames name.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 lean/README.md       |  38 ++++++++-----
 lean/differential.py | 127 +++++++++++++++++++++++++++++++++++++++++--
 2 files changed, 146 insertions(+), 19 deletions(-)

diff --git a/lean/README.md b/lean/README.md
index ea58b529..f3a0cb43 100644
--- a/lean/README.md
+++ b/lean/README.md
@@ -491,25 +491,33 @@ documentation rather than from the code.
 
 ## Current agreement
 
-500 random programs (`./lean/differential.py --random 500 --seed 99 --max-fails 0`),
-model versus crate, comparing every return value plus both maps in full:
+20000 random programs (`./lean/differential.py --random 20000 --seed 7
+--max-fails 0`), model versus crate, comparing every return value plus both maps
+in full:
 
 ```
-404/500 inputs agree exactly
- 87/500 hit one of the classified defects in FINDINGS.md
-  9/500 diverge for reasons not yet classified
+19735/20000 inputs agree exactly
+  265/20000 hit one of the classified defects
+    0/20000 diverge for reasons not yet classified
 ```
 
-The 87 break down as: `to_next_val` after `to_next_step` (19), `ascend_until`
-corrupting a write zipper (17), zippers escaping their root (16), a `set_val`
-unwrap on `None` (14), the `TrieRef` slice underflow (12), `make_unique` on an
-empty sentinel (7), `join_into` dropping the source (2).
-
-Every defect listed in FINDINGS.md reproduces here exactly as it does on
-`master`; the blind-zipper migration neither fixed nor introduced any of them.
-
-`differential.py` prints that breakdown itself, so new divergences stay visible
-as the known ones are fixed.
+The 265 break down as `graft_masked_branches` creating the focus (177),
+`join_into` dropping the source (24), `AlgebraicStatus` imprecision (20 + 18),
+value bias by node layout (11), a dangling child kept by an algebraic op (11),
+`val_at` at a dangling path (3), `subtract_into` dropping a value (1).
+
+Five of those classes are keyed on the *shape* of the divergence rather than on
+an operation name, because the same defect surfaces under whichever operation
+happens to read the damaged location -- value bias, for instance, is reported by
+`meet_into` where it is introduced but by `dump`, `val_at` or the final map dump
+wherever it is later observed.  `divergence_shape` in `differential.py` decides
+those, and returning "no familiar shape" is its important case: it is what keeps
+a genuinely new defect out of the known buckets.  A shrunk reproducer for each
+class is in `lean/corpus/`, and `./lean/differential.py lean/corpus/*.bin`
+replays them all.
+
+`differential.py` prints the breakdown itself, so new divergences stay visible as
+the known ones are fixed.
 
 ## ArenaCompactTree as the read source
 
diff --git a/lean/differential.py b/lean/differential.py
index ef6d658d..47b593dd 100755
--- a/lean/differential.py
+++ b/lean/differential.py
@@ -196,6 +196,11 @@ def run(self, blob):
 # and message.  See lean/FINDINGS.md for the write-up of each, and
 # `cargo run -p differential --bin zipper_bug_repros -- <case>` for a reproducer.
 KNOWN = [
+    # Tested first: this one is keyed on a shape, and an ACT val_count-only
+    # difference can land on a line whose op name matches an entry below.
+    (["ACT-VALCOUNT-ONLY"],
+     "ACTZipper::val_count() counts from the zipper root, not the focus "
+     "[act: val_count_ignores_focus]"),
     (["ESCAPED-ROOT"],
      "a zipper left its own root: root_prefix_path() changed [root_escape]"),
     (["to_next_val"],
@@ -261,9 +266,6 @@ def run(self, blob):
      "copy-on-write cannot make a shared dangling path unique (finding 16) "
      "[shared_dangling_cow]"),
     # ArenaCompactTree read source (differential.py --act).
-    (["ACT-VALCOUNT-ONLY"],
-     "ACTZipper::val_count() counts from the zipper root, not the focus "
-     "[act: val_count_ignores_focus]"),
     (["k_path_walk"],
      "ACTZipper::descend_first_k_path() only walks the leftmost chain "
      "[act: first_k_path_no_backtrack]"),
@@ -273,9 +275,122 @@ def run(self, blob):
     (["descend_last_path"],
      "ACTZipper::descend_last_path() runs one byte past the end of the trie "
      "[act: last_path_overshoots]"),
+    # Shape classes, from `divergence_shape`.  Last on purpose: every entry
+    # above is more specific, and these are meant to catch only what none of
+    # them explain.  Reproducers for each are in lean/corpus/.
+    (["STATUS-ONLY"],
+     "AlgebraicStatus::Identity is not returned reliably when nothing changed "
+     "(finding 8); meet_into/subtract_into, status only, effects agree "
+     "[status_imprecise]"),
+    (["DANGLING-KEPT"],
+     "an algebraic op keeps a dangling child the spec drops: an empty child "
+     "node meets/subtracts to itself rather than disappearing "
+     "[meet_keeps_dangling]"),
+    (["CONTENT-DROPPED"],
+     "subtract_into() drops a value under a path present in the source "
+     "[subtract_drops_value]"),
+    (["VALUE-ONLY"],
+     "which value survives a collision follows node layout rather than the "
+     "left-biased spec (join/meet and everything that later reads the "
+     "location) [value_bias_by_node_layout]"),
+    (["FOCUS-VALUE-FOR-DANGLING"],
+     "val_at()/get_val_at() return the focus value for a dangling child path "
+     "[val_at_dangling]"),
 ]
 
 
+# Shapes that several operations share.  These classes are defined by *which
+# fields of the trace line moved*, not by which operation produced them: the
+# same defect surfaces under whichever op happens to read the damaged location,
+# so keying them on an op name would both miss cases and over-match.
+STATUSES = ("Identity", "Element", "None")
+# Ops whose `ret` is a value rather than a flag or a count.  A bool return
+# renders as `ret=1`/`ret=0`, which is indistinguishable from a value by shape,
+# so the value-bias rule for `ret` is confined to these.
+VALUE_RET_OPS = ("val_at", "set_val", "remove_val")
+
+
+def _key(tok):
+    """The field name a trace token belongs to: `v126` -> v, `ret=X` -> ret."""
+    if "=" in tok:
+        return tok.split("=", 1)[0]
+    m = re.match(r"[A-Za-z]+", tok)
+    return m.group(0) if m else tok
+
+
+def _dump_shape(sa, sb):
+    """Shape of a difference between two trie dumps (`p:v,p:v,...`).
+
+    Both the `MAP0`/`MAP1` final dumps and the `dump` op's return are this
+    shape, and the value-bias class shows up in either.
+    """
+    ea, eb = sa.split(","), sb.split(",")
+    if len(ea) != len(eb):
+        return None
+    pa = [e.rsplit(":", 1) for e in ea]
+    pb = [e.rsplit(":", 1) for e in eb]
+    if any(len(x) != 2 for x in pa + pb):
+        return None
+    if [x[0] for x in pa] != [x[0] for x in pb]:
+        return None                      # the set of locations moved
+    moved = [(x[1], y[1]) for x, y in zip(pa, pb) if x[1] != y[1]]
+    if not moved or any("-" in m for m in moved):
+        return None                      # a value appeared or vanished
+    return "VALUE-ONLY"
+
+
+def divergence_shape(a, b):
+    """Name the shape of a divergence, or None when it has no familiar one.
+
+    Returning None is the important case: it is what keeps a genuinely new
+    defect out of the known buckets, so each shape below is deliberately narrow.
+    """
+    ta, tb = a.split(), b.split()
+    if len(ta) != len(tb):
+        return None
+    diff = [(x, y) for x, y in zip(ta, tb) if x != y]
+    if not diff:
+        return None
+    if ta[0].startswith(("MAP", "ROOT")):
+        return _dump_shape(ta[1], tb[1]) if len(ta) == 2 else None
+    keys = {_key(x) for x, _ in diff}
+    vals = {t[1:] for t in ta if _key(t) == "v"}
+    if keys == {"ret"}:
+        ra, rb = diff[0][0].split("=", 1)[1], diff[0][1].split("=", 1)[1]
+        if ra in STATUSES and rb in STATUSES:
+            return "STATUS-ONLY"
+        # `-` on the model side against the focus value on the crate side, in
+        # a bare return (`val_at`) or a component of one (`get_val_agrees`).
+        ca, cb = ra.split(":"), rb.split(":")
+        if len(ca) == len(cb):
+            moved = [(x, y) for x, y in zip(ca, cb) if x != y]
+            if moved and all(x == "-" and y in vals for x, y in moved):
+                return "FOCUS-VALUE-FOR-DANGLING"
+        if "," in ra or ra.count(":") == 1:
+            return _dump_shape(ra, rb)      # `dump` returns a whole subtrie
+        if ra.isdigit() and rb.isdigit() and len(ta) > 1 and ta[1] in VALUE_RET_OPS:
+            return "VALUE-ONLY"
+        return None
+    if keys == {"v"}:
+        # Both sides must hold a value: `v-` against `v42` is a value appearing
+        # or vanishing, which is a content difference, not a biased choice.
+        if all(x[1:].isdigit() and y[1:].isdigit() for x, y in diff):
+            return "VALUE-ONLY"
+        return None
+    if keys <= {"ret", "c", "n"} and ({"c", "n"} & keys):
+        # `c` (child_count) when it moved, else `n` (val_count): a dangling
+        # child adds a child without adding a value, a dropped value the
+        # reverse, so whichever field moved is the one that says which it was.
+        field = "c" if "c" in keys else "n"
+        xa = [int(x[1:]) for x, _ in diff if _key(x) == field]
+        xb = [int(y[1:]) for _, y in diff if _key(y) == field]
+        if all(y > x for x, y in zip(xa, xb)):
+            return "DANGLING-KEPT"
+        if all(y < x for x, y in zip(xa, xb)):
+            return "CONTENT-DROPPED"
+    return None
+
+
 def act_valcount_only(a, b):
     """Do these two trace lines differ *only* in the read zipper's val_count?
 
@@ -314,7 +429,11 @@ def compare(blob, oracle, other, other_label, act=False):
         return "%s %s" % (other_label, real_err)
     for i, (a, b) in enumerate(zip(lean, real)):
         if a != b:
-            tag = "ACT-VALCOUNT-ONLY " if act and act_valcount_only(a, b) else ""
+            tags = ["ACT-VALCOUNT-ONLY"] if act and act_valcount_only(a, b) else []
+            shape = divergence_shape(a, b)
+            if shape:
+                tags.append(shape)
+            tag = "".join(t + " " for t in tags)
             return "%sline %d\n  lean:  %s\n  %-5s: %s" % (tag, i, a, other_label, b)
     if len(lean) != len(real):
         return "length %d (lean) vs %d (%s)" % (len(lean), len(real), other_label)

From 15ac67d82945200fe31abd2eb0ad599d6b9f12cb Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Tue, 15 Sep 2026 19:47:53 -0500
Subject: [PATCH 28/29] CI: resolve the persistent cache dirs from $HOME, not a
 hardcoded /home/gh-runner

The cache paths were pinned to the user the first runner happened to run as, so
any runner under a different user failed at the first step that touched them:

    mkdir: cannot create directory '/home/gh-runner': Permission denied

CARGO_TARGET_DIR could not simply be respelled with $HOME in the workflow `env:`
block, because values there are not shell expanded -- cargo would have taken the
literal string and created a directory named `$HOME`. Each job now exports it,
and LAKE_CACHE, from its existing toolchain step via $GITHUB_ENV, where the
shell does expand it. Same for the lean job, which used the path inline.

Both bench sides still resolve to one target dir per runner, so the A/B builds
share it as before, and the dirs stay outside _work and survive checkout.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 .github/workflows/ci.yml | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 7c04aae5..ff6fb1f0 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -29,8 +29,9 @@ concurrency:
 
 env:
   CARGO_TERM_COLOR: never
-  # Persistent across jobs on the runner (outside its _work dir), so builds are incremental.
-  CARGO_TARGET_DIR: /home/gh-runner/cache/target
+  # CARGO_TARGET_DIR and LAKE_CACHE are deliberately not set here: they live under the runner
+  # user's $HOME, and values in this block are not shell expanded.  Each job exports them from
+  # its toolchain step via $GITHUB_ENV, so a runner under any user works.
 
 jobs:
   test:
@@ -44,6 +45,7 @@ jobs:
         run: |
           [ -x "$HOME/.cargo/bin/rustup" ] || curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal --default-toolchain none --no-modify-path
           echo "$HOME/.cargo/bin" >> "$GITHUB_PATH"
+          echo "CARGO_TARGET_DIR=$HOME/cache/target" >> "$GITHUB_ENV"   # persists outside _work, so builds stay incremental
           export PATH="$HOME/.cargo/bin:$PATH"
           rustup toolchain install stable --profile minimal
           rustup default stable
@@ -77,6 +79,7 @@ jobs:
         run: |
           [ -x "$HOME/.cargo/bin/rustup" ] || curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal --default-toolchain none --no-modify-path
           echo "$HOME/.cargo/bin" >> "$GITHUB_PATH"
+          echo "CARGO_TARGET_DIR=$HOME/cache/target" >> "$GITHUB_ENV"   # persists outside _work, so builds stay incremental
           export PATH="$HOME/.cargo/bin:$PATH"
           rustup toolchain install stable --profile minimal
           rustup default stable
@@ -142,8 +145,8 @@ jobs:
       - name: build the model, check proofs and guards
         run: |
           # checkout wipes ignored files, so keep lake's build dir in the persistent cache
-          mkdir -p /home/gh-runner/cache/lean-lake/proofs
-          ln -sfn /home/gh-runner/cache/lean-lake/proofs lean/.lake
+          mkdir -p "$HOME"/cache/lean-lake/proofs
+          ln -sfn "$HOME"/cache/lean-lake/proofs lean/.lake
           cd lean
           lake build 2>&1 | tee ../lake.log
           test "${PIPESTATUS[0]}" -eq 0
@@ -198,6 +201,8 @@ jobs:
           export PATH="$HOME/.cargo/bin:$HOME/.elan/bin:$PATH"
           echo "$HOME/.cargo/bin" >> "$GITHUB_PATH"
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+          echo "CARGO_TARGET_DIR=$HOME/cache/target" >> "$GITHUB_ENV"   # persists outside _work, so builds stay incremental
+          echo "LAKE_CACHE=$HOME/cache/lean-lake" >> "$GITHUB_ENV"   # checkout wipes ignored files such as lean/.lake
           rustup toolchain install stable --profile minimal
           rustup default stable
           rustc --version && cargo --version
@@ -217,7 +222,6 @@ jobs:
         env:
           FUZZ_INPUTS: ${{ inputs.fuzz_inputs || '20000' }}
           FUZZ_OUT: ${{ runner.temp }}/fuzz-out
-          LAKE_CACHE: /home/gh-runner/cache/lean-lake   # checkout wipes ignored files such as lean/.lake
         run: |
           .github/scripts/fuzz_ab.py "${{ steps.base.outputs.sha }}" "${{ github.sha }}"
       - name: comment on the PR

From 8d36b681ac2a9e03d19471f3a5497af06986f75b Mon Sep 17 00:00:00 2001
From: Igor Malovitsa <igor.malovitsa@gmail.com>
Date: Tue, 15 Sep 2026 19:56:19 -0500
Subject: [PATCH 29/29] CI bench: drop the `bench` runner label requirement

The label was carried by one runner, so with that runner down the bench job sat
queued instead of running. It now schedules on any self-hosted linux x64 runner,
like the other three jobs.

Both sides of an A/B still build and run on the same runner, so a single run's
comparison stays valid; absolute numbers are no longer comparable across runs
that landed on different hardware.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 .github/workflows/ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index ff6fb1f0..90baa18e 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -65,7 +65,7 @@ jobs:
     # and manual runs only; a push to master has nothing to compare against.
     needs: [test, fuzz]
     if: github.event_name == 'pull_request' || github.event_name == 'workflow_dispatch'
-    runs-on: [self-hosted, linux, x64, bench]
+    runs-on: [self-hosted, linux, x64]
     timeout-minutes: 300
     permissions:
       contents: read