Skip to content

🔍 Audit MLIR pass, verifier, and rewrite contracts - #2287

Open
simon1hofmann wants to merge 17 commits into
mainfrom
codex/2255-qir-base-contract
Open

🔍 Audit MLIR pass, verifier, and rewrite contracts#2287
simon1hofmann wants to merge 17 commits into
mainfrom
codex/2255-qir-base-contract

Conversation

@simon1hofmann

@simon1hofmann simon1hofmann commented Aug 31, 2026

Copy link
Copy Markdown
Contributor

🤖 AI text below 🤖

Description

Records five reproduced correctness failures in MLIR lowering and JeFF import,
with minimal CLI examples, source evidence, ownership, and limits for each
proposed fix. The audit is based on main at 6cc98f059.

The diff contains only one 271-line audit report.
There are no production or test changes; the findings remain open for focused
fixes. The report also reconciles the merged and closed split PRs.

Passes may assume verified IR. The retained findings concern valid source
programs or an external import boundary. Generic pass-entry validation,
invalid-QCO regressions, blanket failure-atomicity requirements, and speculative
resource caps are excluded.

Confirmed findings

  1. High: QIR Base moves a later gate before a measurement of the same qubit,
    changing the recorded result.
  2. High: QC-to-QCO aborts on valid branches that use the same dominating
    qubit reference.
  3. High: a malformed JeFF file aborts the importing process instead of
    returning an import error.
  4. Medium: sparse static qubit IDs produce insufficient QIR resource
    metadata; ID 7 is emitted with required_num_qubits="1".
  5. Medium: Adaptive QIR moves a branch-local qubit release into the epilogue,
    producing a dominance error and failing compilation.

Validation

  • Built the compiler and compiler tests with LLVM/MLIR 23.1.0 and the pinned
    jeff-mlir dependency.
  • All 163 compiler tests passed.
  • Executed all five CLI reproducers after rebuilding the merged branch. They
    confirm the existing failures; this PR does not implement their fixes.
  • uvx nox -s lint and git diff --check passed.
  • Current GitHub CI has not been verified as part of this update.

Tracks #2255.

Checklist

  • The pull request's diff is focused and relevant to this change.
  • I have added appropriate tests that cover the new/changed functionality. — N/A: report only; executed reproducers are included in the report.
  • I have updated the documentation to reflect these changes.
  • I have added entries to the changelog for any noteworthy additions, changes, fixes, or removals. — N/A: internal audit report only.
  • I have added migration instructions to the upgrade guide (if needed). — N/A: no API or behavior changes.
  • The changes follow the project's style guidelines and introduce no new warnings.
  • The changes are fully tested and pass the CI checks. — Local checks passed; current CI is unverified.
  • The final report and diff have been reviewed.

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.

AI assistance disclosure: Codex refreshed the audit against current main,
reproduced the retained findings, removed the old implementation snapshot, and
updated this description under explicit human direction. Human review remains
required before acceptance or merge.

Audit every MQT-owned pass, verifier, rewrite pattern, conversion target, and registration surface. Harden diagnostics, atomicity, resource bounds, metadata checks, and importer boundaries.

Add focused regressions across conversions, QIR, mapping, JEFF, OpenQASM, decision diagrams, and Qiskit interoperability.

Assisted-by: GPT-5.6 Sol via Codex
…ontract

# Conflicts:
#	mlir/lib/Compiler/Programs.cpp
#	mlir/lib/Dialect/QCO/IR/Modifiers/ModifierUtils.cpp
#	mlir/unittests/Conversion/QCToQCO/test_qc_to_qco.cpp
@simon1hofmann simon1hofmann self-assigned this Sep 1, 2026
Preserve landed focused fixes while retaining the independent contract-audit guards and regressions.

Assisted-by: GPT-5.6 via Codex
Preserve the dependency-safe behavior from #2301 while retaining terminal-reset handling from the contract audit.

Assisted-by: GPT-5.6 via Codex
@mergify mergify Bot removed the conflict label Sep 1, 2026
Record the focused pull request outcomes and revise the audit gate so passes may assume verifier-valid IR. Withdraw speculative and invalid-input findings across the original snapshot.

Assisted-by: GPT-5.6 via Codex
@simon1hofmann simon1hofmann changed the title ♻️ Harden MLIR pass, verifier, and rewrite contracts 🔍 Audit MLIR pass, verifier, and rewrite contracts Sep 1, 2026
Move the invalid-QCO finding from pending withdrawal to closed and refresh the focused audit counts.

Assisted-by: GPT-5.6 via Codex
@mergify mergify Bot added the conflict label Sep 1, 2026
…ontract

# Conflicts:
#	mlir/include/mlir/Conversion/CBitToMemRef/CBitToMemRef.td
#	mlir/lib/Conversion/CBitToMemRef/CBitToMemRef.cpp
@burgholzer burgholzer added this to the v4.0.0 - IEEE Quantum Week milestone Sep 1, 2026
Remove focused, merged, closed, malformed-IR, and speculative changes from the audit snapshot. Retain only uniquely owned boundary, verifier, resource, semantic, and output-atomicity findings, with valid regressions.

Assisted-by: GPT-5.6 via Codex
…ontract

# Conflicts:
#	mlir/unittests/Conversion/QCOToQC/test_qco_to_qc.cpp
Accept valid QC programs whose dynamic register indices cannot be proven distinct, and remove a registration-only assertion without an executable reproducer. Finalize the reconciled audit counts and validation record.

Assisted-by: GPT-5.6 via Codex
@mergify mergify Bot added conflict and removed conflict labels Sep 1, 2026
Extract scalar floats from MLIR pass options before calling std::isfinite so the retained option validation compiles with MSVC.

Assisted-by: GPT-5.6 via Codex
@mergify mergify Bot added the conflict label Sep 1, 2026
Retain the audit conversion validation and atomicity changes while integrating the focused constant-folding, benchmark-registration, and idempotent QIR metadata updates now on main.

Assisted-by: GPT-5.6 via Codex
Remove the five implementation and regression copies now owned by #2318 through #2322 while preserving the complete audit ledger.

Clear the remaining changed-file Clang-Tidy warnings exposed by the reduced snapshot.

Assisted-by: GPT-5.6 via Codex
Preserve the audit mapping validation and failure-atomic rewrite while adopting the separated placement and routing implementation.

Assisted-by: GPT-5.6 via Codex
Merge main and replace the residual implementation snapshot with five reproduced findings and their minimal CLI examples.

Assisted-by: GPT-6 via Codex
Assisted-by: GPT-6 via Codex
@mergify mergify Bot removed the conflict label Sep 7, 2026
@simon1hofmann

Copy link
Copy Markdown
Contributor Author

@burgholzer I let Astra rerun the audit to only focus on reproducible and real findings. It identified 5 actionable items, let me know what you think and I'll be happy to implement them if needed.

@simon1hofmann
simon1hofmann marked this pull request as ready for review September 7, 2026 13:24

@burgholzer burgholzer left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @simon1hofmann 🙏🏼 commented on all five findings. SHould hopefully be enough for resolving them 😌 let me know if not!

Comment on lines +51 to +58
```qasm
OPENQASM 3.0;
include "stdgates.inc";
qubit q;
bit c;
c = measure q;
x q;
```

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, this can definitely not be a valid base profile program. (at least not without any passes commuting gates through measurements).
Let's fix this.

Comment on lines +96 to +101
cf.cond_br %c, ^then, ^else
^then:
qc.x %q : !qc.qubit
return
^else:
qc.z %q : !qc.qubit

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we do not really support generic cf flow (yet). And I would rather like to hard-fail here with a diagnostic.
None of the input programs/program formats should currently produce such instructions; we just need to make this more explicit.

Comment on lines +146 to +149
Observed: exit 134 (`SIGABRT`) and `LLVM ERROR: No functions found in module`.
The stack reaches `deserializeFromFile` from `loadJeffFile`. The CLI failure was
executed; the byte/file library methods' use of the same fatal dependency was
checked in source, not in a separate host-process experiment.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This definitely needs to be fixed 👍🏼

Comment on lines +186 to +193
Observed: exit 0; `x` receives `inttoptr (i64 7 to ptr)`, but the entry point
declares `required_num_qubits="1"`. Preserving ID 7 requires a capacity of at
least 8. The emitted program therefore violates the target contract.

**Limits and disposition.** Proposed. Preserve physical-qubit identity; do not
silently renumber mapped qubits. The regression should check capacity and the
retained ID. Sparse result IDs and other pointer-provenance cases were not
separately reproduced and are not additional findings here.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, this should also be fixed. This is a valid program.

Comment on lines +214 to +218
scf.if %c {
%q = qco.alloc : !qco.qubit
%out = qco.x %q : !qco.qubit -> !qco.qubit
qco.sink %out : !qco.qubit
}

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Puh. I am not sure we actually should allow this at the moment.
I believe none of the frontends we currently support allow qubit allocations in SCF constructs. Maybe we should just be rather explicit on forbidding this?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

code quality Code quality improvements MLIR Anything related to MLIR refactor Anything related to code refactoring

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants