wai-quantum: rewrites, convergence, and the 0.6.16 / 0.1.4 release #498

Merged

dcharlot merged 4 commits from wai/quantum-converge into main 2026-10-26 18:00:43 -04:00

Conversation 0 Commits 4 Files changed 48 +1907 -49

dcharlot commented 2026-10-26 16:11:36 -04:00

Owner

Copy link

Features 11 and 12 of the co-design report, and the release that carries everything since 0.6.15 to the package registry, as three commits. The verified-rewrite lens comes with the general equivalence check it needs first; then the convergence monitor; then wai-quantum 0.6.16 and wai-quantum-cli 0.1.4. Stacked on #497: once it merges, this PR is these three commits alone.

Once this merges, the following go out together, from the merge:

• the CLI release tag;
• the crates;
• the taps;
• the job service;
• the site's Studio.

Rewrites, each checked, and equivalence proved by them at any width (c979c300f)

• engine::rewrite. The rules propose and the engine decides. The rules:

  • cancel: a gate and its inverse;
  • merge: rotations about one axis; phase gates add up;
  • conjugate: a gate between two Hadamards, as in h cx h → cz;
  • drop: a gate that does nothing;
  • through: a gate carried past gates it commutes with, to its partner;
  • move: two gates that commute trade places.

  Each rewrite is checked on just the qubits it touches, by tableau or on every basis state (equiv::proved_equal). So a chain of them proves two programs equal at any width and with any gates.

• Equivalence by rewriting. rewrite::prove reduces the first program followed by the other's inverse to nothing. equiv::equivalent_programs now tries this after the exact check and before random inputs, answering how: rewrites. The workbench and the taste model count that as a proof.

• Explanations. rewrite::explain gives a readable chain: both programs simplified to a fixed point, then compared gate for gate, or up to the order of gates that commute, by a proof.

• Options. rewrite::options gives each rewrite as an edit to the program's own lines (a merge writes rz(0.25 + 0.5), comments stay). Each is read back and compared gate for gate before it is offered.

• CLI and MCP: wai-quantum rewrite options | apply | simplify | explain; the rewrite_qasm tool. The check_equivalent descriptions now name the new proof, in the service's MCP too.

• Studio:

  • "Rewrites" under the circuit: each rewrite in words, its gates marked on the diagram, and "Take" to offer it as the engine's proposal. The list follows the program as it changes.
  • Alternatives: a candidate that is the same circuit as the draft says how the draft becomes it, as a chain.

• Tests. The old wide-equivalence test now proves its pair by rewrites. The random-inputs path is kept on a swap written as three cx.

Whether designs converge on a model's, and a while on one's own (94fabb574)

• Along a program's history (engine::converge::history), each version the person made after a model proposed gets:

  • its structural distance from the proposals in its line of work;
  • the model's share of its gates.

  The history is converging when most of the program is the model's, or when the last versions come closer each time, and it says which. Versions noted organic exploration are the assistant-off probes, set beside the rest.

• A cohort (converge::cohort) gets:

  • the Vendi score, the effective number of distinct designs (Jacobi eigenvalues of 1 − distance);
  • each program's distance to the centroid, the medoid and the outlier;
  • with times, the score in windows, and whether it narrows.

• CLI and MCP: wai-quantum converge history | cohort; the converge_cohort and converge_history tools.

• 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;
  • Alternatives' Explore and the Workbench's "Ask the model" wait;
  • the person's versions are noted as made on their own.

  "End" lets the model propose again.

• CI: wai-web's native engine test count goes from 11 to 13.

wai-quantum 0.6.16 and wai-quantum-cli 0.1.4 (7309053e4)

• What it carries: the five entries since 0.6.15 (the person's rules, what is new, taste, rewrites, convergence), and 0.6.15's own. 0.6.15 and 0.1.3 reached the binaries and the taps, but not the registry.
• Requirements: the CLI and the desktop app require 0.6.16.
• Lockfiles: all 12 that hold wai-quantum or wai-quantum-cli move with them. Each was checked with cargo metadata --locked, and cargo package packs wai-quantum.

Checked on the build host (run at low priority, so the macOS runner's timing tests were not starved):

• engine engine:: 115 pass;
• CLI 17 pass, clippy clean with default and no default features;
• service 18 pass;
• wai-web native engine tests: 13 pass;
• desktop: 5 pass, clippy clean;
• Studio e2e: 132 checks pass;
• the public-names check is clean.

🤖 Generated with Claude Code

Features 11 and 12 of the co-design report, and the release that carries everything since 0.6.15 to the package registry, as three commits. The verified-rewrite lens comes with the general equivalence check it needs first; then the convergence monitor; then wai-quantum 0.6.16 and wai-quantum-cli 0.1.4. Stacked on #497: once it merges, this PR is these three commits alone. Once this merges, the following go out together, from the merge: - the CLI release tag; - the crates; - the taps; - the job service; - the site's Studio. ## Rewrites, each checked, and equivalence proved by them at any width (`c979c300f`) - **`engine::rewrite`.** The rules propose and the engine decides. The rules: - **cancel:** a gate and its inverse; - **merge:** rotations about one axis; phase gates add up; - **conjugate:** a gate between two Hadamards, as in `h cx h` → `cz`; - **drop:** a gate that does nothing; - **through:** a gate carried past gates it commutes with, to its partner; - **move:** two gates that commute trade places. Each rewrite is checked on just the qubits it touches, by tableau or on every basis state (`equiv::proved_equal`). So a chain of them proves two programs equal at any width and with any gates. - **Equivalence by rewriting.** `rewrite::prove` reduces the first program followed by the other's inverse to nothing. `equiv::equivalent_programs` now tries this after the exact check and before random inputs, answering `how: rewrites`. The workbench and the taste model count that as a proof. - **Explanations.** `rewrite::explain` gives a readable chain: both programs simplified to a fixed point, then compared gate for gate, or up to the order of gates that commute, by a proof. - **Options.** `rewrite::options` gives each rewrite as an edit to the program's own lines (a merge writes `rz(0.25 + 0.5)`, comments stay). Each is read back and compared gate for gate before it is offered. - **CLI and MCP:** `wai-quantum rewrite options | apply | simplify | explain`; the `rewrite_qasm` tool. The `check_equivalent` descriptions now name the new proof, in the service's MCP too. - **Studio:** - **"Rewrites" under the circuit:** each rewrite in words, its gates marked on the diagram, and "Take" to offer it as the engine's proposal. The list follows the program as it changes. - **Alternatives:** a candidate that is the same circuit as the draft says how the draft becomes it, as a chain. - **Tests.** The old wide-equivalence test now proves its pair by `rewrites`. The random-inputs path is kept on a swap written as three `cx`. ## Whether designs converge on a model's, and a while on one's own (`94fabb574`) - **Along a program's history** (`engine::converge::history`), each version the person made after a model proposed gets: - its structural distance from the proposals in its line of work; - the model's share of its gates. The history is converging when most of the program is the model's, or when the last versions come closer each time, and it says which. Versions noted `organic exploration` are the assistant-off probes, set beside the rest. - **A cohort** (`converge::cohort`) gets: - the Vendi score, the effective number of distinct designs (Jacobi eigenvalues of `1 − distance`); - each program's distance to the centroid, the medoid and the outlier; - with times, the score in windows, and whether it narrows. - **CLI and MCP:** `wai-quantum converge history | cohort`; the `converge_cohort` and `converge_history` tools. - **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; - Alternatives' Explore and the Workbench's "Ask the model" wait; - the person's versions are noted as made on their own. "End" lets the model propose again. - **CI:** wai-web's native engine test count goes from 11 to 13. ## wai-quantum 0.6.16 and wai-quantum-cli 0.1.4 (`7309053e4`) - **What it carries:** the five entries since 0.6.15 (the person's rules, what is new, taste, rewrites, convergence), and 0.6.15's own. 0.6.15 and 0.1.3 reached the binaries and the taps, but not the registry. - **Requirements:** the CLI and the desktop app require 0.6.16. - **Lockfiles:** all 12 that hold wai-quantum or wai-quantum-cli move with them. Each was checked with `cargo metadata --locked`, and `cargo package` packs wai-quantum. **Checked on the build host** (run at low priority, so the macOS runner's timing tests were not starved): - engine `engine::` 115 pass; - CLI 17 pass, clippy clean with default and no default features; - service 18 pass; - wai-web native engine tests: 13 pass; - desktop: 5 pass, clippy clean; - Studio e2e: 132 checks pass; - the public-names check is clean. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 4 commits 2026-10-26 16:11:36 -04:00

wai-quantum: a person's taste, learned from their own choices between equals ... dcb5391f90

Feature 10 of the co-design report: a personal, plural taste model.

- engine::taste:
  - a choice is recorded only when the engine proves the two programs the
    same circuit or the same state, by a proof (tableau, exact, state),
    never by random inputs: it is about taste, never correctness;
  - a Bradley-Terry logistic over differences of measured features (gates,
    two-qubit gates, depth, two-qubit depth, T gates, modelled error) and
    of the text (statements, kinds of gate, repetition, comments), ridge
    penalised and fitted by Newton's method: deterministic everywhere;
  - the rubric's parts (economy, clarity, insight, precision, utility),
    each learned from its own choices; a ranking names where a part or the
    cost puts another first;
  - profiles personal and plural, by name, never pooled;
  - typicality (one less engine::novelty's novelty) shown and never
    learned; the novelty dial blends the standardised order by taste with
    the order by novelty; a floor on each feature's spread keeps a feature
    that barely varied from turning into certainty;
  - measured: choices predicted as made and held out (last 100), the ones
    nothing measured separates, and whether a ranking's first three are
    built more alike than the cost's; scores about the candidates' mean;
  - next: the least certain pair the engine proves equal; call for hosts.
- novelty::token is shared with it.
- The command line: taste choose | show | rank | next (files or --spec),
  profiles in quantum-taste.json beside the user's key.
- MCP: taste_rank and taste_next read the person's profile; no tool
  records a choice. initialize tells an agent so, and to call a program
  new only when novelty_qasm says so.
- The Studio: "Your taste" in the Workbench (Compare two with the part a
  choice was about, Rank by my taste with typicality and the dial,
  profiles by name); an alternative that is the same circuit as the draft,
  taken whole or refused whole, is a choice; Improve orders by the profile.
- Bindings: engine_taste in the page, taste in the desktop app.
- CI: wai-web's native engine tests count 11.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-quantum: rewrites, each checked, and equivalence proved by them at any width ... c979c300ff

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.

- engine::rewrite:
  - rules propose, the engine decides: cancel (a gate and its inverse),
    merge (rotations about one axis; phase gates add up), conjugate (a
    gate between two Hadamards), drop (a gate that does nothing), through
    (carried past gates it commutes with to its partner), move (two that
    commute trade places);
  - 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 a chain is a proof at any width;
  - prove: one program followed by the other's inverse rewritten to
    nothing; explain: both simplified and compared (gate for gate, or up
    to the order of gates that commute, by a proof); options: each rewrite
    as an edit to the program's own lines, read back and compared before it
    is offered; call for hosts.
- equiv::equivalent_programs tries the proof after the exact check and
  before random inputs (how: rewrites); the workbench and the taste model
  count it as a proof. critique's line edits and qasm::builtin are shared.
- The command line: rewrite options | apply | simplify | explain.
- MCP: rewrite_qasm; check_equivalent's description names the new proof
  (and the service's).
- The Studio: "Rewrites" under the circuit (each 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; "by checked rewrites".
- Bindings: engine_rewrite in the page, rewrite in the desktop app.
- CI: wai-web's native engine tests count 12.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-quantum: whether designs converge on a model's, and a while on one's own ... 94fabb574d

Feature 12 of the co-design report: a convergence monitor.

- engine::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) and the model's share of its gates; converging when
    most of the program is the model's or the last versions come closer
    each time, with why; versions noted "organic exploration" (the
    assistant-off probes) set beside the rest;
  - cohort: the Vendi score over 1 - distance (Jacobi eigenvalues), each
    program's distance to the centroid of the gate-token bags, the medoid
    and the outlier, and with times the score in windows and a narrowing;
  - call for hosts. novelty::bag is shared.
- The command line: converge history | cohort (a file's time from its
  history, else the file's).
- MCP: converge_cohort and converge_history.
- The Studio: "Your own way" under Versions, and "Explore on my own for a
  while": the assistant only asks and offers no program, Explore and Ask
  the model wait, the person's versions are noted; End lets the model
  propose again.
- Bindings: engine_converge in the page, converge in the desktop app.
- CI: wai-web's native engine tests count 13.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-quantum 0.6.16 and wai-quantum-cli 0.1.4: the person's rules, what is new, taste, rewrites and convergence ... 7309053e46

This carries the person's rules for proposals, what is new in a program,
a person's taste, checked rewrites with equivalence proved by them, and the
convergence monitor to the package registry, with 0.6.15's entry, which
reached the binaries and the taps but not the registry.

- wai-quantum 0.6.16: engine::locks, engine::novelty, engine::taste,
  engine::rewrite (equiv answers how: rewrites) and engine::converge.
- wai-quantum-cli 0.1.4 requires it: locks, novelty, discover novelty,
  taste, rewrite and converge, and their MCP tools.
- 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.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

dcharlot added 1 commit 2026-10-26 17:06:23 -04:00

wai-web: the wasm test of a wide equivalence expects the rewrite proof ... defc8c6f8d

Equivalence now proves a wide pair whose rotations merge by rewriting
(how: rewrites), as the native test in engine::equiv already expects. The
random check is kept, on a swap written as three cx, which no pair of
gates rewrites.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

dcharlot merged commit f1a34c0687 into main 2026-10-26 18:00:43 -04:00

dcharlot referenced this pull request from a commit 2026-10-26 18:00:43 -04:00

Merge pull request 'wai-quantum: rewrites, convergence, and the 0.6.16 / 0.1.4 release' (#498) from wai/quantum-converge into main

dcharlot referenced this pull request 2026-10-26 19:26:45 -04:00

wai merge train E: twenty-five PRs onto main, the relay's upstream window bounded, and three fixes the merged tree needed #499

dcharlot referenced this pull request from a commit 2026-10-26 19:26:45 -04:00

Merge origin/main (f1a34c068): #498, wai-quantum 0.6.16 and wai-quantum-cli 0.1.4

dcharlot referenced this pull request from a commit 2026-10-26 19:26:45 -04:00

wai-audit, wai-key-proxy, wai-ledger: their locks on wai-quantum 0.6.16, as #498 moved it (#474, #471, #473)

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

Transaction-Science/open-standards!498

No description provided.