[ondrik]

Fixes #34.

Problem

AutoQ splits the kets for the same qubits into units once, using all of them together. That covers the kets in one set, across ∪, and across pre.hsl and post.hsl in ver. It then rewrites each ket by walking that split. A ket shorter or longer than the others ran off the end of its string, and autoq aborted with an uncaught std::out_of_range (SIGABRT, exit status 134) instead of reporting the misalignment.

Changes

• Length check in the rewrite pass: every ket of a tensor segment must have the same number of qubits as the first one. Otherwise AutoQ reports an AutoQError that names both kets, for example:

  [ERROR] .../EvaluationVisitorDirac.h:232: Not aligned: the ket |0⟩ has 1 qubit(s), but the ket |0x⟩ for the same qubits has 2.
  

  This one check covers all three shapes in the issue:
  • a shorter ket ({|0x> : |x|=1} ∪ {|0>}, or pre {|xy> : ...} with post {|0>});
  • a longer ket ({|x> : |x|=1} ∪ {|00>});
  • a ket that ends inside a constant unit ({|0x> : |x|=2} ∪ {|00>}).
• The unit loop no longer indexes an empty or too-short remainder. It reports Not aligned! instead, as a second line of defence.
• Shared ket length: the collect pass and the rewrite pass now compute a ket's length with the same helper, ket_units.

Behaviour change

The issue also notes that kets made only of constants, with different lengths across files, were not reported. For example, pre {|00>} with post {|0>} made ver print [failed]. These are now rejected with the same Not aligned error, since the postcondition describes a different number of qubits than the precondition. {|x0> : |x|=1} ∪ {|0>} was already rejected, with "Two automata of different numbers of qubits cannot be unioned together". It now gets the Not aligned message as well.

Testing

• New unit test, misaligned_kets_are_rejected:

  • the three shapes, and the shorter post.hsl with ReadTwoAutomata, throw AutoQError;
  • aligned input still parses.

  Without the fix, the test stops with the original std::out_of_range. With it, the test passes. ctest passes (2/2).

• Unchanged behaviour on the benchmarks: I compared ver/ex against the saved outputs of the cleanup PR (Repository cleanup: stray files, dead code and duplicated logic #63), 645 runs from every benchmark family.

  • 638 are identical.
  • The other 7 only hit the 60 s limit because the machine was overloaded (load average about 7 on 4 CPUs). Re-run one at a time, all 7 give the same [OK] as before. The old build was just as slow under the same load.

• print on .hsl files: identical output for every file that finished, across benchmarks/, demo/, unit_tests/ and docs/. Many larger instances timed out with both builds.

• This branch merges cleanly with Playground: add the one-Grover-iteration demo #67–Fix inclusion into an automaton with no root states (#40) #70.

🤖 Generated with Claude Code

https://claude.ai/code/session_013gtFQRPe1eSSpmA7EJ2KNY

[ondrik]

Checking that the alignment check is correct

Why the rule is right. docs/hsl_description.md (section Alignment) requires that kets in the same tensor segment describe the same qubits. That applies within a set, across ∪, and across the pre/post/invariant files. Rule 2 also assumes that every ket covers each qubit range. "All kets of a tensor segment have the same length" therefore follows from the format.

Why the implementation computes the right length.

• The grammar produces kets only as |…⟩ or ∑ varcons |…⟩, inside sets combined with ∪, ;, ⊗ and powers. Powers are expanded before these passes.
• The rewrite pass sets globalVar2len for each set before visiting its kets, exactly as the collect pass does (EvaluationVisitorSet.h). Both passes now compute ket length with the same helper, ket_units. Local variables take precedence over global ones, and complements (x' becomes X) are looked up in lower case, both as before.
• currentSegmentKetLength is reset when the rewrite pass enters each tensor segment (EvaluationVisitorTset.h). Segments of different sizes, such as {|0>} ⊗ {|11>}, are therefore unaffected.

Differential test. A random generator (source below) builds .hsl inputs that follow both alignment rules. The inputs contain:

• 1–3 tensor segments of 1–3 qubits each, split into constant and variable units;
• unions of sets and several diracs per set;
• superpositions with coefficients 1/2, -1/2 and ei2pi(1/4);
• global variables (|x|=k) with complements and x≠c constraints, and ∑-local variables.

Each input runs with autoq print and with autoq ver (pre and post generated independently from the same unit layout, with an empty circuit). It runs once with a build from before this PR and once with this branch. Each input is then made misaligned by adding or removing one qubit in one ket (in the file for print, in post.hsl for ver).

1,200 valid inputs (4 seeds × 300)
print	1,200 identical
ver	1,199 identical (64 [OK], 1,135 [failed]); 1 differed only by the old build exceeding the 30 s limit, see below

2,400 misaligned variants	before → after
abort (std::out_of_range, SIGABRT)	1,251 → Not aligned
"Two automata of different numbers of qubits cannot be unioned together"	700 → Not aligned
silently accepted: print printed a state	153 → Not aligned
silently accepted: ver gave [failed]	184 → Not aligned
silently accepted: ver gave [OK]	12 → Not aligned
the changed ket was the only ket in its segment, so the input was still aligned	100 → unchanged, accepted identically by both builds

• The inputs the old build accepted were wrong, not merely different. For example, {|1> + ei2pi(1/4) |10>, …} was printed as (1/1 + i * (1/1))|1>: the 2-qubit ket was read as the 1-qubit |1>. In one case, ver gave [OK] for a postcondition containing ei2pi(1/4) |1> + ei2pi(1/4) |10>.
• The one valid input that differed gives [failed] with both builds. The pre-PR build took 39 s, past the generator's 30 s limit, and this branch took 17 s. A build of current main without this change also takes 17 s, so the speed-up comes from changes already on main.

Other checks.

• The examples in docs/hsl_description.md give identical output with both builds.
• All 645 saved ver/ex benchmark runs give identical results, as described in the PR.
• The new unit test fails before the fix and passes after.

gen.py (the random differential test)

python3 gen.py <old autoq> <new autoq> <count> <seed> <work dir>

#!/usr/bin/env python3
"""Differential test for the ket-alignment check (#34).

Generates random Extended Dirac inputs that follow the alignment rules of
docs/hsl_description.md, runs `autoq print` (one file) and `autoq ver`
(pre/post with an empty circuit) with the old and the new build, and
compares. Then makes each input misaligned by adding or removing one qubit in
one ket and records what both builds do.

Usage: gen.py OLD NEW COUNT SEED WORKDIR
"""
import os, random, re, subprocess, sys
from collections import Counter

OLD, NEW, COUNT, SEED, WORK = sys.argv[1], sys.argv[2], int(sys.argv[3]), int(sys.argv[4]), sys.argv[5]
rng = random.Random(SEED)
os.makedirs(WORK, exist_ok=True)


def units_for(length):
    """Split a segment of `length` qubits into units: ('c', k) constant-only or ('v', k) variable."""
    units, left = [], length
    while left:
        k = rng.randint(1, min(2, left))
        units.append(('v' if rng.random() < 0.5 else 'c', k))
        left -= k
    return units


def const(k):
    return ''.join(rng.choice('01') for _ in range(k))


def make_set(units, global_letters):
    """One {diracs : varcons} set over the given units."""
    glob = {}  # letter -> length, declared in this set
    diracs = []
    for _ in range(rng.randint(1, 2)):
        terms = []
        for t in range(rng.randint(1, 2)):
            ket, local = '', None
            for kind, k in units:
                if kind == 'c' or rng.random() < 0.3:
                    ket += const(k)
                elif local is None and rng.random() < 0.3:
                    local = (rng.choice('ijk'), k)
                    ket += local[0]
                else:
                    letter = global_letters[len(ket) % len(global_letters)]
                    if letter in glob and glob[letter] != k:
                        ket += const(k)
                        continue
                    glob[letter] = k
                    ket += letter + ("'" if rng.random() < 0.2 else '')
            coef = rng.choice(['', '1/2 ', '-1/2 ', 'ei2pi(1/4) '])
            if local:
                term = f"{coef}∑ |{local[0]}|={local[1]} |{ket}>"
            else:
                term = f"{coef}|{ket}>"
            terms.append(term)
        diracs.append(' + '.join(terms))
    cons = [f"|{v}|={k}" for v, k in glob.items()]
    for v, k in glob.items():
        if rng.random() < 0.3:
            cons.append(f"{v}≠{const(k)}")
    # A global letter used only in a complemented or dropped position must still be declared.
    body = ', '.join(diracs)
    return '{' + body + (' : ' + ', '.join(cons) if cons else '') + '}'


def make_file(segments):
    parts = []
    for units in segments:
        sets = [make_set(units, 'xyzw') for _ in range(rng.randint(1, 2))]
        parts.append(' ∪ '.join(sets))
    return 'Extended Dirac\n' + ' ⊗ '.join(parts) + '\n'


def misalign(text):
    """Add or remove one qubit in one random ket."""
    kets = list(re.finditer(r'\|([01a-zA-Z\']+)>', text))
    m = rng.choice(kets)
    s = m.group(1)
    if rng.random() < 0.5 or len(s.replace("'", '')) <= 1:
        s2 = s + rng.choice('01')
    else:
        s2 = s[:-1] if s[-1] in '01' else s + '0'
        if s2 == s:
            s2 = s + '0'
    return text[:m.start(1)] + s2 + text[m.end(1):]


def run(binary, args):
    try:
        p = subprocess.run([binary] + args, cwd=WORK, capture_output=True, text=True, timeout=30)
        out = re.sub(r':\d+:', ':N:', p.stdout + p.stderr)
        out = re.sub(r'\[[0-9.]+(ms|us|s|m|h)?\]', '[T]', out)
        out = re.sub(r'\[\d+MB\]', '[MB]', out)
        return p.returncode, out
    except subprocess.TimeoutExpired:
        return 'timeout', ''


def outcome(code, out):
    if code == 'timeout':
        return 'timeout'
    if code < 0 or code == 134:
        return 'abort'
    if 'Not aligned' in out:
        return 'error: Not aligned'
    if code != 0:
        first = next((l for l in out.splitlines() if '[ERROR]' in l), out.strip()[:60])
        return 'error: ' + re.sub(r'^.*:N: ', '', first)[:70]
    if '[OK]' in out or '[failed]' in out:
        return 'verdict ' + ('[OK]' if '[OK]' in out else '[failed]')
    return 'ok'


aligned = Counter()
misaligned = Counter()
examples = []
for i in range(COUNT):
    segments = [units_for(rng.randint(1, 3)) for _ in range(rng.randint(1, 3))]
    n = sum(k for units in segments for _, k in units)
    pre, post = make_file(segments), make_file(segments)
    open(f'{WORK}/pre.hsl', 'w').write(pre)
    open(f'{WORK}/post.hsl', 'w').write(post)
    open(f'{WORK}/c.qasm', 'w').write(f'OPENQASM 2.0;\ninclude "qelib1.inc";\nqreg q[{n}];\n')
    for args in (['print', 'pre.hsl'], ['ver', 'pre.hsl', 'c.qasm', 'post.hsl']):
        o, nw = run(OLD, args), run(NEW, args)
        key = f"{args[0]}: {'same' if o == nw else 'DIFFERENT'} ({outcome(*o)})"
        aligned[key] += 1
        if o != nw:
            import shutil
            for f in ('pre.hsl', 'post.hsl', 'c.qasm'):
                shutil.copy(f'{WORK}/{f}', f'{WORK}/diff{i}_{f}')
            print(f'SAVED diff{i} ({args[0]}) old={o[0]} new={nw[0]}', flush=True)
        if o != nw and len(examples) < 5:
            examples.append(('aligned', args[0], pre, post, o, nw))
    # Misaligned variants: one ket in the single file, or one ket in post.hsl only.
    bad = misalign(pre)
    open(f'{WORK}/bad.hsl', 'w').write(bad)
    for args in (['print', 'bad.hsl'], ['ver', 'pre.hsl', 'c.qasm', 'bad_post.hsl']):
        if args[0] == 'ver':
            open(f'{WORK}/bad_post.hsl', 'w').write(misalign(post))
        o, nw = run(OLD, args), run(NEW, args)
        misaligned[f"{args[0]}: old {outcome(*o)} -> new {outcome(*nw)}"] += 1
        if (outcome(*nw) != 'error: Not aligned' or outcome(*o) == 'ok' or outcome(*o).startswith('verdict')) and len(examples) < 12:
            examples.append(('misaligned', args[0], bad, open(f'{WORK}/bad_post.hsl').read() if args[0] == 'ver' else '', o, nw))

print(f"== {COUNT} aligned inputs (print and ver):")
for k, v in sorted(aligned.items()):
    print(f"  {v:6d}  {k}")
print(f"== misaligned variants:")
for k, v in sorted(misaligned.items(), key=lambda kv: -kv[1]):
    print(f"  {v:6d}  {k}")
for ex in examples:
    print('---', ex[0], ex[1]); print(ex[2]); print(ex[3]); print('old:', ex[4]); print('new:', ex[5])

🤖 Generated with Claude Code

https://claude.ai/code/session_013gtFQRPe1eSSpmA7EJ2KNY