[FawadHa1der]

This adds a fourth contender to the race: the same Lean apps, run by Lean's own interpreter inside QED64's wasm64 build of Lean 4.35, in a Web Worker. It also makes the race's lanes modules. The new lane lives in qed64/, apart from everything else, like vir/. It is optional: off unless a visitor ticks "Add Lean's interpreter on QED64 (about 42 MB)" under the race, or asks for it with ?lanes=.

What the lane is

• Host program: QED64's lean.wasm runs lean --run on a small host program (qed64/LeanUIQed/Host.lean). The host reads events from stdin and writes LeanUI's update buffers to stdout, through a shared-memory ring and a stdout tap in the Worker. The page applies the buffers with the unchanged runtime/leanui.js.
• What is interpreted: LeanUI, the diff and the apps run in Lean's IR interpreter. Only Init and Std run as compiled code, inside lean.wasm.
• What the browser downloads: the pinned runtime (lean.wasm 106 MB, 11.0 MB with brotli) and one header snapshot of the apps (114 MB, 30.9 MB gzipped). That is 41.9 MB per session, cached afterwards.
• What is fetched and built: everything is fetched and verified from qed64/qed64.lock.json (sha256 per chunk, two sources). The Std modules, the shimmed LeanUI and the snapshot are built by lean.wasm itself. Nothing large is committed.
• The LeanUI shim: a copy of LeanUI with its two inline-C helpers made plain Lean, because the interpreter cannot run inline C. The output is byte-identical.

Pluggable lanes (bench/race/lanes.mjs)

The race reads its lanes from a registry. A lane can be:

• optional: offered as a box only where its page was built;
• asynchronous: the referee awaits window.__idle() after each click, and clicks nothing else meanwhile, so the time still runs from the click to the page updated.

A lane can also report its own figures: downloads, start phases, and Lean / transport / DOM time. The three existing lanes behave and measure as before.

Checks

• qed64/test/node.mjs (Node 24): the lane's updates are byte-identical to a compiled reference host in all 8 scenarios. It also runs the 10,000-row create under a 0.49 MiB pthread stack, and 20 empty pings.
• tests/browser/race.mjs --lanes vanilla,wasm64,vir,qed64:
  • Chromium: Life and the table. All four lanes agree after every operation, with no stalls.
  • Firefox: Life.
• CI: builds the lane cold with caches (about 3–4 minutes extra cold, cached after), runs the Node test and the four-lane race, and smoke-tests the lane in the site container.
• Review: an adversarial review found five small problems, all fixed:
  • the snapshot copy is now freed after the mount;
  • a failed lane is reported at once;
  • QED64=0 is honoured;
  • the lane's credits show only when it was built;
  • two README slips.

Numbers

CI machine, to be re-measured on the reference Mac.

Chromium, ms per click (vanilla / wasm64 / lean-vir / QED64):

Operation	vanilla	wasm64	lean-vir	QED64
Life step	0.06	0.55	14.6	15.3
create 1,000 rows	5.1	9.4	154	141
create 10,000 rows	39	89	1532	1395

• QED64 is about as fast as lean-vir: two interpreters, side by side.
• Of a Life step's 15.3 ms, 14.4 is Lean, 0.8 the Worker round trip and 0.1 the DOM.
• The lane is ready about 1.8 s after its page loads.
• Memory: about 500 MB of renderer memory in Chromium, about 1.3 GB in Firefox.
• Firefox: boots in about 9 s, almost all of it compiling the wasm.

The site

• Route: /race/qed64-rt/ is served immutable and cross-origin isolated, like /race/.
• Staging: stage.sh keeps the lane's prebuilt brotli and gzip files.
• Container size: the container grows by about 165 MB.
• Container memory: the server reads a whole file per response, so a burst of visitors adding the lane costs container memory (8 at once: 128 → 363 MiB). docs/DEPLOY.md notes this. An edge cache in the Worker is a possible follow-up.

🤖 Generated with Claude Code

https://claude.ai/code/session_016R1ctPHanJvc74mwoJrYgd