whitepaper: GAS + i5-8350U hardware note, Lean EML sets the MOAD bar

Two additions requested by fox:

1. Methodology is now explicit: GNU assembler (GAS, AT&T syntax),
   Intel Core i5-8350U 8th-gen mobile, Ubuntu 24.04, Linux 6.17,
   gcc 13.3, as 2.42, Python 3.12. Loopback TCP for all socket
   benchmarks. Same hardware across every benchmark in the paper.

2. §12 opens with the Lean EML proof as the rigor standard. The
   proof is 40× faster than the brute-force numerical verification
   it replaced — that speedup IS the MOAD-0001 story at the proof
   layer. We hold the implementations to the same bar: hot paths
   must be fast for a reason (hash / cache / O(1) invariant), not
   by benchmark luck; correctness must hold for a reason, not
   coincidence.

   The scanner is the second line; building with understanding is
   the first. Noted that the most recent scan found 18 HIGH MOAD-
   0001 candidates in C — all inspected individually turn out to
   be false positives (bounded-depth ancestor walks, hash bucket
   chain walks already O(1) amortized, static 6-element tables,
   one-shot option parsing). The MOAD-0003 Python flags are
   scanner misfires on a non-ContextVar Env.set() method.

   New-work-introduced MOAD-0001 defects: zero. All defects fixed
   in this paper (intern_symbol, _define_record_type,
   bi_string_replace, _tokenize_lines, Env.lookup shortcut) were
   surfaced by other pressures — benchmarks, crashes, portal
   exchanges — not the scanner.

whitepaper/uncommonlisp-whitepaper.rst

@@ -337,7 +337,7 @@ Folding only applies when all operands are compile-time constants & the function
 6. Benchmarks: Three Evaluators vs CPython
 --------------------------------------------
 
-All benchmarks run on the same machine, same Python 3 interpreter. Three columns: tree-walking interpreter (``leval``), bytecode VM (``--fast``), & equivalent CPython. Times are best-of-3 in milliseconds.
+**Methodology.** All benchmarks in this paper run on a single laptop: **Intel Core i5-8350U (8th-gen mobile, 4 cores / 8 threads, 1.70 GHz base)**, Ubuntu 24.04, Linux 6.17, gcc 13.3, GNU assembler 2.42 (GAS AT&T syntax), Python 3.12. Loopback TCP for all socket benchmarks. Three columns below: tree-walking interpreter (``leval``), bytecode VM (``--fast``), & equivalent CPython. Times are best-of-3 in milliseconds. The same hardware is used for the HTTP, RPC, chain, and portal-over-HTTP benchmarks reported later in §11.
 
 6.1 Raw Results
 ^^^^^^^^^^^^^^^^
@@ -713,7 +713,7 @@ All C & Python benchmarks measured in-process (no startup overhead). Assembly ti
 
 **The JIT runs Scheme faster than CPython runs Python.** ``ack(3,4)`` completes in 0.19 ms (JIT) vs 1.3 ms (CPython) — 7× faster. ``sum-to(50000)`` completes in 0.55 ms (JIT) vs 5.5 ms (CPython) — 10× faster. The JIT compiles Scheme AST directly to x86_64 machine code via ``mmap(PROT_EXEC)`` & raw byte emission. It handles ``if``, ``cond``, ``and``, ``or``, ``let``, named-let loops (native ``jmp`` — zero call overhead), ``car``/``cdr``/``cons``, arithmetic, comparisons, & self-recursive calls. Functions that use ``call/cc``, macros, or complex forms fall back to the interpreter.
 
-**The assembly implementation proves the language runs on bare metal.** 4,968 lines of GNU assembler, **22 KB stripped binary**, zero external dependencies. Fourteen Linux syscalls (``read``, ``write``, ``open``, ``close``, ``lseek``, ``mmap``, ``munmap``, ``socket``, ``connect``, ``accept``, ``bind``, ``listen``, ``clock_gettime``, ``exit``) — no libc, no stdlib. A bump allocator with ``heap-snapshot``/``heap-restore`` arena primitives, tag-in-low-3-bits values, **91 builtins** (including ``load``, ports, ``write-file``, ``file->string``, ``portal-save``, ``portal-resume``, the six ``tcp-*`` socket primitives, ``read-from-string``, ``eval``, ``symbol->string``, ``current-time-ms``), & TCO via ``jmp``. It runs ``(ack 3 4) = 125`` & ``(fib 35) = 9227465`` correctly, serves HTTP at **2,994 req/s**, and survives indefinitely with flat O(1) memory when the programmer uses the snapshot/restore arena in a per-request loop.
+**The assembly implementation proves the language runs on bare metal.** 4,968 lines of **GNU assembler (GAS, AT&T syntax)**, **22 KB stripped binary**, zero external dependencies. Fourteen Linux syscalls (``read``, ``write``, ``open``, ``close``, ``lseek``, ``mmap``, ``munmap``, ``socket``, ``connect``, ``accept``, ``bind``, ``listen``, ``clock_gettime``, ``exit``) — no libc, no stdlib. A bump allocator with ``heap-snapshot``/``heap-restore`` arena primitives, tag-in-low-3-bits values, **91 builtins** (including ``load``, ports, ``write-file``, ``file->string``, ``portal-save``, ``portal-resume``, the six ``tcp-*`` socket primitives, ``read-from-string``, ``eval``, ``symbol->string``, ``current-time-ms``), & TCO via ``jmp``. It runs ``(ack 3 4) = 125`` & ``(fib 35) = 9227465`` correctly, serves HTTP at **2,994 req/s**, and survives indefinitely with flat O(1) memory when the programmer uses the snapshot/restore arena in a per-request loop.
 
 **The bytecode VM delivers 7--19× speedup over tree-walking.** The Python implementation compiles Scheme to 40 opcodes (plus 20 specialized & 5 superinstructions), executed on an explicit frame stack with inline caching, constant folding, & peephole optimization. Full first-class continuations (multi-shot, upward) enable generators, coroutines, & machine state migration via portal.
 
@@ -910,6 +910,10 @@ This is not a general-purpose allocator. It is an escape hatch the programmer us
 
 We scanned all three implementations for the five MOADs. Every project contains its own sediment.
 
+**Standard: what the Lean EML proof sets.** §8 documents a formal Lean 4 proof that ``eml(x, y) = exp(x) - ln(y)`` generates every elementary function — and that the proof is 40× faster than the brute-force numerical verification it replaced. That speedup is the MOAD-0001 story in microcosm: algebraic understanding beats O(N²) search, at the proof layer just like at every other layer. We take that standard as the bar for the implementations too. Every hot path should be fast for a *reason* (a hash, a cache, an O(1) invariant), not because a test didn't happen to hit the slow case. Every behavior should be correct for a reason, not by coincidence. The audit below is where we hold ourselves to that bar.
+
+We also ran the unmoad scanner on the full tree at each release. Most recent scan (2026-04-17, post portal-over-HTTP): 18 HIGH MOAD-0001 candidates in C and 4 MOAD-0003 candidates in Python. All 18 C candidates inspected individually turn out to be false positives — one-shot option parsing, bounded-depth ancestor walks, hash bucket chain walks (already O(1) amortized), or static 6-element tables (e.g. ``#\space`` char-literal names). The 4 Python MOAD-0003 candidates are scanner misfires on a non-ContextVar ``Env.set()`` method. New-work-introduced MOAD-0001: **zero**. The defects fixed in this paper (``intern_symbol``, ``_define_record_type``, ``bi_string_replace``, ``_tokenize_lines``, ``Env.lookup`` shortcut) were all surfaced by other pressures — benchmarks, crashes, portal exchanges — not by the scanner. The scanner remains a second line; the first line is building with understanding.
+
 12.1 MOAD-0001: The Sedimentary Defect in Our Own Code
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^