Share the browser verifier across LiquidJava sites

README.md

@@ -46,7 +46,7 @@ npm run test:playground
 bundle exec jekyll build
 ```
 
-The build requires JDK 17, Python 3, Node.js, and access to Maven Central. It recompiles the published verifier and annotation API sources for Java 17 without changing them, packages their dependencies, and adds the docs-owned runner and Z3 loader. `scripts/playground/pom.xml` is the single source of truth for the Maven artifact versions; the Python build reads it directly, without requiring Maven. The verifier binary and sources always use the same version. The standard-library classpath comes from the build JDK's `java.base.jmod`. Generated runtime files are ignored by Git and included in the Pages artifact.
+The build requires JDK 17, Python 3, Node.js, and access to Maven Central. It recompiles the published verifier and annotation API sources for Java 17 without changing them, packages their dependencies, and adds the docs-owned runner and Z3 loader. `scripts/playground/pom.xml` is the single source of truth for the Maven artifact versions; the Python build reads it directly, without requiring Maven. The verifier binary and sources always use the same version. The standard-library classpath includes the build JDK's `java.base`, `java.desktop`, `java.datatransfer`, and `java.xml` modules for the gallery's JDK protocols. Generated runtime files are ignored by Git and included in the Pages artifact.
 
 After the configuration is merged into `main`, Dependabot checks the manifest daily and opens update PRs for the LiquidJava verifier and annotation API. Every pull request builds the playground, runs its tests, and builds Jekyll. Review upgrades with browser verification before merging, including successful and failing refinements and typestate transitions. Pages deployment runs only after a push to `main` or a manual workflow run.
 
@@ -62,4 +62,12 @@ Open `http://127.0.0.1:8770/playground/`. This uses a static server with HTTP ra
 
 `playground/isolation.js` is a service worker scoped to `/playground/`. It adds the cross-origin isolation response headers Z3 requires on static hosting, including GitHub Pages. The first visit registers it and reloads once. Other docs pages are outside its scope. CheerpJ loads from its official CDN inside the verification worker; its runtime is not copied into this repository.
 
-The playground checks a single Java file using Java 8 source syntax, bundled annotations and core standard-library types from `java.base`. External dependencies and other Java modules are not available. Z3 4.16 runs behind the verifier's 4.8.17 Java API; browser integration tests must be repeated when updating either version. Unsupported native operations and unknown solver results fail explicitly instead of reporting success. This integration is kept entirely in `liquidjava-docs`.
+The playground checks a single Java file using Java 8 source syntax, bundled annotations and standard-library types from those four JDK modules. External dependencies and other Java modules are not available. Z3 4.16 runs behind the verifier's 4.8.17 Java API; browser integration tests must be repeated when updating either version. Unsupported native operations and unknown solver results fail explicitly instead of reporting success. The shared runtime is maintained in `liquidjava-docs`.
+
+## Shared verifier for the tutorial and website
+
+After `npm run build:playground`, run `node scripts/playground/export.mjs PATH_TO_SITE` to export the generated runtime, compact client, and isolation service worker. Consumers host these files on their own origin; Java code never goes to a verification service. The runtime is maintained here and rebuilt by each consumer’s deployment workflow.
+
+The worker accepts `{ type: 'verify', files: { 'Example.java': source, ... } }`. Each request clears the previous Java files, so specifications cannot leak between examples. The runner returns structured `title` and `message` fields alongside the playground’s full diagnostics. The exported `BrowserVerifier` client exposes only the compact results, handles loading/timeouts/cancellation, and reuses the initialized worker for subsequent checks.
+
+Call `prepareVerifier()` before mounting editable content: it prepares cross-origin isolation and performs the first-visit reload before edits are possible. Exported sites scope `isolation.js` to their site root; the docs playground keeps its own narrower scope. Runtime assets load on the first verification request.

playground/isolation.js

@@ -1,8 +1,12 @@
-// GitHub Pages cannot set these response headers; isolate only the playground.
+// GitHub Pages cannot set these headers; isolate pages within this worker’s scope.
 self.addEventListener('install', () => self.skipWaiting());
 self.addEventListener('activate', event => event.waitUntil(self.clients.claim()));
 self.addEventListener('fetch', event => {
-  if (new URL(event.request.url).origin !== self.location.origin) return;
+  const url = new URL(event.request.url);
+  if (url.origin !== self.location.origin) return;
+  // a root-hosted website must not isolate neighboring GitHub Pages projects
+  const relative = url.pathname.slice(new URL('./', self.location.href).pathname.length);
+  if (event.request.mode === 'navigate' && relative.includes('/')) return;
   event.respondWith((async () => {
     const response = await fetch(event.request);
     if (response.type === 'opaque') return response;

scripts/playground/build.py

@@ -89,10 +89,13 @@ def main():
             out.writestr(item.filename, jar.read(item.filename))
         for file in classes.rglob('*.class'):
             out.writestr(file.relative_to(classes).as_posix(), file.read_bytes())
-    with zipfile.ZipFile(java_home / 'jmods/java.base.jmod') as jar, zipfile.ZipFile(OUTPUT / 'java-base.jar', 'w', zipfile.ZIP_DEFLATED) as out:
-        for name in jar.namelist():
-            if name.startswith('classes/') and name.endswith('.class') and name != 'classes/module-info.class':
-                out.writestr(name[len('classes/'):], jar.read(name))
+    with zipfile.ZipFile(OUTPUT / 'java-base.jar', 'w', zipfile.ZIP_DEFLATED) as out:
+        # include the JDK types used by the website's Swing and image examples
+        for module in ['java.base', 'java.desktop', 'java.datatransfer', 'java.xml']:
+            with zipfile.ZipFile(java_home / f'jmods/{module}.jmod') as jar:
+                for name in jar.namelist():
+                    if name.startswith('classes/') and name.endswith('.class') and name != 'classes/module-info.class':
+                        out.writestr(name[len('classes/'):], jar.read(name))
     with zipfile.ZipFile(z3_sources) as jar:
         native = jar.read('com/microsoft/z3/Native.java').decode()
     methods = []

scripts/playground/client.mjs

@@ -0,0 +1,92 @@
+import { summarize } from './summary.mjs';
+
+// Called before editors are mounted so the first isolation reload cannot lose edits.
+export async function prepareVerifier() {
+  const key = 'liquidjava-isolation:' + new URL('../', import.meta.url).pathname;
+  if (globalThis.crossOriginIsolated) {
+    sessionStorage.removeItem(key);
+    return;
+  }
+  if (!globalThis.isSecureContext || !navigator.serviceWorker) {
+    throw new Error('Verification requires HTTPS and a browser with cross-origin isolation support.');
+  }
+  if (sessionStorage.getItem(key)) {
+    throw new Error('This browser could not enable verification. Try a current Chrome, Firefox or Safari browser.');
+  }
+  const script = new URL('../isolation.js', import.meta.url);
+  await navigator.serviceWorker.register(script, {
+    scope: new URL('../', import.meta.url).pathname, updateViaCache: 'none'
+  });
+  await new Promise((resolve, reject) => {
+    const finish = error => {
+      clearTimeout(timer);
+      navigator.serviceWorker.removeEventListener('controllerchange', controlled);
+      if (error) reject(error); else resolve();
+    };
+    const controlled = () => {
+      if (navigator.serviceWorker.controller?.scriptURL === script.href) finish();
+    };
+    const timer = setTimeout(() => finish(new Error('The browser could not prepare verification. Reload and try again.')), 15000);
+    navigator.serviceWorker.addEventListener('controllerchange', controlled);
+    controlled();
+  });
+  sessionStorage.setItem(key, 'reload');
+  location.reload();
+  await new Promise(() => {});
+}
+
+export class BrowserVerifier {
+  worker;
+  pending;
+  timer;
+
+  cancel() {
+    clearTimeout(this.timer);
+    this.worker?.terminate();
+    this.worker = undefined;
+    this.pending?.reject(new DOMException('Verification stopped.', 'AbortError'));
+    this.pending = undefined;
+  }
+
+  verify(files, onStatus = () => {}) {
+    if (this.pending) throw new Error('Verification is already running.');
+    if (!globalThis.crossOriginIsolated || typeof SharedArrayBuffer === 'undefined') {
+      return Promise.reject(new Error('This browser cannot start the verifier. Reload the page and try again.'));
+    }
+    return new Promise((resolve, reject) => {
+      this.pending = { resolve, reject };
+      const fail = message => {
+        this.pending?.reject(new Error(message));
+        this.pending = undefined;
+        this.cancel();
+      };
+      const send = () => {
+        clearTimeout(this.timer);
+        onStatus('Verifying…');
+        this.timer = setTimeout(() => fail('Verification timed out. Simplify the example and try again.'), 60000);
+        this.worker.postMessage({ type: 'verify', files });
+      };
+      if (this.worker) { send(); return; }
+      onStatus('Downloading and starting the verifier. This may take a moment…');
+      this.timer = setTimeout(() => fail('The verifier took too long to load. Check your connection and try again.'), 120000);
+      try { this.worker = new Worker(new URL('./worker.js', import.meta.url)); }
+      catch { fail('The verifier could not start. Reload the page and try again.'); return; }
+      const current = this.worker;
+      current.onerror = () => {
+        if (this.worker === current) fail('The verifier could not start. Reload the page and try again.');
+      };
+      current.onmessage = ({ data }) => {
+        if (this.worker !== current) return;
+        if (data.type === 'status') onStatus(data.message);
+        if (data.type === 'ready') send();
+        if (data.type === 'failure') fail(data.message);
+        if (data.type === 'result') {
+          clearTimeout(this.timer);
+          this.pending.resolve(summarize(data.result));
+          this.pending = undefined;
+          if (data.result.status === 'failure') this.cancel();
+        }
+      };
+    });
+  }
+}

scripts/playground/client.test.mjs

@@ -0,0 +1,50 @@
+import test from 'node:test';
+import assert from 'node:assert/strict';
+import { BrowserVerifier } from './client.mjs';
+
+class Worker {
+  static instances = [];
+  constructor() { Worker.instances.push(this); }
+  postMessage(data) { this.sent = data; }
+  terminate() { this.terminated = true; }
+  emit(data) { this.onmessage({ data }); }
+}
+
+test('reuse a ready worker with new files and compact results', async t => {
+  globalThis.Worker = Worker;
+  globalThis.crossOriginIsolated = true;
+  t.after(() => { delete globalThis.Worker; delete globalThis.crossOriginIsolated; });
+  const client = new BrowserVerifier();
+  const first = client.verify({ 'A.java': 'class A {}' });
+  const worker = Worker.instances.at(-1);
+  worker.emit({ type: 'ready' });
+  assert.equal(worker.sent.files['A.java'], 'class A {}');
+  worker.emit({ type: 'result', result: { status: 'success', diagnostics: [] } });
+  assert.equal((await first).status, 'success');
+  const second = client.verify({ 'B.java': 'class B {}' });
+  assert.deepEqual(worker.sent.files, { 'B.java': 'class B {}' });
+  worker.emit({ type: 'result', result: { status: 'error', diagnostics: [{ title: 'Error', message: 'Bad value', output: 'full output' }] } });
+  assert.deepEqual((await second).diagnostics, [{ title: 'Error', message: 'Bad value' }]);
+  client.cancel();
+});
+
+test('cancellation terminates workers and late results cannot settle a later request', async t => {
+  globalThis.Worker = Worker;
+  globalThis.crossOriginIsolated = true;
+  t.after(() => { delete globalThis.Worker; delete globalThis.crossOriginIsolated; });
+  const client = new BrowserVerifier();
+  const first = client.verify({ 'A.java': '' });
+  const old = Worker.instances.at(-1);
+  const cancelled = assert.rejects(first, { name: 'AbortError' });
+  client.cancel();
+  await cancelled;
+  assert.ok(old.terminated);
+  const next = client.verify({ 'B.java': '' });
+  const current = Worker.instances.at(-1);
+  old.emit({ type: 'result', result: { status: 'success', diagnostics: [] } });
+  assert.ok(client.pending);
+  current.emit({ type: 'ready' });
+  current.emit({ type: 'failure', message: 'Solver unavailable' });
+  await assert.rejects(next, /Solver unavailable/);
+  assert.ok(current.terminated);
+});

scripts/playground/editor.js

@@ -84,7 +84,7 @@ function send() {
   clearTimeout(timer);
   message('Verifying…');
   timer = setTimeout(() => failure('Verification timed out. Simplify the example and try again.'), 30000);
-  worker.postMessage({ type: 'verify', source });
+  worker.postMessage({ type: 'verify', files: { 'Example.java': source } });
 }
 async function run() {
   if (checking || loading) return;

scripts/playground/export.mjs

@@ -0,0 +1,16 @@
+import { copyFile, mkdir } from 'node:fs/promises';
+import { resolve } from 'node:path';
+import { fileURLToPath } from 'node:url';
+
+const destination = process.argv[2];
+if (!destination) throw new Error('Usage: node scripts/playground/export.mjs SITE_DIRECTORY');
+const root = fileURLToPath(new URL('../../', import.meta.url));
+const runtime = resolve(destination, 'verifier');
+await mkdir(runtime, { recursive: true });
+for (const file of ['worker.js', 'liquidjava.jar', 'java-base.jar', 'native-methods.json', 'z3-built.js', 'z3-built.wasm']) {
+  await copyFile(resolve(root, 'playground/runtime', file), resolve(runtime, file));
+}
+for (const file of ['client.mjs', 'summary.mjs']) {
+  await copyFile(new URL(file, import.meta.url), resolve(runtime, file));
+}
+await copyFile(resolve(root, 'playground/isolation.js'), resolve(destination, 'isolation.js'));

scripts/playground/isolation.test.mjs

@@ -0,0 +1,25 @@
+import test from 'node:test';
+import assert from 'node:assert/strict';
+import { readFile } from 'node:fs/promises';
+import { runInNewContext } from 'node:vm';
+
+const source = await readFile(new URL('../../playground/isolation.js', import.meta.url), 'utf8');
+
+test('root isolation leaves neighboring Pages projects unchanged', async () => {
+  const listeners = {};
+  runInNewContext(source, {
+    self: { location: new URL('https://example.com/isolation.js'), addEventListener: (type, listener) => { listeners[type] = listener; } },
+    URL, Headers, Response, fetch: async () => new Response('body')
+  });
+  const response = async (path, mode = 'navigate') => {
+    let pending;
+    listeners.fetch({ request: { url: new URL(path, 'https://example.com').href, mode }, respondWith: value => { pending = value; } });
+    return pending;
+  };
+  assert.equal((await response('/')).headers.get('Cross-Origin-Embedder-Policy'), 'require-corp');
+  assert.equal((await response('/states')).headers.get('Cross-Origin-Opener-Policy'), 'same-origin');
+  assert.equal((await response('/verifier/worker.js', 'same-origin')).headers.get('Cross-Origin-Embedder-Policy'), 'require-corp');
+  assert.equal(await response('/liquidjava-docs/'), undefined);
+  assert.equal(await response('/liquidjava-docs/annotations/'), undefined);
+  assert.equal(await response('https://other.example/'), undefined);
+});

scripts/playground/java/liquidjava/playground/BrowserRunner.java

@@ -1,10 +1,12 @@
 package liquidjava.playground;
 
 import com.google.gson.Gson;
+import com.google.gson.reflect.TypeToken;
 import java.nio.file.Files;
 import java.nio.file.Path;
 import java.util.ArrayList;
 import java.util.LinkedHashMap;
+import java.util.List;
 import java.util.Map;
 import liquidjava.diagnostics.Diagnostics;
 import liquidjava.diagnostics.LJDiagnostic;
@@ -26,32 +28,45 @@
 import spoon.support.compiler.jdt.JDTBasedSpoonCompiler;
 
 public final class BrowserRunner {
-    public static String verify(String source, String jar, String javaBase) {
+    public static String verify(String sources, String jar, String javaBase) {
         Map<String, Object> result = new LinkedHashMap<>();
         ArrayList<Map<String, Object>> issues = new ArrayList<>();
         try {
             Path dir = Path.of("/files/playground");
             Files.createDirectories(dir);
-            Path input = dir.resolve("Example.java");
-            Files.writeString(input, source);
+            try (var previous = Files.list(dir)) {
+                for (Path file : previous.toList()) Files.delete(file);
+            }
+            Map<String, String> files = new Gson().fromJson(sources, new TypeToken<Map<String, String>>() {}.getType());
+            if (files == null || files.isEmpty()) throw new IllegalArgumentException("No Java files supplied");
+            List<String> inputs = new ArrayList<>();
+            for (var file : files.entrySet()) {
+                if (!file.getKey().matches("[A-Za-z_$][A-Za-z0-9_$]*\\.java"))
+                    throw new IllegalArgumentException("Invalid Java filename");
+                Path input = dir.resolve(file.getKey());
+                Files.writeString(input, file.getValue());
+                inputs.add(input.toString());
+            }
             Diagnostics.getInstance().clear();
             ContextHistory.getInstance().clearHistory();
             Launcher launcher = new Launcher();
-            launcher.addInputResource(input.toString());
+            launcher.addInputResource(dir.toString());
             launcher.getEnvironment().setNoClasspath(true);
             launcher.getEnvironment().setComplianceLevel(8);
             launcher.getEnvironment().setSourceClasspath(new String[] {jar});
             JDTBuilder builder = new JDTBuilderImpl()
                 .classpathOptions(new ClasspathOptions().classpath(jar).bootclasspath(javaBase))
                 .complianceOptions(new ComplianceOptions().compliance(8))
                 .advancedOptions(new AdvancedOptions().preserveUnusedVars().continueExecution().enableJavadoc())
-                .sources(new SourceOptions().sources(input.toString()));
+                .sources(new SourceOptions().sources(inputs.toArray(String[]::new)));
             JDTBasedSpoonCompiler compiler = (JDTBasedSpoonCompiler) launcher.getModelBuilder();
             boolean built = compiler.build(builder);
             for (CategorizedProblem problem : compiler.getProblems()) {
                 if (!problem.isError()) continue;
                 Map<String, Object> issue = new LinkedHashMap<>();
                 issue.put("severity", "error");
+                issue.put("title", "Java error");
+                issue.put("message", problem.getMessage());
                 issue.put("output", problem.toString());
                 issue.put("line", problem.getSourceLineNumber());
                 issue.put("from", problem.getSourceStart());
@@ -84,6 +99,8 @@ public static String verify(String source, String jar, String javaBase) {
     private static Map<String, Object> issue(LJDiagnostic issue, String severity) {
         Map<String, Object> result = new LinkedHashMap<>();
         result.put("severity", severity);
+        result.put("title", issue.getTitle());
+        result.put("message", issue.getMessage());
         result.put("output", issue.toString());
         if (issue.getPosition() != null && issue.getPosition().isValidPosition()) {
             result.put("line", issue.getPosition().getLine());

scripts/playground/summary.mjs

@@ -0,0 +1,8 @@
+export function summarize(result) {
+  if (result.status === 'failure') {
+    return { status: 'failure', diagnostics: [{ title: 'Verification could not complete', message: result.message || 'Please try again.' }] };
+  }
+  const diagnostics = result.diagnostics.map(({ title, message }) => ({ title, message }));
+  if (!diagnostics.length) diagnostics.push({ title: 'Verification passed', message: 'All refinements verified.' });
+  return { status: result.status, diagnostics };
+}