|
| 1 | +#!/usr/bin/env bash |
| 2 | +# |
| 3 | +# bench_verify.sh — interleaved A/B/B/A paired verifier benchmark (PR vs main). |
| 4 | +# Positive numbers are improvements (PR faster). |
| 5 | +# |
| 6 | +# Usage: scripts/bench_verify.sh REF_A [REF_B=origin/main] [N_PAIRS=20] |
| 7 | +# REF_A/REF_B refs to compare (A = PR side); N_PAIRS even, default 20 (~4 min). |
| 8 | +# Env: REBUILD=1 forces rebuild; BENCH_FEATURES=<list> (default: jemalloc-stats). |
| 9 | + |
| 10 | +set -euo pipefail |
| 11 | + |
| 12 | +if [ $# -lt 1 ]; then |
| 13 | + echo "usage: bench_verify.sh REF_A [REF_B=origin/main] [N_PAIRS=20]" >&2 |
| 14 | + echo " REF_A: ref or SHA to evaluate (the PR side)" >&2 |
| 15 | + exit 2 |
| 16 | +fi |
| 17 | +REF_A="$1" |
| 18 | +REF_B="${2:-origin/main}" |
| 19 | +N_PAIRS="${3:-20}" |
| 20 | +BENCH_FEATURES="${BENCH_FEATURES:-jemalloc-stats}" |
| 21 | + |
| 22 | +ELF_REL="executor/program_artifacts/rust/ethrex.elf" |
| 23 | +INPUT_REL="executor/tests/ethrex_bench_20.bin" |
| 24 | +WORK="/tmp/verify_run" |
| 25 | +WT="/tmp/verify_wt" |
| 26 | +PROOF="/tmp/verify_proof.bin" |
| 27 | + |
| 28 | +ROOT="$(git rev-parse --show-toplevel)" |
| 29 | +cd "$ROOT" |
| 30 | + |
| 31 | +# Fail fast on the toolchain the final stats step needs, before the build. |
| 32 | +command -v python3 >/dev/null 2>&1 || { echo "ERROR: python3 is required (final stats step)." >&2; exit 1; } |
| 33 | + |
| 34 | +echo "==> Refs" |
| 35 | +git fetch origin --quiet || echo "WARNING: 'git fetch origin' failed -- resolving against possibly-stale local refs." >&2 |
| 36 | +SHA_A="$(git rev-parse "$REF_A")" |
| 37 | +SHA_B="$(git rev-parse "$REF_B")" |
| 38 | +echo " A (PR) $REF_A -> ${SHA_A:0:10}" |
| 39 | +echo " B (baseline) $REF_B -> ${SHA_B:0:10}" |
| 40 | +if [ $((N_PAIRS % 2)) -ne 0 ]; then |
| 41 | + echo " WARNING: N_PAIRS=$N_PAIRS is odd; use an even count so AB/BA orders balance." |
| 42 | +fi |
| 43 | +echo " pairs=$N_PAIRS (=$((N_PAIRS * 2)) verify runs)" |
| 44 | + |
| 45 | +mkdir -p "$WORK" |
| 46 | + |
| 47 | +# --- 1. Guest ELF + fixture (identical for both sides; build once if missing) --- |
| 48 | +if [ ! -f "$ELF_REL" ]; then |
| 49 | + echo "==> Building ethrex guest ELF (missing)" |
| 50 | + export SYSROOT_DIR="${SYSROOT_DIR:-$HOME/.lambda-vm-sysroot}" |
| 51 | + make "$ELF_REL" |
| 52 | +fi |
| 53 | +if [ ! -f "$INPUT_REL" ]; then |
| 54 | + echo "==> Generating ethrex 20-transfer fixture (missing)" |
| 55 | + ( cd tooling/ethrex-fixtures && cargo build --release ) |
| 56 | + tooling/ethrex-fixtures/target/release/ethrex-fixtures 20 "$INPUT_REL" distinct |
| 57 | +fi |
| 58 | +ELF="$(cd "$(dirname "$ELF_REL")" && pwd)/$(basename "$ELF_REL")" |
| 59 | +INPUT="$(cd "$(dirname "$INPUT_REL")" && pwd)/$(basename "$INPUT_REL")" |
| 60 | + |
| 61 | +# --- 2. Build (or reuse) both cli binaries --- |
| 62 | +need_build=0 |
| 63 | +if [ "${REBUILD:-0}" = "1" ] || [ ! -x "$WORK/cli_A" ] || [ ! -x "$WORK/cli_B" ]; then |
| 64 | + need_build=1 |
| 65 | +elif [ "$(cat "$WORK/cli_A.sha" 2>/dev/null)" != "$SHA_A $BENCH_FEATURES" ] || \ |
| 66 | + [ "$(cat "$WORK/cli_B.sha" 2>/dev/null)" != "$SHA_B $BENCH_FEATURES" ]; then |
| 67 | + echo "==> Cached binaries are for different refs/features; rebuilding." |
| 68 | + need_build=1 |
| 69 | +fi |
| 70 | +if [ "$need_build" = "1" ]; then |
| 71 | + cleanup() { git worktree remove --force "$WT" 2>/dev/null || true; } |
| 72 | + trap cleanup EXIT |
| 73 | + git worktree remove --force "$WT" 2>/dev/null || true |
| 74 | + echo "==> Building both cli binaries in isolated worktree $WT" |
| 75 | + git worktree add --detach "$WT" "$SHA_B" >/dev/null |
| 76 | + build_cli() { # $1=sha $2=out (shared target dir -> 2nd build is incremental) |
| 77 | + echo "==> Building cli @ ${1:0:10} -> $2 (features: $BENCH_FEATURES)" |
| 78 | + git -C "$WT" checkout --quiet -f "$1" |
| 79 | + if ! ( cd "$WT" && cargo build --release -p cli --features "$BENCH_FEATURES" >"$WORK/build_$2.log" 2>&1 ); then |
| 80 | + echo "ERROR: cargo build failed for $2 (@ ${1:0:10}). Tail of $WORK/build_$2.log:" >&2 |
| 81 | + tail -40 "$WORK/build_$2.log" >&2 |
| 82 | + exit 1 |
| 83 | + fi |
| 84 | + cp "$WT/target/release/cli" "$WORK/$2" |
| 85 | + echo "$1 $BENCH_FEATURES" > "$WORK/$2.sha" |
| 86 | + } |
| 87 | + build_cli "$SHA_B" cli_B |
| 88 | + build_cli "$SHA_A" cli_A |
| 89 | + cleanup |
| 90 | + trap - EXIT |
| 91 | +else |
| 92 | + echo "==> Reusing cached binaries (refs + features match; REBUILD=1 to force):" |
| 93 | + echo " cli_A=${SHA_A:0:10} cli_B=${SHA_B:0:10} features=$BENCH_FEATURES" |
| 94 | +fi |
| 95 | + |
| 96 | +# --- 3. Prove once (shared), then interleaved A/B/B/A verify measurement --- |
| 97 | +prove_once() { # $1=binary $2=proof-path |
| 98 | + if ! "$1" prove "$ELF" --private-input "$INPUT" -o "$2" --time >"$WORK/prove_$(basename "$2").log" 2>&1; then |
| 99 | + echo "ERROR: prove failed for $1. Tail of log:" >&2 |
| 100 | + tail -20 "$WORK/prove_$(basename "$2").log" >&2 |
| 101 | + exit 1 |
| 102 | + fi |
| 103 | +} |
| 104 | +run_verify() { # $1=binary $2=proof-path -> echoes verification time (s) |
| 105 | + local out t |
| 106 | + out="$("$1" verify "$2" "$ELF" --time 2>&1)" |
| 107 | + t="$(printf '%s\n' "$out" | grep -o 'Verification time: [0-9.]*' | awk '{print $3}')" |
| 108 | + if [ -z "$t" ]; then |
| 109 | + echo "ERROR: could not parse 'Verification time' from cli output:" >&2 |
| 110 | + printf '%s\n' "$out" >&2 |
| 111 | + exit 1 |
| 112 | + fi |
| 113 | + echo "$t" |
| 114 | +} |
| 115 | + |
| 116 | +# One shared proof for both sides: per-side proofs leak a proof-specific bias ABBA can't cancel. |
| 117 | +echo "==> Proving once with the baseline binary (both sides verify this same proof)" |
| 118 | +prove_once "$WORK/cli_B" "$PROOF" |
| 119 | + |
| 120 | +echo "==> Running $N_PAIRS interleaved pairs (improvement: + = PR faster)" |
| 121 | +printf 'pair,a_time,b_time\n' > "$WORK/pairs.csv" |
| 122 | +for i in $(seq 1 "$N_PAIRS"); do |
| 123 | + if [ $((i % 2)) -eq 1 ]; then # odd pair: A then B |
| 124 | + a="$(run_verify "$WORK/cli_A" "$PROOF")"; b="$(run_verify "$WORK/cli_B" "$PROOF")" |
| 125 | + else # even pair: B then A (ABBA pattern) |
| 126 | + b="$(run_verify "$WORK/cli_B" "$PROOF")"; a="$(run_verify "$WORK/cli_A" "$PROOF")" |
| 127 | + fi |
| 128 | + printf '%d,%s,%s\n' "$i" "$a" "$b" >> "$WORK/pairs.csv" |
| 129 | + printf ' pair %2d/%d A=%ss B=%ss PR %+.2f%% (+=faster)\n' \ |
| 130 | + "$i" "$N_PAIRS" "$a" "$b" "$(awk "BEGIN{print ($b-$a)/$b*100}")" |
| 131 | +done |
| 132 | +rm -f "$PROOF" |
| 133 | + |
| 134 | +# --- 4. Paired t-test + robust median/Wilcoxon (same stats as bench_abba.sh) --- |
| 135 | +python3 - "$WORK/pairs.csv" <<'PY' |
| 136 | +import sys, csv, math |
| 137 | +
|
| 138 | +rows = list(csv.DictReader(open(sys.argv[1]))) |
| 139 | +A = [float(r['a_time']) for r in rows] # PR |
| 140 | +B = [float(r['b_time']) for r in rows] # baseline |
| 141 | +n = len(A) |
| 142 | +# per-pair improvement: positive => PR (A) faster than baseline (B) |
| 143 | +d = [(b - a) / b * 100.0 for a, b in zip(A, B)] |
| 144 | +
|
| 145 | +# ---- parametric: paired t ---- |
| 146 | +mean = sum(d) / n |
| 147 | +var = sum((x - mean) ** 2 for x in d) / (n - 1) if n > 1 else 0.0 |
| 148 | +sd = math.sqrt(var) |
| 149 | +se = sd / math.sqrt(n) if n else float('inf') |
| 150 | +TT = {1:12.706,2:4.303,3:3.182,4:2.776,5:2.571,6:2.447,7:2.365,8:2.306,9:2.262, |
| 151 | + 10:2.228,11:2.201,12:2.179,13:2.160,14:2.145,15:2.131,16:2.120,17:2.110, |
| 152 | + 18:2.101,19:2.093,20:2.086,21:2.080,22:2.074,23:2.069,24:2.064,25:2.060, |
| 153 | + 26:2.056,27:2.052,28:2.048,29:2.045,30:2.042,35:2.030,40:2.021,50:2.009, |
| 154 | + 60:2.000,80:1.990,120:1.980} |
| 155 | +df = n - 1 |
| 156 | +tc = TT.get(df) or (1.96 if df > 120 else TT[min(TT, key=lambda k: abs(k - df))]) |
| 157 | +lo, hi = mean - tc * se, mean + tc * se |
| 158 | +
|
| 159 | +# ---- robust: median + Wilcoxon signed-rank (tie-averaged ranks, EXACT p, pure stdlib) ---- |
| 160 | +def median(xs): |
| 161 | + s = sorted(xs); m = len(s) |
| 162 | + return s[m // 2] if m % 2 else (s[m // 2 - 1] + s[m // 2]) / 2 |
| 163 | +
|
| 164 | +nz = [x for x in d if x != 0.0] |
| 165 | +m = len(nz) |
| 166 | +order = sorted(range(m), key=lambda i: abs(nz[i])) |
| 167 | +ranks = [0.0] * m |
| 168 | +i = 0 |
| 169 | +while i < m: # average ranks within ties on |d| |
| 170 | + j = i |
| 171 | + while j + 1 < m and abs(nz[order[j + 1]]) == abs(nz[order[i]]): |
| 172 | + j += 1 |
| 173 | + avg = (i + 1 + j + 1) / 2.0 |
| 174 | + for k in range(i, j + 1): |
| 175 | + ranks[order[k]] = avg |
| 176 | + i = j + 1 |
| 177 | +Wp = sum(r for r, x in zip(ranks, nz) if x > 0) |
| 178 | +Wn = sum(r for r, x in zip(ranks, nz) if x < 0) |
| 179 | +mu = m * (m + 1) / 4.0 |
| 180 | +sig = math.sqrt(m * (m + 1) * (2 * m + 1) / 24.0) if m else 0.0 |
| 181 | +z = (Wp - mu - (0.5 if Wp > mu else -0.5)) / sig if sig else 0.0 # normal approx (display only) |
| 182 | +# EXACT two-sided p via generating-function DP over the signed-rank null distribution. |
| 183 | +if m: |
| 184 | + ir = [int(round(2 * r)) for r in ranks] |
| 185 | + poly = [1] |
| 186 | + for r in ir: |
| 187 | + nxt = [0] * (len(poly) + r) |
| 188 | + for v, c in enumerate(poly): |
| 189 | + if c: |
| 190 | + nxt[v] += c |
| 191 | + nxt[v + r] += c |
| 192 | + poly = nxt |
| 193 | + Wp2 = int(round(2 * Wp)) |
| 194 | + p = min(1.0, 2.0 * min(sum(poly[:Wp2 + 1]), sum(poly[Wp2:])) / (1 << m)) |
| 195 | +else: |
| 196 | + p = 1.0 |
| 197 | +med = median(d) |
| 198 | +
|
| 199 | +# ---- server stability (byproduct): run-to-run jitter + within-session drift ---- |
| 200 | +def cv(xs): |
| 201 | + mm = sum(xs) / len(xs) |
| 202 | + s = math.sqrt(sum((x - mm) ** 2 for x in xs) / (len(xs) - 1)) if len(xs) > 1 else 0.0 |
| 203 | + return (s / mm * 100.0) if mm else 0.0 |
| 204 | +mA, mB = sum(A) / n, sum(B) / n |
| 205 | +cvA, cvB = cv(A), cv(B) |
| 206 | +seq = [] |
| 207 | +for i in range(n): |
| 208 | + seq += ([('A', A[i]), ('B', B[i])] if (i + 1) % 2 else [('B', B[i]), ('A', A[i])]) |
| 209 | +nrm = [(t / (mA if lbl == 'A' else mB) - 1) * 100 for lbl, t in seq] |
| 210 | +N = len(nrm); mi = (N - 1) / 2.0; mn = sum(nrm) / N |
| 211 | +denom = sum((i - mi) ** 2 for i in range(N)) |
| 212 | +slope = (sum((i - mi) * (nrm[i] - mn) for i in range(N)) / denom) if denom else 0.0 |
| 213 | +half = N // 2 |
| 214 | +drift_shift = sum(nrm[half:]) / (N - half) - sum(nrm[:half]) / half |
| 215 | +
|
| 216 | +# Markdown table (rendered directly in the PR comment) + paired detail. |
| 217 | +sign = lambda v: f"+{v:.2f}" if v >= 0 else f"{v:.2f}" |
| 218 | +icon = "🟢" if (lo > 0 and p < 0.05) else "🔴" if (hi < 0 and p < 0.05) else "⚪" |
| 219 | +print("\n=== Verify ABBA result (improvement: + = PR faster) ===") |
| 220 | +print() |
| 221 | +print("| Metric | main | PR | Δ (paired) |") |
| 222 | +print("|--------|------|----|------------|") |
| 223 | +print(f"| **Verify time** | {mB:.3f}s | {mA:.3f}s | {sign(mean)}% {icon} |") |
| 224 | +print() |
| 225 | +print("```") |
| 226 | +print(f" pairs: {n} mean A (PR): {mA:.3f}s mean B (main): {mB:.3f}s") |
| 227 | +print(f" [parametric] paired-t mean {mean:+.2f}% sd {sd:.2f}% se {se:.2f}%") |
| 228 | +print(f" 95% CI: [{lo:+.2f}%, {hi:+.2f}%] (t df={df} = {tc})") |
| 229 | +pstr = f"{p:.4f}" if p >= 1e-4 else f"{p:.1e}" |
| 230 | +print(f" [robust] median {med:+.2f}% Wilcoxon W+={Wp:.0f} W-={Wn:.0f} p(exact)={pstr} (z={z:+.2f})") |
| 231 | +print() |
| 232 | +print(f" run-to-run jitter: A CV {cvA:.2f}% B CV {cvB:.2f}% (lower = steadier)") |
| 233 | +print(f" within-session drift: {slope * N:+.2f}% over the run, 1st->2nd half {drift_shift:+.2f}%") |
| 234 | +print("```") |
| 235 | +if lo > 0 and p < 0.05: |
| 236 | + print(f"\n> 🟢 **REAL IMPROVEMENT** — PR verifies ~{mean:.2f}% faster (paired-t and Wilcoxon agree).") |
| 237 | +elif hi < 0 and p < 0.05: |
| 238 | + print(f"\n> 🔴 **REAL REGRESSION** — PR verifies ~{-mean:.2f}% slower (paired-t and Wilcoxon agree).") |
| 239 | +elif (lo > 0) != (p < 0.05): |
| 240 | + print(f"\n> ⚪ **BORDERLINE** — parametric and robust disagree; suspect outlier pair(s). Trust the median ({med:+.2f}%); add pairs.") |
| 241 | +else: |
| 242 | + print(f"\n> ⚪ **INCONCLUSIVE** — effect not separable from 0 at n={n} (point estimate ~{med:+.2f}%). Add pairs to resolve.") |
| 243 | +PY |
0 commit comments