🐛 Enforce quantum allocation and QIR output contracts

[simon1hofmann]

🤖 AI text below 🤖

Description

Dynamic QC/QCO qubit allocations must occur directly in the entry block of the mqt.entry_point function. The shared MQT verifier enforces this program contract, builders reject invalid insertion points, and standalone QIR and mapping passes invoke the same allocation check before transforming input.

Adaptive QIR preserves the control-flow position of quantum releases. Scalar results now use dynamic allocation alongside result registers, and only owned results are released. The QIR builder applies the same result policy independently of qubit allocation and releases owned qubits at finalization.

Shared QIR output preparation requires one entry-function return and validates measurement/store fusion before rewriting returns or deleting stores. Fusion requires the same block, an available index, and no intervening classical interference; stores to distinct constant indices remain supported. Unknown effects, overlapping writes, and changed execution conditions produce diagnostics. qc.yield is effect-free so recursive analysis can recognize supported quantum modifier bodies.

Addresses the conditional-allocation finding in #2287 and the allocation, lifetime, result-ownership, and output-store audit findings. No new dependencies.

Validation: 1,952 native tests passed across the mapping, compiler, MQT/QC/QCO/QIR IR, QC-to-QCO, Base/Adaptive QIR, and OpenQASM suites after integrating main (784519cf9). The release build used AppleClang 21 with LLVM/MLIR 23.1.0 and ENABLE_IPO=ON. The compiler and MQT suites were rebuilt and passed again after fixing two lint warnings in the merged tests. uvx nox -s lint and uvx nox -s cpp-lint passed; C++ lint checked every line of the changed C++ files with clang-tidy 23 and reported zero findings. Hosted CI for the updated head is pending; the full Python and documentation suites were not run locally.

The allocation-verifier tests use SCF without an added CF dependency, and the conditional-release regression uses scf.if. CF remains an internal QIR lowering dependency and is used to test rejection of unsupported multiple returns. Changelog and upgrade-guide updates for unreleased v4 functionality are deferred to the release cleanup.

GPT-6 via Codex assisted the implementation, regression tests, validation, and PR text.

Checklist

• The pull request only contains commits that are focused and relevant to this change.
• I have added appropriate tests that cover the new/changed functionality.
• I have updated the documentation to reflect these changes.
• I have added entries to the changelog for any noteworthy additions, changes, fixes, or removals.
• I have added migration instructions to the upgrade guide (if needed).
• The changes follow the project's style guidelines and introduce no new warnings.
• The changes are fully tested and pass the CI checks.
• I have reviewed my own code changes.

If PR contains AI-assisted content:

• Any agent that created, edited, or submitted GitHub content was explicitly authorized for that scope, as required by our AI Usage Guidelines.
• Every agent-authored or agent-edited public text body begins with the visible disclosure 🤖 *AI text below* 🤖 (titles are exempt).
• I have disclosed AI assistance in the PR description.
• I confirm that I have personally reviewed and understood all AI-generated content, and accept full responsibility for it.

[codecov]

Codecov Report

❌ Patch coverage is 97.18310% with 6 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
...lir/lib/Conversion/QCToQIR/QIRCommon/QIRCommon.cpp	96.4%	4 Missing ⚠️
...Conversion/QCToQIR/QIRAdaptive/QCToQIRAdaptive.cpp	93.7%	1 Missing ⚠️
...lir/lib/Conversion/QCToQIR/QIRBase/QCToQIRBase.cpp	80.0%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!

[burgholzer]

I am wondering whether this is the right scope to reject this.
Shouldn't we reject this at the QC/QCO dialect verification level already? I do not think our current infrastructure can handle programs with allocations placed in SCF regions or modifiers (which already forbid them).
Even functions, at least how they are currently implemented, do not really support this.

[simon1hofmann]

🤖 AI text below 🤖

@burgholzer Yes, if this is a general allocation invariant, checking it once during QC/QCO program verification makes sense.

There is existing behavior to align: this QC-to-QCO test explicitly verifies and converts an allocation inside scf.if, and the ordinary QC/QCO function builders track helper-local resources. Modifiers already reject scalar qubit allocations, while mqt.unitary functions reject non-unitary operations. A general ban would therefore tighten the current contract, not just move an existing verifier check.

Is the intended rule that dynamic quantum allocations may occur only in the entry block of the mqt.entry_point function, with ordinary helper functions receiving their quantum resources as arguments?

If so, I propose reworking this PR to enforce that rule consistently for qc.alloc, qco.alloc, qubit memref.alloc, and quantum qtensor.alloc; align the builders, documentation, and verification tests; then remove the Adaptive-specific allocation scan. Checking only the scalar allocation operations would leave the register cases uncovered. Classical allocations and static qubit references would stay out of scope.

The code is unchanged pending agreement on that scope.

[burgholzer]

Is the intended rule that dynamic quantum allocations may occur only in the entry block of the mqt.entry_point function, with ordinary helper functions receiving their quantum resources as arguments?

Yeah, I would be tempted to say so.
This feels like an assumption to go with and simplify around.
We may loosen that in the future, but for now I actually think it may help to be explicit.

[simon1hofmann]

🤖 AI text below 🤖

@burgholzer Implemented the agreed rule in 6fc5241 and rebased onto main
at ec799da.

Dynamic qc.alloc, qco.alloc, qubit memref.alloc, and qtensor.alloc
must now appear directly in the entry block of the mqt.entry_point function.
The shared MQT entry-point verifier owns this check; QC/QCO program imports
also enforce it for modules without an entry marker and caller-supplied
contexts. Builders, documentation, and tests follow the same rule. Helpers
receive quantum resources as arguments; classical allocations and static qubit
references remain unchanged.

Removed the Adaptive-specific allocation scan and the redundant Mapping
placement check. Mapping now discovers allocations directly in the entry block.

Local validation passed: the full lint-preset build, all 2,358 configured MLIR
CTest entries with LLVM/MLIR 23.1.0, uvx nox -s lint, and whole-changed-file
uvx nox -s cpp-lint against the new base. Local clang-tidy was 23.0.0git;
these results do not attest to CI for this push.

[burgholzer]

I iterated on this quite a bit and added another QIR audit on top of it. This does a bit more now, but I believe it does it well.
If you are fine with the changes as well, let's get this in.