diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml new file mode 100644 index 000000000..92ba2c945 --- /dev/null +++ b/.github/workflows/pages.yml @@ -0,0 +1,82 @@ +# Deploys the site in site/ to GitHub Pages: the landing page plus the +# playground, which runs AutoQ compiled to WebAssembly (wasm/build.sh). +# +# One-time setup before the first run: in the repository settings, open +# Settings -> Pages -> Build and deployment and set Source to "GitHub Actions". +# Without that, the Configure Pages step fails. (Passing `enablement: true` to +# actions/configure-pages would enable Pages automatically, but it needs a +# token with admin rights; the default GITHUB_TOKEN does not have them.) +# +# After the first deploy, compare the page_url printed by the deploy step with +# the canonical and og: URLs in site/index.html (https://fmlab-iis.github.io/AutoQ/). +# +# The first run builds Z3 and the ANTLR runtime for WebAssembly, which takes +# a while; later runs restore them from the cache. +name: Deploy landing page + +on: + push: + branches: [main] + paths: + - "site/**" + - "wasm/**" + - "src/**" + - "include/**" + - "cli/**" + - "CMakeLists.txt" + - ".github/workflows/pages.yml" + workflow_dispatch: + +permissions: + contents: read + pages: write + id-token: write + +concurrency: + group: "pages" + cancel-in-progress: false + +env: + EMSDK_VERSION: "6.0.12" + +jobs: + deploy: + environment: + name: github-pages + url: ${{ steps.deployment.outputs.page_url }} + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 # autoq -v reports the commit from git describe + + - name: Install Boost headers + run: sudo apt-get update && sudo apt-get install -y libboost-dev + + - name: Install Emscripten + run: | + git clone --depth 1 https://github.com/emscripten-core/emsdk.git "$RUNNER_TEMP/emsdk" + "$RUNNER_TEMP/emsdk/emsdk" install "$EMSDK_VERSION" + "$RUNNER_TEMP/emsdk/emsdk" activate "$EMSDK_VERSION" + + - name: Cache Z3 and ANTLR for WebAssembly + uses: actions/cache@v4 + with: + path: build-wasm/deps + key: wasm-deps-${{ env.EMSDK_VERSION }}-${{ hashFiles('wasm/build.sh') }} + + - name: Build the playground (AutoQ to WebAssembly) + run: | + source "$RUNNER_TEMP/emsdk/emsdk_env.sh" + wasm/build.sh site/playground + + - name: Configure Pages + uses: actions/configure-pages@v5 + - name: Upload site + uses: actions/upload-pages-artifact@v3 + with: + path: site + - name: Deploy to GitHub Pages + id: deployment + uses: actions/deploy-pages@v4 diff --git a/.gitignore b/.gitignore index ec540a9cd..f1fe076e9 100644 --- a/.gitignore +++ b/.gitignore @@ -28,4 +28,8 @@ POPL24/TABLES/Algorithms/*.pdf POPL24/TABLES/Algorithms/*.tex POPL24/TABLES/Algorithms/*.log POPL24/TABLES/Algorithms/*.aux -benchmark*/_others/** \ No newline at end of file +benchmark*/_others/** +# WebAssembly build (wasm/build.sh); the playground binaries are built in CI +build-wasm/ +site/playground/autoq.js +site/playground/autoq.wasm diff --git a/CMakeLists.txt b/CMakeLists.txt index 3da6d74c4..e8c827082 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -158,17 +158,26 @@ include(CTest) # DEPENDENCIES ############################################################################## -# Boost -set(Boost_USE_MULTITHREADED OFF) -find_package(Boost 1.71.0...1.89.0 CONFIG COMPONENTS # 1.89.0 is for macOS on GitHub CI - filesystem -# system - unit_test_framework - REQUIRED) -# IMPORTANT CHANGE: https://github.com/facebook/folly/issues/2489 -# Boost.System has been header-only since 1.69. -# If someone increases minimum Boost to 1.71 then can just remove the system component. -include_directories(${Boost_INCLUDE_DIRS}) +if (EMSCRIPTEN) + # WebAssembly build (wasm/build.sh). Only header-only parts of Boost are + # used, and Z3 and the ANTLR runtime are prebuilt static libraries. + set(AUTOQ_WASM_BOOST_INCLUDE "" CACHE PATH "Directory containing the boost/ headers") + set(AUTOQ_WASM_Z3_LIB "" CACHE FILEPATH "Z3 static library built with Emscripten") + set(AUTOQ_WASM_ANTLR4_LIB "" CACHE FILEPATH "ANTLR4 C++ runtime static library built with Emscripten") + include_directories(${AUTOQ_WASM_BOOST_INCLUDE}) +else() + # Boost + set(Boost_USE_MULTITHREADED OFF) + find_package(Boost 1.71.0...1.89.0 CONFIG COMPONENTS # 1.89.0 is for macOS on GitHub CI + filesystem + # system + unit_test_framework + REQUIRED) + # IMPORTANT CHANGE: https://github.com/facebook/folly/issues/2489 + # Boost.System has been header-only since 1.69. + # If someone increases minimum Boost to 1.71 then can just remove the system component. + include_directories(${Boost_INCLUDE_DIRS}) +endif() include_directories(../include/z3) # Doxygen - voluntary @@ -189,6 +198,8 @@ endif() # Process subdirectories add_subdirectory(src) add_subdirectory(cli) -add_subdirectory(unit_tests) +if (NOT EMSCRIPTEN) + add_subdirectory(unit_tests) +endif() # add_subdirectory(parametric) # add_subdirectory(tests) diff --git a/cli/CMakeLists.txt b/cli/CMakeLists.txt index 5710e727e..cf2aef233 100644 --- a/cli/CMakeLists.txt +++ b/cli/CMakeLists.txt @@ -34,3 +34,23 @@ endforeach() if (MAKE_STATIC_AUTOQ) SET(CMAKE_CXX_LINK_EXECUTABLE "${CMAKE_CXX_LINK_EXECUTABLE} -static") endif() + +if (EMSCRIPTEN) + # WebAssembly build (wasm/build.sh): an ES module exporting createAutoQ(). + # The playground (site/playground) writes the input files into the + # in-memory filesystem and runs main() through callMain() on a fresh + # instance per run. + target_link_options(autoq PRIVATE + -fwasm-exceptions + -sMODULARIZE=1 + -sEXPORT_ES6=1 + -sEXPORT_NAME=createAutoQ + -sENVIRONMENT=web,worker,node + -sINVOKE_RUN=0 + -sEXIT_RUNTIME=1 + -sALLOW_MEMORY_GROWTH=1 + -sMAXIMUM_MEMORY=4GB + -sSTACK_SIZE=8MB + -sFORCE_FILESYSTEM=1 + -sEXPORTED_RUNTIME_METHODS=callMain,FS) +endif() diff --git a/cli/autoq.cc b/cli/autoq.cc index bbcb557eb..77684e1ec 100644 --- a/cli/autoq.cc +++ b/cli/autoq.cc @@ -234,7 +234,9 @@ static void run_verification(const std::string& pre, const std::string& post, co int main(int argc, char **argv) { try { // set_timeout(600); +#ifndef __EMSCRIPTEN__ // WebAssembly has no floating-point exception traps feenableexcept(FE_ALL_EXCEPT & ~FE_INEXACT); +#endif CLI::App app{"AutoQ 2.0: An automata-based C++ tool for quantum program verification."}; std::string pre, circuit, post, circuit1, circuit2; diff --git a/site/.nojekyll b/site/.nojekyll new file mode 100644 index 000000000..e69de29bb diff --git a/site/assets/apple-touch-icon.png b/site/assets/apple-touch-icon.png new file mode 100644 index 000000000..3d3ac8b3f Binary files /dev/null and b/site/assets/apple-touch-icon.png differ diff --git a/site/assets/favicon-32.png b/site/assets/favicon-32.png new file mode 100644 index 000000000..f8eadf9e8 Binary files /dev/null and b/site/assets/favicon-32.png differ diff --git a/site/assets/favicon.svg b/site/assets/favicon.svg new file mode 100644 index 000000000..568d177e9 --- /dev/null +++ b/site/assets/favicon.svg @@ -0,0 +1,11 @@ + + + + Q + + diff --git a/site/assets/fonts/OFL.txt b/site/assets/fonts/OFL.txt new file mode 100644 index 000000000..cd8eb940f --- /dev/null +++ b/site/assets/fonts/OFL.txt @@ -0,0 +1,98 @@ +The web fonts in this folder are subsets served by Google Fonts and are +used under the SIL Open Font License, Version 1.1: + +Bodoni Moda: Copyright 2020 The Bodoni Moda Project Authors (https://github.com/indestructible-type/Bodoni) +Instrument Sans: Copyright 2022 The Instrument Sans Project Authors (https://github.com/Instrument/instrument-sans) +JetBrains Mono: Copyright 2020 The JetBrains Mono Project Authors (https://github.com/JetBrains/JetBrainsMono) +Noto Sans Math: Copyright 2022 Google LLC. All Rights Reserved. +Noto Sans Mono: Copyright 2022 The Noto Project Authors (https://github.com/notofonts/latin-greek-cyrillic) + +The license is copied below, and is also available with a FAQ at: +https://openfontlicense.org + +----------------------------------------------------------- +SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007 +----------------------------------------------------------- + +PREAMBLE +The goals of the Open Font License (OFL) are to stimulate worldwide +development of collaborative font projects, to support the font creation +efforts of academic and linguistic communities, and to provide a free and +open framework in which fonts may be shared and improved in partnership +with others. + +The OFL allows the licensed fonts to be used, studied, modified and +redistributed freely as long as they are not sold by themselves. The +fonts, including any derivative works, can be bundled, embedded, +redistributed and/or sold with any software provided that any reserved +names are not used by derivative works. The fonts and derivatives, +however, cannot be released under any other type of license. The +requirement for fonts to remain under this license does not apply +to any document created using the fonts or their derivatives. + +DEFINITIONS +"Font Software" refers to the set of files released by the Copyright +Holder(s) under this license and clearly marked as such. This may +include source files, build scripts and documentation. + +"Reserved Font Name" refers to any names specified as such after the +copyright statement(s). + +"Original Version" refers to the collection of Font Software components as +distributed by the Copyright Holder(s). + +"Modified Version" refers to any derivative made by adding to, deleting, +or substituting -- in part or in whole -- any of the components of the +Original Version, by changing formats or by porting the Font Software to a +new environment. + +"Author" refers to any designer, engineer, programmer, technical +writer or other person who contributed to the Font Software. + +PERMISSION & CONDITIONS +Permission is hereby granted, free of charge, to any person obtaining +a copy of the Font Software, to use, study, copy, merge, embed, modify, +redistribute, and sell modified and unmodified copies of the Font +Software, subject to the following conditions: + +1) Neither the Font Software nor any of its individual components, +in Original or Modified Versions, may be sold by itself. + +2) Original or Modified Versions of the Font Software may be bundled, +redistributed and/or sold with any software, provided that each copy +contains the above copyright notice and this license. These can be +included either as stand-alone text files, human-readable headers or +in the appropriate machine-readable metadata fields within text or +binary files as long as those fields can be easily viewed by the user. + +3) No Modified Version of the Font Software may use the Reserved Font +Name(s) unless explicit written permission is granted by the corresponding +Copyright Holder. This restriction only applies to the primary font name as +presented to the users. + +4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font +Software shall not be used to promote, endorse or advertise any +Modified Version, except to acknowledge the contribution(s) of the +Copyright Holder(s) and the Author(s) or with their explicit written +permission. + +5) The Font Software, modified or unmodified, in part or in whole, +must be distributed entirely under this license, and must not be +distributed under any other license. The requirement for fonts to +remain under this license does not apply to any document created +using the Font Software. + +TERMINATION +This license becomes null and void if any of the above conditions are +not met. + +DISCLAIMER +THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT +OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE +COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, +INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL +DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM +OTHER DEALINGS IN THE FONT SOFTWARE. diff --git a/site/assets/fonts/bodoni-moda-italic-latin-ext.woff2 b/site/assets/fonts/bodoni-moda-italic-latin-ext.woff2 new file mode 100644 index 000000000..62606666e Binary files /dev/null and b/site/assets/fonts/bodoni-moda-italic-latin-ext.woff2 differ diff --git a/site/assets/fonts/bodoni-moda-italic-latin.woff2 b/site/assets/fonts/bodoni-moda-italic-latin.woff2 new file mode 100644 index 000000000..3c7c2ec8a Binary files /dev/null and b/site/assets/fonts/bodoni-moda-italic-latin.woff2 differ diff --git a/site/assets/fonts/bodoni-moda-italic-math.woff2 b/site/assets/fonts/bodoni-moda-italic-math.woff2 new file mode 100644 index 000000000..9916a527e Binary files /dev/null and b/site/assets/fonts/bodoni-moda-italic-math.woff2 differ diff --git a/site/assets/fonts/bodoni-moda-italic-symbols.woff2 b/site/assets/fonts/bodoni-moda-italic-symbols.woff2 new file mode 100644 index 000000000..69f166727 Binary files /dev/null and b/site/assets/fonts/bodoni-moda-italic-symbols.woff2 differ diff --git a/site/assets/fonts/bodoni-moda-normal-latin-ext.woff2 b/site/assets/fonts/bodoni-moda-normal-latin-ext.woff2 new file mode 100644 index 000000000..c370e140a Binary files /dev/null and b/site/assets/fonts/bodoni-moda-normal-latin-ext.woff2 differ diff --git a/site/assets/fonts/bodoni-moda-normal-latin.woff2 b/site/assets/fonts/bodoni-moda-normal-latin.woff2 new file mode 100644 index 000000000..7905afa99 Binary files /dev/null and b/site/assets/fonts/bodoni-moda-normal-latin.woff2 differ diff --git a/site/assets/fonts/bodoni-moda-normal-math.woff2 b/site/assets/fonts/bodoni-moda-normal-math.woff2 new file mode 100644 index 000000000..fb0b95722 Binary files /dev/null and b/site/assets/fonts/bodoni-moda-normal-math.woff2 differ diff --git a/site/assets/fonts/bodoni-moda-normal-symbols.woff2 b/site/assets/fonts/bodoni-moda-normal-symbols.woff2 new file mode 100644 index 000000000..07d14497a Binary files /dev/null and b/site/assets/fonts/bodoni-moda-normal-symbols.woff2 differ diff --git a/site/assets/fonts/instrument-sans-italic-latin-ext.woff2 b/site/assets/fonts/instrument-sans-italic-latin-ext.woff2 new file mode 100644 index 000000000..5e3f41eb9 Binary files /dev/null and b/site/assets/fonts/instrument-sans-italic-latin-ext.woff2 differ diff --git a/site/assets/fonts/instrument-sans-italic-latin.woff2 b/site/assets/fonts/instrument-sans-italic-latin.woff2 new file mode 100644 index 000000000..b10fd1c00 Binary files /dev/null and b/site/assets/fonts/instrument-sans-italic-latin.woff2 differ diff --git a/site/assets/fonts/instrument-sans-normal-latin-ext.woff2 b/site/assets/fonts/instrument-sans-normal-latin-ext.woff2 new file mode 100644 index 000000000..0ea0da04c Binary files /dev/null and b/site/assets/fonts/instrument-sans-normal-latin-ext.woff2 differ diff --git a/site/assets/fonts/instrument-sans-normal-latin.woff2 b/site/assets/fonts/instrument-sans-normal-latin.woff2 new file mode 100644 index 000000000..8611e41b1 Binary files /dev/null and b/site/assets/fonts/instrument-sans-normal-latin.woff2 differ diff --git a/site/assets/fonts/jetbrains-mono-italic-greek.woff2 b/site/assets/fonts/jetbrains-mono-italic-greek.woff2 new file mode 100644 index 000000000..bd07500ce Binary files /dev/null and b/site/assets/fonts/jetbrains-mono-italic-greek.woff2 differ diff --git a/site/assets/fonts/jetbrains-mono-italic-latin-ext.woff2 b/site/assets/fonts/jetbrains-mono-italic-latin-ext.woff2 new file mode 100644 index 000000000..c88b32dd9 Binary files /dev/null and b/site/assets/fonts/jetbrains-mono-italic-latin-ext.woff2 differ diff --git a/site/assets/fonts/jetbrains-mono-italic-latin.woff2 b/site/assets/fonts/jetbrains-mono-italic-latin.woff2 new file mode 100644 index 000000000..3d3c5d77e Binary files /dev/null and b/site/assets/fonts/jetbrains-mono-italic-latin.woff2 differ diff --git a/site/assets/fonts/jetbrains-mono-normal-greek.woff2 b/site/assets/fonts/jetbrains-mono-normal-greek.woff2 new file mode 100644 index 000000000..a53d52d6d Binary files /dev/null and b/site/assets/fonts/jetbrains-mono-normal-greek.woff2 differ diff --git a/site/assets/fonts/jetbrains-mono-normal-latin-ext.woff2 b/site/assets/fonts/jetbrains-mono-normal-latin-ext.woff2 new file mode 100644 index 000000000..82f96681c Binary files /dev/null and b/site/assets/fonts/jetbrains-mono-normal-latin-ext.woff2 differ diff --git a/site/assets/fonts/jetbrains-mono-normal-latin.woff2 b/site/assets/fonts/jetbrains-mono-normal-latin.woff2 new file mode 100644 index 000000000..4d09cda4a Binary files /dev/null and b/site/assets/fonts/jetbrains-mono-normal-latin.woff2 differ diff --git a/site/assets/fonts/noto-sans-math-normal-subset.woff2 b/site/assets/fonts/noto-sans-math-normal-subset.woff2 new file mode 100644 index 000000000..2d247d69f Binary files /dev/null and b/site/assets/fonts/noto-sans-math-normal-subset.woff2 differ diff --git a/site/assets/fonts/noto-sans-mono-normal-subset.woff2 b/site/assets/fonts/noto-sans-mono-normal-subset.woff2 new file mode 100644 index 000000000..94411ec60 Binary files /dev/null and b/site/assets/fonts/noto-sans-mono-normal-subset.woff2 differ diff --git a/site/assets/og.png b/site/assets/og.png new file mode 100644 index 000000000..0c325d537 Binary files /dev/null and b/site/assets/og.png differ diff --git a/site/index.html b/site/index.html new file mode 100644 index 000000000..71314b2a7 --- /dev/null +++ b/site/index.html @@ -0,0 +1,1680 @@ + + + + + + +AutoQ 2.0: quantum program verification + + + + + + + + + + + + + + + + + + + + + + + + + +

+ +
+
+ AutoQ + + GitHub + +
+
+ +
+ +
+
+
+
+

AutoQ 2.0

+

An automata-based C++ tool for quantum program verification.

+
+
+

AutoQ verifies the partial correctness of quantum programs. You state a precondition and a postcondition as sets of pure quantum states and give the program in OpenQASM. AutoQ represents each set as a tree automaton, carries it through the program gate by gate, and checks that every resulting state lies in the postcondition, up to a nonzero complex factor.

+
+ View on GitHub +
+ Try it in your browser + Get started + Read the papers +
+
+
+ +
+
+ {P} + + preconditiona set of pure quantum states, written in .hsl or .lsta +
+
+ C + + programa quantum program in a subset of OpenQASM 2.0 or 3.0 +
+
+ {Q} + + postconditionthe set that must contain every result, up to scaling +
+ +
+ + +
+
+
+ + +
+
+

What AutoQ checks

+ +
+
+

A Hoare triple {P} C {Q} is a claim about a program C: run it from a state allowed by the precondition P, and if it terminates, it ends in a state allowed by the postcondition Q. This is partial correctness, and AutoQ checks claims of this kind for quantum programs, up to scaling.

+

In AutoQ, P and Q each describe a set of pure quantum states rather than a single state. AutoQ starts from the whole set ℒ(P), computes how it is transformed immediately after each gate, and hands the result to the next gate. When the program ends, it checks that ℒ(Q) contains the final set C(ℒ(P)), up to scaling:

+
+ C(ℒ(P)) ⊆uts ℒ(Q) + +
+

That is, for every state |s⟩ ∈ C(ℒ(P)) there is a nonzero complex number c ∈ ℂ∖{0} with c|s⟩ ∈ ℒ(Q). A postcondition can therefore leave out normalization factors such as 1/√2; the worked example below relies on exactly that.

+
+ +
+ +

Sets of states as tree automata

+
+
+

AutoQ represents a set of states with a tree automaton. A state becomes a tree with one level per qubit, and each leaf stores one amplitude: in Figure 1 the leaf 000 stores the amplitude of |000⟩, 001 that of |001⟩, and so on. One automaton accepts many such trees, so it can stand for a whole set of states.

+

AutoQ 2.0 uses level-synchronized tree automata, in which each transition carries a set of choices. It also reorders qubits according to the precondition, postcondition and loop invariants, to keep the automata it builds small.

+
+ +
+ +
+ + A 3-qubit state as a binary tree + The root x1 has two children x2; each x2 has two children x3; the eight leaves, from left to right, are 000, 001, 010, 011, 100, 101, 110 and 111. + + + + + + + + + + + + + + + + x1 + x2 + x2 + x3 + x3 + x3 + x3 + + + 000001010011 + 100101110111 + + +
Figure 1. A 3-qubit state as a tree, one level per qubit. The leaf 000 stores the amplitude of |000⟩, and so on. Redrawn from docs/internal_structure.md.
+
+
+
+ + +
+
+

A worked example

+ +
+
+

This two-qubit example is adapted from the README. The precondition holds two states, and the program applies three gates. Each step shows the set of states after one more gate, the tree of each state, and the output of autoq ex on the program up to that point.

+
+
pre.hsl
+
Extended Dirac
+{|00>, 1/2 |00> + 1/2 |01> + 1/2 |10> + 1/2 |11>}
+
+
+
circuit.qasm
+
OPENQASM 3;
+include "stdgates.inc";
+qubit[2] qb;
+
+x qb[0];
+x qb[1];
+h qb[1];
+
+

circuit0.qasm, circuit1.qasm and circuit2.qasm in the steps below are the same file cut after zero, one and two gates.

+
+ +
+ +
+
+ + Circuit: X on qb[0], then X on qb[1], then H on qb[1] + qb[0] + qb[1] + + + X + X + H + + +
+ +
+
+
+ + +
+
+

+ +
    +
  1. +

    0 Start from the precondition

    +
    +
    +

    ℒ(P) = {|00⟩, 12|00⟩ + 12|01⟩ + 12|10⟩ + 12|11⟩}

    +
    1000010100111/2001/2011/2101/211
    +

    Two states: the basis state |00⟩ and the equal superposition of all four basis states.

    +
    +
    +
    Run on a circuit with no gates
    +
    $ autoq ex pre.hsl circuit0.qasm
+OUTPUT:
+{(1/1)|00>,
+ (1/2)|00> + (1/2)|01> + (1/2)|10> + (1/2)|11>}
    +
    +
    +
    2. +
  2. +

    1 x qb[0];

    +
    +
    +

    {|10⟩, 12|10⟩ + 12|11⟩ + 12|00⟩ + 12|01⟩}

    +
    0000011100111/2001/2011/2101/211
    +

    X flips the left bit, so in every tree the two halves under the root swap. The equal superposition maps onto itself, which is why its tree and its line of output do not change.

    +
    +
    +
    Run on the circuit up to this gate
    +
    $ autoq ex pre.hsl circuit1.qasm
+OUTPUT:
+{(1/1)|10>,
+ (1/2)|00> + (1/2)|01> + (1/2)|10> + (1/2)|11>}
    +
    +
    +
    3. +
  3. +

    2 x qb[1];

    +
    +
    +

    {|11⟩, 12|11⟩ + 12|10⟩ + 12|01⟩ + 12|00⟩}

    +
    0000010101111/2001/2011/2101/211
    +

    X flips the right bit, so under each node of the next level the two leaves swap.

    +
    +
    +
    Run on the circuit up to this gate
    +
    $ autoq ex pre.hsl circuit2.qasm
+OUTPUT:
+{(1/1)|11>,
+ (1/2)|00> + (1/2)|01> + (1/2)|10> + (1/2)|11>}
    +
    +
    +
    4. +
  4. +

    3 h qb[1];

    +
    +
    +

    C(ℒ(P)) = {|10⟩/√2 − |11⟩/√2, |10⟩/√2 + |00⟩/√2}

    +
    0000011/√210−1/√2111/√2000011/√210011
    +

    H on qb[1] mixes each pair of sibling leaves a, b into (a+b)/√2 and (a−b)/√2. This is the final set C(ℒ(P)); AutoQ prints 1/√2 as sqrt2*1/2.

    +
    +
    +
    Run on the whole circuit
    +
    $ autoq ex pre.hsl circuit.qasm
+OUTPUT:
+{(sqrt2*1/2)|10> + (sqrt2*-1/2)|11>,
+ (sqrt2*1/2)|00> + (sqrt2*1/2)|10>}
    +
    +
    +
    5. +
  5. +

    4 Check against two postconditions

    +
    +
    +

    Postcondition Q1 passes

    +
    +
    post_Q1.hsl
    +
    Extended Dirac
+{|10> - |11>, |10> + |00>}
    +
    +
    +
    $ autoq ver pre.hsl circuit.qasm post_Q1.hsl
+The quantum program has [2] qubits and [3] gates. The verification process [OK] in [0.2s] with [77MB] memory usage.
    +
    +

    The same two states without the 1/√2 factors. They match up to scaling, so the check passes.

    +
    +
    +

    Postcondition Q2 fails

    +
    +
    post_Q2.hsl
    +
    Extended Dirac
+{|10> - |11>, |10> - |00>}
    +
    +
    +
    $ autoq ver pre.hsl circuit.qasm post_Q2.hsl
+The quantum program has [2] qubits and [3] gates. The verification process [failed] in [0.1s] with [77MB] memory usage.
    +
    +

    One sign is flipped. The state |10⟩/√2 + |00⟩/√2 is in C(ℒ(P)), but no nonzero factor turns it into a state of ℒ(Q2).

    +
    +
    +
    6. +
+
+
+
+ + +
+
+

Get started

+
+
+

To try AutoQ without installing anything, open the playground: it runs the same tool in your browser, compiled to WebAssembly, with the examples from this page ready to run.

+

To install it, AutoQ builds from source on Linux (Ubuntu or Debian), macOS and WSL2. Four steps take you from a fresh clone to a verified program.

+
    +
  1. +

    Clone the repository

    +
    +
    Clone
    +
    git clone https://github.com/fmlab-iis/AutoQ.git
+cd AutoQ
    +
    +
    2. +
  2. +

    Install the dependencies

    +
    +
    +
    Ubuntu, Debian, WSL2
    +
    sudo ./install-dependencies.sh
    +
    +
    +
    macOS
    +
    ./install-dependencies.sh
    +
    +
    +

    On Ubuntu and Debian, including under WSL2, the script installs g++, make, cmake, libboost-filesystem-dev, libboost-test-dev and libantlr4-runtime-dev with apt, so run it with sudo. On macOS, run it without sudo: it uses Homebrew to install gcc, make, cmake, boost and antlr4-cpp-runtime.

    +
    3. +
  3. +

    Build and test

    +
    +
    Build and test
    +
    make
+make test
    +
    +

    make compiles AutoQ with optimizations, and make test runs the unit tests. The binary is build/cli/autoq. For a debug build, run make debug instead of make.

    +
    4. +
  4. +

    Verify a program

    +

    ver is the mode used most often in the AutoQ papers. It takes a precondition, a circuit and a postcondition. Here it checks the README’s example, a Grover’s search benchmark on five qubits.

    +
    +
    Verify the example
    +
    $ ./build/cli/autoq ver \
+    benchmarks/all/Grover/03/pre.hsl \
+    benchmarks/all/Grover/03/circuit.qasm \
+    benchmarks/all/Grover/03/post.hslThe quantum program has [5] qubits and [52] gates. The verification process [OK] in [0.1s] with [77MB] memory usage.
    +
    +

    Times and memory figures in the outputs on this page come from one machine and will vary on yours.

    +
    +
    +
    pre.hsl
    +
    Constants
+c1 := 1
+Extended Dirac
+{c1 |00000>}
    +
    +
    +
    post.hsl
    +
    Constants
+aH := 11 / (sqrt2 ^ 7)
+aL := -1 / (sqrt2 ^ 7)
+Extended Dirac
+{aH |01001> + aL ∑ |i|=3, i≠010 |i01>}
    +
    +
    +

    The demo folder has more small examples, including Bernstein–Vazirani and a Grover iteration.

    +
    5. +
+
+ +
+

Commands

+
+
ex
autoq ex [OPTIONS] pre.hsl circuit.qasm
Execute a quantum circuit with a given precondition.
Option: --loopsum
+
ver
autoq ver [OPTIONS] pre.hsl circuit.qasm post.hsl
Verify the execution result against a given postcondition.
Options: --loopsum, -l, --latex
+
eq
autoq eq [OPTIONS] circuit1.qasm circuit2.qasm
Check equivalence of two given quantum circuits.
Option: --loopsum
+
print
autoq print [OPTIONS] states.hsl
Print the set of quantum states.
+
+

--loopsum summarizes loops using symbolic execution. -l, --latex on ver prints the statistics for tables in LaTeX. autoq -v prints the full Git commit hash.

+
+
+ + +
+
+

From circuits to programs

+
+
+

AutoQ 2.0 goes beyond straight-line circuits. It verifies programs that measure, branch and loop, and it accepts symbolic amplitudes in specifications. AutoQ can also check whether two circuits are equivalent.

+
+
+ +

4.1 Symbolic amplitudes

+
+
+

An amplitude may use names that are not declared in the Constants section. AutoQ treats them as free symbolic variables, which the optional Constraints section can restrict. The precondition below, {x|0⟩ + y|1⟩}, therefore stands for every state of that form, and the postcondition requires each amplitude to come back unchanged.

+
+
+
benchmarks/all/H2Sym/pre.hsl
+
Extended Dirac
+{x |0> + y |1>}
+
+
+
H2Sym/post.hsl
+
Extended Dirac
+{p1 |0> + p2 |1>}
+Constraints
+real(p1) = real(x)
+imag(p1) = imag(x)
+real(p2) = real(y)
+imag(p2) = imag(y)
+
+
+

Applying H twice passes. In the H2BugSym benchmark the second H is replaced by Y, and verification fails.

+
+
+
Gates of H2Sym/circuit.qasm, and the run
+
h qubits[0];
+h qubits[0];
+$ autoq ver pre.hsl circuit.qasm post.hsl
+The quantum program has [1] qubits and [2] gates. The verification process [OK] in [0.2s] with [85MB] memory usage.
+
+
+
Gates of H2BugSym/circuit.qasm, and the run
+
h qubits[0];
+y qubits[0];
+$ autoq ver pre.hsl circuit.qasm post.hsl
+The quantum program has [1] qubits and [2] gates. The verification process [failed] in [0.2s] with [86MB] memory usage.
+
+
+
+ +
+ +

4.2 Measurement, branching and loops

+
+
+

A program can measure a qubit into a classical bit and then branch on it with if and else, or loop on it with while. The if block runs on the states where the outcome is 1, the else block on those where it is 0, and AutoQ joins the two results. Both if (!c) and while (!c) are allowed, and else is optional.

+

A while loop needs a measurement just before the loop and at the end of its body, plus a loop invariant: a set of states in its own .hsl file, named in a comment on the while line. AutoQ checks that the states reaching the loop lie in the invariant, and that one pass of the body maps the invariant’s continuing states back into it. It then carries on with the states that leave the loop.

+
+
benchmarks/all/control_mini/while/circuit.qasm
+
OPENQASM 3;
+include "stdgates.inc";
+qubit[2] qb;
+bit[2] outcome;
+
+h qb[0];
+cx qb[0], qb[1];
+outcome[0] = measure qb[0];
+while (!outcome[0]) { // loop-invariant.hsl
+    x qb[0];
+    h qb[0];
+    cx qb[0], qb[1];
+    outcome[0] = measure qb[0];
+}
+
+
+
+
loop-invariant.hsl
+
Extended Dirac
+{|00> - |11>,
+ |01> - |10>}
+
+
+
pre.hsl and post.hsl (identical)
+
Extended Dirac
+{|10>, |11>}
+
+
+
+
$ autoq ver pre.hsl circuit.qasm post.hsl
+The quantum program has [2] qubits and [6] gates. The verification process [OK] in [0.2s] with [84MB] memory usage.
+
+
+ +
+ +

4.3 Loop summarization

+
+
+

A loop for int i in [x:y] { C } runs its body C exactly y − x + 1 times. By default AutoQ applies the body’s gates one iteration after another. With --loopsum on ex or ver, AutoQ applies its loop summarization algorithm, which uses symbolic execution, to the loop’s body.

+
+
From docs/qasm_description.md
+
...
+qreg qb[1]; // quantum register
+...
+for int i in [1:2] {
+    h qb[0];
+    t qb[0];
+}
+...
+
+
+
+ +

4.4 Circuit equivalence

+
+
+

autoq eq checks whether two circuits are equal. A CX gate equals a CZ placed between two H gates on the target qubit; reversing control and target gives a different circuit.

+
+
+
a.qasm
+
OPENQASM 2.0;
+include "qelib1.inc";
+qreg q[2];
+cx q[0], q[1];
+
+
+
b.qasm
+
OPENQASM 2.0;
+include "qelib1.inc";
+qreg q[2];
+h q[1];
+cz q[0], q[1];
+h q[1];
+
+
+
+
$ autoq eq a.qasm b.qasm
+The two quantum programs are verified to be [equal] in [0.0s] with [7MB] memory usage.
+$ autoq eq a.qasm c.qasm  # c.qasm: cx q[1], q[0];
+The two quantum programs are verified to be [unequal] in [0.0s] with [7MB] memory usage.
+
+
+ +
+ +

4.5 Gate set

+
+
+

AutoQ documents the fourteen gates below, written in OpenQASM with the spelling shown under each. Gates the parser does not recognise, such as u3 or cy, stop the run with an unsupported gate error.

+
+
+
    +
  • Xx
    • +
  • Yy
    • +
  • Zz
    • +
  • Hh
    • +
  • Tt
    • +
  • T†tdg
    • +
  • Ss
    • +
  • S†sdg
    • +
  • Rx(π/2)rx(pi/2)
    • +
  • Ry(π/2)ry(pi/2)
    • +
  • CXcx
    • +
  • CZcz
    • +
  • CCXccx
    • +
  • SWAPswap
    • +
+
+
+ + +
+
+

Writing specifications

+
+
+

Preconditions, postconditions and loop invariants are all sets of quantum states. Specifications are written in .hsl or .lsta; programs in .qasm.

+
+
.hsl

A high-level specification language that extends Dirac notation to describe sets of quantum states. A file has a Constants section (optional), an Extended Dirac section, and a Constraints section (optional), in that order.

The .hsl format
+
.qasm

OpenQASM 2.0 or 3.0, with very limited syntax: a single quantum register, classical bits used only right before control flow, the fourteen gates above, if/else, while and for.

The supported OpenQASM subset
+
.lsta

A set of states written directly as a level-synchronized tree automaton. It keeps Constants and Constraints and replaces Extended Dirac with Root States and Transitions.

The .lsta format
+
+
+
+ +

Reading an .hsl file

+
+
+

The GHZall/002 benchmark runs a two-qubit circuit, h qubits[0]; cx qubits[0], qubits[1];, on all four basis states at once.

+
+
+
GHZall/002/pre.hsl
+
Constants
+c1 := 1
+Extended Dirac
+{c1 |ji> : |j|=1, |i|=1}
+
+
+
GHZall/002/post.hsl
+
Constants
+cp := 1/sqrt2
+cn := -1/sqrt2
+Extended Dirac
+{cp |0i> + cp |1i'> : |i|=1} ∪
+{cp |0i> + cn |1i'> : |i|=1}
+
+
+
    +
  1. {c1 |ji> : |j|=1, |i|=1} lets j and i range over 1-bit strings, so the precondition holds all four basis states. autoq print pre.hsl lists them.
    2. +
  2. In |1i'>, i' is the bitwise complement of i.
    3. +
  3. ∪ joins two sets: here, the states with a plus sign and those with a minus sign.
    4. +
+
+
+
$ autoq print pre.hsl
+{(1/1)|11>,
+ (1/1)|10>,
+ (1/1)|01>,
+ (1/1)|00>}
+
+
+
$ autoq ver pre.hsl circuit.qasm post.hsl
+The quantum program has [2] qubits and [2] gates. The verification process [OK] in [0.1s] with [77MB] memory usage.
+
+
+
+ +
+ +
+
+
+ Table 1. Extended Dirac notation at a glance +
+ + + + + + + + + + + + +
Extended Dirac notation
NotationMeaningASCII
S ∪ Tunion of two sets of states
S ⊗ Ttensor product of two setsS * T
S ^ ntensor power
|i⟩, |1i′⟩binary-string variable (lowercase), and its complement|1i'>
∑ |i|=4, i≠0101 |i⟩sum over strings that meet the constraintsΣ, !=
{ … : |s|=4, s≠0101 }set-builder notation with constraints!=
= ≠ < ≤ > ≥ ¬ ∧ ∨operators in the Constraints section, one conjunct per line!= <= >= ! && ||
+
+

Kets can be closed with ⟩ or >. Constants may use real(c), imag(c), eipi(r), ei2pi(r), sqrt2, nonnegative integers and + - * / ^.

+
+
+
+
+
+ + +
+
+

Papers

+
+
+

Please cite the following papers if you use this tool for your research.

+
+
+
    +
  1. + +
    +

    Verifying Quantum Circuits with Level-Synchronized Tree Automata

    +

    Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Lukáš Holík, Ondřej Lengál, Jyun-Ao Lin, Fang-Yi Lo, Wei-Lun Tsai

    +

    Proceedings of the ACM on Programming Languages 9 (POPL), 2025, pp. 923–953

    +
    + doi:10.1145/3704868 + Benchmarks: POPL25 + +
    +
    +
    + BibTeX +
    +
    @article{10.1145/3704868,
+  title = {Verifying Quantum Circuits with Level-Synchronized Tree Automata},
+  author = {Abdulla, Parosh Aziz and Chen, Yo-Ga and Chen, Yu-Fang and Hol\'{\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej and Lin, Jyun-Ao and Lo, Fang-Yi and Tsai, Wei-Lun},
+  journal = {Proceedings of the ACM on Programming Languages},
+  volume = {9},
+  number = {POPL},
+  year = {2025},
+  pages = {923--953},
+  doi = {10.1145/3704868}
+}
    +
    +
    +
    2. +
  2. + +
    +

    AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs

    +

    Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Ondřej Lengál, Jyun-Ao Lin, Wei-Lun Tsai

    +

    International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2025, pp. 87–108

    +
    + doi:10.1007/978-3-031-90660-2_5 + Benchmarks: TACAS25 + +
    +
    +
    + BibTeX +
    +
    @InProceedings{10.1007/978-3-031-90660-2_5,
+  author = {Chen, Yu-Fang and Chung, Kai-Min and Hsieh, Min-Hsiu and Huang, Wei-Jia and Leng{\'a}l, Ond{\v{r}}ej and Lin, Jyun-Ao and Tsai, Wei-Lun},
+  booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
+  title = {AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs},
+  year = {2025},
+  pages = {87--108},
+  doi = {10.1007/978-3-031-90660-2_5}
+}
    +
    +
    +
    3. +
+
+
+

The benchmarks folder holds all the files used to produce the experimental results.

+
+
+
+
+ + +
+
+

Learn more, ask questions

+
+
+

Watch

+

The introductory video shows more examples of how to use AutoQ.

+ + + Watch the introductory video on YouTube + +
+
+

Read

+ +
+
+

Ask

+

If you have any questions or suggestions, create an issue on GitHub or contact us via alan23273850@gmail.com.

+
+
+
+
+ +
+ + + + + + diff --git a/site/playground/examples.js b/site/playground/examples.js new file mode 100644 index 000000000..c69971286 --- /dev/null +++ b/site/playground/examples.js @@ -0,0 +1,207 @@ +// Playground examples; `source` says where each one comes from. +export const EXAMPLES = [ + { + "id": "readme", + "title": "README example (2 qubits, X X H)", + "source": "README.md (as on the landing page)", + "mode": "ver", + "files": [ + { + "name": "pre.hsl", + "content": "Extended Dirac\n{|00>, 1/2 |00> + 1/2 |01> + 1/2 |10> + 1/2 |11>}\n" + }, + { + "name": "circuit.qasm", + "content": "OPENQASM 3;\ninclude \"stdgates.inc\";\nqubit[2] qb;\n\nx qb[0];\nx qb[1];\nh qb[1];\n" + }, + { + "name": "post.hsl", + "content": "Extended Dirac\n{|10> - |11>, |10> + |00>}\n" + } + ] + }, + { + "id": "bv", + "title": "Bernstein–Vazirani, 4 qubits", + "source": "benchmarks/all/BV/03", + "mode": "ver", + "files": [ + { + "name": "pre.hsl", + "content": "Constants\nc1 := 1\nExtended Dirac\n{c1 |0000>}\n" + }, + { + "name": "circuit.qasm", + "content": "OPENQASM 2.0;\ninclude \"qelib1.inc\";\nqreg qubits[4];\n\nh qubits[0];\nh qubits[1];\nh qubits[2];\nh qubits[3];\nz qubits[3];\ncx qubits[0], qubits[3];\ncx qubits[2], qubits[3];\nh qubits[0];\nh qubits[1];\nh qubits[2];\nh qubits[3];\n" + }, + { + "name": "post.hsl", + "content": "Constants\nc1 := 1\nExtended Dirac\n{c1 |1011>}\n" + } + ] + }, + { + "id": "grover-sym", + "title": "Grover search, symbolic amplitudes", + "source": "benchmarks/all/GroverSym/02", + "mode": "ver", + "files": [ + { + "name": "pre.hsl", + "content": "Constants\nc1 := 1\nExtended Dirac\n{ c1 |000> }\n" + }, + { + "name": "circuit.qasm", + "content": "OPENQASM 2.0;\ninclude \"qelib1.inc\";\nqreg qubits[3];\nx qubits[2];\n\nh qubits[0];\nh qubits[1];\nh qubits[2];\nx qubits[0];\nccx qubits[0], qubits[1], qubits[2];\nx qubits[0];\nh qubits[0];\nh qubits[1];\nx qubits[0];\nx qubits[1];\ncz qubits[0], qubits[1];\nx qubits[0];\nx qubits[1];\nh qubits[0];\nh qubits[1];\nh qubits[2];\n" + }, + { + "name": "post.hsl", + "content": "Extended Dirac\n{pH |011> + pL ∑ |i|=3, i≠011 |i>}\nConstraints\nreal(pL) * real(pL) < 1/8\nimag(pL) = 0\nreal(pH) * real(pH) > 7/8\nimag(pH) = 0\n" + } + ] + }, + { + "id": "grover", + "title": "Grover search, 5 qubits", + "source": "benchmarks/all/Grover/03", + "mode": "ver", + "files": [ + { + "name": "pre.hsl", + "content": "Constants\nc1 := 1\nExtended Dirac\n{c1 |00000>}\n" + }, + { + "name": "circuit.qasm", + "content": "OPENQASM 2.0;\ninclude \"qelib1.inc\";\nqreg qubits[5];\nx qubits[4];\n\nh qubits[0];\nh qubits[1];\nh qubits[2];\nh qubits[4];\n\nx qubits[0];\nx qubits[2];\nccx qubits[0], qubits[1], qubits[3];\ncz qubits[3], qubits[2];\nccx qubits[0], qubits[1], qubits[3];\nx qubits[0];\nx qubits[2];\nh qubits[0];\nh qubits[1];\nh qubits[2];\nx qubits[0];\nx qubits[1];\nx qubits[2];\nccx qubits[0], qubits[1], qubits[3];\ncz qubits[3], qubits[2];\nccx qubits[0], qubits[1], qubits[3];\nx qubits[0];\nx qubits[1];\nx qubits[2];\nh qubits[0];\nh qubits[1];\nh qubits[2];\nx qubits[4];\n\nx qubits[0];\nx qubits[2];\nccx qubits[0], qubits[1], qubits[3];\ncz qubits[3], qubits[2];\nccx qubits[0], qubits[1], qubits[3];\nx qubits[0];\nx qubits[2];\nh qubits[0];\nh qubits[1];\nh qubits[2];\nx qubits[0];\nx qubits[1];\nx qubits[2];\nccx qubits[0], qubits[1], qubits[3];\ncz qubits[3], qubits[2];\nccx qubits[0], qubits[1], qubits[3];\nx qubits[0];\nx qubits[1];\nx qubits[2];\nh qubits[0];\nh qubits[1];\nh qubits[2];\nx qubits[4];\n\nh qubits[4];\n" + }, + { + "name": "post.hsl", + "content": "Constants\naH := 11 / (sqrt2 ^ 7)\naL := -1 / (sqrt2 ^ 7)\nExtended Dirac\n{aH |01001> + aL ∑ |i|=3, i≠010 |i01>}\n" + } + ] + }, + { + "id": "ifelse", + "title": "Measurement and if", + "source": "benchmarks/all/control_mini/if-else", + "mode": "ver", + "files": [ + { + "name": "pre.hsl", + "content": "Extended Dirac\n{|10>, |11>}\n" + }, + { + "name": "circuit.qasm", + "content": "OPENQASM 3;\ninclude \"stdgates.inc\";\nqubit[2] qb;\nbit[2] outcome;\n\nh qb[0];\ncx qb[0], qb[1];\noutcome[0] = measure qb[0];\nif (!outcome[0]) {\n x qb[0];\n}\n" + }, + { + "name": "post.hsl", + "content": "Extended Dirac\n{|10>, |11>}\n" + } + ] + }, + { + "id": "while", + "title": "While loop with an invariant", + "source": "benchmarks/all/control_mini/while", + "mode": "ver", + "files": [ + { + "name": "pre.hsl", + "content": "Extended Dirac\n{|10>, |11>}\n" + }, + { + "name": "circuit.qasm", + "content": "OPENQASM 3;\ninclude \"stdgates.inc\";\nqubit[2] qb;\nbit[2] outcome;\n\nh qb[0];\ncx qb[0], qb[1];\noutcome[0] = measure qb[0];\nwhile (!outcome[0]) { // loop-invariant.hsl\n x qb[0];\n h qb[0];\n cx qb[0], qb[1];\n outcome[0] = measure qb[0];\n}\n" + }, + { + "name": "post.hsl", + "content": "Extended Dirac\n{|10>, |11>}\n" + }, + { + "name": "loop-invariant.hsl", + "content": "Extended Dirac\n{|00> - |11>,\n |01> - |10>}\n" + } + ] + }, + { + "id": "eq", + "title": "Equivalence: CX = H·CZ·H", + "source": "landing page", + "mode": "eq", + "files": [ + { + "name": "a.qasm", + "content": "OPENQASM 2.0;\ninclude \"qelib1.inc\";\nqreg q[2];\ncx q[0], q[1];\n" + }, + { + "name": "b.qasm", + "content": "OPENQASM 2.0;\ninclude \"qelib1.inc\";\nqreg q[2];\nh q[1];\ncz q[0], q[1];\nh q[1];\n" + } + ] + }, + { + "id": "eq-swap", + "title": "Equivalence: SWAP = three CX gates", + "source": "standard identity", + "mode": "eq", + "files": [ + { + "name": "a.qasm", + "content": "OPENQASM 2.0;\ninclude \"qelib1.inc\";\nqreg q[2];\nswap q[0], q[1];\n" + }, + { + "name": "b.qasm", + "content": "OPENQASM 2.0;\ninclude \"qelib1.inc\";\nqreg q[2];\ncx q[0], q[1];\ncx q[1], q[0];\ncx q[0], q[1];\n" + } + ] + }, + { + "id": "eq-toffoli", + "title": "Equivalence: Toffoli in Clifford+T", + "source": "standard Clifford+T decomposition (7 T gates, 6 CX)", + "mode": "eq", + "files": [ + { + "name": "a.qasm", + "content": "OPENQASM 2.0;\ninclude \"qelib1.inc\";\nqreg q[3];\nccx q[0], q[1], q[2];\n" + }, + { + "name": "b.qasm", + "content": "OPENQASM 2.0;\ninclude \"qelib1.inc\";\nqreg q[3];\nh q[2];\ncx q[1], q[2];\ntdg q[2];\ncx q[0], q[2];\nt q[2];\ncx q[1], q[2];\ntdg q[2];\ncx q[0], q[2];\nt q[1];\nt q[2];\nh q[2];\ncx q[0], q[1];\nt q[0];\ntdg q[1];\ncx q[0], q[1];\n" + } + ] + }, + { + "id": "eq-toffoli-bug", + "title": "Non-equivalence: Toffoli with a wrong T gate", + "source": "eq-toffoli with one T replaced by T†", + "mode": "eq", + "files": [ + { + "name": "a.qasm", + "content": "OPENQASM 2.0;\ninclude \"qelib1.inc\";\nqreg q[3];\nccx q[0], q[1], q[2];\n" + }, + { + "name": "b.qasm", + "content": "OPENQASM 2.0;\ninclude \"qelib1.inc\";\nqreg q[3];\nh q[2];\ncx q[1], q[2];\ntdg q[2];\ncx q[0], q[2];\ntdg q[2]; // should be: t q[2];\ncx q[1], q[2];\ntdg q[2];\ncx q[0], q[2];\nt q[1];\nt q[2];\nh q[2];\ncx q[0], q[1];\nt q[0];\ntdg q[1];\ncx q[0], q[1];\n" + } + ] + }, + { + "id": "eq-phase", + "title": "Equivalence up to global phase: XZ vs ZX", + "source": "standard identity (XZ = −ZX)", + "mode": "eq", + "files": [ + { + "name": "a.qasm", + "content": "OPENQASM 2.0;\ninclude \"qelib1.inc\";\nqreg q[1];\nx q[0];\nz q[0];\n" + }, + { + "name": "b.qasm", + "content": "OPENQASM 2.0;\ninclude \"qelib1.inc\";\nqreg q[1];\nz q[0];\nx q[0];\n" + } + ] + } +]; diff --git a/site/playground/index.html b/site/playground/index.html new file mode 100644 index 000000000..761327da8 --- /dev/null +++ b/site/playground/index.html @@ -0,0 +1,110 @@ + + + + + + +AutoQ playground: verify quantum programs in your browser + + + + + + + + + + + + + + + + + + + +
+
+ AutoQ + Playground + +
+
+ +
+
+

Playground

+

Run AutoQ in your browser. This is the command-line tool itself, compiled to WebAssembly: it reads the same .hsl and OpenQASM files and prints the same output. Everything runs on your machine; nothing is uploaded.

+

Loading AutoQ…

+
+ + + +
+
+ +
+ Command +
+ + + +
+
+ +
+ + + +
+
+ +
+
+
+
+
+ + 

+      

+      

+        

+          Output
+          
+        

+        

+      

+    

+  

+
+  

+    
Notes

+    
+  

+

+
+
+
+
diff --git a/site/playground/playground.css b/site/playground/playground.css
new file mode 100644
index 000000000..c7334be2c
--- /dev/null
+++ b/site/playground/playground.css
@@ -0,0 +1,338 @@
+/* AutoQ playground. Fonts and colour tokens are copied from ../index.html. */
+/* Self-hosted subsets of Bodoni Moda, Instrument Sans, JetBrains Mono, Noto Sans Math and Noto Sans Mono (SIL OFL 1.1, see assets/fonts/OFL.txt). */
+@font-face {
+  font-family: 'Bodoni Moda';
+  font-style: italic;
+  font-weight: 400 700;
+  font-display: swap;
+  src: url(../assets/fonts/bodoni-moda-italic-math.woff2) format('woff2');
+  unicode-range: U+0302-0303, U+0305, U+0307-0308, U+0310, U+0312, U+0315, U+031A, U+0326-0327, U+032C, U+032F-0330, U+0332-0333, U+0338, U+033A, U+0346, U+034D, U+0391-03A1, U+03A3-03A9, U+03B1-03C9, U+03D1, U+03D5-03D6, U+03F0-03F1, U+03F4-03F5, U+2016-2017, U+2034-2038, U+203C, U+2040, U+2043, U+2047, U+2050, U+2057, U+205F, U+2070-2071, U+2074-209F, U+20D0-20DC, U+20E1, U+20E5-20EF, U+2100-2112, U+2114-2115, U+2117-2121, U+2123-214F, U+2190, U+2192, U+2194-21AE, U+21B0-21E5, U+21F1-21F2, U+21F4-2211, U+2213-2214, U+2216-22FF, U+2308-230B, U+2310, U+2319, U+231C-2321, U+2336-237A, U+237C, U+2395, U+239B-23B7, U+23D0, U+23DC-23E1, U+2474-2475, U+25AF, U+25B3, U+25B7, U+25BD, U+25C1, U+25CA, U+25CC, U+25FB, U+266D-266F, U+27C0-27FF, U+2900-2AFF, U+2B0E-2B11, U+2B30-2B4C, U+2BFE, U+3030, U+FF5B, U+FF5D, U+1D400-1D7FF, U+1EE00-1EEFF;
+}
+@font-face {
+  font-family: 'Bodoni Moda';
+  font-style: italic;
+  font-weight: 400 700;
+  font-display: swap;
+  src: url(../assets/fonts/bodoni-moda-italic-symbols.woff2) format('woff2');
+  unicode-range: U+0001-000C, U+000E-001F, U+007F-009F, U+20DD-20E0, U+20E2-20E4, U+2150-218F, U+2190, U+2192, U+2194-2199, U+21AF, U+21E6-21F0, U+21F3, U+2218-2219, U+2299, U+22C4-22C6, U+2300-243F, U+2440-244A, U+2460-24FF, U+25A0-27BF, U+2800-28FF, U+2921-2922, U+2981, U+29BF, U+29EB, U+2B00-2BFF, U+4DC0-4DFF, U+FFF9-FFFB, U+10140-1018E, U+10190-1019C, U+101A0, U+101D0-101FD, U+102E0-102FB, U+10E60-10E7E, U+1D2C0-1D2D3, U+1D2E0-1D37F, U+1F000-1F0FF, U+1F100-1F1AE, U+1F1E6-1F1FF, U+1F30D-1F30F, U+1F315, U+1F31C, U+1F31E, U+1F320-1F32C, U+1F336, U+1F378, U+1F37D, U+1F382, U+1F393-1F39F, U+1F3A7-1F3A8, U+1F3AC-1F3AF, U+1F3C2, U+1F3C4-1F3C6, U+1F3CA-1F3CE, U+1F3D4-1F3E0, U+1F3ED, U+1F3F1-1F3F3, U+1F3F5-1F3F7, U+1F408, U+1F415, U+1F41F, U+1F426, U+1F43F, U+1F441-1F442, U+1F444, U+1F446-1F449, U+1F44C-1F44E, U+1F453, U+1F46A, U+1F47D, U+1F4A3, U+1F4B0, U+1F4B3, U+1F4B9, U+1F4BB, U+1F4BF, U+1F4C8-1F4CB, U+1F4D6, U+1F4DA, U+1F4DF, U+1F4E3-1F4E6, U+1F4EA-1F4ED, U+1F4F7, U+1F4F9-1F4FB, U+1F4FD-1F4FE, U+1F503, U+1F507-1F50B, U+1F50D, U+1F512-1F513, U+1F53E-1F54A, U+1F54F-1F5FA, U+1F610, U+1F650-1F67F, U+1F687, U+1F68D, U+1F691, U+1F694, U+1F698, U+1F6AD, U+1F6B2, U+1F6B9-1F6BA, U+1F6BC, U+1F6C6-1F6CF, U+1F6D3-1F6D7, U+1F6E0-1F6EA, U+1F6F0-1F6F3, U+1F6F7-1F6FC, U+1F700-1F80B, U+1F810-1F847, U+1F850-1F859, U+1F860-1F887, U+1F890-1F8AD, U+1F8B0-1F8BB, U+1F8C0-1F8C1, U+1F8D0-1F8D8, U+1F900-1F90B, U+1F93B, U+1F946, U+1F984, U+1F996, U+1F9E9, U+1FA00-1FA6F, U+1FA70-1FA7C, U+1FA80-1FAC6, U+1FAC8, U+1FACC-1FADD, U+1FADF-1FAEB, U+1FAEF-1FAFA, U+1FB00-1FBFF;
+}
+@font-face {
+  font-family: 'Bodoni Moda';
+  font-style: italic;
+  font-weight: 400 700;
+  font-display: swap;
+  src: url(../assets/fonts/bodoni-moda-italic-latin-ext.woff2) format('woff2');
+  unicode-range: U+0100-02BA, U+02BD-02C5, U+02C7-02CC, U+02CE-02D7, U+02DD-02FF, U+0304, U+0308, U+0329, U+1D00-1DBF, U+1E00-1E9F, U+1EF2-1EFF, U+2020, U+20A0-20AB, U+20AD-20C4, U+2113, U+2C60-2C7F, U+A720-A7FF;
+}
+@font-face {
+  font-family: 'Bodoni Moda';
+  font-style: italic;
+  font-weight: 400 700;
+  font-display: swap;
+  src: url(../assets/fonts/bodoni-moda-italic-latin.woff2) format('woff2');
+  unicode-range: U+0000-00FF, U+0131, U+0152-0153, U+02BB-02BC, U+02C6, U+02DA, U+02DC, U+0304, U+0308, U+0329, U+2000-206F, U+20AC, U+2122, U+2191, U+2193, U+2212, U+2215, U+FEFF, U+FFFD;
+}
+@font-face {
+  font-family: 'Bodoni Moda';
+  font-style: normal;
+  font-weight: 400 700;
+  font-display: swap;
+  src: url(../assets/fonts/bodoni-moda-normal-math.woff2) format('woff2');
+  unicode-range: U+0302-0303, U+0305, U+0307-0308, U+0310, U+0312, U+0315, U+031A, U+0326-0327, U+032C, U+032F-0330, U+0332-0333, U+0338, U+033A, U+0346, U+034D, U+0391-03A1, U+03A3-03A9, U+03B1-03C9, U+03D1, U+03D5-03D6, U+03F0-03F1, U+03F4-03F5, U+2016-2017, U+2034-2038, U+203C, U+2040, U+2043, U+2047, U+2050, U+2057, U+205F, U+2070-2071, U+2074-209F, U+20D0-20DC, U+20E1, U+20E5-20EF, U+2100-2112, U+2114-2115, U+2117-2121, U+2123-214F, U+2190, U+2192, U+2194-21AE, U+21B0-21E5, U+21F1-21F2, U+21F4-2211, U+2213-2214, U+2216-22FF, U+2308-230B, U+2310, U+2319, U+231C-2321, U+2336-237A, U+237C, U+2395, U+239B-23B7, U+23D0, U+23DC-23E1, U+2474-2475, U+25AF, U+25B3, U+25B7, U+25BD, U+25C1, U+25CA, U+25CC, U+25FB, U+266D-266F, U+27C0-27FF, U+2900-2AFF, U+2B0E-2B11, U+2B30-2B4C, U+2BFE, U+3030, U+FF5B, U+FF5D, U+1D400-1D7FF, U+1EE00-1EEFF;
+}
+@font-face {
+  font-family: 'Bodoni Moda';
+  font-style: normal;
+  font-weight: 400 700;
+  font-display: swap;
+  src: url(../assets/fonts/bodoni-moda-normal-symbols.woff2) format('woff2');
+  unicode-range: U+0001-000C, U+000E-001F, U+007F-009F, U+20DD-20E0, U+20E2-20E4, U+2150-218F, U+2190, U+2192, U+2194-2199, U+21AF, U+21E6-21F0, U+21F3, U+2218-2219, U+2299, U+22C4-22C6, U+2300-243F, U+2440-244A, U+2460-24FF, U+25A0-27BF, U+2800-28FF, U+2921-2922, U+2981, U+29BF, U+29EB, U+2B00-2BFF, U+4DC0-4DFF, U+FFF9-FFFB, U+10140-1018E, U+10190-1019C, U+101A0, U+101D0-101FD, U+102E0-102FB, U+10E60-10E7E, U+1D2C0-1D2D3, U+1D2E0-1D37F, U+1F000-1F0FF, U+1F100-1F1AE, U+1F1E6-1F1FF, U+1F30D-1F30F, U+1F315, U+1F31C, U+1F31E, U+1F320-1F32C, U+1F336, U+1F378, U+1F37D, U+1F382, U+1F393-1F39F, U+1F3A7-1F3A8, U+1F3AC-1F3AF, U+1F3C2, U+1F3C4-1F3C6, U+1F3CA-1F3CE, U+1F3D4-1F3E0, U+1F3ED, U+1F3F1-1F3F3, U+1F3F5-1F3F7, U+1F408, U+1F415, U+1F41F, U+1F426, U+1F43F, U+1F441-1F442, U+1F444, U+1F446-1F449, U+1F44C-1F44E, U+1F453, U+1F46A, U+1F47D, U+1F4A3, U+1F4B0, U+1F4B3, U+1F4B9, U+1F4BB, U+1F4BF, U+1F4C8-1F4CB, U+1F4D6, U+1F4DA, U+1F4DF, U+1F4E3-1F4E6, U+1F4EA-1F4ED, U+1F4F7, U+1F4F9-1F4FB, U+1F4FD-1F4FE, U+1F503, U+1F507-1F50B, U+1F50D, U+1F512-1F513, U+1F53E-1F54A, U+1F54F-1F5FA, U+1F610, U+1F650-1F67F, U+1F687, U+1F68D, U+1F691, U+1F694, U+1F698, U+1F6AD, U+1F6B2, U+1F6B9-1F6BA, U+1F6BC, U+1F6C6-1F6CF, U+1F6D3-1F6D7, U+1F6E0-1F6EA, U+1F6F0-1F6F3, U+1F6F7-1F6FC, U+1F700-1F80B, U+1F810-1F847, U+1F850-1F859, U+1F860-1F887, U+1F890-1F8AD, U+1F8B0-1F8BB, U+1F8C0-1F8C1, U+1F8D0-1F8D8, U+1F900-1F90B, U+1F93B, U+1F946, U+1F984, U+1F996, U+1F9E9, U+1FA00-1FA6F, U+1FA70-1FA7C, U+1FA80-1FAC6, U+1FAC8, U+1FACC-1FADD, U+1FADF-1FAEB, U+1FAEF-1FAFA, U+1FB00-1FBFF;
+}
+@font-face {
+  font-family: 'Bodoni Moda';
+  font-style: normal;
+  font-weight: 400 700;
+  font-display: swap;
+  src: url(../assets/fonts/bodoni-moda-normal-latin-ext.woff2) format('woff2');
+  unicode-range: U+0100-02BA, U+02BD-02C5, U+02C7-02CC, U+02CE-02D7, U+02DD-02FF, U+0304, U+0308, U+0329, U+1D00-1DBF, U+1E00-1E9F, U+1EF2-1EFF, U+2020, U+20A0-20AB, U+20AD-20C4, U+2113, U+2C60-2C7F, U+A720-A7FF;
+}
+@font-face {
+  font-family: 'Bodoni Moda';
+  font-style: normal;
+  font-weight: 400 700;
+  font-display: swap;
+  src: url(../assets/fonts/bodoni-moda-normal-latin.woff2) format('woff2');
+  unicode-range: U+0000-00FF, U+0131, U+0152-0153, U+02BB-02BC, U+02C6, U+02DA, U+02DC, U+0304, U+0308, U+0329, U+2000-206F, U+20AC, U+2122, U+2191, U+2193, U+2212, U+2215, U+FEFF, U+FFFD;
+}
+@font-face {
+  font-family: 'Instrument Sans';
+  font-style: italic;
+  font-weight: 400 700;
+  font-stretch: 100%;
+  font-display: swap;
+  src: url(../assets/fonts/instrument-sans-italic-latin-ext.woff2) format('woff2');
+  unicode-range: U+0100-02BA, U+02BD-02C5, U+02C7-02CC, U+02CE-02D7, U+02DD-02FF, U+0304, U+0308, U+0329, U+1D00-1DBF, U+1E00-1E9F, U+1EF2-1EFF, U+2020, U+20A0-20AB, U+20AD-20C4, U+2113, U+2C60-2C7F, U+A720-A7FF;
+}
+@font-face {
+  font-family: 'Instrument Sans';
+  font-style: italic;
+  font-weight: 400 700;
+  font-stretch: 100%;
+  font-display: swap;
+  src: url(../assets/fonts/instrument-sans-italic-latin.woff2) format('woff2');
+  unicode-range: U+0000-00FF, U+0131, U+0152-0153, U+02BB-02BC, U+02C6, U+02DA, U+02DC, U+0304, U+0308, U+0329, U+2000-206F, U+20AC, U+2122, U+2191, U+2193, U+2212, U+2215, U+FEFF, U+FFFD;
+}
+@font-face {
+  font-family: 'Instrument Sans';
+  font-style: normal;
+  font-weight: 400 700;
+  font-stretch: 100%;
+  font-display: swap;
+  src: url(../assets/fonts/instrument-sans-normal-latin-ext.woff2) format('woff2');
+  unicode-range: U+0100-02BA, U+02BD-02C5, U+02C7-02CC, U+02CE-02D7, U+02DD-02FF, U+0304, U+0308, U+0329, U+1D00-1DBF, U+1E00-1E9F, U+1EF2-1EFF, U+2020, U+20A0-20AB, U+20AD-20C4, U+2113, U+2C60-2C7F, U+A720-A7FF;
+}
+@font-face {
+  font-family: 'Instrument Sans';
+  font-style: normal;
+  font-weight: 400 700;
+  font-stretch: 100%;
+  font-display: swap;
+  src: url(../assets/fonts/instrument-sans-normal-latin.woff2) format('woff2');
+  unicode-range: U+0000-00FF, U+0131, U+0152-0153, U+02BB-02BC, U+02C6, U+02DA, U+02DC, U+0304, U+0308, U+0329, U+2000-206F, U+20AC, U+2122, U+2191, U+2193, U+2212, U+2215, U+FEFF, U+FFFD;
+}
+@font-face {
+  font-family: 'JetBrains Mono';
+  font-style: italic;
+  font-weight: 400;
+  font-display: swap;
+  src: url(../assets/fonts/jetbrains-mono-italic-greek.woff2) format('woff2');
+  unicode-range: U+0370-0377, U+037A-037F, U+0384-038A, U+038C, U+038E-03A1, U+03A3-03FF;
+}
+@font-face {
+  font-family: 'JetBrains Mono';
+  font-style: italic;
+  font-weight: 400;
+  font-display: swap;
+  src: url(../assets/fonts/jetbrains-mono-italic-latin-ext.woff2) format('woff2');
+  unicode-range: U+0100-02BA, U+02BD-02C5, U+02C7-02CC, U+02CE-02D7, U+02DD-02FF, U+0304, U+0308, U+0329, U+1D00-1DBF, U+1E00-1E9F, U+1EF2-1EFF, U+2020, U+20A0-20AB, U+20AD-20C4, U+2113, U+2C60-2C7F, U+A720-A7FF;
+}
+@font-face {
+  font-family: 'JetBrains Mono';
+  font-style: italic;
+  font-weight: 400;
+  font-display: swap;
+  src: url(../assets/fonts/jetbrains-mono-italic-latin.woff2) format('woff2');
+  unicode-range: U+0000-00FF, U+0131, U+0152-0153, U+02BB-02BC, U+02C6, U+02DA, U+02DC, U+0304, U+0308, U+0329, U+2000-206F, U+20AC, U+2122, U+2191, U+2193, U+2212, U+2215, U+FEFF, U+FFFD;
+}
+@font-face {
+  font-family: 'JetBrains Mono';
+  font-style: normal;
+  font-weight: 400 700;
+  font-display: swap;
+  src: url(../assets/fonts/jetbrains-mono-normal-greek.woff2) format('woff2');
+  unicode-range: U+0370-0377, U+037A-037F, U+0384-038A, U+038C, U+038E-03A1, U+03A3-03FF;
+}
+@font-face {
+  font-family: 'JetBrains Mono';
+  font-style: normal;
+  font-weight: 400 700;
+  font-display: swap;
+  src: url(../assets/fonts/jetbrains-mono-normal-latin-ext.woff2) format('woff2');
+  unicode-range: U+0100-02BA, U+02BD-02C5, U+02C7-02CC, U+02CE-02D7, U+02DD-02FF, U+0304, U+0308, U+0329, U+1D00-1DBF, U+1E00-1E9F, U+1EF2-1EFF, U+2020, U+20A0-20AB, U+20AD-20C4, U+2113, U+2C60-2C7F, U+A720-A7FF;
+}
+@font-face {
+  font-family: 'JetBrains Mono';
+  font-style: normal;
+  font-weight: 400 700;
+  font-display: swap;
+  src: url(../assets/fonts/jetbrains-mono-normal-latin.woff2) format('woff2');
+  unicode-range: U+0000-00FF, U+0131, U+0152-0153, U+02BB-02BC, U+02C6, U+02DA, U+02DC, U+0304, U+0308, U+0329, U+2000-206F, U+20AC, U+2122, U+2191, U+2193, U+2212, U+2215, U+FEFF, U+FFFD;
+}
+@font-face {
+  font-family: 'Noto Sans Math';
+  font-style: normal;
+  font-weight: 400;
+  font-display: swap;
+  src: url(../assets/fonts/noto-sans-math-normal-subset.woff2) format('woff2');
+}
+@font-face {
+  font-family: 'Noto Sans Mono';
+  font-style: normal;
+  font-weight: 400;
+  font-stretch: 100%;
+  font-display: swap;
+  src: url(../assets/fonts/noto-sans-mono-normal-subset.woff2) format('woff2');
+  unicode-range: U+2b, U+3c-3e, U+7c, U+ac, U+338, U+2032, U+2102, U+2112, U+2200, U+2203-2204, U+2208-2209, U+2211-2212, U+2216, U+221a, U+2227-2228, U+222a, U+2260, U+2264-2265, U+226e-2271, U+2286, U+2288, U+2295, U+2297, U+27e8-27e9;
+}
+:root {
+  --paper: #F5F5F0;
+  --paper-deep: #EAEAE3;
+  --paper-lift: #FBFBF8;
+  --ink: #1A1C21;
+  --ink-2: #444851;
+  --ink-3: #5C6068;
+  --rule: #D3D3CA;
+  --control: #82858A;
+  --accent: #0B6B55;
+  --accent-wash: rgba(11, 107, 85, .10);
+  --fail: #A3262F;
+  --on-ink: #F5F5F0;
+
+  --serif: "Bodoni Moda", "Bodoni 72", Didot, "Noto Serif Display", Georgia, serif;
+  --math: "Noto Sans Math", "Bodoni Moda", "STIX Two Text", Cambria, "DejaVu Serif", Georgia, "STIX Two Math", "Cambria Math", serif;
+  --sans: "Instrument Sans", "Helvetica Neue", Helvetica, Arial, system-ui, sans-serif;
+  --mono: "JetBrains Mono", "Noto Sans Mono", ui-monospace, SFMono-Regular, Menlo, Consolas, monospace;
+
+  --measure: 40rem;
+  --side: 16.5rem;
+  --gutter: clamp(16px, 4vw, 48px);
+  color-scheme: light;
+}
+@media (prefers-color-scheme: dark) {
+  :root:not([data-theme="light"]) {
+    --paper: #13171D;
+    --paper-deep: #1C2129;
+    --paper-lift: #171C23;
+    --ink: #E9E7E0;
+    --ink-2: #BEBCB5;
+    --ink-3: #9D9C96;
+    --rule: #2F3641;
+    --control: #6E6F6D;
+    --accent: #6CCBAA;
+    --accent-wash: rgba(108, 203, 170, .12);
+    --fail: #F2958F;
+    --on-ink: #13171D;
+    color-scheme: dark;
+  }
+}
+:root[data-theme="dark"] {
+  --paper: #13171D;
+  --paper-deep: #1C2129;
+  --paper-lift: #171C23;
+  --ink: #E9E7E0;
+  --ink-2: #BEBCB5;
+  --ink-3: #9D9C96;
+  --rule: #2F3641;
+  --control: #6E6F6D;
+  --accent: #6CCBAA;
+  --accent-wash: rgba(108, 203, 170, .12);
+  --fail: #F2958F;
+  --on-ink: #13171D;
+  color-scheme: dark;
+}
+
+*, *::before, *::after { box-sizing: border-box; }
+[hidden] { display: none !important; }
+html { -webkit-text-size-adjust: 100%; }
+body {
+  margin: 0;
+  background: var(--paper);
+  color: var(--ink);
+  font: 400 1rem/1.6 var(--sans);
+  overflow-wrap: break-word;
+}
+a { color: inherit; text-decoration-color: var(--accent); text-underline-offset: .18em; }
+a:hover { color: var(--accent); }
+:focus-visible { outline: 2px solid var(--accent); outline-offset: 2px; }
+code, kbd, pre, textarea { font-family: var(--mono); font-size: .875rem; font-variant-ligatures: none; }
+.wrap { max-width: 1240px; margin-inline: auto; padding-inline: var(--gutter); }
+.skip { position: absolute; left: -999px; }
+.skip:focus { left: 1rem; top: .5rem; z-index: 10; background: var(--paper-lift); padding: .5rem .75rem; }
+
+/* Masthead */
+.masthead { position: sticky; top: 0; z-index: 5; background: var(--paper); border-bottom: 1px solid var(--rule); }
+.masthead .wrap { display: flex; align-items: center; gap: 1.25rem; height: 3.5rem; }
+.wordmark { font: italic 400 1.45rem/1 var(--serif); text-decoration: none; color: var(--ink); }
+.crumb { color: var(--ink-2); font-size: .9375rem; }
+.masthead .links { margin-left: auto; display: flex; align-items: center; gap: 1.25rem; font-size: .9375rem; }
+.masthead .links a { text-decoration: none; color: var(--ink-2); }
+.masthead .links a:hover { color: var(--ink); text-decoration: underline; text-decoration-color: var(--accent); }
+.theme { flex: none; display: inline-grid; place-items: center; width: 2.25rem; height: 2.25rem; padding: 0; color: var(--ink-2); background: none; border: 1px solid var(--control); border-radius: 2px; cursor: pointer; }
+.theme svg { width: 1.05rem; height: 1.05rem; }
+
+/* Intro */
+.intro { padding-block: clamp(1.75rem, 4vw, 3rem) 1.25rem; }
+.intro h1 { margin: 0; font: 400 clamp(2.4rem, 6vw, 3.6rem)/1.05 var(--serif); letter-spacing: -.01em; }
+.intro p { margin: .75rem 0 0; max-width: 46rem; color: var(--ink-2); }
+.intro .meta { font-size: .875rem; color: var(--ink-3); }
+
+/* Toolbar */
+.toolbar { display: flex; flex-wrap: wrap; align-items: end; gap: .75rem 1.25rem; padding-block: 1rem; border-top: 1px solid var(--rule); }
+.field { display: grid; gap: .3rem; }
+.field > span, .legend { font-size: .8125rem; color: var(--ink-3); letter-spacing: .02em; }
+select {
+  font: inherit; font-size: .9375rem; color: var(--ink); background: var(--paper-lift);
+  border: 1px solid var(--control); border-radius: 2px; padding: .45rem 2rem .45rem .6rem; min-height: 2.5rem;
+  appearance: none; background-image: linear-gradient(45deg, transparent 50%, currentColor 50%), linear-gradient(135deg, currentColor 50%, transparent 50%);
+  background-position: calc(100% - 15px) 55%, calc(100% - 10px) 55%; background-size: 5px 5px; background-repeat: no-repeat;
+}
+fieldset.modes { border: 0; margin: 0; padding: 0; display: grid; gap: .3rem; }
+.seg { display: inline-flex; border: 1px solid var(--control); border-radius: 2px; overflow: hidden; }
+.seg label { position: relative; }
+.seg input { position: absolute; opacity: 0; inset: 0; margin: 0; cursor: pointer; }
+.seg span { display: block; padding: .45rem .8rem; min-height: 2.5rem; line-height: 1.5rem; font-family: var(--mono); font-size: .875rem; color: var(--ink-2); }
+.seg label + label span { border-left: 1px solid var(--control); }
+.seg input:checked + span { background: var(--ink); color: var(--on-ink); }
+.seg input:focus-visible + span { outline: 2px solid var(--accent); outline-offset: -4px; }
+.check { display: inline-flex; align-items: center; gap: .45rem; min-height: 2.5rem; font-family: var(--mono); font-size: .875rem; color: var(--ink-2); }
+.check input { width: 1.05rem; height: 1.05rem; accent-color: var(--accent); }
+.actions { margin-left: auto; display: flex; align-items: center; gap: .6rem; }
+.btn {
+  font: 600 .9375rem/1 var(--sans); padding: 0 1.15rem; min-height: 2.75rem; border-radius: 2px; cursor: pointer;
+  border: 1px solid var(--ink); background: var(--ink); color: var(--on-ink);
+}
+.btn:hover:not(:disabled) { background: var(--accent); border-color: var(--accent); color: var(--on-ink); }
+.btn.quiet { background: none; color: var(--ink); border-color: var(--control); font-weight: 500; }
+.btn.quiet:hover:not(:disabled) { color: var(--ink); background: var(--paper-deep); border-color: var(--ink-2); }
+.btn:disabled { opacity: .5; cursor: not-allowed; }
+kbd { font-size: .75rem; border: 1px solid var(--rule); border-bottom-width: 2px; border-radius: 3px; padding: 0 .3rem; color: var(--ink-3); }
+.btn kbd { margin-left: .5rem; color: inherit; border-color: currentColor; opacity: .7; font-weight: 400; white-space: nowrap; }
+@media (pointer: coarse), (max-width: 640px) { .btn kbd { display: none; } }
+
+/* Workspace */
+.workspace { display: grid; grid-template-columns: minmax(0, 1.15fr) minmax(0, 1fr); gap: 1.25rem; padding-bottom: 2.5rem; }
+.panel { display: flex; flex-direction: column; min-width: 0; border: 1px solid var(--rule); background: var(--paper-lift); border-radius: 2px; }
+.panel-head { display: flex; align-items: center; gap: .75rem; min-height: 2.75rem; padding: 0 .75rem; border-bottom: 1px solid var(--rule); background: var(--paper-deep); }
+.panel-title { font-size: .8125rem; color: var(--ink-3); letter-spacing: .02em; }
+.tabs { display: flex; gap: 0; overflow-x: auto; margin-inline: -.75rem; scrollbar-width: thin; }
+.tabs button {
+  flex: none; font: 500 .8125rem/1 var(--mono); color: var(--ink-2); background: none; border: 0; border-right: 1px solid var(--rule);
+  padding: 0 .9rem; min-height: 2.75rem; cursor: pointer;
+}
+.tabs button[aria-selected="true"] { color: var(--ink); background: var(--paper-lift); box-shadow: inset 0 -2px 0 var(--accent); }
+.editor {
+  display: block; width: 100%; flex: 1; min-height: 24rem; resize: vertical; margin: 0; border: 0; padding: .9rem 1rem;
+  background: transparent; color: var(--ink); line-height: 1.6; tab-size: 4; white-space: pre; overflow: auto;
+}
+.editor:focus-visible { outline-offset: -2px; }
+.cmd { margin: 0; padding: .6rem 1rem; border-top: 1px solid var(--rule); color: var(--ink-2); white-space: pre-wrap; word-break: break-all; }
+.cmd .pr { color: var(--ink-3); user-select: none; }
+.output { flex: 1; margin: 0; padding: .9rem 1rem; min-height: 24rem; overflow: auto; white-space: pre-wrap; word-break: break-word; line-height: 1.6; }
+.output .err { color: var(--fail); }
+.output .ok { color: var(--accent); font-weight: 600; }
+.output .bad { color: var(--fail); font-weight: 600; }
+.output .muted { color: var(--ink-3); }
+.status { margin-left: auto; font-size: .8125rem; color: var(--ink-3); }
+.status.busy::before { content: ""; display: inline-block; width: .55rem; height: .55rem; margin-right: .4rem; border-radius: 50%; background: var(--accent); animation: pulse 1s ease-in-out infinite alternate; }
+@keyframes pulse { from { opacity: .25; } to { opacity: 1; } }
+
+.notes { padding-block: 0 3rem; color: var(--ink-2); font-size: .9375rem; }
+.notes::before { content: ""; display: block; border-top: 1px solid var(--rule); margin-bottom: 1.5rem; }
+.notes h2 { font: 400 1.5rem/1.2 var(--serif); color: var(--ink); margin: 0 0 .75rem; }
+.notes ul { margin: 0; padding-left: 1.1rem; max-width: 48rem; }
+.notes li + li { margin-top: .4rem; }
+.noscript { padding: 1rem; border: 1px solid var(--fail); color: var(--fail); }
+
+@media (max-width: 900px) {
+  .workspace { grid-template-columns: minmax(0, 1fr); }
+  .editor { min-height: 18rem; }
+  .output { min-height: 12rem; }
+}
+@media (max-width: 640px) {
+  .masthead .crumb { display: none; }
+  .actions { margin-left: 0; width: 100%; }
+  .actions .btn { flex: 1; }
+}
+@media (prefers-reduced-motion: reduce) {
+  .status.busy::before { animation: none; }
+}
diff --git a/site/playground/playground.js b/site/playground/playground.js
new file mode 100644
index 000000000..90a9ff53e
--- /dev/null
+++ b/site/playground/playground.js
@@ -0,0 +1,240 @@
+import { EXAMPLES } from './examples.js';
+
+const $ = (id) => document.getElementById(id);
+const els = {
+  example: $('example'), tabs: $('tabs'), editor: $('editor'), cmd: $('cmd'), output: $('output'),
+  status: $('status'), run: $('run'), stop: $('stop'), reset: $('reset'), toolbar: $('toolbar'),
+  loopsum: $('loopsum'), loopsumWrap: $('loopsum-wrap'), version: $('version'),
+};
+
+// Files each command reads, in argument order.
+const MODES = {
+  ver: ['pre.hsl', 'circuit.qasm', 'post.hsl'],
+  ex: ['pre.hsl', 'circuit.qasm'],
+  eq: ['a.qasm', 'b.qasm'],
+};
+// ver and ex run one circuit on a set of states and share a workspace; eq
+// compares two circuits and has its own files and examples. Each workspace
+// keeps its edits while the other one is shown.
+const kind = (mode) => (mode === 'eq' ? 'eq' : 'circuit');
+
+const state = { mode: 'ver', workspaces: {} };
+const ws = () => state.workspaces[kind(state.mode)];
+
+// ---------- theme toggle (shared with the landing page) ----------
+(function theme() {
+  const btn = document.querySelector('.theme');
+  if (!btn) return;
+  const root = document.documentElement;
+  const current = () => root.getAttribute('data-theme')
+    || (matchMedia('(prefers-color-scheme: dark)').matches ? 'dark' : 'light');
+  const label = () => btn.setAttribute('aria-label', current() === 'dark' ? 'Switch to light theme' : 'Switch to dark theme');
+  btn.hidden = false;
+  label();
+  btn.addEventListener('click', () => {
+    const next = current() === 'dark' ? 'light' : 'dark';
+    root.setAttribute('data-theme', next);
+    try { localStorage.setItem('autoq-theme', next); } catch (e) { /* storage unavailable */ }
+    label();
+  });
+})();
+
+// ---------- examples, tabs, editor ----------
+// Loads an example into its workspace. Within the same workspace the command
+// stays as it is (an ex run can switch examples); otherwise it becomes the
+// example's own command.
+function loadExample(id) {
+  const ex = EXAMPLES.find((e) => e.id === id) ?? EXAMPLES[0];
+  state.workspaces[kind(ex.mode)] = { example: ex, files: ex.files.map((f) => ({ ...f })), active: 0 };
+  showMode(kind(ex.mode) === kind(state.mode) ? state.mode : ex.mode);
+}
+
+function setMode(mode) {
+  if (!state.workspaces[kind(mode)]) {
+    const first = EXAMPLES.find((e) => kind(e.mode) === kind(mode));
+    state.workspaces[kind(mode)] = { example: first, files: first.files.map((f) => ({ ...f })), active: 0 };
+  }
+  showMode(mode);
+}
+
+function showMode(mode) {
+  state.mode = mode;
+  els.toolbar.querySelector(`input[name="mode"][value="${mode}"]`).checked = true;
+  els.loopsumWrap.hidden = mode === 'eq';
+  els.example.replaceChildren(...EXAMPLES
+    .filter((e) => kind(e.mode) === kind(mode))
+    .map((e) => new Option(e.title, e.id)));
+  els.example.value = ws().example.id;
+  render();
+}
+
+function args() {
+  const a = [state.mode];
+  if (state.mode !== 'eq' && els.loopsum.checked) a.push('--loopsum');
+  return a.concat(MODES[state.mode]);
+}
+
+function render() {
+  const { files, active } = ws();
+  els.tabs.replaceChildren(...files.map((f, i) => {
+    const b = document.createElement('button');
+    b.type = 'button';
+    b.role = 'tab';
+    b.id = `tab-${i}`;
+    b.textContent = f.name;
+    b.setAttribute('aria-selected', String(i === active));
+    b.setAttribute('aria-controls', 'editor');
+    b.tabIndex = i === active ? 0 : -1;
+    b.addEventListener('click', () => select(i));
+    return b;
+  }));
+  els.editor.value = files[active].content;
+  els.editor.setAttribute('aria-labelledby', `tab-${active}`);
+  els.cmd.innerHTML = '$ ' + escapeHtml(['autoq', ...args()].join(' '));
+}
+
+function select(i, focus = false) {
+  ws().active = i;
+  render();
+  if (focus) document.getElementById(`tab-${i}`).focus();
+}
+
+els.tabs.addEventListener('keydown', (e) => {
+  const { files, active } = ws();
+  const n = files.length;
+  const moves = { ArrowRight: 1, ArrowLeft: n - 1 };
+  if (e.key in moves) { e.preventDefault(); select((active + moves[e.key]) % n, true); }
+  else if (e.key === 'Home') { e.preventDefault(); select(0, true); }
+  else if (e.key === 'End') { e.preventDefault(); select(n - 1, true); }
+});
+els.editor.addEventListener('input', () => { ws().files[ws().active].content = els.editor.value; });
+els.example.addEventListener('change', () => loadExample(els.example.value));
+els.toolbar.addEventListener('change', (e) => {
+  if (e.target.name === 'mode') setMode(e.target.value);
+  if (e.target === els.loopsum) render();
+});
+els.reset.addEventListener('click', () => loadExample(ws().example.id));
+
+// ---------- running ----------
+let worker = null;
+let ready = false;
+let running = false;
+let timer = 0;
+
+function startWorker() {
+  ready = false;
+  worker = new Worker(new URL('./worker.js', import.meta.url), { type: 'module' });
+  worker.onmessage = onMessage;
+  worker.onerror = (e) => {
+    setStatus('');
+    els.version.textContent = 'AutoQ could not be loaded in this browser.';
+    show([{ stream: 'err', line: `Could not load AutoQ: ${e.message || 'unknown error'}` }]);
+  };
+  setStatus('Downloading AutoQ…', true);
+  worker.postMessage({ type: 'warmup' });
+}
+
+let versionPending = false;
+function onMessage({ data }) {
+  if (data.type === 'ready') {
+    if (!els.version.dataset.done) {
+      // Ask for the version first; Run is enabled once it answers.
+      versionPending = true;
+      worker.postMessage({ args: ['-v'], files: [] });
+    } else {
+      markReady();
+    }
+    return;
+  }
+  if (versionPending) {
+    versionPending = false;
+    const v = (data.out ?? []).map((o) => o.line).join(' ').trim();
+    els.version.dataset.done = '1';
+    if (/^[0-9a-f]{40}$/.test(v)) {
+      const a = document.createElement('a');
+      a.href = `https://github.com/fmlab-iis/AutoQ/commit/${v}`;
+      a.textContent = v.slice(0, 9);
+      els.version.replaceChildren('AutoQ at commit ', a, ', compiled to WebAssembly.');
+    } else {
+      els.version.textContent = v ? `AutoQ ${v}, compiled to WebAssembly.` : 'AutoQ, compiled to WebAssembly.';
+    }
+    markReady();
+    return;
+  }
+  if (!running) return;
+  running = false;
+  clearInterval(timer);
+  els.run.disabled = false;
+  els.stop.disabled = true;
+  const secs = (data.ms / 1000).toFixed(2);
+  if (data.type === 'error') {
+    show([...data.out, { stream: 'err', line: `AutoQ stopped unexpectedly: ${data.message}` }]);
+    setStatus(`Error after ${secs}s`);
+  } else {
+    show(data.out, `exit code ${data.code} · ${secs}s in the browser`);
+    setStatus(`Finished in ${secs}s`);
+  }
+}
+
+function markReady() {
+  ready = true;
+  setStatus('Ready');
+  els.run.disabled = false;
+}
+
+function run() {
+  if (!ready || running) return;
+  running = true;
+  els.run.disabled = true;
+  els.stop.disabled = false;
+  show([]);
+  const t0 = performance.now();
+  setStatus('Running… 0.0s', true);
+  timer = setInterval(() => setStatus(`Running… ${((performance.now() - t0) / 1000).toFixed(1)}s`, true), 100);
+  worker.postMessage({ args: args(), files: ws().files });
+}
+
+function stop() {
+  if (!running) return;
+  running = false;
+  clearInterval(timer);
+  worker.terminate();
+  els.stop.disabled = true;
+  els.run.disabled = true;
+  show([{ stream: 'err', line: 'Stopped.' }]);
+  startWorker();
+}
+
+els.toolbar.addEventListener('submit', (e) => { e.preventDefault(); run(); });
+els.stop.addEventListener('click', stop);
+document.addEventListener('keydown', (e) => {
+  if (e.key === 'Enter' && (e.ctrlKey || e.metaKey)) { e.preventDefault(); run(); }
+});
+
+// ---------- output ----------
+function escapeHtml(s) {
+  return s.replace(/[&<>"]/g, (c) => ({ '&': '&', '<': '<', '>': '>', '"': '"' }[c]));
+}
+function highlight(line) {
+  return escapeHtml(line)
+    .replace(/\[OK\]|\[equal\]/g, (m) => `${m}`)
+    .replace(/\[failed\]|\[unequal\]|\[ERROR\]/g, (m) => `${m}`);
+}
+function show(lines, footer) {
+  const html = lines.map((o) => o.stream === 'err'
+    ? `${highlight(o.line)}`
+    : highlight(o.line));
+  if (footer) html.push(`\n${escapeHtml(footer)}`);
+  els.output.innerHTML = html.join('\n');
+}
+function setStatus(text, busy = false) {
+  els.status.textContent = text;
+  els.status.classList.toggle('busy', busy);
+}
+
+// ---------- start ----------
+loadExample(new URLSearchParams(location.search).get('example') ?? EXAMPLES[0].id);
+if (typeof WebAssembly === 'object') startWorker();
+else {
+  els.version.textContent = 'This browser does not support WebAssembly.';
+}
diff --git a/site/playground/worker.js b/site/playground/worker.js
new file mode 100644
index 000000000..189508e69
--- /dev/null
+++ b/site/playground/worker.js
@@ -0,0 +1,56 @@
+// Runs AutoQ (compiled to WebAssembly by wasm/build.sh) off the main thread.
+// Message in:  { args: string[], files: {name, content}[] }
+// Messages out: { type: 'ready' } once the module is compiled,
+//               { type: 'done', code, out, ms } or { type: 'error', message, out, ms }.
+import createAutoQ from './autoq.js';
+
+const WASM_URL = new URL('./autoq.wasm', import.meta.url);
+let compiled = null;
+
+async function compile() {
+  if (compiled) return compiled;
+  try {
+    compiled = await WebAssembly.compileStreaming(fetch(WASM_URL));
+  } catch {
+    // Some servers send .wasm without the application/wasm type.
+    const bytes = await (await fetch(WASM_URL)).arrayBuffer();
+    compiled = await WebAssembly.compile(bytes);
+  }
+  return compiled;
+}
+
+self.onmessage = async ({ data }) => {
+  if (data.type === 'warmup') {
+    try { await compile(); self.postMessage({ type: 'ready' }); }
+    catch (e) { self.postMessage({ type: 'error', message: String(e?.message ?? e), out: [], ms: 0 }); }
+    return;
+  }
+  const { args, files } = data;
+  const out = [];
+  const t0 = performance.now();
+  try {
+    const wasmModule = await compile();
+    // A fresh instance per run: main() keeps global state between calls.
+    const mod = await createAutoQ({
+      instantiateWasm(imports, done) {
+        WebAssembly.instantiate(wasmModule, imports).then((instance) => done(instance, wasmModule));
+        return {};
+      },
+      print: (line) => out.push({ stream: 'out', line }),
+      printErr: (line) => out.push({ stream: 'err', line }),
+    });
+    mod.FS.mkdir('/work');
+    mod.FS.chdir('/work');
+    for (const f of files) mod.FS.writeFile(f.name, f.content);
+    let code;
+    try {
+      code = mod.callMain(args);
+    } catch (e) {
+      if (e && e.name === 'ExitStatus') code = e.status;
+      else throw e;
+    }
+    self.postMessage({ type: 'done', code, out, ms: performance.now() - t0 });
+  } catch (e) {
+    self.postMessage({ type: 'error', message: String(e?.message ?? e), out, ms: performance.now() - t0 });
+  }
+};
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 833a55afd..c30b268ae 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -8,8 +8,11 @@ project(autoq)
 # Export compile commands to be used with YouCompleteMe
 set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
 
-# Library-only: -fPIC (common flags from parent)
-set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fPIC")
+# Library-only: -fPIC (common flags from parent). Not used for the
+# WebAssembly build, which links everything statically.
+if (NOT EMSCRIPTEN)
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fPIC")
+endif ()
 
 # uncomment for profiling
 #add_definitions(-pg)
@@ -30,7 +33,10 @@ set_source_files_properties(${Extended_Dirac_SOURCE_FILES} PROPERTIES COMPILE_FL
 ##############################################################################
 
 # USE_SYSTEM_Z3 is defined in the parent CMakeLists.txt (change OFF to ON there to use system Z3).
-if (APPLE)
+if (EMSCRIPTEN)
+    # WebAssembly build (wasm/build.sh): a static Z3 built with Emscripten.
+    target_link_libraries(lsta "${AUTOQ_WASM_Z3_LIB}")
+elseif (APPLE)
     target_link_libraries(lsta "${CMAKE_CURRENT_SOURCE_DIR}/../libz3.a")
 elseif (UNIX)
     if (USE_SYSTEM_Z3)
@@ -51,7 +57,10 @@ include_directories(../include/z3)
 ##############################################################################
 #                              DEPENDENCIES - ANTLR
 ##############################################################################
-if (APPLE)
+if (EMSCRIPTEN)
+    # WebAssembly build (wasm/build.sh): a static ANTLR4 runtime built with Emscripten.
+    target_link_libraries(lsta "${AUTOQ_WASM_ANTLR4_LIB}")
+elseif (APPLE)
     execute_process(
         COMMAND brew --prefix antlr4-cpp-runtime
         OUTPUT_VARIABLE ANTLR4_CPP_RUNTIME_PREFIX
diff --git a/src/util/memory.cpp b/src/util/memory.cpp
index de3034615..a94148e76 100755
--- a/src/util/memory.cpp
+++ b/src/util/memory.cpp
@@ -13,7 +13,10 @@ size_t peakSize    = AUTOQ::Util::getPeakRSS();
 
 #include "autoq/util/util.hh"
 
-#if defined(_WIN32)
+#if defined(__EMSCRIPTEN__)
+#include 
+
+#elif defined(_WIN32)
 #include 
 #include 
 
@@ -45,7 +48,14 @@ size_t peakSize    = AUTOQ::Util::getPeakRSS();
  */
 size_t AUTOQ::Util::getPeakRSS()
 {
-#if defined(_WIN32)
+#if defined(__EMSCRIPTEN__)
+    /* WebAssembly ---------------------------------------------- */
+    /* The linear memory only grows, so its size is both the current
+     * and the peak footprint. (Emscripten's getrusage() does not fill in
+     * ru_maxrss.) */
+    return emscripten_get_heap_size();
+
+#elif defined(_WIN32)
     /* Windows -------------------------------------------------- */
     PROCESS_MEMORY_COUNTERS info;
     GetProcessMemoryInfo( GetCurrentProcess( ), &info, sizeof(info) );
@@ -91,7 +101,14 @@ size_t AUTOQ::Util::getPeakRSS()
  */
 size_t AUTOQ::Util::getCurrentRSS()
 {
-#if defined(_WIN32)
+#if defined(__EMSCRIPTEN__)
+    /* WebAssembly ---------------------------------------------- */
+    /* The linear memory only grows, so its size is both the current
+     * and the peak footprint. (Emscripten's getrusage() does not fill in
+     * ru_maxrss.) */
+    return emscripten_get_heap_size();
+
+#elif defined(_WIN32)
     /* Windows -------------------------------------------------- */
     PROCESS_MEMORY_COUNTERS info;
     GetProcessMemoryInfo( GetCurrentProcess( ), &info, sizeof(info) );
diff --git a/wasm/README.md b/wasm/README.md
new file mode 100644
index 000000000..efac443ba
--- /dev/null
+++ b/wasm/README.md
@@ -0,0 +1,89 @@
+# AutoQ in the browser (WebAssembly)
+
+`wasm/build.sh` compiles the AutoQ command-line tool to WebAssembly with
+[Emscripten](https://emscripten.org). The result, `autoq.js` and `autoq.wasm`,
+powers the playground at `site/playground/`, which runs AutoQ entirely in the
+browser. It is the same `main()` as the native CLI, so it accepts the same
+arguments and files and prints the same output.
+
+## Building
+
+You need an activated [emsdk](https://emscripten.org/docs/getting_started/downloads.html)
+(tested with 6.0.12), `git`, `python3`, and the Boost headers (for example
+`apt install libboost-dev`).
+
+```sh
+git clone https://github.com/emscripten-core/emsdk.git ~/emsdk
+~/emsdk/emsdk install 6.0.12 && ~/emsdk/emsdk activate 6.0.12
+source ~/emsdk/emsdk_env.sh
+
+wasm/build.sh            # writes site/playground/autoq.js and autoq.wasm
+```
+
+The first run builds Z3 4.12.5 and the ANTLR 4.13.2 C++ runtime as static
+WebAssembly libraries in `build-wasm/deps/` and takes a while. Later runs reuse
+them and only rebuild AutoQ. Both versions match the headers bundled in
+`include/z3` and `include/antlr4-runtime`.
+
+Environment variables: `AUTOQ_WASM_DEPS` (dependency cache, default
+`build-wasm/deps`), `AUTOQ_WASM_BUILD` (AutoQ build directory, default
+`build-wasm/autoq`), `BOOST_INCLUDE_DIR` (default `/usr/include`) and `JOBS`.
+An optional argument sets the output directory.
+
+## Trying it locally
+
+```sh
+python3 -m http.server -d site 8000
+# open http://localhost:8000/playground/
+```
+
+The page needs to be served over HTTP: browsers don't load module workers
+from `file://` URLs.
+
+## Checking it against the native build
+
+```sh
+node wasm/compare.mjs build/cli/autoq site/playground
+```
+
+This runs every playground example (`site/playground/examples.js`) with the
+native `autoq` and with the WebAssembly build and checks that both print the
+same output and exit code, ignoring the timing and memory figures. Set
+`VERBOSE=1` to see the outputs.
+
+## How it fits together
+
+- **CMake.** When configured with `emcmake`, the root `CMakeLists.txt` takes
+  Boost from `AUTOQ_WASM_BOOST_INCLUDE` (only header-only parts are used) and
+  skips the unit tests; `src/CMakeLists.txt` links the prebuilt Z3 and ANTLR
+  libraries; `cli/CMakeLists.txt` links `autoq` as an ES module that exports
+  `createAutoQ()` and does not run `main()` on load. The native build is
+  unchanged.
+- **The page.** `site/playground/worker.js` compiles `autoq.wasm` once, then
+  creates a fresh instance for every run (`main()` keeps global state), writes
+  the files into the in-memory file system and calls `main()` through
+  `callMain([...args])`. The page itself never blocks, and Stop simply
+  terminates the worker.
+- **Deployment.** `.github/workflows/pages.yml` installs emsdk, restores the
+  cached Z3 and ANTLR build, runs `wasm/build.sh` and deploys `site/`. The
+  generated `autoq.js` and `autoq.wasm` are not committed.
+
+## Differences from the native build
+
+- WebAssembly has no floating-point traps, so the `feenableexcept()` call in
+  `cli/autoq.cc` is skipped: an arithmetic error that stops the native tool
+  with `SIGFPE` produces `inf` or `NaN` here instead.
+- The reported memory usage is the size of the WebAssembly heap, which only
+  grows; Emscripten does not report a resident set size.
+- Runs are single-threaded and limited to the memory a browser grants a page
+  (at most 4 GB), so the largest benchmarks are better run natively.
+- Source paths in error messages are relative to the repository root.
+
+## Patches to Z3
+
+`wasm/build.sh` patches three lines of Z3 4.12.5 after cloning it. They are
+uses of nonexistent members (`get`, `m_low_bound`,
+`get_value_of_column_cell`) in templates that are never instantiated; GCC and
+older clang accept them, the clang in current Emscripten does not. Later Z3
+releases contain the same fixes. Drop the patches if you move to a newer Z3,
+and update `Z3_TAG` together with `include/z3`.
diff --git a/wasm/build.sh b/wasm/build.sh
new file mode 100755
index 000000000..83ad91eeb
--- /dev/null
+++ b/wasm/build.sh
@@ -0,0 +1,90 @@
+#!/usr/bin/env bash
+# Build AutoQ for WebAssembly with Emscripten.
+#
+# Usage:   wasm/build.sh [OUT_DIR]          (default OUT_DIR: site/playground)
+# Needs:   an activated emsdk (emcc/emcmake on PATH; tested with 6.0.12), git, python3, and the
+#          Boost headers (BOOST_INCLUDE_DIR, default /usr/include).
+# Env:     AUTOQ_WASM_DEPS   where Z3 and ANTLR are built and cached
+#                            (default: build-wasm/deps)
+#          AUTOQ_WASM_BUILD  build directory for AutoQ (default: build-wasm/autoq)
+#          JOBS              parallel build jobs
+#
+# Z3 and the ANTLR runtime are built once as static WebAssembly libraries and
+# reused on later runs. Everything is compiled with native WebAssembly
+# exceptions (-fwasm-exceptions), which all current browsers support.
+set -euo pipefail
+
+ROOT=$(cd "$(dirname "$0")/.." && pwd)
+DEPS=${AUTOQ_WASM_DEPS:-$ROOT/build-wasm/deps}
+BUILD=${AUTOQ_WASM_BUILD:-$ROOT/build-wasm/autoq}
+OUT=${1:-$ROOT/site/playground}
+BOOST_INCLUDE_DIR=${BOOST_INCLUDE_DIR:-/usr/include}
+JOBS=${JOBS:-$(nproc 2>/dev/null || sysctl -n hw.ncpu 2>/dev/null || echo 2)}
+
+# Keep these in sync with the bundled headers in include/z3 and include/antlr4-runtime.
+Z3_TAG=z3-4.12.5
+ANTLR_TAG=4.13.2
+EH_FLAGS="-fwasm-exceptions"
+
+command -v emcmake >/dev/null || { echo "error: emcmake not found; install and activate emsdk first" >&2; exit 1; }
+[ -d "$BOOST_INCLUDE_DIR/boost" ] || { echo "error: Boost headers not found in $BOOST_INCLUDE_DIR" >&2; exit 1; }
+mkdir -p "$DEPS"
+
+# Boost: header-only parts only. Expose just the boost/ directory so that no
+# other host headers leak into the Emscripten build.
+mkdir -p "$DEPS/boost-include"
+ln -sfn "$BOOST_INCLUDE_DIR/boost" "$DEPS/boost-include/boost"
+
+# Z3
+if [ ! -f "$DEPS/z3/libz3.a" ]; then
+  [ -d "$DEPS/z3-src" ] || git clone --depth 1 --branch "$Z3_TAG" https://github.com/Z3Prover/z3.git "$DEPS/z3-src"
+  # Recent clang rejects references to nonexistent members inside
+  # uninstantiated templates. This Z3 release has three such leftovers from
+  # renames; later Z3 releases contain the same fixes.
+  sed -i.orig 's/v\.m_matrix\.get(v\.m_row, v\.m_col)/v.m_matrix.get_elem(v.m_row, v.m_col)/' \
+    "$DEPS/z3-src/src/math/lp/static_matrix.h"
+  sed -i.orig 's/c\.m_low_bound)/c.m_lower_bound)/' "$DEPS/z3-src/src/math/lp/column_info.h"
+  sed -i.orig 's/A\.get_value_of_column_cell(col)/A.get_val(col)/' "$DEPS/z3-src/src/math/lp/static_matrix_def.h"
+  emcmake cmake -S "$DEPS/z3-src" -B "$DEPS/z3-build" \
+    -DCMAKE_BUILD_TYPE=Release \
+    -DCMAKE_CXX_FLAGS="$EH_FLAGS" \
+    -DZ3_SINGLE_THREADED=ON \
+    -DZ3_BUILD_LIBZ3_SHARED=OFF \
+    -DZ3_BUILD_EXECUTABLE=OFF \
+    -DZ3_BUILD_TEST_EXECUTABLES=OFF \
+    -DZ3_ENABLE_EXAMPLE_TARGETS=OFF \
+    -DZ3_BUILD_PYTHON_BINDINGS=OFF \
+    -DZ3_BUILD_DOCUMENTATION=OFF
+  cmake --build "$DEPS/z3-build" --target libz3 -j "$JOBS"
+  mkdir -p "$DEPS/z3"
+  cp "$DEPS/z3-build/libz3.a" "$DEPS/z3/libz3.a"
+fi
+
+# ANTLR4 C++ runtime
+if [ ! -f "$DEPS/antlr4/libantlr4-runtime.a" ]; then
+  [ -d "$DEPS/antlr4-src" ] || git clone --depth 1 --branch "$ANTLR_TAG" https://github.com/antlr/antlr4.git "$DEPS/antlr4-src"
+  emcmake cmake -S "$DEPS/antlr4-src/runtime/Cpp" -B "$DEPS/antlr4-build" \
+    -DCMAKE_BUILD_TYPE=Release \
+    -DCMAKE_CXX_FLAGS="$EH_FLAGS" \
+    -DANTLR_BUILD_CPP_TESTS=OFF \
+    -DANTLR_BUILD_SHARED=OFF \
+    -DANTLR_BUILD_STATIC=ON \
+    -DWITH_DEMO=OFF
+  cmake --build "$DEPS/antlr4-build" --target antlr4_static -j "$JOBS"
+  mkdir -p "$DEPS/antlr4"
+  cp "$(find "$DEPS/antlr4-build" -name 'libantlr4-runtime.a' | head -n 1)" "$DEPS/antlr4/libantlr4-runtime.a"
+fi
+
+# AutoQ
+# -ffile-prefix-map keeps the build machine's paths out of error messages.
+emcmake cmake -S "$ROOT" -B "$BUILD" \
+  -DCMAKE_BUILD_TYPE=Release \
+  -DCMAKE_CXX_FLAGS="$EH_FLAGS -ffile-prefix-map=$ROOT/=" \
+  -DAUTOQ_WASM_BOOST_INCLUDE="$DEPS/boost-include" \
+  -DAUTOQ_WASM_Z3_LIB="$DEPS/z3/libz3.a" \
+  -DAUTOQ_WASM_ANTLR4_LIB="$DEPS/antlr4/libantlr4-runtime.a"
+cmake --build "$BUILD" --target autoq -j "$JOBS"
+
+mkdir -p "$OUT"
+cp "$BUILD/cli/autoq.js" "$BUILD/cli/autoq.wasm" "$OUT/"
+echo "Wrote $OUT/autoq.js and $OUT/autoq.wasm"
diff --git a/wasm/compare.mjs b/wasm/compare.mjs
new file mode 100644
index 000000000..10a593b47
--- /dev/null
+++ b/wasm/compare.mjs
@@ -0,0 +1,50 @@
+// Runs every playground example with the native CLI and with the WebAssembly
+// build, and checks that both print the same output (timing and memory
+// figures are masked).
+//
+// Usage: node wasm/compare.mjs [path/to/native/autoq] [dir with autoq.js]
+//        defaults: build/cli/autoq and site/playground
+import { execFileSync } from 'node:child_process';
+import { mkdtempSync, writeFileSync } from 'node:fs';
+import { tmpdir } from 'node:os';
+import { join, resolve } from 'node:path';
+import { pathToFileURL } from 'node:url';
+
+const native = resolve(process.argv[2] ?? 'build/cli/autoq');
+const wasmDir = resolve(process.argv[3] ?? 'site/playground');
+const { EXAMPLES } = await import(pathToFileURL(join(wasmDir, 'examples.js')));
+const { default: createAutoQ } = await import(pathToFileURL(join(wasmDir, 'autoq.js')));
+
+const ARGS = { ver: ['pre.hsl', 'circuit.qasm', 'post.hsl'], ex: ['pre.hsl', 'circuit.qasm'], eq: ['a.qasm', 'b.qasm'] };
+const mask = (s) => s
+  .replace(/\[\d+(\.\d+)?(ms|s|m|h|d)?\](?= with| memory|\.|$)/g, '[T]')
+  .replace(/\[\d+(\.\d+)?(ms|us|s|m)\]/g, '[T]')
+  .replace(/\[\d+MB\]/g, '[MB]')
+  .trim();
+
+let failures = 0;
+for (const ex of EXAMPLES) {
+  const args = [ex.mode, ...ARGS[ex.mode]];
+  const dir = mkdtempSync(join(tmpdir(), 'autoq-cmp-'));
+  for (const f of ex.files) writeFileSync(join(dir, f.name), f.content);
+
+  let nat, natCode = 0;
+  try { nat = execFileSync(native, args, { cwd: dir, encoding: 'utf8', stdio: ['ignore', 'pipe', 'pipe'] }); }
+  catch (e) { nat = (e.stdout ?? '') + (e.stderr ?? ''); natCode = e.status; }
+
+  const lines = [];
+  const mod = await createAutoQ({ print: (l) => lines.push(l), printErr: (l) => lines.push(l) });
+  mod.FS.mkdir('/work'); mod.FS.chdir('/work');
+  for (const f of ex.files) mod.FS.writeFile(f.name, f.content);
+  let wasmCode;
+  try { wasmCode = mod.callMain([...args]); } catch (e) { if (e?.name === 'ExitStatus') wasmCode = e.status; else throw e; }
+  const wasm = lines.join('\n');
+
+  const same = mask(nat) === mask(wasm) && natCode === wasmCode;
+  if (!same) failures++;
+  console.log(`${same ? 'same' : 'DIFF'}  ${ex.id.padEnd(8)} autoq ${args.join(' ')}  (exit ${natCode}/${wasmCode})`);
+  if (process.env.VERBOSE) console.log('  ' + mask(wasm).split('\n').join('\n  '));
+  if (!same) console.log(`  native: ${mask(nat)}\n  wasm:   ${mask(wasm)}`);
+}
+console.log(failures ? `${failures} example(s) differ` : 'All examples match.');
+process.exit(failures ? 1 : 0);