[FawadHa1der]

A follow-up to #6 with two small fixes. A review of the site version, run while #6 was merging, found both.

• examples/roster.html: the site now links the Roster app, which needs WebAssembly Memory64. In a browser without it (Safari), the page used to show the raw "LeanUI failed to start" error. It now shows the same plain message as the photo editor (examples/editor.html). The verify page is wasm32 and works in Safari regardless.
• examples/Site.lean: the Examples blurb said "a roster comes with a proof", but the site has no notary. It now says what the site has: one roster notarized when the site was built, which an independent kernel checks again in your browser.

Checks

• lake build leanui-site passes.
• tests/browser/roster.mjs passes in Chromium with the new page (84 checks).
• Not tested in Safari: no Safari here.
• CI runs on this PR.

---

Generated by Claude Code

[FawadHa1der]

Final summary (stop time, 2026-10-22 18:00 UTC)

This PR has two small fixes to the Roster demo on the site:

• a plain "needs Memory64" message, instead of the raw start error, in browsers without Memory64 (Safari);
• an exact Examples blurb: the site has no notary, only one roster notarized when it was built.

A review of the site version, run while #6 was merging, found both. Checked locally:

• lake build leanui-site passes;
• tests/browser/roster.mjs passes in Chromium on the new page (84 checks).

It is a draft, and CI run 39826434271 had not finished at stop time.

What this session did: #6, the Roster demo, merged at 17:38 UTC.

• The app: an untrusted solver, a lying-solver switch, and a checker proved sound and complete (Hall's theorem, from Mathlib). The proof steps_inv covers the model; the view that draws it is tested.
• The notary (leanui-roster, Lean 4.35 plus leanexport).
• The verify page: nanoda as wasm32-wasip1, four checks, and a tamper button.
• The site serves it at /roster/ without a notary: one receipt made at staging, and a "no notary" answer linking to it.

CI

• Run 39824067827 on Roster: a proof-carrying staffing sheet (proved checker, lying solver, notary, verify page) #6's last commit (4501786): green, including the container smoke test with the Roster app's and verify page's browser tests.
• Run 39824488882 on main (d5043e7): at 17:58 every test step had passed, including the Roster Mathlib job and the container smoke test. It was uploading the site container, and the deploy job comes after that. Check that it went live at /roster/ on the site.

Numbers (CI machines, to be re-measured on the reference Mac)

• Notarizing takes about 2.5 s.
• A receipt is 2.0 MB, or 222 kB with brotli.
• Checking it in the browser takes about 0.25 s in Chromium and 0.8–1.2 s in Firefox.
• checker.wasm is 257 KB gzipped.
• The Mathlib job takes about 1.5 min.

Open problems

• The site cannot notarize. That needs Lean 4.35 (lean, leanexport, the core library) in the container.
• Safari is out of scope for the wasm64 app; the verify page works anywhere.
• c′ trusts the verify page as served, as roster/README.md says.

Next steps for you

1. Confirm the deploy of run 39824488882, then open /roster/ and /roster/verify/?receipt=/roster/receipts/feasible.ndjson on the site.
2. Let CI finish here, mark this ready, and merge.
3. Optionally, the full notary on the site as a follow-up.
4. Re-measure the timings on the reference Mac.

---

Generated by Claude Code