fix!: close the coefficient-index and error-precedence divergences

Summary

Closes the findings from the self-review of the QUI-1062 hardening series, plus the divergences that review turned up but did not name.

The series adds spec/xqvm/SPEC.md's Faults table, which makes fault identity normative rather than advisory. That is what promotes three latent divergences into spec violations, and why they are fixed here rather than deferred.

Coefficient indices are bounded on both VMs. GETQUAD, SETQUAD, ADDQUAD, EXCLUDE and IMPLIES converted their popped indices with usize::try_from and never compared the result against m.size, so any non-negative i64 was accepted and the write landed in the sparse map. A 4-variable model came out holding a coefficient on variable 9, the constraint the program asked for was attached to variables that do not exist, and the model still solved cleanly and answered wrongly. xqvm_py's get_linear and get_quadratic had the mirror defect on the read side, answering 0 for an index the Rust VM rejects. One bounded_index helper now carries the check for all eight handlers, replacing three duplicated copies in the linear trio.

Operand pops now precede register reads. SPEC.md states the order normatively: pops first, then the allocation charge, then type and range validation. Twenty-two xqvm_py runners did the reverse, so a short stack plus a wrong-typed register raised TypeMismatch here and StackUnderflow on the Rust VM. Both VMs rejected the program, but the identity is what the Faults table makes normative. Every runner was measured against the Rust VM opcode by opcode rather than fixed from a list: all 22 diverged, all 22 now agree, on both halves of the rule.

The pallet fixture can name its allocation budget. submit_program bounded the step budget and left the allocation budget at the VM's 1 GiB default, so a fixed-weight extrinsic could still exhaust a runtime heap -- and inside a Wasm runtime a failed allocation traps the whole execution rather than returning a fault the pallet can report. memory_limit is now a sixth argument, capped by Config::MaxMemoryLimit.

The generated verifier handles inequality-composed slack. _emit_inequality composes SLACK and EQUALITY over one vec pair, leaving the vectors extended exactly as a bare slack() would, but _scan_slack_equalities keyed only on kind == "slack". An apply_inequality() followed by an apply_equality() over the same registers left the second checked with EQ over slack-free vectors, so the verifier rejected samples the encoder's model accepts.

Three review findings were corrected by measurement rather than taken at face value: the SLACK ordering finding was already fixed and its generalisation covers 22 runners rather than 9; the planned _charge_coefficient signature change proved unnecessary, since it is already a no-op for a non-model register; and five ValueError claims in the spec were stale, falsified by this series' own f77d8b3.

Every new test was run against the tree before its fix and fails there -- 6 of 8 crate-local Rust tests, 5 of 5 xqmx tests, 44 of 44 precedence assertions, 8 of 8 conformance vectors, 2 of 2 xqcp tests. Conformance is 112 vectors on both interpreters, up from 102.

Closes QUI-1062 Closes QUI-1029 Closes QUI-1174

Type of Change

  • Bug fix (non-breaking change which fixes an issue)
  • New feature (non-breaking change which adds functionality)
  • Breaking change (fix or feature that would cause existing functionality to not work as expected)
  • Documentation update

Checklist

Preflight Checks

Run locally what CI enforces. Mark a language N/A if this MR does not touch it.

  • make preflight-rs passes -- fmt, taplo, clippy, rustdoc, deny, unit/integration/doc tests (or N/A)
  • make preflight-py passes -- taplo, ruff format + lint, pytest (or N/A)
  • make preflight-parity passes -- opcode parity, conformance, example smoke (if opcode or VM semantics changed)

Optional Checks

  • make test-miri passes -- N/A, no unsafe added or changed
  • make test-quip passes -- N/A, xqsa/quip*.py untouched

Commits & Documentation

  • This MR's title follows Conventional Commits (<type>[(scope)][!]: <description>) -- enforced by verify:policy
  • Commit subject lines are 72 characters or fewer and use the imperative mood
  • Commits are signed off (git commit -s)
  • All public items are documented

License Compliance Checklist

  • All new files include the required AGPL-3.0-or-later license header -- N/A, the only added files are conformance vectors (.xqasm / .json), which carry no header
  • Any new dependencies are AGPL-3.0-or-later compatible -- N/A, none added
  • Any new Python dependencies (pyproject.toml / uv.lock) are AGPL-3.0-or-later compatible -- N/A, none added
  • NOTICE file updated if adding AGPL-3.0-or-later compatible dependencies. -- N/A, no new dependencies
  • deny.toml updated if the license is not listed and it's compatible with AGPL-3.0-or-later -- N/A, no new dependencies
  • No proprietary or incompatible code was incorporated

Notes for the reviewer (not part of the MR description)

Three commits carry !: the coefficient bound and the two xqvm_py fixes change which programs fault, and feat(pallet-xqvm)! adds a sixth dispatch argument. This is why the MR title carries ! too -- see the note under the title above.

Squash-on-merge means none of the ten commit messages below reaches main; the squash commit's subject is the MR title and its body is whatever GitLab composes. The per-commit reasoning -- which measurement contradicted which review finding, why each bound is where it is, which tests were run against the pre-fix tree -- survives only in this description and in the MR's own commit list. Worth reading the commits during review rather than after.

Commit map, oldest first:

Commit What
dd45c7e fix(xqcp): check every declared constraint in the verifier
477ef08 docs: describe what the generated verifier now checks
dfc48b2 fix(xqvm)!: bound every coefficient index against the model size
5d39c95 fix(xqvm_py)!: bound a coefficient read against the declared size
84ee7fe fix(xqvm_py)!: pop an instruction's operands before reading its register
e0cb677 docs(spec): state the index bound the coefficient opcodes now enforce
12570bc test(conformance): pin the coefficient index bound on both interpreters
aef983f feat(pallet-xqvm)!: take the allocation budget as an extrinsic argument
4328b6d docs: correct two comments the hardening series left behind
f31fc89 fix(xqcp): treat an inequality's slack as slack in the verifier scan

Left out deliberately, recorded on their own tickets: the quad-op-on-sample divergence and the Fault::XqmxMode identity question stay on QUI-1160, since the bytecode verifier rejects those programs and they are outside this MR's signed-account scope. spec/xqvm/ISA.md:235's claim that xqvm_py raises XqmxMode there is factually wrong today and is noted on that ticket rather than corrected here.

Outstanding before this goes up: the branch is not pushed, and QUI-1029's first acceptance-criteria checkbox is still unticked.

Base: origin/main at 6ece608. Rebased three times during development as QUI-1107 was rewritten, squashed into f14a04e and merged; the tree has been byte-identical across every rebase.

Merge request reports

Loading
Loading