.github/workflows/wai-web-wasm.yml

@@ -169,14 +169,15 @@ jobs:
       # critique, equivalence and variants as JSON, the classical shortcuts, the
       # workbench run and sealed in the page, a program's history recorded and
       # blamed there, the reader's rules checking a proposal, what is new in a
-      # program and in a workbench entry, and the reader's taste learned there.
+      # program and in a workbench entry, the reader's taste learned there, the
+      # rewrites offered and explained there, and convergence measured there.
       - name: The job engine in a page (native unit tests)
         shell: bash
         working-directory: wai/wai-web
         run: |
           set -euo pipefail
           cargo test --locked --lib --features quantum_engine quantum_engine:: 2>&1 | tee "$RUNNER_TEMP/wai-web-engine.log"
-          grep -q "test result: ok. 11 passed; 0 failed" "$RUNNER_TEMP/wai-web-engine.log"
+          grep -q "test result: ok. 13 passed; 0 failed" "$RUNNER_TEMP/wai-web-engine.log"
       # The crate's native unit tests, run on the host: the pure-Rust halves of the
       # bindings, which wasm_tests does not run. They decode the committed integer
       # payloads to their sidecars' SHA-256 (int_payload::tests) and check that the

joule-code/joule-code-rs/crates/joule-moq-room/Cargo.lock

@@ -3436,7 +3436,7 @@ version = "0.1.0"
 
 [[package]]
 name = "wai-quantum"
-version = "0.6.15"
+version = "0.6.16"
 dependencies = [
  "blake3",
  "ed25519-dalek",

wai/CHANGELOG.md

@@ -1562,6 +1562,48 @@ wire format may change and such changes are recorded here.
 - **`tools/ops-gpu-bench`** times each capability's decode with its graphs on the CPU and on each adapter, and reads the energy counters the host has.
 - **CI:** `wai-ops-gpu.yml` runs the Metal and browser legs on the `macos` runner, and requires on a runner with no GPU that the device tests skip without `WAI_OPS_GPU_REQUIRE` and fail with it.
 
+### wai-quantum 0.6.16 and wai-quantum-cli 0.1.4: the person's rules, what is new, taste, rewrites and convergence
+
+This release carries the five entries below it to the package registry, and 0.6.15's with them: 0.6.15 and 0.1.3 went out as binaries and to the package taps only. `wai-quantum-cli` 0.1.4 requires 0.6.16.
+
+- **wai-quantum 0.6.16:**
+  - the person's rules for proposals (`engine::locks`), with the blocked changes kept in a version's review;
+  - what is new in a program, the known constructions found again, and aberrations (`engine::novelty`, `discover::novelty`);
+  - a person's taste, learned from their own choices between programs proved equal (`engine::taste`);
+  - rewrites, each checked on the qubits they touch, and equivalence proved by them at any width (`engine::rewrite`; `equiv::equivalent_programs` answers `how: rewrites`);
+  - whether designs converge on a model's, and a cohort's diversity (`engine::converge`).
+- **wai-quantum-cli 0.1.4:**
+  - `locks check | brief`, `novelty`, `discover novelty`, `taste choose | show | rank | next`, `rewrite options | apply | simplify | explain` and `converge history | cohort`;
+  - the MCP tools `novelty_qasm`, `discover_novelty`, `rewrite_qasm`, `converge_cohort`, `converge_history`, `taste_rank` and `taste_next`, and `history_commit` refusing an edit that breaks the person's rules.
+- The desktop app requires 0.6.16 too. Every lockfile that holds wai-quantum or wai-quantum-cli moves with them, so a `--locked` build still reads its own.
+
+### wai-quantum: whether designs converge on a model's, and a while on one's own
+
+Feature 12 of the co-design report: a convergence monitor.
+
+- **Along a history** (`converge::history`): for each version the person made after a model proposed, its structural distance from the proposals in its line of work (the whole proposal, taken or not) and the model's share of its gates (alone or then edited by the person). It is converging when most of the program is the model's, or when the last versions come closer to the proposals each time; `why` says which.
+- **The assistant-off probes:** versions noted `organic exploration` are set beside the rest, by their distance from the proposals.
+- **A cohort** (`converge::cohort`): the Vendi score over `1 − distance` (Jacobi eigenvalues), the effective number of distinct designs; each program's distance to the centroid of their gate-token bags; the medoid and the one built least like the rest; with times, the score in windows and whether it narrows.
+- **The command line:** `wai-quantum converge history | cohort`.
+- **For agents:** `converge_cohort` and `converge_history`.
+- **The Studio:** "Your own way" under Versions, and "Explore on my own for a while". While it is on, the assistant only asks and offers no program, Explore and "Ask the model" wait, and the person's versions are noted; "End" lets the model propose again.
+- **For hosts:** `converge::call`, `engine_converge` in the page, `converge` in the desktop app.
+- **CI:** wai-web's native engine tests count 13.
+
+### wai-quantum: rewrites, each checked, and equivalence proved by them at any width
+
+Feature 11 of the co-design report: a verified-rewrite lens shared by the person and the assistant, and the general equivalence check it needs first.
+
+- **The rewrites** (`engine::rewrite`): a gate and its inverse cancel; two rotations about one axis merge, and the phase gates add up (`t t` is `s`); a gate between two Hadamards becomes its conjugate (`h x h` is `z`, `h cx h` on the target is `cz`); a gate that does nothing is dropped; a gate is carried past gates it commutes with to cancel or merge with its partner; two gates that commute trade places. The rules propose and the engine decides: each rewrite's gates are checked against its replacement on just the qubits they touch, by tableau or on every basis state (`equiv::proved_equal`), so no rule is trusted.
+- **Equivalence proved by rewriting** (`rewrite::prove`): one program followed by the other's inverse is rewritten toward nothing. When nothing is left, the two are the same unitary up to a global phase at any width and with any gates. `equiv::equivalent_programs` now tries it after the exact check and before random inputs, answering `how: rewrites`, which the workbench and the taste model count as a proof. When it does not reduce, nothing is concluded and the next check runs.
+- **A chain** (`rewrite::explain`): both programs simplified to a fixed point and compared, gate for gate or, where they differ only in the order of gates that commute, by a proof. Each step is in words.
+- **The lens** (`rewrite::options`): every rewrite a program admits as an edit to its own lines (a merge writes `rz(0.25 + 0.5)`, comments stay), read back and compared gate for gate before it is offered. A generator is rewritten as the circuit it writes out.
+- **The command line:** `wai-quantum rewrite options | apply | simplify | explain`.
+- **For agents:** `rewrite_qasm`.
+- **The Studio:** "Rewrites" under the circuit (each rewrite in words, its gates marked on the diagram, "Take" to offer it as the engine's proposal, the list following the program); Alternatives says how the draft becomes a candidate that is the same circuit, as a chain; an equivalence proved by rewriting reads "by checked rewrites".
+- **For hosts:** `rewrite::call`, `engine_rewrite` in the page, `rewrite` in the desktop app.
+- **CI:** wai-web's native engine tests count 12.
+
 ### wai-quantum: a person's taste, learned from their own choices between equals
 
 Feature 10 of the co-design report: a personal, plural taste model.

wai/quantum-studio/README.md

@@ -39,6 +39,10 @@ The Workbench searches a family of circuits for its cheapest members, and the en
 
 A proposal is verified only when it reads, keeps the rules and passes the check at every size. Each kept entry is sealed with this browser's key (the desktop app's, in the app). Clicking a point shows its cost, how it was checked, its seal and where it came from; "Open in editor" puts it in the editor. The archive is kept in this browser and comes back with the page. "Download" saves the specification and its archive side by side (`NAME.json` and `NAME.archive.json`), so `wai-quantum discover verify NAME.json` checks every seal. In the desktop app a search also counts its seconds and the joules its process spent.
 
+## Rewrites
+
+"Rewrites", under the circuit, lists every rewrite the program admits that keeps its meaning: gates that cancel, rotations that merge, a gate between two Hadamards that becomes its conjugate, a gate carried past what it commutes with, two gates that trade places. The engine checks each one on the qubits it touches. Pointing at a rewrite marks its gates on the diagram; "Take" offers it as the engine's proposal, reviewed like any other, and the list follows the program as it changes. In Alternatives, a candidate that is the same circuit as the draft says how the draft becomes it, as a chain of checked rewrites.
+
 ## What is new, and Found
 
 The engine says what is new in a program: the known construction it is, found again; a known result reached by a different route; or how far it is from the nearest program it was compared with. The known constructions are GHZ by a chain, by doubling and by fan-out, the uniform superposition and the quantum Fourier transform. The distance is structural, from 0 (built alike) to 1 (nothing shared), and it is the engine's, not a search of the literature.
@@ -47,6 +51,16 @@ The engine says what is new in a program: the known construction it is, found ag
 - **The Workbench:** each kept generator is named for what it is, and its entry shows it with the measures it beats the reference on that the cost does not weigh. A candidate that breaks only one rule of the specification (a gate, or the line) and would be verified without it is an aberration. It is never kept: the log says what it would cost, and "Try without that rule" loosens the specification, for a new archive under it.
 - **Found** keeps what is worth a second look: a different route to a known result, an aberration, a verified entry far from everything it was compared with. Each can be opened in the editor, saved with a note, or dismissed. Its count says how many were flagged and how many saved. It is kept in this browser.
 
+## Your own way
+
+Under Versions, "Your own way" says whether your versions are converging on the model's proposals: how far your latest is built from them, and how much of the program is the model's. "Explore on my own for a while" pauses the model while you work:
+
+- the assistant only asks questions, and does not offer its programs;
+- Alternatives' Explore and the Workbench's "Ask the model" wait;
+- the versions you make are noted as made on your own, and the line sets their distance from the proposals beside the rest.
+
+"End" lets the model propose again. The mode is kept in this browser.
+
 ## Your taste
 
 "Your taste", in the Workbench, learns what you prefer from your own choices:

wai/quantum-studio/src/assistant.js

@@ -45,7 +45,7 @@ export const TOOLS = [
   { type: 'function', function: { name: 'get_program', description: 'The program in the editor, the job settings, and a summary of the last result.', parameters: { type: 'object', properties: {} } } },
   { type: 'function', function: { name: 'lint_qasm', description: 'Read an OpenQASM program as the engine reads it: its qubits, gates and measurements, or the first problem with its line.', parameters: { type: 'object', required: ['qasm'], properties: { qasm: { type: 'string' } } } } },
   { type: 'function', function: { name: 'critique_qasm', description: 'A program\'s measures (gates by kind, two-qubit gates, depth, two-qubit depth, T count, whether it is a Clifford circuit, a fidelity under reference error rates, which is a model and not a run) and its smells: gates that cancel, rotations that merge or do nothing, idle or unmeasured qubits, each with its lines.', parameters: { type: 'object', required: ['qasm'], properties: { qasm: { type: 'string' } } } } },
-  { type: 'function', function: { name: 'check_equivalent', description: 'Whether two programs are the same circuit up to a global phase, and how the engine knows: equal tableaus (Clifford, any size), every basis state (to 8 qubits), random inputs (to 22 qubits, evidence rather than proof), or unchecked. b defaults to the program in the editor.', parameters: { type: 'object', required: ['a'], properties: { a: { type: 'string' }, b: { type: 'string' } } } } },
+  { type: 'function', function: { name: 'check_equivalent', description: 'Whether two programs are the same circuit up to a global phase, and how the engine knows: equal tableaus (Clifford, any size), every basis state (to 8 qubits), checked rewrites to nothing (a proof at any width), random inputs (to 22 qubits, evidence rather than proof), or unchecked. b defaults to the program in the editor.', parameters: { type: 'object', required: ['a'], properties: { a: { type: 'string' }, b: { type: 'string' } } } } },
   { type: 'function', function: { name: 'classical_shortcuts', description: 'Every exact classical route the engine knows for simulating a program (stabilizer tableau, cut-rank sum, exact matrix product state at a rigorous bond bound, light cone, tensor network when thorough, state vector), each with its memory and the log2 of its operations, and the cheapest for each question. A cheap route proves the program classically easy; none being cheap proves nothing about hardness.', parameters: { type: 'object', properties: { qasm: { type: 'string' }, thorough: { type: 'boolean' } } } } },
   { type: 'function', function: { name: 'novelty_qasm', description: 'What is new in a program: its structural distance, 0 (built alike) to 1 (nothing shared), from the known constructions (GHZ by a chain, by doubling and by fan-out; the uniform superposition; the quantum Fourier transform) and from the program in the editor, the nearest named; and each known construction the engine proves it to be (the same state, or the same circuit), built alike or by a different route. A high distance is a reason to look, not a claim that nobody has built it. qasm defaults to the program in the editor.', parameters: { type: 'object', properties: { qasm: { type: 'string' } } } } },
   { type: 'function', function: { name: 'draw_circuit', description: 'A program\'s circuit drawn as text.', parameters: { type: 'object', required: ['qasm'], properties: { qasm: { type: 'string' } } } } },

wai/quantum-studio/src/converge.js

@@ -0,0 +1,74 @@
+// Whether the reader's designs converge on the assistant's (engine::converge),
+// and exploring on one's own.
+//
+// Along the program's history, each version the reader made after a model
+// proposed is set against the proposals in its line of work: how far it is
+// built from them, and how much of the program is the model's. When that
+// converges, the Studio offers a while on one's own: the assistant only asks,
+// Alternatives and the Workbench do not ask the model, and the versions the
+// reader makes are noted, so what they made alone is set beside the rest.
+// Nothing leaves this browser.
+import { el } from './dom.js';
+
+export const ORGANIC = 'organic exploration';
+const SAVED = 'wai.quantum-studio.organic';
+
+// Whether the reader is exploring on their own, kept in this browser.
+export function organicMode() {
+  let on = false;
+  try { on = localStorage.getItem(SAVED) === '1'; } catch (e) {}
+  const heard = new Set();
+  return {
+    on: () => on,
+    set(v) {
+      on = !!v;
+      try { localStorage.setItem(SAVED, on ? '1' : '0'); } catch (e) {}
+      for (const f of heard) f(on);
+    },
+    onChange: (f) => heard.add(f),
+  };
+}
+
+const cap = (s) => s[0].toUpperCase() + s.slice(1);
+
+// The monitor's answer in words.
+export function convergeText(v, organicOn = false) {
+  const out = [v.converging ? `Converging: ${v.why}.` : `${cap(v.why)}.`];
+  const last = v.series?.at(-1);
+  if (last) out.push(`Your latest version is ${last.distance.toFixed(2)} from the model’s proposals in how it is built.`);
+  if (v.organic?.versions) out.push(`On your own: ${v.organic.versions} version${v.organic.versions === 1 ? '' : 's'}, ${v.organic.distance.toFixed(2)} from them${v.assisted?.distance != null ? `; the rest ${v.assisted.distance.toFixed(2)}` : ''}.`);
+  if (v.converging && !organicOn) out.push('Try a while on your own: the assistant then only asks.');
+  return out.join(' ');
+}
+
+// The panel, under Versions: `history()` the program's history, read at
+// `inputs()`; `organic` the mode.
+export function convergePanel({ engine, history, inputs, organic }) {
+  const line = el('p', { class: 'qs-note', id: 'qs-converge' });
+  const toggle = el('button', { class: 'qs-btn qs-small', id: 'qs-organic', type: 'button' });
+  const chip = el('span', { class: 'qs-badge find', id: 'qs-organic-chip', text: 'on your own', hidden: true });
+  const node = el('div', { class: 'qs-converge', id: 'qs-converge-box' },
+    el('div', { class: 'qs-actions' }, el('span', { class: 'qs-k', text: 'Your own way' }), chip, el('span', { class: 'qs-grow' }), toggle),
+    line);
+  let last = null;
+  function label() {
+    const on = organic.on();
+    toggle.textContent = on ? 'End: let the assistant propose again' : 'Explore on my own for a while';
+    toggle.title = on ? 'The assistant, Alternatives and the Workbench may ask the model again' : 'The assistant only asks; Alternatives and the Workbench do not ask the model; your versions are noted as made on your own';
+    toggle.setAttribute('aria-pressed', String(on));
+    chip.hidden = !on;
+    if (last) line.textContent = convergeText(last, on);
+  }
+  async function show() {
+    const h = history();
+    if (!h) { label(); return; }
+    last = await engine.converge('history', { history: h, inputs: inputs() }).catch(() => null);
+    node.classList.toggle('converging', !!last?.converging && !organic.on());
+    if (!last) line.textContent = '';
+    label();
+  }
+  toggle.addEventListener('click', () => { organic.set(!organic.on()); show(); });
+  organic.onChange(label);
+  label();
+  return { node, show };
+}

wai/quantum-studio/src/dom.js

@@ -17,7 +17,7 @@ export const el = (tag, attrs = {}, ...kids) => {
 export function sameness(eq) {
   if (!eq) return { text: 'not checked', cls: '' };
   if (eq.verdict === 'equivalent') {
-    const how = eq.how === 'tableau' ? 'equal tableaus' : eq.how === 'exact' ? 'on every basis state' : eq.how === 'random' ? 'on random inputs' : eq.how;
+    const how = eq.how === 'tableau' ? 'equal tableaus' : eq.how === 'exact' ? 'on every basis state' : eq.how === 'rewrites' ? 'by checked rewrites' : eq.how === 'random' ? 'on random inputs' : eq.how;
     return { text: `same circuit · ${how}`, cls: 'ok', why: eq.why };
   }
   if (eq.verdict === 'different') return { text: 'a different circuit', cls: 'bad', why: eq.why };

wai/quantum-studio/src/engine.js

@@ -85,6 +85,10 @@ export class TabEngine {
   discoverNovelty(spec, archive, entry) { return this.call('discover_novelty', { spec, archive, entry }); }
   // The person's taste model: `name` is features, choose, summary, rank or next; the profile goes in `args`.
   taste(name, args) { return this.call('taste', { name, args }); }
+  // The rewrites: `name` is options, apply, simplify, explain or prove.
+  rewrite(name, args) { return this.call('rewrite', { name, args }); }
+  // The convergence monitor: `name` is history or cohort.
+  converge(name, args) { return this.call('converge', { name, args }); }
   async signer() { return (await this.call('signer')).did; }
   cancel() {
     this.worker?.terminate();
@@ -165,6 +169,8 @@ export class DesktopEngine {
   novelty(args) { return this.call('novelty', { args: JSON.stringify(args) }); }
   discoverNovelty(spec, archive, entry) { return this.call('discover_novelty', { spec: JSON.stringify(spec), archive: JSON.stringify(archive), id: entry }); }
   taste(name, args) { return this.call('taste', { name, args: JSON.stringify(args) }); }
+  rewrite(name, args) { return this.call('rewrite', { name, args: JSON.stringify(args) }); }
+  converge(name, args) { return this.call('converge', { name, args: JSON.stringify(args) }); }
   async signer() { return (await this.call('signer', {})).did; }
   saveJob(name, job) { return this.call('save_job', { name, job: JSON.stringify(job, null, 2) }); }
   saveProgram(name, text) { return this.call('save_program', { name, text }); }

wai/quantum-studio/src/gallery.js

@@ -82,7 +82,8 @@ export function atlas(draft, cands, onPick) {
 // `taste` is the reader's taste profiles (taste.js): an alternative that is
 // the same circuit as the draft, taken whole or refused whole, is a choice
 // between the two, and Improve's candidates are ordered by the profile.
-export function galleryPane({ engine, draft, model, apply, check = null, found = null, taste = null }) {
+// `paused()` is true while the reader explores on their own: the model is not asked.
+export function galleryPane({ engine, draft, model, apply, check = null, found = null, taste = null, paused = () => false }) {
   const intent = el('input', { class: 'qs-input', id: 'qs-explore-aim', placeholder: 'Toward… fewer qubits, another entangler, more symmetry', autocomplete: 'off', 'aria-label': 'What Explore should aim for' });
   const improveBtn = el('button', { class: 'qs-btn qs-small', id: 'qs-improve', type: 'button', text: 'Improve', title: 'The same circuit, cheaper: each checked equivalent to the draft' });
   const exploreBtn = el('button', { class: 'qs-btn qs-small', id: 'qs-explore', type: 'button', text: 'Explore', title: 'Different circuits toward the aim, from the model, each measured by the engine' });
@@ -93,6 +94,16 @@ export function galleryPane({ engine, draft, model, apply, check = null, found =
     el('div', { class: 'qs-alt-aim' }, intent), note, body);
 
   let busy = false;
+  // How the draft becomes a candidate, each rewrite checked.
+  const chainView = (ch) => {
+    const n = ch.a_steps.length + ch.b_steps.length;
+    return el('details', { class: 'qs-chain' },
+      el('summary', { text: n ? `How: ${n} rewrite${n === 1 ? '' : 's'}, each checked` : 'How: the same gates, in another order' }),
+      ch.a_steps.length ? el('ol', {}, ...ch.a_steps.map((s) => el('li', { text: s.why }))) : null,
+      ch.b_steps.length ? el('p', { class: 'qs-note', text: 'and this one reduces to the same by:' }) : null,
+      ch.b_steps.length ? el('ol', {}, ...ch.b_steps.map((s) => el('li', { text: s.why }))) : null,
+      ch.reordered ? el('p', { class: 'qs-note', text: 'The two are then the same up to the order of gates that commute.' }) : null);
+  };
   // A candidate {label, qasm, source, idea?, equivalence?} measured against the draft.
   // Why a candidate is left out by the reader's rules: every change it makes
   // breaks one. A candidate with any change the rules allow is offered, and
@@ -113,7 +124,9 @@ export function galleryPane({ engine, draft, model, apply, check = null, found =
     // What is new in it, against the known constructions and the draft; an
     // engine without the call offers the candidate without it.
     const novelty = await engine.novelty?.({ qasm: c.qasm, against: [{ name: 'the draft', qasm: src }] }).catch(() => null);
-    return { ...c, measures: crit, equivalence, novelty, distance: lineDistance(src, c.qasm), base };
+    // The same circuit: how the draft becomes it, as a chain of checked rewrites.
+    const chain = equivalence?.verdict === 'equivalent' && !declared(src).length ? await engine.rewrite?.('explain', { a: src, b: c.qasm }).catch(() => null) : null;
+    return { ...c, measures: crit, equivalence, novelty, chain: chain?.found ? chain : null, distance: lineDistance(src, c.qasm), base };
   }
 
   // A proposal taken whole or refused whole is a choice between it and the
@@ -152,6 +165,7 @@ export function galleryPane({ engine, draft, model, apply, check = null, found =
           el('span', { class: 'qs-note', text: c.distance.changed ? `${c.distance.changed} lines changed` : 'the same lines' }),
           nv ? el('span', { class: `qs-badge qs-novelty ${nv.cls}`, title: nv.why, text: nv.text }) : null),
         c.changes?.length ? el('p', { class: 'qs-note', text: c.changes.join('; ') }) : null,
+        c.chain ? chainView(c.chain) : null,
         el('details', { class: 'qs-cand-src' }, el('summary', { text: 'Program' }), el('pre', { class: 'qs-ai-code', text: c.qasm })),
         el('div', { class: 'qs-actions' },
           el('button', { class: 'qs-btn qs-small qs-apply', type: 'button', text: 'Apply', onclick: async () => learn(await apply(c.qasm, `${mode === 'improve' ? 'An improvement' : 'An exploration'} from ${c.source === 'engine' ? 'the engine' : 'the model'}: ${c.idea || c.label}. ${s.text[0].toUpperCase() + s.text.slice(1)}.`, by), c, src) })));
@@ -178,8 +192,8 @@ export function galleryPane({ engine, draft, model, apply, check = null, found =
       if (!base.ok) { body.replaceChildren(el('p', { class: 'qs-empty', text: `The engine cannot read the draft: ${base.error}` })); return; }
       const v = await engine.variants(src);
       const raw = (v.candidates || []).map((c) => ({ label: c.label, qasm: c.qasm, changes: c.changes, source: 'engine', equivalence: c.equivalence }));
-      const m = model();
-      let said = m ? '' : 'Connect a model under “Model…” in the Assistant for its rewrites as well.';
+      const m = paused() ? null : model();
+      let said = paused() ? 'You are exploring on your own: these are the engine’s alone.' : m ? '' : 'Connect a model under “Model…” in the Assistant for its rewrites as well.';
       if (m) {
         try { for (const p of await m.improve(src, 3)) raw.push({ label: p.idea || 'a rewrite', idea: p.idea, qasm: p.qasm, source: 'model' }); }
         catch (e) { said = `The model did not answer (${e.message}); these are the engine’s alone.`; }
@@ -201,6 +215,7 @@ export function galleryPane({ engine, draft, model, apply, check = null, found =
 
   async function explore() {
     if (busy) return;
+    if (paused()) { body.replaceChildren(el('p', { class: 'qs-empty', id: 'qs-alt-paused', text: 'You are exploring on your own: Explore asks the model, so it waits until you end that under Versions. Improve works without it.' })); return; }
     const m = model();
     if (!m) { body.replaceChildren(el('p', { class: 'qs-empty', id: 'qs-alt-nomodel', text: 'Explore asks a model for ideas, and none is connected. Connect one under “Model…” in the Assistant; Improve works without one.' })); return; }
     busy = true; improveBtn.disabled = exploreBtn.disabled = true;

wai/quantum-studio/src/main.js

@@ -34,10 +34,12 @@ import { galleryPane } from './gallery.js';
 import { workbenchPane } from './workbench.js';
 import { foundPane } from './novelty.js';
 import { tasteStore } from './taste.js';
+import { organicMode, convergePanel, ORGANIC } from './converge.js';
 import { versionsPane, HANDS, whoName } from './versions.js';
 import { rulesPane, heldLines, LOCK, UNLOCK } from './rules.js';
 import { declared, inputsBar, withInputs } from './generators.js';
 import { shortcutsPanel } from './shortcuts-view.js';
+import { rewritePanel } from './rewrite-view.js';
 import * as Predict from './predict.js';
 
 const METHOD_NAMES = {
@@ -188,9 +190,14 @@ function mount(root) {
   });
   // The classical-shortcut lens, asked for: every exact route and its cost.
   const lens = shortcutsPanel({ engine: local, program: () => text() });
+  // The rewrite lens, asked for: each rewrite that keeps the meaning, taken one at a time.
+  const rewrites = rewritePanel({ engine: local, program: () => text(), onMark: (ops) => mark(diagram, 'qc-rewrite', ops), offer: (qasm, note) => offer(qasm, { kind: 'engine', name: 'Rewrite lens' }, note) });
   const circuitPane = el('section', { class: 'qs-pane qs-circ', 'aria-labelledby': 'qs-circuit-h' },
     el('div', { class: 'qs-head' }, el('h2', { id: 'qs-circuit-h', text: 'Circuit' }), el('span', { class: 'qs-grow' }), el('span', { class: 'qs-note', id: 'qs-plan' }), asText),
-    diagram, circuit, legend, critique.node, lens.node);
+    diagram, circuit, legend, critique.node, lens.node, rewrites.node);
+
+  // ---- a while on one's own: the assistant only asks ----
+  const organic = organicMode();
 
   // ---- the reader's taste, learned from their choices ----
   const taste = tasteStore(native);
@@ -207,6 +214,7 @@ function mount(root) {
     check: (base, qasm) => local.locks('check', { base, proposed: qasm, locks: rules.locks(), inputs: genInputs() }),
     found,
     taste,
+    paused: () => organic.on(),
   });
 
   // ---- the workbench ----
@@ -218,6 +226,7 @@ function mount(root) {
     save: (name, body) => saveFile(name, body, 'application/json'),
     found,
     taste,
+    paused: () => organic.on(),
   });
 
   // ---- the result ----
@@ -287,6 +296,7 @@ function mount(root) {
   // ---- the versions ----
   const editable = new Compartment();
   const handsCol = new Compartment();
+  let converge = null;
   const versions = versionsPane({
     engine: local,
     text: () => text(),
@@ -299,7 +309,12 @@ function mount(root) {
     onHands: (b) => showHands(b),
     save: (name, body, type) => saveFile(name, body, type),
     status: (s, cls) => setStatus(s, cls),
+    editNote: () => (organic.on() ? ORGANIC : null),
+    onRender: () => converge?.show(),
   });
+  // Whether the reader's versions converge on the model's, under Versions.
+  converge = convergePanel({ engine: native, history: () => versions.history(), inputs: genInputs, organic });
+  versions.node.append(converge.node);
 
   root.replaceChildren(header, el('div', { class: 'qs-grid' }, program, el('div', { class: 'qs-side' }, circuitPane, gallery.node, workbench.node, found.node, resultPane, versions.node, aiPane, historyPane)), footer);
 
@@ -394,6 +409,7 @@ function mount(root) {
       const src = text();
       try { localStorage.setItem(DRAFT, src); } catch (e) {}
       lens.stale(src);
+      rewrites.stale(src);
       try {
         const [d, l, c] = await Promise.all([local.draw(src, Math.max(40, Math.floor((circuit.clientWidth || diagram.clientWidth) / 7.8) || 80)), local.layout(src), local.critique(src)]);
         circuit.textContent = d.text ?? '';
@@ -712,7 +728,7 @@ function mount(root) {
   const assistantFor = () => {
     const m = model();
     if (!assistant || assistant.model.endpoint !== m.endpoint || assistant.model.name !== m.name) {
-      assistant = new Assistant({ engine: local, model: m, context: () => ({ qasm: text(), job: request(), last: current?.job }), stance: () => aiStance.value, rules: brief });
+      assistant = new Assistant({ engine: local, model: m, context: () => ({ qasm: text(), job: request(), last: current?.job }), stance: () => (organic.on() ? 'questions' : aiStance.value), rules: brief });
     }
     return assistant;
   };
@@ -746,7 +762,9 @@ function mount(root) {
               const counts = r?.counts ? Object.entries(r.counts).sort((a, b) => b[1] - a[1]).slice(0, 4).map(([k, n]) => `${compact(k)}: ${n}`).join(', ') : '';
               box.append(el('span', { class: 'qs-badge ok', text: `checked: ${p.lint.qubits} qubits, ${p.lint.gates} gates` }),
                 el('span', { class: 'qs-note', text: p.job ? ` ran here on ${METHOD_NAMES[p.job.method] || p.job.method}${counts ? '; ' + counts : ''}` : p.error ? ` did not run: ${p.error}` : '' }),
-                el('button', { class: 'qs-btn qs-small qs-ai-apply', type: 'button', text: 'Apply', onclick: () => offer(p.qasm, { kind: 'assistant', name: assistant?.model?.name || undefined }, 'The assistant’s program, checked and run before it was offered.') }));
+                organic.on()
+                  ? el('span', { class: 'qs-note qs-ai-held', text: ' You are exploring on your own: end that under Versions to take it.' })
+                  : el('button', { class: 'qs-btn qs-small qs-ai-apply', type: 'button', text: 'Apply', onclick: () => offer(p.qasm, { kind: 'assistant', name: assistant?.model?.name || undefined }, 'The assistant’s program, checked and run before it was offered.') }));
             }
             li.append(box);
           }

wai/quantum-studio/src/rewrite-view.js

@@ -0,0 +1,66 @@
+// The rewrite lens: every rewrite the program admits that keeps its meaning,
+// each checked by the engine on the qubits it touches (engine::rewrite). A gate
+// and its inverse cancel, rotations merge, Hadamards conjugate, a gate is
+// carried past what it commutes with, two gates that commute trade places. It
+// runs when asked, then again as the program changes. Pointing at a rewrite
+// marks its gates on the diagram; "Take" offers it as the engine's proposal,
+// reviewed like any other, so the reader makes the optimisation one checked
+// step at a time.
+import { el } from './dom.js';
+
+const ORDER = ['cancel', 'merge', 'through', 'conjugate', 'drop', 'move'];
+const WORDS = { cancel: 'cancel', merge: 'merge', through: 'carry', conjugate: 'conjugate', drop: 'drop', move: 'move' };
+
+// `engine` answers rewrite(name, args); `program()` is the editor's text;
+// `onMark(ops)` marks gates on the diagram; `offer(qasm, note)` proposes a program.
+export function rewritePanel({ engine, program, onMark, offer }) {
+  const ask = el('button', { class: 'qs-btn qs-small', id: 'qs-rewrites', type: 'button', text: 'Rewrites', title: 'Every rewrite that keeps the program’s meaning, each checked by the engine' });
+  const body = el('div', { class: 'qs-shortcuts-body', id: 'qs-rewrites-body' });
+  const node = el('div', { class: 'qs-shortcuts qs-rewrites', id: 'qs-rewrites-panel' },
+    el('div', { class: 'qs-shortcuts-head' }, el('span', { class: 'qs-k', text: 'Rewrites' }), el('span', { class: 'qs-grow' }), ask),
+    body);
+  let checkedFor = null;
+  let busy = false;
+
+  function row(o) {
+    const take = el('button', { class: 'qs-btn qs-small qs-rewrite-take', type: 'button', text: 'Take', onclick: () => offer(o.result, `A rewrite, checked by the engine: ${o.why}.`) });
+    const lines = [...new Set(o.lines)];
+    const li = el('li', { 'data-id': o.id, 'data-rule': o.rule, tabindex: '0' },
+      el('span', { class: 'qs-chip', text: WORDS[o.rule] ?? o.rule }),
+      el('span', { class: 'qs-rewrite-why', text: o.why }),
+      el('span', { class: 'qs-note', text: `line${lines.length === 1 ? '' : 's'} ${lines.join(', ')}` }),
+      take);
+    for (const ev of ['mouseenter', 'focusin']) li.addEventListener(ev, () => onMark(o.gates));
+    for (const ev of ['mouseleave', 'focusout']) li.addEventListener(ev, () => onMark([]));
+    return li;
+  }
+
+  async function look() {
+    if (busy) return;
+    busy = true; ask.disabled = true;
+    const src = program();
+    node.classList.remove('stale');
+    if (checkedFor == null) body.replaceChildren(el('p', { class: 'qs-note', text: 'The engine is checking each rewrite…' }));
+    try {
+      const v = await engine.rewrite('options', { qasm: src });
+      checkedFor = src;
+      onMark([]);
+      if (v.unread) { body.replaceChildren(el('p', { class: 'qs-note', text: `The engine cannot read the program: ${v.unread}` })); return; }
+      const opts = [...(v.options ?? [])].sort((a, b) => ORDER.indexOf(a.rule) - ORDER.indexOf(b.rule));
+      body.replaceChildren(...[
+        v.note ? el('p', { class: 'qs-note', text: `${v.note[0].toUpperCase()}${v.note.slice(1)}.` }) : null,
+        opts.length ? el('ol', { class: 'qs-rewrite-list', id: 'qs-rewrite-list' }, ...opts.map(row)) : null,
+        !opts.length && !v.note ? el('p', { class: 'qs-note', id: 'qs-rewrite-none', text: 'No rewrite applies: no gates cancel, merge or conjugate, and no two that commute sit side by side.' }) : null,
+        opts.length ? el('p', { class: 'qs-note', text: 'Each keeps the circuit’s meaning: the engine checks the gates a rewrite takes against the gates it puts, on the qubits they touch. Take one at a time; the review shows the change.' }) : null].filter(Boolean));
+      if (program() !== src) stale(program());
+    } catch (e) { body.replaceChildren(el('p', { class: 'qs-note', text: e.message })); }
+    finally { busy = false; ask.disabled = false; }
+  }
+
+  // Once asked, the lens follows the program.
+  function stale(src) {
+    if (checkedFor != null && src !== checkedFor) { node.classList.add('stale'); look(); }
+  }
+  ask.addEventListener('click', look);
+  return { node, look, stale };
+}

wai/quantum-studio/src/studio.css

@@ -359,3 +359,21 @@
 .qs-taste-list .qs-chip:hover, .qs-taste-list .qs-chip:focus-visible { color: var(--text-primary); outline: 1px solid var(--accent); }
 .qs-taste-typ { display: inline-flex; align-items: center; gap: 6px; font: 11px var(--font-mono, ui-monospace, monospace); font-variant-numeric: tabular-nums; color: var(--text-secondary); }
 .qs-taste-bar { width: 48px; height: 6px; border-radius: 3px; background: linear-gradient(to right, var(--accent) calc(var(--t) * 100%), var(--border) 0); }
+
+/* The rewrite lens, and how an alternative is reached. */
+.qs-rewrite-list { margin: 0; padding: 0 0 0 20px; display: flex; flex-direction: column; gap: 4px; font-size: 12px; }
+.qs-rewrite-list li { display: flex; flex-wrap: wrap; align-items: center; gap: 4px 8px; padding: 2px 4px; border-radius: 6px; }
+.qs-rewrite-list li:hover, .qs-rewrite-list li:focus-within { background: color-mix(in srgb, var(--accent) 10%, transparent); outline: none; }
+.qs-rewrite-why { flex: 1 1 220px; min-width: 0; color: var(--text-primary); }
+.qs-rewrites.stale .qs-rewrite-list { opacity: 0.55; }
+.qc-rewrite .qc-box, .qc-rewrite .qc-ring { stroke: var(--accent); stroke-width: 2.6; stroke-dasharray: none; fill: color-mix(in srgb, var(--accent) 18%, var(--bg-surface)); }
+.qc-name.qc-rewrite { fill: var(--accent-text); font-weight: 650; }
+.qs-chain summary { cursor: pointer; font: 11px var(--font-mono, ui-monospace, monospace); color: var(--text-muted); }
+.qs-chain ol { margin: 4px 0 0; padding-left: 20px; font-size: 12px; color: var(--text-secondary); }
+.qs-chain .qs-note { margin: 4px 0 0; }
+
+/* Your own way: convergence on the model's proposals, and a while on one's own. */
+.qs-converge { display: flex; flex-direction: column; gap: 6px; padding: 8px 12px 10px; border-top: 1px solid var(--border); }
+.qs-converge .qs-note { margin: 0; }
+.qs-converge.converging { background: color-mix(in srgb, var(--accent) 7%, transparent); }
+.qs-converge .qs-badge[hidden] { display: none; }

wai/quantum-studio/src/versions.js

@@ -52,7 +52,9 @@ function lanes(versions) {
 // hand each line and gate is in; `save(name, body)` keeps a file; `rules()`
 // gives the reader's rules for proposals (the engine's locks), and `taken()`
 // hears that a proposal was decided.
-export function versionsPane({ engine, text, setText, inputs, lock, reviewHost, onHands, save, status, rules = () => ({}), taken = () => {} }) {
+// `editNote()` notes the reader's own edits (a while on their own, say);
+// `onRender()` hears each time the history is shown again.
+export function versionsPane({ engine, text, setText, inputs, lock, reviewHost, onHands, save, status, rules = () => ({}), taken = () => {}, editNote = () => null, onRender = () => {} }) {
   let history = null;
   let current = null;
   let selected = null;
@@ -81,7 +83,7 @@ export function versionsPane({ engine, text, setText, inputs, lock, reviewHost,
 
   // ---- recording ----
   // The program as the editor holds it, recorded as `by`'s edit if it changed.
-  function record(by = { kind: 'person' }, note) {
+  function record(by = { kind: 'person' }, note = by.kind === 'person' ? editNote() ?? undefined : undefined) {
     clearTimeout(timer);
     return serial(async () => {
       if (!history || reviewing) return current;
@@ -276,6 +278,7 @@ export function versionsPane({ engine, text, setText, inputs, lock, reviewHost,
     if (showing) onHands(b);
     const v = history.versions.find((x) => x.id === (selected && source(selected) != null ? selected : current));
     if (v) showDetail(v, log);
+    onRender();
   }
 
   handsBox.addEventListener('change', async () => {

wai/quantum-studio/src/workbench.js

@@ -131,7 +131,8 @@ const byOf = (p) => (p === 'mutate' ? { kind: 'engine', name: 'the blind search'
 // where it went. `apply(source, note, by)` offers a generator to the editor as
 // `by`'s proposal. `found` is the Found pane; `taste` the reader's taste
 // profiles (taste.js), learned from choices between kept generators.
-export function workbenchPane({ engine, draft, model, apply, save, found = null, taste = null }) {
+// `paused()` is true while the reader explores on their own: the model is not asked.
+export function workbenchPane({ engine, draft, model, apply, save, found = null, taste = null, paused = () => false }) {
   const startBtn = el('button', { class: 'qs-btn qs-small', id: 'qs-wb-start', type: 'button', text: 'Start', title: 'A new archive, seeded with the program in the editor as the reference' });
   const task = el('select', { class: 'qs-input qs-small', id: 'qs-wb-task', 'aria-label': 'What each member must do' },
     el('option', { value: 'prepares', text: 'prepare the same state from |0…0⟩' }), el('option', { value: 'equivalent', text: 'be the same circuit (unitary)' }));
@@ -316,6 +317,7 @@ export function workbenchPane({ engine, draft, model, apply, save, found = null,
   async function ask() {
     if (busy || !spec) return;
     const m = model();
+    if (paused()) { say('You are exploring on your own: the model waits until you end that under Versions.', 'bad'); return; }
     if (!m) { say('Ask the model needs one: connect it under “Model…” in the Assistant.', 'bad'); return; }
     setBusy(true);
     stats.textContent = 'The model is proposing; the engine will judge each…';

wai/quantum-studio/src/worker.js

@@ -51,6 +51,8 @@ self.onmessage = async (ev) => {
       case 'history': text = e().history(ev.data.name, JSON.stringify(ev.data.args ?? {})); break;
       case 'locks': text = mod.engine_locks(ev.data.name, JSON.stringify(ev.data.args ?? {})); break;
       case 'novelty': text = mod.engine_novelty(JSON.stringify(ev.data.args ?? {})); break;
+      case 'converge': text = mod.engine_converge(ev.data.name, JSON.stringify(ev.data.args ?? {})); break;
+      case 'rewrite': text = mod.engine_rewrite(ev.data.name, JSON.stringify(ev.data.args ?? {})); break;
       case 'taste': text = mod.engine_taste(ev.data.name, JSON.stringify(ev.data.args ?? {})); break;
       case 'discover_novelty': text = mod.engine_discover_novelty(JSON.stringify(ev.data.spec), JSON.stringify(ev.data.archive), ev.data.entry); break;
       default: throw new Error(`no operation ${op}`);

wai/quantum-studio/test/studio.test.mjs

@@ -25,7 +25,12 @@
 //     applied; Explore without a model says it needs one; a rewrite that reaches the GHZ
 //     state by a different route is labelled so and flagged in Found, saved there with a
 //     note, and kept with the page; an alternative that is the same circuit, taken whole, is
-//     a choice the reader's taste learns from;
+//     a choice the reader's taste learns from, and the card says how the draft becomes it, as
+//     a chain of checked rewrites;
+//   - the rewrite lens: each rewrite the program admits, its gates marked on the diagram,
+//     one taken as the engine's proposal, and the list following the program;
+//   - your own way: a while on one's own, kept in this browser, Explore waiting for it, a
+//     version made then noted so, the convergence line, and its end;
 //   - the classical-shortcut lens: a Clifford ring with a closing rotation layer priced by
 //     the cut-rank sum, a Clifford circuit easy at any width, a contraction searched only
 //     when thorough, and a check marked stale once the program changes;
@@ -221,6 +226,7 @@ const chip = (k) => page.$eval(`#qs-measures [data-k=${k}]`, (c) => c.textConten
   check(/the engine/.test(card) && /same circuit · on every basis state/.test(card) && /2 gates/.test(card), `Improve offers the engine's rewrite, checked on every basis state (${card.slice(0, 160)})`);
   check(await page.isVisible('#qs-atlas') && (await page.$$('#qs-atlas .qs-dot')).length === (await page.$$('.qs-cand')).length && (await page.$$('#qs-atlas .qs-ring')).length === 1, 'the atlas plots the draft and each alternative');
   check(/Connect a model/.test(await page.textContent('#qs-alt-body')), 'without a model, Improve says the engine’s are the only ones');
+  check(/How: 1 rewrite, each checked/.test(card) && card.includes('rz(0.25) q[0] and rz(0.5) q[0] merge into rz(0.75) q[0]'), `the card says how the draft becomes it, a chain of checked rewrites (${card.slice(0, 220)})`);
   check((await doc()) === MERGE, 'nothing changes the program until an alternative is applied');
   await page.click('.qs-cand .qs-apply');
   await page.waitForSelector('#qs-review:not([hidden]) #qs-review-apply', { timeout: LONG });
@@ -254,6 +260,48 @@ const chip = (k) => page.$eval(`#qs-measures [data-k=${k}]`, (c) => c.textConten
   check((await page.textContent('#qs-found-count')) === '1 flagged · 1 saved' && (await page.textContent('#qs-found-list .qs-found-save')) === 'Saved', 'Save keeps it, and the count says so');
 }
 
+// The rewrite lens: each rewrite that keeps the meaning, checked, taken one at a time.
+{
+  const LENS = 'OPENQASM 3.0;\nqubit[2] q;\nh q[1];\ncx q[0], q[1];\nh q[1];\nt q[0];\nt q[0];\n';
+  await setProgram(LENS);
+  // The diagram is drawn a moment after the edit; marks go on the one drawn.
+  // (The measurements it draws at the end carry no gate.)
+  await page.waitForFunction(() => /5 gates/.test(document.querySelector('#qs-lint')?.textContent ?? '') && [...document.querySelectorAll('#qs-diagram .qc-item')].filter((g) => /^\d+$/.test(g.dataset.op ?? '')).length === 5, null, { timeout: LONG });
+  await page.click('#qs-rewrites');
+  await page.waitForSelector('#qs-rewrite-list li', { timeout: LONG });
+  const rows = await page.$$eval('#qs-rewrite-list li', (ls) => ls.map((l) => [l.dataset.rule, l.textContent]));
+  check(rows.some(([r, t]) => r === 'conjugate' && t.includes('cx q[0], q[1] between two h q[1] is cz q[0], q[1]')) && rows.some(([r, t]) => r === 'merge' && t.includes('t q[0] and t q[0] merge into s q[0]')),
+    `the lens lists each rewrite the program admits, in words (${rows.map(([r]) => r).join(', ')})`);
+  await page.hover('#qs-rewrite-list li[data-rule=conjugate]');
+  const marked = await page.waitForFunction(() => document.querySelectorAll('#qs-diagram .qc-item.qc-rewrite').length === 3, null, { timeout: 5000 }).then(() => true, () => false);
+  check(marked, `pointing at one marks its gates on the diagram (${(await page.$$('#qs-diagram .qc-item.qc-rewrite')).length} marked)`);
+  await page.click('#qs-rewrite-list li[data-rule=conjugate] .qs-rewrite-take');
+  await page.waitForSelector('#qs-review:not([hidden]) #qs-review-apply', { timeout: LONG });
+  check(/A proposal from the engine \(Rewrite lens\)/.test(await page.textContent('#qs-review')) && (await doc()) === LENS, 'Take offers it as the engine’s proposal, to review');
+  await page.click('#qs-review-apply');
+  await page.waitForFunction(() => /cz q\[0\], q\[1\];/.test(window.quantumStudio.view.state.doc.toString()) && !/h q\[1\]/.test(window.quantumStudio.view.state.doc.toString()), null, { timeout: LONG });
+  await page.waitForFunction(() => !document.querySelector('#qs-rewrite-list li[data-rule=conjugate]') && document.querySelector('#qs-rewrite-list li[data-rule=merge]'), null, { timeout: LONG });
+  check(true, 'taken, the lens follows the program: the conjugation is gone and the merge is still offered');
+}
+
+// Your own way: whether the versions converge on the model's, and a while on one's own.
+{
+  check(/^Explore on my own/.test(await page.textContent('#qs-organic')) && await page.isHidden('#qs-organic-chip'), 'Versions offers a while on one’s own');
+  await page.click('#qs-organic');
+  check(await page.isVisible('#qs-organic-chip') && (await page.getAttribute('#qs-organic', 'aria-pressed')) === 'true' && (await page.evaluate(() => localStorage.getItem('wai.quantum-studio.organic'))) === '1', 'on one’s own: marked, and kept in this browser');
+  await page.click('#qs-explore');
+  await page.waitForSelector('#qs-alt-paused', { timeout: LONG });
+  check(true, 'Explore, which asks the model, waits');
+  await setProgram('OPENQASM 3.0;\nqubit[2] q;\nh q[0];\ncx q[0], q[1];\nz q[1];\n');
+  await page.evaluate(() => window.quantumStudio.versions.record());
+  const note = await page.evaluate(() => window.quantumStudio.versions.history().versions.at(-1).note);
+  check(note === 'organic exploration', `a version made on one’s own is noted so (${note})`);
+  await page.waitForFunction(() => /\.$/.test(document.querySelector('#qs-converge')?.textContent ?? ''), null, { timeout: LONG });
+  check(true, `the line says whether the versions converge on the model’s (${await page.textContent('#qs-converge')})`);
+  await page.click('#qs-organic');
+  check(await page.isHidden('#qs-organic-chip') && /^Explore on my own/.test(await page.textContent('#qs-organic')), 'ended, the model may be asked again');
+}
+
 // Versions: each change and who made it; a proposal taken change by change;
 // whose hand each line and gate is in; the run's receipt binding the count; a
 // line of work from an older version, brought back in; and all of it kept.

wai/tools/quantum-meter/Cargo.lock

@@ -1017,7 +1017,7 @@ checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
 
 [[package]]
 name = "wai-quantum"
-version = "0.6.15"
+version = "0.6.16"
 dependencies = [
  "blake3",
  "ed25519-dalek",

wai/tools/quantum-wgsl-check/Cargo.lock

@@ -599,7 +599,7 @@ checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
 
 [[package]]
 name = "wai-quantum"
-version = "0.6.15"
+version = "0.6.16"
 dependencies = [
  "blake3",
  "ed25519-dalek",

wai/wai-pack/Cargo.lock

@@ -1257,7 +1257,7 @@ dependencies = [
 
 [[package]]
 name = "wai-quantum"
-version = "0.6.15"
+version = "0.6.16"
 dependencies = [
  "blake3",
  "ed25519-dalek",

wai/wai-quantum-cli/Cargo.lock

@@ -1120,7 +1120,7 @@ checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
 
 [[package]]
 name = "wai-quantum"
-version = "0.6.15"
+version = "0.6.16"
 dependencies = [
  "blake3",
  "ed25519-dalek",
@@ -1133,7 +1133,7 @@ dependencies = [
 
 [[package]]
 name = "wai-quantum-cli"
-version = "0.1.3"
+version = "0.1.4"
 dependencies = [
  "clap",
  "clap_complete",

wai/wai-quantum-cli/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "wai-quantum-cli"
-version = "0.1.3"
+version = "0.1.4"
 edition = "2024"
 rust-version = "1.97"
 license = "Apache-2.0"
@@ -34,4 +34,4 @@ getrandom = "0.4"
 # result's receipt still verifies after any JSON writer has carried it.
 serde_json = { version = "1", features = ["float_roundtrip"] }
 ureq = { version = "3", optional = true, features = ["json"] }
-wai-quantum = { version = "0.6.15", path = "../wai-quantum", default-features = false, features = ["full"] }
+wai-quantum = { version = "0.6.16", path = "../wai-quantum", default-features = false, features = ["full"] }

wai/wai-quantum-cli/README.md

@@ -121,7 +121,7 @@ wai-quantum shortcuts prog.qasm              # each exact classical route to sim
 
 The critique's figures are computed, not estimated: gates by kind, two-qubit gates, depth and two-qubit depth, the T count, and whether the program is a Clifford circuit. Its fidelity is a model at reference error rates, and says so. Its smells are gates that cancel, rotations that merge or do nothing, idle qubits, and qubits acted on but never measured.
 
-`equivalent` compares two programs up to a global phase. Clifford circuits are compared by their tableaus at any size, and others on every basis state up to 8 qubits. Between 8 and 22 qubits it compares them on random product states, which is evidence, not proof. Beyond that it answers unchecked, with the reason. `improve` rewrites only statements alone on their lines, and prints a rewrite only when the check does not find it different.
+`equivalent` compares two programs up to a global phase. Clifford circuits are compared by their tableaus at any size, and others on every basis state up to 8 qubits. Wider than that, it tries to rewrite one program followed by the other's inverse to nothing, each rewrite checked on the qubits it touches (`rewrites`, below): when that works it is a proof at any width, with any gates. Otherwise, between 8 and 22 qubits, it compares them on random product states, which is evidence, not proof. Beyond that it answers unchecked, with the reason. `improve` rewrites only statements alone on their lines, and prints a rewrite only when the check does not find it different.
 
 `shortcuts` lists every exact classical route the engine knows for simulating the program, each with its memory and operations, and names the cheapest. The routes:
 
@@ -153,6 +153,8 @@ A cheap route proves a design classically easy. None being cheap proves nothing
 - `verify_quantum_result`
 - `discover_evaluate`, `discover_submit` and `discover_archive` (the workbench, below)
 - `novelty_qasm` and `discover_novelty` (what is new, below)
+- `rewrite_qasm` (rewrites, below)
+- `converge_cohort` and `converge_history` (convergence, below)
 - `taste_rank` and `taste_next` (your taste, below)
 - `history_commit`, `history_changes`, `history_blame` and `history_log` (a program's history, below)
 - `list_methods`
@@ -256,6 +258,37 @@ wai-quantum discover novelty ghz-all.json e12          # one entry of an archive
 
 A high distance is a reason to look, not a claim that nobody has built it: the engine knows the constructions above and the programs it is given, not the literature.
 
+## Rewrites
+
+`wai-quantum rewrite` makes an optimisation one checked step at a time:
+
+```sh
+wai-quantum rewrite options prog.qasm               # every rewrite it admits, each with its id, in words
+wai-quantum rewrite apply prog.qasm merge:6,7       # the program with that one made
+wai-quantum rewrite simplify prog.qasm              # every rewrite to a fixed point: the steps, then the result
+wai-quantum rewrite explain prog.qasm theirs.qasm   # how one becomes the other, as a chain
+```
+
+- **The rules propose; the engine decides.** A gate and its inverse cancel; two rotations about one axis merge, and `t`, `s` and `z` add up; a gate between two Hadamards becomes its conjugate (`h x h` is `z`, and `cx` between two `h` on its target is `cz`); a gate that does nothing is dropped; a gate is carried past gates it commutes with to cancel or merge with its partner; and two gates that commute trade places.
+- **Each rewrite is checked** on just the qubits it touches, by their tableaus or on every basis state. Replacing a few gates by others with the same unitary keeps the whole circuit's, so a chain of rewrites proves two programs equal at any width and with any gates.
+- **Each option is an edit to the program's own lines.** A merge writes `rz(0.25 + 0.5)`, comments and the other lines stay as they are, and the result is read back and compared gate for gate before it is offered. A generator is rewritten as the circuit it writes out.
+- **`explain`** simplifies both programs and compares what is left. The steps are a readable account of why an optimisation is the same circuit.
+
+## Convergence
+
+`wai-quantum converge` says whether your designs are converging on a model's, and how diverse a set of designs is:
+
+```sh
+wai-quantum converge history prog.qasm               # along its history: how far your versions are from a model's proposals
+wai-quantum converge cohort designs/*.qasm --input n=6   # the Vendi score, the centroid, and the score over time
+```
+
+- **Along a history:** for each version you made after a model proposed, its structural distance from the proposals in its line of work, and the share of its gates in a model's hand. It is converging when most of the program is the model's, or when your last versions come closer to its proposals each time.
+- **On your own:** versions noted `organic exploration` (the Studio's "Explore on my own") are the assistant-off probes. Their distance from the proposals is set beside the rest.
+- **A cohort:** programs for one task, a group's or yours over months. The Vendi score is the effective number of distinct designs, from 1 when they are all built alike to the number of programs. Each program's distance to the centroid is given, with the medoid and the one built least like the rest. With times (a history's last version, or the file's), the score is taken in windows, and a narrowing is named.
+
+Everything is read from the files given, and nothing is sent anywhere.
+
 ## Your taste
 
 `wai-quantum taste` learns your taste in circuits from your own choices:

wai/wai-quantum-cli/src/converge.rs

@@ -0,0 +1,94 @@
+//! `wai-quantum converge`: whether a person's designs converge on a model's
+//! proposals, and how diverse a cohort's designs are
+//! ([`wai_quantum::engine::converge`]). Everything is read from files here;
+//! nothing is sent anywhere.
+
+use clap::Subcommand;
+use serde_json::Value;
+use std::path::{Path, PathBuf};
+use wai_quantum::engine::converge::{self, Design};
+
+#[derive(Subcommand)]
+pub enum Cmd {
+    /// Along a program's history: how far your versions are built from a model's proposals, and its share of the gates
+    History {
+        /// The program
+        program: PathBuf,
+        /// The history (default: beside the program, as NAME.history.json)
+        #[arg(long)]
+        history: Option<PathBuf>,
+        #[arg(long)]
+        json: bool,
+    },
+    /// How diverse a set of programs is: the Vendi score, each one's distance to the centroid, and the score over time
+    Cohort {
+        /// The programs: each one's time is its history's last version, or the file's
+        files: Vec<PathBuf>,
+        /// Windows over time to take the score in
+        #[arg(long, default_value_t = 3)]
+        windows: usize,
+        #[arg(long)]
+        json: bool,
+    },
+}
+
+/// When a program was made: its history's last version, or the file's time,
+/// in milliseconds since 1970.
+fn made(p: &Path) -> Option<u64> {
+    if let Ok(h) = crate::history::load(&crate::history::path(p, None)) {
+        return h.versions.iter().map(|v| v.at).max();
+    }
+    let t = std::fs::metadata(p).ok()?.modified().ok()?;
+    t.duration_since(std::time::UNIX_EPOCH).ok().map(|d| d.as_millis() as u64)
+}
+
+/// A history's convergence in words.
+pub fn history_text(v: &Value) -> String {
+    let mut out = String::new();
+    for s in v["series"].as_array().into_iter().flatten() {
+        out += &format!("{:<6} {} from the model's proposals; {:.0}% of its gates a model's{}\n", s["version"].as_str().unwrap_or(""), s["distance"], s["share"].as_f64().unwrap_or(0.0) * 100.0, if s["organic"] == true { "  (on your own)" } else { "" });
+    }
+    out += &format!("{}: {}\n", if v["converging"] == true { "converging" } else { "not converging" }, v["why"].as_str().unwrap_or(""));
+    if let (Some(o), Some(a)) = (v["organic"]["distance"].as_f64(), v["assisted"]["distance"].as_f64()) {
+        out += &format!("on your own, {} version(s) {o:.2} from the proposals; the rest {a:.2}\n", v["organic"]["versions"]);
+    }
+    if v["converging"] == true {
+        out += "try a while on your own: in the Studio, \"Explore on my own\"; versions made that way are noted \"organic exploration\"\n";
+    }
+    out
+}
+
+/// A cohort's diversity in words.
+pub fn cohort_text(v: &Value) -> String {
+    let mut out = format!("{} programs, Vendi score {} ({:.0}% of the most it could be): about {} distinct designs\n", v["programs"], v["vendi"], v["share"].as_f64().unwrap_or(0.0) * 100.0, v["vendi"].as_f64().unwrap_or(0.0).round());
+    out += &format!("medoid {}; built least like the rest: {}\n", v["medoid"].as_str().unwrap_or(""), v["outlier"].as_str().unwrap_or(""));
+    for c in v["centroid"].as_array().into_iter().flatten() {
+        out += &format!("  {:<40} {} from the centroid\n", c["name"].as_str().unwrap_or(""), c["distance"]);
+    }
+    for w in v["windows"].as_array().into_iter().flatten() {
+        out += &format!("window of {}: Vendi {} ({:.0}%)\n", w["programs"], w["vendi"], w["share"].as_f64().unwrap_or(0.0) * 100.0);
+    }
+    if v["narrowing"] == true {
+        out += "narrowing: the later designs are built more alike than the earlier\n";
+    }
+    out
+}
+
+pub fn main(cmd: Cmd) {
+    let inputs = super::INPUTS.get().cloned().unwrap_or_default();
+    let r = (|| match cmd {
+        Cmd::History { program, history, json } => {
+            let h = crate::history::load(&crate::history::path(&program, history.as_deref()))?;
+            let v = converge::history(&h, &inputs)?;
+            if json { println!("{v}") } else { print!("{}", history_text(&v)) }
+            Ok(())
+        }
+        Cmd::Cohort { files, windows, json } => {
+            let designs = files.iter().map(|p| Ok(Design { name: p.display().to_string(), source: super::read_text(Some(p))?, at: made(p) })).collect::<Result<Vec<_>, String>>()?;
+            let v = converge::cohort(&designs, &inputs, windows)?;
+            if json { println!("{v}") } else { print!("{}", cohort_text(&v)) }
+            Ok(())
+        }
+    })();
+    r.unwrap_or_else(|e: String| super::die(&e));
+}

wai/wai-quantum-cli/src/main.rs

@@ -39,11 +39,13 @@
 //! circuits. Every command reads one circuit of the family, at the values
 //! given with `--input`, and `instance` prints that circuit.
 
+mod converge;
 mod discover;
 mod history;
 mod lab;
 mod locks;
 mod mcp;
+mod rewrite;
 mod taste;
 
 use clap::{Args, CommandFactory, Parser, Subcommand};
@@ -217,6 +219,16 @@ enum Command {
         #[command(subcommand)]
         cmd: locks::Cmd,
     },
+    /// Whether your designs converge on a model's proposals, and how diverse a set of programs is (`wai-quantum converge --help`)
+    Converge {
+        #[command(subcommand)]
+        cmd: converge::Cmd,
+    },
+    /// Rewrites that keep a program's meaning, each checked: the ones it admits, one made, all to a fixed point, or how one program becomes another (`wai-quantum rewrite --help`)
+    Rewrite {
+        #[command(subcommand)]
+        cmd: rewrite::Cmd,
+    },
     /// Your taste in circuits, learned from your own choices between programs the engine proves equal (`wai-quantum taste --help`)
     Taste {
         #[command(subcommand)]
@@ -726,6 +738,8 @@ fn main() {
         Command::History { cmd } => history::main(cmd),
         Command::Locks { cmd } => locks::main(cmd),
         Command::Taste { cmd } => taste::main(cmd),
+        Command::Rewrite { cmd } => rewrite::main(cmd),
+        Command::Converge { cmd } => converge::main(cmd),
         Command::Novelty { file, against, reference, weigh, json } => {
             let inputs = INPUTS.get().cloned().unwrap_or_default();
             let text = read_text(file.as_deref()).unwrap_or_else(|e| die(&e));

wai/wai-quantum-cli/src/mcp.rs

@@ -75,7 +75,7 @@ fn tools() -> Value {
         {
             "name": "check_equivalent",
             "title": "Check two programs are the same circuit",
-            "description": "Whether two programs are the same circuit up to a global phase, and how the engine knows: equal tableaus for Clifford circuits at any size, every basis state to 8 qubits, random product states to 22 qubits (evidence, not proof), or unchecked with the reason.",
+            "description": "Whether two programs are the same circuit up to a global phase, and how the engine knows: equal tableaus for Clifford circuits at any size, every basis state to 8 qubits, checked rewrites of one followed by the other's inverse to nothing (a proof at any width), random product states to 22 qubits (evidence, not proof), or unchecked with the reason.",
             "inputSchema": { "type": "object", "required": ["a", "b"], "properties": { "a": { "type": "string", "description": "The first program." }, "b": { "type": "string", "description": "The second program." }, "inputs": inputs_schema() } },
         },
         {
@@ -132,6 +132,24 @@ fn tools() -> Value {
             "description": "For one entry of a workbench archive, read at the specification's largest size: its nearest known construction or elite and the distance, each known construction it is found to be (and whether by a different route), and the measures it beats the reference on that the specification's cost does not weigh.",
             "inputSchema": { "type": "object", "required": ["spec", "id"], "properties": { "spec": { "type": "string", "description": "The specification's path." }, "archive": { "type": "string", "description": "The archive's path, if not beside the specification." }, "id": { "type": "string", "description": "The entry's id." } } },
         },
+        {
+            "name": "rewrite_qasm",
+            "title": "Rewrite a program, each step checked",
+            "description": "Rewrites that keep a program's meaning, each checked by the engine on the qubits it touches (a gate and its inverse cancel, rotations merge, Hadamards conjugate, a gate is carried past what it commutes with, two gates that commute trade places). op options: every rewrite the program admits, each an edit to its own lines with its id; apply: the program with the rewrite `id` made; simplify: every rewrite to a fixed point, each step in words; explain: how the program becomes `other`, as a chain of rewrites. Use explain to show the person why an optimisation is the same circuit.",
+            "inputSchema": { "type": "object", "required": ["qasm", "op"], "properties": { "qasm": { "type": "string" }, "op": { "type": "string", "enum": ["options", "apply", "simplify", "explain"] }, "id": { "type": "string", "description": "For apply: a rewrite's id from options." }, "other": { "type": "string", "description": "For explain: the program it should become." }, "inputs": inputs_schema() } },
+        },
+        {
+            "name": "converge_cohort",
+            "title": "How diverse a set of programs is",
+            "description": "For programs written for one task (a group's, or one person's over time): the Vendi score (the effective number of distinct designs, from 1 when all are built alike to the number of programs), each one's structural distance to the centroid, the medoid and the one built least like the rest, and with times (milliseconds) the score in windows over time and whether it narrows. Use it before proposing, to see whether your proposals would narrow what the person has made.",
+            "inputSchema": { "type": "object", "required": ["programs"], "properties": { "programs": { "type": "array", "items": { "type": "object", "required": ["name", "qasm"], "properties": { "name": { "type": "string" }, "qasm": { "type": "string" }, "at": { "type": "integer" } } } }, "inputs": inputs_schema(), "windows": { "type": "integer" } } },
+        },
+        {
+            "name": "converge_history",
+            "title": "Whether the person's designs converge on a model's",
+            "description": "Along a program's history (the path of NAME.history.json): for each version the person made after a model proposed, how far it is built from the proposals and the share of its gates in a model's hand; whether that is converging, and why; and the versions made exploring on their own set beside the rest. When it converges, propose less and ask more.",
+            "inputSchema": { "type": "object", "required": ["history"], "properties": { "history": { "type": "string", "description": "The history file's path." }, "inputs": inputs_schema() } },
+        },
         {
             "name": "taste_rank",
             "title": "Rank programs by the person's taste",
@@ -228,6 +246,23 @@ fn call(name: &str, args: &Value, memory_gb: u64, key: &SigningKey, client: &Cli
         }
         "list_methods" => Ok(json!({ "methods": catalog::describe(memory_gb << 30) })),
         "novelty_qasm" => wai_quantum::engine::novelty::call(raw),
+        "converge_cohort" => wai_quantum::engine::converge::call("cohort", raw),
+        "converge_history" => {
+            let path = raw.get("history").and_then(Value::as_str).ok_or("give \"history\": the history file's path")?;
+            let h = crate::history::load(std::path::Path::new(path))?;
+            let mut a = raw.clone();
+            a["history"] = serde_json::to_value(&h).map_err(|e| e.to_string())?;
+            wai_quantum::engine::converge::call("history", &a)
+        }
+        "rewrite_qasm" => {
+            let op = raw.get("op").and_then(Value::as_str).ok_or("give \"op\": options, apply, simplify or explain")?;
+            let mut a = raw.clone();
+            if op == "explain" {
+                a["a"] = raw.get("qasm").cloned().unwrap_or(Value::Null);
+                a["b"] = raw.get("other").cloned().ok_or("explain: give \"other\", the program it should become")?;
+            }
+            wai_quantum::engine::rewrite::call(op, &a)
+        }
         _ => Err(format!("no tool {name}")),
     }
 }
@@ -435,7 +470,7 @@ mod tests {
         assert!(handle(&json!({ "jsonrpc": "2.0", "method": "notifications/initialized" }), 1, &key(), &mut Client::default()).is_none());
         let list = handle(&json!({ "jsonrpc": "2.0", "id": 2, "method": "tools/list" }), 1, &key(), &mut Client::default()).unwrap();
         let names: Vec<&str> = list["result"]["tools"].as_array().unwrap().iter().map(|t| t["name"].as_str().unwrap()).collect();
-        assert_eq!(names, ["run_quantum_circuit", "plan_quantum_circuit", "lint_qasm", "critique_qasm", "check_equivalent", "improve_qasm", "classical_shortcuts", "draw_circuit", "verify_quantum_result", "discover_evaluate", "discover_submit", "discover_archive", "novelty_qasm", "discover_novelty", "taste_rank", "taste_next", "history_commit", "history_changes", "history_blame", "history_log", "list_methods"]);
+        assert_eq!(names, ["run_quantum_circuit", "plan_quantum_circuit", "lint_qasm", "critique_qasm", "check_equivalent", "improve_qasm", "classical_shortcuts", "draw_circuit", "verify_quantum_result", "discover_evaluate", "discover_submit", "discover_archive", "novelty_qasm", "discover_novelty", "rewrite_qasm", "converge_cohort", "converge_history", "taste_rank", "taste_next", "history_commit", "history_changes", "history_blame", "history_log", "list_methods"]);
         let run = handle(
             &json!({ "jsonrpc": "2.0", "id": 3, "method": "tools/call", "params": { "name": "run_quantum_circuit", "arguments": { "qasm": "OPENQASM 3.0; qubit[2] q; h q[0]; cx q[0], q[1];", "observables": ["Z0 Z1"] } } }),
             1,
@@ -495,6 +530,28 @@ mod tests {
         assert!(call("lint_qasm", &json!({ "qasm": star }), 1, &key(), &Client::default()).unwrap_err().contains("give n a value"));
     }
 
+    #[test]
+    fn an_agent_reads_a_cohort_s_diversity() {
+        let a = "OPENQASM 3.0;\nqubit[1] q;\nh q[0];\n";
+        let v = call("converge_cohort", &json!({ "programs": [{ "name": "a", "qasm": a }, { "name": "b", "qasm": a }, { "name": "c", "qasm": "OPENQASM 3.0;\nqubit[1] q;\nt q[0];\n" }] }), 1, &key(), &Client::default()).unwrap();
+        let score = v["vendi"].as_f64().unwrap();
+        assert!(score > 1.0 && score < 3.0 && v["outlier"] == "c", "{v}");
+        assert!(call("converge_history", &json!({ "history": "/nonexistent/x.history.json" }), 1, &key(), &Client::default()).is_err());
+    }
+
+    #[test]
+    fn an_agent_rewrites_step_by_step_and_explains_an_optimisation() {
+        let src = "OPENQASM 3.0;\nqubit[2] q;\nh q[1];\ncx q[0], q[1];\nh q[1];\nt q[0];\nt q[0];\n";
+        let o = call("rewrite_qasm", &json!({ "qasm": src, "op": "options" }), 1, &key(), &Client::default()).unwrap();
+        let ids: Vec<&str> = o["options"].as_array().unwrap().iter().map(|x| x["id"].as_str().unwrap()).collect();
+        assert!(ids.contains(&"conjugate:3,4,5") && ids.contains(&"merge:6,7"), "{o}");
+        let one = call("rewrite_qasm", &json!({ "qasm": src, "op": "apply", "id": "merge:6,7" }), 1, &key(), &Client::default()).unwrap();
+        assert!(one["result"].as_str().unwrap().contains("s q[0];"), "{one}");
+        let e = call("rewrite_qasm", &json!({ "qasm": src, "op": "explain", "other": "OPENQASM 3.0;\nqubit[2] q;\ncz q[0], q[1];\ns q[0];\n" }), 1, &key(), &Client::default()).unwrap();
+        assert_eq!(e["found"], true, "{e}");
+        assert!(call("rewrite_qasm", &json!({ "qasm": src, "op": "explain" }), 1, &key(), &Client::default()).unwrap_err().contains("other"));
+    }
+
     #[test]
     fn an_agent_asks_what_is_new_and_what_is_found_again() {
         let ladder = "OPENQASM 3.0;\ninput uint n;\nqubit[n] q;\nh q[n - 1];\nfor uint i in [1:n-1] {\n  cx q[n - i], q[n - i - 1];\n}\n";

wai/wai-quantum-cli/src/rewrite.rs

@@ -0,0 +1,116 @@
+//! `wai-quantum rewrite`: rewrites that keep a program's meaning, each
+//! checked by the engine on the qubits it touches
+//! ([`wai_quantum::engine::rewrite`]).
+
+use clap::Subcommand;
+use serde_json::{Value, json};
+use std::path::PathBuf;
+use wai_quantum::engine::rewrite;
+
+#[derive(Subcommand)]
+pub enum Cmd {
+    /// Every rewrite the program admits, each an edit to its own lines
+    Options {
+        file: PathBuf,
+        #[arg(long)]
+        json: bool,
+    },
+    /// The program with one rewrite made (its id from `options`): to standard output, or to --out
+    Apply {
+        file: PathBuf,
+        id: String,
+        #[arg(long)]
+        out: Option<PathBuf>,
+    },
+    /// Every rewrite, to a fixed point: each step in words, and the result written out
+    Simplify {
+        file: PathBuf,
+        #[arg(long)]
+        json: bool,
+    },
+    /// How one program becomes another by checked rewrites, if the engine finds it
+    Explain {
+        a: PathBuf,
+        b: PathBuf,
+        #[arg(long)]
+        json: bool,
+    },
+}
+
+/// The steps of a simplification or an explanation, one a line.
+fn steps_text(steps: &Value) -> String {
+    steps.as_array().into_iter().flatten().enumerate().map(|(i, s)| format!("{:>3}. {}\n", i + 1, s["why"].as_str().unwrap_or(""))).collect()
+}
+
+pub fn main(cmd: Cmd) {
+    let inputs = super::INPUTS.get().cloned().unwrap_or_default();
+    let read = |p: &PathBuf| super::read_text(Some(p));
+    let r = (|| match cmd {
+        Cmd::Options { file, json } => {
+            let v = rewrite::options(&read(&file)?);
+            if let Some(e) = v["unread"].as_str() {
+                return Err(format!("{}: {e}", file.display()));
+            }
+            if json {
+                println!("{v}");
+                return Ok(());
+            }
+            if let Some(n) = v["note"].as_str() {
+                println!("{n}");
+            }
+            let opts = v["options"].as_array().cloned().unwrap_or_default();
+            if opts.is_empty() && v["note"].is_null() {
+                println!("no rewrite applies");
+            }
+            for o in &opts {
+                println!("{:<16} {}", o["id"].as_str().unwrap_or(""), o["why"].as_str().unwrap_or(""));
+            }
+            Ok(())
+        }
+        Cmd::Apply { file, id, out } => {
+            let v = rewrite::call("apply", &json!({ "qasm": read(&file)?, "id": id }))?;
+            let text = v["result"].as_str().unwrap_or("");
+            match out {
+                Some(p) => {
+                    std::fs::write(&p, text).map_err(|e| format!("{}: {e}", p.display()))?;
+                    eprintln!("{}: {}", p.display(), v["why"].as_str().unwrap_or(""));
+                }
+                None => print!("{text}"),
+            }
+            Ok(())
+        }
+        Cmd::Simplify { file, json } => {
+            let v = rewrite::call("simplify", &json!({ "qasm": read(&file)?, "inputs": inputs }))?;
+            if json {
+                println!("{v}");
+            } else {
+                eprint!("{}", steps_text(&v["steps"]));
+                eprintln!("{} gates to {}, each step checked on the qubits it touches", v["gates"][0], v["gates"][1]);
+                print!("{}", v["result"].as_str().unwrap_or(""));
+            }
+            Ok(())
+        }
+        Cmd::Explain { a, b, json } => {
+            let v = rewrite::call("explain", &json!({ "a": read(&a)?, "b": read(&b)?, "inputs": inputs }))?;
+            if json {
+                println!("{v}");
+                return Ok(());
+            }
+            if v["found"] != true {
+                println!("the engine finds no chain of rewrites between them (which proves nothing either way)");
+                return Ok(());
+            }
+            println!("{} becomes {} by these rewrites, each checked:", a.display(), b.display());
+            print!("{}", steps_text(&v["a_steps"]));
+            if v["b_steps"].as_array().is_some_and(|s| !s.is_empty()) {
+                println!("and {} reduces to the same by:", b.display());
+                print!("{}", steps_text(&v["b_steps"]));
+            }
+            if v["reordered"] == true {
+                println!("the two are then the same up to the order of gates that commute");
+            }
+            Ok(())
+        }
+    })();
+    r.unwrap_or_else(|e: String| super::die(&e));
+}

wai/wai-quantum-desktop/Cargo.lock

@@ -4130,7 +4130,7 @@ dependencies = [
 
 [[package]]
 name = "wai-quantum"
-version = "0.6.15"
+version = "0.6.16"
 dependencies = [
  "blake3",
  "ed25519-dalek",
@@ -4143,7 +4143,7 @@ dependencies = [
 
 [[package]]
 name = "wai-quantum-cli"
-version = "0.1.3"
+version = "0.1.4"
 dependencies = [
  "clap",
  "clap_complete",

wai/wai-quantum-desktop/Cargo.toml

@@ -16,7 +16,7 @@ tauri = { version = "2", features = [] }
 serde_json = { version = "1", features = ["float_roundtrip"] }
 # The assistant's model server, called by the app (a local one by default).
 ureq = { version = "3", features = ["json"] }
-wai-quantum = { version = "0.6.15", path = "../wai-quantum", default-features = false, features = ["quantum_engine", "quantum_receipt", "quantum_toolchain"] }
+wai-quantum = { version = "0.6.16", path = "../wai-quantum", default-features = false, features = ["quantum_engine", "quantum_receipt", "quantum_toolchain"] }
 wai-quantum-cli = { version = "0.1.0", path = "../wai-quantum-cli", default-features = false }
 
 [features]

wai/wai-quantum-desktop/src/main.rs

@@ -26,7 +26,7 @@ use std::process::{Child, Command, Stdio};
 use std::sync::{Arc, Mutex};
 use wai_quantum::ed25519_dalek::SigningKey;
 use wai_quantum::engine::discover::{self, Archive, Budget, Evaluator, SearchOptions, Spec, search};
-use wai_quantum::engine::{catalog, critique, draw, energy, equiv, job, locks, novelty, shortcuts, taste, versions};
+use wai_quantum::engine::{catalog, converge, critique, draw, energy, equiv, job, locks, novelty, rewrite, shortcuts, taste, versions};
 
 /// What a result says of its energy here.
 const UNMETERED: &str = "the desktop app does not meter a run's energy";
@@ -223,6 +223,27 @@ fn novelty(args: String) -> String {
         .unwrap_or_else(error_json)
 }
 
+/// `name` on the convergence monitor ([`converge::call`]): the answer, or
+/// `{error}`.
+#[tauri::command]
+fn converge(name: String, args: String) -> String {
+    serde_json::from_str::<Value>(&args)
+        .map_err(|e| format!("{name}: the arguments are not JSON: {e}"))
+        .and_then(|a| converge::call(&name, &a))
+        .map(|v| v.to_string())
+        .unwrap_or_else(error_json)
+}
+
+/// `name` on the rewrites ([`rewrite::call`]): the answer, or `{error}`.
+#[tauri::command]
+fn rewrite(name: String, args: String) -> String {
+    serde_json::from_str::<Value>(&args)
+        .map_err(|e| format!("{name}: the arguments are not JSON: {e}"))
+        .and_then(|a| rewrite::call(&name, &a))
+        .map(|v| v.to_string())
+        .unwrap_or_else(error_json)
+}
+
 /// `name` on the person's taste model ([`taste::call`]), the profile kept by
 /// the Studio and passed in the arguments: the answer, or `{error}`.
 #[tauri::command]
@@ -443,7 +464,7 @@ fn main() {
     };
     tauri::Builder::default()
         .manage(Studio { key, job_bytes: job_bytes(), running: Arc::new(Mutex::new(None)), cancelled: Arc::new(Mutex::new(false)) })
-        .invoke_handler(tauri::generate_handler![run_job, cancel, plan_job, methods, lint, critique, equivalent, variants, shortcuts, draw, layout, verify, signer, save_job, save_program, chat, models, discover_start, discover_submit, discover_search, discover_evaluate, discover_novelty, instantiate, history, locks, novelty, taste])
+        .invoke_handler(tauri::generate_handler![run_job, cancel, plan_job, methods, lint, critique, equivalent, variants, shortcuts, draw, layout, verify, signer, save_job, save_program, chat, models, discover_start, discover_submit, discover_search, discover_evaluate, discover_novelty, instantiate, history, locks, novelty, rewrite, taste, converge])
         .run(tauri::generate_context!())
         .expect("the window opens");
 }

wai/wai-quantum-qpu/Cargo.lock

@@ -422,7 +422,7 @@ checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
 
 [[package]]
 name = "wai-quantum"
-version = "0.6.15"
+version = "0.6.16"
 dependencies = [
  "blake3",
  "ed25519-dalek",

wai/wai-quantum-serve/Cargo.lock

@@ -599,7 +599,7 @@ dependencies = [
 
 [[package]]
 name = "wai-quantum"
-version = "0.6.15"
+version = "0.6.16"
 dependencies = [
  "blake3",
  "ed25519-dalek",

wai/wai-quantum-service/Cargo.lock

@@ -857,7 +857,7 @@ checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
 
 [[package]]
 name = "wai-quantum"
-version = "0.6.15"
+version = "0.6.16"
 dependencies = [
  "blake3",
  "ed25519-dalek",

wai/wai-quantum-service/src/mcp.rs

@@ -67,7 +67,7 @@ fn tools() -> Value {
         {
             "name": "check_equivalent",
             "title": "Check two quantum programs are the same circuit",
-            "description": "Whether two programs are the same circuit up to a global phase, and how the engine knows: Clifford circuits by their tableaus at any size, others on every basis state to 8 qubits, on random product states to 22 (evidence, not proof), otherwise unchecked with the reason. A check that would take long here is refused with the command that runs it locally.",
+            "description": "Whether two programs are the same circuit up to a global phase, and how the engine knows: Clifford circuits by their tableaus at any size, others on every basis state to 8 qubits, then by checked rewrites of one followed by the other's inverse to nothing (a proof at any width), then on random product states to 22 (evidence, not proof), otherwise unchecked with the reason. A check that would take long here is refused with the command that runs it locally.",
             "inputSchema": { "type": "object", "required": ["a", "b"], "properties": { "a": { "type": "string" }, "b": { "type": "string" } } },
             "annotations": { "readOnlyHint": true }
         },

wai/wai-quantum/Cargo.lock

@@ -1079,7 +1079,7 @@ checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
 
 [[package]]
 name = "wai-quantum"
-version = "0.6.15"
+version = "0.6.16"
 dependencies = [
  "blake3",
  "block2",

wai/wai-quantum/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "wai-quantum"
-version = "0.6.15"
+version = "0.6.16"
 edition = "2024"
 rust-version = "1.97"
 license = "Apache-2.0"

wai/wai-quantum/README.md

@@ -68,7 +68,7 @@ never creates information.
 | `quantum` | byte-exact statevector simulation (dyadic Clifford+T+P(k)), as `wai.quantum.circuit2` by default or as the frozen `wai.quantum.circuit` |
 | `quantum_toolchain` | algorithm library, backend recommendation, **OpenQASM 2/3 ingest of what the mainstream toolchains actually export** — both register and both measurement spellings, `rx`/`ry`/`rz`/`sx`/`u`/`u2`/`u3`/`crz`, and exact rational-multiple-of-pi angles (non-dyadic angles are refused, never rounded); **device-ready OpenQASM 2/3** (`device::device_qasm`): every gate lowered exactly to its dialect's standard library, multi-controlled gates included, every qubit measured into `c[i]`, and the service's counts read back onto the crate's basis; **native programs** (`native::compile`): a processor's own basis (`rz`/`sx`/`x`/`cz`; `prx`/`cz`; or `gpi`/`gpi2`/`zz` with angles in turns, written exactly; the Z rotations carried in the phases of the last two) on its own qubits, routed over its coupling map, and checked against the circuit by simulation before it is sent — Bloch / entanglement / purity analysis |
 | `quantum_qasm` | **the OpenQASM reader the job service runs**, for every surface that takes a program: OpenQASM 3 and the OpenQASM 2 forms in common use, every register, a gate on a whole register, gate definitions with parameters, `ctrl`/`negctrl` modifiers, angle expressions, comments, and measurement in every spelling. A program that measures and then acts, resets after a gate or uses `if` is kept as dynamic steps. Generators: integer `input`s, `const`s and `for` loops (ranges, steps, sets, nested), with integer arithmetic in indices and sizes and `if` on integers decided on reading, so one program describes a family of circuits; `qasm::parse_with` reads it at given inputs and `qasm::instantiate` writes that circuit out as plain OpenQASM. `while`, `inv`, `pow` and anything else not listed are refused with their line. Lowered to each method's input exactly up to a global phase. `qasm::dyadic_circuit` gives the exact state vector's circuit (dyadic angles) for a program whose measurements all come at the end, and refuses any other with the reason |
-| `quantum_engine` | **the quantum job service's engine, for every host**: a job (an OpenQASM program and what is asked of it: shots, Pauli expectation values, amplitudes, noise) planned onto the strongest method it admits, with the reason and the memory and work it will take; run; answered in the service's JSON with its accuracy class; and sealed over the request and the result in their canonical JSON (`engine::job`, `engine::receipt`), so a result from the service, the command line or a browser tab checks the same way. Also a program's circuit drawn as text (`engine::draw`); the specification-and-evaluator workbench (`engine::discover`: a specification, the engine's verdict on a generator at every size, and an archive of the cheapest verified generator in every cell of two measures, sealed); a program's history, attributed (`engine::versions`: versions in a sealed chain, each with who made it and how, proposals reviewed change by change, and each line and gate in the hand that wrote it, which a job's receipt can bind); the person's rules for proposals (`engine::locks`: held blocks, the gates allowed, the qubit declarations, what to avoid and a region, checked change by change); what is new in a program (`engine::novelty`: its structural distance to the known constructions and to programs given, each known construction it is proved to be and whether by a different route, and the strengths a cost did not ask for; a workbench candidate that breaks only a rule is an aberration, with the cost it would have); a person's taste (`engine::taste`: a Bradley–Terry model of their own choices between programs the engine proves equal, part by part of a rubric, with typicality shown beside it and moved only by a dial, and how well it predicts them measured); and the CPU energy the kernel counts for one process (`engine::energy`). It builds for `wasm32-unknown-unknown`, where it runs on one thread and claims no time |
+| `quantum_engine` | **the quantum job service's engine, for every host**: a job (an OpenQASM program and what is asked of it: shots, Pauli expectation values, amplitudes, noise) planned onto the strongest method it admits, with the reason and the memory and work it will take; run; answered in the service's JSON with its accuracy class; and sealed over the request and the result in their canonical JSON (`engine::job`, `engine::receipt`), so a result from the service, the command line or a browser tab checks the same way. Also a program's circuit drawn as text (`engine::draw`); the specification-and-evaluator workbench (`engine::discover`: a specification, the engine's verdict on a generator at every size, and an archive of the cheapest verified generator in every cell of two measures, sealed); a program's history, attributed (`engine::versions`: versions in a sealed chain, each with who made it and how, proposals reviewed change by change, and each line and gate in the hand that wrote it, which a job's receipt can bind); the person's rules for proposals (`engine::locks`: held blocks, the gates allowed, the qubit declarations, what to avoid and a region, checked change by change); what is new in a program (`engine::novelty`: its structural distance to the known constructions and to programs given, each known construction it is proved to be and whether by a different route, and the strengths a cost did not ask for; a workbench candidate that breaks only a rule is an aberration, with the cost it would have); convergence (`engine::converge`: along a program's history, how far the person's versions are built from a model's proposals and the model's share of the gates, with the versions made on their own set beside the rest; and a cohort's diversity, its Vendi score, centroid and narrowing over time); rewrites that keep a circuit's meaning (`engine::rewrite`: cancellations, merges, Hadamard conjugations and gates carried past what they commute with, each checked on the qubits it touches, so a chain of them proves two programs equal at any width, explains an optimisation, and offers a person one rewrite at a time); a person's taste (`engine::taste`: a Bradley–Terry model of their own choices between programs the engine proves equal, part by part of a rubric, with typicality shown beside it and moved only by a dial, and how well it predicts them measured); and the CPU energy the kernel counts for one process (`engine::energy`). It builds for `wasm32-unknown-unknown`, where it runs on one thread and claims no time |
 | `quantum_stabilizer` | stabilizer (CHP) tableau — `O(n²)`, scales far past statevector |
 | `quantum_mps` | tensor-network (matrix-product-state) backend |
 | `quantum_pauli` | sparse-Pauli / Heisenberg observable propagation over the dyadic gate set (up to 64 qubits) |

wai/wai-quantum/src/engine/converge.rs

@@ -0,0 +1,362 @@
+//! Whether a person's designs converge on a model's, and how diverse a
+//! cohort's designs are.
+//!
+//! - **Convergence** ([`history`]): along a program's history, for each
+//!   version the person made after a model proposed, how far it is built from
+//!   the proposals in its line of work (the structural distance of
+//!   [`super::novelty::distance`], 0 built alike to 1 nothing shared), and
+//!   the share of its gates in a model's hand, alone or then edited by the
+//!   person. A share that rises, or a distance that falls, over the person's
+//!   last versions is convergence.
+//! - **Exploring on one's own**: versions the person made while the
+//!   assistant only asked are marked in their note ([`ORGANIC`]). They are
+//!   the assistant-off probes, and their distance from the proposals is set
+//!   beside the rest.
+//! - **Diversity** ([`cohort`]): programs for one task (a group's, or one
+//!   person's over months), each read at the same inputs. The Vendi score,
+//!   `exp` of the entropy of the eigenvalues of `K/n` where
+//!   `K_ij = 1 − distance`, is the effective number of distinct designs: 1
+//!   when they are all built alike, `n` when no two share anything. Each
+//!   program's distance to the centroid (the mean of their gate-token bags)
+//!   and the medoid are given, and with times the score is taken in windows,
+//!   so a narrowing shows.
+//!
+//! A cohort is the programs given to whoever runs it; nothing is sent
+//! anywhere.
+
+use super::novelty;
+use super::versions::{Hand, History, Kind};
+use crate::qasm::{self, Inputs, Program};
+use serde_json::{Value, json};
+use std::collections::{BTreeMap, BTreeSet};
+
+/// What a version's note says when the person made it exploring on their own.
+pub const ORGANIC: &str = "organic exploration";
+/// The person's last versions a trend is taken over.
+const RECENT: usize = 6;
+/// A model's share of the gates at which the program is mostly the model's.
+const MOSTLY: f64 = 0.5;
+/// How fast a distance must fall, per version, to be converging.
+const FALLING: f64 = 0.05;
+
+fn round(x: f64) -> f64 {
+    (x * 1000.0).round() / 1000.0
+}
+
+/// The least-squares slope of `ys` against their index.
+fn slope(ys: &[f64]) -> Option<f64> {
+    let n = ys.len();
+    if n < 3 {
+        return None;
+    }
+    let mx = (n - 1) as f64 / 2.0;
+    let my = ys.iter().sum::<f64>() / n as f64;
+    let (mut num, mut den) = (0.0, 0.0);
+    for (i, y) in ys.iter().enumerate() {
+        num += (i as f64 - mx) * (y - my);
+        den += (i as f64 - mx).powi(2);
+    }
+    Some(num / den)
+}
+
+fn ancestry(h: &History, i: usize) -> BTreeSet<usize> {
+    let at: BTreeMap<&str, usize> = h.versions.iter().enumerate().map(|(k, v)| (v.id.as_str(), k)).collect();
+    let mut seen = BTreeSet::new();
+    let mut todo = vec![i];
+    while let Some(k) = todo.pop() {
+        if seen.insert(k) {
+            todo.extend(h.versions[k].parents.iter().filter_map(|p| at.get(p.as_str()).copied()));
+        }
+    }
+    seen
+}
+
+/// A program's convergence on the models that proposed to it, version by
+/// version, read at `inputs`: each of the person's versions after a
+/// proposal, its distance from the nearest proposal in its line of work and
+/// the models' share of its gates; the trend over the last [`RECENT`]; and
+/// the versions made exploring on one's own set beside the rest.
+pub fn history(h: &History, inputs: &Inputs) -> Result<Value, String> {
+    let read = |src: &str| qasm::parse_with(src, inputs).ok();
+    let mut series = Vec::new();
+    let (mut organic, mut assisted) = (Vec::new(), Vec::new());
+    for (i, v) in h.versions.iter().enumerate() {
+        if v.by.kind != Kind::Person {
+            continue;
+        }
+        let proposals: Vec<Program> = ancestry(h, i)
+            .into_iter()
+            .filter(|&k| k != i && h.versions[k].by.kind == Kind::Assistant)
+            .filter_map(|k| read(h.versions[k].review.as_ref().map_or(&h.versions[k].source, |r| &r.proposed)))
+            .collect();
+        if proposals.is_empty() {
+            continue;
+        }
+        let Some(p) = read(&v.source) else { continue };
+        let d = proposals.iter().map(|q| novelty::distance(&p, q)).fold(f64::INFINITY, f64::min);
+        let a = h.authorship(&v.id, inputs)?;
+        let model = [Hand::Assistant, Hand::AssistantThenPerson].iter().map(|k| a.gates.get(k).copied().unwrap_or(0)).sum::<u64>();
+        let share = if a.of.gates == 0 { 0.0 } else { model as f64 / a.of.gates as f64 };
+        let own = v.note.as_deref().is_some_and(|n| n.contains(ORGANIC));
+        (if own { &mut organic } else { &mut assisted }).push(d);
+        series.push(json!({ "version": v.id, "at": v.at, "distance": round(d), "share": round(share), "organic": own }));
+    }
+    let recent: Vec<&Value> = series.iter().rev().take(RECENT).rev().collect();
+    let ds: Vec<f64> = recent.iter().filter_map(|x| x["distance"].as_f64()).collect();
+    let ss: Vec<f64> = recent.iter().filter_map(|x| x["share"].as_f64()).collect();
+    let (dslope, sslope) = (slope(&ds), slope(&ss));
+    let share_now = h.head().ok().and_then(|v| h.authorship(&v.id, inputs).ok()).map(|a| {
+        let m = [Hand::Assistant, Hand::AssistantThenPerson].iter().map(|k| a.gates.get(k).copied().unwrap_or(0)).sum::<u64>();
+        if a.of.gates == 0 { 0.0 } else { m as f64 / a.of.gates as f64 }
+    });
+    let mostly = share_now.is_some_and(|s| s >= MOSTLY);
+    let falling = dslope.is_some_and(|s| s < -FALLING);
+    let rising = sslope.is_some_and(|s| s > 0.0);
+    let converging = mostly || (falling && rising) || (falling && ds.last().is_some_and(|&d| d < 0.25));
+    let why = if mostly {
+        format!("{:.0}% of the program's gates are a model's", share_now.unwrap_or(0.0) * 100.0)
+    } else if falling {
+        format!("the last {} versions came {:.2} closer to the model's proposals each", ds.len(), -dslope.unwrap_or(0.0))
+    } else if series.is_empty() {
+        "no version of yours follows a model's proposal yet".into()
+    } else {
+        "holding its own: not moving toward the model's proposals".into()
+    };
+    let mean = |v: &[f64]| (!v.is_empty()).then(|| round(v.iter().sum::<f64>() / v.len() as f64));
+    Ok(json!({
+        "series": series,
+        "share": share_now.map(round),
+        "distance_trend": dslope.map(round),
+        "share_trend": sslope.map(round),
+        "converging": converging,
+        "why": why,
+        "organic": { "versions": organic.len(), "distance": mean(&organic) },
+        "assisted": { "versions": assisted.len(), "distance": mean(&assisted) },
+    }))
+}
+
+/// The eigenvalues of a symmetric matrix, by cyclic Jacobi rotations.
+fn eigenvalues(mut a: Vec<Vec<f64>>) -> Vec<f64> {
+    let n = a.len();
+    for _ in 0..100 {
+        let off: f64 = (0..n).flat_map(|i| (0..n).filter(move |&j| j != i).map(move |j| (i, j))).map(|(i, j)| a[i][j] * a[i][j]).sum();
+        if off < 1e-22 {
+            break;
+        }
+        for p in 0..n {
+            for q in p + 1..n {
+                if a[p][q].abs() < 1e-300 {
+                    continue;
+                }
+                let theta = (a[q][q] - a[p][p]) / (2.0 * a[p][q]);
+                let t = theta.signum() / (theta.abs() + (theta * theta + 1.0).sqrt());
+                let t = if theta == 0.0 { 1.0 } else { t };
+                let c = 1.0 / (t * t + 1.0).sqrt();
+                let s = t * c;
+                for row in a.iter_mut() {
+                    let (akp, akq) = (row[p], row[q]);
+                    row[p] = c * akp - s * akq;
+                    row[q] = s * akp + c * akq;
+                }
+                let (lo, hi) = a.split_at_mut(q);
+                for (x, y) in lo[p].iter_mut().zip(hi[0].iter_mut()) {
+                    let (apk, aqk) = (*x, *y);
+                    *x = c * apk - s * aqk;
+                    *y = s * apk + c * aqk;
+                }
+            }
+        }
+    }
+    (0..n).map(|i| a[i][i]).collect()
+}
+
+/// The Vendi score of programs whose pairwise distances are `d`.
+fn vendi(d: &[Vec<f64>]) -> f64 {
+    let n = d.len();
+    if n == 0 {
+        return 0.0;
+    }
+    let k: Vec<Vec<f64>> = d.iter().map(|row| row.iter().map(|x| (1.0 - x) / n as f64).collect()).collect();
+    let h: f64 = eigenvalues(k).into_iter().filter(|&l| l > 1e-12).map(|l| -l * l.ln()).sum();
+    h.exp()
+}
+
+/// A program of a cohort: its name, its text and, if known, when it was made.
+#[derive(Clone, Debug)]
+pub struct Design {
+    pub name: String,
+    pub source: String,
+    pub at: Option<u64>,
+}
+
+/// How diverse `designs` are, each read at `inputs`: the Vendi score and its
+/// share of the most it could be, each one's distance to the centroid, the
+/// medoid and the one built least like the rest; with times, the score in
+/// `windows` consecutive windows and whether it narrows.
+pub fn cohort(designs: &[Design], inputs: &Inputs, windows: usize) -> Result<Value, String> {
+    let progs: Vec<Program> = designs.iter().map(|d| qasm::parse_with(&d.source, inputs).map_err(|e| format!("{} does not read: {e}", d.name))).collect::<Result<_, _>>()?;
+    let n = progs.len();
+    if n < 2 {
+        return Err("a cohort is two programs or more".into());
+    }
+    let dist: Vec<Vec<f64>> = (0..n).map(|i| (0..n).map(|j| if i == j { 0.0 } else { novelty::distance(&progs[i], &progs[j]) }).collect()).collect();
+    let score = vendi(&dist);
+    // The centroid: the mean count of every gate token and pair.
+    let bags: Vec<BTreeMap<String, u64>> = progs.iter().map(novelty::bag).collect();
+    let mut centre: BTreeMap<&str, f64> = BTreeMap::new();
+    for b in &bags {
+        for (k, c) in b {
+            *centre.entry(k.as_str()).or_default() += *c as f64 / n as f64;
+        }
+    }
+    let to_centre = |b: &BTreeMap<String, u64>| {
+        let (mut both, mut either) = (0.0, 0.0);
+        for (k, &m) in &centre {
+            let c = b.get(*k).copied().unwrap_or(0) as f64;
+            both += c.min(m);
+            either += c.max(m);
+        }
+        if either == 0.0 { 0.0 } else { 1.0 - both / either }
+    };
+    let total: Vec<f64> = dist.iter().map(|r| r.iter().sum()).collect();
+    let arg = |better: &dyn Fn(f64, f64) -> bool| (0..n).fold(0, |b, i| if better(total[i], total[b]) { i } else { b });
+    let (medoid, outlier) = (arg(&|x, y| x < y), arg(&|x, y| x > y));
+    let mut out = json!({
+        "programs": n,
+        "vendi": round(score),
+        "share": round(score / n as f64),
+        "mean_distance": round(total.iter().sum::<f64>() / (n * (n - 1)) as f64),
+        "centroid": designs.iter().zip(&bags).map(|(d, b)| json!({ "name": d.name, "distance": round(to_centre(b)) })).collect::<Vec<_>>(),
+        "medoid": designs[medoid].name,
+        "outlier": designs[outlier].name,
+    });
+    if windows >= 2 && designs.iter().all(|d| d.at.is_some()) && n >= 2 * windows {
+        let mut order: Vec<usize> = (0..n).collect();
+        order.sort_by_key(|&i| (designs[i].at, i));
+        let size = n / windows;
+        let ws: Vec<Value> = (0..windows)
+            .map(|w| {
+                let idx: Vec<usize> = order[w * size..if w + 1 == windows { n } else { (w + 1) * size }].to_vec();
+                let sub: Vec<Vec<f64>> = idx.iter().map(|&i| idx.iter().map(|&j| dist[i][j]).collect()).collect();
+                let v = vendi(&sub);
+                json!({ "from": designs[idx[0]].at, "to": designs[*idx.last().unwrap()].at, "programs": idx.len(), "vendi": round(v), "share": round(v / idx.len() as f64) })
+            })
+            .collect();
+        let shares: Vec<f64> = ws.iter().filter_map(|w| w["share"].as_f64()).collect();
+        out["narrowing"] = json!(shares.first().zip(shares.last()).is_some_and(|(a, b)| b < &(a - 0.05)));
+        out["windows"] = json!(ws);
+    }
+    Ok(out)
+}
+
+fn inputs_of(args: &Value) -> Result<Inputs, String> {
+    match args.get("inputs") {
+        None | Some(Value::Null) => Ok(Inputs::new()),
+        Some(v) => serde_json::from_value(v.clone()).map_err(|e| format!("inputs: {e}")),
+    }
+}
+
+/// The monitor as a page, an app or an agent calls it, with JSON arguments:
+/// `history` (`history`, `inputs`) and `cohort` (`programs`: `[{name, qasm,
+/// at?}]`, `inputs`, `windows`).
+pub fn call(op: &str, args: &Value) -> Result<Value, String> {
+    let inputs = inputs_of(args)?;
+    match op {
+        "history" => history(&History::from_json(args.get("history").ok_or("history: give \"history\"")?)?, &inputs),
+        "cohort" => {
+            let designs: Vec<Design> = args
+                .get("programs")
+                .and_then(Value::as_array)
+                .ok_or("cohort: give \"programs\": [{name, qasm, at?}]")?
+                .iter()
+                .map(|p| Ok(Design { name: p.get("name").and_then(Value::as_str).ok_or("a program needs a name")?.to_string(), source: p.get("qasm").and_then(Value::as_str).ok_or("a program needs its qasm")?.to_string(), at: p.get("at").and_then(Value::as_u64) }))
+                .collect::<Result<_, String>>()?;
+            cohort(&designs, &inputs, args.get("windows").and_then(Value::as_u64).unwrap_or(3) as usize)
+        }
+        _ => Err(format!("{op}: no such call on the convergence monitor")),
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::engine::versions::By;
+
+    fn d(name: &str, src: &str, at: u64) -> Design {
+        Design { name: name.into(), source: src.into(), at: Some(at) }
+    }
+
+    #[test]
+    fn the_vendi_score_counts_distinct_designs() {
+        let a = "OPENQASM 3.0;\nqubit[3] q;\nh q[0];\ncx q[0], q[1];\ncx q[1], q[2];\n";
+        let alike = [d("a", a, 1), d("b", a, 2), d("c", a, 3)];
+        let r = cohort(&alike, &Inputs::new(), 0).unwrap();
+        assert!((r["vendi"].as_f64().unwrap() - 1.0).abs() < 1e-3, "three alike are one design: {r}");
+        let apart = [d("x", "OPENQASM 3.0;\nqubit[1] q;\nh q[0];\n", 1), d("y", "OPENQASM 3.0;\nqubit[1] q;\nt q[0];\n", 2), d("z", "OPENQASM 3.0;\nqubit[1] q;\nx q[0];\n", 3)];
+        let r = cohort(&apart, &Inputs::new(), 0).unwrap();
+        assert!((r["vendi"].as_f64().unwrap() - 3.0).abs() < 1e-3, "three that share nothing are three: {r}");
+        let mixed = [d("a", a, 1), d("b", a, 2), d("x", "OPENQASM 3.0;\nqubit[1] q;\nh q[0];\n", 3)];
+        let r = cohort(&mixed, &Inputs::new(), 0).unwrap();
+        let v = r["vendi"].as_f64().unwrap();
+        assert!(v > 1.0 && v < 3.0, "{r}");
+        assert_eq!(r["outlier"], "x");
+        assert!(cohort(&mixed[..1], &Inputs::new(), 0).unwrap_err().contains("two programs"));
+    }
+
+    /// Designs that start varied and end alike: the score in windows narrows.
+    #[test]
+    fn a_narrowing_cohort_shows_over_time() {
+        let gates = ["h", "t", "x", "s", "z", "sx"];
+        let mut ds = Vec::new();
+        for (i, g) in gates.iter().enumerate() {
+            ds.push(d(&format!("early {i}"), &format!("OPENQASM 3.0;\nqubit[1] q;\n{g} q[0];\n"), i as u64));
+        }
+        for i in 0..6 {
+            ds.push(d(&format!("late {i}"), "OPENQASM 3.0;\nqubit[2] q;\nh q[0];\ncx q[0], q[1];\n", 100 + i));
+        }
+        let r = cohort(&ds, &Inputs::new(), 2).unwrap();
+        assert_eq!(r["windows"].as_array().unwrap().len(), 2, "{r}");
+        assert_eq!(r["narrowing"], true, "{r}");
+    }
+
+    /// A person who takes a model's proposal and then edits less and less
+    /// away from it is converging; versions made on their own are set apart.
+    #[test]
+    fn convergence_on_a_model_s_proposals_is_measured() {
+        let bell = "OPENQASM 3.0;\nqubit[3] q;\nh q[0];\n";
+        let mut h = History::start(bell, By::new(Kind::Person, None), None, 1, None).unwrap();
+        let model = "OPENQASM 3.0;\nqubit[3] q;\nh q[0];\ncx q[0], q[1];\ncx q[1], q[2];\n";
+        h.propose("v0", model, &[0], By::new(Kind::Assistant, Some("m")), None, 2, None).unwrap();
+        let mut parent = "v1".to_string();
+        for (k, extra) in ["x q[2];\nz q[1];\n", "x q[2];\n", ""].iter().enumerate() {
+            let src = format!("{model}{extra}");
+            if src == h.get(&parent).unwrap().source {
+                continue;
+            }
+            parent = h.commit(&parent, &src, By::new(Kind::Person, None), None, 3 + k as u64, None).unwrap().id.clone();
+        }
+        let own = format!("{bell}h q[1];\nh q[2];\n");
+        h.commit(&parent, &own, By::new(Kind::Person, None), Some(ORGANIC), 9, None).unwrap();
+        let r = history(&h, &Inputs::new()).unwrap();
+        let series = r["series"].as_array().unwrap();
+        assert!(series.len() >= 2, "{r}");
+        assert_eq!((r["organic"]["versions"].as_u64(), r["assisted"]["versions"].as_u64().map(|n| n >= 1)), (Some(1), Some(true)), "{r}");
+        assert!(r["organic"]["distance"].as_f64().unwrap() > r["assisted"]["distance"].as_f64().unwrap(), "on its own it is built further from the proposal: {r}");
+        let start = History::start(bell, By::new(Kind::Person, None), None, 1, None).unwrap();
+        assert_eq!(history(&start, &Inputs::new()).unwrap()["converging"], false);
+    }
+
+    #[test]
+    fn mostly_a_model_s_program_is_converging() {
+        let mut h = History::start("OPENQASM 3.0;\nqubit[2] q;\n", By::new(Kind::Person, None), None, 1, None).unwrap();
+        let model = "OPENQASM 3.0;\nqubit[2] q;\nh q[0];\ncx q[0], q[1];\nx q[1];\n";
+        h.propose("v0", model, &[0], By::new(Kind::Assistant, Some("m")), None, 2, None).unwrap();
+        h.commit("v1", &format!("{model}z q[0];\n"), By::new(Kind::Person, None), None, 3, None).unwrap();
+        let r = call("history", &json!({ "history": h })).unwrap();
+        assert_eq!(r["converging"], true, "{r}");
+        assert!(r["why"].as_str().unwrap().contains("% of the program's gates are a model's"), "{r}");
+        let c = call("cohort", &json!({ "programs": [{ "name": "a", "qasm": model }, { "name": "b", "qasm": "OPENQASM 3.0;\nqubit[2] q;\nt q[0];\n" }] })).unwrap();
+        assert_eq!(c["programs"], 2);
+        assert!(call("nonsense", &json!({})).unwrap_err().contains("no such call"));
+    }
+}

wai/wai-quantum/src/engine/critique.rs

@@ -70,7 +70,7 @@ pub fn kind_name(k: Kind) -> &'static str {
 
 /// One change to a line of the source (lines from 1).
 #[derive(Clone, Debug, PartialEq)]
-enum Edit {
+pub(super) enum Edit {
     Delete(usize),
     Replace(usize, String),
 }
@@ -424,7 +424,7 @@ fn smells(src: &str, p: &Program, lines: &[usize]) -> Vec<Smell> {
 }
 
 /// `src` with `edits` made (lines from 1).
-fn apply(src: &str, edits: &[Edit]) -> String {
+pub(super) fn apply(src: &str, edits: &[Edit]) -> String {
     let mut text: Vec<Option<String>> = src.split('\n').map(|l| Some(l.to_string())).collect();
     for e in edits {
         match e {

wai/wai-quantum/src/engine/discover.rs

@@ -187,7 +187,7 @@ fn describe(inputs: &Inputs) -> String {
 /// How strong a passed check is: a proof up to rounding, or a check.
 fn rank(how: &str) -> u8 {
     match how {
-        "tableau" | "exact" | "state" => 2,
+        "tableau" | "exact" | "state" | "rewrites" => 2,
         "random" => 1,
         _ => 0,
     }

wai/wai-quantum/src/engine/equiv.rs

@@ -12,6 +12,11 @@
 //! - **exact**: at most [`EXACT_MAX_QUBITS`] qubits (and within a work budget).
 //!   Every basis state `|k⟩` is run through both, and the outputs must agree
 //!   with one phase for all `k`. Exact up to rounding.
+//! - **rewrites**: wider than the exact check affords, at any width and with
+//!   any gates: one program followed by the other's inverse is rewritten to
+//!   nothing by rewrites the engine checks one window at a time
+//!   ([`super::rewrite::prove`]). A proof when it reduces; when it does not,
+//!   nothing is concluded and the next check runs.
 //! - **random**: at most [`RANDOM_MAX_QUBITS`] qubits. [`RANDOM_INPUTS`]
 //!   product states with seeded random angles are run through both. Two
 //!   different unitaries agree on such a state with probability zero, so this
@@ -78,6 +83,9 @@ pub fn equivalent_programs(a: &Program, b: &Program) -> Value {
         let inputs: Vec<Vec<Gate>> = (0..1usize << n).map(|k| basis(n, k)).collect();
         return compare(n, &ga, &gb, &inputs, "exact", |k| format!("|{}⟩", bits(n, k)));
     }
+    if let Some(v) = super::rewrite::prove(a, b) {
+        return v;
+    }
     if n <= RANDOM_MAX_QUBITS {
         let mut s = 0x2545_f491_4f6c_dd1du64;
         let inputs: Vec<Vec<Gate>> = (0..RANDOM_INPUTS).map(|_| random_product(n, &mut s)).collect();
@@ -86,6 +94,24 @@ pub fn equivalent_programs(a: &Program, b: &Program) -> Value {
     json!({ "verdict": "unchecked", "how": "none", "why": format!("{n} qubits and not both Clifford: wider than this check runs ({RANDOM_MAX_QUBITS} qubits)") })
 }
 
+/// Whether the engine proves two programs of at most [`EXACT_MAX_QUBITS`]
+/// qubits the same unitary up to a global phase, by their tableaus or on
+/// every basis state, and by nothing weaker: what a rewrite's window is
+/// checked with.
+pub(crate) fn proved_equal(a: &Program, b: &Program) -> bool {
+    let n = a.n_qubits;
+    if n != b.n_qubits || n > EXACT_MAX_QUBITS {
+        return false;
+    }
+    if let (Ok(ca), Ok(cb)) = (a.clifford(), b.clifford())
+        && let (Ok(ta), Ok(tb)) = (Tableau::run(n, &ca), Tableau::run(n, &cb))
+    {
+        return ta == tb;
+    }
+    let inputs: Vec<Vec<Gate>> = (0..1usize << n).map(|k| basis(n, k)).collect();
+    compare(n, &a.matrices(), &b.matrices(), &inputs, "exact", |k| format!("|{}⟩", bits(n, k)))["verdict"] == "equivalent"
+}
+
 /// Whether `a` and `b` prepare the same state from `|0…0⟩`, up to a global
 /// phase, as JSON in the form of [`equivalent_programs`]: a weaker question
 /// than the same unitary, and the one a state-preparation circuit answers.
@@ -218,10 +244,16 @@ mod tests {
     }
 
     #[test]
-    fn wide_programs_take_the_random_check_and_shapes_are_compared_first() {
+    fn wide_programs_are_proved_by_rewriting_or_take_the_random_check_and_shapes_are_compared_first() {
         let a = "qubit[12] q; h q; rx(0.25) q[3]; rx(0.5) q[3]; cx q[3], q[9]; rz(1.1) q[11];";
         let b = "qubit[12] q; h q; rx(0.75) q[3]; cx q[3], q[9]; rz(1.1) q[11];";
         let r = equivalent(a, b);
+        assert_eq!((r["verdict"].as_str().unwrap(), r["how"].as_str().unwrap()), ("equivalent", "rewrites"), "{r}");
+        // A swap written as three cx is no pair of gates that cancel or merge:
+        // random inputs decide it, and say that is not a proof.
+        let s1 = "qubit[12] q; h q; swap q[3], q[9]; rz(1.1) q[11];";
+        let s2 = "qubit[12] q; h q; cx q[3], q[9]; cx q[9], q[3]; cx q[3], q[9]; rz(1.1) q[11];";
+        let r = equivalent(s1, s2);
         assert_eq!((r["verdict"].as_str().unwrap(), r["how"].as_str().unwrap()), ("equivalent", "random"), "{r}");
         assert!(r["why"].as_str().unwrap().contains("not a proof"));
         let c = "qubit[12] q; h q; rx(0.75) q[3]; cx q[3], q[9]; rz(1.0) q[11];";

wai/wai-quantum/src/engine/mod.rs

@@ -18,12 +18,21 @@
 //! - [`job`] (with `quantum_receipt`): a job end to end, planned, run and
 //!   sealed, in the service's form; its check; and a program's lint.
 //! - [`draw`]: a program's circuit as text.
+//! - [`converge`] (with `quantum_receipt`): whether a person's designs
+//!   converge on a model's proposals along a program's history, and how
+//!   diverse a cohort's designs are (the Vendi score, the centroid, the
+//!   score over time).
 //! - [`critique`]: what the engine can say about a design before it runs (its
 //!   measures and its smells, each with its lines), and the variants its fixes
 //!   make, each checked equivalent before it is offered.
 //! - [`equiv`]: whether two programs apply the same gates up to a global
 //!   phase, and how that was decided (a tableau, every basis state, or random
 //!   product states).
+//! - [`rewrite`]: rewrites that keep a circuit's meaning, each checked on
+//!   the qubits it touches: a gate and its inverse cancel, rotations merge,
+//!   Hadamards conjugate, a gate is carried past what it commutes with. A
+//!   chain of them explains an optimisation, offers a person one rewrite at a
+//!   time, and proves two programs equal at any width.
 //! - [`shortcuts`]: every exact classical route the engine knows for a
 //!   circuit, each with its cost on it, and the cheapest for each question. A
 //!   cheap route proves a design classically easy; none being cheap proves
@@ -59,6 +68,8 @@
 //! whatever hosts the engine.
 
 pub mod catalog;
+#[cfg(feature = "quantum_receipt")]
+pub mod converge;
 pub mod critique;
 pub mod draw;
 pub mod dynamic;
@@ -74,6 +85,7 @@ pub mod locks;
 pub mod novelty;
 #[cfg(feature = "quantum_receipt")]
 pub mod receipt;
+pub mod rewrite;
 pub mod run;
 pub mod shortcuts;
 #[cfg(feature = "quantum_receipt")]

wai/wai-quantum/src/engine/novelty.rs

@@ -87,7 +87,7 @@ pub(super) fn token(op: &qasm::Op) -> String {
     format!("{}:{}", critique::kind_name(op.kind), rel.join(","))
 }
 
-fn bag(p: &Program) -> BTreeMap<String, u64> {
+pub(super) fn bag(p: &Program) -> BTreeMap<String, u64> {
     let toks: Vec<String> = p.ops.iter().map(token).collect();
     let mut m = BTreeMap::new();
     for t in &toks {

wai/wai-quantum/src/engine/rewrite.rs

@@ -0,0 +1,756 @@
+//! Rewrites that keep a circuit's meaning, each checked by the engine, and
+//! equivalence proved by them at any width.
+//!
+//! - **A rewrite** takes a few gates that sit together on their qubits (no
+//!   gate between them acts on those qubits, or every one that does commutes
+//!   with the gate carried past it) and puts others on the same qubits. The
+//!   engine checks the gates it takes against the ones it puts, on just the
+//!   qubits they touch, by tableau or on every basis state
+//!   ([`equiv::proved_equal`]). So a rewrite keeps the whole circuit's
+//!   unitary, up to a global phase, at any width and with any gates: the
+//!   proof is local, and no rule is trusted, only checked.
+//! - **The rules** propose; the check decides. A gate and its inverse cancel;
+//!   two rotations about one axis merge; a gate between two Hadamards
+//!   becomes its conjugate (`h x h` is `z`, `h cx h` on the target is `cz`);
+//!   a gate that does nothing is dropped; a gate is carried past gates it
+//!   commutes with to cancel or merge with its partner; and two gates that
+//!   commute trade places.
+//! - **A chain** of rewrites carries a program to a simpler one, and is a
+//!   readable account of an optimisation ([`explain`]).
+//! - **Equivalence by rewriting** ([`prove`]): one program followed by the
+//!   other's inverse is rewritten toward nothing. If nothing is left, the two
+//!   are the same unitary up to a global phase, at any number of qubits. If
+//!   something is left, nothing is concluded.
+//! - **The lens** ([`options`]): every rewrite the program admits, each as an
+//!   edit to its own lines, so a person can take one at a time.
+
+use super::critique::{self, Edit};
+use super::equiv;
+use crate::qasm::{self, Inputs, Kind, Op, Program};
+use serde_json::{Value, json};
+use std::cell::RefCell;
+use std::collections::{BTreeSet, HashMap};
+use std::f64::consts::PI;
+
+/// The most rewrites one simplification takes.
+pub const MAX_STEPS: usize = 1 << 15;
+/// The most gates a proof rewrites (one program and the other's inverse).
+pub const MAX_GATES: usize = 1 << 13;
+/// How many gates on its qubits a gate is carried past to meet its partner.
+const REACH: usize = 32;
+const EPS: f64 = 1e-9;
+
+/// What a rewrite does.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum Rule {
+    Cancel,
+    Merge,
+    Conjugate,
+    Drop,
+    Through,
+    Move,
+}
+
+impl Rule {
+    pub fn name(self) -> &'static str {
+        match self {
+            Rule::Cancel => "cancel",
+            Rule::Merge => "merge",
+            Rule::Conjugate => "conjugate",
+            Rule::Drop => "drop",
+            Rule::Through => "through",
+            Rule::Move => "move",
+        }
+    }
+}
+
+/// One checked rewrite of a program's gates: the gates it takes (their
+/// indices), the gates it puts (each where a taken gate was), and what it
+/// does in words.
+#[derive(Clone, Debug)]
+pub struct Step {
+    pub rule: Rule,
+    pub take: Vec<usize>,
+    pub put: Vec<(usize, Op)>,
+    pub why: String,
+}
+
+/// The check every rewrite passes, remembered by the gates it compared.
+#[derive(Default)]
+struct Checker {
+    seen: RefCell<HashMap<String, bool>>,
+}
+
+impl Checker {
+    /// Whether `before` and `after` are the same unitary on the qubits they
+    /// touch.
+    fn same(&self, before: &[&Op], after: &[&Op]) -> bool {
+        let mut qs: Vec<u32> = before.iter().chain(after).flat_map(|o| o.qubits.iter().copied()).collect();
+        qs.sort_unstable();
+        qs.dedup();
+        if qs.is_empty() || qs.len() as u32 > equiv::EXACT_MAX_QUBITS {
+            return false;
+        }
+        let local = |o: &&Op| Op { kind: o.kind, qubits: o.qubits.iter().map(|q| qs.binary_search(q).unwrap_or(0) as u32).collect(), params: o.params.clone() };
+        let (b, a): (Vec<Op>, Vec<Op>) = (before.iter().map(local).collect(), after.iter().map(local).collect());
+        let key = format!("{b:?}|{a:?}");
+        if let Some(&r) = self.seen.borrow().get(&key) {
+            return r;
+        }
+        let prog = |ops: Vec<Op>| Program { n_qubits: qs.len() as u32, ops, measured: Vec::new(), n_bits: 0, dynamic: None };
+        let r = equiv::proved_equal(&prog(b), &prog(a));
+        self.seen.borrow_mut().insert(key, r);
+        r
+    }
+
+    fn commute(&self, a: &Op, b: &Op) -> bool {
+        a.qubits.iter().all(|q| !b.qubits.contains(q)) || self.same(&[a, b], &[b, a])
+    }
+}
+
+/// A gate's inverse, as gates.
+pub fn inverse(op: &Op) -> Vec<Op> {
+    use Kind::*;
+    let p = &op.params;
+    let one = |kind, params: Vec<f64>| vec![Op { kind, qubits: op.qubits.clone(), params }];
+    match op.kind {
+        Id | X | Y | Z | H | Cx | Cy | Cz | Ch | Swap | Ccx | Ccz | Cswap => vec![op.clone()],
+        S => one(Sdg, vec![]),
+        Sdg => one(S, vec![]),
+        T => one(Tdg, vec![]),
+        Tdg => one(T, vec![]),
+        Sx => one(Sxdg, vec![]),
+        Sxdg => one(Sx, vec![]),
+        Rx | Ry | Rz | P | Crx | Cry | Crz | Cp | Rxx | Ryy | Rzz => one(op.kind, vec![-p[0]]),
+        U => one(U, vec![-p[0], -p[2], -p[1]]),
+        Cu => one(Cu, vec![-p[0], -p[2], -p[1], -p[3]]),
+        // iswap⁴ is the identity.
+        Iswap => vec![op.clone(), op.clone(), op.clone()],
+    }
+}
+
+/// An angle as a person reads it: a multiple of π where it is one.
+pub fn angle(x: f64) -> String {
+    if x.abs() < EPS {
+        return "0".into();
+    }
+    for d in [1i64, 2, 3, 4, 6, 8] {
+        let k = x * d as f64 / PI;
+        if (k - k.round()).abs() < 1e-9 {
+            let k = k.round() as i64;
+            let num = match k {
+                1 => "π".to_string(),
+                -1 => "-π".to_string(),
+                _ => format!("{k}π"),
+            };
+            return if d == 1 { num } else { format!("{num}/{d}") };
+        }
+    }
+    let s = format!("{x:.6}");
+    s.trim_end_matches('0').trim_end_matches('.').to_string()
+}
+
+/// A gate as a person reads it, on the qubits `q[i]` in the order it takes them.
+pub fn op_text(o: &Op) -> String {
+    let params = if o.params.is_empty() { String::new() } else { format!("({})", o.params.iter().map(|&x| angle(x)).collect::<Vec<_>>().join(", ")) };
+    let qs: Vec<String> = o.qubits.iter().map(|q| format!("q[{q}]")).collect();
+    format!("{}{params} {}", critique::kind_name(o.kind), qs.join(", "))
+}
+
+fn qset(o: &Op) -> Vec<u32> {
+    let mut v = o.qubits.clone();
+    v.sort_unstable();
+    v
+}
+
+const ROTATIONS: &[Kind] = &[Kind::Rx, Kind::Ry, Kind::Rz, Kind::P, Kind::Crx, Kind::Cry, Kind::Crz, Kind::Cp, Kind::Rxx, Kind::Ryy, Kind::Rzz];
+
+/// A one-qubit gate's angle, if it is a phase gate: `z`, `s`, `t`, their
+/// inverses and `p` (`rz` merges only with `rz`).
+fn phase_angle(o: &Op) -> Option<f64> {
+    use Kind::*;
+    Some(match o.kind {
+        Z => PI,
+        S => PI / 2.0,
+        Sdg => -PI / 2.0,
+        T => PI / 4.0,
+        Tdg => -PI / 4.0,
+        P => o.params[0],
+        _ => return None,
+    })
+}
+
+/// The phase gate of angle `a`, by name where it has one; `None` for none.
+fn phase_gate(a: f64, q: u32) -> Option<Op> {
+    use Kind::*;
+    let r = a.rem_euclid(2.0 * PI);
+    let near = |x: f64| (r - x).abs() < EPS || (r - x - 2.0 * PI).abs() < EPS;
+    let named = |kind| Some(Op { kind, qubits: vec![q], params: vec![] });
+    if near(0.0) {
+        None
+    } else if near(PI) {
+        named(Z)
+    } else if near(PI / 2.0) {
+        named(S)
+    } else if near(1.5 * PI) {
+        named(Sdg)
+    } else if near(PI / 4.0) {
+        named(T)
+    } else if near(1.75 * PI) {
+        named(Tdg)
+    } else {
+        Some(Op { kind: P, qubits: vec![q], params: vec![a] })
+    }
+}
+
+/// Two gates on the same qubits as one: `Some(None)` when they make
+/// nothing, `Some(Some(op))` for the one gate they make.
+fn merged(a: &Op, b: &Op) -> Option<Option<Op>> {
+    if a.kind == b.kind && a.qubits == b.qubits && ROTATIONS.contains(&a.kind) {
+        let sum = a.params[0] + b.params[0];
+        return Some(if sum.abs() < EPS { None } else { Some(Op { kind: a.kind, qubits: a.qubits.clone(), params: vec![sum] }) });
+    }
+    if a.qubits.len() == 1 && a.qubits == b.qubits {
+        let (x, y) = (phase_angle(a)?, phase_angle(b)?);
+        return Some(phase_gate(x + y, a.qubits[0]));
+    }
+    None
+}
+
+/// The conjugate of a gate between two Hadamards on qubit `q`.
+fn conjugate(j: &Op, q: u32) -> Option<Op> {
+    use Kind::*;
+    let on = |kind, params: Vec<f64>| Some(Op { kind, qubits: j.qubits.clone(), params });
+    if j.qubits == [q] {
+        return match j.kind {
+            X => on(Z, vec![]),
+            Z => on(X, vec![]),
+            Y => on(Y, vec![]),
+            S => on(Sx, vec![]),
+            Sdg => on(Sxdg, vec![]),
+            Sx => on(S, vec![]),
+            Sxdg => on(Sdg, vec![]),
+            Rx => on(Rz, j.params.clone()),
+            Rz => on(Rx, j.params.clone()),
+            Ry => on(Ry, vec![-j.params[0]]),
+            P => on(Rx, j.params.clone()),
+            T => on(Rx, vec![PI / 4.0]),
+            Tdg => on(Rx, vec![-PI / 4.0]),
+            _ => None,
+        };
+    }
+    match j.kind {
+        Cx if j.qubits.get(1) == Some(&q) => on(Cz, vec![]),
+        Cz if j.qubits.contains(&q) => {
+            let c = if j.qubits[0] == q { j.qubits[1] } else { j.qubits[0] };
+            Some(Op { kind: Cx, qubits: vec![c, q], params: vec![] })
+        }
+        _ => None,
+    }
+}
+
+/// The gate after `i` on qubit `q`, if any.
+fn next_on(ops: &[Op], i: usize, q: u32) -> Option<usize> {
+    (i + 1..ops.len()).find(|&k| ops[k].qubits.contains(&q))
+}
+
+/// Whether no gate strictly between `i` and `j` acts on a qubit of either.
+fn adjacent(ops: &[Op], i: usize, j: usize) -> bool {
+    (i + 1..j).all(|k| !ops[k].qubits.iter().any(|q| ops[i].qubits.contains(q) || ops[j].qubits.contains(q)))
+}
+
+/// A cancellation or merge of the gates at `i` and `j`, if the check holds.
+fn pair(ops: &[Op], i: usize, j: usize, ck: &Checker, through: &[usize]) -> Option<Step> {
+    let (a, b) = (&ops[i], &ops[j]);
+    if qset(a) != qset(b) {
+        return None;
+    }
+    let via = if through.is_empty() { String::new() } else { format!(", carried past {}, which it commutes with,", through.iter().map(|&k| op_text(&ops[k])).collect::<Vec<_>>().join(" and ")) };
+    let rule = |r| if through.is_empty() { r } else { Rule::Through };
+    // The merged gate goes where the later one was: the earlier one is carried to it.
+    if ck.same(&[a, b], &[]) {
+        return Some(Step { rule: rule(Rule::Cancel), take: vec![i, j], put: vec![], why: format!("{}{via} and {} cancel", op_text(a), op_text(b)) });
+    }
+    if let Some(Some(m)) = merged(a, b)
+        && ck.same(&[a, b], &[&m])
+    {
+        return Some(Step { rule: rule(Rule::Merge), take: vec![i, j], put: vec![(j, m.clone())], why: format!("{}{via} and {} merge into {}", op_text(a), op_text(b), op_text(&m)) });
+    }
+    None
+}
+
+/// The rewrites that start at gate `i`: dropped, cancelled or merged with
+/// its neighbour, conjugated between Hadamards, carried to its partner, or
+/// (with `moves`) traded with a neighbour it commutes with.
+fn steps_at(ops: &[Op], i: usize, ck: &Checker, moves: bool) -> Vec<Step> {
+    let mut out = Vec::new();
+    let o = &ops[i];
+    if (o.kind == Kind::Id || (!o.params.is_empty() && o.params.iter().all(|p| p.rem_euclid(2.0 * PI) < EPS || (2.0 * PI - p.rem_euclid(2.0 * PI)) < EPS))) && ck.same(&[o], &[]) {
+        out.push(Step { rule: Rule::Drop, take: vec![i], put: vec![], why: format!("{} does nothing", op_text(o)) });
+    }
+    let mut next: BTreeSet<usize> = BTreeSet::new();
+    for &q in &o.qubits {
+        if let Some(j) = next_on(ops, i, q)
+            && adjacent(ops, i, j)
+        {
+            next.insert(j);
+        }
+    }
+    for &j in &next {
+        if let Some(s) = pair(ops, i, j, ck, &[]) {
+            out.push(s);
+        } else if moves && ck.commute(o, &ops[j]) {
+            out.push(Step { rule: Rule::Move, take: vec![i, j], put: vec![(i, ops[j].clone()), (j, o.clone())], why: format!("{} and {} commute: they trade places", op_text(o), op_text(&ops[j])) });
+        }
+    }
+    if o.kind == Kind::H {
+        let q = o.qubits[0];
+        if let Some(j) = next_on(ops, i, q)
+            && let Some(k) = next_on(ops, j, q)
+            && ops[k].kind == Kind::H
+            && ops[k].qubits == [q]
+            && let Some(c) = conjugate(&ops[j], q)
+            && ops[j].qubits.iter().all(|&r| r == q || (i + 1..k).filter(|&m| m != j).all(|m| !ops[m].qubits.contains(&r)))
+            && ck.same(&[o, &ops[j], &ops[k]], &[&c])
+        {
+            out.push(Step { rule: Rule::Conjugate, take: vec![i, j, k], put: vec![(j, c.clone())], why: format!("{} between two h q[{q}] is {}", op_text(&ops[j]), op_text(&c)) });
+        }
+    }
+    // Carried along its qubits, past gates it commutes with, to a partner.
+    let mut passed = Vec::new();
+    let mut k = i;
+    while passed.len() < REACH {
+        let Some(j) = (k + 1..ops.len()).find(|&m| ops[m].qubits.iter().any(|q| o.qubits.contains(q))) else { break };
+        if !passed.is_empty()
+            && let Some(s) = pair(ops, i, j, ck, &passed)
+        {
+            out.push(s);
+            break;
+        }
+        if !ck.commute(o, &ops[j]) {
+            break;
+        }
+        passed.push(j);
+        k = j;
+    }
+    out
+}
+
+/// `ops` with `step` made.
+pub fn apply(ops: &[Op], step: &Step) -> Vec<Op> {
+    let mut out = Vec::with_capacity(ops.len());
+    for (i, o) in ops.iter().enumerate() {
+        if step.take.contains(&i) {
+            out.extend(step.put.iter().filter(|(at, _)| *at == i).map(|(_, p)| p.clone()));
+        } else {
+            out.push(o.clone());
+        }
+    }
+    out
+}
+
+fn simplify_ops(ops: &[Op], ck: &Checker) -> (Vec<Op>, Vec<Step>) {
+    let mut cur = ops.to_vec();
+    let mut steps = Vec::new();
+    // After a rewrite the search takes up a little before it, and the whole
+    // program is searched once more before it stops.
+    let mut from = 0;
+    while steps.len() < MAX_STEPS {
+        match (from..cur.len()).find_map(|i| steps_at(&cur, i, ck, false).into_iter().next().map(|s| (i, s))) {
+            Some((i, s)) => {
+                cur = apply(&cur, &s);
+                steps.push(s);
+                from = i.saturating_sub(REACH * 4);
+            }
+            None if from > 0 => from = 0,
+            None => break,
+        }
+    }
+    (cur, steps)
+}
+
+/// `p` simplified by checked rewrites, to a fixed point: the gates left and
+/// each rewrite taken, in order.
+pub fn simplify(p: &Program) -> (Vec<Op>, Vec<Step>) {
+    simplify_ops(&p.ops, &Checker::default())
+}
+
+/// The gates of `ops` in one order fixed by their dependencies alone: two
+/// programs whose gates differ only in the order of gates on different
+/// qubits give the same list.
+pub fn canonical(ops: &[Op]) -> Vec<Op> {
+    let n = ops.iter().flat_map(|o| o.qubits.iter()).max().map_or(0, |&q| q as usize + 1);
+    let mut last: Vec<Option<usize>> = vec![None; n];
+    let mut after: Vec<Vec<usize>> = vec![Vec::new(); ops.len()];
+    let mut waiting = vec![0usize; ops.len()];
+    for (i, o) in ops.iter().enumerate() {
+        let mut before: BTreeSet<usize> = BTreeSet::new();
+        for &q in &o.qubits {
+            if let Some(p) = last[q as usize] {
+                before.insert(p);
+            }
+            last[q as usize] = Some(i);
+        }
+        waiting[i] = before.len();
+        for p in before {
+            after[p].push(i);
+        }
+    }
+    let key = |i: usize| (ops[i].qubits.clone(), critique::kind_name(ops[i].kind), ops[i].params.iter().map(|x| x.to_bits()).collect::<Vec<_>>(), i);
+    let mut ready: BTreeSet<_> = (0..ops.len()).filter(|&i| waiting[i] == 0).map(key).collect();
+    let mut out = Vec::with_capacity(ops.len());
+    while let Some(k) = ready.pop_first() {
+        let i = k.3;
+        out.push(ops[i].clone());
+        for &j in &after[i] {
+            waiting[j] -= 1;
+            if waiting[j] == 0 {
+                ready.insert(key(j));
+            }
+        }
+    }
+    out
+}
+
+fn same_ops(a: &[Op], b: &[Op]) -> bool {
+    a.len() == b.len() && a.iter().zip(b).all(|(x, y)| x.kind == y.kind && x.qubits == y.qubits && x.params.len() == y.params.len() && x.params.iter().zip(&y.params).all(|(p, q)| (p - q).abs() < 1e-9))
+}
+
+/// Whether `a` and `b` are proved the same unitary up to a global phase by
+/// rewriting `a` followed by `b`'s inverse to nothing: the verdict in
+/// [`equiv::equivalent_programs`]'s form, or `None` when it does not reduce
+/// (which concludes nothing).
+pub fn prove(a: &Program, b: &Program) -> Option<Value> {
+    if a.dynamic.is_some() || b.dynamic.is_some() || a.n_qubits != b.n_qubits || a.measured != b.measured || a.ops.len() + b.ops.len() > MAX_GATES {
+        return None;
+    }
+    let mut ops = a.ops.clone();
+    for o in b.ops.iter().rev() {
+        ops.extend(inverse(o));
+    }
+    let (rest, steps) = simplify_ops(&ops, &Checker::default());
+    rest.is_empty().then(|| {
+        json!({
+            "verdict": "equivalent",
+            "how": "rewrites",
+            "why": format!("the first followed by the second's inverse rewrites to nothing in {} steps, each checked on the qubits it touches: the same unitary up to a global phase, at any number of qubits", steps.len()),
+            "steps": steps.len(),
+        })
+    })
+}
+
+/// How `a` becomes `b` by checked rewrites, if the engine finds it: each
+/// simplified to a fixed point, and the two forms compared, gate for gate
+/// or, where they differ in the order of gates that commute, by
+/// [`prove`] (`reordered`). `a_steps` and `b_steps` are the rewrites each
+/// took, in words.
+pub fn explain(a: &Program, b: &Program) -> Value {
+    let ck = Checker::default();
+    let (na, sa) = simplify_ops(&a.ops, &ck);
+    let (nb, sb) = simplify_ops(&b.ops, &ck);
+    let shape = a.n_qubits == b.n_qubits && a.measured == b.measured;
+    let alike = shape && same_ops(&canonical(&na), &canonical(&nb));
+    let form = |ops: &[Op]| Program { n_qubits: a.n_qubits, ops: ops.to_vec(), measured: a.measured.clone(), n_bits: a.n_bits, dynamic: None };
+    let reordered = shape && !alike && prove(&form(&na), &form(&nb)).is_some();
+    let words = |s: &[Step]| s.iter().map(|x| json!({ "rule": x.rule.name(), "why": x.why })).collect::<Vec<_>>();
+    json!({ "ok": true, "found": alike || reordered, "reordered": reordered, "a_steps": words(&sa), "b_steps": words(&sb), "gates": [a.ops.len(), b.ops.len()], "form": na.len() })
+}
+
+/// A program's gates written out as OpenQASM 3 on one register `q`, its
+/// measurements into `c`.
+pub fn render(ops: &[Op], n_qubits: u32, measured: &[(u32, u32)], n_bits: u32) -> String {
+    let mut s = format!("OPENQASM 3.0;\nqubit[{n_qubits}] q;\n");
+    if n_bits > 0 {
+        s += &format!("bit[{n_bits}] c;\n");
+    }
+    for o in ops {
+        let params = if o.params.is_empty() { String::new() } else { format!("({})", o.params.iter().map(|x| format!("{x:?}")).collect::<Vec<_>>().join(", ")) };
+        let qs: Vec<String> = o.qubits.iter().map(|q| format!("q[{q}]")).collect();
+        s += &format!("{}{params} {};\n", critique::kind_name(o.kind), qs.join(", "));
+    }
+    for (q, b) in measured {
+        s += &format!("c[{b}] = measure q[{q}];\n");
+    }
+    s
+}
+
+/// One statement's parts: its indent, gate name, the text of its
+/// parameters, and its operands as written.
+struct Stmt<'a> {
+    indent: &'a str,
+    name: &'a str,
+    params: Option<&'a str>,
+    operands: &'a str,
+}
+
+fn stmt(line: &str) -> Option<Stmt<'_>> {
+    let indent = &line[..line.len() - line.trim_start().len()];
+    let code = line.split("//").next()?.trim();
+    let code = code.strip_suffix(';')?.trim_end();
+    let end = code.find(|c: char| c == '(' || c.is_whitespace())?;
+    let (name, rest) = code.split_at(end);
+    let (params, operands) = if let Some(r) = rest.strip_prefix('(') {
+        let mut depth = 1;
+        let close = r.char_indices().find(|&(_, c)| {
+            depth += match c {
+                '(' => 1,
+                ')' => -1,
+                _ => 0,
+            };
+            depth == 0
+        })?;
+        (Some(&r[..close.0]), r[close.0 + 1..].trim())
+    } else {
+        (None, rest.trim())
+    };
+    (!operands.is_empty() && !operands.contains(';')).then_some(Stmt { indent, name, params, operands })
+}
+
+/// The text of a phase gate's angle, from its statement.
+fn angle_text(o: &Op, s: &Stmt) -> Option<String> {
+    use Kind::*;
+    Some(match o.kind {
+        Z => "pi".into(),
+        S => "pi/2".into(),
+        Sdg => "-pi/2".into(),
+        T => "pi/4".into(),
+        Tdg => "-pi/4".into(),
+        P => s.params?.to_string(),
+        _ => return None,
+    })
+}
+
+fn plus(a: &str, b: &str) -> String {
+    match b.trim().strip_prefix('-') {
+        Some(rest) => format!("{a} - {rest}"),
+        None => format!("{a} + {b}"),
+    }
+}
+
+/// The edits to `src` that make `step`, each gate it takes alone on its
+/// line and written there by its own name; `None` when a gate shares its
+/// line, comes from a loop or a gate definition, or is not written by name.
+fn edits(src_lines: &[&str], ops: &[Op], lines: &[usize], step: &Step) -> Option<Vec<Edit>> {
+    let alone = |i: usize| lines.iter().filter(|&&l| l == lines[i]).count() == 1;
+    let st = |i: usize| -> Option<Stmt> {
+        let s = stmt(src_lines.get(lines[i].checked_sub(1)?)?)?;
+        (alone(i) && qasm::builtin(s.name).map(|(k, _)| k) == Some(ops[i].kind)).then_some(s)
+    };
+    let line = |i: usize| lines[i];
+    match step.rule {
+        Rule::Drop => Some(vec![Edit::Delete(line(step.take[0]))]),
+        Rule::Cancel | Rule::Merge | Rule::Through => {
+            let (i, j) = (step.take[0], step.take[1]);
+            let (si, sj) = (st(i)?, st(j)?);
+            let Some((_, m)) = step.put.first() else { return Some(vec![Edit::Delete(line(i)), Edit::Delete(line(j))]) };
+            let text = if ops[i].kind == ops[j].kind && ROTATIONS.contains(&ops[i].kind) && m.kind == ops[i].kind {
+                format!("{}{}({}) {};", sj.indent, sj.name, plus(si.params?, sj.params?), sj.operands)
+            } else if m.params.is_empty() {
+                format!("{}{} {};", sj.indent, critique::kind_name(m.kind), sj.operands)
+            } else {
+                format!("{}p({}) {};", sj.indent, plus(&angle_text(&ops[i], &si)?, &angle_text(&ops[j], &sj)?), sj.operands)
+            };
+            Some(vec![Edit::Delete(line(i)), Edit::Replace(line(j), text)])
+        }
+        Rule::Conjugate => {
+            let (i, j, k) = (step.take[0], step.take[1], step.take[2]);
+            let (_, _, sj) = (st(i)?, st(k)?, st(j)?);
+            let (_, c) = step.put.first()?;
+            let params = match (c.params.first(), sj.params) {
+                (None, _) => String::new(),
+                (Some(_), Some(p)) if c.params == ops[j].params => format!("({p})"),
+                (Some(_), Some(p)) if c.kind == Kind::Ry => format!("(-({p}))"),
+                (Some(&x), _) => format!("({x:?})"),
+            };
+            let operands = if c.qubits == ops[j].qubits { sj.operands.to_string() } else { sj.operands.split(',').map(str::trim).rev().collect::<Vec<_>>().join(", ") };
+            Some(vec![Edit::Delete(line(i)), Edit::Delete(line(k)), Edit::Replace(line(j), format!("{}{}{params} {operands};", sj.indent, critique::kind_name(c.kind)))])
+        }
+        Rule::Move => {
+            let (i, j) = (step.take[0], step.take[1]);
+            st(i)?;
+            st(j)?;
+            Some(vec![Edit::Replace(line(i), src_lines[line(j) - 1].to_string()), Edit::Replace(line(j), src_lines[line(i) - 1].to_string())])
+        }
+    }
+}
+
+/// Every rewrite `src` admits, each as an edit to its lines and checked:
+/// `{ok, options: [{id, rule, why, gates, lines, result}]}`. A generator's
+/// gates come from its loops, so it is rewritten as the circuit it writes
+/// out, and has none here.
+pub fn options(src: &str) -> Value {
+    if qasm::inputs(src).is_ok_and(|v| !v.is_empty()) {
+        return json!({ "ok": true, "options": [], "note": "a generator: its gates are written by its loops, so a rewrite applies to the circuit it writes out; write one out to rewrite it" });
+    }
+    let (p, lines) = match qasm::parse_lines(src) {
+        Ok(x) => x,
+        Err(e) => return json!({ "ok": false, "unread": e }),
+    };
+    if p.dynamic.is_some() {
+        return json!({ "ok": true, "options": [], "note": "this program measures in the middle or acts on what it measured; the rewrites keep a unitary, so they take programs whose measurements all come at the end" });
+    }
+    let ck = Checker::default();
+    let src_lines: Vec<&str> = src.split('\n').collect();
+    let mut out = Vec::new();
+    let mut ids = BTreeSet::new();
+    for i in 0..p.ops.len() {
+        for s in steps_at(&p.ops, i, &ck, true) {
+            let Some(e) = edits(&src_lines, &p.ops, &lines, &s) else { continue };
+            let result = critique::apply(src, &e);
+            // The text must say what the rewrite says, gate for gate.
+            let Ok(back) = qasm::parse(&result) else { continue };
+            if back.measured != p.measured || !same_ops(&canonical(&back.ops), &canonical(&apply(&p.ops, &s))) {
+                continue;
+            }
+            let ls: Vec<usize> = s.take.iter().map(|&k| lines[k]).collect();
+            let id = format!("{}:{}", s.rule.name(), ls.iter().map(|l| l.to_string()).collect::<Vec<_>>().join(","));
+            if ids.insert(id.clone()) {
+                out.push(json!({ "id": id, "rule": s.rule.name(), "why": s.why, "gates": s.take, "lines": ls, "result": result }));
+            }
+        }
+    }
+    json!({ "ok": true, "options": out })
+}
+
+fn inputs_of(args: &Value) -> Result<Inputs, String> {
+    match args.get("inputs") {
+        None | Some(Value::Null) => Ok(Inputs::new()),
+        Some(v) => serde_json::from_value(v.clone()).map_err(|e| format!("inputs: {e}")),
+    }
+}
+
+/// The rewrites as a page, an app or an agent calls them, with JSON
+/// arguments: `options` (`qasm`), `apply` (`qasm`, `id`: the program with
+/// that rewrite made), `simplify` (`qasm`, `inputs`: every rewrite to a
+/// fixed point, the steps in words and the result written out), `explain`
+/// (`a`, `b`, `inputs`) and `prove` (`a`, `b`, `inputs`).
+pub fn call(op: &str, args: &Value) -> Result<Value, String> {
+    let s = |k: &str| args.get(k).and_then(Value::as_str).ok_or_else(|| format!("{op}: give \"{k}\""));
+    let read = |k: &str| -> Result<Program, String> { qasm::parse_with(s(k)?, &inputs_of(args)?).map_err(|e| format!("{k} does not read: {e}")) };
+    match op {
+        "options" => Ok(options(s("qasm")?)),
+        "apply" => {
+            let id = s("id")?;
+            let all = options(s("qasm")?);
+            let found = all["options"].as_array().into_iter().flatten().find(|o| o["id"] == id).ok_or_else(|| format!("{id}: no such rewrite of this program"))?;
+            Ok(json!({ "result": found["result"], "why": found["why"] }))
+        }
+        "simplify" => {
+            let p = read("qasm")?;
+            let (rest, steps) = simplify(&p);
+            Ok(json!({ "steps": steps.iter().map(|x| json!({ "rule": x.rule.name(), "why": x.why })).collect::<Vec<_>>(), "gates": [p.ops.len(), rest.len()], "result": render(&rest, p.n_qubits, &p.measured, p.n_bits) }))
+        }
+        "explain" => Ok(explain(&read("a")?, &read("b")?)),
+        "prove" => Ok(prove(&read("a")?, &read("b")?).unwrap_or_else(|| json!({ "verdict": "unproved", "how": "rewrites", "why": "the first followed by the second's inverse does not rewrite to nothing; that concludes nothing" }))),
+        _ => Err(format!("{op}: no such call on the rewrites")),
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    fn ops(src: &str) -> Vec<Op> {
+        qasm::parse(src).unwrap().ops
+    }
+
+    #[test]
+    fn every_gate_s_inverse_undoes_it() {
+        let ck = Checker::default();
+        use Kind::*;
+        for kind in [Id, X, Y, Z, H, S, Sdg, T, Tdg, Sx, Sxdg, Rx, Ry, Rz, P, U, Cx, Cy, Cz, Ch, Cp, Crx, Cry, Crz, Cu, Swap, Iswap, Rxx, Ryy, Rzz, Ccx, Ccz, Cswap] {
+            let (np, nq) = kind.arity();
+            let op = Op { kind, qubits: (0..nq as u32).rev().collect(), params: (0..np).map(|k| 0.37 + 0.71 * k as f64).collect() };
+            let mut both = vec![op.clone()];
+            both.extend(inverse(&op));
+            assert!(ck.same(&both.iter().collect::<Vec<_>>(), &[]), "{kind:?}");
+        }
+    }
+
+    #[test]
+    fn a_rewrite_is_only_what_the_check_holds() {
+        let ck = Checker::default();
+        // cx one way then the other is no cancellation, though the qubits match.
+        let p = ops("OPENQASM 3.0;\nqubit[2] q;\ncx q[0], q[1];\ncx q[1], q[0];\n");
+        assert!(steps_at(&p, 0, &ck, false).is_empty());
+        let p = ops("OPENQASM 3.0;\nqubit[2] q;\nh q[0];\nx q[1];\nx q[1];\nrz(0.25) q[0];\nrz(0.5) q[0];\nt q[0];\nt q[0];\n");
+        let (rest, steps) = simplify_ops(&p, &ck);
+        let rules: Vec<&str> = steps.iter().map(|s| s.rule.name()).collect();
+        assert_eq!(rules, ["cancel", "merge", "merge"], "{steps:?}");
+        assert_eq!(rest.iter().map(op_text).collect::<Vec<_>>(), ["h q[0]", "rz(0.75) q[0]", "s q[0]"]);
+        assert_eq!(steps[2].why, "t q[0] and t q[0] merge into s q[0]");
+    }
+
+    #[test]
+    fn a_gate_is_carried_past_what_it_commutes_with_and_hadamards_conjugate() {
+        let ck = Checker::default();
+        let p = ops("OPENQASM 3.0;\nqubit[2] q;\nx q[1];\ncx q[0], q[1];\nx q[1];\n");
+        let s = &steps_at(&p, 0, &ck, false)[0];
+        assert_eq!((s.rule, s.why.as_str()), (Rule::Through, "x q[1], carried past cx q[0], q[1], which it commutes with, and x q[1] cancel"));
+        let p = ops("OPENQASM 3.0;\nqubit[2] q;\nh q[1];\ncx q[0], q[1];\nh q[1];\n");
+        let s = &steps_at(&p, 0, &ck, false)[0];
+        assert_eq!((s.rule, s.why.as_str()), (Rule::Conjugate, "cx q[0], q[1] between two h q[1] is cz q[0], q[1]"));
+        let p = ops("OPENQASM 3.0;\nqubit[1] q;\nh q[0];\nrz(0.3) q[0];\nh q[0];\n");
+        assert_eq!(op_text(&apply(&p, &steps_at(&p, 0, &ck, false)[0])[0]), "rx(0.3) q[0]");
+        // A control between two gates on the target, which it does not commute with, stops the carry.
+        let p = ops("OPENQASM 3.0;\nqubit[2] q;\nz q[1];\ncx q[0], q[1];\nz q[1];\n");
+        assert!(steps_at(&p, 0, &ck, false).iter().all(|s| s.rule != Rule::Through), "z on the target does not pass cx");
+    }
+
+    /// Wide and not Clifford: rewriting proves what only random inputs could
+    /// support before, and the equivalence check now says so.
+    #[test]
+    fn equivalence_is_proved_by_rewriting_at_any_width() {
+        let n = 12;
+        let mut a = format!("OPENQASM 3.0;\nqubit[{n}] q;\n");
+        let mut b = a.clone();
+        for i in 0..n - 1 {
+            a += &format!("t q[{i}];\nrz(0.2) q[{i}];\ncx q[{i}], q[{}];\nrz(0.3) q[{i}];\nx q[{}];\nx q[{}];\n", i + 1, i + 1, i + 1);
+            b += &format!("t q[{i}];\ncx q[{i}], q[{}];\nrz(0.5) q[{i}];\n", i + 1);
+        }
+        let (pa, pb) = (qasm::parse(&a).unwrap(), qasm::parse(&b).unwrap());
+        let v = prove(&pa, &pb).expect("it reduces");
+        assert_eq!(v["how"], "rewrites", "{v}");
+        assert_eq!(equiv::equivalent_programs(&pa, &pb)["how"], "rewrites");
+        // A different circuit does not reduce, and the check falls to its next method.
+        let c = b.replace("rz(0.5) q[3];", "rz(0.6) q[3];");
+        let pc = qasm::parse(&c).unwrap();
+        assert!(prove(&pa, &pc).is_none());
+        assert_eq!(equiv::equivalent_programs(&pa, &pc)["verdict"], "different");
+    }
+
+    #[test]
+    fn the_lens_offers_each_rewrite_as_an_edit_to_its_lines() {
+        let src = "OPENQASM 3.0;\nqubit[2] q;\nh q[0];   // into superposition\nx q[1];\nx q[1];\nrz(0.25) q[0];\nrz(-pi/8) q[0];\ncx q[0], q[1];\n";
+        let v = options(src);
+        let by: HashMap<&str, &Value> = v["options"].as_array().unwrap().iter().map(|o| (o["id"].as_str().unwrap(), o)).collect();
+        assert!(by.contains_key("cancel:4,5") && by.contains_key("merge:6,7"), "{v}");
+        let merged = by["merge:6,7"]["result"].as_str().unwrap();
+        assert!(merged.contains("rz(0.25 - pi/8) q[0];") && merged.contains("// into superposition"), "{merged}");
+        let back = qasm::parse(merged).unwrap();
+        assert_eq!(equiv::equivalent_programs(&qasm::parse(src).unwrap(), &back)["verdict"], "equivalent");
+        assert!(by.keys().any(|k| k.starts_with("move:")), "two gates that commute may trade places: {v}");
+        let r = call("apply", &json!({ "qasm": src, "id": "cancel:4,5" })).unwrap();
+        assert!(!r["result"].as_str().unwrap().contains("x q[1]"), "{r}");
+        assert!(call("apply", &json!({ "qasm": src, "id": "cancel:9,9" })).unwrap_err().contains("no such rewrite"));
+        let g = options("OPENQASM 3.0;\ninput uint n;\nqubit[n] q;\nh q[0];\n");
+        assert!(g["note"].as_str().unwrap().contains("generator"), "{g}");
+    }
+
+    #[test]
+    fn an_optimisation_is_explained_as_a_chain() {
+        let a = qasm::parse("OPENQASM 3.0;\nqubit[2] q;\nh q[1];\ncx q[0], q[1];\nh q[1];\nt q[0];\nt q[0];\n").unwrap();
+        let b = qasm::parse("OPENQASM 3.0;\nqubit[2] q;\ns q[0];\ncz q[0], q[1];\n").unwrap();
+        let e = explain(&a, &b);
+        assert_eq!((e["found"].as_bool(), e["reordered"].as_bool()), (Some(true), Some(true)), "s and cz commute: the forms differ only in their order: {e}");
+        let whys: Vec<&str> = e["a_steps"].as_array().unwrap().iter().map(|s| s["why"].as_str().unwrap()).collect();
+        assert_eq!(whys, ["cx q[0], q[1] between two h q[1] is cz q[0], q[1]", "t q[0] and t q[0] merge into s q[0]"], "{e}");
+        let other = qasm::parse("OPENQASM 3.0;\nqubit[2] q;\nz q[0];\ncz q[0], q[1];\n").unwrap();
+        assert_eq!(explain(&a, &other)["found"], false);
+        let s = call("simplify", &json!({ "qasm": "OPENQASM 3.0;\nqubit[1] q;\nbit[1] c;\nh q[0];\nh q[0];\nx q[0];\nc[0] = measure q[0];\n" })).unwrap();
+        assert_eq!(s["gates"], json!([3, 1]), "{s}");
+        assert!(s["result"].as_str().unwrap().contains("c[0] = measure q[0];"), "{s}");
+        assert_eq!(angle(-PI / 2.0), "-π/2");
+        assert_eq!(angle(0.75 * PI), "3π/4");
+    }
+}

wai/wai-quantum/src/engine/taste.rs

@@ -75,7 +75,7 @@ const LEANING: f64 = 0.3;
 /// The most choices the profile's measures are taken over (the last ones).
 const MEASURED: usize = 100;
 /// The verdicts a choice accepts: proofs, not evidence on random inputs.
-const PROOFS: &[&str] = &["tableau", "exact", "state"];
+const PROOFS: &[&str] = &["tableau", "exact", "state", "rewrites"];
 
 /// One side of a choice: the program, its digest and its features.
 #[derive(Clone, Debug, Deserialize, Serialize, PartialEq)]
@@ -96,7 +96,7 @@ pub struct Choice {
     /// `equivalent` (the same circuit) or `prepares` (the same state from
     /// `|0…0⟩`).
     pub task: String,
-    /// The check that proved it: `tableau`, `exact` or `state`.
+    /// The check that proved it: `tableau`, `exact`, `rewrites` or `state`.
     pub how: String,
     #[serde(default, skip_serializing_if = "BTreeMap::is_empty")]
     pub inputs: Inputs,

wai/wai-quantum/src/qasm.rs

@@ -117,7 +117,7 @@ impl Kind {
 }
 
 /// A builtin gate name: its kind, and any parameters it fixes or reorders.
-fn builtin(name: &str) -> Option<(Kind, usize)> {
+pub(crate) fn builtin(name: &str) -> Option<(Kind, usize)> {
     use Kind::*;
     // (kind, the number of parameters the name takes)
     Some(match name {

wai/wai-rs/Cargo.lock

@@ -4541,7 +4541,7 @@ dependencies = [
 
 [[package]]
 name = "wai-quantum"
-version = "0.6.15"
+version = "0.6.16"
 dependencies = [
  "blake3",
  "ed25519-dalek",

wai/wai-web/Cargo.lock

@@ -1241,7 +1241,7 @@ version = "0.1.0"
 
 [[package]]
 name = "wai-quantum"
-version = "0.6.15"
+version = "0.6.16"
 dependencies = [
  "blake3",
  "ed25519-dalek",

wai/wai-web/src/quantum_engine.rs

@@ -8,7 +8,7 @@
 use ed25519_dalek::SigningKey;
 use serde_json::{Value, json};
 use wai::engine::discover::{self, Archive, Budget, Evaluator, SearchOptions, Spec, search};
-use wai::engine::{catalog, critique, draw, equiv, job, locks, novelty, shortcuts, taste, versions};
+use wai::engine::{catalog, converge, critique, draw, equiv, job, locks, novelty, rewrite, shortcuts, taste, versions};
 use wasm_bindgen::prelude::*;
 
 /// What a result run in a tab says of its energy.
@@ -289,6 +289,28 @@ pub fn engine_discover_novelty(spec: &str, archive_json: &str, id: &str) -> Stri
         .unwrap_or_else(error_json)
 }
 
+/// `op` on the convergence monitor ([`converge::call`]): `history` (the
+/// page's history of the program) or `cohort`: the answer, or `{error}`.
+#[wasm_bindgen]
+pub fn engine_converge(op: &str, args: &str) -> String {
+    serde_json::from_str::<Value>(args)
+        .map_err(|e| format!("{op}: the arguments are not JSON: {e}"))
+        .and_then(|a| converge::call(op, &a))
+        .map(|v| v.to_string())
+        .unwrap_or_else(error_json)
+}
+
+/// `op` on the rewrites ([`rewrite::call`]): `options`, `apply`, `simplify`,
+/// `explain` or `prove`, its arguments as JSON: the answer, or `{error}`.
+#[wasm_bindgen]
+pub fn engine_rewrite(op: &str, args: &str) -> String {
+    serde_json::from_str::<Value>(args)
+        .map_err(|e| format!("{op}: the arguments are not JSON: {e}"))
+        .and_then(|a| rewrite::call(op, &a))
+        .map(|v| v.to_string())
+        .unwrap_or_else(error_json)
+}
+
 /// `op` on the person's taste model ([`taste::call`]), the profile kept by
 /// the page and passed in the arguments as JSON: the answer, or `{error}`.
 #[wasm_bindgen]
@@ -394,6 +416,32 @@ mod tests {
         assert!(engine_discover_novelty(&spec, &sub["archive"].to_string(), "e99").contains("no such entry"));
     }
 
+    /// The convergence monitor in the page, on a history the page keeps.
+    #[test]
+    fn convergence_is_measured_in_the_page() {
+        let e = QuantumEngine::new(&[9; 32], 64).unwrap();
+        let start = "OPENQASM 3.0;\nqubit[2] q;\n";
+        let model = "OPENQASM 3.0;\nqubit[2] q;\nh q[0];\ncx q[0], q[1];\n";
+        let r: Value = serde_json::from_str(&e.history("start", &json!({ "source": start, "by": { "kind": "person" }, "at": 1 }).to_string())).unwrap();
+        let r: Value = serde_json::from_str(&e.history("propose", &json!({ "history": r["history"], "parent": "v0", "proposed": model, "accepted": [0], "by": { "kind": "assistant", "name": "m" }, "at": 2 }).to_string())).unwrap();
+        let r: Value = serde_json::from_str(&e.history("commit", &json!({ "history": r["history"], "parent": "v1", "source": format!("{model}x q[1];\n"), "by": { "kind": "person" }, "at": 3 }).to_string())).unwrap();
+        let c: Value = serde_json::from_str(&engine_converge("history", &json!({ "history": r["history"] }).to_string())).unwrap();
+        assert_eq!((c["converging"].as_bool(), c["series"].as_array().map(Vec::len)), (Some(true), Some(1)), "{c}");
+        assert!(engine_converge("cohort", "{}").contains("programs"));
+    }
+
+    /// The rewrites in the page: each one the program admits as an edit to
+    /// its lines, and an optimisation explained as a chain.
+    #[test]
+    fn rewrites_are_offered_and_explained_in_the_page() {
+        let src = "OPENQASM 3.0;\nqubit[2] q;\nx q[1];\ncx q[0], q[1];\nx q[1];\n";
+        let o: Value = serde_json::from_str(&engine_rewrite("options", &json!({ "qasm": src }).to_string())).unwrap();
+        assert!(o["options"].as_array().unwrap().iter().any(|x| x["rule"] == "through" && x["id"] == "through:3,5"), "{o}");
+        let e: Value = serde_json::from_str(&engine_rewrite("explain", &json!({ "a": src, "b": "OPENQASM 3.0;\nqubit[2] q;\ncx q[0], q[1];\n" }).to_string())).unwrap();
+        assert_eq!(e["found"], true, "{e}");
+        assert!(engine_rewrite("nonsense", "{}").contains("no such call"));
+    }
+
     /// The taste model in the page: a choice between programs the engine
     /// proves equal is kept in the profile the page holds, and ranks.
     #[test]
@@ -518,7 +566,11 @@ mod wasm_tests {
     fn critique_equivalence_and_variants_run_in_wasm() {
         let c: Value = serde_json::from_str(&engine_critique("qubit[2] q; h q[0]; rz(0.3) q[1]; cx q[0], q[1];")).unwrap();
         assert_eq!((c["depth"].as_u64(), c["non_clifford"].as_u64()), (Some(2), Some(1)), "{c}");
+        // Wide and not Clifford: proved by rewriting, the merge checked on its one qubit.
         let e: Value = serde_json::from_str(&engine_equivalent("qubit[12] q; h q; rx(0.25) q[3]; rx(0.5) q[3];", "qubit[12] q; h q; rx(0.75) q[3];")).unwrap();
+        assert_eq!((e["verdict"].as_str(), e["how"].as_str()), (Some("equivalent"), Some("rewrites")), "{e}");
+        // A swap written as three cx is no pair that cancels or merges: random inputs decide it.
+        let e: Value = serde_json::from_str(&engine_equivalent("qubit[12] q; h q; swap q[3], q[9]; rz(1.1) q[11];", "qubit[12] q; h q; cx q[3], q[9]; cx q[9], q[3]; cx q[3], q[9]; rz(1.1) q[11];")).unwrap();
         assert_eq!((e["verdict"].as_str(), e["how"].as_str()), (Some("equivalent"), Some("random")), "{e}");
         let v: Value = serde_json::from_str(&engine_variants("qubit[1] q;\nrz(0.5) q[0];\nrz(-0.5) q[0];\nh q[0];\n")).unwrap();
         assert_eq!(v["candidates"][0]["qasm"], "qubit[1] q;\nh q[0];\n", "{v}");