bench-gc-http + asm-gc rows in existing benches; §6.6.4 HTTP validation

New infra:
  - examples/http-server-noarena.lsp: same HTTP server minus the
    heap-snapshot/heap-restore arena loop. Isolates whether the GC
    build actually holds memory under real traffic, independent
    of the portable snapshot pattern.
  - tests/bench-gc-http.sh: drives 5,000 concurrent requests per
    cell across the full 2x2 matrix {no-GC, GC} x {snapshot, no}.
  - Makefile: new `bench-gc-http` target.

Extended benches to exercise both asm binaries:
  - tests/bench-hashset.sh now runs against both asm/uncommonlisp
    and asm/uncommonlisp-gc, with set +e so a GC-build crash on
    one workload doesn't abort the other.
  - tests/web-benchmark.sh adds a dedicated asm-gc row (and prints
    its stripped binary size) so the HTTP throughput comparison
    reports both.

Whitepaper updates:
  - §6.6.4 "Validation: HTTP Server Under Sustained Load" — the
    4-cell memory matrix. 3/4 cells green; cell 4 (GC + no
    snapshot) crashes at first GC trigger — another instance of
    the conservative-scan type-confusion class we already fixed
    once at the env/string boundary. Logged as a known issue
    rather than shipping a partial fix under time pressure.
    heap-snapshot + heap-restore remains the recommended pattern
    for production asm code; the naive GC is diagnostic + control
    group, not a replacement for the arena discipline.
  - §6.5 hash-set speedup table slightly softened to ~15-20x (was
    15-21x) since run-to-run noise on a shared laptop shifts the
    per-phase ratio by a few percent. Ratio is stable to first
    order.
  - §8.6 narrative references the ~1280x symbolic-vs-brute-force
    figure instead of the stale 40x.
  - §6 reproducibility list now lists `make bench-gc-http`.

All 137 asm no-GC + 137 asm GC + 189 shared functional tests
still pass.

Makefile

@@ -135,6 +135,9 @@ bench-gc-arena: asm-build
 bench-gc-adaptive: asm-build
 	@bash tests/bench-gc-adaptive.sh
 
+bench-gc-http: asm-build
+	@bash tests/bench-gc-http.sh
+
 bench-all: bench c-bench bench-3way bench-portal bench-portal-cross bench-web bench-rpc-chain bench-proof
 	@echo "═══════════════════════════════════════════════════════════"
 	@echo "All benchmarks complete. Numbers in the whitepaper §6.4,"

examples/http-server-noarena.lsp

@@ -0,0 +1,85 @@
+;;; http-server-noarena.lsp — same HTTP server as http-server.lsp
+;;; but with the heap-snapshot / heap-restore arena loop removed.
+;;;
+;;; On asm without GC this leaks per-request allocations forever
+;;; (every request grows %r15). On asm with GC_NAIVE the collector
+;;; reclaims between requests once heap pressure hits.
+;;;
+;;; Used by tests/bench-gc-http.sh to isolate whether GC_NAIVE
+;;; actually holds memory under real load, independent of the
+;;; portable snapshot pattern.
+
+(define *port* 8080)
+(define *crlf* "\r\n")
+(define *crlf-crlf* "\r\n\r\n")
+(define *max-requests* 100000)
+
+(define (http-response status ctype body)
+  (string-append
+    "HTTP/1.0 " status *crlf*
+    "Content-Type: " ctype *crlf*
+    "Content-Length: " (number->string (string-length body)) *crlf*
+    "Connection: close" *crlf-crlf*
+    body))
+
+(define SPACE 32)
+(define (char-at s i) (char->integer (string-ref s i)))
+
+(define (first-token s)
+  (let ((len (string-length s)))
+    (let loop ((i 0))
+      (cond
+        ((= i len) s)
+        ((= (char-at s i) SPACE) (substring s 0 i))
+        (else (loop (+ i 1)))))))
+
+(define (second-token s)
+  (let ((len (string-length s)))
+    (let loop1 ((i 0))
+      (cond
+        ((= i len) "")
+        ((= (char-at s i) SPACE)
+         (let loop2 ((j (+ i 1)))
+           (cond
+             ((= j len) (substring s (+ i 1) len))
+             ((= (char-at s j) SPACE) (substring s (+ i 1) j))
+             (else (loop2 (+ j 1))))))
+        (else (loop1 (+ i 1)))))))
+
+(define *bench-body*
+  (let loop ((s "") (i 0))
+    (if (= i 32) s
+        (loop (string-append s "0123456789abcdef0123456789abcdef") (+ i 1)))))
+
+(define (handle-request req)
+  (let ((path (second-token req)))
+    (cond
+      ((string=? path "/")
+       (http-response "200 OK" "text/html"
+         "<!doctype html><title>uncommonlisp</title><h1>feedback is all you need</h1>"))
+      ((string=? path "/bench")
+       (http-response "200 OK" "text/plain" *bench-body*))
+      (else
+       (http-response "404 Not Found" "text/plain"
+         (string-append "not found: " path "\n"))))))
+
+(define server (tcp-listen *port*))
+
+(define (server-loop n)
+  (if (>= n *max-requests*)
+      (begin
+        (display "request cap reached, exiting\n")
+        (tcp-close server))
+      (begin
+        (let ((client (tcp-accept server)))
+          (let ((req (tcp-recv client 4096)))
+            (if (and req (> (string-length req) 0))
+                (tcp-send client (handle-request req))
+                #f))
+          (tcp-close client))
+        ;; NO heap-restore here — heap grows per request.
+        (server-loop (+ n 1)))))
+
+(display "noarena http server on :") (display *port*)
+(display " (no heap-snapshot, heap grows per request)") (newline)
+(server-loop 0)

tests/bench-gc-http.sh

@@ -0,0 +1,104 @@
+#!/bin/bash
+# bench-gc-http.sh — validate the asm naive GC under sustained HTTP
+# load. Starts each server, hits it with N requests, samples peak
+# RSS. Expected: server with GC holds memory flat under the
+# no-arena workload; server without GC leaks monotonically.
+#
+# Four configs compared:
+#   1. asm no-GC + http-server.lsp          (bounded via heap-snapshot)
+#   2. asm GC   + http-server.lsp          (bounded via snapshot + GC backstop)
+#   3. asm no-GC + http-server-noarena.lsp (leaks — baseline failure)
+#   4. asm GC   + http-server-noarena.lsp  (bounded via GC alone)
+
+set -u
+cd "$(dirname "$0")/.."
+
+REQUESTS=${REQUESTS:-5000}
+CONCURRENCY=${CONCURRENCY:-8}
+
+# Kill stragglers on exit. The noarena + no-GC case can balloon
+# to gigabytes if the test somehow overshoots REQUESTS; ulimit -v
+# on each spawn caps blast radius.
+declare -a SPAWNED=()
+cleanup() {
+    local pid
+    for pid in "${SPAWNED[@]}"; do kill -9 "$pid" 2>/dev/null; done
+    sleep 0.2
+    pkill -9 -u "$USER" -f 'examples/http-server' 2>/dev/null || true
+}
+trap cleanup EXIT INT TERM
+
+make -s -C asm all
+
+printf "\n═══════════════════════════════════════════════════════\n"
+printf "asm GC vs no-GC under sustained HTTP load\n"
+printf "  %s requests, concurrency %s, 1 KB body per request\n" "$REQUESTS" "$CONCURRENCY"
+printf "═══════════════════════════════════════════════════════\n"
+
+run_case() {
+    local label="$1" bin="$2" srv="$3" vcap="$4"
+    # Fresh port per case so we don't collide with a lingering socket.
+    local pid peak=0 rss time_s=0 t0 t1
+    printf "\n── %s ──\n" "$label"
+    ( ulimit -v "$vcap" && exec "$bin" < "$srv" >/dev/null 2>&1 ) &
+    pid=$!
+    SPAWNED+=("$pid")
+    # Wait for port.
+    for _ in $(seq 1 30); do
+        if curl -s -o /dev/null -w "%{http_code}" "http://localhost:8080/" 2>/dev/null | grep -q 200; then
+            break
+        fi
+        sleep 0.1
+    done
+    if ! kill -0 "$pid" 2>/dev/null; then
+        echo "  SERVER FAILED TO START (ulimit -v $vcap may be too tight)"
+        return 1
+    fi
+    # Baseline RSS
+    local rss0
+    rss0=$(awk '/^VmRSS:/ {print $2}' /proc/$pid/status 2>/dev/null || echo 0)
+    printf "  baseline_rss_kb=%s\n" "$rss0"
+    # Drive traffic; sample RSS every 200ms.
+    t0=$(date +%s.%N)
+    ( seq 1 "$REQUESTS" | xargs -P "$CONCURRENCY" -I_ \
+        curl -s -o /dev/null "http://localhost:8080/bench" ) &
+    local curl_pid=$!
+    while kill -0 "$curl_pid" 2>/dev/null; do
+        if kill -0 "$pid" 2>/dev/null; then
+            rss=$(awk '/^VmRSS:/ {print $2}' /proc/$pid/status 2>/dev/null || echo 0)
+            [ "$rss" -gt "$peak" ] && peak=$rss
+        else
+            echo "  SERVER DIED MID-RUN (likely OOM at ulimit -v $vcap)"
+            kill "$curl_pid" 2>/dev/null
+            break
+        fi
+        sleep 0.2
+    done
+    wait "$curl_pid" 2>/dev/null || true
+    t1=$(date +%s.%N)
+    # Final RSS right before we kill the server.
+    local final_rss=0
+    if kill -0 "$pid" 2>/dev/null; then
+        final_rss=$(awk '/^VmRSS:/ {print $2}' /proc/$pid/status 2>/dev/null || echo 0)
+    fi
+    kill -9 "$pid" 2>/dev/null
+    wait "$pid" 2>/dev/null || true
+    time_s=$(python3 -c "print(f'{float(\"$t1\")-float(\"$t0\"):.2f}')")
+    local rps
+    rps=$(python3 -c "print(f'{$REQUESTS / ($time_s if $time_s>0 else 1):.0f}')")
+    printf "  time_s=%s  req/s=%s  peak_rss_kb=%s  final_rss_kb=%s  growth_kb=%s\n" \
+        "$time_s" "$rps" "$peak" "$final_rss" "$((final_rss - rss0))"
+}
+
+# vcap = ulimit -v in KB. 131072 = 128 MB — enough for one GC chunk
+# and the process; tight enough that a leaker will OOM before the
+# kernel eats all RAM. Widen if the no-GC noarena case needs to run
+# to completion rather than OOM'd.
+VCAP=${VCAP:-524288}
+
+run_case "asm no-GC + snapshot loop"     "./asm/uncommonlisp"    "examples/http-server.lsp"         "$VCAP" || true
+run_case "asm GC   + snapshot loop"      "./asm/uncommonlisp-gc" "examples/http-server.lsp"         "$VCAP" || true
+run_case "asm no-GC + no snapshot"       "./asm/uncommonlisp"    "examples/http-server-noarena.lsp" "$VCAP" || true
+run_case "asm GC   + no snapshot"        "./asm/uncommonlisp-gc" "examples/http-server-noarena.lsp" "$VCAP" || true
+
+printf "\n"

tests/bench-hashset.sh

@@ -1,7 +1,7 @@
 #!/bin/bash
 # bench-hashset.sh — run the asm native hash-set vs portable benchmark
 # and echo the speedup. ASM-only: C/Python have no hash-set builtin.
-set -e
+set +e
 cd "$(dirname "$0")/.."
 
 ulimit -v 524288
@@ -12,10 +12,19 @@ if [ ! -x asm/uncommonlisp ] || [ asm/uncommonlisp.s -nt asm/uncommonlisp ]; the
     make -s asm-build
 fi
 
+echo "── asm no-GC ──"
 timeout 60 ./asm/uncommonlisp < examples/bench-hashset.lsp
+echo ""
+echo "── asm GC (GC_NAIVE build) ──"
+# Under GC_NAIVE the heap is 1 MB per chunk; build-list(K=500) runs
+# into the bump threshold and triggers implicit GC. That's the
+# intended comparison — same primitives, different allocator.
+timeout 60 ./asm/uncommonlisp-gc < examples/bench-hashset.lsp
 
-# Verify cleanup
-if pgrep -u "$USER" -f 'asm/uncommonlisp' > /dev/null; then
-    echo "STRAGGLER asm/uncommonlisp detected" >&2
+# Verify cleanup. pgrep with -x matches the exact command basename
+# so it doesn't false-positive on the parent shell.
+if pgrep -u "$USER" -x uncommonlisp > /dev/null || \
+   pgrep -u "$USER" -x uncommonlisp-gc > /dev/null; then
+    echo "STRAGGLER asm binary detected" >&2
     exit 1
 fi

tests/web-benchmark.sh

@@ -15,6 +15,7 @@ CONCURRENCY=${CONCURRENCY:-10}
 PY="python3 uncommonlisp.py --fast"
 C="./c/uncommonlisp"
 ASM="./asm/uncommonlisp"
+ASM_GC="./asm/uncommonlisp-gc"
 
 # Track every server PID we spawn; the EXIT trap kills them all.
 # Asm has no GC — a leaked server leaks 64 MB per heap growth
@@ -115,11 +116,18 @@ PID=$(start_server "$C examples/http-server.lsp" 8080)
 bench_one "uncommonlisp C       (/bench, 1 KB)" 8080 /bench
 stop_server "$PID"
 
-# ── uncommonlisp asm ──
+# ── uncommonlisp asm (bump-only) ──
 PID=$(start_server "$ASM < examples/http-server.lsp" 8080)
 bench_one "uncommonlisp asm     (/bench, 1 KB)" 8080 /bench
 stop_server "$PID"
 
+# ── uncommonlisp asm-gc (naive mark-sweep + meta-GC build) ──
+if [ -x "$ASM_GC" ]; then
+    PID=$(start_server "$ASM_GC < examples/http-server.lsp" 8080)
+    bench_one "uncommonlisp asm-gc  (/bench, 1 KB)" 8080 /bench
+    stop_server "$PID"
+fi
+
 # ── Python http.server (stdlib) ──
 (cd "$STATIC_DIR" && python3 -m http.server 8080 > /dev/null 2>&1) &
 PID=$!
@@ -140,7 +148,9 @@ echo
 echo "═══════════════════════════════════════════════════════════════"
 echo "Binary sizes"
 echo "═══════════════════════════════════════════════════════════════"
-printf "  uncommonlisp asm:   %s\n" "$(du -b asm/uncommonlisp | cut -f1) bytes"
-printf "  uncommonlisp C:     %s\n" "$(du -b c/uncommonlisp | cut -f1) bytes"
+printf "  uncommonlisp asm:    %s\n" "$(du -b asm/uncommonlisp | cut -f1) bytes"
+[ -x asm/uncommonlisp-gc ] && \
+printf "  uncommonlisp asm-gc: %s\n" "$(du -b asm/uncommonlisp-gc | cut -f1) bytes (GC_NAIVE build)"
+printf "  uncommonlisp C:      %s\n" "$(du -b c/uncommonlisp | cut -f1) bytes"
 printf "  busybox httpd:      %s\n" "$(du -b /usr/bin/busybox | cut -f1) bytes (multi-call)"
 printf "  python3:            %s bytes (interpreter binary)\n" "$(du -bL $(which python3) | cut -f1)"

whitepaper/uncommonlisp-whitepaper.rst

@@ -354,6 +354,7 @@ Folding only applies when all operands are compile-time constants & the function
 - §6.6 asm naive GC (bump vs mark-sweep memory): ``make bench-gc``
 - §6.6 asm meta-GC (arena fast path vs naive sweep): ``make bench-gc-arena``
 - §6.6.3 asm adaptive meta-GC (greedy vs EMA-driven across 3 workloads): ``make bench-gc-adaptive``
+- §6.6.4 asm GC vs no-GC under HTTP load: ``make bench-gc-http``
 - §7.2 Cross-impl portal matrix: ``make bench-portal-cross``
 - §7.5 Portal save+load timings: ``make bench-portal``
 - §11.3 HTTP server vs busybox / python http.server: ``make bench-web``
@@ -459,12 +460,12 @@ A native hash-set moves the same algorithm into asm: ``bi_hash_set_add`` is one
    ============================= =============== =============== ===========
    Phase (N=5,000 integers)      portable (ms)   native (ms)     Speedup
    ============================= =============== =============== ===========
-   insert-N                          129              6           21×
-   hit-lookup-N                      124              8           15×
-   miss-lookup-N                     238             12           19×
+   insert-N                          ~130           ~7            ~20×
+   hit-lookup-N                      ~125           ~9            ~15×
+   miss-lookup-N                     ~240          ~15            ~18×
    ============================= =============== =============== ===========
 
-Same hash function (key value for ints, djb2 for strings, identity for everything else), same 64-bucket chaining, same load factor. The 15–21× factor is **purely the cost of interpretation on the bucket walk**: each Scheme-level ``car`` pays a tag check plus an eval dispatch, while the asm-level loop is two memory loads and a compare per step.
+Same hash function (key value for ints, djb2 for strings, identity for everything else), same 64-bucket chaining, same load factor. The ~15–20× factor is **purely the cost of interpretation on the bucket walk**: each Scheme-level ``car`` pays a tag check plus an eval dispatch, while the asm-level loop is two memory loads and a compare per step. Run-to-run variance on a shared laptop sits at a few percent — the ratio is stable to first order.
 
 This matters beyond one data structure. Every container that lives in Lumbda-the-language-on-asm-the-interpreter pays the same overhead. For a server that processes thousands of proofs per minute, pulling the hash-set into the asm primitive layer erases a dominant cost. The same pattern applies to any structure with a tight inner loop: vector sort, string search, rolling checksum. Asm's tree-walker is slow on user code; asm's builtins run at the speed of the host CPU.
 
@@ -619,6 +620,38 @@ Reading the numbers:
 
 **Reproduce:** ``make bench-gc-adaptive`` (source: ``tests/bench-gc-adaptive.sh``, ``examples/bench-gc-adaptive.lsp``). Each (workload × mode) pair runs in a fresh asm-gc process so results don't contaminate each other across phases.
 
+6.6.4 Validation: HTTP Server Under Sustained Load
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The reason we built the GC at all was to let long-running asm HTTP servers not leak. Bench-gc-http drives ``examples/http-server.lsp`` (uses the portable ``heap-snapshot`` / ``heap-restore`` arena loop) and ``examples/http-server-noarena.lsp`` (same server with the snapshot pattern removed) under 5,000 concurrent requests against each asm build. The matrix has four cells because the snapshot pattern is orthogonal to the collector: either, both, or neither.
+
+.. table::
+   :widths: 38 14 14 14 20
+
+   ============================== ========= ========= ========== =============
+   Config                          req/s     baseline  peak RSS   growth KB
+                                             RSS KB    KB
+   ============================== ========= ========= ========== =============
+   asm no-GC + ``heap-snapshot``    484       100        104        **4**
+   asm GC    + ``heap-snapshot``    462       120        124        **4**
+   asm no-GC + no snapshot           463       96        45,812     **46,096**
+   asm GC    + no snapshot           †         —          —          —
+   ============================== ========= ========= ========== =============
+
+† Crashes at first GC — latent conservative-scan bug, see below.
+
+Three cells validate cleanly:
+
+- **Cells 1 and 2** show that on idiomatic code using ``heap-snapshot``, both binaries hold memory absolutely flat (~4 KB growth over 5,000 requests is normal VM noise). The GC build costs ~5% throughput for a feature the snapshot pattern doesn't need — a meaningful signal that if your server is well-written, GC is optional overhead.
+
+- **Cell 3** demonstrates the leak scenario we explicitly designed the GC build to solve. Without ``heap-snapshot``, the no-GC asm server grows **~9 KB per request** — 46 MB over 5,000 requests, heading to OOM on any real workload. This is the bump-only allocator working exactly as documented.
+
+- **Cell 4** is the one that should have been bounded by naive mark-sweep and wasn't. The server crashes at the first GC trigger (~1 MB of allocations into the run), fixed-size workload triggering another variant of the conservative stack scan's type-confusion. The pattern is identical in kind to the 24-byte env/string collision (§6.6.1) we already fixed — probably a 24- or 40-byte response block being walked as something it isn't. The fix requires tightening one more walker; we logged it as a known issue rather than shipping a fix under time pressure.
+
+**Honest read.** The GC build succeeds at validating the snapshot pattern (cell 2 is the real deployment target for long-running asm servers) but the "use GC instead of snapshots" use case (cell 4) has an outstanding correctness bug. ``heap-snapshot`` + ``heap-restore`` remain the recommended pattern for production asm code; the naive GC serves as a diagnostic backstop and as the control-group baseline for future memory-management work. This is still progress — we now have a concrete failing case to aim the next round of debugging at, rather than a vague worry.
+
+**Reproduce:** ``make bench-gc-http``. Tuning: ``REQUESTS=10000 CONCURRENCY=16 VCAP=524288 bash tests/bench-gc-http.sh``.
+
 7. Portal: Feedback Across Time
 ----------------------------------------
 
@@ -926,7 +959,7 @@ Two comparisons matter. **Cold vs cold** is the honest end-to-end compare: Lumbd
 
 **All four Lumbda tiers verify the proof.** A C ``--fast`` bytecode-compiler bug originally caused the final tier to hang on the rewriter's named-let loop; narrowed to a minimal reproduction (see ``c/TODO-named-let-bytecode.md``) and worked around in the proof file by using an internal recursive ``define`` in place of the offending named-let. All four tiers now complete in under 100 ms cold. **Reproduce:** ``make bench-proof`` (source: ``tests/bench-proof.sh``).
 
-**First machine-checked treatment.** The original paper (Odrzywołek, arXiv:2603.21852v2, 2026-04-04) presents the EML universality claim analytically — pure LaTeX mathematics, no formal tool. The companion Zenodo artifact is symbolic-regression / gradient-optimization code, not a verification. To our knowledge the Lean 4 proof shipped in this repo is the first machine-checked treatment of the EML identities, and the accompanying Lumbda-native checker is the first self-hosted machine-checked version. Five theorems, zero ``sorry``, no Mathlib dependency — 40× faster than the brute-force numerical search it replaced, and carrying the additional guarantee that no implementation quirk of floating point can ever break the conclusion.
+**First machine-checked treatment.** The original paper (Odrzywołek, arXiv:2603.21852v2, 2026-04-04) presents the EML universality claim analytically — pure LaTeX mathematics, no formal tool. The companion Zenodo artifact is symbolic-regression / gradient-optimization code, not a verification. To our knowledge the Lean 4 proof shipped in this repo is the first machine-checked treatment of the EML identities, and the accompanying Lumbda-native checker is the first self-hosted machine-checked version. Five theorems, zero ``sorry``, no Mathlib dependency — **~1,280× faster than the brute-force numerical search** it replaced once the symbolic rewriter was written (see §8.6 for the full six-row comparison), and carrying the additional guarantee that no implementation quirk of floating point can ever break the conclusion.
 
 
 9. Language Coverage