xq-rs Documentation

Technical Documentation: QuipNetwork/xq-rs

ℹ️ Provenance: Multi-Tier Ingestion · CodeWiki Reference

Overview (`README.md`) Copy Section

XQuad

Early public release. The instruction set, binary format, and public API
may still change before v1.0. Production use is not recommended yet.

XQuad is a hardware-agnostic toolchain for expressing and running quadratic
optimization problems (QUBO / Ising / integer) across quantum annealers and
classical solvers. It ships as three Rust crates plus five Python distributions
built around a single virtual-machine specification.

Think of it as LLVM for quadratic models -- a common intermediate
representation that lets you write a problem once and retarget it to any
supported backend.

• Spec-first. Every behaviour is nailed down in spec/xqvm/SPEC.md
  and cross-implementation parity is mechanically enforced: every committed
  conformance vector runs on both the Rust production VM (xqvm) and the
  Python reference VM (xqvm_py) in CI; disagreement fails the build.
• Embeddable. The Rust core supports no_std + alloc, so the same VM
  runs inside WASM runtimes, Substrate pallets, and native binaries.
• Interactive. The Python umbrella (xquad) is REPL and Jupyter-friendly:
  load a program once, run it with different calldata, inspect outputs by
  slot. Low-level FFI lives in xqffi; user-facing Program / Session /
  RunResult live in xquad.program.

Install Copy Chapter

Rust (from crates.io) Copy Section

cargo install xqcli           # gives you the `xquad` binary

Python (from PyPI) Copy Section

pip install xquad             # umbrella -- full pipeline
# or pick individual pieces:
pip install xqffi xqcp xqsa   # FFI bindings + DSL + solvers

Prebuilt wheels are available for Linux x86_64 and aarch64 (CPython >= 3.13). On macOS and Windows, pip builds the xqffi Rust extension from source -- this requires a Rust toolchain (>= 1.85).

GPU/QPU support Copy Section

The base install includes CPU simulated annealing only. To use GPU or quantum hardware solvers, install the corresponding extra:

Extras are composable: pip install xquad[cuda,dwave]. See xqsa/README.md for driver prerequisites and per-solver quick-starts.

For a guided walkthrough that installs XQuad, verifies it, and runs a
complete problem end to end, see
Install XQuad in the book.

Package map Copy Chapter

Three Rust crates on crates.io:

Five Python distributions on PyPI:

The one Rust package without a crates.io artefact is the xqffi pyo3
crate itself -- it ships as the xqffi PyPI wheel rather than a reusable
Rust library.

Quick start Copy Chapter

A minimal program (CLI) Copy Section

; add.xqasm -- push two integers and add them
PUSH 10
PUSH 32
ADD
HALT

xquad asm add.xqasm -o add.xqb && xquad run add.xqb

End-to-end (Python, via the umbrella) Copy Section

The recommended user-facing surface is xquad.program.Program +
Session + RunResult. Load once, run many times with different
calldata, inspect outputs by slot:

from xquad.program import Program

program = Program.from_source("""
PUSH 0
INPUT r0
PUSH 1
INPUT r1
LOAD r0
LOAD r1
ADD
STOW r2
PUSH 0
OUTPUT r2
HALT
""")

session = program.session(output_slots=1)
session.set_calldata([40, 2])
result = session.run()
assert dict(result.outputs) == {0: 42}

Program.load(bytes) takes wire-format bytecode; Session.run()
returns a RunResult with dict-keyed outputs (unset slots present as
None), residual stack, and step count. See
Running Programs for the full tour.

Low-level / conformance surface

For conformance harnesses and one-shot execution, the raw
xqffi.vm.Vm is still available directly:

from xqffi.asm import assemble_source
from xqffi.vm import Vm

bytecode = assemble_source(src)
v = Vm()
v.set_calldata([40, 2])
v.set_output_slots(1)
v.run(bytecode)
assert v.outputs() == [42]

The xquad.vm.VM class offers a middle tier -- a unified wrapper with
backend dispatch (VMBackend.RUST / VMBackend.PYTHON) that accepts
.xqasm source and normalises types across the two interpreters.

End-to-end worked example Copy Section

examples/tsp/ shows a full Travelling Salesman Problem
driven from the xqcp DSL through the VM and xqsa solver, runnable on
either the Python reference VM or the Rust VM:

uv run python examples/tsp/runner.py --seed 42
uv run python examples/maxcut/runner.py --seed 42 --interpreter rust

# Run every example on both interpreters, check each finds a valid solution:
make example-smoke

Architecture Copy Chapter

XQuad is a stack-based interpreter with a 256-slot register file. Registers
hold typed values -- integers, integer vectors, QUBO/Ising models
(XqmxModel), and candidate solutions (XqmxSample). A dedicated loop stack
drives RANGE/ITER iteration.

The opcode table is declared once in xqvm/src/bytecode/types/table.rs via
the opcodes! x-macro; conformance/opcodes.yaml is the machine-readable
mirror that all three representations (YAML, Rust macro, xqvm_py.opcodes)
are checked against at build time and in CI
(scripts/check-opcode-parity.py).

The binary format (.xqb) opens with a fixed 15-byte XQBC header --
magic, version, calldata/output-slot counts, code length, and a CRC-32
checksum of the payload -- followed by the instruction stream: an
opcode byte followed by its operands in big-endian byte order.

See conformance/opcodes.md for
instruction-by-instruction semantics and
spec/xqvm/SPEC.md for the normative spec.

Development Copy Chapter

Prerequisites Copy Section

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh   # stable Rust
make deps                                                          # dev tools

Local setup Copy Section

make xquad

This syncs the Python workspace (xqvm_py, xqcp, xqsa, xqffi,
xquad) into .venv/, builds the xqffi pyo3 extension via maturin,
puts the repo root on sys.path so scripts anywhere in the repo can
import xqcp / xqsa / xqvm_py / xqffi / xquad naturally, and
installs the xquad CLI binary under ~/.cargo/bin/.

Open a REPL with everything ready:

make repl

CI-equivalent locally Copy Section

make preflight    # what CI enforces, split into preflight-rs / -py / -parity / -docs / -policy
make conformance  # cross-impl parity suite (Rust + Python)

Contributing Copy Section

See CONTRIBUTING.md for the development workflow, commit
conventions, and DCO sign-off requirements. Agent guidelines for AI coding
assistants are in AGENTS.md; cutting a release is documented in
RELEASING.md.

License Copy Chapter

Licensed under the GNU Affero General Public License v3.0 or later.

Overview (`conformance/README.md`) Copy Section

XQVM Conformance Harness

Mechanical cross-implementation check that the Rust production VM
(xqvm) and the Python reference VM
(xqvm_py) agree on every observable behaviour defined
by spec/xqvm/SPEC.md.

The harness is a Rust test crate (xquad-conformance). Each vector
becomes two #[test] functions -- one per runtime -- generated at
cargo build time by build.rs. CI runs both through the
verify:parity job's make -k check-parity, which keeps running
every target after one fails so a Python-side regression cannot mask a
Rust-side pass (or vice versa).

Layout Copy Chapter

conformance/
├── opcodes.yaml          single machine-readable source for the 93-opcode table
├── vectors/
│   ├── arithmetic/<name>/
│   │   ├── program.xqasm       canonical assembly source
│   │   ├── inputs.json         {"calldata": [i64, ...], "output_slots": N}
│   │   └── expected.json       {"outputs": [...], "final_stack": [...]} or {"error": FAULT}
│   ├── control-flow/<name>/
│   ├── energy/<name>/
│   ├── constraints/<name>/
│   ├── vector-ops/<name>/
│   └── xqmx-grid/<name>/
├── src/                  Rust library + manual CLI binary
├── tests/rust.rs         generated in-process Rust runner tests
└── tests/python.rs       generated subprocess Python runner tests

File format Copy Chapter

`program.xqasm` Copy Section

Canonical human-readable source. The assembler is authoritative: whatever
xqasm::assemble_source() produces becomes the canonical bytecode.
Prefer explicit PUSH1/PUSH2/... forms when the constant width matters
for the vector; use the PUSH sugar where it doesn't.

The harness assembles program.xqasm in-process on every run; encoding
correctness is owned by the xqasm crate's own test suite, so no
pre-assembled bytecode artifact is committed.

`inputs.json` Copy Section

{
  "calldata": [6, 7],
  "output_slots": 16,
  "step_limit": 50,
  "memory_limit": 1048576
}

output_slots is optional (defaults to 16, matching xquad run). The
calldata array is exposed to the program in slot order: slot 0 holds
the first value, slot 1 the second, and so on. step_limit is optional
and defaults to 10000000, matching xquad run; the harness resolves the
default itself and passes it to both runners, because the two
implementations disagree on what an omitted budget means and a vector
that left it out used to run bounded on Rust and unbounded on Python.
Set it only for a vector that is specifically exercising the budget.

memory_limit is the same arrangement for the allocation budget: optional,
defaulting to 1073741824 (xqvm::DEFAULT_MEMORY_LIMIT), resolved once by
the harness and passed to both runners. It is what makes the
allocation-charge half of the fault-ordering rule below assertable, since
those faults are only reachable against a budget the charge exhausts.

`expected.json` Copy Section

A vector asserts either an outcome or a fault. Supplying both, or
neither, is rejected as a vector-authoring mistake rather than silently
preferring one half.

{
  "outputs": [42],
  "final_stack": []
}

outputs is a sparse map, per the state model in spec/xqvm/SPEC.md --
each entry is either an i64 (the value written by OUTPUT) or null
(the slot was reserved but explicitly zeroed by a peer entry). Trailing
unset slots are omitted entirely, so a program that writes slot 0 out of
16 reserved slots produces [42], not [42, null, ...].
Explicitly-written zeroes are preserved; only slots that OUTPUT never
touched disappear. final_stack is the residual stack at HALT (bottom
to top); an empty stack is typical.

A vector that expects the program to fault writes the fault's identity
instead:

{
  "error": "DIVISION_BY_ZERO"
}

Fault identities Copy Section

Neither implementation's spelling can serve as the identity: Rust raises
enum variants, Python raises exception classes, and the two vocabularies
do not line up one-to-one. expected.json therefore names a third,
implementation-neutral vocabulary that both sides map onto.

Byte position is deliberately not part of the identity. Only the
fault itself is compared, so vectors do not turn brittle against
unrelated codegen changes. Position assertions can be added later if a
bug ever motivates them.

The Rust mapping is an exhaustive match, so adding a variant to
xqvm::Error without extending this table fails to compile rather than
silently degrading to an "unknown" fault. The Python mapping is by class
name and is necessarily partial: a -- above means that implementation
has no distinct class for the fault yet, and a vector asserting it will
fail loudly on the Python runner until one exists.

The loop faults were that gap until QUI-1289: xqvm_py raised one
LoopError class for both NO_ACTIVE_LOOP and UNMATCHED_LOOP, which
the harness could not resolve to either identity without picking
arbitrarily, so it mapped neither. The class is now split into
NoActiveLoop and UnmatchedLoop, and each identity is pinned by its own
vector: vectors/control-flow/next_outside_loop and
vectors/control-flow/range_empty_unmatched.

Fault ordering (QUI-1178) Copy Section

spec/xqvm/SPEC.md fixes the order of work within one instruction: pops,
then the allocation charge, then validation. Where a register read once
preceded the pops in xqvm_py, the divergence was reachable two ways --
a short stack (which the verifier rejects) and an operand fault raised
ahead of the register read (which it admits). Only the second is
consensus-visible.

Of the 22 opcodes reordered, the second route reaches:

The ONEHOTR/ONEHOTC row read "none" before QUI-1202 as well, on a
justification that did not hold. exec_one_hot_r sizes its charge from a
peek that yields cols only for RegVal::Model and 0 for everything
else, then resolves with as_model_mut; neither Python runner peeked at
all -- both went pop, _get_register_as_xqmx (which accepts a sample),
dimensions, charge -- so a sample's real extent sized the charge and a
tight budget raised MemoryLimitExceeded where the Rust VM charged
nothing. _peek_model_grid closes it: the peek is is_model()-gated on
both VMs now, and the budget can no longer decide the fault.

That mattered because the register reaches ONEHOTR as a sample without
the verifier objecting. check_reads requires R::Model there, and a
register the verifier knows is a Sample is rejected statically -- but it
does not always know. Two routes got past it, of which one is still open:

• Host calldata. Vm::set_calldata takes any RegVal, samples
  included ("This allows passing models, samples, and vectors between
  programs"), and INPUT clones the entry into the register. INPUT
  writes RegType::Any, which satisfies every requirement, so
  PUSH 0 / INPUT r0 / PUSH 0 / PUSH 1 / ONEHOTR r0 is verifier-clean and
  arrives holding whatever the embedder supplied. The --calldata CLI flag
  parses i64s and cannot express this; the embedding API is the reachable
  surface, and on a chain runtime it is the host that fills those slots.
• A branch join. meet_reg merged Model and Sample to
  RegType::Any, so a program that wrote BQMX on one branch and BSMX
  on the other, joined, and called ONEHOTR verified clean using nothing
  but its own instructions. QUI-1160 closed that: the join now yields
  RegType::Grid, which satisfies the grid operations and not R::Model.
  Host calldata is the remaining route, and it is open by design.

The name the surviving fault carries is settled as of QUI-1160:
xqvm_py rejects the sample with XQMXModeError and the Rust VM with
RegisterType, and both map onto TYPE_MISMATCH. The test above still
pins the charge rather than the name, because the charge is what QUI-1202
fixed; the name is pinned by the coefficient-access vectors instead.

Authoring a new vector Copy Chapter

1. Write program.xqasm with a minimal scenario that exercises the
   behaviour you care about.
2. Pick the matching vector directory under vectors/ (or create a new
   one). These directory names are a separate, coarser vocabulary from
   opcodes.yaml's own category field -- the two do not need to match,
   and mostly don't.
3. Write inputs.json with the calldata the program reads.
4. Produce expected.json by running one of the two impls and
   inspecting the result. The harness then asserts the other impl
   agrees. If they disagree, you've found spec drift -- file a bug
   ticket, and either fix the divergent impl or exclude the vector
   with a comment referencing the ticket.

Drift policy Copy Chapter

There is no DRIFT.md. Either every vector passes on both runtimes or
the build is broken. Concrete enforcement:

• Opcode table -- xqvm/build.rs asserts opcodes.yaml against the
  opcodes! x-macro at compile time; scripts/check-opcode-parity.py
  asserts opcodes.yaml against xqvm_py/opcodes.py in CI. The Rust
  check compares the wire byte, the mnemonic, the net stack effect and
  each operand's name and encoded byte width. It compares the net effect
  rather than the stack_pop/stack_push pair, because the x-macro
  stores only the net delta; the pair is compared on the Python side.
• Bytecode encoding -- owned by the xqasm crate's own test suite
  (xqasm/tests/integration.rs plus assembler unit tests).
• Observable behaviour -- check_vector asserts the
  observed {outputs, final_stack}, or the observed fault identity,
  matches expected.json for both runtimes.
• Coverage -- coverage.rs computes which opcodes
  the vectors cover, and CI prints the report on every pipeline as the
  last step of make check-parity. It does not require completeness,
  which would fail today; tests/coverage.rs holds
  the current numbers as floors so coverage cannot regress unremarked.

Running locally Copy Chapter

# Full matrix (both runtimes, all vectors)
cargo test -p xquad-conformance

# Rust only
cargo test -p xquad-conformance --no-default-features --features rust

# Python only (needs python3 + xqvm_py importable from xqvm_py/)
cargo test -p xquad-conformance --no-default-features --features python

# Manual CLI for authoring / triaging a single vector
cargo run -p xquad-conformance -- --filter arithmetic/add_basic --impl both

# Which opcodes no vector covers
make conformance-coverage

The coverage report gives two numbers. Present counts opcodes
appearing in a vector's assembled program; reached counts those a
vector executes to completion. Reached is always the smaller: an opcode
behind an untaken branch is present but not reached, and so is the
instruction an error vector exists to fault on, since a faulting
instruction never completes a step. An opcode missing from both lists is
a genuine hole; one that is present but never reached has an error vector
and no success-path vector.

Override the Python interpreter with XQUAD_CONFORMANCE_PYTHON=....

Overview (`examples/README.md`) Copy Section

XQuad Examples

Fourteen self-contained optimisation problems, one directory each. Every
directory holds a README.md describing the formulation and a runner.py
that builds the model, solves it, and verifies the result end to end.

Run one from the repository root:

uv run python examples/maxcut/runner.py --seed 42

Every runner accepts --seed, --interpreter (python or rust),
--solver, and -o/--output. Problem size flags vary; each directory's
README.md carries the exact table.

Graph problems Copy Chapter

Examples that encode graph cuts, colouring, covers, independent sets, and tours.

• Max-Cut -- Find a 2-colour partition of a weighted graph that maximises the cut weight.
• Graph Coloring -- Assign colours to graph nodes so adjacent nodes do not share a colour.
• Maximum Independent Set -- Select the largest subset of graph nodes with no selected edge between them.
• Vertex Cover -- Select the smallest vertex subset that covers every graph edge.
• Travelling Salesman Problem -- Find the shortest Hamiltonian tour through a random symmetric distance matrix.

Selection and packing Copy Chapter

Examples that select subsets, cover demands, pack bins, and balance integer weights.

• Knapsack -- Select items that maximise value while respecting a capacity constraint.
• Bin Packing -- Pack items into the minimum number of fixed-capacity bins.
• Set Cover -- Select the minimum set collection whose union covers the universe.
• Weighted Set Cover -- Select sets with capacities to cover element demands at minimum cost.
• Number Partition -- Split positive integers into two subsets with nearly equal sums.
• Portfolio Optimization -- Select a fixed-size portfolio while penalising higher-order risk interactions.
• Portfolio Rebalance -- Choose signed integer asset weights against a risk matrix and a budget.

Satisfiability and higher-order Copy Chapter

Examples that reduce clauses and higher-order pseudo-Boolean objectives to quadratic models.

• Max-3-SAT -- Find the assignment that satisfies the maximum number of 3-literal clauses.
• Cubic Optimization -- Minimise a cubic pseudo-Boolean objective through HOBO degree reduction.
• Quartic Optimization -- Minimise a degree-4 pseudo-Boolean objective through two-stage REDUCE chaining.

Further reading Copy Chapter

• Using the Examples -- what every
  directory has in common, how to run one, and how to adapt one into a problem
  of your own
• Modelling with XQCP -- the DSL these
  runners are written in
• Cookbook -- the recurring encoding
  patterns these examples are built from

Overview (`spec/README.md`) Copy Section

XQuad Toolchain Specifications

Authoritative specifications for each layer of the XQuad Toolchain. Every
specification here is the single source of truth for its layer. The
conformance/ harness does not check either implementation against this
prose: it checks the Rust and Python implementations against each other,
and against conformance/opcodes.yaml. Where a divergence between a spec
and an implementation is known, the relevant book page records it.

Layers Copy Chapter

• xqvm/ -- X-Quadratic Virtual Machine. Bytecode format,
  instruction semantics, stack and register model, binary encoding.
  See xqvm/README.md for the document index.
• xqcp/ -- X-Quadratic Constraint Programming DSL. Symbolic
  problem description and compilation to XQVM assembly. See
  xqcp/README.md.
• xqsa/ -- X-Quadratic Solver Adapters. Solver-backend
  interface and sample/energy contracts. See
  xqsa/README.md.

Drift policy Copy Chapter

There is no tolerated drift between spec and implementations. Any change
to the xqvm/ spec files that affects observable behaviour must land with:

1. A matching update to ../conformance/opcodes.yaml.
2. Updated or new conformance vectors under ../conformance/vectors/.
3. Both xqvm (Rust) and xqvm_py (Python) passing the full conformance
   suite.

Builds fail on mismatch -- there is no DRIFT.md.

Overview (`xqasm/README.md`) Copy Section

xqasm

Text assembler for the XQuad Toolchain.

xqasm turns .xqasm assembly source into xqvm::Program bytecode: a
pest grammar parses source text into an
AST, the assembler lowers the AST to instructions via
xqvm::InstructionBuilder, and errors are reported as rich
miette diagnostics with source spans.
This crate declares no binary; the xquad asm subcommand in
xqcli is the
command-line entry point.

Install Copy Chapter

cargo add xqasm

Quick start Copy Chapter

The one-call entry point is assemble_source:

use xqasm::assemble_source;
use xqvm::Vm;

let program = assemble_source("PUSH 10\nPUSH 32\nADD\nHALT").unwrap();

let mut vm = Vm::new();
vm.run(&program).unwrap();
assert_eq!(vm.stack(), &[42]);

For finer control over the two phases, parse and assemble are exposed
separately:

use xqasm::{assemble, parse};

let source = "PUSH 10\nPUSH 32\nADD\nHALT";
let lines = parse(source, "<input>").unwrap();
let program = assemble(&lines, source, "<input>").unwrap();
assert!(!program.code().is_empty());

Assembly syntax, briefly Copy Chapter

• Line comments start with ; and run to end of line.
• Jump targets are declared with TARGET .N and referenced as JUMP .N /
  JUMPI .N, where .N is a numeric label ID (.0, .1, and so on)
  assigned sequentially during pre-scan; the .N text is assembler-only and
  never appears in the bytecode.
• PUSH <value> desugars to the smallest PUSH1-PUSH8 opcode that fits
  the signed integer literal.
• Registers are r0..r255.

Links out Copy Chapter

• Bytecode encoding spec -- assembly syntax and binary format
• Normative VM spec
• xqvm -- bytecode types and interpreter this crate targets
• xqcli -- the xquad CLI, wraps this crate as xquad asm
• Repository

License Copy Chapter

AGPL-3.0-or-later.

Overview (`xqcli/README.md`) Copy Section

xqcli

Unified CLI for the XQuad Toolchain.

This crate is named xqcli; it builds the xquad binary. That is:
cargo install xqcli installs a command called xquad, not xqcli.
Running xqcli --help after installing will fail because no such binary
exists.

Install Copy Chapter

cargo install xqcli
xquad --help

Subcommands Copy Chapter

xquad has four subcommands, one per stage of the toolchain: asm,
dism, run, verify.

Run xquad <subcommand> --help for the full option list; the summaries
below are the parts most people need first.

• xquad asm: -o, --output <OUTPUT> (defaults to .xqb), --stdout to write bytecode to stdout instead of a file.
• xquad dism: reads from stdin when FILE is omitted.
• xquad run: --text to treat FILE as assembly, --calldata <CALLDATA> (comma-separated integers), --outputs <OUTPUTS> (default 16), --step-limit <STEP_LIMIT> (default 10000000; the value is an exact limit, so 0 executes nothing), --unlimited-steps to run without a step limit, --trace with --trace-format text|json and --trace-file <FILE>.
• xquad verify: --text to treat FILE as assembly before verifying.

Quick start Copy Chapter

cat > add.xqasm <<'EOF'
; add.xqasm -- push two integers and add them
PUSH 10
PUSH 32
ADD
HALT
EOF

xquad asm add.xqasm -o add.xqb
xquad run add.xqb
xquad dism add.xqb
xquad verify add.xqb

xquad run add.xqb prints the residual stack:

stack (bottom to top):
  42

Links out Copy Chapter

• xqvm -- bytecode types and interpreter this CLI drives
• xqasm -- text assembler behind xquad asm
• Normative VM spec
• Bytecode encoding spec
• Repository

License Copy Chapter

AGPL-3.0-or-later.

Overview (`xqcp/README.md`) Copy Section

XQCP -- X-Quadratic Constraint Programmer

A constraint-programming DSL that compiles a problem description into three
XQVM assembly programs: an encoder, a verifier, and a decoder. See
Three Programs
for what those three are and why there are three.

Install Copy Chapter

pip install xqcp

A complete example Copy Chapter

Max-Cut for three nodes -- the same graph
Quadratic Models
derives by hand -- built with Problem and compiled to .xqasm:

from xqcp import Domain, Problem, Types

problem = Problem("Triangle")
n = problem.input("n", type=Types.Int)
edges = problem.input("edges", type=Types.Vec)
problem.define_model(size=n, domain=Domain.BINARY)

edge_count = problem.stow("edge_count", edges.veclen() // 3)
with problem.range(0, edge_count) as e:
    offset = e * 3
    i = problem.stow("i", edges.get(offset))
    j = problem.stow("j", edges.get(offset + 1))
    w = problem.stow("w", edges.get(offset + 2))
    problem.model.linear[i].add(-w)
    problem.model.linear[j].add(-w)
    problem.model.quadratic[i, j].add(w * 2)

partition = problem.output("partition", type=Types.Vec)
with problem.range(0, n) as node:
    partition.append(problem.sample.getline(node))

programs = problem.compile()
print(programs.encoder.count("\n"), "lines in the compiled encoder")
# 57 lines in the compiled encoder

programs.encoder builds the model; programs.verifier checks a sample
against it and computes its energy; programs.decoder reads a sample back
into a partition. Each is a standalone .xqasm string, runnable through
any XQVM interpreter.

Domain also covers integer variables (INTEGER with k=, or with
lo=/hi= for a range XQCP shifts into the model and back out through
sample.value()) and unordered cases (CATEGORICAL with k= and
penalty=, recorded as a one-hot binary grid read with sample.case()).
The Modelling
chapter covers each form and what constraints are available on it.

How it works Copy Chapter

Problem records every DSL call (input, define_model, range,
stow, model.linear[i].add(w), and the rest) as an Action. Nothing is
assembled until compile() runs: it walks the recorded actions once per
program and emits assembly with automatic register allocation and loop
nesting.

DSL reference Copy Chapter

The full DSL -- inputs, expressions, objectives, constraints, control flow,
outputs, and what compile() produces -- is
Modelling,
eight chapters built around this exact package. The normative reference is
spec/xqcp/SPEC.md;
this package follows it, and any divergence here is a bug.

Examples Copy Chapter

Fifteen complete problems built with this DSL, from
Max-Cut
to
Travelling Salesman,
are listed in the
example gallery.

Also see Copy Chapter

• xqvm_py -- pure-Python reference VM that runs the compiled programs.
• xqffi -- pyo3 FFI bindings to the Rust runtime.
• xqsa -- solver adapters for the models this package builds.
• xquad -- umbrella meta-package.

License Copy Chapter

AGPL-3.0-or-later.

Overview (`xqffi/README.md`) Copy Section

xqffi -- PyO3 FFI bindings for the XQuad Rust runtime

The Python extension that exposes the Rust xqvm interpreter and xqasm assembler. Ships as abi3 manylinux wheels (x86_64 + aarch64, CPython >= 3.13) plus a universal sdist for other platforms, all built by maturin.

xqffi is a pure FFI shim -- it only re-exposes the Rust types and entry points. User-facing conveniences (Program / Session / RunResult, keyword calldata, trace inspection) live in the xquad umbrella package.

Install Copy Chapter

pip install xqffi

Surface Copy Chapter

`xqffi.vm` -- low-level one-shot Copy Section

What the conformance harness drives. Small wrapper over xqvm::Vm:

from xqffi.vm import Vm
from xqffi.asm import assemble_source

vm = Vm()
vm.set_calldata([40, 2])
vm.set_output_slots(1)
vm.run(assemble_source(src))
assert vm.outputs() == [42]

XqmxModel and XqmxSample are thin getter/setter wrappers around the Rust types for direct model/sample manipulation. They refuse what bytecode could not build: a size over MAX_ALLOCATION_SIZE or a grid that does not fit (ValueError), a sample value outside its domain (ValueError), and a coefficient index outside 0..size, negative included (IndexError).

`xqffi.asm` -- assembly Copy Section

parse_xqasm(str) -> wire dict; assemble_source(str) -> raw bytes; disassemble(bytes) -> human-readable listing; instruction_count(bytes) -> instruction count.

`xqffi.verifier` -- static verification Copy Section

verify(bytes) and verify_source(str) run the pre-execution verifier: every jump lands on a TARGET, every register is read after it is written, and stack depth balances. Both return None on success and raise ValueError on a rejected program. See Verifier.

Interactive / multi-run API Copy Chapter

Use xquad.program for the REPL / notebook / script workflow:

from xquad.program import Program

program = Program.from_source(src)
session = program.session(output_slots=1)
session.set_calldata([40, 2])
result = session.run()
assert dict(result.outputs) == {0: 42}

Program.load(bytes) takes wire-format bytecode; Session.run() returns a RunResult with dict-keyed outputs (unset slots present as None), residual stack, and step count.

Also see Copy Chapter

• xqvm_py -- pure-Python reference VM (conformance oracle).
• xqcp -- constraint programming DSL that compiles to .xqasm.
• xqsa -- solver adapters: CPU/GPU annealers, D-Wave QPU, Quip network.
• xquad -- umbrella meta-package with the interactive API.
• Running Programs -- full tour.

License Copy Chapter

AGPL-3.0-or-later.

Overview (`xqsa/README.md`) Copy Section

xqsa -- Solver adapters for XQMX models

Pluggable solvers for quadratic optimisation models produced by the XQuad
toolchain. One interface, five backends:

Install Copy Chapter

pip install xqsa               # CPU simulated annealing only
pip install xqsa[dwave]        # add D-Wave QPU support
pip install xqsa[cuda]         # add CUDA GPU support
pip install xqsa[metal]        # add Metal GPU support
pip install xqsa[quip]         # add Quip network support

Extras are composable: pip install "xqsa[cuda,dwave]".

A complete example Copy Chapter

build_solver picks a backend by name, so a caller can stay
backend-agnostic across all five:

from xqsa import SOLVERS, build_solver
from xqvm_py import XQMX

model = XQMX.binary_model(size=4)
model.set_linear(0, -1)
model.set_quadratic(0, 1, 2)

print(sorted(SOLVERS))
# ['cuda-gpu', 'dwave-cpu', 'dwave-qpu', 'metal-gpu', 'quip']

solver = build_solver("dwave-cpu", seed=42)
result = solver.solve(model)
print(result.sample)
print(result.energy)
# XQMX(mode=SAMPLE, domain=BINARY, size=4, linear_terms=1, quadratic_terms=0)
# -1

Every backend's solve() returns the same SolverResult(sample, energy, timing, metadata): sample is the best assignment found, energy is the
Hamiltonian recomputed independently in exact integer arithmetic (never
taken on faith from the backend), and metadata's shape is per-backend.
build_solver("dwave-cpu", ...) is equivalent to constructing
SolverDWaveCPU(...) directly; reach for the class constructor instead of
build_solver when the backend is fixed at write time rather than chosen
by name at run time.

SolverQuip also splits a job into steps: create_order(model) returns
a draft JobOrder whose options (payout rule, allowlist, quality
floors) are checked before anything is signed, quote() prices it and
submit() sends it. A submitted order leaves a JobOrderReceipt, which
any session rebuilds from the order id with get_receipt(). Import them
from xqsa.quip.

Reference Copy Chapter

Driver prerequisites, per-backend parameters, embedding on a D-Wave QPU,
the Quip network job lifecycle and its job orders, and what the reported
energy means on
fixed-precision hardware are covered in
Solving Overview
and its chapters. The normative reference is
spec/xqsa/SPEC.md;
this package follows it, and any divergence here is a bug.

Also see Copy Chapter

• xqvm_py -- pure-Python reference VM.
• xqffi -- pyo3 FFI bindings to the Rust runtime.
• xqcp -- constraint-programming DSL that compiles to models this package can sample.
• xquad -- umbrella meta-package.
• Running Programs -- end-to-end tour.

License Copy Chapter

AGPL-3.0-or-later.

Overview (`xquad/README.md`) Copy Section

xquad -- Primary user-facing package for the XQuad toolchain

xquad is the Python distribution most users should install. It provides the interactive Program / Session / RunResult API, a unified VM wrapper that dispatches to either the Rust or Python interpreter, and re-exports the lower-level peer packages (xqffi, xqcp, xqsa) under a single namespace.

Install Copy Chapter

pip install xquad

Pulls xqffi, xqcp, xqsa, and xqvm_py as runtime dependencies.
Peer installs stay valid (pip install xqffi xqcp xqsa) if you only
need a subset.

Interactive usage Copy Chapter

Load a program once, run it with different calldata, inspect outputs by slot:

from xquad.program import Program

program = Program.from_source("""
PUSH 0
INPUT r0
PUSH 1
INPUT r1
LOAD r0
LOAD r1
ADD
STOW r2
PUSH 0
OUTPUT r2
HALT
""")

session = program.session(output_slots=1)
session.set_calldata([40, 2])
result = session.run()
assert dict(result.outputs) == {0: 42}

Program.load(bytes) takes wire-format bytecode; Session.run() returns a RunResult with dict-keyed outputs (unset slots present as None), residual stack, and step count.

Full pipeline Copy Chapter

Compile a problem via the DSL, execute, sample:

from xquad import cp, sa
from xquad.vm import VM, VMBackend

problem = cp.Problem("MyProblem")
# ... define inputs, model, objective, decoder ...
programs = problem.compile()

vm = VM(backend=VMBackend.RUST)   # or VMBackend.PYTHON for the reference interpreter
vm.set_output_slots(1)
vm.run(programs.encoder)
model = vm.outputs()[0]

sample = sa.SolverDWaveCPU().solve(model).sample

Re-exports of peer packages are identity, not copies:

import xquad, xqcp
assert xquad.cp.Problem is xqcp.Problem   # always True

So isinstance works whether the caller imported directly from the peer or via the umbrella.

Subnamespaces Copy Chapter

Lower-level escape hatches remain available directly via the peer packages (xqffi.vm.Vm for the raw FFI one-shot surface; xqvm_py.Executor for the pure-Python reference VM).

Also see Copy Chapter

• xqffi -- PyO3 FFI bindings (low-level / conformance).
• xqvm_py -- pure-Python reference VM (conformance oracle).
• xqcp -- constraint-programming DSL.
• xqsa -- solver adapters.
• Running Programs -- end-to-end tour including the Program/Session, xqffi.vm, and xquad.vm surfaces.

License Copy Chapter

AGPL-3.0-or-later.

Overview (`xqvm/README.md`) Copy Section

xqvm

X-Quadratic Virtual Machine -- bytecode interpreter for the XQuad Toolchain.

xqvm is the runtime layer of XQuad: the opcode table, instruction types, a
bytecode builder and codec, an incremental instruction-stream reader, the
VM interpreter, and a disassembler. A problem compiled once to XQVM
bytecode runs unchanged on this interpreter or on the pure-Python
reference VM (xqvm_py); the two are checked for behavioural parity in CI.

The crate is no_std + alloc-compatible. The bytecode layer (opcode
table, instruction codec, InstructionBuilder, Program) and the
interpreter core always build without std. The std feature, enabled
by default, adds the disassembler, JSON/text execution tracers, and
miette-backed runtime diagnostics.

Install Copy Chapter

cargo add xqvm

For a no_std target (WASM runtimes, Substrate pallets, embedded):

cargo add xqvm --no-default-features

Quick start Copy Chapter

Build a program with InstructionBuilder, then run it on Vm:

use xqvm::{InstructionBuilder, Vm};

let mut builder = InstructionBuilder::new();
builder.emit_push(10).emit_push(32).emit_add().emit_halt();
let program = builder.build().unwrap();

let mut vm = Vm::new();
vm.run(&program).unwrap();
assert_eq!(vm.stack(), &[42]);

This builds the same four instructions (PUSH 10, PUSH 32, ADD,
HALT) that the xqasm
text assembler produces from source; see that crate to load .xqasm
files instead of building bytecode by hand.

What is in this crate Copy Chapter

Wire format Copy Chapter

A .xqb file opens with a fixed 15-byte XQBC header (magic, version,
calldata/output-slot counts, code length, and a CRC-32 checksum of the
payload), followed immediately by the instruction stream: an opcode byte
followed by its operands in big-endian byte order. See the encoding spec
linked below for the full field layout.

Links out Copy Chapter

• Normative VM spec
• Bytecode encoding spec
• xqasm -- text assembler that emits xqvm::Program
• xqcli -- the xquad CLI, built on this crate
• Repository

License Copy Chapter

AGPL-3.0-or-later.

Overview (`xqvm_py/README.md`) Copy Section

xqvm_py

Status -- transitional. xqvm_py is the executable conformance
oracle for the XQuad toolchain: every vector under
conformance/ must produce identical
observable state on both this Python reference and the Rust xqvm
production runtime. The arrangement is explicitly transitional. Once
the Rust runtime is fully battle-tested, xqvm_py may be dropped
entirely (with conformance vectors graduating to "Rust must
produce exactly these outputs" reference data) or demoted to a
prototyping sandbox for trying out new opcodes / VM features in
Python before they earn a spec slot. Do not build infrastructure
that hard-depends on xqvm_py's existence.

Python reference implementation of the X-Quadratic Virtual Machine.
See spec/xqvm/SPEC.md for the authoritative
technical specification.

Scope Copy Chapter

• Pure-Python executor, state model, opcodes, xqmx
  (sparse quadratic matrix), vector, and tracer.
• No assembler or disassembler: the Rust xqasm crate is the only
  implementation, exposed to Python via xqffi.asm (pyo3). Tests
  and the CLI shim call
  xqvm_py.program_from_xqasm to turn .xqasm text
  into an executable Program.

Layout Copy Chapter

xqvm_py/                  <-- this directory IS the package (flat layout)
  __init__.py             re-exports the public surface (Executor, Program, ...)
  __main__.py             entry point for `python -m xqvm_py`
  executor.py             fetch-decode-execute loop
  state.py                stack, registers, loop control, jump table
  opcodes.py              Opcode enum + operand metadata
  program.py              Program dataclass + program_from_xqasm()
  xqmx.py                 sparse quadratic matrix (model + sample modes)
  vector.py               typed vec<int> / vec<xqmx>
  errors.py               typed runtime errors
  tracer.py               step-by-step execution tracer
  cli/                    python -m xqvm_py run ...
  tests/                  pytest suite (wheel-excluded)

Quick start Copy Chapter

From the xquad workspace root:

uv sync                                       # installs xqvm_py editable + xqffi via maturin
uv run pytest xqvm_py/tests                   # run the full test suite
echo "PUSH 5
PUSH 3
ADD
HALT" > /tmp/prog.xqasm
uv run python -m xqvm_py run /tmp/prog.xqasm  # CLI shim

Programmatic use:

from xqvm_py import Executor, program_from_xqasm

prog = program_from_xqasm("PUSH 10\nPUSH 5\nADD\nSTOW r0\nHALT\n")
executor = Executor()
executor.execute(prog)
print(executor.state.get_register(0))  # 15

Conformance Copy Chapter

Behavioural parity with the Rust xqvm crate is enforced by the
xquad-conformance Rust test harness at
conformance/. New VM semantics require a new
vector. Divergence between implementations fails CI with no "drift
tracking" middle ground.

Overview (`examples/bin_packing/README.md`) Copy Section

Bin Packing

Pack N items with given integer sizes into the minimum number of bins, each
with a fixed capacity C.

QUBO formulation Copy Chapter

• Input: N item sizes (Vec), number of bins B, bin capacity C
• Model: (N + 1) * B binary variables in an (N + 1) x B grid. Rows 0..N-1 are the assignment cells: x[i,b] = 1 if item i is placed in bin b. Row N holds one indicator per bin: y[b] = 1 if bin b is open.
• Objective: +BIN_COST on each indicator y[b], so the energy counts the bins the packing opens. A bias spread over the assignment cells instead would be identically N on every feasible packing, because each item lands in exactly one bin, and could not tell a one-bin packing from a three-bin one.
• Constraints:
  • Assignment per item i: sum_b x[i,b] = 1 (ONEHOTR, penalty 200)
  • Linking per (i, b): x[i,b] -> y[b] (IMPLIES, penalty 200)
  • Capacity per bin b: sum_i s_i * x[i,b] <= C (SLACK + EQUALITY, penalty 100)

The capacity inequality is encoded by appending binary slack variable entries
to the column index/coefficient vectors, converting it to a weighted equality.
Each bin gets its own slack block: bin b's entries start at
(N + 1) * B + b * bitlen(C), past every model variable and past every
earlier bin's block. Sharing one start index across bins would let one bin's
slack absorb another's overflow, leaving the capacity constraint
under-constrained.

DSL methods used Copy Chapter

• model.apply_onehot_row(row, penalty) -- ONEHOTR assignment constraint
• model.apply_implies(coord_a, coord_b, penalty) -- IMPLIES linking constraint
• problem.vec() -- allocate untyped vector registers for indices and coefficients
• problem.slack(indices, coeffs, start_index, capacity) -- append slack entries
• model.apply_equality(indices, coeffs, target, penalty) -- EQUALITY constraint
• xq_bitlen(value) -- BITLEN, used to size each bin's slack block

Pipeline overview Copy Chapter

1. CP (xqcp) -- generate random item sizes, declare an (N + 1) x B binary grid, and add ONEHOTR assignment constraints per item, IMPLIES links per cell, and SLACK + EQUALITY capacity constraints per bin.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary, the per-item assignment, the bin-usage links and the per-bin capacity, then computes energy
6. Decode -- decoder extracts the bin assignments

Usage Copy Chapter

uv run python examples/bin_packing/runner.py --seed 42
uv run python examples/bin_packing/runner.py --n 5 --bins 4 --interpreter rust

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/cubic_opt/README.md`) Copy Section

Cubic Optimization

Minimise a cubic pseudo-Boolean objective over binary variables via single-stage
HOBO degree reduction.

QUBO formulation Copy Chapter

• Input: N binary variables, M cubic interaction terms (i, j, k, c)
• Model: N binary variables. Linear bias -1 per variable rewards selection, creating tension with the positive cubic terms.
• Objective: sum(c_t * x_i * x_j * x_k) - sum(x_v)

Each cubic term (i, j, k, c) is degree-reduced to quadratic via:

1. REDUCE(i, j, P_AUX) -> w -- allocates auxiliary variable w with Rosenberg enforcement P_AUX*(x_i*x_j - 2*x_i*w - 2*x_j*w + 3*w)
2. ADDQUAD(w, k, c) -- adds c*w*x_k = c*x_i*x_j*x_k to the QUBO

DSL methods used Copy Chapter

• model.reduce(var_a, var_b, p_aux) -- single-stage HOBO degree reduction

Pipeline overview Copy Chapter

1. CP (xqcp) -- generate random cubic interaction terms, declare binary variables with linear bias, and degree-reduce each cubic term via REDUCE.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary and that each Rosenberg REDUCE auxiliary equals the product it stands for, then computes energy
6. Decode -- decoder extracts the variable assignment

Usage Copy Chapter

uv run python examples/cubic_opt/runner.py --seed 42
uv run python examples/cubic_opt/runner.py --n 5 --m 4 --interpreter rust

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/graph_coloring/README.md`) Copy Section

Graph Coloring

Assign one of C colors to each node of an undirected graph such that no two
adjacent nodes share the same color (proper C-coloring).

QUBO formulation Copy Chapter

• Input: number of nodes N, number of colors C, edge list
• Model: N categorical variables over C cases. Domain.CATEGORICAL records that as an N x C binary grid, x[v,c] = 1 if node v gets color c, with a one-hot row per node.
• Objective: none. The problem is pure constraint satisfaction: a colouring is scored only by its constraint violations. A valid C-colouring scores -penalty * N, not 0, because XQMX has no constant-term field and each satisfied ONEHOTR stores -penalty rather than 0. That is -1000 at the --n 5, penalty 200 defaults. The colour count defaults to 4 because a G(5, 0.5) graph routinely contains a 4-clique -- the default seed's does -- and a 4-clique has no 3-colouring, so --colors 3 would make the canonical instance unsatisfiable. See Constraints.
• Constraints:
  • One-hot per node: sum_c x[v,c] = 1 (ONEHOTR, penalty 200) -- implied by the domain, not written
  • Exclusion per (edge, color): x[u,c] + x[v,c] <= 1 (EXCLUDE, penalty 200)

Encoding strategy Copy Section

The one-hot row per node is what makes a categorical variable categorical, so
define_model(domain=Domain.CATEGORICAL, k=C, penalty=200) emits it: the grid
and one ONEHOTR per row, through the same record paths a hand-written loop
would use. The compiled program is what this example emitted before the
domain existed.

EXCLUDE is applied per (edge (u,v), color c) pair via a nested range loop.
The 2D coordinates (u, c) and (v, c) are resolved to flat indices using
IDXGRID: u * num_colors + c and v * num_colors + c.

Reading the answer back is sample.case(v), a ROWFIND for the 1 in node v's
row. ROWFIND returns -1 where a row holds no 1, which is the uncoloured
sentinel this example used to produce in host code.

DSL methods used Copy Chapter

• problem.define_model(size=N, domain=Domain.CATEGORICAL, k=C, penalty=200) -- the grid and its one-hot rows
• model.apply_exclude((u, c), (v, c), penalty) -- EXCLUDE per edge per color
• sample.case(node) -- the case a node took, or -1

Pipeline overview Copy Chapter

1. CP (xqcp) -- generate a random graph, declare N categorical variables over C cases, and add EXCLUDE constraints per (edge, color) pair.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary, the one-hot row sums, and the per-edge exclusions, then computes energy
6. Decode -- decoder reads each node's case with ROWFIND, giving one color index per node

Usage Copy Chapter

uv run python examples/graph_coloring/runner.py --seed 42
uv run python examples/graph_coloring/runner.py --n 6 --colors 4 --interpreter rust

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/knapsack/README.md`) Copy Section

Knapsack

The 0/1 Knapsack problem: given N items with integer weights and values,
select a subset maximising total value subject to a weight capacity constraint.

QUBO formulation Copy Chapter

• Input: N item weights and values, capacity W
• Model: N binary variables. x_i = 1 means item i is selected.
• Objective: minimise -sum(v_i * x_i)
• Constraints: capacity sum(w_i * x_i) <= W (SLACK + EQUALITY)

The inequality is encoded via SLACK + EQUALITY. SLACK appends binary slack
variable entries (s_j with coefficients 2^j) to the index and coefficient
vectors, converting the inequality to the equality sum(w_i*x_i) + sum(s_j*2^j) = W.
EQUALITY then adds the penalty term P*(sum(a_k*x_k) - W)^2 to the QUBO.

DSL methods used Copy Chapter

• problem.vec() -- allocate untyped vector registers for indices and coefficients
• problem.slack(indices, coeffs, start_index, capacity) -- append slack entries
• model.apply_equality(indices, coeffs, target, penalty) -- EQUALITY constraint

Pipeline overview Copy Chapter

1. CP (xqcp) -- generate random item weights and values, declare binary variables, and encode the capacity inequality via SLACK + EQUALITY.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary and that the capacity constraint holds, then computes energy
6. Decode -- decoder extracts the item selection

Usage Copy Chapter

uv run python examples/knapsack/runner.py --seed 42
uv run python examples/knapsack/runner.py --n 6 --interpreter rust

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/max3sat/README.md`) Copy Section

Max-3-SAT

Given M clauses of 3 positive literals over N binary variables, find the
assignment that satisfies the maximum number of clauses.

QUBO formulation Copy Chapter

• Input: N binary variables, M clauses of 3 positive literals
• Model: N binary variables. x_v in {0, 1}.
• Objective: minimise sum over clauses of P*(1-x_i)(1-x_j)(1-x_k)

A clause (i,j,k) is violated when all three variables are 0. Expanding
the product (dropping the constant term):

P*(-x_i - x_j - x_k + x_i*x_j + x_i*x_k + x_j*x_k - x_i*x_j*x_k)

The cubic term -P*x_i*x_j*x_k is degree-reduced via REDUCE(i, j) -> w,
introducing one auxiliary variable w per clause with Rosenberg enforcement
P_AUX*(x_i*x_j - 2*x_i*w - 2*x_j*w + 3*w). The cubic term becomes the
quadratic term -P*w*x_k.

DSL methods used Copy Chapter

• model.reduce(var_a, var_b, p_aux) -- HOBO degree reduction; returns a
  RegLoad holding the auxiliary variable index for chaining into quadratic terms

Pipeline overview Copy Chapter

1. CP (xqcp) -- generate random 3-literal clauses, declare binary variables, and degree-reduce the cubic violation terms via REDUCE.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary and that each Rosenberg REDUCE auxiliary equals the product it stands for, then computes energy
6. Decode -- decoder extracts the variable assignment

Usage Copy Chapter

uv run python examples/max3sat/runner.py --seed 42
uv run python examples/max3sat/runner.py --n 8 --m 10 --interpreter rust

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/max_independent_set/README.md`) Copy Section

Max Independent Set

Find the largest subset of nodes in an undirected graph such that no two
selected nodes share an edge.

QUBO formulation Copy Chapter

• Input: number of nodes N, edge list
• Model: N binary variables. x_i = 1 if node i is in the independent set.
• Objective: minimise -sum(x_i) (maximise set size)
• Constraints: per edge (i,j): x_i + x_j <= 1 (SLACK + EQUALITY)

Each edge inequality is encoded via SLACK + EQUALITY. A single binary slack
variable s (capacity = 1) converts x_i + x_j <= 1 into the equality
x_i + x_j + s = 1, and EQUALITY adds the penalty P*(x_i + x_j + s - 1)^2.

Slack variable indices start at num_nodes and are allocated one per edge.

DSL methods used Copy Chapter

• problem.vec() -- allocate untyped vector registers for indices and coefficients
• problem.slack(indices, coeffs, start_index, capacity) -- append one slack entry per edge
• model.apply_equality(indices, coeffs, target, penalty) -- EQUALITY constraint

Pipeline overview Copy Chapter

1. CP (xqcp) -- generate a random graph, declare binary variables (one per node), and encode each edge independence constraint via SLACK + EQUALITY.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary and that the independence constraints hold, then computes energy
6. Decode -- decoder extracts the selected nodes

Usage Copy Chapter

uv run python examples/max_independent_set/runner.py --seed 42
uv run python examples/max_independent_set/runner.py --n 7 --interpreter rust

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/maxcut/README.md`) Copy Section

Max-Cut

Find a 2-colour partition of a weighted graph that maximises the total weight
of edges crossing the partition.

QUBO formulation Copy Chapter

• Input: num_nodes (int), edges (Vec of flat (i, j, w) triples, 3*|E| entries)
• Model: n binary variables, one per node. x[v] in {0, 1} selects the side of the cut.
• Objective: for each edge (i, j, w), add -w*(x_i + x_j) and +2w*x_i*x_j. Minimising this minimises -sum w*[x_i != x_j], i.e. maximises the cut.

DSL methods used Copy Chapter

• problem.input() -- declare typed calldata inputs
• problem.define_model() -- allocate binary XQMX model
• problem.stow() -- bind intermediate computations to named registers
• problem.range() -- emit RANGE loops
• model.linear[i].add() -- accumulate linear bias on variable i
• model.quadratic[i, j].add() -- accumulate quadratic coupling between variables i and j
• problem.output() -- declare typed output slots
• problem.sample.getline() -- read a row from the sample bitstring

Pipeline overview Copy Chapter

1. CP (xqcp) -- build a random weighted complete graph, declare binary variables (one per node), and add linear/quadratic QUBO terms per edge.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary, then computes energy; this problem declares no constraints for it to check
6. Decode -- decoder extracts the 2-colour partition

Usage Copy Chapter

uv run python examples/maxcut/runner.py --seed 42
uv run python examples/maxcut/runner.py --n 6 --seed 7 -o /tmp/mc.json

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/number_partition/README.md`) Copy Section

Number Partitioning

Given N positive integers, find a way to split them into two subsets of
equal sum (or as close as possible if an exact split does not exist).

QUBO formulation Copy Chapter

• Input: N positive integers a_i
• Model: N binary variables. x_i = 1 puts number a_i in subset A.
• Objective: minimise P * (sum(a_i * x_i) - S/2)^2 where S = sum(a_i)

An exact partition exists when S is even and the penalty evaluates to zero.
The QUBO minimiser finds the balanced partition when one exists, or the
most balanced split when the total is odd.

DSL methods used Copy Chapter

• problem.vec() -- allocate untyped vector registers for indices and coefficients
• model.apply_equality(indices, coeffs, target, penalty) -- EQUALITY constraint

Pipeline overview Copy Chapter

1. CP (xqcp) -- generate random positive integers, declare binary variables (one per number), and encode the half-sum equality constraint via EQUALITY.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary and that the partition constraint holds, then computes energy
6. Decode -- decoder extracts the subset assignment

Usage Copy Chapter

uv run python examples/number_partition/runner.py --seed 42
uv run python examples/number_partition/runner.py --n 8 --interpreter rust

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/portfolio_opt/README.md`) Copy Section

Portfolio Optimization

Select a portfolio of exactly B assets from N candidates to maximise expected
return while penalising higher-order risk cross-interactions.

QUBO formulation Copy Chapter

• Input: N asset returns, cubic risk interactions (i, j, k, sigma), budget B
• Model: N binary variables. x_i = 1 if asset i is selected.
• Objective: -sum(r_i * x_i) + sum(sigma_ijk * x_i * x_j * x_k) -- first term maximises return (minimising its negation), second penalises correlated three-asset risk interactions.
• Constraints: budget sum(x_i) = B (EQUALITY with unit coefficients, penalty 200)

Encoding strategy Copy Section

Return terms are linear: ADDLINE(i, -r_i) per asset.

Cubic risk terms (i, j, k, sigma) are degree-reduced:

1. REDUCE(i, j, P_AUX) -> w (Rosenberg enforcement for w = x_i * x_j)
2. ADDQUAD(w, k, sigma) (sigma * w * x_k = sigma * x_i * x_j * x_k)

Budget constraint builds uniform-coefficient index/coeff vecs then calls
EQUALITY with target = B and penalty = 200. EQUALITY is emitted after all
objective (body) actions because it lands in the constraint section.

DSL methods used Copy Chapter

• model.reduce(var_a, var_b, p_aux) -- HOBO degree reduction for cubic risk terms
• problem.vec() -- allocate index/coefficient vecs for the budget constraint
• model.apply_equality(indices, coeffs, target, penalty) -- budget EQUALITY

Pipeline overview Copy Chapter

1. CP (xqcp) -- generate random returns and cubic risk interactions, declare binary variables, degree-reduce risk terms via REDUCE, and add a budget EQUALITY constraint.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary, that the budget constraint holds, and that each REDUCE auxiliary equals the product it stands for, then computes energy
6. Decode -- decoder extracts the selected assets

Usage Copy Chapter

uv run python examples/portfolio_opt/runner.py --seed 42
uv run python examples/portfolio_opt/runner.py --n 6 --budget 3 --interpreter rust

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/portfolio_rebalance/README.md`) Copy Section

Portfolio Rebalance

Choose a signed integer weight for each asset, trading expected return off
against a risk matrix, subject to the weights summing to a budget. Negative
weights are short positions, which is the whole reason this example is not a
binary select-or-not model.

QUBO formulation Copy Chapter

• Input: number of assets N, a return per asset, a symmetric N x N risk matrix flattened row-major
• Model: N integer variables x_i in [-5, 5], declared with lo=/hi=. The model holds y_i = x_i - lo in {0, ..., 10}; coefficients are written over x and sample.value() shifts back on the way out.
• Objective: -sum(r_i * x_i) + sum_{i <= j} C_ij * x_i * x_j
• Constraint: sum(x_i) = B, as the penalty P * (sum_i x_i - B)^2
• Energy: shifted twice over, and not comparable with any other example's. The ranged domain drops the constant that substituting x = y + lo produces, because XQMX carries no offset field, and the budget square drops its own P*B^2 the way EQUALITY does. Both shifts are uniform across assignments, so argmin is exact even though the number is not the objective's true value.

Encoding strategy Copy Section

The budget constraint is written out by hand rather than handed to
apply_equality. Every high-level constraint in the VM expands under
x^2 = x, which holds for binary variables only, so xqcp refuses all of them
off a binary model. Expanded, P * (sum_i x_i - B)^2 is P on each diagonal,
2P on each off-diagonal pair, and -2PB on each linear coefficient. Writing
that square is the same work the HLF would have done, and it is what the open
question about per-domain expansions is about.

The ranged domain then does its own rewriting underneath. Each quadratic write
records w*lo against the linear coefficient of both named indices, because
w * x_i * x_j expands to w*y_i*y_j + w*lo*y_i + w*lo*y_j + w*lo^2 once
x = y + lo is substituted. A write to the diagonal lands both corrections on
the one index, giving the 2*w*lo that squaring asks for. None of that is
visible in the model-building code above.

lo and hi are literals. A runtime lo would want the decoder's single
calldata scalar, which the output loop bound already spends, and xqcp raises
naming both rather than picking one.

DSL methods used Copy Chapter

• problem.define_model(size=N, domain=Domain.INTEGER, lo=-5, hi=5) -- ranged integer weights
• model.linear[i].add(w) and model.quadratic[i, j].add(w) -- the only operations a non-binary model supports
• sample.value(i) -- the weight in the domain it was declared over, rather than the stored y

What this example proves Copy Chapter

valid == 1 proves that the domain check, the record-layer shift and the
decode compose on a chosen assignment. It proves nothing about optimisation:
no solver samples an integer model yet, so --solver is accepted, ignored,
and the pipeline runs against a hand-picked weight vector that sits inside the
domain and sums to the budget. Integer lowering is XQSA v0.5.0 work.

Pipeline overview Copy Chapter

1. CP (xqcp) -- generate returns and a symmetric risk matrix, declare N ranged integer weights, and write the objective and the budget square as coefficients
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- skipped; the runner supplies the assignment itself
5. Verify -- verifier checks every weight is inside {0, ..., 10} against the k replayed from define_model, then computes energy
6. Decode -- decoder reads each weight and adds lo, giving the signed weights back

Usage Copy Chapter

uv run python examples/portfolio_rebalance/runner.py --seed 42
uv run python examples/portfolio_rebalance/runner.py --n 6 --interpreter rust

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/quartic_opt/README.md`) Copy Section

Quartic Optimization

Minimise a degree-4 pseudo-Boolean objective via two-stage REDUCE chaining.

QUBO formulation Copy Chapter

• Input: N binary variables, M quartic interaction terms (i, j, k, l, c)
• Model: N binary variables. Linear bias -1 per variable rewards selection, creating tension with the positive quartic terms.
• Objective: sum(c_t * x_i * x_j * x_k * x_l) - sum(x_v)

Each quartic term (i, j, k, l, c) is encoded via two-stage REDUCE:

1. w = REDUCE(i, j, P_AUX) -- introduces auxiliary w; w approximates x_i*x_j.
2. v = REDUCE(w, k, P_AUX) -- introduces auxiliary v; v approximates w*x_k = x_i*x_j*x_k. Here w is the variable index returned from the first REDUCE.
3. ADDQUAD(v, l, c) -- adds c*v*x_l = c*x_i*x_j*x_k*x_l to the QUBO.

Each quartic term allocates 2 auxiliary variables. With M terms, the model
grows by 2*M variables beyond the original N.

DSL methods used Copy Chapter

• model.reduce(var_a, var_b, p_aux) -- two chained HOBO degree reductions;
  the RegLoad returned by the first REDUCE is passed as var_a to the second

Pipeline overview Copy Chapter

1. CP (xqcp) -- generate random quartic interaction terms, declare binary variables with linear bias, and two-stage degree-reduce each quartic term via chained REDUCE.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary and that each Rosenberg REDUCE auxiliary equals the product it stands for, then computes energy
6. Decode -- decoder extracts the variable assignment

Usage Copy Chapter

uv run python examples/quartic_opt/runner.py --seed 42
uv run python examples/quartic_opt/runner.py --n 6 --m 3 --interpreter rust

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/set_cover/README.md`) Copy Section

Set Cover

Given a universe of E elements and a collection of S sets, find the minimum
sub-collection whose union equals the universe.

QUBO formulation Copy Chapter

• Input: number of elements E, number of sets S, coverage membership matrix (flat Vec of E*S entries, covers[e][s] = 1 if set s covers element e)
• Model: S binary variables. x_s = 1 if set s is selected.
• Objective: minimise sum(x_s)
• Constraints: per element e: sum_{s: covers[e][s]=1} x_s >= 1 (ATLEAST with k=1)

For each element, the encoder iterates over all sets and uses a branch to
conditionally push only covering set indices into the element's index vector.
ATLEAST then enforces that at least one covering set is selected.

DSL methods used Copy Chapter

• problem.vec() -- allocate a vector register for each element's covering set indices
• problem.branch(cond, arm, default) -- conditional VECPUSH based on coverage membership
• model.apply_atleast(indices, k, penalty) -- ATLEAST constraint with k=1

Pipeline overview Copy Chapter

1. CP (xqcp) -- generate a random coverage matrix, declare binary variables (one per set), and encode per-element coverage constraints via conditional branching and ATLEAST.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary and that every element is covered, then computes energy
6. Decode -- decoder extracts the selected sets

Usage Copy Chapter

uv run python examples/set_cover/runner.py --seed 42
uv run python examples/set_cover/runner.py --num-sets 6 --interpreter rust

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/tsp/README.md`) Copy Section

TSP -- Travelling Salesman Problem

Find the shortest Hamiltonian tour through N cities given a random symmetric
distance matrix.

QUBO formulation Copy Chapter

• Input: num_cities (int), distance_matrix (Vec, flat upper triangle, n*(n-1)/2 entries)
• Model: an n x n binary grid. x[i, p] = 1 means city i is at tour position p.
• Objective: sum of distances between consecutive positions in the tour.
• Constraints: one-hot row (each city at exactly one position) and one-hot column (each position holds exactly one city), both with penalty 100.

Hamiltonian Copy Chapter

The Hamiltonian is the sum of three terms:

$$H = H_{\text{dist}} + H_{\text{row}} + H_{\text{col}}$$

\(H_{\text{dist}}\) is the tour length. For every pair of cities \(i < j\) and
every position \(p\), a term fires whichever direction the tour visits them
in -- city i at p and city j at the next position, or the reverse:

$$H_{\text{dist}} = \sum_{i<j} \sum_{p=0}^{n-1} d_{ij} \left( x_{i,p}, x_{j,(p+1) \bmod n} + x_{j,p}, x_{i,(p+1) \bmod n} \right)$$

\(H_{\text{row}}\) and \(H_{\text{col}}\) are the one-hot constraints
apply_onehot_row and apply_onehot_col add, at penalty \(P = 100\):

$$H_{\text{row}} = P \sum_{i=0}^{n-1} \left( \sum_{p=0}^{n-1} x_{i,p} - 1 \right)^2, \qquad H_{\text{col}} = P \sum_{p=0}^{n-1} \left( \sum_{i=0}^{n-1} x_{i,p} - 1 \right)^2$$

XQMX has no field for a constant term. Each satisfied one-hot constraint
drops its +P and leaves -P in the stored model instead of 0 -- see
Constraints.

\(H_{\text{row}}\) forces each city onto exactly one position; \(H_{\text{col}}\)
forces each position to hold exactly one city. Both terms are zero as
written on a valid tour, so they never change which valid tour is
shortest -- but because of the dropped constant above, what a satisfied
constraint actually contributes is -P, not 0. That is the
-2 * P * n = -800 term in the worked example below. A violation (a
city visiting two positions, or a position holding two cities) still
costs more than a satisfied constraint.

Whether that makes every invalid grid's energy exceed every valid
tour's depends on \(P\) relative to the tour-length difference a
violation can buy back.
Constraints
gives the general criterion. At \(P = 100\) it holds for this
seed-42, 4-city instance. The best invalid grid scores -581, 6
above the worst valid tour's -587. It does not hold at every instance
where \(P = 100\) is used. At --n 5 --seed 7, the second command
under Usage below, an invalid grid scores -770, below 40 of the
120 valid tours.

DSL methods used Copy Chapter

• problem.input() -- declare typed calldata inputs
• problem.define_model() -- allocate binary 2D grid XQMX model
• problem.stow() -- bind intermediate computations to named registers
• problem.range() -- emit RANGE loops
• model.quadratic[(city_i, pos), (city_j, pos)].add() -- accumulate quadratic coupling using 2D grid coordinates
• model.apply_onehot_row() -- ONEHOTR constraint per city
• model.apply_onehot_col() -- ONEHOTC constraint per position
• problem.output() -- declare typed output slots
• problem.sample.colfind() -- find the row index with value 1 in a given column

Pipeline overview Copy Chapter

1. CP (xqcp) -- build a random symmetric distance matrix, declare an n x n binary grid, and add quadratic distance terms plus one-hot row/column constraints.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary and the one-hot row and column constraints, then computes energy
6. Decode -- decoder extracts the tour as a sequence of city indices

Steps 3-6 are three independent XQVM programs plus a solver call in between,
sharing data only through calldata and outputs:

flowchart LR
    ENC[Encoder] -->|model| SLV[xqsa solver]
    ENC -->|model| VER[Verifier]
    SLV -->|sample| VER
    SLV -->|sample| DEC[Decoder]
    VER -->|energy, valid| OUT[Host program]
    DEC -->|tour| OUT

The encoder's calldata is num_cities, distance_matrix; the verifier's is
model, sample, num_cities; the decoder's is sample, num_cities. See
Three Programs for why the
split exists.

Worked example Copy Chapter

uv run python examples/tsp/runner.py --n 4 --seed 42 builds this
4-city instance (edge labels are distance_matrix, indexed by the
upper-triangle position of each city pair):

graph LR
    0 ---|82| 1
    0 ---|15| 2
    0 ---|95| 3
    1 ---|4| 2
    1 ---|36| 3
    2 ---|32| 3

Both interpreters return the same tour:

{
  "_note": "canonical CI golden",
  "_seed": 42,
  "energy": -650,
  "n": 4,
  "tour": [0, 2, 1, 3],
  "tour_distance": 150,
  "valid": 1
}

tour_distance is d(0,2) + d(2,1) + d(1,3) + d(3,0) = 15 + 4 + 36 + 95 = 150, matching \(H_{\text{dist}}\) for a valid tour. energy is
H_{\text{dist}} + H_{\text{row}} + H_{\text{col}}: on a valid tour, each
of the 4 rows and 4 columns contributes its one active variable's -P
linear term and nothing from the quadratic term (no two variables in the
same row or column are both 1), for -P * n per constraint family, so
energy = tour_distance - 2 * P * n = 150 - 2 * 100 * 4 = -650, matching
the run.

Usage Copy Chapter

uv run python examples/tsp/runner.py --seed 42
uv run python examples/tsp/runner.py --n 5 --seed 7 -o /tmp/tsp.json

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/vertex_cover/README.md`) Copy Section

Vertex Cover

Find the minimum subset of vertices such that every edge in an undirected
graph has at least one endpoint in the subset.

QUBO formulation Copy Chapter

• Input: number of nodes N, edge list
• Model: N binary variables. x_v = 1 if vertex v is in the cover.
• Objective: minimise sum(x_v)
• Constraints: per edge (i,j): x_i + x_j >= 1 (ATLEAST with k=1)

The at-least-1 constraint is encoded directly with ATLEAST. For each edge,
ATLEAST allocates one slack variable at model.size and adds the penalty
P*(x_i + x_j - 1 - s)^2, where s in {0,1} accounts for the case when
both endpoints are selected (sum = 2).

DSL methods used Copy Chapter

• problem.vec() -- allocate a vector register for the two endpoint indices per edge
• model.apply_atleast(indices, k, penalty) -- ATLEAST constraint with k=1

Pipeline overview Copy Chapter

1. CP (xqcp) -- generate a random graph, declare binary variables (one per vertex), and encode per-edge coverage constraints via ATLEAST.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary and that every edge is covered, then computes energy
6. Decode -- decoder extracts the selected vertices

Usage Copy Chapter

uv run python examples/vertex_cover/runner.py --seed 42
uv run python examples/vertex_cover/runner.py --n 7 --interpreter rust

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`examples/weighted_set_cover/README.md`) Copy Section

Weighted Set Cover

A generalisation of Set Cover where each set s has a coverage capacity cap[s]
and each element e has a demand demand[e]. The goal is to select sets of
minimum total cost such that the total capacity of covering selected sets
meets each element's demand.

QUBO formulation Copy Chapter

• Input: number of elements E, number of sets S, set costs, set capacities, element demands, coverage membership matrix
• Model: S binary variables. x_s = 1 if set s is selected.
• Objective: minimise sum(cost[s] * x_s)
• Constraints: per element e: sum_{s: covers[e][s]=1} cap[s] * x_s >= demand[e] (ATLEASTW)

For each element, a branch conditionally pushes (set index, capacity) pairs
into per-element index/coefficient vectors, then ATLEASTW enforces the
weighted threshold.

DSL methods used Copy Chapter

• problem.vec() -- allocate vector registers for covering set indices and capacities
• problem.branch(cond, arm, default) -- conditional VECPUSH based on coverage membership
• model.apply_atleastw(indices, coeffs, k, penalty) -- ATLEASTW constraint

Pipeline overview Copy Chapter

1. CP (xqcp) -- generate a random weighted coverage instance, declare binary variables (one per set), and encode per-element weighted demand constraints via conditional branching and ATLEASTW.
2. Assemble -- .xqasm text to bytecode via xquad.asm
3. Encode -- run encoder on chosen XQVM to produce the XQMX model
4. Sample -- solver runs SA/QPU/GPU over the model
5. Verify -- verifier checks the sample is binary and that every demand is met, then computes energy
6. Decode -- decoder extracts the selected sets

Usage Copy Chapter

uv run python examples/weighted_set_cover/runner.py --seed 42
uv run python examples/weighted_set_cover/runner.py --num-sets 6 --interpreter rust

Choosing a solver Copy Chapter

See GPU/QPU installation for driver
prerequisites and xqsa solver quick-starts for
per-solver parameter tuning.

Non-default solvers will not reproduce the canonical output (different
RNG/hardware). example-smoke always runs dwave-cpu.

Canonical output Copy Chapter

example-smoke validates both interpreters produce valid == 1 with
--seed 42 --solver dwave-cpu. The smoke test is invariant-based --
it checks validity, not exact output.

Overview (`spec/xqcp/README.md`) Copy Section

XQCP Specification

Authoritative specification for X-Quadratic Constraint Programming. The spec is split across focused documents; each is the single source of truth for its topic.

Documents Copy Chapter

Reference implementation Copy Chapter

../../xqcp/ -- Python package. The spec is reverse-engineered from this reference; once landed, the spec is authoritative and any divergence in the reference is a bug.

Related specifications Copy Chapter

• XQVM -- the virtual machine that executes the compiled programs
• XQSA -- solver adapters that sit between the encoder and verifier in the pipeline

Overview (`spec/xqsa/README.md`) Copy Section

XQSA Specification

Authoritative specification for X-Quadratic Solver Adapters. The spec is split across focused documents; each is the single source of truth for its topic.

Documents Copy Chapter

Reference implementation Copy Chapter

../../xqsa/ -- Python package. v0.3.0 implements SolverDWaveCPU wrapping dwave-samplers simulated annealing.

Related specifications Copy Chapter

• XQVM -- the virtual machine that executes encoder, verifier, and decoder programs around the solver
• XQCP -- the constraint-programming DSL that compiles problems into XQVM programs and XQMX models

Overview (`spec/xqvm/README.md`) Copy Section

XQVM Specification

Authoritative specification for the X-Quadratic Virtual Machine. The spec is split across focused documents; each is the single source of truth for its topic.

Documents Copy Chapter

Overview (`docs/book/src/README.md`) Copy Section

Introduction

XQuad is a hardware-agnostic toolchain for expressing and running quadratic
optimisation problems -- QUBO, Ising, and integer formulations -- on quantum
annealers and classical solvers. A problem is written once against the XQVM
instruction set and runs unchanged on any backend the toolchain supports.

Think of it as LLVM for quantum computing: write a problem once, compile
it to XQVM bytecode, and run it on any supported backend.

What XQuad solves Copy Chapter

Combinatorial optimisation problems -- travelling salesman, graph colouring,
knapsack, set cover, and their relatives -- can be expressed as quadratic
binary models and handed to a quantum annealer or a classical sampler. XQuad
gives that pipeline a single intermediate representation, XQVM bytecode, and
a reference virtual machine, so the same compiled program runs on a D-Wave
QPU, a local simulated-annealing sampler, or the Quip network without a
rewrite. See Quadratic Models for what a
QUBO/Ising model actually is, and Backends for the
solvers XQuad targets.

The real components Copy Chapter

The toolchain is dual-language: a Rust core (VM, assembler, bytecode, CLI)
with Python interfaces (reference VM, constraint-programming DSL, solver
adapters, FFI bindings).

Three Rust crates, published to crates.io:

A fourth crate, xqffi,
is a PyO3 bridge that exposes xqvm and xqasm to Python. It ships as a
Python wheel rather than a crates.io library.

Five Python distributions, published to PyPI:

Parity on every committed conformance vector between the Rust xqvm
interpreter and the Python xqvm_py reference VM is enforced mechanically:
each vector runs on both implementations in CI, and disagreement fails the
build. See Conformance for what a vector does
and does not cover.

Architecture at a glance Copy Chapter

XQVM is a stack-based interpreter with a 256-slot register file. The value
stack holds i64 integers; registers hold typed values (RegVal): integers,
integer vectors, QUBO/Ising/integer models (XqmxModel), model vectors, and
candidate solutions (XqmxSample). A dedicated loop stack drives RANGE and
ITER iteration.

The instruction set comprises 93 instructions, declared once in the
opcodes! table at
xqvm/src/bytecode/types/table.rs.
The Opcode enum, the Instruction enum, mnemonic strings, and operand
arity are all derived from that single table.

Every .xqb file opens with a fixed 15-byte XQBC header -- magic bytes,
format version, calldata/output-slot counts, instruction-stream length, and
a CRC-32 checksum -- followed by the raw instruction stream: an opcode byte
followed by its operands in big-endian byte order. See
Bytecode Format for the full field layout.

Where to go next Copy Chapter

• Getting Started -- install the toolchain and run
  your first program.
• Concepts -- what a QUBO/Ising model is, the ways
  to use XQuad, and the backends it targets.
• Modelling with XQCP -- write a problem with the
  constraint-programming DSL.
• Running Programs and
  Solving -- execute a compiled program and hand it
  to a solver.
• XQVM Reference -- the machine model, assembly
  language, instruction set, and bytecode format.
• Embedding -- using the Rust crates directly,
  no_std support, and cross-implementation conformance.
• Examples -- worked problems including a
  Travelling Salesman Problem.

License Copy Chapter

Licensed under the
GNU Affero General Public License v3.0 or later.

Overview (`docs/book/src/concepts/README.md`) Copy Section

Toolchain Map

XQuad turns one problem description into bytecode that runs unchanged on
any backend it supports. This page names the pieces that make that true,
and what each one consumes and produces.

flowchart LR
    P["DSL (xqcp) or hand-written .xqasm"] --> ASM[Assembler]
    ASM --> B[XQVM bytecode]
    B --> V["VM: xqvm or xqvm_py"]
    H[Host program] -->|calldata| V
    V -->|model-building program| M[XQMX model]
    M --> H
    H --> SLV[xqsa solver]
    SLV -->|sample| H
    H -->|sample as calldata| V
    V -->|verifier / decoder programs| H

Following the Pipeline Copy Chapter

A hand-written program can skip most of this. Save the following as
add.xqasm:

; push two integers and add them
PUSH 10
PUSH 32
ADD
HALT

$ xquad asm add.xqasm -o add.xqb
assembled 4 instructions (21 bytes) -> add.xqb
$ xquad run add.xqb
stack (bottom to top):
  42

Here the pipeline is just two rows: the assembler and the VM. The xquad
CLI plays the host program's role, reading add.xqb from disk and
printing the result, and that already runs the real toolchain end to end.
XQVM Reference walks through this same add.xqasm
again, from the machine's side: what each instruction does to the stack as
it runs.

A problem worth handing to a solver uses every row in the table above.
xqcp compiles a Problem into three separate .xqasm programs, not one
-- see Three Programs for what those three are and
why. The first one builds a model; xqsa solves it; the other two check
and decode the answer. A Python host program -- xquad.program,
xqffi.vm, or a full xqcp pipeline -- drives it, injecting calldata
before each VM run and reading outputs back after. See
Ways to Use XQuad for which surface plays that host-program
role in each of the six ways to work with XQuad.

Where to Go From Here Copy Chapter

• Ways to Use XQuad -- the six surfaces that build a
  model and drive execution, and how to pick one.
• Quadratic Models -- what the model in the
  middle of this pipeline actually is, and why constraints become part of
  it.
• Three Programs -- why xqcp compiles a problem
  into three separate programs instead of one.
• Backends -- the solvers that sit in the gap between
  encoder and verifier.

Past this chapter: Modelling builds a model with
the DSL, Running Programs and
Solving Overview execute it and hand it to a
solver, and XQVM Reference is the machine this whole
pipeline compiles down to.

Overview (`docs/book/src/cookbook/README.md`) Copy Section

Cookbook

The fourteen examples under examples/ each solve one problem --
Knapsack, TSP, Graph Coloring -- and each already contains a working
encoding. Nothing in the repository names those encodings as patterns you
can reuse on a problem that is not itself Knapsack or TSP. This chapter
names five recurring shapes instead, each grounded in the example or
examples that embody it and shown as code that actually ran. One further
page covers getting the arithmetic right once a shape is chosen.

This chapter assumes Modelling -- it builds
problems with the same xqcp calls that chapter introduces and does not
re-explain them. It also assumes
Quadratic Models for what a penalty
term is and why one exists at all.

The Five Shapes Copy Chapter

Permutations and Assignment are the same grid with one constraint family
removed -- see Assignment
for the direction that mistake most often runs. Selection Under Budget and
Mutual Exclusion overlap at one boundary: a capacity of exactly 1 on a
pair is the same instruction family EXCLUDE gives you directly, covered
in Mutual Exclusion.
examples/bin_packing/ and examples/graph_coloring/ each compose two of
these shapes in one problem (assignment plus a capacity, and assignment
plus exclusion, respectively) -- reading a problem as "which of these
shapes does each part look like" scales to a combined problem the same
way it does to a single-pattern one.

The Arithmetic Page Copy Chapter

Integer Scaling is not a shape -- every pattern
above needs it, sooner or later, while turning real-valued problem data
into the integer coefficients every pattern above is written in terms of.
Sizing the penalty weight itself, and reading a solver's output to tell
whether a cheap constraint violation bought a good-looking energy, is
Constraints's
territory, not a cookbook page of its own.

Where This Chapter Stops Copy Chapter

None of these pages re-derives what a one-hot, EXCLUDE, or EQUALITY
constraint expands to in linear and quadratic coefficients -- that table
is High-Level Constraints, already
written, and this chapter links to it rather than repeating it. This
chapter is about recognising which instruction family a new problem
needs and what it costs once chosen, not about the instructions
themselves.

Overview (`docs/book/src/embedding/README.md`) Copy Section

Embedding Overview

Everything so far in this book drives XQuad from Python or the xquad CLI.
This chapter is for embedding the Rust crates directly. That means building
bytecode with a fluent Rust API instead of .xqasm text, running it without
a Python process in the loop, and compiling for no_std targets.

Crate Map Copy Chapter

A Rust program that only needs to build and run bytecode depends on xqvm
alone; add xqasm to parse .xqasm source instead of building bytecode by
hand with InstructionBuilder. xqcli is the CLI's own
crate, useful as a reference for wiring the other two together rather than
as a library dependency.

The `no_std` Story Copy Chapter

xqvm builds no_std + alloc. Two layers are always compiled without
std:

• Bytecode -- the opcode table, Instruction, Register,
  InstructionBuilder, Program, and the wire codec.
• Interpreter core -- Vm, Error, RegVal, XqmxModel /
  XqmxSample, the bytecode verifier, and the Tracer trait with its
  no-op implementation.

The std feature, enabled by default, adds three things a no_std
embedder gives up: the disassembler (disasm::Disassembly), miette-backed
runtime diagnostics (RuntimeDiagnostic), and the JsonTracer /
TextTracer implementations. None of these change what a program computes;
they change how a fault or a trace is reported. Build for a no_std target
with:

cargo add xqvm --no-default-features

This is exercised, not just claimed: fixtures/xqvm-wasm is a freestanding
wasm32-unknown-unknown test crate depending on xqvm with
default-features = false, and CI's test:wasm job runs cargo build -p xqvm --target wasm32v1-none --no-default-features followed by
wasm-pack test --node against it. The job is path-gated: it runs on
merge requests and feature branches whenever the diff can reach xqvm or
the fixture, and unconditionally on protected refs and release tags.

Running In-Process, Without `.xqasm` Copy Chapter

Builder API covers InstructionBuilder in full: emitting
instructions one at a time, resolving forward and backward labels, and
reading back the resulting JumpTable. It is the API a no_std embedder
uses when parsing text is not an option.

On-Chain: The Pallet Fixture Copy Chapter

Pallet Fixture documents fixtures/pallet-xqvm, a Substrate
FRAME pallet that embeds xqvm inside a runtime as an integration gate, not
a production deployment path. It is a real, CI-tested example of a no_std
embedder, and the one currently in this repository.

On-Chain: Which Opcodes a Chain May Admit Copy Chapter

On-Chain Admissibility answers which of the 93 opcodes a
runtime embedding xqvm may accept from an untrusted account. The answer is
all of them, because chain compatibility is a property of the instruction set
rather than a per-embedder decision; the page states the bar an opcode has to
clear, where each half of it is enforced, what every family charges, and
which parts of that boundary the tree does not yet enforce.

Checking an Implementation Against the Spec Copy Chapter

Conformance covers the harness that holds the Rust xqvm
and the Python xqvm_py to the same observable behaviour. Read it if you
are embedding xqvm somewhere that needs to trust its output matches the
reference implementation.

Overview (`docs/book/src/examples/README.md`) Copy Section

Examples

Graph problems Copy Chapter

Examples that encode graph cuts, colouring, covers, independent sets, and tours.

• Max-Cut -- Find a 2-colour partition of a weighted graph that maximises the cut weight.
• Graph Coloring -- Assign colours to graph nodes so adjacent nodes do not share a colour.
• Maximum Independent Set -- Select the largest subset of graph nodes with no selected edge between them.
• Vertex Cover -- Select the smallest vertex subset that covers every graph edge.
• Travelling Salesman Problem -- Find the shortest Hamiltonian tour through a random symmetric distance matrix.

Selection and packing Copy Chapter

Examples that select subsets, cover demands, pack bins, and balance integer weights.

• Knapsack -- Select items that maximise value while respecting a capacity constraint.
• Bin Packing -- Pack items into the minimum number of fixed-capacity bins.
• Set Cover -- Select the minimum set collection whose union covers the universe.
• Weighted Set Cover -- Select sets with capacities to cover element demands at minimum cost.
• Number Partition -- Split positive integers into two subsets with nearly equal sums.
• Portfolio Optimization -- Select a fixed-size portfolio while penalising higher-order risk interactions.
• Portfolio Rebalance -- Choose signed integer asset weights against a risk matrix and a budget.

Satisfiability and higher-order Copy Chapter

Examples that reduce clauses and higher-order pseudo-Boolean objectives to quadratic models.

• Max-3-SAT -- Find the assignment that satisfies the maximum number of 3-literal clauses.
• Cubic Optimization -- Minimise a cubic pseudo-Boolean objective through HOBO degree reduction.
• Quartic Optimization -- Minimise a degree-4 pseudo-Boolean objective through two-stage REDUCE chaining.

Overview (`docs/book/src/modelling/README.md`) Copy Section

Modelling Lifecycle

XQCP is a Python-embedded DSL that turns a problem description into three
XQVM assembly programs. You declare a Problem's runtime inputs, allocate
the quadratic model those inputs fill, add objective terms and
constraints, declare what you want back, then call compile(). XQCP
records every call you make against Problem as you make it and only
turns that recording into .xqasm when compile() runs -- see
Compiling for how the recording becomes three programs.

A problem definition follows one call sequence, in order:

Problem(name) -> input()* -> define_model() -> body* -> output()* -> compile()

input() calls come first: Inputs and Model Shape
covers why, and what a declared input becomes at run time. define_model()
runs exactly once and makes problem.model available for the rest of the
body: objective terms, constraints, and loops, in any order, covered
across Expressions, Objectives,
Constraints, and Control Flow. Your
first output() call marks the start of the decoder section, covered in
Outputs and Decoding.

Why XQCP, Not Assembly Copy Chapter

Ways to Use XQuad names six surfaces for
getting a problem into XQuad; XQCP is one of them. Reach for it when you
are modelling a combinatorial problem from scratch and would otherwise
hand-write the same loop-over-variables, add-a-coefficient pattern in
.xqasm three times over, once per program -- Problem records that
pattern once, and the compiler emits all three. Write .xqasm directly
instead when a program is small enough that the three-program duplication
costs nothing to write by hand. Reach for
xqvm::InstructionBuilder
instead when a Rust host is generating programs and adding a Python step
to emit them buys nothing.

One Problem, Once Copy Chapter

Every page in this chapter builds on the same running example:
examples/knapsack/runner.py. It takes item weights, item values, and a
capacity, and chooses the subset of items maximising total value without
exceeding the capacity. build_problem is the whole of it:

def build_problem(n: int, weights: list[int], values: list[int], capacity: int) -> Problem:
    problem = Problem("Knapsack")

    num_items = problem.input("num_items", type=Types.Int)
    weights_in = problem.input("weights", type=Types.Vec)
    values_in = problem.input("values", type=Types.Vec)
    capacity_in = problem.input("capacity", type=Types.Int)

    problem.define_model(size=num_items, domain=Domain.BINARY)

    # Objective: minimise -sum(v_i * x_i)
    with problem.range(0, num_items) as i:
        vi = problem.stow("vi", values_in.get(i))
        problem.model.linear[i].add(-vi)

    # Constraint: sum(w_i * x_i) <= W
    indices = problem.vec()
    coeffs = problem.vec()
    with problem.range(0, num_items) as i:
        indices.push(i)
        coeffs.push(weights_in.get(i))

    problem.slack(indices, coeffs, num_items, capacity_in)
    problem.model.apply_equality(indices, coeffs, capacity_in, 100)

    selected = problem.output("selected", type=Types.Vec)
    with problem.range(0, num_items) as i:
        selected.append(problem.sample.getline(i))

    return problem

One binary variable per item: x_i = 1 means item i is selected.
Four inputs, one 1D binary model sized to num_items, a range loop
building the objective, a second range loop paired with slack and
apply_equality encoding the capacity constraint, and a decoder loop
reading the solved sample back into a selected vector. Running it end
to end:

$ uv run python examples/knapsack/runner.py --seed 42
{
  "_note": "canonical CI golden",
  "_seed": 42,
  "capacity": 18,
  "energy": -32446,
  "n": 5,
  "selection": [
    1,
    1,
    1,
    0,
    1
  ],
  "total_value": 46,
  "total_weight": 12,
  "valid": 1,
  "values": [
    5,
    4,
    18,
    3,
    19
  ],
  "weights": [
    2,
    1,
    5,
    4,
    4
  ]
}

_note and _seed are the runner's own bookkeeping, the same as in
Three Programs. energy
is the full model's Hamiltonian, capacity constraint included, so it is
not simply -total_value here the way Max-Cut's energy is -cut_weight
-- Objectives isolates just the objective term's
contribution, and Constraints covers what the rest of
energy is paying for.

This run is not the optimum: the five weights sum to 16, under the
capacity of 18, so every item fits and the true best value is 49, not
the 46 printed above. A heuristic solver returns a good sample, not a
proven best one. valid: 1 reports only the verifier's binary-domain
check here, not the capacity constraint; see
Compiling for
what a verifier actually checks.

Inputs and Model Shape starts with the four
problem.input() calls and the define_model() line above; the rest of
the chapter works through the remaining lines in the order they appear.

Where to Go From Here Copy Chapter

• Inputs and Model Shape -- runtime inputs and
  the 1D/2D model they fill.
• Expressions -- the operators and functions that
  build a coefficient or a loop bound.
• Objectives -- turning "minimise this" into
  linear/quadratic coefficients, sign included.
• Constraints -- folding a rule into the objective
  as a penalty.
• Control Flow -- range, iter, and branch.
• Outputs and Decoding -- reading a solved
  sample back into your problem's own terms.
• Compiling -- what problem.compile() actually
  produces.

Overview (`docs/book/src/running/README.md`) Copy Section

Running Programs

This page covers driving an already-compiled .xqasm or .xqb program from
Python: loading it, supplying calldata, running it, and reading outputs back.
Ways to Use XQuad names the surfaces; this page
is the full coverage for three of them: xquad.program, and the two VM
wrappers underneath and alongside it. For writing a problem with the xqcp
DSL, see
Modelling. For what xquad verify checks and how
to fix a rejected program, see Verification.

Every example on this page ran against the Rust backend, the default for
both xquad.program and xquad.vm.VM.

Program and Session Copy Chapter

xquad.program.Program loads a program once; Program.session() gives you
a Session you call .run() on repeatedly, each time with fresh calldata.
Each run returns a RunResult with dict-keyed outputs, the residual stack,
and the step count:

from xquad.program import Program

src = """
PUSH 0
INPUT r0
PUSH 1
INPUT r1
LOAD r0
LOAD r1
ADD
STOW r2
PUSH 0
OUTPUT r2
HALT
"""

program = Program.from_source(src)
assert program.instruction_count == 11
assert program.source is not None   # retained for debugging

session = program.session(output_slots=4)
session.set_calldata([40, 2])
result = session.run()

assert dict(result.outputs) == {0: 42, 1: None, 2: None, 3: None}
assert result.stack == []
assert result.steps == 11

# Re-run with different calldata -- sessions carry no hidden state.
session.set_calldata([100, 200])
assert dict(session.run().outputs) == {0: 300, 1: None, 2: None, 3: None}

RunResult.outputs is a dict keyed by slot index; a slot the program never
wrote reads as None rather than raising. Program is immutable and
reusable; Session carries the mutable calldata and output-slot count.
Deriving a second Session from the same Program gives you two runners
that share no state.

Step limits Copy Section

Session.set_step_limit(n) caps how many instructions a run may execute
before run() raises. The limit is exact: 0 permits no instructions at
all. A fresh Session starts at xquad.vm.DEFAULT_STEP_LIMIT, which is
10,000,000. None is the only unbounded spelling, and a caller has to
write it -- unbounded execution is asked for, never inherited.

session = program.session(output_slots=1)
session.set_calldata([1, 2])
assert "step_limit=10000000" in repr(session)

session.set_step_limit(3)
try:
    session.run()
except RuntimeError as e:
    assert "StepLimitExceeded" in str(e)

# 0 is not a sentinel for "unlimited" -- it executes nothing, so this
# 11-step program fails at its first instruction.
session.set_step_limit(0)
try:
    session.run()
except RuntimeError as e:
    assert "StepLimitExceeded" in str(e)

# None removes the bound. A program that never halts will not return,
# and it does not take SIGALRM: the GIL is held inside the Rust run.
session.set_step_limit(None)
assert "step_limit=unlimited" in repr(session)
assert dict(session.run().outputs) == {0: 3}

A budget that exactly covers the program succeeds. This one needs 11
steps, so set_step_limit(11) runs it and set_step_limit(10) does not.

Loading bytecode directly Copy Chapter

Program.load(bytes) parses raw wire-format bytes -- a .xqb blob produced
by xquad asm or by program.bytecode(). No source is retained:

blob = program.bytecode()
reloaded = Program.load(blob)
assert reloaded.source is None
assert reloaded.instruction_count == program.instruction_count

Program.load never validates its input; a malformed blob decodes
successfully as a Program object and only fails once a Session tries to
run it. A one-byte blob is too short even for the wire-format header:

p = Program.load(b"\x43")
s = p.session()
try:
    s.run()
except RuntimeError as e:
    print(e)
# decode error: TruncatedHeader

Program.from_source validates at load time instead: an unassemblable
string raises ValueError immediately, before a Session exists.

Calldata types Copy Chapter

A calldata list may mix any of int, list[int], xqffi.vm.XqmxModel,
xqffi.vm.XqmxSample, and None (unset). Session.set_calldata checks
every element's type as soon as you call it, not at run time:

from xqffi.vm import XqmxModel, XqmxSample

model = XqmxModel("binary", size=4)
model.set_linear(0, -1)
model.set_quad(0, 1, 2)

sample = XqmxSample("spin", values=[-1, 1, -1, 1])

session.set_calldata([model, sample, [1, 2, 3], 42])
# session.run() now sees four typed input slots.

try:
    XqmxModel("binary", size=4, rows=2, cols=3)
except ValueError as e:
    print(e)
# a 2 x 3 grid does not fit 4 variables; rows and cols must both be 0,
# or both positive with rows * cols <= size

try:
    session.set_calldata([object()])
except TypeError as e:
    print(e)
# unsupported calldata element type: object; expected int, list[int],
# XqmxModel, XqmxSample, or None

The constructors also refuse a size over
xqffi.vm.MAX_ALLOCATION_SIZE, the largest allocation bytecode can
make, with ValueError, and XqmxSample refuses a value outside its
domain the same way. The coefficient accessors (set_linear,
get_linear, set_quad, get_quad) raise IndexError for a variable
index outside 0..size, a negative index included:

try:
    model.set_linear(4, 1)
except IndexError as e:
    print(e)
# variable index 4 is out of range for a model of size 4

Inspecting a model or sample Copy Chapter

XqmxModel and XqmxSample are pyo3 objects; there is no dict-conversion
helper in this package today. Read a model's coefficients through its own
accessors:

model = XqmxModel("binary", size=4)
model.set_linear(0, -1)
model.set_linear(2, 3)
model.set_quad(0, 1, 2)

model.domain          # "binary"
model.size            # 4
list(model.linear_items())     # [(0, -1), (2, 3)]
list(model.quadratic_items())  # [((0, 1), 2)]
model.get_linear(0)   # -1
model.get_quad(0, 1)  # 2
repr(model)            # 'XqmxModel(domain=binary, size=4)'

__repr__ is intentionally minimal. Convert to xquad.types.XQMX (the
canonical, backend-independent type covered next) if you want a Python
object you can inspect with normal attribute access, or serialise by
iterating linear_items() / quadratic_items() yourself.

The other two VM surfaces Copy Chapter

Two lower-level wrappers sit underneath and alongside xquad.program,
both worth knowing about directly.

xqffi.vm.Vm is the thinnest possible wrapper over the Rust
interpreter: construct it, call set_calldata / set_output_slots, call
.run(bytecode), read .outputs() as a positional list. It always targets
the Rust backend. .reset() clears the stack, registers, loop stack, and
step counter, but calldata and output slots are untouched by it -- both
persist across runs until you call set_calldata() or set_output_slots()
again. It is what Session.run() builds internally:

from xqffi.vm import Vm

vm_src = "PUSH 7\nPUSH 5\nADD\nSTOW r0\nPUSH 0\nOUTPUT r0\nHALT\n"
bytecode = Program.from_source(vm_src).bytecode()

vm = Vm()
vm.set_output_slots(1)
vm.run(bytecode)
assert vm.outputs() == [12]

Ways to Use XQuad
covers when to reach for it directly instead of Session.

xquad.vm.VM is a separate wrapper that every example runner under
examples/ actually uses (examples/maxcut/runner.py,
examples/knapsack/runner.py). It selects between the Rust interpreter and
the pure-Python reference VM via VMBackend, converts FFI
objects to and from the canonical xquad.types.XQMX at the boundary, and
runs .xqasm source text directly rather than pre-assembled bytecode:

from xquad.vm import VM, VMBackend

src = "PUSH 7\nPUSH 5\nADD\nSTOW r0\nPUSH 0\nOUTPUT r0\nHALT\n"
v = VM(backend=VMBackend.RUST)  # RUST is also the default with no argument
v.set_output_slots(1)
v.run(src)
assert v.outputs() == [12]
assert v.stack() == []

VM.outputs() returns xquad.types.XQMX instances for model and sample
outputs, where xqffi.vm.Vm.outputs() and Session.run().outputs return
the raw pyo3 XqmxModel / XqmxSample objects. Pick VM when you need
Python-backend parity checking or when your calldata and outputs are
already in xquad.types terms; pick Session for the dict-keyed,
slot-sparse ergonomics shown above; pick xqffi.vm.Vm only if you are
building your own layer on top of the raw Rust FFI.

VM.set_calldata() applies the same size, grid and index rules to every
xquad.types.XQMX it is given, with the same errors on both backends,
and applies them again at run(), since it keeps your objects rather
than copying them. A sample value outside its domain raises
xqvm_py.errors.SampleOutOfDomain, a ValueError subclass, from
set_calldata() on both backends. A sample changed out of its domain
after set_calldata() is caught again at run(), where RUST raises a
plain ValueError instead.

A complete run across three programs Copy Chapter

A compiled problem is three independent programs -- see Three
Programs for why. Driving all three from
xquad.program looks like this, using the exact build_problem function
examples/knapsack/runner.py defines (see Compiling
for what compile() emits):

from examples.knapsack.runner import build_problem
from xquad.program import Program
from xqffi.vm import XqmxSample

n = 4
weights = [2, 3, 4, 5]
values = [3, 4, 5, 8]
capacity = 8

problem = build_problem(n, weights, values, capacity)
programs = problem.compile()

# Encoder: inputs in, model out.
encoder = Program.from_source(programs.encoder)
enc_session = encoder.session(output_slots=1)
enc_session.set_calldata([n, weights, values, capacity])
model = enc_session.run().outputs[0]

# A hand-picked sample -- items 1, 2, 3 selected, no solver involved.
sample = XqmxSample("binary", values=[0, 1, 1, 1, 0, 0, 0, 0])

# Verifier: the encoder's own inputs, then model and sample; (energy, valid) out.
verifier = Program.from_source(programs.verifier)
ver_session = verifier.session(output_slots=2)
ver_session.set_calldata([n, weights, values, capacity, model, sample])
ver_result = ver_session.run()
energy, valid = ver_result.outputs[0], ver_result.outputs[1]

# Decoder: sample + N in, decoded selection out.
decoder = Program.from_source(programs.decoder)
dec_session = decoder.session(output_slots=1)
dec_session.set_calldata([sample, n])
selected = dec_session.run().outputs[0]

assert (energy, valid, selected) == (-4817, 0, [0, 1, 1, 1])

Items 1, 2 and 3 weigh 3 + 4 + 5 = 12 against a capacity of 8, so the
sample violates the capacity constraint and valid comes back 0.
energy is still computed: ENERGY recomputes the objective whatever the
sample's feasibility, so the two outputs answer different questions. Swap
in [1, 1, 0, 0, 0, 0, 0, 0] -- items 0 and 1, weighing 5 -- and the same
run gives (-5507, 1).
Verification
says what valid covers.

The verifier takes the encoder's calldata because it replays the encoder to
rebuild the constraint data, then appends the model and the sample. Each
program's own .set_calldata order and .set_output_slots count are fixed
by what it was compiled from -- Compiling
has the full table. A real pipeline replaces the hand-picked sample above
with xqsa.build_solver(...).solve(model).sample; see Solving
Overview.

What this page does not cover Copy Chapter

• Tracing. Step-by-step execution inspection is not part of Session
  today.
• Keyword calldata (session.set_calldata(n=4, ...)). Session takes a
  positional list only; there is no input-slot labelling to key against.
• A _repr_html_ for notebooks. __repr__ is the only representation
  Program, Session, RunResult, XqmxModel and XqmxSample provide.
• A to_numpy() helper. Convert via linear_items() /
  quadratic_items() and numpy.asarray(...) on your own side; this
  package does not carry a numpy dependency.

Overview (`docs/book/src/solving/README.md`) Copy Section

Solving Overview

Backends names the five solvers and what
distinguishes them. This chapter covers each one in enough depth to run
it: installation, parameters, and what its result actually contains.

xqsa is the package that does this. It defines one abstract interface,
Solver, and five classes built on it -- SolverDWaveCPU,
SolverDWaveQPU, SolverCudaGPU, SolverMetalGPU, and SolverQuip. A
model built from xqcp or by hand in XQVM bytecode does not know or care
which one samples it.

The Solver Interface Copy Chapter

Every backend defines the same single method:

class Solver(ABC):
    @abstractmethod
    def solve(self, model: XQMX, **kwargs: Any) -> SolverResult: ...

model is an XQMX in MODEL mode, binary or spin domain. **kwargs
override that solver's constructor defaults for this call only --
solver = SolverDWaveCPU(num_reads=100) then solver.solve(model, num_reads=500) runs 500 reads without building a new solver. solve()
raises on failure (hardware unreachable, no embedding found, connection
lost); it never returns a partial or empty result.

The return value is a frozen dataclass:

@dataclass(frozen=True)
class SolverResult:
    sample: XQMX
    energy: int
    timing: float
    metadata: dict[str, Any] = field(default_factory=dict)

sample is the solution, an XQMX in SAMPLE mode. energy is the
authoritative Hamiltonian energy. timing is wall-clock seconds spent
solving. metadata defaults to an empty dict; its actual shape is
per-backend, covered below.

energy is never the backend's own reported value taken on faith. Every
solve() recomputes it with the same integer formula the XQVM ENERGY
opcode uses, over the model and the returned sample. See
Energy and Precision for what that buys you
and what it costs on hardware with limited precision.

metadata's shape is not identical across all five backends. The three
classical simulated-annealing backends -- dwave-cpu, cuda-gpu, and
metal-gpu -- carry seed and reads at the top level plus a params
dict of solver-specific detail (sweep counts, the raw pre-recompute
energy). dwave-qpu carries a params dict the same way, but omits
seed (there is no seed on physical hardware) and adds solver and
qpu_timing at the top level, alongside reads; see
D-Wave QPU. quip returns a
different set entirely -- no seed, reads, or params at all; see
Quip Network. Check the backend you are
calling before indexing into result.metadata.

Picking a Backend by Name Copy Chapter

build_solver constructs any of the five from a short string, so a
caller -- an example runner, a CLI flag, a script -- can stay
backend-agnostic:

from xqsa import SOLVERS, DEFAULT_SOLVER, build_solver

print(sorted(SOLVERS))
# ['cuda-gpu', 'dwave-cpu', 'dwave-qpu', 'metal-gpu', 'quip']
print(DEFAULT_SOLVER)
# dwave-cpu

solver = build_solver("dwave-cpu", seed=42)
result = solver.solve(model)

seed reaches the three classical simulated-annealing backends
(dwave-cpu, cuda-gpu, metal-gpu) and is ignored for dwave-qpu
(physical hardware has no seed) and quip (configured from the
environment; the miner's own randomness is out of the caller's control).

build_solver otherwise uses each backend's own constructor defaults,
with one exception: for cuda-gpu and metal-gpu it raises num_reads
to 200 and num_sweeps to 2000, rather than the 100 and 1000 the bare
constructor defaults to. Local Solvers
has the constructor defaults for every backend.

Swapping Backends Without Changing the Model Copy Chapter

This is the claim the whole toolchain rests on, so here it is checked
rather than asserted. examples/maxcut/runner.py builds one Max-Cut
model with xqcp, runs the encoder on the Rust XQVM, and samples the
result with whichever solver --solver names, built through
build_solver. Run it against two different backends -- dwave-cpu
(CPU simulated annealing, 100 reads and 1000 sweeps) and metal-gpu (an
Apple Silicon GPU kernel, a different process on different hardware, and
-- per build_solver's override above -- 200 reads and 2000 sweeps) --
and nothing about the model or the encoder changes:

uv run python examples/maxcut/runner.py --n 6 --seed 42 --interpreter rust --solver dwave-cpu
uv run python examples/maxcut/runner.py --n 6 --seed 42 --interpreter rust --solver metal-gpu

Both print the same result: "energy": -571, "cut_weight": 571,
"valid": 1, the identical partition. The encoder produced one QUBO;
two unrelated solvers minimised it and agreed. That agreement is not
guaranteed in general -- a harder model can leave different backends in
different local optima -- but the model they were handed, and the
verifier that checked what came back, never changed.

The Domain Every Backend Rejects Copy Chapter

XQVM has three domains: binary, spin, and integer. Every current
xqsa solver's _validate_model() accepts binary and spin and raises
ValueError on integer:

from xqsa import SolverDWaveCPU
from xqvm_py.xqmx import XQMX

model = XQMX.integer_model(size=3, k=4)
SolverDWaveCPU().solve(model)
# ValueError: Unsupported domain for solving: INTEGER

An integer XqmxModel is a real thing you can build in XQVM bytecode
today -- see Three Domains
-- but nothing in this chapter can solve one. spec/xqsa/DOMAINS.md
calls this "reserved": a future solver may relax the check, but none of
the current five does. Re-encoding the problem in binary or spin is the
only route around it today.

Choosing Among the Rest Copy Chapter

That baseline requirement -- runs anywhere, needs nothing -- is exactly
DEFAULT_SOLVER: every other backend is worth comparing against
dwave-cpu before you trust its answer.

Overview (`docs/book/src/start/README.md`) Copy Section

Install XQuad

This page installs XQuad, confirms the install works, and gets the
runnable examples this book uses. It also covers what a GPU or QPU solver
needs beyond the base install. First Problem picks up
from here with a real run.

Install Copy Chapter

The root README's Install section
is the canonical install reference for both ecosystems this project ships
into -- prebuilt wheel platforms, the Rust toolchain required to build the
xqffi extension from source, and installing individual Python packages
instead of the umbrella. The two commands most readers need:

cargo install xqcli      # gives you the `xquad` binary
pip install xquad        # Python umbrella: the full pipeline

Verify the Install Copy Chapter

xquad --version prints the installed CLI's version, confirming the
xqcli binary is on PATH and runs. Importing the umbrella package
confirms the Python half:

$ python -c "import xquad; print('ok')"
ok

Get the Examples Copy Chapter

Every uv run python examples/... command in this book, including on
the next page, runs against a checkout of this repository -- the
examples are not part of any published package, so cargo install and
pip install above do not put them on disk. Get one and set up the
Python workspace once:

git clone https://gitlab.com/quip.network/xquad.git
cd xquad
make deps-py

make deps-py needs uv
and the Rust toolchain cargo install xqcli above already needed. It
syncs the Python workspace and wires up cross-package imports, so
uv run python examples/<name>/runner.py then works from the repository
root -- the same command every example and cookbook page in this book
uses.

GPU and QPU Install Prerequisites Copy Chapter

The base install runs CPU simulated annealing only, through xqsa's
dwave-cpu backend. Every other solver -- a local GPU or a real D-Wave
QPU -- needs an extra on top, and the extra needs hardware or credentials
this page cannot install for you. xqsa/pyproject.toml defines the
extras, and xquad/pyproject.toml forwards to the ones it re-exports:

• cuda -- cupy-cuda12x>=13.0, nvidia-cuda-nvrtc-cu12, and
  nvidia-cuda-runtime-cu12, for a local NVIDIA GPU.
• dwave -- dwave-system>=1.0, for the real D-Wave QPU.
• metal -- pyobjc-framework-Metal>=11.0, marked sys_platform == 'darwin', for a local Apple GPU. The marker means pip install xquad[metal] succeeds on Linux and installs nothing.
• quip -- substrate-interface>=1.7.4,<2 plus
  quip-signer>=0.3.0,<0.4,
  for the Quip network solver, which needs a QUIP_RPC_URL and a
  configured signer; see Quip Network for
  what that solver does.

xqcp, xqffi, and xqvm_py define no optional dependencies at all.

The only extra this page can fully specify is [dwave]: it needs a D-Wave
Leap account and a DWAVE_API_TOKEN, and dwave ping confirms both. A
local GPU ([cuda] or [metal]) is another option; see Local
Solvers for those two extras
and their driver checks.

pip install xquad[cuda], xquad[metal], xquad[dwave], and
xquad[quip] each forward to the matching xqsa extra, and extras are
composable: pip install "xquad[cuda,dwave]".

A missing extra does not break the base install: import xqsa never
fails just because an optional extra is absent. Only constructing the
solver class that needs it does, raising ImportError with a
pip install xqsa[...] hint naming the extra to add.

Per-solver parameters, driver-level troubleshooting, and what a QPU
result contains that a CPU one does not are covered in
Solving Overview, Local Solvers,
and D-Wave QPU. This section only covers what
to install before you get there.

Where to Go From Here Copy Chapter

• First Problem -- run a complete problem end to
  end and get a real answer back.
• What Happened -- the explanation of what that
  run just did.
• XQVM Reference -- a minimal hand-written
  .xqasm program, if you want to see the machine underneath before
  running anything larger.
• Toolchain Map -- the pieces XQuad is built
  from, and how they hand off to each other.

Overview (`docs/book/src/xqvm/README.md`) Copy Section

XQVM Reference

XQVM is the virtual machine at the core of XQuad: a stack-based interpreter
with a 256-slot register file that executes compiled quadratic-optimisation
programs. This section is the reference for that machine -- its execution
model, assembly language, instruction set, binary format, and verifier. For
what a QUBO/Ising model is and why you would want one, start at
Concepts instead; this section assumes you already
have a program, or want to write one directly in .xqasm, and want to know
exactly what the machine does with it.

A minimal program Copy Chapter

Save this as add.xqasm, then assemble and run it:

; push two integers and add them
PUSH 10
PUSH 32
ADD
HALT

$ xquad asm add.xqasm -o add.xqb
assembled 4 instructions (21 bytes) -> add.xqb
$ xquad run add.xqb
stack (bottom to top):
  42

The program pushes 10 and 32 onto the value stack, adds them, and halts. The
result remains on the stack and is printed by xquad run. xquad run --text add.xqasm skips the separate assembly step and runs the source directly.

What this section covers Copy Chapter

• VM Architecture -- the value stack, the 256-slot
  register file, and the loop stack.
• Loop Stack -- RANGE/ITER/NEXT iteration.
• Calldata and Outputs -- getting values into a program with
  INPUT and out with OUTPUT.
• Execution -- the fetch-decode-execute cycle and
  execution tracing.
• Assembly -- the .xqasm text syntax.
• Assembly Examples -- worked .xqasm programs.
• Instructions -- all 93 instructions, by
  category.
• Opcode Reference -- the generated opcode table.
• Bytecode Format -- the .xqb wire format.
• Verifier -- what the pre-execution verifier checks.
• CLI -- the xquad command-line tool.
• Limits and Errors -- fixed and configurable
  limits, and every runtime and verifier error.

Overview (`docs/book/src/xqvm/cli/README.md`) Copy Section

CLI Reference

xquad is the unified command-line driver for the XQVM toolchain. It is
built by the xqcli crate, but the crate and the binary have different
names: cargo install xqcli installs a command called xquad, not
xqcli. Running xqcli --help after installing fails because no such
binary exists.

Installation Copy Chapter

cargo install xqcli
xquad --help

Or build from this repository:

cargo build -p xqcli --release

The binary is at target/release/xquad.

Subcommands Copy Chapter

xquad has four subcommands, one per stage of the toolchain:

General usage Copy Chapter

xquad <COMMAND> [OPTIONS] [ARGS]
xquad --help
xquad <COMMAND> --help

xquad asm reads .xqasm source and writes bytecode; it has no --text
flag and rejects a .xqb file. xquad dism reads bytecode from a file or
stdin, also with no --text flag. xquad run and xquad verify read
bytecode by default and read .xqasm assembly instead when --text is
passed.

Error reporting is not uniform across the four subcommands. Only xquad asm propagates the real xqasm::Error, with its NamedSource and
SourceSpan, so only asm prints a highlighted source snippet pointing
at the failing token. xquad run --text and xquad verify --text both
flatten an assembly failure through miette::miette!("{e}"), which
formats the error to a plain string and discards the span; xquad verify
on a .xqb file flattens a verifier failure the same way. Decode errors
(a malformed .xqb file) go through .into_diagnostic(), which also
carries no span. So an assembly, verification or decode failure reaches
you as a bare message -- see xquad verify
for what that looks like in practice. A VM runtime fault under xquad run is the one exception: it goes through into_diagnostic(), which
disassembles the program around the failing offset and annotates it, so
that path does print a snippet. Argument-parsing failures, such as
asm's -o/--stdout conflict, are plain clap errors, a third and
unrelated error path.

A minimal round trip Copy Chapter

cat > add.xqasm <<'EOF'
; add.xqasm -- push two integers and add them
PUSH 10
PUSH 32
ADD
HALT
EOF

xquad asm add.xqasm -o add.xqb
xquad verify add.xqb
xquad run add.xqb

xquad run add.xqb prints the residual stack:

stack (bottom to top):
  42

Overview (`docs/book/src/xqvm/instructions/README.md`) Copy Section

Instruction Set Reference

This section documents all 93 XQVM instructions, organised into the 14
categories below. Each page covers the semantics, error conditions, and
worked examples for one category. For the opcode byte, mnemonic, operand
layout, and stack effect of every instruction, see the generated
Opcode Reference -- that table is the single source of
truth for wire-level facts, so the pages in this section carry prose and
teaching content instead of repeating it.

Notation Copy Chapter

• Stack effect -- described in prose on this page ("Pop b, then a")
  and summarised on the generated Opcode Reference as a
  Stack column of the form 2 → 1, meaning two values popped and one
  pushed. The value stack is last-in-first-out: whichever value was pushed
  most recently is popped first, so PUSH a; PUSH b; SUB computes
  a - b, not b - a. Every "pop x, then y" operand order on this
  section's pages, including the ones on constraints.md and
  index-math.md, depends on this rule.
• reg -- the u8 operand encoded in the instruction byte stream,
  identifying a register slot (r0--r255).
• label -- a sequential id assigned to each TARGET instruction, in
  program order, during the load-time pre-scan described in
  Bytecode Format. It is not a byte offset, and not
  the .N token used in .xqasm source -- that token is assembler-only and
  is resolved to the sequential id before encoding. JUMP1/JUMPI1 encode
  the id as a single u8 operand; JUMP2/JUMPI2 encode it as a u16
  operand (big-endian). See Control Flow for how the
  assembler picks between the two.
• Assignments use \(\leftarrow\) (register write) and \(\to\) (stack push).
• Iverson brackets -- \([P]\) equals \(1\) if \(P\) is true, \(0\) otherwise.
• Checked arithmetic -- every integer operation is checked against the
  i64 range. A result that would leave it raises ArithmeticOverflow
  rather than wrapping or panicking; see
  Arithmetic.

Register Effect Vocabulary Copy Section

A handful of pages, constraints.md and
energy.md, annotate individual opcodes with a **Register effect:** line using three terms:

• read -- register contents are inspected but not changed.
• write -- register is replaced wholesale with a new value.
• mutate -- register's existing value is modified in-place (e.g.
  appending to a vec, incrementing a coefficient).

Most category pages group opcodes by topic or mechanism rather than
walking through them one at a time, so they carry no such line.

`RegVal` -- The Register Value Type Copy Chapter

Each of the 256 registers holds one variant of RegVal -- Unset, Int,
VecInt, VecXqmx, Model, or Sample. See VM
Architecture for the full table.

Type mismatches at runtime produce a RegisterType error with the expected
and actual variant names; reading an Unset register via LOAD or OUTPUT
produces UnsetRegister instead, since there is no variant to compare
against.

Categories Copy Chapter

Reserved Opcodes Copy Chapter

Every byte value not listed in Opcode Reference is illegal;
the decoder rejects it. The 93 assigned bytes are not contiguous -- there are
gaps both between and within the ranges above, plus one large unassigned
block above the normal instruction space. The full gap set, derived by
diffing the 93 assigned byte values against the complete 0x00-0xFF space:

NOP (0xF0) and HALT (0xFF) are the only two assigned bytes outside
0x00-0x7F; every other byte in 0x80-0xFF is illegal. See
spec/xqvm/ISA.md
for the normative list, organised the same way.

Book Src Appendix Spec Index (`docs/book/src/appendix/spec-index.md`) Copy Section

Spec Index

The book teaches; spec/ is what XQuad actually is. Every file below is
the normative source for its topic's intent. The conformance harness does
not check either implementation against these documents: it checks the
Rust and Python implementations against each other and against
conformance/opcodes.yaml. The implementation is what ships, and the two
can diverge; where a divergence is known, the relevant book page says so.
Conformance
explains why a green run is evidence about the programs a vector covers
rather than a blanket guarantee.

The lists below are not closed. For anything they omit, check the book
chapter covering the component you are working with, or search the spec
files directly.

Top Level Copy Chapter

• spec/README.md
  -- index of the three layers below, and the drift policy that ties spec
  to implementation.

XQVM Copy Chapter

Normative for the virtual machine: the instruction set, the wire format,
and the bytecode verifier.

• spec/xqvm/README.md
  -- document index for this layer.
• spec/xqvm/SPEC.md
  -- normative for the machine overview, the three-program architecture,
  the state model, determinism, the type system, and runtime limits.
• spec/xqvm/ISA.md
  -- normative for the instruction set: notation, per-category opcode
  tables, semantic notes, and reserved opcodes.
• spec/xqvm/HLF.md
  -- normative for the high-level constraint expansion formulas: the QUBO
  penalty terms ONEHOTR, ONEHOTC, EXCLUDE, IMPLIES, EQUALITY,
  ATLEAST, ATLEASTW, and REDUCE inject.
• spec/xqvm/ENCODING.md
  -- normative for both file formats: .xqasm assembly syntax and the
  .xqb binary encoding, including the XQBC header layout.
• spec/xqvm/VERIFIER.md
  -- normative for the bytecode verifier: its phase pipeline and every
  error it can raise.
• spec/xqvm/METERING.md
  -- normative for step metering: what a step is, the cost constants and
  how they were measured, the per-opcode charge table, the three formulas,
  and the conformance rules for step counts and operand validation order.

XQCP Copy Chapter

Normative for the constraint-programming DSL that compiles a Problem
into the three XQVM programs.

• spec/xqcp/README.md
  -- document index for this layer.
• spec/xqcp/SPEC.md
  -- normative for the DSL overview, the three-program architecture as
  xqcp implements it, the problem lifecycle, and the compilation
  contract.
• spec/xqcp/TYPES.md
  -- normative for the symbolic value types, the expression tree, the
  operator algebra, and the free functions built on top of it.
• spec/xqcp/CONSTRAINTS.md
  -- normative for the constraint taxonomy, each constraint method's
  signature, and its cross-reference into the matching HLF expansion.
• spec/xqcp/COMPILER.md
  -- normative for the compilation pipeline: encoder/verifier/decoder
  generation, register allocation, and action recording.

XQSA Copy Chapter

Normative for the solver-adapter interface between a model and a backend.

• spec/xqsa/README.md
  -- document index for this layer.
• spec/xqsa/SPEC.md
  -- normative for the architecture overview, where solving sits in the
  pipeline, and the plugin model new solvers implement.
• spec/xqsa/INTERFACE.md
  -- normative for the Solver abstract class, the solve() contract,
  the SolverResult type, and parameter-passing conventions.
• spec/xqsa/ENERGY.md
  -- normative for the energy computation formula, its precision contract,
  and the sparse representation solvers exchange it in.
• spec/xqsa/DOMAINS.md
  -- normative for the domain support matrix, sample encoding, grid
  metadata, and capability negotiation between a model and a solver.
• spec/xqsa/SOLVERS.md
  -- normative for the solver registry, its naming convention, algorithm
  families, and the dependency model behind each optional extra.

Reading a Spec File Like a Reference, Not a Tutorial Copy Chapter

Every file above assumes the concepts this book explains from scratch --
what a quadratic model is, why a problem becomes three programs, what a
penalty weight does. Arrive from Concepts or the
relevant chapter first; the spec files are where to go once you need the
exact rule the book page summarised, not where to start.

Guide Development Workflow (`docs/guide/development-workflow.md`) Copy Section

xquad development workflow

This document describes how changes move from authoring to main and
dev in the xquad repository. The central idea -- carried over from the
xq-rs <-> xq-py merge (QUI-412) -- is that two implementations of the
same VM must stay in lockstep. Everything else in the workflow is in
service of that invariant.

Who maintains what Copy Chapter

One repository, two implementations, one spec:

Branches Copy Chapter

Two long-lived branches. Before 1.0, main is the non-breaking line
and dev is the breaking one; which a change targets is decided by
whether it breaks, not by whether it is a fix.
gitflow-protocol.md is the normative
description -- routing, releases, betas and the back-merge -- and what
follows is only the naming.

• main -- the non-breaking line, at the next patch's -dev
  version. Protected: everything lands by merge request except the
  version bump that reopens it after a release, which the code owners push
  directly and CI holds to a version-only change. A merge lands as a
  real merge commit with a GitLab-generated merge: branch '' into 'main' subject. Merges are not squashed.
• dev -- the breaking line, at the next minor's -dev version.
  Protected; Maintainers may push to it, for back-merges and version
  bumps only. It contains main at all times, and CI marks dev red
  while a back-merge is outstanding.
• feature/qui-[-tag] -- short-lived branches for individual
  tickets, cut from and merged into whichever line the change belongs
  on. One branch may carry several tickets when they touch the same
  files. The MR body lists each ticket it consumes (QUI-*), so Linear
  status moves in lockstep with git state.
• release/v<version> -- prepares a release: cut from main for a
  patch or from dev for a minor, carries the version bump, and merges
  into main unsquashed. release:auto-tag cuts the tag from the
  merge.
• chore/<tag> -- repository maintenance belonging to no ticket.

The atomic spec-MR rule Copy Chapter

Any MR that changes VM semantics must touch all four of the
following in the same MR:

1. spec/xqvm/*.md -- any normative spec file: the change documented.
   SPEC.md, ISA.md, HLF.md, ENCODING.md and VERIFIER.md all
   satisfy this layer; the guard matches the directory, not one file.
2. xqvm/src/**/*.rs -- the Rust production impl updated.
3. xqvm_py/{executor,opcodes,xqmx,state,vector,tracer,errors}.py --
   the Python reference impl updated.
4. conformance/vectors/** or conformance/opcodes.yaml -- a new
   or modified conformance vector that exercises the change.

Why Copy Section

• No drift-tracking middle ground. Before the merge, drift
  between xq-rs and xq-py was tracked as a running list. Ten
  drift points accumulated before we stopped accepting it and merged
  the repos (QUI-412). The atomic rule makes divergence impossible by
  construction: you can't commit a spec change without updating both
  impls in the same diff.
• Reviewable as one story. A reviewer sees the spec delta next
  to the two impl deltas next to the test that proves they agree.
  The mental model is contained in one MR.
• CI coverage that scales. The conformance harness runs every
  vector against both runtimes. Adding a vector at the same time as
  the semantics change means the harness is as up-to-date as the
  spec on the day of the merge.

Enforcement Copy Section

A CI guard -- scripts/check-atomic-spec-mr.sh
-- runs as part of verify:policy on every merge request. It classifies
changed files into the four layers and fails the pipeline if an MR
touches 1-3 layers but not all four. Touching 0 layers (pure
docs / CI / tooling MRs) or all 4 passes.

Run locally the same way CI does:

scripts/check-atomic-spec-mr.sh origin/main HEAD

Exemptions Copy Section

Some legitimate changes only touch one or two layers -- the guard
would flag them as drift even though they're alignment fixes. The
exempt cases:

• One-sided alignment fix. One impl already matches the spec;
  the other impl is brought in line without changing the canonical
  behaviour. Example: QUI-453 changed only xqvm_py/xqmx.py to pre-
  populate a spin sample with -1 per position, matching what Rust
  had always done -- no Rust change, no opcode table change.
• Spec clarification. The spec text gains precision without
  changing the normative rules. No impl updates needed.
• Conformance-only coverage addition. A new vector exercises
  existing semantics. No spec / impl changes.
• Cross-implementation alignment with no normative change. Both
  impls move, and sometimes the harness with them, to converge on
  behaviour the spec already states -- so the spec layer has nothing to
  add and the guard's four-layer test cannot be satisfied honestly.
  This is the case the v0.4.0 series used most: QUI-1147's step-budget
  export touched xqvm/src/ and xqvm_py/ together, and QUI-1032's
  opcode-signature check touched those two plus conformance/, neither
  of them changing what the spec says.

To take an exemption, add a commit-message trailer of the form
Atomic-Spec-Exempt: QUI- <reason>. It goes in the message's last
paragraph, at column 0, beside the sign-off:

Align Python SSMX default to Rust's [-1, -1, ...] initialisation.

Python was shipping empty-dict samples where Rust used vec![-1; size];
this aligns the Python side. No Rust change needed.

Fixes QUI-453
Atomic-Spec-Exempt: QUI-453 one-sided Python fix, no semantics change
Signed-off-by: You <[email protected]>

The layout is not stylistic. git reads trailers out of the last
paragraph only, and a paragraph break above the trailer hides it from
git log --format='%(trailers)', from GitLab's commit view, and from
everything else built on git's trailer parsing. Every exempt trailer
written before QUI-1030 sat in a paragraph of its own above the ticket
footer, so not one of them parses -- which is how eleven exemptions were
taken without any of them being findable.

Two more rules follow from how git treats that paragraph:

• The whole reason goes on the trailer line. A continuation line is
  not a trailer, and git either drops it -- silently truncating the
  reason to its first line -- or, with no sign-off in the paragraph,
  stops reading the paragraph altogether.
• A Fixes QUI-NNN footer may share the paragraph, but not the line
  directly below the trailer. It has no colon, so it is not a trailer
  either; the mandatory sign-off is what makes git tolerate it. Directly
  below the trailer it is indistinguishable from a wrapped reason, so the
  guard rejects that position rather than guess. Put it above the
  trailer, or below the sign-off.

A trailer that breaks any of this fails the guard rather than being
ignored by it, because an exemption nobody can find is worse than no
exemption at all. Column 0 is git's rule too, which is why an indented
example in a commit body -- like the ones in this repository's own
documentation commits -- is not mistaken for a real exemption.

The guard scans every commit message in the MR range and bypasses when
it finds at least one well-formed trailer. Reviewers should see the
exemption and confirm the rationale holds; there is no approval process
beyond review.

What does NOT trigger the rule Copy Chapter

• Consumer-side surface work -- the PyO3 bindings under
  xqffi/src/*.rs (Rust, but consumer glue -- they expose the VM to
  Python, they don't define its semantics), plus xquad/program.py
  and the xquad / xqcp / xqsa Python packages. Changes here
  don't need spec or conformance updates.
• Build glue and tooling -- xqvm/build.rs, xqvm/Cargo.toml,
  xqvm_py/pyproject.toml, Makefile, CI config, scripts. Not
  semantic.
• Docs -- everything under docs/, READMEs, CHANGELOG. Not
  semantic.
• Tests -- xqvm/src/**/tests.rs, xqvm_py/tests/**,
  conformance/tests/**. Tests exercise semantics but don't define
  them; the conformance vectors (under conformance/vectors/) are
  the authoritative cross-impl check and that's what the guard
  watches.

The opcode-addition gate Copy Chapter

Adding a row to the opcodes! table in
xqvm/src/bytecode/types/table.rs is a change to VM semantics, and the
merge request that adds it argues in its description that the new opcode
clears all six clauses of the on-chain admissibility bar:

1. No floating point. Integer arithmetic only, with every operation
   range-checked so that it faults rather than wrapping.
2. No host I/O, wall-clock, or ambient state. An instruction's
   result is a function of the program, the calldata and the VM's own
   state. Stated normatively in spec/xqvm/SPEC.md under Determinism.
3. No nondeterministic iteration order. Anything that walks a
   collection walks it in an order the spec fixes.
4. Bounded allocation. Every allocation is charged against a budget
   before it happens, and the budget is not escapable by a value the
   submitting account controls.
5. Bounded per-instruction work. The work one instruction performs
   is charged against the step budget before it happens, at a rate that
   scales with the data the program controls, so that a step is a unit
   of cost rather than a unit of dispatch.
6. Specified behaviour, pinned by a vector. The result and every
   fault the opcode can raise are specified normatively in
   spec/xqvm/, and a conformance vector covers the behaviour, failure
   paths included.

An opcode that cannot clear all six does not ship. The operation belongs
in xqcp, xqsa, the xquad API or a helper library, where it is
ordinary code rather than something every embedder has to trust.

Why Copy Section

The bar is a property of the instruction set rather than a decision each
embedder makes, and that is only true while every row on the table has
been held to it. The denied set is empty by construction, so an embedder
has nothing to gate -- but "by construction" names a construction
somebody has to carry out. Each of the six clauses was argued for every
opcode shipped so far, and none of those arguments was recorded where
the next proposal's reviewer would find it. An unwritten rule holds
nothing.