From 967e93081326f5c709e3255d8a3a1d4b48540c34 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Wed, 3 Jun 2026 15:35:10 +0200
Subject: [PATCH 01/32] Start refactoring

---
 mlir/lib/Support/IRVerification.cpp      | 322 ++++++++++-------------
 mlir/unittests/programs/qc_programs.cpp  |   9 +-
 mlir/unittests/programs/qco_programs.cpp |  13 +-
 3 files changed, 149 insertions(+), 195 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index eaac426f0a..d8da874994 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -20,6 +20,9 @@
 #include <llvm/ADT/STLExtras.h>
 #include <llvm/ADT/SmallVector.h>
 #include <llvm/ADT/StringRef.h>
+#include <llvm/Support/Debug.h>
+#include <llvm/Support/raw_ostream.h>
+#include <mlir/Analysis/SliceAnalysis.h>
 #include <mlir/Dialect/Arith/IR/Arith.h>
 #include <mlir/Dialect/Func/IR/FuncOps.h>
 #include <mlir/Dialect/LLVMIR/LLVMDialect.h>
@@ -29,7 +32,9 @@
 #include <mlir/IR/Block.h>
 #include <mlir/IR/BuiltinAttributes.h>
 #include <mlir/IR/BuiltinOps.h>
+#include <mlir/IR/IRMapping.h>
 #include <mlir/IR/OpDefinition.h>
+#include <mlir/IR/Operation.h>
 #include <mlir/IR/Region.h>
 #include <mlir/IR/SymbolTable.h>
 #include <mlir/IR/Value.h>
@@ -44,6 +49,8 @@ using namespace mlir;
 
 namespace {
 
+using Slice = SetVector<Operation*>;
+
 /// Compute a structural hash for an operation (excluding SSA value identities).
 /// This hash is based on operation name, types, and attributes only.
 struct OperationStructuralHash {
@@ -515,7 +522,7 @@ static bool areOperationsEquivalent(Operation* lhs, Operation* rhs,
 
   // Check operands according to value mapping
   for (auto [lhsOperand, rhsOperand] :
-       llvm::zip(lhs->getOperands(), rhs->getOperands())) {
+       llvm::zip_equal(lhs->getOperands(), rhs->getOperands())) {
     if (auto it = valueMap.find(lhsOperand); it != valueMap.end()) {
       // Value already mapped, must match
       if (it->second != rhsOperand) {
@@ -536,26 +543,6 @@ static bool areOperationsEquivalent(Operation* lhs, Operation* rhs,
   return true;
 }
 
-/// Forward declaration for mutual recursion.
-static bool areBlocksEquivalent(Block& lhs, Block& rhs,
-                                ValueEquivalenceMap& valueMap);
-
-/// Compare two regions for structural equivalence.
-static bool areRegionsEquivalent(Region& lhs, Region& rhs,
-                                 ValueEquivalenceMap& valueMap) {
-  if (lhs.getBlocks().size() != rhs.getBlocks().size()) {
-    return false;
-  }
-
-  for (auto [lhsBlock, rhsBlock] : llvm::zip(lhs, rhs)) {
-    if (!areBlocksEquivalent(lhsBlock, rhsBlock, valueMap)) {
-      return false;
-    }
-  }
-
-  return true;
-}
-
 /// Check if an operation has memory effects or control flow side effects
 /// that would prevent reordering.
 static bool hasOrderingConstraints(Operation* op) {
@@ -593,220 +580,186 @@ static bool hasOrderingConstraints(Operation* op) {
   return false;
 }
 
-/// Build a dependence graph for operations.
-/// Returns a map from each operation to the set of operations it depends on.
-DenseMap<Operation*, DenseSet<Operation*>> static buildDependenceGraph(
-    ArrayRef<Operation*> ops) {
-  DenseMap<Operation*, DenseSet<Operation*>> dependsOn;
-  DenseMap<Value, Operation*> valueProducers;
+/// Returns a vector of maximum reachable independent DAGs, as defined via their
+/// def-use chain, where the operations of the setvector are topologically
+/// sorted. The vector is sorted by the size of the DAG (i.e., the number of
+/// operations).
+static SmallVector<Slice> getDisjointSlices(Block& b) {
+  const auto filter = [&b](Operation* op) { return op->getBlock() == &b; };
 
-  // Build value-to-producer map and dependence relationships
-  for (Operation* op : ops) {
-    dependsOn[op] = DenseSet<Operation*>();
+  const BackwardSliceOptions backwardSliceOptions(filter);
+  const SliceOptions forwardSliceOptions(filter);
 
-    // This operation depends on the producers of its operands
-    for (const auto operand : op->getOperands()) {
-      if (auto it = valueProducers.find(operand); it != valueProducers.end()) {
-        dependsOn[op].insert(it->second);
-      }
-    }
+  DenseSet<Operation*> visited;
+  visited.reserve(range_size(b.getOperations()));
 
-    // Register this operation as the producer of its results
-    for (auto result : op->getResults()) {
-      valueProducers[result] = op;
+  SmallVector<SetVector<Operation*>> dags;
+  for (Operation& op : b.getOperations()) {
+    if (visited.contains(&op)) {
+      continue;
     }
+    const auto slice = getSlice(&op, backwardSliceOptions, forwardSliceOptions);
+    const auto& dag = dags.emplace_back(slice);
+    visited.insert_range(dag);
   }
 
-  return dependsOn;
+  sort(dags, [](const auto& lhs, const auto& rhs) {
+    return lhs.size() < rhs.size();
+  });
+
+  return dags;
 }
 
-/// Partition operations into groups that can be compared as multisets.
-/// Operations in the same group are independent and can be reordered.
-SmallVector<SmallVector<Operation*>> static partitionIndependentGroups(
-    ArrayRef<Operation*> ops) {
-  SmallVector<SmallVector<Operation*>> groups;
-  if (ops.empty()) {
-    return groups;
-  }
+static bool areTopLevelEquivalent(Operation* lhs, Operation* rhs) {
+  return lhs->getName() == rhs->getName() &&
+         lhs->getNumOperands() == rhs->getNumOperands() &&
+         lhs->getOperandTypes() == rhs->getOperandTypes() &&
+         lhs->getNumResults() == rhs->getNumResults() &&
+         lhs->getResultTypes() == rhs->getResultTypes() &&
+         lhs->getAttrs().size() == rhs->getAttrs().size() &&
+         lhs->getNumRegions() == rhs->getNumRegions();
 
-  auto dependsOn = buildDependenceGraph(ops);
-  SmallVector<Operation*> currentGroup;
+  
+}
 
-  for (auto* op : ops) {
-    bool dependsOnCurrent = false;
+/// Extract and return "ready" operations from the slice.
+static Slice getReadyOps(Slice& slice, DenseSet<Operation*> finished) {
+  const auto isReady = [&](OpOperand& operand) {
+    if (isa<BlockArgument>(operand.get())) {
+      return true; // The defining op is finished?
+    }
+    return finished.contains(operand.get().getDefiningOp());
+  };
 
-    // Check if this operation depends on any operation in the current group
-    for (auto* groupOp : currentGroup) {
-      if (!dependsOn[op].contains(groupOp)) {
-        continue;
-      }
-      if (isCommutableQTensorInsertDependency(op, groupOp)) {
-        continue;
-      }
-      dependsOnCurrent = true;
-      break;
+  Slice ready;
+  for (Operation* op : slice) {
+    if (llvm::all_of(op->getOpOperands(), isReady)) {
+      ready.insert(op);
+      continue;
     }
 
-    // Check if this operation has ordering constraints
-    const auto hasConstraints = hasOrderingConstraints(op);
+    // If the destination of a tensor insert, has been produced by an insert
+    // operation as well, these two should be interchangable. Thus, also add it
+    // to the ready set vector. Any valid IR will ensure that the indices of the
+    // two insertions are not equivalent, hence, we don't check them here.
 
-    // If it depends on current group or has ordering constraints,
-    // finalize the current group and start a new one
-    if (dependsOnCurrent || (hasConstraints && !currentGroup.empty())) {
-      if (!currentGroup.empty()) {
-        groups.push_back(std::move(currentGroup));
-        currentGroup = {};
+    if (auto insert = dyn_cast<qtensor::InsertOp>(op)) {
+      Operation* prev = insert.getDest().getDefiningOp();
+      if (isa<qtensor::InsertOp>(prev)) {
+        if (ready.contains(prev)) {
+          ready.insert(insert.getOperation());
+        }
       }
     }
 
-    currentGroup.push_back(op);
+    // Analogously for the extract operation.
 
-    // If this operation has ordering constraints, finalize the group
-    if (hasConstraints) {
-      groups.push_back(std::move(currentGroup));
-      currentGroup = {};
+    if (auto extract = dyn_cast<qtensor::ExtractOp>(op)) {
+      Operation* prev = extract.getTensor().getDefiningOp();
+      if (isa<qtensor::ExtractOp>(prev)) {
+        if (ready.contains(prev)) {
+          ready.insert(extract.getOperation());
+        }
+      }
     }
   }
 
-  // Add any remaining operations
-  if (!currentGroup.empty()) {
-    groups.push_back(std::move(currentGroup));
-  }
-
-  return groups;
+  return ready;
 }
 
-/// Compare two groups of independent operations using multiset equivalence.
-static bool areIndependentGroupsEquivalent(ArrayRef<Operation*> lhsOps,
-                                           ArrayRef<Operation*> rhsOps) {
-  if (lhsOps.size() != rhsOps.size()) {
-    return false;
-  }
+static bool areEquivalent(Region& lhs, Region& rhs, IRMapping& m);
 
-  // Build frequency maps for both groups
-  DenseMap<StructuralOperationKey, size_t> lhsFrequencyMap;
-  DenseMap<StructuralOperationKey, size_t> rhsFrequencyMap;
-
-  for (auto* op : lhsOps) {
-    lhsFrequencyMap[StructuralOperationKey(op)]++;
-  }
+static bool areEquivalent(Slice& lhs, Slice& rhs, IRMapping& m) {
+  DenseSet<Operation*> finished;
+  finished.reserve(lhs.size() + rhs.size());
 
-  for (auto* op : rhsOps) {
-    rhsFrequencyMap[StructuralOperationKey(op)]++;
-  }
+  while (true) {
+    const auto readyLhs = getReadyOps(lhs, finished);
+    const auto readyRhs = getReadyOps(rhs, finished);
 
-  // Check structural equivalence
-  if (lhsFrequencyMap.size() != rhsFrequencyMap.size()) {
-    return false;
-  }
+    if (readyLhs.empty() || readyRhs.empty()) {
+      break;
+    }
 
-  // NOLINTNEXTLINE(bugprone-nondeterministic-pointer-iteration-order)
-  for (const auto& [lhsKey, lhsCount] : lhsFrequencyMap) {
-    auto it = rhsFrequencyMap.find(lhsKey);
-    if (it == rhsFrequencyMap.end() || it->second != lhsCount) {
+    if (readyLhs.size() != readyRhs.size()) {
       return false;
     }
+
+    // Greedily search for a structural equivalent operation.
+    for (Operation* opLhs : readyLhs) {
+      for (Operation* opRhs : readyRhs) {
+        if (areTopLevelEquivalent(opLhs, opRhs)) { // TODO: Full equivalence check with attrs etc. 
+          m.map(opLhs, opRhs); // Map operations.
+          // Map operands.
+          // Map results.
+
+          llvm::dbgs() << opLhs->getName() << " == " << opRhs->getName()
+                       << '\n';
+        }
+      }
+    }
+
+    // for (Operation* op : readyLhs) {
+    //   op->dumpPretty();
+    //   for (Region& region : op->getRegions()) {
+    //     IRMapping m;
+    //     if (!areEquivalent(region, region, m)) {
+    //       return false;
+    //     }
+    //   }
+    // }
+
+    finished.insert_range(readyLhs);
+    lhs.set_subtract(readyLhs);
+
+    finished.insert_range(readyRhs);
+    rhs.set_subtract(readyRhs);
   }
 
-  return true;
+  return lhs.empty() && rhs.empty();
 }
 
 /// Compare two blocks for structural equivalence, allowing permutations
 /// of independent operations.
-static bool areBlocksEquivalent(Block& lhs, Block& rhs,
-                                ValueEquivalenceMap& valueMap) {
-  // Check block arguments
+static bool areEquivalent(Block& lhs, Block& rhs, IRMapping& m) {
   if (lhs.getNumArguments() != rhs.getNumArguments()) {
     return false;
   }
 
-  for (auto [lhsArg, rhsArg] :
-       llvm::zip(lhs.getArguments(), rhs.getArguments())) {
-    if (lhsArg.getType() != rhsArg.getType()) {
+  for (auto [lArg, rArg] :
+       llvm::zip_equal(lhs.getArguments(), rhs.getArguments())) {
+    if (lArg.getType() != rArg.getType()) {
       return false;
     }
-    valueMap[lhsArg] = rhsArg;
-  }
-
-  // Collect all operations
-  SmallVector<Operation*> lhsOps;
-  SmallVector<Operation*> rhsOps;
-
-  for (Operation& op : lhs) {
-    lhsOps.push_back(&op);
-  }
-
-  for (Operation& op : rhs) {
-    rhsOps.push_back(&op);
-  }
 
-  if (lhsOps.size() != rhsOps.size()) {
-    return false;
+    m.map(lArg, rArg);
   }
 
-  // Partition operations into independent groups
-  auto lhsGroups = partitionIndependentGroups(lhsOps);
-  auto rhsGroups = partitionIndependentGroups(rhsOps);
+  auto lDAGs = getDisjointSlices(lhs);
+  auto rDAGs = getDisjointSlices(rhs);
 
-  if (lhsGroups.size() != rhsGroups.size()) {
+  if (lDAGs.size() != rDAGs.size()) {
     return false;
   }
 
-  // Compare each group
-  for (size_t groupIdx = 0; groupIdx < lhsGroups.size(); ++groupIdx) {
-    auto& lhsGroup = lhsGroups[groupIdx];
-    auto& rhsGroup = rhsGroups[groupIdx];
-
-    const bool lhsInsertGroup = llvm::all_of(lhsGroup, isQTensorInsertOp);
-    const bool rhsInsertGroup = llvm::all_of(rhsGroup, isQTensorInsertOp);
-    if (lhsInsertGroup || rhsInsertGroup) {
-      if (!lhsInsertGroup || !rhsInsertGroup) {
-        return false;
-      }
-      if (!areInsertGroupsEquivalent(lhsGroup, rhsGroup, valueMap)) {
-        return false;
-      }
-      continue;
-    }
-
-    if (!areIndependentGroupsEquivalent(lhsGroup, rhsGroup)) {
+  for (const auto& [lDAG, rDAG] : llvm::zip_equal(lDAGs, rDAGs)) {
+    if (lDAG.size() != rDAG.size() || !areEquivalent(lDAG, rDAG, m)) {
       return false;
     }
+  }
 
-    // Update value mappings for operations in this group
-    // We need to match operations and update the value map
-    // Since they are structurally equivalent, we can match them
-    // by trying all permutations (for small groups) or use a greedy approach
-
-    // Use a simple greedy matching
-    DenseSet<Operation*> matchedRhs;
-    for (Operation* lhsOp : lhsGroup) {
-      bool matched = false;
-      for (Operation* rhsOp : rhsGroup) {
-        if (matchedRhs.contains(rhsOp)) {
-          continue;
-        }
+  return true;
+}
 
-        ValueEquivalenceMap tempMap = valueMap;
-        if (areOperationsEquivalent(lhsOp, rhsOp, tempMap)) {
-          valueMap = std::move(tempMap);
-          matchedRhs.insert(rhsOp);
-          matched = true;
-
-          // Recursively compare regions
-          for (auto [lhsRegion, rhsRegion] :
-               llvm::zip(lhsOp->getRegions(), rhsOp->getRegions())) {
-            if (!areRegionsEquivalent(lhsRegion, rhsRegion, valueMap)) {
-              return false;
-            }
-          }
-          break;
-        }
-      }
+/// Compare two regions for structural equivalence.
+static bool areEquivalent(Region& lhs, Region& rhs, IRMapping& m) {
+  if (lhs.getBlocks().size() != rhs.getBlocks().size()) {
+    return false;
+  }
 
-      if (!matched) {
-        return false;
-      }
+  for (auto [lhsBlock, rhsBlock] : llvm::zip_equal(lhs, rhs)) {
+    if (!areEquivalent(lhsBlock, rhsBlock, m)) {
+      return false;
     }
   }
 
@@ -814,7 +767,6 @@ static bool areBlocksEquivalent(Block& lhs, Block& rhs,
 }
 
 bool areModulesEquivalentWithPermutations(ModuleOp lhs, ModuleOp rhs) {
-  ValueEquivalenceMap valueMap;
-  return areRegionsEquivalent(lhs.getBodyRegion(), rhs.getBodyRegion(),
-                              valueMap);
+  IRMapping m;
+  return areEquivalent(lhs.getBodyRegion(), rhs.getBodyRegion(), m);
 }
diff --git a/mlir/unittests/programs/qc_programs.cpp b/mlir/unittests/programs/qc_programs.cpp
index 373452252a..b118601af3 100644
--- a/mlir/unittests/programs/qc_programs.cpp
+++ b/mlir/unittests/programs/qc_programs.cpp
@@ -272,11 +272,10 @@ void trivialControlledX(QCProgramBuilder& b) {
 }
 
 void repeatedControlledX(QCProgramBuilder& b) {
-  auto control = b.allocQubit();
-  b.h(control);
-  for (auto i = 0; i < 50; i++) {
-    auto qubit = b.allocQubit();
-    b.cx(control, qubit);
+  auto q = b.allocQubitRegister(2);
+  b.h(q[0]);
+  for (auto i = 0; i < 2; i++) {
+    b.cx(q[0], q[1]);
   }
 }
 
diff --git a/mlir/unittests/programs/qco_programs.cpp b/mlir/unittests/programs/qco_programs.cpp
index 0ad96fbb10..f48444d1ff 100644
--- a/mlir/unittests/programs/qco_programs.cpp
+++ b/mlir/unittests/programs/qco_programs.cpp
@@ -272,11 +272,14 @@ void trivialControlledX(QCOProgramBuilder& b) {
 }
 
 void repeatedControlledX(QCOProgramBuilder& b) {
-  auto q0 = b.allocQubit();
-  auto control = b.h(q0);
-  for (auto i = 0; i < 50; i++) {
-    auto qubit = b.allocQubit();
-    control = b.cx(control, qubit).first;
+  Value q0;
+  Value q1;
+  auto tensor = b.qtensorAlloc(2);
+  std::tie(tensor, q0) = b.qtensorExtract(tensor, 0);
+  q0 = b.h(q0);
+  std::tie(tensor, q1) = b.qtensorExtract(tensor, 1);
+  for (auto i = 0; i < 2; i++) {
+    std::tie(q0, q1) = b.cx(q0, q1);
   }
 }
 

From 13f80c0abe7588cde2a21fb6702ebf69109f7b56 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Tue, 9 Jun 2026 16:06:25 +0200
Subject: [PATCH 02/32] Add operation equivalence and tensor-chain equivalence
 "class" logic

---
 mlir/include/mlir/Support/IRVerification.h |   6 +-
 mlir/lib/Support/IRVerification.cpp        | 341 +++++++++++----------
 mlir/unittests/programs/qco_programs.cpp   |   2 +-
 3 files changed, 191 insertions(+), 158 deletions(-)

diff --git a/mlir/include/mlir/Support/IRVerification.h b/mlir/include/mlir/Support/IRVerification.h
index 9ecb49a59c..4421c6c4c0 100644
--- a/mlir/include/mlir/Support/IRVerification.h
+++ b/mlir/include/mlir/Support/IRVerification.h
@@ -12,9 +12,9 @@
 
 namespace mlir {
 class ModuleOp;
-}
+} // namespace mlir
 
 /// Compare two MLIR modules for structural equivalence, allowing permutations
 /// of speculatable operations.
-[[nodiscard]] bool areModulesEquivalentWithPermutations(mlir::ModuleOp lhs,
-                                                        mlir::ModuleOp rhs);
+[[nodiscard]] bool areModulesEquivalentWithPermutations(mlir::ModuleOp,
+                                                        mlir::ModuleOp);
diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index d8da874994..e504d5b0bb 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -10,7 +10,9 @@
 
 #include "mlir/Support/IRVerification.h"
 
+#include "mlir/Dialect/QCO/IR/QCODialect.h"
 #include "mlir/Dialect/QTensor/IR/QTensorUtils.h"
+#include "mlir/Dialect/QTensor/Utils/TensorIterator.h"
 
 #include <llvm/ADT/ArrayRef.h>
 #include <llvm/ADT/DenseMap.h>
@@ -20,7 +22,9 @@
 #include <llvm/ADT/STLExtras.h>
 #include <llvm/ADT/SmallVector.h>
 #include <llvm/ADT/StringRef.h>
+#include <llvm/Support/Casting.h>
 #include <llvm/Support/Debug.h>
+#include <llvm/Support/ErrorHandling.h>
 #include <llvm/Support/raw_ostream.h>
 #include <mlir/Analysis/SliceAnalysis.h>
 #include <mlir/Dialect/Arith/IR/Arith.h>
@@ -30,6 +34,7 @@
 #include <mlir/Dialect/Utils/StaticValueUtils.h>
 #include <mlir/IR/Attributes.h>
 #include <mlir/IR/Block.h>
+#include <mlir/IR/Builders.h>
 #include <mlir/IR/BuiltinAttributes.h>
 #include <mlir/IR/BuiltinOps.h>
 #include <mlir/IR/IRMapping.h>
@@ -41,6 +46,7 @@
 #include <mlir/Interfaces/SideEffectInterfaces.h>
 #include <mlir/Support/LLVM.h>
 
+#include <algorithm>
 #include <cmath>
 #include <cstddef>
 #include <utility>
@@ -414,8 +420,8 @@ template <> struct llvm::DenseMapInfo<StructuralOperationKey> {
   }
 };
 
-static bool areFloatValuesNear(const APFloat& lhs, const APFloat& rhs,
-                               const unsigned width) {
+static bool approxCompareFloats(const APFloat& lhs, const APFloat& rhs,
+                                const unsigned width) {
   if (lhs.isNaN() || rhs.isNaN()) {
     return lhs.isNaN() && rhs.isNaN();
   }
@@ -443,141 +449,164 @@ static bool areFloatValuesNear(const APFloat& lhs, const APFloat& rhs,
   return absDiff <= absTol + (relTol * scale);
 }
 
-static bool areConstantAttributesEquivalent(const Attribute& lhs,
-                                            const Attribute& rhs) {
-  if (lhs == rhs) {
-    return true;
-  }
-
-  if (auto lhsFloat = dyn_cast<FloatAttr>(lhs)) {
-    auto rhsFloat = dyn_cast<FloatAttr>(rhs);
-    if (!rhsFloat) {
+static bool compareAttributes(const Attribute& attrA, const Attribute& attrB) {
+  if (dyn_cast<UnitAttr>(attrA)) {
+    if (!dyn_cast<UnitAttr>(attrB)) {
       return false;
     }
-    return areFloatValuesNear(lhsFloat.getValue(), rhsFloat.getValue(),
-                              lhsFloat.getType().getIntOrFloatBitWidth());
-  }
-
-  return false;
-}
-
-/// Compare two operations for structural equivalence.
-/// Updates valueMap to track corresponding SSA values.
-static bool areOperationsEquivalent(Operation* lhs, Operation* rhs,
-                                    ValueEquivalenceMap& valueMap) {
-  // Check operation name
-  if (lhs->getName() != rhs->getName()) {
-    return false;
-  }
-
-  // Check arith::ConstantOp
-  if (auto lhsConst = dyn_cast<arith::ConstantOp>(lhs)) {
-    auto rhsConst = dyn_cast<arith::ConstantOp>(rhs);
-    if (!rhsConst) {
+  } else if (auto intAttrA = dyn_cast<IntegerAttr>(attrA)) {
+    auto intAttrB = dyn_cast<IntegerAttr>(attrB);
+    if (!intAttrB || intAttrA.getValue() != intAttrB.getValue()) {
       return false;
     }
+  } else if (auto floatAttrA = dyn_cast<FloatAttr>(attrA)) {
+    auto floatAttrB = dyn_cast<FloatAttr>(attrB);
 
-    if (!areConstantAttributesEquivalent(lhsConst.getValue(),
-                                         rhsConst.getValue())) {
+    if (!floatAttrB ||
+        !approxCompareFloats(floatAttrA.getValue(), floatAttrB.getValue(),
+                             floatAttrA.getType().getIntOrFloatBitWidth())) {
       return false;
     }
-  }
-
-  // Check LLVM::ConstantOp
-  if (auto lhsConst = dyn_cast<LLVM::ConstantOp>(lhs)) {
-    auto rhsConst = dyn_cast<LLVM::ConstantOp>(rhs);
-    if (!rhsConst) {
+  } else if (auto strAttrA = dyn_cast<StringAttr>(attrA)) {
+    auto strAttrB = dyn_cast<StringAttr>(attrB);
+    if (!strAttrB || strAttrA.getValue() != strAttrB.getValue()) {
       return false;
     }
-    if (!areConstantAttributesEquivalent(lhsConst.getValue(),
-                                         rhsConst.getValue())) {
+  } else if (auto arrayAttrA = dyn_cast<ArrayAttr>(attrA)) {
+    auto arrayAttrB = dyn_cast<ArrayAttr>(attrB);
+    if (!arrayAttrB) {
       return false;
     }
-  }
 
-  // Check LLVM::CallOp
-  if (auto lhsCall = dyn_cast<LLVM::CallOp>(lhs)) {
-    auto rhsCall = dyn_cast<LLVM::CallOp>(rhs);
-    if (!rhsCall) {
+    if (arrayAttrA.size() != arrayAttrB.size()) {
       return false;
     }
-    if (lhsCall.getCallee() != rhsCall.getCallee()) {
+
+    // Note: This assumes that the array attributes are equivalently ordered.
+    for (const auto [elementAttrA, elementAttrB] :
+         llvm::zip_equal(arrayAttrA, arrayAttrB)) {
+      if (!compareAttributes(elementAttrA, elementAttrB)) {
+        return false;
+      }
+    }
+  } else if (auto denseArrayAttrA =
+                 llvm::dyn_cast<mlir::DenseArrayAttr>(attrA)) {
+    auto denseArrayAttrB = llvm::dyn_cast<mlir::DenseArrayAttr>(attrB);
+    if (!denseArrayAttrB || denseArrayAttrA.size() != denseArrayAttrB.size() ||
+        denseArrayAttrA.getElementType() != denseArrayAttrB.getElementType()) {
       return false;
     }
+
+    for (const auto [valA, valB] : llvm::zip_equal(
+             denseArrayAttrA.getRawData(), denseArrayAttrB.getRawData())) {
+      if (valA != valB) {
+        return false;
+      }
+    }
+
+  } else {
+    attrA.dump();
+    llvm::reportFatalInternalError("unhandled attribute type!");
+    llvm::llvm_unreachable_internal();
   }
 
-  // Check number of operands and results
-  if (lhs->getNumOperands() != rhs->getNumOperands() ||
-      lhs->getNumResults() != rhs->getNumResults() ||
-      lhs->getNumRegions() != rhs->getNumRegions()) {
+  return true;
+}
+
+static bool isQubitTensor(Value v) {
+  auto tensor = dyn_cast<RankedTensorType>(v.getType());
+  if (!tensor) {
     return false;
   }
 
-  // Note: Attributes are intentionally not checked to allow relaxed comparison
+  return isa<qco::QubitType>(tensor.getElementType());
+}
+
+static bool compareOperations(Operation* opA, Operation* opB, IRMapping& m) {
+
+  // Compare top-level signature-like characteristics.
 
-  // Check result types
-  if (lhs->getResultTypes() != rhs->getResultTypes()) {
+  if (opA->getName() != opB->getName() ||
+      opA->getNumOperands() != opB->getNumOperands() ||
+      opA->getOperandTypes() != opB->getOperandTypes() ||
+      opA->getNumResults() != opB->getNumResults() ||
+      opA->getResultTypes() != opB->getResultTypes() ||
+      opA->getAttrs().size() != opB->getAttrs().size() ||
+      opA->getNumRegions() != opB->getNumRegions() ||
+      opA->getDialect()->getNamespace() != opB->getDialect()->getNamespace()) {
     return false;
   }
 
-  // Check operands according to value mapping
-  for (auto [lhsOperand, rhsOperand] :
-       llvm::zip_equal(lhs->getOperands(), rhs->getOperands())) {
-    if (auto it = valueMap.find(lhsOperand); it != valueMap.end()) {
-      // Value already mapped, must match
-      if (it->second != rhsOperand) {
-        return false;
-      }
-    } else {
-      // Establish new mapping
-      valueMap[lhsOperand] = rhsOperand;
+  // Compare attributes.
+
+  const DenseSet<StringRef> ignore{"function_type"};
+
+  for (const auto& namedAttrA : opA->getAttrs()) {
+    const StringRef keyA = namedAttrA.getName().strref();
+
+    if (ignore.contains(keyA)) {
+      return true;
     }
-  }
 
-  // Update value mapping for results
-  for (auto [lhsResult, rhsResult] :
-       llvm::zip(lhs->getResults(), rhs->getResults())) {
-    valueMap[lhsResult] = rhsResult;
+    if (!opB->hasAttr(keyA)) {
+      return false;
+    }
+
+    if (!compareAttributes(namedAttrA.getValue(), opB->getAttr(keyA))) {
+      return false;
+    }
   }
 
-  return true;
-}
+  // Compare operands.
+  // TODO: Equal type check.
 
-/// Check if an operation has memory effects or control flow side effects
-/// that would prevent reordering.
-static bool hasOrderingConstraints(Operation* op) {
-  // Terminators must maintain their position
-  if (op->hasTrait<OpTrait::IsTerminator>()) {
-    return true;
-  }
+  for (const auto& [operandA, operandB] :
+       llvm::zip_equal(opA->getOperands(), opB->getOperands())) {
 
-  // Symbol-defining operations (like function declarations) can be reordered
-  if (op->hasTrait<OpTrait::SymbolTable>() ||
-      isa<LLVM::LLVMFuncOp, func::FuncOp>(op)) {
-    return false;
-  }
+    if (isQubitTensor(operandA)) {
+      if (!isQubitTensor(operandB)) { // TODO: Assertion?
+        return false;
+      }
 
-  // Check for memory effects that enforce ordering
-  if (auto memInterface = dyn_cast<MemoryEffectOpInterface>(op)) {
-    SmallVector<MemoryEffects::EffectInstance> effects;
-    memInterface.getEffects(effects);
+      auto tensorA = cast<TypedValue<RankedTensorType>>(operandA);
+      qtensor::TensorIterator itA(tensorA);
+      while (std::prev(itA) != itA) {
+        --itA;
+      }
 
-    bool hasNonAllocFreeEffects = false;
-    for (const auto& effect : effects) {
-      // Allow operations with no effects or pure allocation/free effects
-      if (!isa<MemoryEffects::Allocate, MemoryEffects::Free>(
-              effect.getEffect())) {
-        hasNonAllocFreeEffects = true;
-        break;
+      auto tensorB = cast<TypedValue<RankedTensorType>>(operandB);
+      qtensor::TensorIterator itB(tensorB);
+      while (std::prev(itB) != itB) {
+        --itB;
+      }
+
+      if (itA.operation() == nullptr) { // Block-Argument.
+        if (itB.operation() != nullptr) {
+          return false;
+        }
+      } else {
+        auto allocA = cast<qtensor::AllocOp>(itA.operation());
+        auto allocB = cast<qtensor::AllocOp>(itB.operation());
+        if (m.lookup(allocA.getResult()) != allocB.getResult()) {
+          return false;
+        }
       }
     }
+  }
 
-    if (hasNonAllocFreeEffects) {
-      return true;
+  for (const auto& [resA, resB] :
+       llvm::zip_equal(opA->getResults(), opB->getResults())) {
+    if (!isa<qtensor::AllocOp>(opA) && isQubitTensor(resA)) {
+      if (!isQubitTensor(resB)) {
+        return false;
+      }
+      continue;
     }
+
+    m.map(resA, resB);
   }
 
-  return false;
+  return true;
 }
 
 /// Returns a vector of maximum reachable independent DAGs, as defined via their
@@ -610,29 +639,21 @@ static SmallVector<Slice> getDisjointSlices(Block& b) {
   return dags;
 }
 
-static bool areTopLevelEquivalent(Operation* lhs, Operation* rhs) {
-  return lhs->getName() == rhs->getName() &&
-         lhs->getNumOperands() == rhs->getNumOperands() &&
-         lhs->getOperandTypes() == rhs->getOperandTypes() &&
-         lhs->getNumResults() == rhs->getNumResults() &&
-         lhs->getResultTypes() == rhs->getResultTypes() &&
-         lhs->getAttrs().size() == rhs->getAttrs().size() &&
-         lhs->getNumRegions() == rhs->getNumRegions();
-
-  
-}
-
 /// Extract and return "ready" operations from the slice.
-static Slice getReadyOps(Slice& slice, DenseSet<Operation*> finished) {
+static Slice getReadyOps(const Slice& slice, DenseSet<Operation*>& visited) {
   const auto isReady = [&](OpOperand& operand) {
     if (isa<BlockArgument>(operand.get())) {
-      return true; // The defining op is finished?
+      return true;
     }
-    return finished.contains(operand.get().getDefiningOp());
+    return visited.contains(operand.get().getDefiningOp());
   };
 
   Slice ready;
   for (Operation* op : slice) {
+    if (visited.contains(op)) {
+      continue;
+    }
+
     if (llvm::all_of(op->getOpOperands(), isReady)) {
       ready.insert(op);
       continue;
@@ -648,6 +669,7 @@ static Slice getReadyOps(Slice& slice, DenseSet<Operation*> finished) {
       if (isa<qtensor::InsertOp>(prev)) {
         if (ready.contains(prev)) {
           ready.insert(insert.getOperation());
+          continue;
         }
       }
     }
@@ -659,6 +681,7 @@ static Slice getReadyOps(Slice& slice, DenseSet<Operation*> finished) {
       if (isa<qtensor::ExtractOp>(prev)) {
         if (ready.contains(prev)) {
           ready.insert(extract.getOperation());
+          continue;
         }
       }
     }
@@ -667,15 +690,14 @@ static Slice getReadyOps(Slice& slice, DenseSet<Operation*> finished) {
   return ready;
 }
 
-static bool areEquivalent(Region& lhs, Region& rhs, IRMapping& m);
-
-static bool areEquivalent(Slice& lhs, Slice& rhs, IRMapping& m) {
-  DenseSet<Operation*> finished;
-  finished.reserve(lhs.size() + rhs.size());
+static bool compareRegions(Region& regionA, Region& regionB,
+                           DenseSet<Operation*>& visited, IRMapping& m);
 
+static bool compareSlices(const Slice& lhs, const Slice& rhs,
+                          DenseSet<Operation*>& visited, IRMapping& m) {
   while (true) {
-    const auto readyLhs = getReadyOps(lhs, finished);
-    const auto readyRhs = getReadyOps(rhs, finished);
+    const auto readyLhs = getReadyOps(lhs, visited);
+    const auto readyRhs = getReadyOps(rhs, visited);
 
     if (readyLhs.empty() || readyRhs.empty()) {
       break;
@@ -685,35 +707,42 @@ static bool areEquivalent(Slice& lhs, Slice& rhs, IRMapping& m) {
       return false;
     }
 
-    // Greedily search for a structural equivalent operation.
-    for (Operation* opLhs : readyLhs) {
-      for (Operation* opRhs : readyRhs) {
-        if (areTopLevelEquivalent(opLhs, opRhs)) { // TODO: Full equivalence check with attrs etc. 
-          m.map(opLhs, opRhs); // Map operations.
-          // Map operands.
-          // Map results.
+    // Greedily find structural equivalent operation for each op on the lefthand
+    // side.
+    SmallVector<std::pair<Operation*, Operation*>> nested;
+    for (Operation* opA : readyLhs) {
+      bool partnerFound{false};
+      for (Operation* opB : readyRhs) {
+        if (compareOperations(opA, opB, m)) {
+          llvm::dbgs() << opA->getName() << " == " << opB->getName() << '\n';
+          m.map(opA, opB); // Create op mapping.
+
+          if (opA->getNumRegions() != 0) {
+            nested.emplace_back(opA, opB);
+          }
 
-          llvm::dbgs() << opLhs->getName() << " == " << opRhs->getName()
-                       << '\n';
+          partnerFound = true;
+          break;
         }
       }
-    }
 
-    // for (Operation* op : readyLhs) {
-    //   op->dumpPretty();
-    //   for (Region& region : op->getRegions()) {
-    //     IRMapping m;
-    //     if (!areEquivalent(region, region, m)) {
-    //       return false;
-    //     }
-    //   }
-    // }
+      if (!partnerFound) {
+        llvm::dbgs() << "no matching op found: " << opA->getName() << '\n';
+        return false;
+      }
+    }
 
-    finished.insert_range(readyLhs);
-    lhs.set_subtract(readyLhs);
+    visited.insert_range(readyLhs);
+    visited.insert_range(readyRhs);
 
-    finished.insert_range(readyRhs);
-    rhs.set_subtract(readyRhs);
+    for (auto& [opA, opB] : nested) {
+      for (const auto [regionA, regionB] :
+           llvm::zip_equal(opA->getRegions(), opB->getRegions())) {
+        if (!compareRegions(regionA, regionB, visited, m)) {
+          return false;
+        }
+      }
+    }
   }
 
   return lhs.empty() && rhs.empty();
@@ -721,13 +750,14 @@ static bool areEquivalent(Slice& lhs, Slice& rhs, IRMapping& m) {
 
 /// Compare two blocks for structural equivalence, allowing permutations
 /// of independent operations.
-static bool areEquivalent(Block& lhs, Block& rhs, IRMapping& m) {
-  if (lhs.getNumArguments() != rhs.getNumArguments()) {
+static bool compareBlocks(Block& blockA, Block& blockB,
+                          DenseSet<Operation*>& visited, IRMapping& m) {
+  if (blockA.getNumArguments() != blockB.getNumArguments()) {
     return false;
   }
 
   for (auto [lArg, rArg] :
-       llvm::zip_equal(lhs.getArguments(), rhs.getArguments())) {
+       llvm::zip_equal(blockA.getArguments(), blockB.getArguments())) {
     if (lArg.getType() != rArg.getType()) {
       return false;
     }
@@ -735,15 +765,15 @@ static bool areEquivalent(Block& lhs, Block& rhs, IRMapping& m) {
     m.map(lArg, rArg);
   }
 
-  auto lDAGs = getDisjointSlices(lhs);
-  auto rDAGs = getDisjointSlices(rhs);
+  auto lDAGs = getDisjointSlices(blockA);
+  auto rDAGs = getDisjointSlices(blockB);
 
   if (lDAGs.size() != rDAGs.size()) {
     return false;
   }
 
   for (const auto& [lDAG, rDAG] : llvm::zip_equal(lDAGs, rDAGs)) {
-    if (lDAG.size() != rDAG.size() || !areEquivalent(lDAG, rDAG, m)) {
+    if (lDAG.size() != rDAG.size() || !compareSlices(lDAG, rDAG, visited, m)) {
       return false;
     }
   }
@@ -752,13 +782,14 @@ static bool areEquivalent(Block& lhs, Block& rhs, IRMapping& m) {
 }
 
 /// Compare two regions for structural equivalence.
-static bool areEquivalent(Region& lhs, Region& rhs, IRMapping& m) {
-  if (lhs.getBlocks().size() != rhs.getBlocks().size()) {
+static bool compareRegions(Region& regionA, Region& regionB,
+                           DenseSet<Operation*>& visited, IRMapping& m) {
+  if (regionA.getBlocks().size() != regionB.getBlocks().size()) {
     return false;
   }
 
-  for (auto [lhsBlock, rhsBlock] : llvm::zip_equal(lhs, rhs)) {
-    if (!areEquivalent(lhsBlock, rhsBlock, m)) {
+  for (const auto [blockA, blockB] : llvm::zip_equal(regionA, regionB)) {
+    if (!compareBlocks(blockA, blockB, visited, m)) {
       return false;
     }
   }
@@ -768,5 +799,7 @@ static bool areEquivalent(Region& lhs, Region& rhs, IRMapping& m) {
 
 bool areModulesEquivalentWithPermutations(ModuleOp lhs, ModuleOp rhs) {
   IRMapping m;
-  return areEquivalent(lhs.getBodyRegion(), rhs.getBodyRegion(), m);
+  DenseSet<Operation*> visited;
+
+  return compareRegions(lhs.getBodyRegion(), rhs.getBodyRegion(), visited, m);
 }
diff --git a/mlir/unittests/programs/qco_programs.cpp b/mlir/unittests/programs/qco_programs.cpp
index f48444d1ff..6b799b6d6f 100644
--- a/mlir/unittests/programs/qco_programs.cpp
+++ b/mlir/unittests/programs/qco_programs.cpp
@@ -276,8 +276,8 @@ void repeatedControlledX(QCOProgramBuilder& b) {
   Value q1;
   auto tensor = b.qtensorAlloc(2);
   std::tie(tensor, q0) = b.qtensorExtract(tensor, 0);
-  q0 = b.h(q0);
   std::tie(tensor, q1) = b.qtensorExtract(tensor, 1);
+  q0 = b.h(q0);
   for (auto i = 0; i < 2; i++) {
     std::tie(q0, q1) = b.cx(q0, q1);
   }

From cf2796f692e65eaa57c4d64091619efba9e72692 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Tue, 9 Jun 2026 16:21:48 +0200
Subject: [PATCH 03/32] Remove unused functions

---
 mlir/lib/Support/IRVerification.cpp | 487 +++-------------------------
 1 file changed, 42 insertions(+), 445 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index e504d5b0bb..aa84dd9333 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -11,7 +11,6 @@
 #include "mlir/Support/IRVerification.h"
 
 #include "mlir/Dialect/QCO/IR/QCODialect.h"
-#include "mlir/Dialect/QTensor/IR/QTensorUtils.h"
 #include "mlir/Dialect/QTensor/Utils/TensorIterator.h"
 
 #include <llvm/ADT/ArrayRef.h>
@@ -22,6 +21,7 @@
 #include <llvm/ADT/STLExtras.h>
 #include <llvm/ADT/SmallVector.h>
 #include <llvm/ADT/StringRef.h>
+#include <llvm/ADT/iterator_range.h>
 #include <llvm/Support/Casting.h>
 #include <llvm/Support/Debug.h>
 #include <llvm/Support/ErrorHandling.h>
@@ -46,380 +46,12 @@
 #include <mlir/Interfaces/SideEffectInterfaces.h>
 #include <mlir/Support/LLVM.h>
 
-#include <algorithm>
 #include <cmath>
 #include <cstddef>
 #include <utility>
 
 using namespace mlir;
 
-namespace {
-
-using Slice = SetVector<Operation*>;
-
-/// Compute a structural hash for an operation (excluding SSA value identities).
-/// This hash is based on operation name, types, and attributes only.
-struct OperationStructuralHash {
-  size_t operator()(Operation* op) const {
-    size_t hash = llvm::hash_value(op->getName().getStringRef());
-
-    // Hash result types
-    for (auto type : op->getResultTypes()) {
-      hash = llvm::hash_combine(hash, type.getAsOpaquePointer());
-    }
-
-    // Hash operand types (not values)
-    for (auto operand : op->getOperands()) {
-      hash = llvm::hash_combine(hash, operand.getType().getAsOpaquePointer());
-    }
-
-    // Hash attributes
-    // for (const auto& attr : op->getAttrDictionary()) {
-    //   hash = llvm::hash_combine(hash, attr.getName().str());
-    //   hash = llvm::hash_combine(hash, attr.getValue().getAsOpaquePointer());
-    // }
-
-    return hash;
-  }
-};
-
-/// Check if two operations are structurally equivalent (excluding SSA value
-/// identities).
-struct OperationStructuralEquality {
-  bool operator()(Operation* lhs, Operation* rhs) const {
-    // Check operation name
-    if (lhs->getName() != rhs->getName()) {
-      return false;
-    }
-
-    // Check result types
-    if (lhs->getResultTypes() != rhs->getResultTypes()) {
-      return false;
-    }
-
-    // Check operand types (not values)
-    auto lhsOperandTypes = lhs->getOperandTypes();
-    auto rhsOperandTypes = rhs->getOperandTypes();
-    return llvm::equal(lhsOperandTypes, rhsOperandTypes);
-
-    // Note: Attributes are intentionally not checked here to allow relaxed
-    // comparison. Attributes like function names, parameter names, etc. may
-    // differ while operations are still structurally equivalent.
-  }
-};
-
-/// Wrapper for Operation* with structural comparison semantics
-struct StructuralOperationKey {
-  Operation* op;
-
-  explicit StructuralOperationKey(Operation* operation = nullptr)
-      : op(operation) {}
-
-  bool operator==(const StructuralOperationKey& other) const {
-    if (op == other.op) {
-      return true;
-    }
-    if (op == nullptr || other.op == nullptr) {
-      return false;
-    }
-    return OperationStructuralEquality{}(op, other.op);
-  }
-
-  bool operator!=(const StructuralOperationKey& other) const {
-    return !(*this == other);
-  }
-};
-
-/// Map to track value equivalence between two modules.
-using ValueEquivalenceMap = DenseMap<mlir::Value, mlir::Value>;
-
-using OperationSet = DenseSet<Operation*>;
-
-struct InsertWrite {
-  Value scalar;
-  Value index;
-};
-
-struct InsertChainSummary {
-  Value baseTensor;
-  Value finalTensor;
-  SmallVector<InsertWrite> writes;
-};
-
-} // namespace
-
-static bool areValuesEquivalent(Value lhs, Value rhs,
-                                ValueEquivalenceMap& valueMap) {
-  if (auto it = valueMap.find(lhs); it != valueMap.end()) {
-    return it->second == rhs;
-  }
-  valueMap[lhs] = rhs;
-  return true;
-}
-
-static bool areIndexValuesEquivalent(Value lhs, Value rhs,
-                                     ValueEquivalenceMap& valueMap) {
-  if (qtensor::areEquivalentIndices(lhs, rhs)) {
-    return true;
-  }
-  return areValuesEquivalent(lhs, rhs, valueMap);
-}
-
-static bool isQTensorInsertOp(Operation* op) {
-  return isa<qtensor::InsertOp>(op);
-}
-
-static bool isCommutableQTensorInsertDependency(Operation* dependent,
-                                                Operation* dependency) {
-  auto dependentInsert = dyn_cast<qtensor::InsertOp>(dependent);
-  auto dependencyInsert = dyn_cast<qtensor::InsertOp>(dependency);
-  if (!dependentInsert || !dependencyInsert) {
-    return false;
-  }
-  if (dependentInsert.getDest() != dependencyInsert.getResult()) {
-    return false;
-  }
-  auto dependentIndex = dependentInsert.getIndex();
-  auto dependencyIndex = dependencyInsert.getIndex();
-  if (!getConstantIntValue(dependentIndex) ||
-      !getConstantIntValue(dependencyIndex)) {
-    return false;
-  }
-  return !qtensor::areEquivalentIndices(dependentIndex, dependencyIndex);
-}
-
-static Value getInsertChainBaseTensor(Value tensor, const OperationSet& group) {
-  auto current = tensor;
-  while (auto insertOp = current.getDefiningOp<qtensor::InsertOp>()) {
-    if (!group.contains(insertOp.getOperation())) {
-      break;
-    }
-    current = insertOp.getDest();
-  }
-  return current;
-}
-
-static bool summarizeInsertGroup(ArrayRef<Operation*> ops,
-                                 SmallVectorImpl<InsertChainSummary>& chains) {
-  OperationSet groupOps;
-  for (Operation* op : ops) {
-    groupOps.insert(op);
-  }
-
-  DenseSet<Value> consumedInsertResults;
-  for (Operation* op : ops) {
-    auto insertOp = cast<qtensor::InsertOp>(op);
-    if (auto definingInsert =
-            insertOp.getDest().getDefiningOp<qtensor::InsertOp>()) {
-      if (groupOps.contains(definingInsert.getOperation())) {
-        consumedInsertResults.insert(insertOp.getDest());
-      }
-    }
-  }
-
-  DenseMap<Value, size_t> chainByBaseTensor;
-  for (Operation* op : ops) {
-    auto insertOp = cast<qtensor::InsertOp>(op);
-    const Value baseTensor =
-        getInsertChainBaseTensor(insertOp.getDest(), groupOps);
-
-    size_t chainIdx = 0;
-    if (auto it = chainByBaseTensor.find(baseTensor);
-        it != chainByBaseTensor.end()) {
-      chainIdx = it->second;
-    } else {
-      chainIdx = chains.size();
-      chainByBaseTensor[baseTensor] = chainIdx;
-      InsertChainSummary summary;
-      summary.baseTensor = baseTensor;
-      chains.emplace_back(std::move(summary));
-    }
-
-    auto& chain = chains[chainIdx];
-    chain.writes.push_back(InsertWrite{.scalar = insertOp.getScalar(),
-                                       .index = insertOp.getIndex()});
-
-    if (!consumedInsertResults.contains(insertOp.getResult())) {
-      if (chain.finalTensor) {
-        return false;
-      }
-      chain.finalTensor = insertOp.getResult();
-    }
-  }
-
-  for (const auto& chain : chains) {
-    if (!chain.finalTensor) {
-      return false;
-    }
-
-    // Reordering writes to the same index is not semantics-preserving.
-    SmallVector<Value> seenIndices;
-    for (const auto& write : chain.writes) {
-      if (llvm::any_of(seenIndices, [&](Value seenIndex) {
-            return qtensor::areEquivalentIndices(seenIndex, write.index);
-          })) {
-        return false;
-      }
-      seenIndices.push_back(write.index);
-    }
-  }
-
-  return true;
-}
-
-static bool areInsertWritesEquivalentRec(const size_t lhsIdx,
-                                         ArrayRef<InsertWrite> lhsWrites,
-                                         ArrayRef<InsertWrite> rhsWrites,
-                                         SmallVectorImpl<char>& rhsUsed,
-                                         ValueEquivalenceMap& valueMap) {
-  if (lhsIdx == lhsWrites.size()) {
-    return true;
-  }
-
-  for (size_t rhsIdx = 0; rhsIdx < rhsWrites.size(); ++rhsIdx) {
-    if (rhsUsed[rhsIdx] != 0) {
-      continue;
-    }
-
-    ValueEquivalenceMap tempMap = valueMap;
-    if (!areValuesEquivalent(lhsWrites[lhsIdx].scalar, rhsWrites[rhsIdx].scalar,
-                             tempMap) ||
-        !areIndexValuesEquivalent(lhsWrites[lhsIdx].index,
-                                  rhsWrites[rhsIdx].index, tempMap)) {
-      continue;
-    }
-
-    rhsUsed[rhsIdx] = 1;
-    if (areInsertWritesEquivalentRec(lhsIdx + 1, lhsWrites, rhsWrites, rhsUsed,
-                                     tempMap)) {
-      valueMap = std::move(tempMap);
-      return true;
-    }
-    rhsUsed[rhsIdx] = 0;
-  }
-
-  return false;
-}
-
-static bool areInsertWritesEquivalent(ArrayRef<InsertWrite> lhsWrites,
-                                      ArrayRef<InsertWrite> rhsWrites,
-                                      ValueEquivalenceMap& valueMap) {
-  if (lhsWrites.size() != rhsWrites.size()) {
-    return false;
-  }
-  SmallVector<char> rhsUsed(rhsWrites.size(), 0);
-  return areInsertWritesEquivalentRec(0, lhsWrites, rhsWrites, rhsUsed,
-                                      valueMap);
-}
-
-static bool areInsertChainsEquivalent(const InsertChainSummary& lhsChain,
-                                      const InsertChainSummary& rhsChain,
-                                      ValueEquivalenceMap& valueMap) {
-  ValueEquivalenceMap tempMap = valueMap;
-  if (!areValuesEquivalent(lhsChain.baseTensor, rhsChain.baseTensor, tempMap)) {
-    return false;
-  }
-
-  if (!areInsertWritesEquivalent(lhsChain.writes, rhsChain.writes, tempMap)) {
-    return false;
-  }
-
-  if (!areValuesEquivalent(lhsChain.finalTensor, rhsChain.finalTensor,
-                           tempMap)) {
-    return false;
-  }
-
-  valueMap = std::move(tempMap);
-  return true;
-}
-
-static bool areInsertGroupsEquivalentRec(const size_t lhsChainIdx,
-                                         ArrayRef<InsertChainSummary> lhsChains,
-                                         ArrayRef<InsertChainSummary> rhsChains,
-                                         SmallVectorImpl<char>& rhsChainUsed,
-                                         ValueEquivalenceMap& valueMap) {
-  if (lhsChainIdx == lhsChains.size()) {
-    return true;
-  }
-
-  for (size_t rhsChainIdx = 0; rhsChainIdx < rhsChains.size(); ++rhsChainIdx) {
-    if (rhsChainUsed[rhsChainIdx] != 0) {
-      continue;
-    }
-
-    ValueEquivalenceMap tempMap = valueMap;
-    if (!areInsertChainsEquivalent(lhsChains[lhsChainIdx],
-                                   rhsChains[rhsChainIdx], tempMap)) {
-      continue;
-    }
-
-    rhsChainUsed[rhsChainIdx] = 1;
-    if (areInsertGroupsEquivalentRec(lhsChainIdx + 1, lhsChains, rhsChains,
-                                     rhsChainUsed, tempMap)) {
-      valueMap = std::move(tempMap);
-      return true;
-    }
-    rhsChainUsed[rhsChainIdx] = 0;
-  }
-
-  return false;
-}
-
-static bool areInsertGroupsEquivalent(ArrayRef<Operation*> lhsOps,
-                                      ArrayRef<Operation*> rhsOps,
-                                      ValueEquivalenceMap& valueMap) {
-  if (lhsOps.size() != rhsOps.size()) {
-    return false;
-  }
-
-  SmallVector<InsertChainSummary> lhsChains;
-  SmallVector<InsertChainSummary> rhsChains;
-  if (!summarizeInsertGroup(lhsOps, lhsChains) ||
-      !summarizeInsertGroup(rhsOps, rhsChains)) {
-    return false;
-  }
-  if (lhsChains.size() != rhsChains.size()) {
-    return false;
-  }
-
-  SmallVector<char> rhsChainUsed(rhsChains.size(), 0);
-  return areInsertGroupsEquivalentRec(0, lhsChains, rhsChains, rhsChainUsed,
-                                      valueMap);
-}
-
-/// DenseMapInfo specialization for StructuralOperationKey
-template <> struct llvm::DenseMapInfo<StructuralOperationKey> {
-  static StructuralOperationKey getEmptyKey() {
-    return StructuralOperationKey(DenseMapInfo<Operation*>::getEmptyKey());
-  }
-
-  static StructuralOperationKey getTombstoneKey() {
-    return StructuralOperationKey(DenseMapInfo<Operation*>::getTombstoneKey());
-  }
-
-  static unsigned getHashValue(const StructuralOperationKey& key) {
-    if (key.op == getEmptyKey().op || key.op == getTombstoneKey().op) {
-      return DenseMapInfo<Operation*>::getHashValue(key.op);
-    }
-    return OperationStructuralHash{}(key.op);
-  }
-
-  static bool isEqual(const StructuralOperationKey& lhs,
-                      const StructuralOperationKey& rhs) {
-    // Handle special keys
-    if (lhs.op == getEmptyKey().op) {
-      return rhs.op == getEmptyKey().op;
-    }
-    if (lhs.op == getTombstoneKey().op) {
-      return rhs.op == getTombstoneKey().op;
-    }
-    if (rhs.op == getEmptyKey().op || rhs.op == getTombstoneKey().op) {
-      return false;
-    }
-    return lhs == rhs;
-  }
-};
-
 static bool approxCompareFloats(const APFloat& lhs, const APFloat& rhs,
                                 const unsigned width) {
   if (lhs.isNaN() || rhs.isNaN()) {
@@ -513,7 +145,7 @@ static bool compareAttributes(const Attribute& attrA, const Attribute& attrB) {
   return true;
 }
 
-static bool isQubitTensor(Value v) {
+static bool hasTypeQubitTensor(Value v) {
   auto tensor = dyn_cast<RankedTensorType>(v.getType());
   if (!tensor) {
     return false;
@@ -563,8 +195,8 @@ static bool compareOperations(Operation* opA, Operation* opB, IRMapping& m) {
   for (const auto& [operandA, operandB] :
        llvm::zip_equal(opA->getOperands(), opB->getOperands())) {
 
-    if (isQubitTensor(operandA)) {
-      if (!isQubitTensor(operandB)) { // TODO: Assertion?
+    if (hasTypeQubitTensor(operandA)) {
+      if (!hasTypeQubitTensor(operandB)) { // TODO: Assertion?
         return false;
       }
 
@@ -596,8 +228,8 @@ static bool compareOperations(Operation* opA, Operation* opB, IRMapping& m) {
 
   for (const auto& [resA, resB] :
        llvm::zip_equal(opA->getResults(), opB->getResults())) {
-    if (!isa<qtensor::AllocOp>(opA) && isQubitTensor(resA)) {
-      if (!isQubitTensor(resB)) {
+    if (!isa<qtensor::AllocOp>(opA) && hasTypeQubitTensor(resA)) {
+      if (!hasTypeQubitTensor(resB)) {
         return false;
       }
       continue;
@@ -609,38 +241,9 @@ static bool compareOperations(Operation* opA, Operation* opB, IRMapping& m) {
   return true;
 }
 
-/// Returns a vector of maximum reachable independent DAGs, as defined via their
-/// def-use chain, where the operations of the setvector are topologically
-/// sorted. The vector is sorted by the size of the DAG (i.e., the number of
-/// operations).
-static SmallVector<Slice> getDisjointSlices(Block& b) {
-  const auto filter = [&b](Operation* op) { return op->getBlock() == &b; };
-
-  const BackwardSliceOptions backwardSliceOptions(filter);
-  const SliceOptions forwardSliceOptions(filter);
-
-  DenseSet<Operation*> visited;
-  visited.reserve(range_size(b.getOperations()));
-
-  SmallVector<SetVector<Operation*>> dags;
-  for (Operation& op : b.getOperations()) {
-    if (visited.contains(&op)) {
-      continue;
-    }
-    const auto slice = getSlice(&op, backwardSliceOptions, forwardSliceOptions);
-    const auto& dag = dags.emplace_back(slice);
-    visited.insert_range(dag);
-  }
-
-  sort(dags, [](const auto& lhs, const auto& rhs) {
-    return lhs.size() < rhs.size();
-  });
-
-  return dags;
-}
-
-/// Extract and return "ready" operations from the slice.
-static Slice getReadyOps(const Slice& slice, DenseSet<Operation*>& visited) {
+/// Extract and return "ready" operations.
+static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> ops,
+                                         DenseSet<Operation*>& visited) {
   const auto isReady = [&](OpOperand& operand) {
     if (isa<BlockArgument>(operand.get())) {
       return true;
@@ -648,8 +251,8 @@ static Slice getReadyOps(const Slice& slice, DenseSet<Operation*>& visited) {
     return visited.contains(operand.get().getDefiningOp());
   };
 
-  Slice ready;
-  for (Operation* op : slice) {
+  SetVector<Operation*> ready;
+  for (Operation* op : ops) {
     if (visited.contains(op)) {
       continue;
     }
@@ -693,11 +296,39 @@ static Slice getReadyOps(const Slice& slice, DenseSet<Operation*>& visited) {
 static bool compareRegions(Region& regionA, Region& regionB,
                            DenseSet<Operation*>& visited, IRMapping& m);
 
-static bool compareSlices(const Slice& lhs, const Slice& rhs,
+/// Compare two blocks for structural equivalence, allowing permutations
+/// of independent operations.
+static bool compareBlocks(Block& blockA, Block& blockB,
                           DenseSet<Operation*>& visited, IRMapping& m) {
+  if (blockA.getNumArguments() != blockB.getNumArguments()) {
+    return false;
+  }
+
+  for (auto [lArg, rArg] :
+       llvm::zip_equal(blockA.getArguments(), blockB.getArguments())) {
+    if (lArg.getType() != rArg.getType()) {
+      return false;
+    }
+
+    m.map(lArg, rArg);
+  }
+
+  SmallVector<Operation*> opsA;
+  opsA.reserve(llvm::range_size(blockA.getOperations()));
+  SmallVector<Operation*> opsB;
+  opsB.reserve(llvm::range_size(blockB.getOperations()));
+
+  for (Operation& op : blockA.getOperations()) {
+    opsA.emplace_back(&op);
+  }
+
+  for (Operation& op : blockB.getOperations()) {
+    opsB.emplace_back(&op);
+  }
+
   while (true) {
-    const auto readyLhs = getReadyOps(lhs, visited);
-    const auto readyRhs = getReadyOps(rhs, visited);
+    const auto readyLhs = getReadyOps(opsA, visited);
+    const auto readyRhs = getReadyOps(opsB, visited);
 
     if (readyLhs.empty() || readyRhs.empty()) {
       break;
@@ -745,39 +376,6 @@ static bool compareSlices(const Slice& lhs, const Slice& rhs,
     }
   }
 
-  return lhs.empty() && rhs.empty();
-}
-
-/// Compare two blocks for structural equivalence, allowing permutations
-/// of independent operations.
-static bool compareBlocks(Block& blockA, Block& blockB,
-                          DenseSet<Operation*>& visited, IRMapping& m) {
-  if (blockA.getNumArguments() != blockB.getNumArguments()) {
-    return false;
-  }
-
-  for (auto [lArg, rArg] :
-       llvm::zip_equal(blockA.getArguments(), blockB.getArguments())) {
-    if (lArg.getType() != rArg.getType()) {
-      return false;
-    }
-
-    m.map(lArg, rArg);
-  }
-
-  auto lDAGs = getDisjointSlices(blockA);
-  auto rDAGs = getDisjointSlices(blockB);
-
-  if (lDAGs.size() != rDAGs.size()) {
-    return false;
-  }
-
-  for (const auto& [lDAG, rDAG] : llvm::zip_equal(lDAGs, rDAGs)) {
-    if (lDAG.size() != rDAG.size() || !compareSlices(lDAG, rDAG, visited, m)) {
-      return false;
-    }
-  }
-
   return true;
 }
 
@@ -800,6 +398,5 @@ static bool compareRegions(Region& regionA, Region& regionB,
 bool areModulesEquivalentWithPermutations(ModuleOp lhs, ModuleOp rhs) {
   IRMapping m;
   DenseSet<Operation*> visited;
-
   return compareRegions(lhs.getBodyRegion(), rhs.getBodyRegion(), visited, m);
 }

From ce4af6322fc07b0a139d10483daa01793ef2b6a9 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Wed, 10 Jun 2026 16:05:19 +0200
Subject: [PATCH 04/32] wip: add recursive ir mappings

---
 mlir/lib/Support/IRVerification.cpp | 210 +++++++++++++++++-----------
 1 file changed, 131 insertions(+), 79 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index aa84dd9333..1233fcd523 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -52,6 +52,29 @@
 
 using namespace mlir;
 
+static bool compareRegions(Region& regionA, Region& regionB,
+                           DenseSet<Operation*>& visited, IRMapping& m);
+
+static bool hasTypeQubitTensor(Value v) {
+  auto tensor = dyn_cast<RankedTensorType>(v.getType());
+  if (!tensor) {
+    return false;
+  }
+
+  return isa<qco::QubitType>(tensor.getElementType());
+}
+
+static void remapResults(Operation* fromOp, Operation* toOp, IRMapping& m) {
+  for (const auto& [fromResult, toResult] :
+       llvm::zip_equal(fromOp->getResults(), toOp->getResults())) {
+    if (!isa<qtensor::AllocOp>(fromOp) && hasTypeQubitTensor(fromResult)) {
+      assert(hasTypeQubitTensor(toResult));
+      continue;
+    }
+    m.map(fromResult, toResult);
+  }
+}
+
 static bool approxCompareFloats(const APFloat& lhs, const APFloat& rhs,
                                 const unsigned width) {
   if (lhs.isNaN() || rhs.isNaN()) {
@@ -136,25 +159,29 @@ static bool compareAttributes(const Attribute& attrA, const Attribute& attrB) {
       }
     }
 
+  } else if (auto symbolRefAttrA =
+                 llvm::dyn_cast<mlir::FlatSymbolRefAttr>(attrA)) {
+    auto symbolRefAttrB = llvm::dyn_cast<mlir::FlatSymbolRefAttr>(attrB);
+    if (!symbolRefAttrB) {
+      return false;
+    }
+
+    if (symbolRefAttrA.getValue() != symbolRefAttrB.getValue()) {
+      return false;
+    }
   } else {
-    attrA.dump();
-    llvm::reportFatalInternalError("unhandled attribute type!");
-    llvm::llvm_unreachable_internal();
+    // attrA.dump();
+    // llvm::dbgs() << "unhandled attribute type!\n";
+    // attrA.dump();
+    // llvm::reportFatalInternalError("unhandled attribute type!");
+    // llvm::llvm_unreachable_internal();
   }
 
   return true;
 }
 
-static bool hasTypeQubitTensor(Value v) {
-  auto tensor = dyn_cast<RankedTensorType>(v.getType());
-  if (!tensor) {
-    return false;
-  }
-
-  return isa<qco::QubitType>(tensor.getElementType());
-}
-
-static bool compareOperations(Operation* opA, Operation* opB, IRMapping& m) {
+static bool compareOperations(Operation* opA, Operation* opB,
+                              DenseSet<Operation*>& visited, IRMapping& m) {
 
   // Compare top-level signature-like characteristics.
 
@@ -163,28 +190,31 @@ static bool compareOperations(Operation* opA, Operation* opB, IRMapping& m) {
       opA->getOperandTypes() != opB->getOperandTypes() ||
       opA->getNumResults() != opB->getNumResults() ||
       opA->getResultTypes() != opB->getResultTypes() ||
-      opA->getAttrs().size() != opB->getAttrs().size() ||
-      opA->getNumRegions() != opB->getNumRegions() ||
-      opA->getDialect()->getNamespace() != opB->getDialect()->getNamespace()) {
+      // opA->getAttrs().size() != opB->getAttrs().size() ||
+      opA->getNumRegions() != opB->getNumRegions()) {
+    llvm::dbgs() << "\t\tUNEQUAL 2!\n";
     return false;
   }
 
   // Compare attributes.
 
-  const DenseSet<StringRef> ignore{"function_type"};
+  const DenseSet<StringRef> ignore{"passthrough"};
 
   for (const auto& namedAttrA : opA->getAttrs()) {
     const StringRef keyA = namedAttrA.getName().strref();
 
     if (ignore.contains(keyA)) {
-      return true;
+      llvm::dbgs() << "ignoring: " << keyA << '\n';
+      continue;
     }
 
     if (!opB->hasAttr(keyA)) {
-      return false;
+      llvm::dbgs() << "missing attribute: " << keyA << '\n';
+      continue;
     }
 
     if (!compareAttributes(namedAttrA.getValue(), opB->getAttr(keyA))) {
+      llvm::dbgs() << "\t\tUNEQUAL 3!\n";
       return false;
     }
   }
@@ -223,21 +253,29 @@ static bool compareOperations(Operation* opA, Operation* opB, IRMapping& m) {
           return false;
         }
       }
-    }
-  }
-
-  for (const auto& [resA, resB] :
-       llvm::zip_equal(opA->getResults(), opB->getResults())) {
-    if (!isa<qtensor::AllocOp>(opA) && hasTypeQubitTensor(resA)) {
-      if (!hasTypeQubitTensor(resB)) {
+    } else {
+      auto mappedOperand = m.lookupOrNull(operandA);
+      if (!mappedOperand || mappedOperand != operandB) {
+        llvm::dbgs() << "\t\tUNEQUAL 6!\n";
+        llvm::dbgs() << "\t\t" << mappedOperand << '\n';
+        llvm::dbgs() << "\t\t" << operandB << '\n';
         return false;
       }
-      continue;
     }
+  }
 
-    m.map(resA, resB);
+  for (const auto [regionA, regionB] :
+       llvm::zip_equal(opA->getRegions(), opB->getRegions())) {
+    if (!compareRegions(regionA, regionB, visited, m)) {
+      llvm::dbgs() << "\t\tUNEQUAL 7!\n";
+      return false;
+    }
   }
 
+  // If the function reached this point, the two operations are equal.
+
+  llvm::dbgs() << "\t\tEQUAL!\n";
+
   return true;
 }
 
@@ -293,11 +331,58 @@ static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> ops,
   return ready;
 }
 
-static bool compareRegions(Region& regionA, Region& regionB,
-                           DenseSet<Operation*>& visited, IRMapping& m);
+static bool compareReady(SetVector<Operation*>::const_iterator it,
+                         const SetVector<Operation*>& readyA,
+                         const SetVector<Operation*>& readyB,
+                         DenseSet<Operation*>& visited, IRMapping& m) {
+  if (it == readyA.end()) {
+    return true;
+  }
+
+  Operation* opA = *it;
+
+  // Because there may be multiple structural equivalent operations,
+  // collect them in a vector for further recursive processing. If there are
+  // no partners, no matching operation has been found and the blocks are
+  // not equivalent.
+
+  llvm::dbgs() << "--- compare ---\n";
+  opA->dumpPretty();
+  SmallVector<Operation*> partners(
+      make_filter_range(readyB, [&](Operation* op) {
+        llvm::dbgs() << "\t";
+        op->dumpPretty();
+        return compareOperations(opA, op, visited, m);
+      }));
+
+  if (partners.empty()) {
+    llvm::dbgs() << "no matching op found: " << *opA << '\n';
+    return false;
+  }
+
+  // If there were only one partner, we could simply update the mapping m
+  // here. Unfortunately, multiple operations can be structurally equivalent
+  // (think arith.constant, for example). Thus, we must test each possible
+  // alternative mapping to identify (if possible) the equivalent partner.
+
+  bool found{false};
+  for (Operation* partner : partners) {
+    llvm::dbgs() << "trying partner: " << *partner << '\n';
+    IRMapping partnerM(m);
+    remapResults(opA, partner, partnerM);
+
+    DenseSet<Operation*> altVisited(visited);
+    if (compareReady(std::next(it), readyA, readyB, altVisited, partnerM)) {
+      visited = std::move(altVisited);
+      m = std::move(partnerM);
+      found = true;
+      break;
+    }
+  }
+
+  return found;
+}
 
-/// Compare two blocks for structural equivalence, allowing permutations
-/// of independent operations.
 static bool compareBlocks(Block& blockA, Block& blockB,
                           DenseSet<Operation*>& visited, IRMapping& m) {
   if (blockA.getNumArguments() != blockB.getNumArguments()) {
@@ -314,65 +399,32 @@ static bool compareBlocks(Block& blockA, Block& blockB,
   }
 
   SmallVector<Operation*> opsA;
-  opsA.reserve(llvm::range_size(blockA.getOperations()));
   SmallVector<Operation*> opsB;
-  opsB.reserve(llvm::range_size(blockB.getOperations()));
 
-  for (Operation& op : blockA.getOperations()) {
-    opsA.emplace_back(&op);
-  }
+  opsA.reserve(llvm::range_size(blockA.getOperations()));
+  opsB.reserve(llvm::range_size(blockB.getOperations()));
 
-  for (Operation& op : blockB.getOperations()) {
-    opsB.emplace_back(&op);
-  }
+  for_each(blockA.getOperations(), [&](auto& op) { opsA.emplace_back(&op); });
+  for_each(blockB.getOperations(), [&](auto& op) { opsB.emplace_back(&op); });
 
   while (true) {
-    const auto readyLhs = getReadyOps(opsA, visited);
-    const auto readyRhs = getReadyOps(opsB, visited);
+    const auto readyA = getReadyOps(opsA, visited);
+    const auto readyB = getReadyOps(opsB, visited);
+
+    visited.insert_range(readyA);
+    visited.insert_range(readyB);
 
-    if (readyLhs.empty() || readyRhs.empty()) {
+    if (readyA.empty() && readyB.empty()) {
       break;
     }
 
-    if (readyLhs.size() != readyRhs.size()) {
+    if ((readyA.empty() && !readyB.empty()) ||
+        (!readyA.empty() && readyB.empty()) || readyA.size() != readyB.size()) {
       return false;
     }
 
-    // Greedily find structural equivalent operation for each op on the lefthand
-    // side.
-    SmallVector<std::pair<Operation*, Operation*>> nested;
-    for (Operation* opA : readyLhs) {
-      bool partnerFound{false};
-      for (Operation* opB : readyRhs) {
-        if (compareOperations(opA, opB, m)) {
-          llvm::dbgs() << opA->getName() << " == " << opB->getName() << '\n';
-          m.map(opA, opB); // Create op mapping.
-
-          if (opA->getNumRegions() != 0) {
-            nested.emplace_back(opA, opB);
-          }
-
-          partnerFound = true;
-          break;
-        }
-      }
-
-      if (!partnerFound) {
-        llvm::dbgs() << "no matching op found: " << opA->getName() << '\n';
-        return false;
-      }
-    }
-
-    visited.insert_range(readyLhs);
-    visited.insert_range(readyRhs);
-
-    for (auto& [opA, opB] : nested) {
-      for (const auto [regionA, regionB] :
-           llvm::zip_equal(opA->getRegions(), opB->getRegions())) {
-        if (!compareRegions(regionA, regionB, visited, m)) {
-          return false;
-        }
-      }
+    if (!compareReady(readyA.begin(), readyA, readyB, visited, m)) {
+      return false;
     }
   }
 

From c4160c4b734b3812048d4ae94c9e9f86781c8bde Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Thu, 11 Jun 2026 10:03:43 +0200
Subject: [PATCH 05/32] Finalize recursive IR mappings

---
 mlir/lib/Support/IRVerification.cpp | 205 +++++++++++++++-------------
 1 file changed, 111 insertions(+), 94 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index 1233fcd523..d2fe70448e 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -48,12 +48,11 @@
 
 #include <cmath>
 #include <cstddef>
-#include <utility>
 
 using namespace mlir;
 
 static bool compareRegions(Region& regionA, Region& regionB,
-                           DenseSet<Operation*>& visited, IRMapping& m);
+                           DenseSet<Operation*>& closed, IRMapping& m);
 
 static bool hasTypeQubitTensor(Value v) {
   auto tensor = dyn_cast<RankedTensorType>(v.getType());
@@ -64,7 +63,7 @@ static bool hasTypeQubitTensor(Value v) {
   return isa<qco::QubitType>(tensor.getElementType());
 }
 
-static void remapResults(Operation* fromOp, Operation* toOp, IRMapping& m) {
+static void mapResults(Operation* fromOp, Operation* toOp, IRMapping& m) {
   for (const auto& [fromResult, toResult] :
        llvm::zip_equal(fromOp->getResults(), toOp->getResults())) {
     if (!isa<qtensor::AllocOp>(fromOp) && hasTypeQubitTensor(fromResult)) {
@@ -75,6 +74,7 @@ static void remapResults(Operation* fromOp, Operation* toOp, IRMapping& m) {
   }
 }
 
+/// Compares two floating point numbers for approximate equivalence.
 static bool approxCompareFloats(const APFloat& lhs, const APFloat& rhs,
                                 const unsigned width) {
   if (lhs.isNaN() || rhs.isNaN()) {
@@ -181,7 +181,7 @@ static bool compareAttributes(const Attribute& attrA, const Attribute& attrB) {
 }
 
 static bool compareOperations(Operation* opA, Operation* opB,
-                              DenseSet<Operation*>& visited, IRMapping& m) {
+                              const IRMapping& m) {
 
   // Compare top-level signature-like characteristics.
 
@@ -192,7 +192,6 @@ static bool compareOperations(Operation* opA, Operation* opB,
       opA->getResultTypes() != opB->getResultTypes() ||
       // opA->getAttrs().size() != opB->getAttrs().size() ||
       opA->getNumRegions() != opB->getNumRegions()) {
-    llvm::dbgs() << "\t\tUNEQUAL 2!\n";
     return false;
   }
 
@@ -214,7 +213,6 @@ static bool compareOperations(Operation* opA, Operation* opB,
     }
 
     if (!compareAttributes(namedAttrA.getValue(), opB->getAttr(keyA))) {
-      llvm::dbgs() << "\t\tUNEQUAL 3!\n";
       return false;
     }
   }
@@ -256,31 +254,17 @@ static bool compareOperations(Operation* opA, Operation* opB,
     } else {
       auto mappedOperand = m.lookupOrNull(operandA);
       if (!mappedOperand || mappedOperand != operandB) {
-        llvm::dbgs() << "\t\tUNEQUAL 6!\n";
-        llvm::dbgs() << "\t\t" << mappedOperand << '\n';
-        llvm::dbgs() << "\t\t" << operandB << '\n';
         return false;
       }
     }
   }
 
-  for (const auto [regionA, regionB] :
-       llvm::zip_equal(opA->getRegions(), opB->getRegions())) {
-    if (!compareRegions(regionA, regionB, visited, m)) {
-      llvm::dbgs() << "\t\tUNEQUAL 7!\n";
-      return false;
-    }
-  }
-
-  // If the function reached this point, the two operations are equal.
-
-  llvm::dbgs() << "\t\tEQUAL!\n";
-
   return true;
 }
 
 /// Extract and return "ready" operations.
-static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> ops,
+/// These are operations that are independent from each other.
+static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> open,
                                          DenseSet<Operation*>& visited) {
   const auto isReady = [&](OpOperand& operand) {
     if (isa<BlockArgument>(operand.get())) {
@@ -290,7 +274,7 @@ static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> ops,
   };
 
   SetVector<Operation*> ready;
-  for (Operation* op : ops) {
+  for (Operation* op : open) {
     if (visited.contains(op)) {
       continue;
     }
@@ -331,60 +315,114 @@ static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> ops,
   return ready;
 }
 
-static bool compareReady(SetVector<Operation*>::const_iterator it,
-                         const SetVector<Operation*>& readyA,
-                         const SetVector<Operation*>& readyB,
-                         DenseSet<Operation*>& visited, IRMapping& m) {
-  if (it == readyA.end()) {
-    return true;
+static void cartesianMappings(
+    const SetVector<Operation*>::const_iterator readyIt,
+    const SmallVector<SmallVector<Operation*, 2>>::const_iterator partnerIt,
+    const SetVector<Operation*>::const_iterator readyEnd,
+    const SmallVector<SmallVector<Operation*, 2>>::const_iterator partnerEnd,
+    IRMapping& m, SmallVectorImpl<IRMapping>& out) {
+  if (readyIt == readyEnd) {
+    assert(partnerIt == partnerEnd);
+    out.emplace_back(m);
+    return;
   }
 
-  Operation* opA = *it;
+  Operation* opA = *readyIt;
+  for (Operation* opB : *partnerIt) {
+    IRMapping m2(m);
+    m2.map(opA, opB);
+    mapResults(opA, opB, m2);
+    cartesianMappings(std::next(readyIt), std::next(partnerIt), readyEnd,
+                      partnerEnd, m2, out);
+  }
+}
 
-  // Because there may be multiple structural equivalent operations,
-  // collect them in a vector for further recursive processing. If there are
-  // no partners, no matching operation has been found and the blocks are
-  // not equivalent.
+static bool compareReady(ArrayRef<Operation*> openA, ArrayRef<Operation*> openB,
+                         DenseSet<Operation*>& closed, IRMapping& m) {
+  const auto readyA = getReadyOps(openA, closed);
+  const auto readyB = getReadyOps(openB, closed);
 
-  llvm::dbgs() << "--- compare ---\n";
-  opA->dumpPretty();
-  SmallVector<Operation*> partners(
-      make_filter_range(readyB, [&](Operation* op) {
-        llvm::dbgs() << "\t";
-        op->dumpPretty();
-        return compareOperations(opA, op, visited, m);
-      }));
+  if (readyA.empty() && readyB.empty()) {
+    return true;
+  }
 
-  if (partners.empty()) {
-    llvm::dbgs() << "no matching op found: " << *opA << '\n';
+  if ((readyA.empty() && !readyB.empty()) ||
+      (!readyA.empty() && readyB.empty()) || readyA.size() != readyB.size()) {
     return false;
   }
 
-  // If there were only one partner, we could simply update the mapping m
-  // here. Unfortunately, multiple operations can be structurally equivalent
-  // (think arith.constant, for example). Thus, we must test each possible
-  // alternative mapping to identify (if possible) the equivalent partner.
-
-  bool found{false};
-  for (Operation* partner : partners) {
-    llvm::dbgs() << "trying partner: " << *partner << '\n';
-    IRMapping partnerM(m);
-    remapResults(opA, partner, partnerM);
-
-    DenseSet<Operation*> altVisited(visited);
-    if (compareReady(std::next(it), readyA, readyB, altVisited, partnerM)) {
-      visited = std::move(altVisited);
-      m = std::move(partnerM);
-      found = true;
+  // Because there may be multiple structural equivalent operations (think
+  // arith.constant, for example), collect them in a vector for further
+  // recursive processing. If there are no partners, no matching operation has
+  // been found and the blocks are not equivalent.
+
+  SmallVector<SmallVector<Operation*, 2>> partners;
+  for (Operation* opA : readyA) {
+    const auto isEmpty =
+        partners
+            .emplace_back(make_filter_range(
+                readyB,
+                [&](Operation* opB) { return compareOperations(opA, opB, m); }))
+            .empty();
+    if (isEmpty) {
+      return false;
+    }
+  }
+
+  assert(partners.size() == readyA.size());
+
+  closed.insert_range(readyA);
+  closed.insert_range(readyB);
+
+  SmallVector<IRMapping> mappings;
+  cartesianMappings(readyA.begin(), partners.begin(), readyA.end(),
+                    partners.end(), m, mappings);
+
+  for (Operation* opA : readyA) {
+
+    // If opA has one or more regions, try each mapping to find the equivalent
+    // operation. Each mapping uniquely identify opA with one potential
+    // partner thus use the mapping to obtain this partner and compare their
+    // respective regions.
+
+    if (opA->getNumRegions() > 0) {
+      SmallVector<IRMapping>::iterator it = mappings.begin();
+      for (; it != mappings.end(); it = std::next(it)) {
+        Operation* opB = it->lookup(opA);
+        assert(opA->getNumRegions() == opB->getNumRegions());
+
+        const auto nequiv = range_size(make_filter_range(
+            llvm::zip_equal(opA->getRegions(), opB->getRegions()),
+            [&](const auto& zip) {
+              const auto& [regionA, regionB] = zip;
+              return compareRegions(regionA, regionB, closed, *it);
+            }));
+        if (nequiv == opA->getNumRegions()) {
+          break;
+        }
+      }
+
+      if (it == mappings.end()) {
+        return false;
+      }
+    }
+  }
+
+  SmallVector<IRMapping>::iterator it = mappings.begin();
+  for (; it != mappings.end(); it = std::next(it)) {
+    DenseSet<Operation*> closed2(closed);
+    if (compareReady(openA, openB, closed2, *it)) {
+      closed = std::move(closed2);
+      m = std::move(*it);
       break;
     }
   }
 
-  return found;
+  return it != mappings.end();
 }
 
 static bool compareBlocks(Block& blockA, Block& blockB,
-                          DenseSet<Operation*>& visited, IRMapping& m) {
+                          DenseSet<Operation*>& closed, IRMapping& m) {
   if (blockA.getNumArguments() != blockB.getNumArguments()) {
     return false;
   }
@@ -398,48 +436,27 @@ static bool compareBlocks(Block& blockA, Block& blockB,
     m.map(lArg, rArg);
   }
 
-  SmallVector<Operation*> opsA;
-  SmallVector<Operation*> opsB;
-
-  opsA.reserve(llvm::range_size(blockA.getOperations()));
-  opsB.reserve(llvm::range_size(blockB.getOperations()));
+  SmallVector<Operation*> openA;
+  SmallVector<Operation*> openB;
 
-  for_each(blockA.getOperations(), [&](auto& op) { opsA.emplace_back(&op); });
-  for_each(blockB.getOperations(), [&](auto& op) { opsB.emplace_back(&op); });
+  openA.reserve(range_size(blockA.getOperations()));
+  openB.reserve(range_size(blockB.getOperations()));
 
-  while (true) {
-    const auto readyA = getReadyOps(opsA, visited);
-    const auto readyB = getReadyOps(opsB, visited);
+  for_each(blockA.getOperations(), [&](auto& op) { openA.emplace_back(&op); });
+  for_each(blockB.getOperations(), [&](auto& op) { openB.emplace_back(&op); });
 
-    visited.insert_range(readyA);
-    visited.insert_range(readyB);
-
-    if (readyA.empty() && readyB.empty()) {
-      break;
-    }
-
-    if ((readyA.empty() && !readyB.empty()) ||
-        (!readyA.empty() && readyB.empty()) || readyA.size() != readyB.size()) {
-      return false;
-    }
-
-    if (!compareReady(readyA.begin(), readyA, readyB, visited, m)) {
-      return false;
-    }
-  }
-
-  return true;
+  return compareReady(openA, openB, closed, m);
 }
 
 /// Compare two regions for structural equivalence.
 static bool compareRegions(Region& regionA, Region& regionB,
-                           DenseSet<Operation*>& visited, IRMapping& m) {
+                           DenseSet<Operation*>& closed, IRMapping& m) {
   if (regionA.getBlocks().size() != regionB.getBlocks().size()) {
     return false;
   }
 
   for (const auto [blockA, blockB] : llvm::zip_equal(regionA, regionB)) {
-    if (!compareBlocks(blockA, blockB, visited, m)) {
+    if (!compareBlocks(blockA, blockB, closed, m)) {
       return false;
     }
   }
@@ -449,6 +466,6 @@ static bool compareRegions(Region& regionA, Region& regionB,
 
 bool areModulesEquivalentWithPermutations(ModuleOp lhs, ModuleOp rhs) {
   IRMapping m;
-  DenseSet<Operation*> visited;
-  return compareRegions(lhs.getBodyRegion(), rhs.getBodyRegion(), visited, m);
+  DenseSet<Operation*> closed;
+  return compareRegions(lhs.getBodyRegion(), rhs.getBodyRegion(), closed, m);
 }

From 0259d833713821a97d577cc1125f3ae7809095d4 Mon Sep 17 00:00:00 2001
From: "pre-commit-ci[bot]"
 <66853113+pre-commit-ci[bot]@users.noreply.github.com>
Date: Thu, 11 Jun 2026 08:15:19 +0000
Subject: [PATCH 06/32] =?UTF-8?q?=F0=9F=8E=A8=20pre-commit=20fixes?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 mlir/lib/Support/IRVerification.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index cc360b889b..dcaabb086e 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -286,7 +286,7 @@ static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> open,
     }
 
     // If the destination of a tensor insert, has been produced by an insert
-    // operation as well, these two should be interchangable. Thus, also add it
+    // operation as well, these two should be interchangeable. Thus, also add it
     // to the ready set vector. Any valid IR will ensure that the indices of the
     // two insertions are not equivalent, hence, we don't check them here.
 

From 135d7592476b3635e54a4530484c382f840c2645 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Thu, 11 Jun 2026 10:27:05 +0200
Subject: [PATCH 07/32] Fix linting

---
 mlir/lib/Support/IRVerification.cpp | 27 ++++++++++-----------------
 1 file changed, 10 insertions(+), 17 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index cc360b889b..f3a057eaca 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -13,48 +13,39 @@
 #include "mlir/Dialect/QCO/IR/QCODialect.h"
 #include "mlir/Dialect/QTensor/Utils/TensorIterator.h"
 
-#include <llvm/ADT/ArrayRef.h>
-#include <llvm/ADT/DenseMap.h>
-#include <llvm/ADT/DenseMapInfo.h>
-#include <llvm/ADT/DenseSet.h>
-#include <llvm/ADT/Hashing.h>
 #include <llvm/ADT/STLExtras.h>
 #include <llvm/ADT/SmallVector.h>
 #include <llvm/ADT/StringRef.h>
-#include <llvm/ADT/iterator_range.h>
 #include <llvm/Support/Casting.h>
 #include <llvm/Support/Debug.h>
 #include <llvm/Support/ErrorHandling.h>
 #include <llvm/Support/raw_ostream.h>
 #include <mlir/Analysis/SliceAnalysis.h>
 #include <mlir/Dialect/Arith/IR/Arith.h>
-#include <mlir/Dialect/Func/IR/FuncOps.h>
-#include <mlir/Dialect/LLVMIR/LLVMDialect.h>
 #include <mlir/Dialect/QTensor/IR/QTensorOps.h>
-#include <mlir/Dialect/Utils/StaticValueUtils.h>
 #include <mlir/IR/Attributes.h>
 #include <mlir/IR/Block.h>
 #include <mlir/IR/Builders.h>
 #include <mlir/IR/BuiltinAttributes.h>
 #include <mlir/IR/BuiltinOps.h>
 #include <mlir/IR/IRMapping.h>
-#include <mlir/IR/OpDefinition.h>
 #include <mlir/IR/Operation.h>
 #include <mlir/IR/Region.h>
 #include <mlir/IR/SymbolTable.h>
 #include <mlir/IR/Value.h>
-#include <mlir/IR/ValueRange.h>
-#include <mlir/Interfaces/SideEffectInterfaces.h>
 #include <mlir/Support/LLVM.h>
 
+#include <cassert>
 #include <cmath>
-#include <cstddef>
+#include <iterator>
+#include <utility>
 
 using namespace mlir;
 
 static bool compareRegions(Region& regionA, Region& regionB,
                            DenseSet<Operation*>& closed, IRMapping& m);
 
+/// Return true, if the given value has the type `tensor<qco.qubit>`.
 static bool hasTypeQubitTensor(Value v) {
   auto tensor = dyn_cast<RankedTensorType>(v.getType());
   if (!tensor) {
@@ -64,10 +55,12 @@ static bool hasTypeQubitTensor(Value v) {
   return isa<qco::QubitType>(tensor.getElementType());
 }
 
-static void mapResults(Operation* fromOp, Operation* toOp, IRMapping& m) {
+/// Map all results from one op to another.
+/// Assumes `op->getNumResults() == other->getNumResults()`.
+static void mapResults(Operation* op, Operation* other, IRMapping& m) {
   for (const auto& [fromResult, toResult] :
-       llvm::zip_equal(fromOp->getResults(), toOp->getResults())) {
-    if (!isa<qtensor::AllocOp>(fromOp) && hasTypeQubitTensor(fromResult)) {
+       llvm::zip_equal(op->getResults(), other->getResults())) {
+    if (!isa<qtensor::AllocOp>(op) && hasTypeQubitTensor(fromResult)) {
       assert(hasTypeQubitTensor(toResult));
       continue;
     }
@@ -280,7 +273,7 @@ static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> open,
       continue;
     }
 
-    if (llvm::all_of(op->getOpOperands(), isReady)) {
+    if (all_of(op->getOpOperands(), isReady)) {
       ready.insert(op);
       continue;
     }

From 71e10b3c98f5cfb1621af64a5d0decbf4644edc5 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Thu, 11 Jun 2026 16:18:12 +0200
Subject: [PATCH 08/32] WiP: Test consistent mappings

---
 mlir/include/mlir/Support/IRVerification.h |   5 +-
 mlir/lib/Support/IRVerification.cpp        | 216 ++++++++++++++-------
 2 files changed, 145 insertions(+), 76 deletions(-)

diff --git a/mlir/include/mlir/Support/IRVerification.h b/mlir/include/mlir/Support/IRVerification.h
index 4421c6c4c0..5fd3ac9fd4 100644
--- a/mlir/include/mlir/Support/IRVerification.h
+++ b/mlir/include/mlir/Support/IRVerification.h
@@ -14,7 +14,8 @@ namespace mlir {
 class ModuleOp;
 } // namespace mlir
 
-/// Compare two MLIR modules for structural equivalence, allowing permutations
-/// of speculatable operations.
+/// Compare two (quantum) module operations for structural equivalence, allowing
+/// some permutations. This function is especially tailored to compare quantum
+/// computations.
 [[nodiscard]] bool areModulesEquivalentWithPermutations(mlir::ModuleOp,
                                                         mlir::ModuleOp);
diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index f3a057eaca..fec4aa1820 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -10,7 +10,9 @@
 
 #include "mlir/Support/IRVerification.h"
 
+#include "mlir/Dialect/QC/IR/QCOps.h"
 #include "mlir/Dialect/QCO/IR/QCODialect.h"
+#include "mlir/Dialect/QCO/IR/QCOOps.h"
 #include "mlir/Dialect/QTensor/Utils/TensorIterator.h"
 
 #include <llvm/ADT/STLExtras.h>
@@ -29,6 +31,7 @@
 #include <mlir/IR/BuiltinAttributes.h>
 #include <mlir/IR/BuiltinOps.h>
 #include <mlir/IR/IRMapping.h>
+#include <mlir/IR/OpDefinition.h>
 #include <mlir/IR/Operation.h>
 #include <mlir/IR/Region.h>
 #include <mlir/IR/SymbolTable.h>
@@ -57,13 +60,19 @@ static bool hasTypeQubitTensor(Value v) {
 
 /// Map all results from one op to another.
 /// Assumes `op->getNumResults() == other->getNumResults()`.
-static void mapResults(Operation* op, Operation* other, IRMapping& m) {
+/// Assumes that the two operations are equivalent to each other.
+static void mapResults(Operation* opL, Operation* opR, IRMapping& m) {
+  if (opL->getNumResults() == 0) {
+    return;
+  }
+
   for (const auto& [fromResult, toResult] :
-       llvm::zip_equal(op->getResults(), other->getResults())) {
-    if (!isa<qtensor::AllocOp>(op) && hasTypeQubitTensor(fromResult)) {
+       llvm::zip_equal(opL->getResults(), opR->getResults())) {
+    if (!isa<qtensor::AllocOp>(opL) && hasTypeQubitTensor(fromResult)) {
       assert(hasTypeQubitTensor(toResult));
       continue;
     }
+
     m.map(fromResult, toResult);
   }
 }
@@ -214,42 +223,84 @@ static bool compareOperations(Operation* opA, Operation* opB,
   // Compare operands.
   // TODO: Equal type check.
 
-  for (const auto& [operandA, operandB] :
-       llvm::zip_equal(opA->getOperands(), opB->getOperands())) {
-
-    if (hasTypeQubitTensor(operandA)) {
-      if (!hasTypeQubitTensor(operandB)) { // TODO: Assertion?
+  // else if (isa<qco::CtrlOp>(opA)) {
+  //   assert(isa<qco::CtrlOp>(opB));
+  //   llvm::reportFatalInternalError("not implemented");
+  // } else if (opA->hasTrait<mlir::OpTrait::IsCommutative>()) {
+  //   assert(opB->hasTrait<mlir::OpTrait::IsCommutative>());
+  //   llvm::reportFatalInternalError("not implemented");
+  // }
+
+  if (isa<qc::CtrlOp>(opA)) {
+    assert(isa<qc::CtrlOp>(opB));
+
+    auto ctrlL = cast<qc::CtrlOp>(opA);
+    auto ctrlR = cast<qc::CtrlOp>(opB);
+
+    DenseSet<Value> workset;
+    workset.insert_range(ctrlR.getControls());
+    for (const auto& ctrl : ctrlL.getControls()) {
+      const auto& mapped = m.lookup(ctrl);
+      if (!workset.contains(mapped)) {
         return false;
       }
+      workset.erase(mapped);
+    }
 
-      auto tensorA = cast<TypedValue<RankedTensorType>>(operandA);
-      qtensor::TensorIterator itA(tensorA);
-      while (std::prev(itA) != itA) {
-        --itA;
-      }
+    assert(workset.empty());
 
-      auto tensorB = cast<TypedValue<RankedTensorType>>(operandB);
-      qtensor::TensorIterator itB(tensorB);
-      while (std::prev(itB) != itB) {
-        --itB;
+    // Analogously for the targets.
+
+    workset.clear();
+    workset.insert_range(ctrlR.getTargets());
+    for (const auto& trgt : ctrlL.getTargets()) {
+      const auto& operand = m.lookup(trgt);
+      if (!workset.contains(operand)) {
+        return false;
       }
+      workset.erase(operand);
+    }
+
+    assert(workset.empty());
+
+  } else {
+    for (const auto& [operandA, operandB] :
+         llvm::zip_equal(opA->getOperands(), opB->getOperands())) {
 
-      if (itA.operation() == nullptr) { // Block-Argument.
-        if (itB.operation() != nullptr) {
+      if (hasTypeQubitTensor(operandA)) {
+        if (!hasTypeQubitTensor(operandB)) { // TODO: Assertion?
           return false;
         }
+
+        auto tensorA = cast<TypedValue<RankedTensorType>>(operandA);
+        qtensor::TensorIterator itA(tensorA);
+        while (std::prev(itA) != itA) {
+          --itA;
+        }
+
+        auto tensorB = cast<TypedValue<RankedTensorType>>(operandB);
+        qtensor::TensorIterator itB(tensorB);
+        while (std::prev(itB) != itB) {
+          --itB;
+        }
+
+        if (itA.operation() == nullptr) { // Block-Argument.
+          if (itB.operation() != nullptr) {
+            return false;
+          }
+        } else {
+          auto allocA = cast<qtensor::AllocOp>(itA.operation());
+          auto allocB = cast<qtensor::AllocOp>(itB.operation());
+          if (m.lookup(allocA.getResult()) != allocB.getResult()) {
+            return false;
+          }
+        }
       } else {
-        auto allocA = cast<qtensor::AllocOp>(itA.operation());
-        auto allocB = cast<qtensor::AllocOp>(itB.operation());
-        if (m.lookup(allocA.getResult()) != allocB.getResult()) {
+        auto operand = m.lookup(operandA);
+        if (operand != operandB) {
           return false;
         }
       }
-    } else {
-      auto mappedOperand = m.lookupOrNull(operandA);
-      if (!mappedOperand || mappedOperand != operandB) {
-        return false;
-      }
     }
   }
 
@@ -309,30 +360,40 @@ static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> open,
   return ready;
 }
 
-static void cartesianMappings(
+static void getCartesianMappings(
     const SetVector<Operation*>::const_iterator readyIt,
     const SmallVector<SmallVector<Operation*, 2>>::const_iterator partnerIt,
-    const SetVector<Operation*>::const_iterator readyEnd,
-    const SmallVector<SmallVector<Operation*, 2>>::const_iterator partnerEnd,
-    IRMapping& m, SmallVectorImpl<IRMapping>& out) {
+    const SetVector<Operation*>::const_iterator readyEnd, const IRMapping& m,
+    SmallVectorImpl<IRMapping>& mappings) {
   if (readyIt == readyEnd) {
-    assert(partnerIt == partnerEnd);
-    out.emplace_back(m);
+    mappings.emplace_back(m);
     return;
   }
 
   Operation* opA = *readyIt;
   for (Operation* opB : *partnerIt) {
-    IRMapping m2(m);
-    m2.map(opA, opB);
-    mapResults(opA, opB, m2);
-    cartesianMappings(std::next(readyIt), std::next(partnerIt), readyEnd,
-                      partnerEnd, m2, out);
+    IRMapping mNew(m);
+    mNew.map(opA, opB);
+    mapResults(opA, opB, mNew);
+    getCartesianMappings(std::next(readyIt), std::next(partnerIt), readyEnd,
+                         mNew, mappings);
   }
 }
 
-static bool compareReady(ArrayRef<Operation*> openA, ArrayRef<Operation*> openB,
-                         DenseSet<Operation*>& closed, IRMapping& m) {
+static SmallVector<IRMapping>
+getCartesianMappings(const SetVector<Operation*>& ready,
+                     const SmallVector<SmallVector<Operation*, 2>>& partners,
+                     const IRMapping& m) {
+  assert(ready.size() == partners.size());
+  SmallVector<IRMapping> mappings;
+  getCartesianMappings(ready.begin(), partners.begin(), ready.end(), m,
+                       mappings);
+  return mappings;
+}
+
+static bool compareTopologically(ArrayRef<Operation*> openA,
+                                 ArrayRef<Operation*> openB,
+                                 DenseSet<Operation*>& closed, IRMapping& m) {
   const auto readyA = getReadyOps(openA, closed);
   const auto readyB = getReadyOps(openB, closed);
 
@@ -352,11 +413,17 @@ static bool compareReady(ArrayRef<Operation*> openA, ArrayRef<Operation*> openB,
 
   SmallVector<SmallVector<Operation*, 2>> partners;
   for (Operation* opA : readyA) {
+    // llvm::dbgs() << "--- compare ---\n";
+    // llvm::dbgs() << *opA << '\n';
     const auto isEmpty =
         partners
-            .emplace_back(make_filter_range(
-                readyB,
-                [&](Operation* opB) { return compareOperations(opA, opB, m); }))
+            .emplace_back(make_filter_range(readyB,
+                                            [&](Operation* opB) {
+                                              // llvm::dbgs() << '\t' << *opB <<
+                                              // '\n';
+                                              return compareOperations(opA, opB,
+                                                                       m);
+                                            }))
             .empty();
     if (isEmpty) {
       return false;
@@ -365,54 +432,55 @@ static bool compareReady(ArrayRef<Operation*> openA, ArrayRef<Operation*> openB,
 
   assert(partners.size() == readyA.size());
 
-  closed.insert_range(readyA);
-  closed.insert_range(readyB);
+  auto mappings = getCartesianMappings(readyA, partners, m);
 
-  SmallVector<IRMapping> mappings;
-  cartesianMappings(readyA.begin(), partners.begin(), readyA.end(),
-                    partners.end(), m, mappings);
+  SmallVector<IRMapping>::iterator mapIter = mappings.begin();
+  for (; mapIter != mappings.end(); mapIter = std::next(mapIter)) {
+    IRMapping& localM = *mapIter;
+    DenseSet<Operation*> local(closed);
+    local.insert_range(readyA);
+    local.insert_range(readyB);
 
-  for (Operation* opA : readyA) {
+    // Regional comparison.
+
+    SetVector<Operation*>::iterator readyIter = readyA.begin();
+    for (; readyIter != readyA.end(); readyIter = std::next(readyIter)) {
+      Operation* opA = *readyIter;
 
-    // If opA has one or more regions, try each mapping to find the equivalent
-    // operation. Each mapping uniquely identify opA with one potential
-    // partner thus use the mapping to obtain this partner and compare their
-    // respective regions.
+      // Otherwise, if opA has one or more regions, try each mapping to find the
+      // equivalent operation. Each mapping uniquely identify opA with one
+      // potential partner thus use the mapping to obtain this partner and
+      // compare their respective regions.
 
-    if (opA->getNumRegions() > 0) {
-      SmallVector<IRMapping>::iterator it = mappings.begin();
-      for (; it != mappings.end(); it = std::next(it)) {
-        Operation* opB = it->lookup(opA);
+      if (opA->getNumRegions() > 0) {
+        Operation* opB = mapIter->lookup(opA);
         assert(opA->getNumRegions() == opB->getNumRegions());
 
         const auto nequiv = range_size(make_filter_range(
             llvm::zip_equal(opA->getRegions(), opB->getRegions()),
             [&](const auto& zip) {
               const auto& [regionA, regionB] = zip;
-              return compareRegions(regionA, regionB, closed, *it);
+              return compareRegions(regionA, regionB, local, localM);
             }));
-        if (nequiv == opA->getNumRegions()) {
+        if (nequiv != opA->getNumRegions()) {
           break;
         }
       }
-
-      if (it == mappings.end()) {
-        return false;
-      }
     }
-  }
 
-  SmallVector<IRMapping>::iterator it = mappings.begin();
-  for (; it != mappings.end(); it = std::next(it)) {
-    DenseSet<Operation*> closed2(closed);
-    if (compareReady(openA, openB, closed2, *it)) {
-      closed = std::move(closed2);
-      m = std::move(*it);
-      break;
+    // If all regions can be matched with this mapping, try the remaining of the
+    // current block.
+
+    if (readyIter == readyA.end()) {
+      if (compareTopologically(openA, openB, local, localM)) {
+        closed = std::move(local);
+        m = std::move(localM);
+        break;
+      }
     }
   }
 
-  return it != mappings.end();
+  return mapIter != mappings.end();
 }
 
 static bool compareBlocks(Block& blockA, Block& blockB,
@@ -421,7 +489,7 @@ static bool compareBlocks(Block& blockA, Block& blockB,
     return false;
   }
 
-  for (auto [lArg, rArg] :
+  for (const auto [lArg, rArg] :
        llvm::zip_equal(blockA.getArguments(), blockB.getArguments())) {
     if (lArg.getType() != rArg.getType()) {
       return false;
@@ -439,7 +507,7 @@ static bool compareBlocks(Block& blockA, Block& blockB,
   for_each(blockA.getOperations(), [&](auto& op) { openA.emplace_back(&op); });
   for_each(blockB.getOperations(), [&](auto& op) { openB.emplace_back(&op); });
 
-  return compareReady(openA, openB, closed, m);
+  return compareTopologically(openA, openB, closed, m);
 }
 
 /// Compare two regions for structural equivalence.

From 59d109a8af38cfa0f251797c7e312ef5ebfb069e Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 07:49:36 +0200
Subject: [PATCH 09/32] WiP: Multiple mappings

---
 mlir/lib/Support/IRVerification.cpp | 61 ++++++++++++++++-------------
 1 file changed, 34 insertions(+), 27 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index 313fe2c849..f29e87e9bb 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -336,11 +336,9 @@ static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> open,
 
     if (auto insert = dyn_cast<qtensor::InsertOp>(op)) {
       Operation* prev = insert.getDest().getDefiningOp();
-      if (isa<qtensor::InsertOp>(prev)) {
-        if (ready.contains(prev)) {
-          ready.insert(insert.getOperation());
-          continue;
-        }
+      if (isa<qtensor::InsertOp>(prev) && ready.contains(prev)) {
+        ready.insert(insert.getOperation());
+        continue;
       }
     }
 
@@ -348,11 +346,9 @@ static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> open,
 
     if (auto extract = dyn_cast<qtensor::ExtractOp>(op)) {
       Operation* prev = extract.getTensor().getDefiningOp();
-      if (isa<qtensor::ExtractOp>(prev)) {
-        if (ready.contains(prev)) {
-          ready.insert(extract.getOperation());
-          continue;
-        }
+      if (isa<qtensor::ExtractOp>(prev) && ready.contains(prev)) {
+        ready.insert(extract.getOperation());
+        continue;
       }
     }
   }
@@ -371,6 +367,10 @@ static void getCartesianMappings(
   }
 
   Operation* opA = *readyIt;
+  // if (opA->getNumResults() == 0) {
+  //   return;
+  // }
+
   for (Operation* opB : *partnerIt) {
     IRMapping mNew(m);
     mNew.map(opA, opB);
@@ -413,23 +413,28 @@ static bool compareTopologically(ArrayRef<Operation*> openA,
 
   SmallVector<SmallVector<Operation*, 2>> partners;
   for (Operation* opA : readyA) {
-    // llvm::dbgs() << "--- compare ---\n";
-    // llvm::dbgs() << *opA << '\n';
     const auto isEmpty =
         partners
-            .emplace_back(make_filter_range(readyB,
-                                            [&](Operation* opB) {
-                                              // llvm::dbgs() << '\t' << *opB <<
-                                              // '\n';
-                                              return compareOperations(opA, opB,
-                                                                       m);
-                                            }))
+            .emplace_back(make_filter_range(
+                readyB,
+                [&](Operation* opB) { return compareOperations(opA, opB, m); }))
             .empty();
     if (isEmpty) {
       return false;
     }
   }
 
+  for (auto& vec : partners) {
+    llvm::dbgs() << "partners:\n";
+    for (Operation* op : vec) {
+      llvm::dbgs() << *op;
+      if (op->getNextNode() != nullptr) {
+        llvm::dbgs() << " | " << *(op->getNextNode());
+      }
+      llvm::dbgs() << "\n";
+    }
+  }
+
   assert(partners.size() == readyA.size());
 
   auto mappings = getCartesianMappings(readyA, partners, m);
@@ -441,7 +446,14 @@ static bool compareTopologically(ArrayRef<Operation*> openA,
     local.insert_range(readyA);
     local.insert_range(readyB);
 
-    // Regional comparison.
+    // Try to compare the rest of the current block with the current mapping.
+
+    if (!compareTopologically(openA, openB, local, localM)) {
+      continue;
+    }
+
+    // If that works, compare the nested regions of each ready operation on the
+    // lhs with its partner on the rhs.
 
     SetVector<Operation*>::iterator readyIter = readyA.begin();
     for (; readyIter != readyA.end(); readyIter = std::next(readyIter)) {
@@ -468,15 +480,10 @@ static bool compareTopologically(ArrayRef<Operation*> openA,
       }
     }
 
-    // If all regions can be matched with this mapping, try the remaining of the
-    // current block.
+    // If we visited each operation on the lhs, the two blocks are equivalent.
 
     if (readyIter == readyA.end()) {
-      if (compareTopologically(openA, openB, local, localM)) {
-        closed = std::move(local);
-        m = std::move(localM);
-        break;
-      }
+      break;
     }
   }
 

From 91175a3e5e45e2f74f4112d93c59f3e6e6b37a15 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 09:22:11 +0200
Subject: [PATCH 10/32] Fix insert order bug

---
 mlir/lib/Support/IRVerification.cpp | 254 ++++++++++++++--------------
 1 file changed, 129 insertions(+), 125 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index f29e87e9bb..9473af3773 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -310,85 +310,95 @@ static bool compareOperations(Operation* opA, Operation* opB,
 /// Extract and return "ready" operations.
 /// These are operations that are independent from each other.
 static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> open,
-                                         DenseSet<Operation*>& visited) {
-  const auto isReady = [&](OpOperand& operand) {
-    if (isa<BlockArgument>(operand.get())) {
+                                         DenseSet<Operation*>& closed) {
+  const auto isReady = [&closed](Value v) {
+    if (isa<BlockArgument>(v)) {
       return true;
     }
-    return visited.contains(operand.get().getDefiningOp());
+    return closed.contains(v.getDefiningOp());
   };
 
   SetVector<Operation*> ready;
   for (Operation* op : open) {
-    if (visited.contains(op)) {
+    if (closed.contains(op) || ready.contains(op)) {
       continue;
     }
 
-    if (all_of(op->getOpOperands(), isReady)) {
-      ready.insert(op);
-      continue;
-    }
+    if (auto insert = dyn_cast<qtensor::InsertOp>(op)) {
 
-    // If the destination of a tensor insert, has been produced by an insert
-    // operation as well, these two should be interchangeable. Thus, also add it
-    // to the ready set vector. Any valid IR will ensure that the indices of the
-    // two insertions are not equivalent, hence, we don't check them here.
+      // If any of the inserts on the chain are ready, we consider the whole
+      // chain ready because the one ready operation could be moved the front
+      // (the top from IR perspective) of the chain.
+      // An insert is considered ready when both the inserted qubit and the
+      // index are ready.
+
+      SmallVector<Operation*> chain;
+      qtensor::TensorIterator it(insert.getResult());
+
+      for (; it != std::default_sentinel &&
+             isa<qtensor::InsertOp>(it.operation());
+           ++it) {
+        auto chainInsert = cast<qtensor::InsertOp>(it.operation());
+        if (isReady(chainInsert.getScalar()) &&
+            isReady(chainInsert.getIndex()) && !closed.contains(chainInsert)) {
+          chain.emplace_back(chainInsert);
+        }
+      }
 
-    if (auto insert = dyn_cast<qtensor::InsertOp>(op)) {
-      Operation* prev = insert.getDest().getDefiningOp();
-      if (isa<qtensor::InsertOp>(prev) && ready.contains(prev)) {
-        ready.insert(insert.getOperation());
-        continue;
+      if (!chain.empty()) {
+        ready.insert_range(chain);
       }
-    }
 
-    // Analogously for the extract operation.
+    } else if (auto extract = dyn_cast<qtensor::ExtractOp>(op)) {
 
-    if (auto extract = dyn_cast<qtensor::ExtractOp>(op)) {
-      Operation* prev = extract.getTensor().getDefiningOp();
-      if (isa<qtensor::ExtractOp>(prev) && ready.contains(prev)) {
-        ready.insert(extract.getOperation());
-        continue;
+      // We apply the analogous logic to extracts.
+
+      SmallVector<Operation*> chain;
+      qtensor::TensorIterator it(extract.getOutTensor());
+
+      for (; it != std::default_sentinel &&
+             isa<qtensor::ExtractOp>(it.operation());
+           ++it) {
+        auto chainExtract = cast<qtensor::ExtractOp>(it.operation());
+        if (isReady(chainExtract.getIndex()) &&
+            !closed.contains(chainExtract)) {
+          chain.emplace_back(chainExtract);
+        }
       }
-    }
-  }
 
-  return ready;
-}
+      if (!chain.empty()) {
+        ready.insert_range(chain);
+      }
+    } else if (auto dealloc = dyn_cast<qtensor::DeallocOp>(op)) {
 
-static void getCartesianMappings(
-    const SetVector<Operation*>::const_iterator readyIt,
-    const SmallVector<SmallVector<Operation*, 2>>::const_iterator partnerIt,
-    const SetVector<Operation*>::const_iterator readyEnd, const IRMapping& m,
-    SmallVectorImpl<IRMapping>& mappings) {
-  if (readyIt == readyEnd) {
-    mappings.emplace_back(m);
-    return;
-  }
+      // Deallocations are ready whenever we've visited each op on the tensor
+      // chain.
 
-  Operation* opA = *readyIt;
-  // if (opA->getNumResults() == 0) {
-  //   return;
-  // }
+      bool fullChain{true};
+      qtensor::TensorIterator it(dealloc.getTensor());
+
+      for (; std::prev(it) != it; --it) {
+        if (!closed.contains(it.operation())) {
+          fullChain = false;
+          break;
+        }
+      }
+
+      if (fullChain) {
+        ready.insert(dealloc);
+      }
 
-  for (Operation* opB : *partnerIt) {
-    IRMapping mNew(m);
-    mNew.map(opA, opB);
-    mapResults(opA, opB, mNew);
-    getCartesianMappings(std::next(readyIt), std::next(partnerIt), readyEnd,
-                         mNew, mappings);
+    } else {
+
+      // Otherwise, simply check if all operands are ready.
+
+      if (llvm::all_of(op->getOperands(), isReady)) {
+        ready.insert(op);
+      }
+    }
   }
-}
 
-static SmallVector<IRMapping>
-getCartesianMappings(const SetVector<Operation*>& ready,
-                     const SmallVector<SmallVector<Operation*, 2>>& partners,
-                     const IRMapping& m) {
-  assert(ready.size() == partners.size());
-  SmallVector<IRMapping> mappings;
-  getCartesianMappings(ready.begin(), partners.begin(), ready.end(), m,
-                       mappings);
-  return mappings;
+  return ready;
 }
 
 static bool compareTopologically(ArrayRef<Operation*> openA,
@@ -397,12 +407,21 @@ static bool compareTopologically(ArrayRef<Operation*> openA,
   const auto readyA = getReadyOps(openA, closed);
   const auto readyB = getReadyOps(openB, closed);
 
+  llvm::dbgs() << "--- readyA ---\n";
+  for (Operation* op : readyA) {
+    llvm::dbgs() << *op << '\n';
+  }
+
+  llvm::dbgs() << "--- readyB ---\n";
+  for (Operation* op : readyB) {
+    llvm::dbgs() << *op << '\n';
+  }
+
   if (readyA.empty() && readyB.empty()) {
     return true;
   }
 
-  if ((readyA.empty() && !readyB.empty()) ||
-      (!readyA.empty() && readyB.empty()) || readyA.size() != readyB.size()) {
+  if (readyA.size() != readyB.size()) {
     return false;
   }
 
@@ -411,83 +430,67 @@ static bool compareTopologically(ArrayRef<Operation*> openA,
   // recursive processing. If there are no partners, no matching operation has
   // been found and the blocks are not equivalent.
 
-  SmallVector<SmallVector<Operation*, 2>> partners;
+  DenseSet<Operation*> matched;
+  matched.reserve(readyB.size());
+
   for (Operation* opA : readyA) {
-    const auto isEmpty =
-        partners
-            .emplace_back(make_filter_range(
-                readyB,
-                [&](Operation* opB) { return compareOperations(opA, opB, m); }))
-            .empty();
-    if (isEmpty) {
-      return false;
-    }
-  }
+    SetVector<Operation*>::iterator it = readyB.begin();
+    for (; it != readyB.end(); it = std::next(it)) {
+      Operation* opB = *it;
+      if (matched.contains(opB)) {
+        continue;
+      }
 
-  for (auto& vec : partners) {
-    llvm::dbgs() << "partners:\n";
-    for (Operation* op : vec) {
-      llvm::dbgs() << *op;
-      if (op->getNextNode() != nullptr) {
-        llvm::dbgs() << " | " << *(op->getNextNode());
+      if (compareOperations(opA, opB, m)) {
+        matched.insert(opB);
+        mapResults(opA, opB, m);
+        m.map(opA, opB);
+        break;
       }
-      llvm::dbgs() << "\n";
     }
-  }
 
-  assert(partners.size() == readyA.size());
-
-  auto mappings = getCartesianMappings(readyA, partners, m);
-
-  SmallVector<IRMapping>::iterator mapIter = mappings.begin();
-  for (; mapIter != mappings.end(); mapIter = std::next(mapIter)) {
-    IRMapping& localM = *mapIter;
-    DenseSet<Operation*> local(closed);
-    local.insert_range(readyA);
-    local.insert_range(readyB);
-
-    // Try to compare the rest of the current block with the current mapping.
-
-    if (!compareTopologically(openA, openB, local, localM)) {
-      continue;
+    if (it == readyB.end()) {
+      llvm::dbgs() << "unmatched op a: " << *opA << '\n';
+      return false;
     }
+  }
 
-    // If that works, compare the nested regions of each ready operation on the
-    // lhs with its partner on the rhs.
-
-    SetVector<Operation*>::iterator readyIter = readyA.begin();
-    for (; readyIter != readyA.end(); readyIter = std::next(readyIter)) {
-      Operation* opA = *readyIter;
-
-      // Otherwise, if opA has one or more regions, try each mapping to find the
-      // equivalent operation. Each mapping uniquely identify opA with one
-      // potential partner thus use the mapping to obtain this partner and
-      // compare their respective regions.
-
-      if (opA->getNumRegions() > 0) {
-        Operation* opB = mapIter->lookup(opA);
-        assert(opA->getNumRegions() == opB->getNumRegions());
-
-        const auto nequiv = range_size(make_filter_range(
-            llvm::zip_equal(opA->getRegions(), opB->getRegions()),
-            [&](const auto& zip) {
-              const auto& [regionA, regionB] = zip;
-              return compareRegions(regionA, regionB, local, localM);
-            }));
-        if (nequiv != opA->getNumRegions()) {
-          break;
-        }
+  // At this point, we've successfully matched each operation on the lhs with
+  // one on the rhs.
+
+  closed.insert_range(readyA);
+  closed.insert_range(readyB);
+
+  SetVector<Operation*>::iterator it = readyA.begin();
+  for (; it != readyA.end(); it = std::next(it)) {
+    Operation* opA = *it;
+
+    // Otherwise, if opA has one or more regions, try each mapping to find the
+    // equivalent operation. Each mapping uniquely identify opA with one
+    // potential partner thus use the mapping to obtain this partner and
+    // compare their respective regions.
+
+    if (opA->getNumRegions() > 0) {
+      Operation* opB = m.lookup(opA);
+      assert(opA->getNumRegions() == opB->getNumRegions());
+
+      const auto nequiv = range_size(make_filter_range(
+          llvm::zip_equal(opA->getRegions(), opB->getRegions()),
+          [&](const auto& zip) {
+            const auto& [regionA, regionB] = zip;
+            return compareRegions(regionA, regionB, closed, m);
+          }));
+      if (nequiv != opA->getNumRegions()) {
+        break;
       }
     }
+  }
 
-    // If we visited each operation on the lhs, the two blocks are equivalent.
-
-    if (readyIter == readyA.end()) {
-      break;
-    }
+  if (it != readyA.end()) {
+    return false;
   }
 
-  return mapIter != mappings.end();
+  return compareTopologically(openA, openB, closed, m);
 }
 
 static bool compareBlocks(Block& blockA, Block& blockB,
@@ -499,6 +502,7 @@ static bool compareBlocks(Block& blockA, Block& blockB,
   for (const auto [lArg, rArg] :
        llvm::zip_equal(blockA.getArguments(), blockB.getArguments())) {
     if (lArg.getType() != rArg.getType()) {
+      llvm::dbgs() << "unequivalent block arguments\n";
       return false;
     }
 

From 5fa41ea65da80b8edfe87adda07a4f2b7ec8398c Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 09:23:34 +0200
Subject: [PATCH 11/32] Remove prints

---
 mlir/lib/Support/IRVerification.cpp | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index 9473af3773..e98ac73c18 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -407,16 +407,6 @@ static bool compareTopologically(ArrayRef<Operation*> openA,
   const auto readyA = getReadyOps(openA, closed);
   const auto readyB = getReadyOps(openB, closed);
 
-  llvm::dbgs() << "--- readyA ---\n";
-  for (Operation* op : readyA) {
-    llvm::dbgs() << *op << '\n';
-  }
-
-  llvm::dbgs() << "--- readyB ---\n";
-  for (Operation* op : readyB) {
-    llvm::dbgs() << *op << '\n';
-  }
-
   if (readyA.empty() && readyB.empty()) {
     return true;
   }

From bc1004385374b38ca7504a9951184a39d2b75267 Mon Sep 17 00:00:00 2001
From: "pre-commit-ci[bot]"
 <66853113+pre-commit-ci[bot]@users.noreply.github.com>
Date: Fri, 12 Jun 2026 07:24:09 +0000
Subject: [PATCH 12/32] =?UTF-8?q?=F0=9F=8E=A8=20pre-commit=20fixes?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 mlir/lib/Support/IRVerification.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index e98ac73c18..71e2795981 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -492,7 +492,7 @@ static bool compareBlocks(Block& blockA, Block& blockB,
   for (const auto [lArg, rArg] :
        llvm::zip_equal(blockA.getArguments(), blockB.getArguments())) {
     if (lArg.getType() != rArg.getType()) {
-      llvm::dbgs() << "unequivalent block arguments\n";
+      llvm::dbgs() << "nonequivalent block arguments\n";
       return false;
     }
 

From 1202fd5f4437fefc907337b0d9a27a3c80f0edf1 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 09:26:53 +0200
Subject: [PATCH 13/32] Remove recursion

---
 mlir/lib/Support/IRVerification.cpp | 126 ++++++++++++++--------------
 1 file changed, 64 insertions(+), 62 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index e98ac73c18..58bd5c731b 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -41,7 +41,6 @@
 #include <cassert>
 #include <cmath>
 #include <iterator>
-#include <utility>
 
 using namespace mlir;
 
@@ -404,83 +403,86 @@ static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> open,
 static bool compareTopologically(ArrayRef<Operation*> openA,
                                  ArrayRef<Operation*> openB,
                                  DenseSet<Operation*>& closed, IRMapping& m) {
-  const auto readyA = getReadyOps(openA, closed);
-  const auto readyB = getReadyOps(openB, closed);
 
-  if (readyA.empty() && readyB.empty()) {
-    return true;
-  }
+  while (true) {
+    const auto readyA = getReadyOps(openA, closed);
+    const auto readyB = getReadyOps(openB, closed);
 
-  if (readyA.size() != readyB.size()) {
-    return false;
-  }
+    if (readyA.empty() && readyB.empty()) {
+      break;
+    }
+
+    if (readyA.size() != readyB.size()) {
+      return false;
+    }
 
-  // Because there may be multiple structural equivalent operations (think
-  // arith.constant, for example), collect them in a vector for further
-  // recursive processing. If there are no partners, no matching operation has
-  // been found and the blocks are not equivalent.
+    // Because there may be multiple structural equivalent operations (think
+    // arith.constant, for example), collect them in a vector for further
+    // recursive processing. If there are no partners, no matching operation has
+    // been found and the blocks are not equivalent.
 
-  DenseSet<Operation*> matched;
-  matched.reserve(readyB.size());
+    DenseSet<Operation*> matched;
+    matched.reserve(readyB.size());
 
-  for (Operation* opA : readyA) {
-    SetVector<Operation*>::iterator it = readyB.begin();
-    for (; it != readyB.end(); it = std::next(it)) {
-      Operation* opB = *it;
-      if (matched.contains(opB)) {
-        continue;
+    for (Operation* opA : readyA) {
+      SetVector<Operation*>::iterator it = readyB.begin();
+      for (; it != readyB.end(); it = std::next(it)) {
+        Operation* opB = *it;
+        if (matched.contains(opB)) {
+          continue;
+        }
+
+        if (compareOperations(opA, opB, m)) {
+          matched.insert(opB);
+          mapResults(opA, opB, m);
+          m.map(opA, opB);
+          break;
+        }
       }
 
-      if (compareOperations(opA, opB, m)) {
-        matched.insert(opB);
-        mapResults(opA, opB, m);
-        m.map(opA, opB);
-        break;
+      if (it == readyB.end()) {
+        llvm::dbgs() << "unmatched op a: " << *opA << '\n';
+        return false;
       }
     }
 
-    if (it == readyB.end()) {
-      llvm::dbgs() << "unmatched op a: " << *opA << '\n';
-      return false;
-    }
-  }
+    // At this point, we've successfully matched each operation on the lhs with
+    // one on the rhs.
+
+    closed.insert_range(readyA);
+    closed.insert_range(readyB);
+
+    SetVector<Operation*>::iterator it = readyA.begin();
+    for (; it != readyA.end(); it = std::next(it)) {
+      Operation* opA = *it;
+
+      // Otherwise, if opA has one or more regions, try each mapping to find the
+      // equivalent operation. Each mapping uniquely identify opA with one
+      // potential partner thus use the mapping to obtain this partner and
+      // compare their respective regions.
 
-  // At this point, we've successfully matched each operation on the lhs with
-  // one on the rhs.
-
-  closed.insert_range(readyA);
-  closed.insert_range(readyB);
-
-  SetVector<Operation*>::iterator it = readyA.begin();
-  for (; it != readyA.end(); it = std::next(it)) {
-    Operation* opA = *it;
-
-    // Otherwise, if opA has one or more regions, try each mapping to find the
-    // equivalent operation. Each mapping uniquely identify opA with one
-    // potential partner thus use the mapping to obtain this partner and
-    // compare their respective regions.
-
-    if (opA->getNumRegions() > 0) {
-      Operation* opB = m.lookup(opA);
-      assert(opA->getNumRegions() == opB->getNumRegions());
-
-      const auto nequiv = range_size(make_filter_range(
-          llvm::zip_equal(opA->getRegions(), opB->getRegions()),
-          [&](const auto& zip) {
-            const auto& [regionA, regionB] = zip;
-            return compareRegions(regionA, regionB, closed, m);
-          }));
-      if (nequiv != opA->getNumRegions()) {
-        break;
+      if (opA->getNumRegions() > 0) {
+        Operation* opB = m.lookup(opA);
+        assert(opA->getNumRegions() == opB->getNumRegions());
+
+        const auto nequiv = range_size(make_filter_range(
+            llvm::zip_equal(opA->getRegions(), opB->getRegions()),
+            [&](const auto& zip) {
+              const auto& [regionA, regionB] = zip;
+              return compareRegions(regionA, regionB, closed, m);
+            }));
+        if (nequiv != opA->getNumRegions()) {
+          break;
+        }
       }
     }
-  }
 
-  if (it != readyA.end()) {
-    return false;
+    if (it != readyA.end()) {
+      return false;
+    }
   }
 
-  return compareTopologically(openA, openB, closed, m);
+  return true;
 }
 
 static bool compareBlocks(Block& blockA, Block& blockB,

From 8b03d8b78a2d47373ff8885ee53eb68ac7c61209 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 09:41:41 +0200
Subject: [PATCH 14/32] Minor clean up

---
 mlir/lib/Support/IRVerification.cpp | 96 +++++++----------------------
 1 file changed, 21 insertions(+), 75 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index d17f09d707..145d1e85cb 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -12,7 +12,6 @@
 
 #include "mlir/Dialect/QC/IR/QCOps.h"
 #include "mlir/Dialect/QCO/IR/QCODialect.h"
-#include "mlir/Dialect/QCO/IR/QCOOps.h"
 #include "mlir/Dialect/QTensor/Utils/TensorIterator.h"
 
 #include <llvm/ADT/STLExtras.h>
@@ -23,7 +22,6 @@
 #include <llvm/Support/ErrorHandling.h>
 #include <llvm/Support/raw_ostream.h>
 #include <mlir/Analysis/SliceAnalysis.h>
-#include <mlir/Dialect/Arith/IR/Arith.h>
 #include <mlir/Dialect/QTensor/IR/QTensorOps.h>
 #include <mlir/IR/Attributes.h>
 #include <mlir/IR/Block.h>
@@ -31,10 +29,8 @@
 #include <mlir/IR/BuiltinAttributes.h>
 #include <mlir/IR/BuiltinOps.h>
 #include <mlir/IR/IRMapping.h>
-#include <mlir/IR/OpDefinition.h>
 #include <mlir/IR/Operation.h>
 #include <mlir/IR/Region.h>
-#include <mlir/IR/SymbolTable.h>
 #include <mlir/IR/Value.h>
 #include <mlir/Support/LLVM.h>
 
@@ -106,64 +102,36 @@ static bool approxCompareFloats(const APFloat& lhs, const APFloat& rhs,
   return absDiff <= absTol + (relTol * scale);
 }
 
-static bool compareAttributes(const Attribute& attrA, const Attribute& attrB) {
-  if (dyn_cast<UnitAttr>(attrA)) {
-    if (!dyn_cast<UnitAttr>(attrB)) {
+/// Compare two attributes for equivality.
+/// Explicitly checks `UnitAttr`, `IntegerAttr`, `FloatAttr`, `StringAttr`, and
+/// `FlatSymbolRefAttr`.
+/// For any other type, the function simply returns true.
+static bool compareAttributes(Attribute attr, Attribute other) {
+  if (dyn_cast<UnitAttr>(attr)) {
+    if (!dyn_cast<UnitAttr>(other)) {
       return false;
     }
-  } else if (auto intAttrA = dyn_cast<IntegerAttr>(attrA)) {
-    auto intAttrB = dyn_cast<IntegerAttr>(attrB);
+  } else if (auto intAttrA = dyn_cast<IntegerAttr>(attr)) {
+    auto intAttrB = dyn_cast<IntegerAttr>(other);
     if (!intAttrB || intAttrA.getValue() != intAttrB.getValue()) {
       return false;
     }
-  } else if (auto floatAttrA = dyn_cast<FloatAttr>(attrA)) {
-    auto floatAttrB = dyn_cast<FloatAttr>(attrB);
+  } else if (auto floatAttrA = dyn_cast<FloatAttr>(attr)) {
+    auto floatAttrB = dyn_cast<FloatAttr>(other);
 
     if (!floatAttrB ||
         !approxCompareFloats(floatAttrA.getValue(), floatAttrB.getValue(),
                              floatAttrA.getType().getIntOrFloatBitWidth())) {
       return false;
     }
-  } else if (auto strAttrA = dyn_cast<StringAttr>(attrA)) {
-    auto strAttrB = dyn_cast<StringAttr>(attrB);
+  } else if (auto strAttrA = dyn_cast<StringAttr>(attr)) {
+    auto strAttrB = dyn_cast<StringAttr>(other);
     if (!strAttrB || strAttrA.getValue() != strAttrB.getValue()) {
       return false;
     }
-  } else if (auto arrayAttrA = dyn_cast<ArrayAttr>(attrA)) {
-    auto arrayAttrB = dyn_cast<ArrayAttr>(attrB);
-    if (!arrayAttrB) {
-      return false;
-    }
-
-    if (arrayAttrA.size() != arrayAttrB.size()) {
-      return false;
-    }
-
-    // Note: This assumes that the array attributes are equivalently ordered.
-    for (const auto [elementAttrA, elementAttrB] :
-         llvm::zip_equal(arrayAttrA, arrayAttrB)) {
-      if (!compareAttributes(elementAttrA, elementAttrB)) {
-        return false;
-      }
-    }
-  } else if (auto denseArrayAttrA =
-                 llvm::dyn_cast<mlir::DenseArrayAttr>(attrA)) {
-    auto denseArrayAttrB = llvm::dyn_cast<mlir::DenseArrayAttr>(attrB);
-    if (!denseArrayAttrB || denseArrayAttrA.size() != denseArrayAttrB.size() ||
-        denseArrayAttrA.getElementType() != denseArrayAttrB.getElementType()) {
-      return false;
-    }
-
-    for (const auto [valA, valB] : llvm::zip_equal(
-             denseArrayAttrA.getRawData(), denseArrayAttrB.getRawData())) {
-      if (valA != valB) {
-        return false;
-      }
-    }
-
   } else if (auto symbolRefAttrA =
-                 llvm::dyn_cast<mlir::FlatSymbolRefAttr>(attrA)) {
-    auto symbolRefAttrB = llvm::dyn_cast<mlir::FlatSymbolRefAttr>(attrB);
+                 llvm::dyn_cast<mlir::FlatSymbolRefAttr>(attr)) {
+    auto symbolRefAttrB = llvm::dyn_cast<mlir::FlatSymbolRefAttr>(other);
     if (!symbolRefAttrB) {
       return false;
     }
@@ -171,12 +139,6 @@ static bool compareAttributes(const Attribute& attrA, const Attribute& attrB) {
     if (symbolRefAttrA.getValue() != symbolRefAttrB.getValue()) {
       return false;
     }
-  } else {
-    // attrA.dump();
-    // llvm::dbgs() << "unhandled attribute type!\n";
-    // attrA.dump();
-    // llvm::reportFatalInternalError("unhandled attribute type!");
-    // llvm::llvm_unreachable_internal();
   }
 
   return true;
@@ -192,25 +154,16 @@ static bool compareOperations(Operation* opA, Operation* opB,
       opA->getOperandTypes() != opB->getOperandTypes() ||
       opA->getNumResults() != opB->getNumResults() ||
       opA->getResultTypes() != opB->getResultTypes() ||
-      // opA->getAttrs().size() != opB->getAttrs().size() ||
       opA->getNumRegions() != opB->getNumRegions()) {
     return false;
   }
 
-  // Compare attributes.
-
-  const DenseSet<StringRef> ignore{"passthrough"};
+  // Compare attributes with specific types.
+  // Silently ignore missing ones.
 
   for (const auto& namedAttrA : opA->getAttrs()) {
     const StringRef keyA = namedAttrA.getName().strref();
-
-    if (ignore.contains(keyA)) {
-      llvm::dbgs() << "ignoring: " << keyA << '\n';
-      continue;
-    }
-
     if (!opB->hasAttr(keyA)) {
-      llvm::dbgs() << "missing attribute: " << keyA << '\n';
       continue;
     }
 
@@ -220,15 +173,8 @@ static bool compareOperations(Operation* opA, Operation* opB,
   }
 
   // Compare operands.
-  // TODO: Equal type check.
-
-  // else if (isa<qco::CtrlOp>(opA)) {
-  //   assert(isa<qco::CtrlOp>(opB));
-  //   llvm::reportFatalInternalError("not implemented");
-  // } else if (opA->hasTrait<mlir::OpTrait::IsCommutative>()) {
-  //   assert(opB->hasTrait<mlir::OpTrait::IsCommutative>());
-  //   llvm::reportFatalInternalError("not implemented");
-  // }
+  // Because the order of target (control) qubits of CtrlOps doesn't matter,
+  // explicitly handle them here.
 
   if (isa<qc::CtrlOp>(opA)) {
     assert(isa<qc::CtrlOp>(opB));
@@ -283,8 +229,8 @@ static bool compareOperations(Operation* opA, Operation* opB,
           --itB;
         }
 
-        if (itA.operation() == nullptr) { // Block-Argument.
-          if (itB.operation() != nullptr) {
+        if (isa<BlockArgument>(itA.tensor())) {
+          if (isa<BlockArgument>(itB.tensor())) {
             return false;
           }
         } else {

From 595b4bbf86c34ab6a4abc3c4032ed1d8e401dec3 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 10:20:49 +0200
Subject: [PATCH 15/32] Implement missing FromElements logic

---
 mlir/lib/Support/IRVerification.cpp | 55 +++++++++++++++++++----------
 1 file changed, 36 insertions(+), 19 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index 145d1e85cb..5ee8bfce64 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -19,6 +19,7 @@
 #include <llvm/ADT/StringRef.h>
 #include <llvm/Support/Casting.h>
 #include <llvm/Support/Debug.h>
+#include <llvm/Support/Error.h>
 #include <llvm/Support/ErrorHandling.h>
 #include <llvm/Support/raw_ostream.h>
 #include <mlir/Analysis/SliceAnalysis.h>
@@ -57,17 +58,13 @@ static bool hasTypeQubitTensor(Value v) {
 /// Assumes `op->getNumResults() == other->getNumResults()`.
 /// Assumes that the two operations are equivalent to each other.
 static void mapResults(Operation* opL, Operation* opR, IRMapping& m) {
-  if (opL->getNumResults() == 0) {
-    return;
-  }
-
   for (const auto& [fromResult, toResult] :
        llvm::zip_equal(opL->getResults(), opR->getResults())) {
-    if (!isa<qtensor::AllocOp>(opL) && hasTypeQubitTensor(fromResult)) {
+    if (!isa<qtensor::AllocOp>(opL) && !isa<qtensor::FromElementsOp>(opL) &&
+        hasTypeQubitTensor(fromResult)) {
       assert(hasTypeQubitTensor(toResult));
       continue;
     }
-
     m.map(fromResult, toResult);
   }
 }
@@ -213,9 +210,7 @@ static bool compareOperations(Operation* opA, Operation* opB,
          llvm::zip_equal(opA->getOperands(), opB->getOperands())) {
 
       if (hasTypeQubitTensor(operandA)) {
-        if (!hasTypeQubitTensor(operandB)) { // TODO: Assertion?
-          return false;
-        }
+        assert(hasTypeQubitTensor(operandB));
 
         auto tensorA = cast<TypedValue<RankedTensorType>>(operandA);
         qtensor::TensorIterator itA(tensorA);
@@ -230,15 +225,33 @@ static bool compareOperations(Operation* opA, Operation* opB,
         }
 
         if (isa<BlockArgument>(itA.tensor())) {
-          if (isa<BlockArgument>(itB.tensor())) {
+          if (!isa<BlockArgument>(itB.tensor())) {
             return false;
           }
-        } else {
+        } else if (isa<qtensor::AllocOp>(itA.operation())) {
+          if (!isa<qtensor::AllocOp>(itB.operation())) {
+            return false;
+          }
+
           auto allocA = cast<qtensor::AllocOp>(itA.operation());
           auto allocB = cast<qtensor::AllocOp>(itB.operation());
+
           if (m.lookup(allocA.getResult()) != allocB.getResult()) {
             return false;
           }
+        } else if (isa<qtensor::FromElementsOp>(itA.operation())) {
+          if (!isa<qtensor::FromElementsOp>(itB.operation())) {
+            return false;
+          }
+
+          auto fromA = cast<qtensor::FromElementsOp>(itA.operation());
+          auto fromB = cast<qtensor::FromElementsOp>(itB.operation());
+
+          if (m.lookup(fromA.getResult()) != fromB.getResult()) {
+            return false;
+          }
+        } else {
+          llvm::reportFatalInternalError("unhandled qtensor source");
         }
       } else {
         auto operand = m.lookup(operandA);
@@ -317,17 +330,21 @@ static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> open,
     } else if (auto dealloc = dyn_cast<qtensor::DeallocOp>(op)) {
 
       // Deallocations are ready whenever we've visited each op on the tensor
-      // chain.
+      // chain. Because we initialize the iterator with its input tensor, the
+      // iterator already points at the previous operation. Thus use a do-while
+      // loop instead of a regular while.
 
       bool fullChain{true};
       qtensor::TensorIterator it(dealloc.getTensor());
 
-      for (; std::prev(it) != it; --it) {
+      do {
         if (!closed.contains(it.operation())) {
           fullChain = false;
           break;
         }
-      }
+
+        --it;
+      } while (std::prev(it) != it);
 
       if (fullChain) {
         ready.insert(dealloc);
@@ -363,9 +380,8 @@ static bool compareTopologically(ArrayRef<Operation*> openA,
     }
 
     // Because there may be multiple structural equivalent operations (think
-    // arith.constant, for example), collect them in a vector for further
-    // recursive processing. If there are no partners, no matching operation has
-    // been found and the blocks are not equivalent.
+    // arith.constant, for example), we apply the assumption that the first
+    // occurence on the lhs corresponds to the first occurence on the rhs, etc.
 
     DenseSet<Operation*> matched;
     matched.reserve(readyB.size());
@@ -374,6 +390,7 @@ static bool compareTopologically(ArrayRef<Operation*> openA,
       SetVector<Operation*>::iterator it = readyB.begin();
       for (; it != readyB.end(); it = std::next(it)) {
         Operation* opB = *it;
+
         if (matched.contains(opB)) {
           continue;
         }
@@ -387,7 +404,6 @@ static bool compareTopologically(ArrayRef<Operation*> openA,
       }
 
       if (it == readyB.end()) {
-        llvm::dbgs() << "unmatched op a: " << *opA << '\n';
         return false;
       }
     }
@@ -440,7 +456,6 @@ static bool compareBlocks(Block& blockA, Block& blockB,
   for (const auto [lArg, rArg] :
        llvm::zip_equal(blockA.getArguments(), blockB.getArguments())) {
     if (lArg.getType() != rArg.getType()) {
-      llvm::dbgs() << "nonequivalent block arguments\n";
       return false;
     }
 
@@ -470,6 +485,8 @@ static bool compareRegions(Region& regionA, Region& regionB,
     if (!compareBlocks(blockA, blockB, closed, m)) {
       return false;
     }
+
+    m.map(&blockA, &blockB);
   }
 
   return true;

From cb2e54533bee33afb1f945cfe7ce6e86c62d2d9c Mon Sep 17 00:00:00 2001
From: "pre-commit-ci[bot]"
 <66853113+pre-commit-ci[bot]@users.noreply.github.com>
Date: Fri, 12 Jun 2026 08:21:28 +0000
Subject: [PATCH 16/32] =?UTF-8?q?=F0=9F=8E=A8=20pre-commit=20fixes?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 mlir/lib/Support/IRVerification.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index 5ee8bfce64..e70f3e7511 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -381,7 +381,8 @@ static bool compareTopologically(ArrayRef<Operation*> openA,
 
     // Because there may be multiple structural equivalent operations (think
     // arith.constant, for example), we apply the assumption that the first
-    // occurence on the lhs corresponds to the first occurence on the rhs, etc.
+    // occurrence on the lhs corresponds to the first occurrence on the rhs,
+    // etc.
 
     DenseSet<Operation*> matched;
     matched.reserve(readyB.size());

From 0ba265c071e6342829c5dd8bc8b63043caa16f25 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 10:34:17 +0200
Subject: [PATCH 17/32] Use lhs/rhs

---
 mlir/lib/Support/IRVerification.cpp | 202 ++++++++++++++--------------
 1 file changed, 101 insertions(+), 101 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index e70f3e7511..647aca728b 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -41,7 +41,7 @@
 
 using namespace mlir;
 
-static bool compareRegions(Region& regionA, Region& regionB,
+static bool compareRegions(Region& lhs, Region& rhs,
                            DenseSet<Operation*>& closed, IRMapping& m);
 
 /// Return true, if the given value has the type `tensor<qco.qubit>`.
@@ -55,12 +55,12 @@ static bool hasTypeQubitTensor(Value v) {
 }
 
 /// Map all results from one op to another.
-/// Assumes `op->getNumResults() == other->getNumResults()`.
+/// Assumes `lhs->getNumResults() == rhs->getNumResults()`.
 /// Assumes that the two operations are equivalent to each other.
-static void mapResults(Operation* opL, Operation* opR, IRMapping& m) {
+static void mapResults(Operation* lhs, Operation* rhs, IRMapping& m) {
   for (const auto& [fromResult, toResult] :
-       llvm::zip_equal(opL->getResults(), opR->getResults())) {
-    if (!isa<qtensor::AllocOp>(opL) && !isa<qtensor::FromElementsOp>(opL) &&
+       llvm::zip_equal(lhs->getResults(), rhs->getResults())) {
+    if (!isa<qtensor::AllocOp>(lhs) && !isa<qtensor::FromElementsOp>(lhs) &&
         hasTypeQubitTensor(fromResult)) {
       assert(hasTypeQubitTensor(toResult));
       continue;
@@ -141,30 +141,30 @@ static bool compareAttributes(Attribute attr, Attribute other) {
   return true;
 }
 
-static bool compareOperations(Operation* opA, Operation* opB,
+static bool compareOperations(Operation* lhs, Operation* rhs,
                               const IRMapping& m) {
 
   // Compare top-level signature-like characteristics.
 
-  if (opA->getName() != opB->getName() ||
-      opA->getNumOperands() != opB->getNumOperands() ||
-      opA->getOperandTypes() != opB->getOperandTypes() ||
-      opA->getNumResults() != opB->getNumResults() ||
-      opA->getResultTypes() != opB->getResultTypes() ||
-      opA->getNumRegions() != opB->getNumRegions()) {
+  if (lhs->getName() != rhs->getName() ||
+      lhs->getNumOperands() != rhs->getNumOperands() ||
+      lhs->getOperandTypes() != rhs->getOperandTypes() ||
+      lhs->getNumResults() != rhs->getNumResults() ||
+      lhs->getResultTypes() != rhs->getResultTypes() ||
+      lhs->getNumRegions() != rhs->getNumRegions()) {
     return false;
   }
 
   // Compare attributes with specific types.
   // Silently ignore missing ones.
 
-  for (const auto& namedAttrA : opA->getAttrs()) {
-    const StringRef keyA = namedAttrA.getName().strref();
-    if (!opB->hasAttr(keyA)) {
+  for (const auto& namedAttrLhs : lhs->getAttrs()) {
+    const StringRef keyLhs = namedAttrLhs.getName().strref();
+    if (!rhs->hasAttr(keyLhs)) {
       continue;
     }
 
-    if (!compareAttributes(namedAttrA.getValue(), opB->getAttr(keyA))) {
+    if (!compareAttributes(namedAttrLhs.getValue(), rhs->getAttr(keyLhs))) {
       return false;
     }
   }
@@ -173,15 +173,15 @@ static bool compareOperations(Operation* opA, Operation* opB,
   // Because the order of target (control) qubits of CtrlOps doesn't matter,
   // explicitly handle them here.
 
-  if (isa<qc::CtrlOp>(opA)) {
-    assert(isa<qc::CtrlOp>(opB));
+  if (isa<qc::CtrlOp>(lhs)) {
+    assert(isa<qc::CtrlOp>(rhs));
 
-    auto ctrlL = cast<qc::CtrlOp>(opA);
-    auto ctrlR = cast<qc::CtrlOp>(opB);
+    auto ctrlLhs = cast<qc::CtrlOp>(lhs);
+    auto ctrlRhs = cast<qc::CtrlOp>(rhs);
 
     DenseSet<Value> workset;
-    workset.insert_range(ctrlR.getControls());
-    for (const auto& ctrl : ctrlL.getControls()) {
+    workset.insert_range(ctrlRhs.getControls());
+    for (const auto& ctrl : ctrlLhs.getControls()) {
       const auto& mapped = m.lookup(ctrl);
       if (!workset.contains(mapped)) {
         return false;
@@ -194,8 +194,8 @@ static bool compareOperations(Operation* opA, Operation* opB,
     // Analogously for the targets.
 
     workset.clear();
-    workset.insert_range(ctrlR.getTargets());
-    for (const auto& trgt : ctrlL.getTargets()) {
+    workset.insert_range(ctrlRhs.getTargets());
+    for (const auto& trgt : ctrlLhs.getTargets()) {
       const auto& operand = m.lookup(trgt);
       if (!workset.contains(operand)) {
         return false;
@@ -206,56 +206,56 @@ static bool compareOperations(Operation* opA, Operation* opB,
     assert(workset.empty());
 
   } else {
-    for (const auto& [operandA, operandB] :
-         llvm::zip_equal(opA->getOperands(), opB->getOperands())) {
+    for (const auto& [operandLhs, operandRhs] :
+         llvm::zip_equal(lhs->getOperands(), rhs->getOperands())) {
 
-      if (hasTypeQubitTensor(operandA)) {
-        assert(hasTypeQubitTensor(operandB));
+      if (hasTypeQubitTensor(operandLhs)) {
+        assert(hasTypeQubitTensor(operandRhs));
 
-        auto tensorA = cast<TypedValue<RankedTensorType>>(operandA);
-        qtensor::TensorIterator itA(tensorA);
-        while (std::prev(itA) != itA) {
-          --itA;
+        auto tensorLhs = cast<TypedValue<RankedTensorType>>(operandLhs);
+        qtensor::TensorIterator itLhs(tensorLhs);
+        while (std::prev(itLhs) != itLhs) {
+          --itLhs;
         }
 
-        auto tensorB = cast<TypedValue<RankedTensorType>>(operandB);
-        qtensor::TensorIterator itB(tensorB);
-        while (std::prev(itB) != itB) {
-          --itB;
+        auto tensorRhs = cast<TypedValue<RankedTensorType>>(operandRhs);
+        qtensor::TensorIterator itRhs(tensorRhs);
+        while (std::prev(itRhs) != itRhs) {
+          --itRhs;
         }
 
-        if (isa<BlockArgument>(itA.tensor())) {
-          if (!isa<BlockArgument>(itB.tensor())) {
+        if (isa<BlockArgument>(itLhs.tensor())) {
+          if (!isa<BlockArgument>(itRhs.tensor())) {
             return false;
           }
-        } else if (isa<qtensor::AllocOp>(itA.operation())) {
-          if (!isa<qtensor::AllocOp>(itB.operation())) {
+        } else if (isa<qtensor::AllocOp>(itLhs.operation())) {
+          if (!isa<qtensor::AllocOp>(itRhs.operation())) {
             return false;
           }
 
-          auto allocA = cast<qtensor::AllocOp>(itA.operation());
-          auto allocB = cast<qtensor::AllocOp>(itB.operation());
+          auto allocLhs = cast<qtensor::AllocOp>(itLhs.operation());
+          auto allocRhs = cast<qtensor::AllocOp>(itRhs.operation());
 
-          if (m.lookup(allocA.getResult()) != allocB.getResult()) {
+          if (m.lookup(allocLhs.getResult()) != allocRhs.getResult()) {
             return false;
           }
-        } else if (isa<qtensor::FromElementsOp>(itA.operation())) {
-          if (!isa<qtensor::FromElementsOp>(itB.operation())) {
+        } else if (isa<qtensor::FromElementsOp>(itLhs.operation())) {
+          if (!isa<qtensor::FromElementsOp>(itRhs.operation())) {
             return false;
           }
 
-          auto fromA = cast<qtensor::FromElementsOp>(itA.operation());
-          auto fromB = cast<qtensor::FromElementsOp>(itB.operation());
+          auto fromLhs = cast<qtensor::FromElementsOp>(itLhs.operation());
+          auto fromRhs = cast<qtensor::FromElementsOp>(itRhs.operation());
 
-          if (m.lookup(fromA.getResult()) != fromB.getResult()) {
+          if (m.lookup(fromLhs.getResult()) != fromRhs.getResult()) {
             return false;
           }
         } else {
           llvm::reportFatalInternalError("unhandled qtensor source");
         }
       } else {
-        auto operand = m.lookup(operandA);
-        if (operand != operandB) {
+        auto operand = m.lookup(operandLhs);
+        if (operand != operandRhs) {
           return false;
         }
       }
@@ -363,19 +363,19 @@ static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> open,
   return ready;
 }
 
-static bool compareTopologically(ArrayRef<Operation*> openA,
-                                 ArrayRef<Operation*> openB,
+static bool compareTopologically(ArrayRef<Operation*> lhsOps,
+                                 ArrayRef<Operation*> rhsOps,
                                  DenseSet<Operation*>& closed, IRMapping& m) {
 
   while (true) {
-    const auto readyA = getReadyOps(openA, closed);
-    const auto readyB = getReadyOps(openB, closed);
+    const auto readyLhs = getReadyOps(lhsOps, closed);
+    const auto readyRhs = getReadyOps(rhsOps, closed);
 
-    if (readyA.empty() && readyB.empty()) {
+    if (readyLhs.empty() && readyRhs.empty()) {
       break;
     }
 
-    if (readyA.size() != readyB.size()) {
+    if (readyLhs.size() != readyRhs.size()) {
       return false;
     }
 
@@ -385,26 +385,26 @@ static bool compareTopologically(ArrayRef<Operation*> openA,
     // etc.
 
     DenseSet<Operation*> matched;
-    matched.reserve(readyB.size());
+    matched.reserve(readyRhs.size());
 
-    for (Operation* opA : readyA) {
-      SetVector<Operation*>::iterator it = readyB.begin();
-      for (; it != readyB.end(); it = std::next(it)) {
-        Operation* opB = *it;
+    for (Operation* opLhs : readyLhs) {
+      SetVector<Operation*>::iterator it = readyRhs.begin();
+      for (; it != readyRhs.end(); it = std::next(it)) {
+        Operation* opRhs = *it;
 
-        if (matched.contains(opB)) {
+        if (matched.contains(opRhs)) {
           continue;
         }
 
-        if (compareOperations(opA, opB, m)) {
-          matched.insert(opB);
-          mapResults(opA, opB, m);
-          m.map(opA, opB);
+        if (compareOperations(opLhs, opRhs, m)) {
+          matched.insert(opRhs);
+          mapResults(opLhs, opRhs, m);
+          m.map(opLhs, opRhs);
           break;
         }
       }
 
-      if (it == readyB.end()) {
+      if (it == readyRhs.end()) {
         return false;
       }
     }
@@ -412,35 +412,35 @@ static bool compareTopologically(ArrayRef<Operation*> openA,
     // At this point, we've successfully matched each operation on the lhs with
     // one on the rhs.
 
-    closed.insert_range(readyA);
-    closed.insert_range(readyB);
+    closed.insert_range(readyLhs);
+    closed.insert_range(readyRhs);
 
-    SetVector<Operation*>::iterator it = readyA.begin();
-    for (; it != readyA.end(); it = std::next(it)) {
-      Operation* opA = *it;
+    SetVector<Operation*>::iterator it = readyLhs.begin();
+    for (; it != readyLhs.end(); it = std::next(it)) {
+      Operation* opLhs = *it;
 
-      // Otherwise, if opA has one or more regions, try each mapping to find the
-      // equivalent operation. Each mapping uniquely identify opA with one
+      // Otherwise, if opLhs has one or more regions, try each mapping to find
+      // the equivalent operation. Each mapping uniquely identify opLhs with one
       // potential partner thus use the mapping to obtain this partner and
       // compare their respective regions.
 
-      if (opA->getNumRegions() > 0) {
-        Operation* opB = m.lookup(opA);
-        assert(opA->getNumRegions() == opB->getNumRegions());
+      if (opLhs->getNumRegions() > 0) {
+        Operation* opRhs = m.lookup(opLhs);
+        assert(opLhs->getNumRegions() == opRhs->getNumRegions());
 
         const auto nequiv = range_size(make_filter_range(
-            llvm::zip_equal(opA->getRegions(), opB->getRegions()),
+            llvm::zip_equal(opLhs->getRegions(), opRhs->getRegions()),
             [&](const auto& zip) {
-              const auto& [regionA, regionB] = zip;
-              return compareRegions(regionA, regionB, closed, m);
+              const auto& [regionLhs, regionRhs] = zip;
+              return compareRegions(regionLhs, regionRhs, closed, m);
             }));
-        if (nequiv != opA->getNumRegions()) {
+        if (nequiv != opLhs->getNumRegions()) {
           break;
         }
       }
     }
 
-    if (it != readyA.end()) {
+    if (it != readyLhs.end()) {
       return false;
     }
   }
@@ -448,46 +448,46 @@ static bool compareTopologically(ArrayRef<Operation*> openA,
   return true;
 }
 
-static bool compareBlocks(Block& blockA, Block& blockB,
-                          DenseSet<Operation*>& closed, IRMapping& m) {
-  if (blockA.getNumArguments() != blockB.getNumArguments()) {
+static bool compareBlocks(Block& lhs, Block& rhs, DenseSet<Operation*>& closed,
+                          IRMapping& m) {
+  if (lhs.getNumArguments() != rhs.getNumArguments()) {
     return false;
   }
 
-  for (const auto [lArg, rArg] :
-       llvm::zip_equal(blockA.getArguments(), blockB.getArguments())) {
-    if (lArg.getType() != rArg.getType()) {
+  for (const auto [lhsArg, rhsArg] :
+       llvm::zip_equal(lhs.getArguments(), rhs.getArguments())) {
+    if (lhsArg.getType() != rhsArg.getType()) {
       return false;
     }
 
-    m.map(lArg, rArg);
+    m.map(lhsArg, rhsArg);
   }
 
-  SmallVector<Operation*> openA;
-  SmallVector<Operation*> openB;
+  SmallVector<Operation*> lhsOps;
+  SmallVector<Operation*> rhsOps;
 
-  openA.reserve(range_size(blockA.getOperations()));
-  openB.reserve(range_size(blockB.getOperations()));
+  lhsOps.reserve(range_size(lhs.getOperations()));
+  rhsOps.reserve(range_size(rhs.getOperations()));
 
-  for_each(blockA.getOperations(), [&](auto& op) { openA.emplace_back(&op); });
-  for_each(blockB.getOperations(), [&](auto& op) { openB.emplace_back(&op); });
+  for_each(lhs.getOperations(), [&](auto& op) { lhsOps.emplace_back(&op); });
+  for_each(rhs.getOperations(), [&](auto& op) { rhsOps.emplace_back(&op); });
 
-  return compareTopologically(openA, openB, closed, m);
+  return compareTopologically(lhsOps, rhsOps, closed, m);
 }
 
 /// Compare two regions for structural equivalence.
-static bool compareRegions(Region& regionA, Region& regionB,
+static bool compareRegions(Region& lhs, Region& rhs,
                            DenseSet<Operation*>& closed, IRMapping& m) {
-  if (regionA.getBlocks().size() != regionB.getBlocks().size()) {
+  if (lhs.getBlocks().size() != rhs.getBlocks().size()) {
     return false;
   }
 
-  for (const auto [blockA, blockB] : llvm::zip_equal(regionA, regionB)) {
-    if (!compareBlocks(blockA, blockB, closed, m)) {
+  for (const auto [lhsBlock, rhsBlock] : llvm::zip_equal(lhs, rhs)) {
+    if (!compareBlocks(lhsBlock, rhsBlock, closed, m)) {
       return false;
     }
 
-    m.map(&blockA, &blockB);
+    m.map(&lhsBlock, &rhsBlock);
   }
 
   return true;

From 569f33850c9098cfb87c22e3fab64ea49b27fa18 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 10:34:59 +0200
Subject: [PATCH 18/32] Remove unused imports

---
 mlir/lib/Support/IRVerification.cpp | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index 647aca728b..b8d4e33d14 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -18,10 +18,7 @@
 #include <llvm/ADT/SmallVector.h>
 #include <llvm/ADT/StringRef.h>
 #include <llvm/Support/Casting.h>
-#include <llvm/Support/Debug.h>
-#include <llvm/Support/Error.h>
 #include <llvm/Support/ErrorHandling.h>
-#include <llvm/Support/raw_ostream.h>
 #include <mlir/Analysis/SliceAnalysis.h>
 #include <mlir/Dialect/QTensor/IR/QTensorOps.h>
 #include <mlir/IR/Attributes.h>

From 4eaa06a08919f39fa1b005dd9f36c11487d2c4b1 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 11:11:33 +0200
Subject: [PATCH 19/32] Split closed set

---
 mlir/lib/Support/IRVerification.cpp | 144 ++++++++++++++--------------
 1 file changed, 72 insertions(+), 72 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index b8d4e33d14..e60038575c 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -39,7 +39,8 @@
 using namespace mlir;
 
 static bool compareRegions(Region& lhs, Region& rhs,
-                           DenseSet<Operation*>& closed, IRMapping& m);
+                           SetVector<Operation*>& lhsClosed,
+                           SetVector<Operation*>& rhsClosed, IRMapping& m);
 
 /// Return true, if the given value has the type `tensor<qco.qubit>`.
 static bool hasTypeQubitTensor(Value v) {
@@ -52,7 +53,7 @@ static bool hasTypeQubitTensor(Value v) {
 }
 
 /// Map all results from one op to another.
-/// Assumes `lhs->getNumResults() == rhs->getNumResults()`.
+/// Assumes that `lhs->getNumResults() == rhs->getNumResults()`.
 /// Assumes that the two operations are equivalent to each other.
 static void mapResults(Operation* lhs, Operation* rhs, IRMapping& m) {
   for (const auto& [fromResult, toResult] :
@@ -100,32 +101,32 @@ static bool approxCompareFloats(const APFloat& lhs, const APFloat& rhs,
 /// Explicitly checks `UnitAttr`, `IntegerAttr`, `FloatAttr`, `StringAttr`, and
 /// `FlatSymbolRefAttr`.
 /// For any other type, the function simply returns true.
-static bool compareAttributes(Attribute attr, Attribute other) {
-  if (dyn_cast<UnitAttr>(attr)) {
-    if (!dyn_cast<UnitAttr>(other)) {
+static bool compareAttributes(Attribute lhs, Attribute rhs) {
+  if (dyn_cast<UnitAttr>(lhs)) {
+    if (!dyn_cast<UnitAttr>(rhs)) {
       return false;
     }
-  } else if (auto intAttrA = dyn_cast<IntegerAttr>(attr)) {
-    auto intAttrB = dyn_cast<IntegerAttr>(other);
+  } else if (auto intAttrA = dyn_cast<IntegerAttr>(lhs)) {
+    auto intAttrB = dyn_cast<IntegerAttr>(rhs);
     if (!intAttrB || intAttrA.getValue() != intAttrB.getValue()) {
       return false;
     }
-  } else if (auto floatAttrA = dyn_cast<FloatAttr>(attr)) {
-    auto floatAttrB = dyn_cast<FloatAttr>(other);
+  } else if (auto floatAttrA = dyn_cast<FloatAttr>(lhs)) {
+    auto floatAttrB = dyn_cast<FloatAttr>(rhs);
 
     if (!floatAttrB ||
         !approxCompareFloats(floatAttrA.getValue(), floatAttrB.getValue(),
                              floatAttrA.getType().getIntOrFloatBitWidth())) {
       return false;
     }
-  } else if (auto strAttrA = dyn_cast<StringAttr>(attr)) {
-    auto strAttrB = dyn_cast<StringAttr>(other);
+  } else if (auto strAttrA = dyn_cast<StringAttr>(lhs)) {
+    auto strAttrB = dyn_cast<StringAttr>(rhs);
     if (!strAttrB || strAttrA.getValue() != strAttrB.getValue()) {
       return false;
     }
   } else if (auto symbolRefAttrA =
-                 llvm::dyn_cast<mlir::FlatSymbolRefAttr>(attr)) {
-    auto symbolRefAttrB = llvm::dyn_cast<mlir::FlatSymbolRefAttr>(other);
+                 llvm::dyn_cast<mlir::FlatSymbolRefAttr>(lhs)) {
+    auto symbolRefAttrB = llvm::dyn_cast<mlir::FlatSymbolRefAttr>(rhs);
     if (!symbolRefAttrB) {
       return false;
     }
@@ -138,6 +139,8 @@ static bool compareAttributes(Attribute attr, Attribute other) {
   return true;
 }
 
+/// Compare two operations for structural equivalence, applying some special
+/// rules for `CtrlOp` s and `qtensor` s.
 static bool compareOperations(Operation* lhs, Operation* rhs,
                               const IRMapping& m) {
 
@@ -264,8 +267,8 @@ static bool compareOperations(Operation* lhs, Operation* rhs,
 
 /// Extract and return "ready" operations.
 /// These are operations that are independent from each other.
-static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> open,
-                                         DenseSet<Operation*>& closed) {
+static SetVector<Operation*> getReadyOps(const SetVector<Operation*>& open,
+                                         const SetVector<Operation*>& closed) {
   const auto isReady = [&closed](Value v) {
     if (isa<BlockArgument>(v)) {
       return true;
@@ -360,33 +363,52 @@ static SetVector<Operation*> getReadyOps(ArrayRef<Operation*> open,
   return ready;
 }
 
-static bool compareTopologically(ArrayRef<Operation*> lhsOps,
-                                 ArrayRef<Operation*> rhsOps,
-                                 DenseSet<Operation*>& closed, IRMapping& m) {
+static bool compareBlocks(Block& lhs, Block& rhs,
+                          SetVector<Operation*>& lhsClosed,
+                          SetVector<Operation*>& rhsClosed, IRMapping& m) {
+  if (lhs.getNumArguments() != rhs.getNumArguments()) {
+    return false;
+  }
+
+  for (const auto [lhsArg, rhsArg] :
+       llvm::zip_equal(lhs.getArguments(), rhs.getArguments())) {
+    if (lhsArg.getType() != rhsArg.getType()) {
+      return false;
+    }
+
+    m.map(lhsArg, rhsArg);
+  }
+
+  SetVector<Operation*> lhsOpen;
+  SetVector<Operation*> rhsOpen;
+
+  for_each(lhs.getOperations(), [&](auto& op) { lhsOpen.insert(&op); });
+  for_each(rhs.getOperations(), [&](auto& op) { rhsOpen.insert(&op); });
+
+  // Compare block operations topologically.
 
   while (true) {
-    const auto readyLhs = getReadyOps(lhsOps, closed);
-    const auto readyRhs = getReadyOps(rhsOps, closed);
+    const auto lhsReady = getReadyOps(lhsOpen, lhsClosed);
+    const auto rhsReady = getReadyOps(rhsOpen, rhsClosed);
 
-    if (readyLhs.empty() && readyRhs.empty()) {
+    if (lhsReady.empty() && rhsReady.empty()) {
       break;
     }
 
-    if (readyLhs.size() != readyRhs.size()) {
+    if (lhsReady.size() != rhsReady.size()) {
       return false;
     }
 
     // Because there may be multiple structural equivalent operations (think
     // arith.constant, for example), we apply the assumption that the first
-    // occurrence on the lhs corresponds to the first occurrence on the rhs,
-    // etc.
+    // occurrence on the lhs corresponds to the first one on the rhs, etc.
 
     DenseSet<Operation*> matched;
-    matched.reserve(readyRhs.size());
+    matched.reserve(rhsReady.size());
 
-    for (Operation* opLhs : readyLhs) {
-      SetVector<Operation*>::iterator it = readyRhs.begin();
-      for (; it != readyRhs.end(); it = std::next(it)) {
+    for (Operation* opLhs : lhsReady) {
+      SetVector<Operation*>::iterator it = rhsReady.begin();
+      for (; it != rhsReady.end(); it = std::next(it)) {
         Operation* opRhs = *it;
 
         if (matched.contains(opRhs)) {
@@ -401,7 +423,7 @@ static bool compareTopologically(ArrayRef<Operation*> lhsOps,
         }
       }
 
-      if (it == readyRhs.end()) {
+      if (it == rhsReady.end()) {
         return false;
       }
     }
@@ -409,17 +431,18 @@ static bool compareTopologically(ArrayRef<Operation*> lhsOps,
     // At this point, we've successfully matched each operation on the lhs with
     // one on the rhs.
 
-    closed.insert_range(readyLhs);
-    closed.insert_range(readyRhs);
+    lhsOpen.set_subtract(lhsReady);
+    lhsClosed.set_union(lhsReady);
 
-    SetVector<Operation*>::iterator it = readyLhs.begin();
-    for (; it != readyLhs.end(); it = std::next(it)) {
-      Operation* opLhs = *it;
+    rhsOpen.set_subtract(rhsReady);
+    rhsClosed.set_union(rhsReady);
 
-      // Otherwise, if opLhs has one or more regions, try each mapping to find
-      // the equivalent operation. Each mapping uniquely identify opLhs with one
-      // potential partner thus use the mapping to obtain this partner and
-      // compare their respective regions.
+    // Once all ready operations have been matched, recursively compare
+    // the nested regions of each operation pair.
+
+    SetVector<Operation*>::iterator it = lhsReady.begin();
+    for (; it != lhsReady.end(); it = std::next(it)) {
+      Operation* opLhs = *it;
 
       if (opLhs->getNumRegions() > 0) {
         Operation* opRhs = m.lookup(opLhs);
@@ -428,8 +451,9 @@ static bool compareTopologically(ArrayRef<Operation*> lhsOps,
         const auto nequiv = range_size(make_filter_range(
             llvm::zip_equal(opLhs->getRegions(), opRhs->getRegions()),
             [&](const auto& zip) {
-              const auto& [regionLhs, regionRhs] = zip;
-              return compareRegions(regionLhs, regionRhs, closed, m);
+              const auto& [lhsRegion, rhsRegion] = zip;
+              return compareRegions(lhsRegion, rhsRegion, lhsClosed, rhsClosed,
+                                    m);
             }));
         if (nequiv != opLhs->getNumRegions()) {
           break;
@@ -437,7 +461,7 @@ static bool compareTopologically(ArrayRef<Operation*> lhsOps,
       }
     }
 
-    if (it != readyLhs.end()) {
+    if (it != lhsReady.end()) {
       return false;
     }
   }
@@ -445,42 +469,16 @@ static bool compareTopologically(ArrayRef<Operation*> lhsOps,
   return true;
 }
 
-static bool compareBlocks(Block& lhs, Block& rhs, DenseSet<Operation*>& closed,
-                          IRMapping& m) {
-  if (lhs.getNumArguments() != rhs.getNumArguments()) {
-    return false;
-  }
-
-  for (const auto [lhsArg, rhsArg] :
-       llvm::zip_equal(lhs.getArguments(), rhs.getArguments())) {
-    if (lhsArg.getType() != rhsArg.getType()) {
-      return false;
-    }
-
-    m.map(lhsArg, rhsArg);
-  }
-
-  SmallVector<Operation*> lhsOps;
-  SmallVector<Operation*> rhsOps;
-
-  lhsOps.reserve(range_size(lhs.getOperations()));
-  rhsOps.reserve(range_size(rhs.getOperations()));
-
-  for_each(lhs.getOperations(), [&](auto& op) { lhsOps.emplace_back(&op); });
-  for_each(rhs.getOperations(), [&](auto& op) { rhsOps.emplace_back(&op); });
-
-  return compareTopologically(lhsOps, rhsOps, closed, m);
-}
-
 /// Compare two regions for structural equivalence.
 static bool compareRegions(Region& lhs, Region& rhs,
-                           DenseSet<Operation*>& closed, IRMapping& m) {
+                           SetVector<Operation*>& lhsClosed,
+                           SetVector<Operation*>& rhsClosed, IRMapping& m) {
   if (lhs.getBlocks().size() != rhs.getBlocks().size()) {
     return false;
   }
 
   for (const auto [lhsBlock, rhsBlock] : llvm::zip_equal(lhs, rhs)) {
-    if (!compareBlocks(lhsBlock, rhsBlock, closed, m)) {
+    if (!compareBlocks(lhsBlock, rhsBlock, lhsClosed, rhsClosed, m)) {
       return false;
     }
 
@@ -492,6 +490,8 @@ static bool compareRegions(Region& lhs, Region& rhs,
 
 bool areModulesEquivalentWithPermutations(ModuleOp lhs, ModuleOp rhs) {
   IRMapping m;
-  DenseSet<Operation*> closed;
-  return compareRegions(lhs.getBodyRegion(), rhs.getBodyRegion(), closed, m);
+  SetVector<Operation*> lhsClosed;
+  SetVector<Operation*> rhsClosed;
+  return compareRegions(lhs.getBodyRegion(), rhs.getBodyRegion(), lhsClosed,
+                        rhsClosed, m);
 }

From c767ffd4007fe3af1e5e87d9871c4215644be9e9 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 11:15:38 +0200
Subject: [PATCH 20/32] Simplify if logic

---
 mlir/lib/Support/IRVerification.cpp | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index e60038575c..646e64b5f7 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -278,25 +278,24 @@ static SetVector<Operation*> getReadyOps(const SetVector<Operation*>& open,
 
   SetVector<Operation*> ready;
   for (Operation* op : open) {
-    if (closed.contains(op) || ready.contains(op)) {
+    if (ready.contains(op)) {
       continue;
     }
 
     if (auto insert = dyn_cast<qtensor::InsertOp>(op)) {
 
-      // If any of the inserts on the chain are ready, we consider the whole
-      // chain ready because the one ready operation could be moved the front
-      // (the top from IR perspective) of the chain.
-      // An insert is considered ready when both the inserted qubit and the
-      // index are ready.
+      // If any of the inserts on the chain are ready, we consider the entire
+      // chain ready because the ready operations could be moved to the front
+      // of the chain.
 
       SmallVector<Operation*> chain;
       qtensor::TensorIterator it(insert.getResult());
 
-      for (; it != std::default_sentinel &&
-             isa<qtensor::InsertOp>(it.operation());
-           ++it) {
-        auto chainInsert = cast<qtensor::InsertOp>(it.operation());
+      for (; it != std::default_sentinel; ++it) {
+        auto chainInsert = dyn_cast<qtensor::InsertOp>(it.operation());
+        if (!chainInsert) {
+          break;
+        }
         if (isReady(chainInsert.getScalar()) &&
             isReady(chainInsert.getIndex()) && !closed.contains(chainInsert)) {
           chain.emplace_back(chainInsert);
@@ -314,10 +313,12 @@ static SetVector<Operation*> getReadyOps(const SetVector<Operation*>& open,
       SmallVector<Operation*> chain;
       qtensor::TensorIterator it(extract.getOutTensor());
 
-      for (; it != std::default_sentinel &&
-             isa<qtensor::ExtractOp>(it.operation());
-           ++it) {
-        auto chainExtract = cast<qtensor::ExtractOp>(it.operation());
+      for (; it != std::default_sentinel; ++it) {
+        auto chainExtract = dyn_cast<qtensor::ExtractOp>(it.operation());
+        if (!chainExtract) {
+          break;
+        }
+
         if (isReady(chainExtract.getIndex()) &&
             !closed.contains(chainExtract)) {
           chain.emplace_back(chainExtract);

From 72c78a16c94f0860154e64a98718ec753ef8a3cd Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 12:47:31 +0200
Subject: [PATCH 21/32] Handle input permutations

---
 mlir/lib/Support/IRVerification.cpp | 45 +++++++++++++++++++++--------
 1 file changed, 33 insertions(+), 12 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index 646e64b5f7..afdae088e8 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -35,6 +35,7 @@
 #include <cassert>
 #include <cmath>
 #include <iterator>
+#include <numeric>
 
 using namespace mlir;
 
@@ -58,15 +59,21 @@ static bool hasTypeQubitTensor(Value v) {
 static void mapResults(Operation* lhs, Operation* rhs, IRMapping& m) {
   for (const auto& [fromResult, toResult] :
        llvm::zip_equal(lhs->getResults(), rhs->getResults())) {
-    if (!isa<qtensor::AllocOp>(lhs) && !isa<qtensor::FromElementsOp>(lhs) &&
-        hasTypeQubitTensor(fromResult)) {
-      assert(hasTypeQubitTensor(toResult));
-      continue;
-    }
     m.map(fromResult, toResult);
   }
 }
 
+/// Map arguments from one block to another using the given permutation.
+/// Assumes that `lhs.getNumArguments() == rhs.getNumArguments()`.
+/// Assumes that `permutation.size() == lhs.getNumArguments()`.
+static void mapArguments(Block& lhs, Block& rhs, ArrayRef<size_t> permutation,
+                         IRMapping& m) {
+  for (const auto& [i, lhsArg] : enumerate(lhs.getArguments())) {
+    BlockArgument rhsArg = rhs.getArgument(permutation[i]);
+    m.map(lhsArg, rhsArg);
+  }
+}
+
 /// Compares two floating point numbers for approximate equivalence.
 static bool approxCompareFloats(const APFloat& lhs, const APFloat& rhs,
                                 const unsigned width) {
@@ -371,13 +378,28 @@ static bool compareBlocks(Block& lhs, Block& rhs,
     return false;
   }
 
-  for (const auto [lhsArg, rhsArg] :
-       llvm::zip_equal(lhs.getArguments(), rhs.getArguments())) {
-    if (lhsArg.getType() != rhsArg.getType()) {
-      return false;
-    }
+  // Map block arguments.
+  // The targets of a `CtrlOp` are commutative, thus, find the permutation from
+  // the i-th argument of the lhs to the j-th argument of the rhs, before
+  // mapping the block arguments.
 
-    m.map(lhsArg, rhsArg);
+  if (isa<qc::CtrlOp>(lhs.getParentOp())) {
+    assert(isa<qc::CtrlOp>(rhs.getParentOp()));
+
+    auto lhsCtrl = cast<qc::CtrlOp>(lhs.getParentOp());
+    auto rhsCtrl = cast<qc::CtrlOp>(rhs.getParentOp());
+
+    SmallVector<size_t> permutation(lhs.getNumArguments());
+    for (const auto& [i, trgt] : llvm::enumerate(lhsCtrl.getTargets())) {
+      const auto it = llvm::find(rhsCtrl.getTargets(), m.lookup(trgt));
+      const auto j = std::distance(rhsCtrl.getTargets().begin(), it);
+      permutation[i] = j;
+    }
+    mapArguments(lhs, rhs, permutation, m);
+  } else {
+    SmallVector<size_t> permutation(lhs.getNumArguments());
+    std::iota(permutation.begin(), permutation.end(), 0);
+    mapArguments(lhs, rhs, permutation, m);
   }
 
   SetVector<Operation*> lhsOpen;
@@ -448,7 +470,6 @@ static bool compareBlocks(Block& lhs, Block& rhs,
       if (opLhs->getNumRegions() > 0) {
         Operation* opRhs = m.lookup(opLhs);
         assert(opLhs->getNumRegions() == opRhs->getNumRegions());
-
         const auto nequiv = range_size(make_filter_range(
             llvm::zip_equal(opLhs->getRegions(), opRhs->getRegions()),
             [&](const auto& zip) {

From 2bc52bb451c95a6dec3856e69dcaa9a6122136aa Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 12:54:53 +0200
Subject: [PATCH 22/32] Add missing include

---
 mlir/lib/Support/IRVerification.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index afdae088e8..4d5160db69 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -34,6 +34,7 @@
 
 #include <cassert>
 #include <cmath>
+#include <cstddef>
 #include <iterator>
 #include <numeric>
 

From b5ec7441705749c9d689f66a082ae90165cdcd31 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 13:09:02 +0200
Subject: [PATCH 23/32] Update CHANGELOG.md

---
 CHANGELOG.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a6f85bdb9e..ab841671d2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -18,7 +18,7 @@ This project adheres to [Semantic Versioning], with the exception that minor rel
 - ✨ Add conversions between `jeff` and QCO ([#1479], [#1548], [#1565], [#1637], [#1676], [#1706], [#1776]) ([**@denialhaag**], [**@burgholzer**])
 - ✨ Add a `place-and-route` pass for mapping circuits to architectures with restricted topologies ([#1537], [#1547], [#1568], [#1581], [#1583], [#1588], [#1600], [#1664], [#1709], [#1716], [#1748]) ([**@MatthiasReumann**], [**@burgholzer**])
 - ✨ Add initial infrastructure for new QC and QCO MLIR dialects
-  ([#1264], [#1330], [#1402], [#1428], [#1430], [#1436], [#1443], [#1446], [#1464], [#1465], [#1470], [#1471], [#1472], [#1474], [#1475], [#1506], [#1510], [#1513], [#1521], [#1542], [#1548], [#1550], [#1554], [#1567], [#1569], [#1570], [#1572], [#1573], [#1580], [#1602], [#1620], [#1623], [#1624], [#1626], [#1627], [#1635], [#1638], [#1673], [#1675], [#1700], [#1717], [#1728], [#1730], [#1749], [#1751], [#1762], [#1765], [#1774])
+  ([#1264], [#1330], [#1402], [#1428], [#1430], [#1436], [#1443], [#1446], [#1464], [#1465], [#1470], [#1471], [#1472], [#1474], [#1475], [#1506], [#1510], [#1513], [#1521], [#1542], [#1548], [#1550], [#1554], [#1567], [#1569], [#1570], [#1572], [#1573], [#1580], [#1602], [#1620], [#1623], [#1624], [#1626], [#1627], [#1635], [#1638], [#1673], [#1675], [#1700], [#1717], [#1728], [#1730], [#1749], [#1751], [#1762], [#1765], [#1774], [#1781])
   ([**@burgholzer**], [**@denialhaag**], [**@taminob**], [**@DRovara**], [**@li-mingbao**], [**@Ectras**], [**@MatthiasReumann**], [**@simon1hofmann**])
 
 ### Changed
@@ -402,6 +402,7 @@ _📚 Refer to the [GitHub Release Notes](https://github.com/munich-quantum-tool
 
 <!-- PR links -->
 
+[#1781]: https://github.com/munich-quantum-toolkit/core/pull/1781
 [#1776]: https://github.com/munich-quantum-toolkit/core/pull/1776
 [#1774]: https://github.com/munich-quantum-toolkit/core/pull/1774
 [#1765]: https://github.com/munich-quantum-toolkit/core/pull/1765

From 7a9e62d8bb323b1ac4775dfcd471fb7055d711be Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 13:09:13 +0200
Subject: [PATCH 24/32] Add result permutations

---
 mlir/lib/Support/IRVerification.cpp | 100 +++++++++++++++++++---------
 1 file changed, 68 insertions(+), 32 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index 4d5160db69..ea4ebd4304 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -12,6 +12,7 @@
 
 #include "mlir/Dialect/QC/IR/QCOps.h"
 #include "mlir/Dialect/QCO/IR/QCODialect.h"
+#include "mlir/Dialect/QCO/IR/QCOOps.h"
 #include "mlir/Dialect/QTensor/Utils/TensorIterator.h"
 
 #include <llvm/ADT/STLExtras.h>
@@ -54,13 +55,13 @@ static bool hasTypeQubitTensor(Value v) {
   return isa<qco::QubitType>(tensor.getElementType());
 }
 
-/// Map all results from one op to another.
+/// Map all results from one op to another using the given permutation.
 /// Assumes that `lhs->getNumResults() == rhs->getNumResults()`.
 /// Assumes that the two operations are equivalent to each other.
-static void mapResults(Operation* lhs, Operation* rhs, IRMapping& m) {
-  for (const auto& [fromResult, toResult] :
-       llvm::zip_equal(lhs->getResults(), rhs->getResults())) {
-    m.map(fromResult, toResult);
+static void mapResults(Operation* lhs, Operation* rhs,
+                       ArrayRef<size_t> permutation, IRMapping& m) {
+  for (const auto& [i, lhsResult] : llvm::enumerate(lhs->getResults())) {
+    m.map(lhsResult, rhs->getResult(permutation[i]));
   }
 }
 
@@ -70,11 +71,36 @@ static void mapResults(Operation* lhs, Operation* rhs, IRMapping& m) {
 static void mapArguments(Block& lhs, Block& rhs, ArrayRef<size_t> permutation,
                          IRMapping& m) {
   for (const auto& [i, lhsArg] : enumerate(lhs.getArguments())) {
-    BlockArgument rhsArg = rhs.getArgument(permutation[i]);
-    m.map(lhsArg, rhsArg);
+    m.map(lhsArg, rhs.getArgument(permutation[i]));
   }
 }
 
+/// Return a permutation vector, where permutation[i] maps the i-th target of
+/// the lhs to the j-th target of the rhs.
+static SmallVector<size_t> getTargetPermutation(qc::CtrlOp lhs, qc::CtrlOp rhs,
+                                                const IRMapping& m) {
+  SmallVector<size_t> permutation(lhs.getNumTargets());
+  for (const auto& [i, trgt] : llvm::enumerate(lhs.getTargets())) {
+    const auto it = llvm::find(rhs.getTargets(), m.lookup(trgt));
+    const auto j = std::distance(rhs.getTargets().begin(), it);
+    permutation[i] = j;
+  }
+  return permutation;
+}
+
+/// Return a permutation vector, where permutation[i] maps the i-th input target
+/// of the lhs to the j-th input target of the rhs.
+static SmallVector<size_t>
+getTargetPermutation(qco::CtrlOp lhs, qco::CtrlOp rhs, const IRMapping& m) {
+  SmallVector<size_t> permutation(lhs.getNumTargets());
+  for (const auto& [i, trgt] : llvm::enumerate(lhs.getInputTargets())) {
+    const auto it = llvm::find(rhs.getInputTargets(), m.lookup(trgt));
+    const auto j = std::distance(rhs.getInputTargets().begin(), it);
+    permutation[i] = j;
+  }
+  return permutation;
+}
+
 /// Compares two floating point numbers for approximate equivalence.
 static bool approxCompareFloats(const APFloat& lhs, const APFloat& rhs,
                                 const unsigned width) {
@@ -147,7 +173,7 @@ static bool compareAttributes(Attribute lhs, Attribute rhs) {
   return true;
 }
 
-/// Compare two operations for structural equivalence, applying some special
+/// Compare two operations for structural equivalence, applying special
 /// rules for `CtrlOp` s and `qtensor` s.
 static bool compareOperations(Operation* lhs, Operation* rhs,
                               const IRMapping& m) {
@@ -379,24 +405,18 @@ static bool compareBlocks(Block& lhs, Block& rhs,
     return false;
   }
 
-  // Map block arguments.
-  // The targets of a `CtrlOp` are commutative, thus, find the permutation from
-  // the i-th argument of the lhs to the j-th argument of the rhs, before
-  // mapping the block arguments.
+  // Map block arguments while allowing commutation of operands for `CtrlOp`s.
 
   if (isa<qc::CtrlOp>(lhs.getParentOp())) {
     assert(isa<qc::CtrlOp>(rhs.getParentOp()));
-
     auto lhsCtrl = cast<qc::CtrlOp>(lhs.getParentOp());
     auto rhsCtrl = cast<qc::CtrlOp>(rhs.getParentOp());
-
-    SmallVector<size_t> permutation(lhs.getNumArguments());
-    for (const auto& [i, trgt] : llvm::enumerate(lhsCtrl.getTargets())) {
-      const auto it = llvm::find(rhsCtrl.getTargets(), m.lookup(trgt));
-      const auto j = std::distance(rhsCtrl.getTargets().begin(), it);
-      permutation[i] = j;
-    }
-    mapArguments(lhs, rhs, permutation, m);
+    mapArguments(lhs, rhs, getTargetPermutation(lhsCtrl, rhsCtrl, m), m);
+  } else if (isa<qco::CtrlOp>(lhs.getParentOp())) {
+    assert(isa<qco::CtrlOp>(rhs.getParentOp()));
+    auto lhsCtrl = cast<qco::CtrlOp>(lhs.getParentOp());
+    auto rhsCtrl = cast<qco::CtrlOp>(rhs.getParentOp());
+    mapArguments(lhs, rhs, getTargetPermutation(lhsCtrl, rhsCtrl, m), m);
   } else {
     SmallVector<size_t> permutation(lhs.getNumArguments());
     std::iota(permutation.begin(), permutation.end(), 0);
@@ -430,19 +450,37 @@ static bool compareBlocks(Block& lhs, Block& rhs,
     DenseSet<Operation*> matched;
     matched.reserve(rhsReady.size());
 
-    for (Operation* opLhs : lhsReady) {
+    for (Operation* lhsOp : lhsReady) {
       SetVector<Operation*>::iterator it = rhsReady.begin();
       for (; it != rhsReady.end(); it = std::next(it)) {
-        Operation* opRhs = *it;
+        Operation* rhsOp = *it;
 
-        if (matched.contains(opRhs)) {
+        if (matched.contains(rhsOp)) {
           continue;
         }
 
-        if (compareOperations(opLhs, opRhs, m)) {
-          matched.insert(opRhs);
-          mapResults(opLhs, opRhs, m);
-          m.map(opLhs, opRhs);
+        if (compareOperations(lhsOp, rhsOp, m)) {
+          matched.insert(rhsOp);
+
+          if (isa<qc::CtrlOp>(lhsOp)) {
+            assert(isa<qc::CtrlOp>(rhsOp));
+            auto lhsCtrl = cast<qc::CtrlOp>(lhsOp);
+            auto rhsCtrl = cast<qc::CtrlOp>(rhsOp);
+            mapResults(lhsCtrl, rhsCtrl,
+                       getTargetPermutation(lhsCtrl, rhsCtrl, m), m);
+          } else if (isa<qco::CtrlOp>(lhsOp)) {
+            assert(isa<qco::CtrlOp>(rhsOp));
+            auto lhsCtrl = cast<qco::CtrlOp>(lhsOp);
+            auto rhsCtrl = cast<qco::CtrlOp>(rhsOp);
+            mapResults(lhsCtrl, rhsCtrl,
+                       getTargetPermutation(lhsCtrl, rhsCtrl, m), m);
+          } else {
+            SmallVector<size_t> permutation(lhsOp->getNumResults());
+            std::iota(permutation.begin(), permutation.end(), 0);
+            mapResults(lhsOp, rhsOp, permutation, m);
+          }
+
+          m.map(lhsOp, rhsOp);
           break;
         }
       }
@@ -453,7 +491,8 @@ static bool compareBlocks(Block& lhs, Block& rhs,
     }
 
     // At this point, we've successfully matched each operation on the lhs with
-    // one on the rhs.
+    // one on the rhs. Subsequently, update the open and closed sets and
+    // recursively compare the nested regions of each operation pair.
 
     lhsOpen.set_subtract(lhsReady);
     lhsClosed.set_union(lhsReady);
@@ -461,9 +500,6 @@ static bool compareBlocks(Block& lhs, Block& rhs,
     rhsOpen.set_subtract(rhsReady);
     rhsClosed.set_union(rhsReady);
 
-    // Once all ready operations have been matched, recursively compare
-    // the nested regions of each operation pair.
-
     SetVector<Operation*>::iterator it = lhsReady.begin();
     for (; it != lhsReady.end(); it = std::next(it)) {
       Operation* opLhs = *it;

From f6ba5f1c45dfa6c2895e4e1d76ff6999a1edd5b8 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 15:21:21 +0200
Subject: [PATCH 25/32] Implement equiv groups

---
 mlir/lib/Support/IRVerification.cpp | 318 +++++++++++++++++++---------
 1 file changed, 216 insertions(+), 102 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index ea4ebd4304..8f55eef92d 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -18,10 +18,12 @@
 #include <llvm/ADT/STLExtras.h>
 #include <llvm/ADT/SmallVector.h>
 #include <llvm/ADT/StringRef.h>
+#include <llvm/ADT/TypeSwitch.h>
 #include <llvm/Support/Casting.h>
 #include <llvm/Support/ErrorHandling.h>
 #include <mlir/Analysis/SliceAnalysis.h>
 #include <mlir/Dialect/QTensor/IR/QTensorOps.h>
+#include <mlir/Dialect/SCF/IR/SCF.h>
 #include <mlir/IR/Attributes.h>
 #include <mlir/IR/Block.h>
 #include <mlir/IR/Builders.h>
@@ -32,6 +34,7 @@
 #include <mlir/IR/Region.h>
 #include <mlir/IR/Value.h>
 #include <mlir/Support/LLVM.h>
+#include <mlir/Support/WalkResult.h>
 
 #include <cassert>
 #include <cmath>
@@ -41,9 +44,32 @@
 
 using namespace mlir;
 
+namespace {
+struct TensorMapping {
+  /// Maps all tensor values of the lhs to its equiv group.
+  DenseMap<Value, size_t> lhsEquivGroups;
+  /// Maps all tensor values of the rhs to its equiv group.
+  DenseMap<Value, size_t> rhsEquivGroups;
+  /// Maps the i-th group of lhs to the j-th group of rhs.
+  DenseMap<size_t, size_t> equivGroupMapping;
+
+  /// Map equivalence group identifiers of two tensors.
+  void map(Value lhs, Value rhs) {
+    equivGroupMapping[lhsEquivGroups[lhs]] = rhsEquivGroups[rhs];
+  }
+
+  /// Return true if the given tensor values have the same equiv group.
+  [[nodiscard]] bool equals(Value lhs, Value rhs) const {
+    const auto i = lhsEquivGroups.at(lhs);
+    return equivGroupMapping.at(i) == rhsEquivGroups.at(rhs);
+  }
+};
+} // namespace
+
 static bool compareRegions(Region& lhs, Region& rhs,
                            SetVector<Operation*>& lhsClosed,
-                           SetVector<Operation*>& rhsClosed, IRMapping& m);
+                           SetVector<Operation*>& rhsClosed, IRMapping& m,
+                           TensorMapping& tm);
 
 /// Return true, if the given value has the type `tensor<qco.qubit>`.
 static bool hasTypeQubitTensor(Value v) {
@@ -55,6 +81,62 @@ static bool hasTypeQubitTensor(Value v) {
   return isa<qco::QubitType>(tensor.getElementType());
 }
 
+/// Recursively initialize the equivalence group for a tensor value.
+static void initEquivGroup(TypedValue<RankedTensorType> v, size_t id,
+                           DenseMap<Value, size_t>& group) {
+  qtensor::TensorIterator it(v);
+  for (; it != std::default_sentinel; ++it) {
+    if (it.tensor() == nullptr) {
+      continue;
+    }
+
+    group[it.tensor()] = id;
+
+    if (isa<BlockArgument>(it.tensor())) {
+      continue;
+    }
+
+    if (auto op = dyn_cast<qco::IfOp>(it.operation())) {
+      const auto prev = std::prev(it);
+      const auto qIt = llvm::find(op.getQubits(), prev.tensor());
+      assert(qIt != op.getQubits().end());
+      const auto idx = std::distance(op.getQubits().begin(), qIt);
+
+      auto& thenRegion = op.getThenRegion();
+      auto& elseRegion = op.getElseRegion();
+
+      const auto& thenArg = thenRegion.getArgument(idx);
+      const auto& elseArg = elseRegion.getArgument(idx);
+
+      initEquivGroup(cast<TypedValue<RankedTensorType>>(thenArg), id, group);
+      initEquivGroup(cast<TypedValue<RankedTensorType>>(elseArg), id, group);
+    } else if (auto op = dyn_cast<scf::ForOp>(it.operation())) {
+      const auto& arg =
+          op.getTiedLoopRegionIterArg(cast<OpResult>(it.tensor()));
+      initEquivGroup(cast<TypedValue<RankedTensorType>>(arg), id, group);
+    }
+  }
+}
+
+/// Generate equivalence group for all allocated and created tensors.
+static DenseMap<Value, size_t> getEquivGroup(ModuleOp mod) {
+  size_t id = 0;
+  DenseMap<Value, size_t> group;
+
+  mod->walk([&](Operation* op) {
+    if (auto alloc = dyn_cast<qtensor::AllocOp>(op)) {
+      initEquivGroup(alloc.getResult(), id, group);
+      ++id;
+    } else if (auto from = dyn_cast<qtensor::FromElementsOp>(op)) {
+      initEquivGroup(cast<TypedValue<RankedTensorType>>(from.getResult()), id,
+                     group);
+      ++id;
+    }
+  });
+
+  return group;
+}
+
 /// Map all results from one op to another using the given permutation.
 /// Assumes that `lhs->getNumResults() == rhs->getNumResults()`.
 /// Assumes that the two operations are equivalent to each other.
@@ -70,6 +152,7 @@ static void mapResults(Operation* lhs, Operation* rhs,
 /// Assumes that `permutation.size() == lhs.getNumArguments()`.
 static void mapArguments(Block& lhs, Block& rhs, ArrayRef<size_t> permutation,
                          IRMapping& m) {
+
   for (const auto& [i, lhsArg] : enumerate(lhs.getArguments())) {
     m.map(lhsArg, rhs.getArgument(permutation[i]));
   }
@@ -88,8 +171,8 @@ static SmallVector<size_t> getTargetPermutation(qc::CtrlOp lhs, qc::CtrlOp rhs,
   return permutation;
 }
 
-/// Return a permutation vector, where permutation[i] maps the i-th input target
-/// of the lhs to the j-th input target of the rhs.
+/// Return a permutation vector, where permutation[i] maps the i-th input
+/// target of the lhs to the j-th input target of the rhs.
 static SmallVector<size_t>
 getTargetPermutation(qco::CtrlOp lhs, qco::CtrlOp rhs, const IRMapping& m) {
   SmallVector<size_t> permutation(lhs.getNumTargets());
@@ -101,7 +184,79 @@ getTargetPermutation(qco::CtrlOp lhs, qco::CtrlOp rhs, const IRMapping& m) {
   return permutation;
 }
 
-/// Compares two floating point numbers for approximate equivalence.
+/// Return a permutation vector, where permutation[i] maps the i-th input
+/// target of the lhs to the j-th input target of the rhs.
+static SmallVector<size_t>
+getControlPermutation(qco::CtrlOp lhs, qco::CtrlOp rhs, const IRMapping& m) {
+  SmallVector<size_t> permutation(lhs.getNumControls());
+  for (const auto& [i, trgt] : llvm::enumerate(lhs.getInputControls())) {
+    const auto it = llvm::find(rhs.getInputControls(), m.lookup(trgt));
+    const auto j = std::distance(rhs.getInputControls().begin(), it);
+    permutation[i] = j;
+  }
+  return permutation;
+}
+
+/// Compare two ctrl operations, allowing permutations of control and target
+/// qubits.
+static bool compareCtrlOps(qc::CtrlOp lhs, qc::CtrlOp rhs, const IRMapping& m) {
+  DenseSet<Value> workset;
+  workset.insert_range(rhs.getControls());
+  for (const auto& ctrl : lhs.getControls()) {
+    const auto& v = m.lookup(ctrl);
+    if (!workset.contains(v)) {
+      return false;
+    }
+    workset.erase(v);
+  }
+
+  if (!workset.empty()) {
+    return false;
+  }
+
+  workset.insert_range(rhs.getTargets());
+  for (const auto& trgt : lhs.getTargets()) {
+    const auto& v = m.lookup(trgt);
+    if (!workset.contains(v)) {
+      return false;
+    }
+    workset.erase(v);
+  }
+
+  return workset.empty();
+}
+
+/// Compare two ctrl operations, allowing permutations of input control and
+/// input target qubits.
+static bool compareCtrlOps(qco::CtrlOp lhs, qco::CtrlOp rhs,
+                           const IRMapping& m) {
+  DenseSet<Value> workset;
+  workset.insert_range(rhs.getInputControls());
+  for (const auto& ctrl : lhs.getInputControls()) {
+    const auto& v = m.lookup(ctrl);
+    if (!workset.contains(v)) {
+      return false;
+    }
+    workset.erase(v);
+  }
+
+  if (!workset.empty()) {
+    return false;
+  }
+
+  workset.insert_range(rhs.getInputTargets());
+  for (const auto& trgt : lhs.getInputTargets()) {
+    const auto& v = m.lookup(trgt);
+    if (!workset.contains(v)) {
+      return false;
+    }
+    workset.erase(v);
+  }
+
+  return workset.empty();
+}
+
+/// Compare two floating point numbers for approximate equivalence.
 static bool approxCompareFloats(const APFloat& lhs, const APFloat& rhs,
                                 const unsigned width) {
   if (lhs.isNaN() || rhs.isNaN()) {
@@ -132,9 +287,9 @@ static bool approxCompareFloats(const APFloat& lhs, const APFloat& rhs,
 }
 
 /// Compare two attributes for equivality.
-/// Explicitly checks `UnitAttr`, `IntegerAttr`, `FloatAttr`, `StringAttr`, and
-/// `FlatSymbolRefAttr`.
-/// For any other type, the function simply returns true.
+/// Explicitly checks `UnitAttr`, `IntegerAttr`, `FloatAttr`, `StringAttr`,
+/// and `FlatSymbolRefAttr`. For any other type, the function simply returns
+/// true.
 static bool compareAttributes(Attribute lhs, Attribute rhs) {
   if (dyn_cast<UnitAttr>(lhs)) {
     if (!dyn_cast<UnitAttr>(rhs)) {
@@ -176,7 +331,7 @@ static bool compareAttributes(Attribute lhs, Attribute rhs) {
 /// Compare two operations for structural equivalence, applying special
 /// rules for `CtrlOp` s and `qtensor` s.
 static bool compareOperations(Operation* lhs, Operation* rhs,
-                              const IRMapping& m) {
+                              const IRMapping& m, const TensorMapping& tm) {
 
   // Compare top-level signature-like characteristics.
 
@@ -209,87 +364,26 @@ static bool compareOperations(Operation* lhs, Operation* rhs,
 
   if (isa<qc::CtrlOp>(lhs)) {
     assert(isa<qc::CtrlOp>(rhs));
-
-    auto ctrlLhs = cast<qc::CtrlOp>(lhs);
-    auto ctrlRhs = cast<qc::CtrlOp>(rhs);
-
-    DenseSet<Value> workset;
-    workset.insert_range(ctrlRhs.getControls());
-    for (const auto& ctrl : ctrlLhs.getControls()) {
-      const auto& mapped = m.lookup(ctrl);
-      if (!workset.contains(mapped)) {
-        return false;
-      }
-      workset.erase(mapped);
+    if (!compareCtrlOps(cast<qc::CtrlOp>(lhs), cast<qc::CtrlOp>(rhs), m)) {
+      return false;
     }
-
-    assert(workset.empty());
-
-    // Analogously for the targets.
-
-    workset.clear();
-    workset.insert_range(ctrlRhs.getTargets());
-    for (const auto& trgt : ctrlLhs.getTargets()) {
-      const auto& operand = m.lookup(trgt);
-      if (!workset.contains(operand)) {
-        return false;
-      }
-      workset.erase(operand);
+  } else if (isa<qco::CtrlOp>(lhs)) {
+    assert(isa<qco::CtrlOp>(rhs));
+    if (!compareCtrlOps(cast<qco::CtrlOp>(lhs), cast<qco::CtrlOp>(rhs), m)) {
+      return false;
     }
-
-    assert(workset.empty());
-
   } else {
-    for (const auto& [operandLhs, operandRhs] :
+    for (const auto& [lhsOperand, rhsOperand] :
          llvm::zip_equal(lhs->getOperands(), rhs->getOperands())) {
+      if (hasTypeQubitTensor(lhsOperand)) {
+        assert(hasTypeQubitTensor(rhsOperand));
 
-      if (hasTypeQubitTensor(operandLhs)) {
-        assert(hasTypeQubitTensor(operandRhs));
-
-        auto tensorLhs = cast<TypedValue<RankedTensorType>>(operandLhs);
-        qtensor::TensorIterator itLhs(tensorLhs);
-        while (std::prev(itLhs) != itLhs) {
-          --itLhs;
-        }
-
-        auto tensorRhs = cast<TypedValue<RankedTensorType>>(operandRhs);
-        qtensor::TensorIterator itRhs(tensorRhs);
-        while (std::prev(itRhs) != itRhs) {
-          --itRhs;
-        }
-
-        if (isa<BlockArgument>(itLhs.tensor())) {
-          if (!isa<BlockArgument>(itRhs.tensor())) {
-            return false;
-          }
-        } else if (isa<qtensor::AllocOp>(itLhs.operation())) {
-          if (!isa<qtensor::AllocOp>(itRhs.operation())) {
-            return false;
-          }
-
-          auto allocLhs = cast<qtensor::AllocOp>(itLhs.operation());
-          auto allocRhs = cast<qtensor::AllocOp>(itRhs.operation());
-
-          if (m.lookup(allocLhs.getResult()) != allocRhs.getResult()) {
-            return false;
-          }
-        } else if (isa<qtensor::FromElementsOp>(itLhs.operation())) {
-          if (!isa<qtensor::FromElementsOp>(itRhs.operation())) {
-            return false;
-          }
-
-          auto fromLhs = cast<qtensor::FromElementsOp>(itLhs.operation());
-          auto fromRhs = cast<qtensor::FromElementsOp>(itRhs.operation());
-
-          if (m.lookup(fromLhs.getResult()) != fromRhs.getResult()) {
-            return false;
-          }
-        } else {
-          llvm::reportFatalInternalError("unhandled qtensor source");
+        if (!tm.equals(lhsOperand, rhsOperand)) {
+          return false;
         }
       } else {
-        auto operand = m.lookup(operandLhs);
-        if (operand != operandRhs) {
+        const auto& v = m.lookup(lhsOperand);
+        if (v != rhsOperand) {
           return false;
         }
       }
@@ -366,8 +460,8 @@ static SetVector<Operation*> getReadyOps(const SetVector<Operation*>& open,
 
       // Deallocations are ready whenever we've visited each op on the tensor
       // chain. Because we initialize the iterator with its input tensor, the
-      // iterator already points at the previous operation. Thus use a do-while
-      // loop instead of a regular while.
+      // iterator already points at the previous operation. Thus use a
+      // do-while loop instead of a regular while.
 
       bool fullChain{true};
       qtensor::TensorIterator it(dealloc.getTensor());
@@ -400,7 +494,8 @@ static SetVector<Operation*> getReadyOps(const SetVector<Operation*>& open,
 
 static bool compareBlocks(Block& lhs, Block& rhs,
                           SetVector<Operation*>& lhsClosed,
-                          SetVector<Operation*>& rhsClosed, IRMapping& m) {
+                          SetVector<Operation*>& rhsClosed, IRMapping& m,
+                          TensorMapping& tm) {
   if (lhs.getNumArguments() != rhs.getNumArguments()) {
     return false;
   }
@@ -459,21 +554,36 @@ static bool compareBlocks(Block& lhs, Block& rhs,
           continue;
         }
 
-        if (compareOperations(lhsOp, rhsOp, m)) {
+        if (compareOperations(lhsOp, rhsOp, m, tm)) {
           matched.insert(rhsOp);
 
-          if (isa<qc::CtrlOp>(lhsOp)) {
-            assert(isa<qc::CtrlOp>(rhsOp));
-            auto lhsCtrl = cast<qc::CtrlOp>(lhsOp);
-            auto rhsCtrl = cast<qc::CtrlOp>(rhsOp);
-            mapResults(lhsCtrl, rhsCtrl,
-                       getTargetPermutation(lhsCtrl, rhsCtrl, m), m);
-          } else if (isa<qco::CtrlOp>(lhsOp)) {
+          if (isa<qco::CtrlOp>(lhsOp)) {
             assert(isa<qco::CtrlOp>(rhsOp));
             auto lhsCtrl = cast<qco::CtrlOp>(lhsOp);
             auto rhsCtrl = cast<qco::CtrlOp>(rhsOp);
-            mapResults(lhsCtrl, rhsCtrl,
-                       getTargetPermutation(lhsCtrl, rhsCtrl, m), m);
+
+            SmallVector<size_t> permutation;
+            permutation.reserve(lhsCtrl.getNumQubits());
+            permutation.append(getControlPermutation(lhsCtrl, rhsCtrl, m));
+            for (const auto i : getTargetPermutation(lhsCtrl, rhsCtrl, m)) {
+              permutation.emplace_back(lhsCtrl.getNumControls() + i);
+            }
+            mapResults(lhsCtrl, rhsCtrl, permutation, m);
+          } else if (isa<qtensor::AllocOp>(lhsOp)) {
+            assert(isa<qtensor::AllocOp>(rhsOp));
+            auto lhsAlloc = cast<qtensor::AllocOp>(lhsOp);
+            auto rhsAlloc = cast<qtensor::AllocOp>(rhsOp);
+            tm.map(lhsAlloc.getResult(), rhsAlloc.getResult());
+          } else if (isa<qtensor::FromElementsOp>(lhsOp)) {
+            assert(isa<qtensor::FromElementsOp>(rhsOp));
+            auto lhsFrom = cast<qtensor::FromElementsOp>(lhsOp);
+            auto rhsFrom = cast<qtensor::FromElementsOp>(rhsOp);
+            tm.map(lhsFrom.getResult(), rhsFrom.getResult());
+          } else if (isa<qtensor::ExtractOp>(lhsOp)) {
+            assert(isa<qtensor::ExtractOp>(rhsOp));
+            auto lhsExtract = cast<qtensor::ExtractOp>(lhsOp);
+            auto rhsExtract = cast<qtensor::ExtractOp>(rhsOp);
+            m.map(lhsExtract.getResult(), rhsExtract.getResult());
           } else {
             SmallVector<size_t> permutation(lhsOp->getNumResults());
             std::iota(permutation.begin(), permutation.end(), 0);
@@ -490,8 +600,8 @@ static bool compareBlocks(Block& lhs, Block& rhs,
       }
     }
 
-    // At this point, we've successfully matched each operation on the lhs with
-    // one on the rhs. Subsequently, update the open and closed sets and
+    // At this point, we've successfully matched each operation on the lhs
+    // with one on the rhs. Subsequently, update the open and closed sets and
     // recursively compare the nested regions of each operation pair.
 
     lhsOpen.set_subtract(lhsReady);
@@ -512,7 +622,7 @@ static bool compareBlocks(Block& lhs, Block& rhs,
             [&](const auto& zip) {
               const auto& [lhsRegion, rhsRegion] = zip;
               return compareRegions(lhsRegion, rhsRegion, lhsClosed, rhsClosed,
-                                    m);
+                                    m, tm);
             }));
         if (nequiv != opLhs->getNumRegions()) {
           break;
@@ -531,16 +641,16 @@ static bool compareBlocks(Block& lhs, Block& rhs,
 /// Compare two regions for structural equivalence.
 static bool compareRegions(Region& lhs, Region& rhs,
                            SetVector<Operation*>& lhsClosed,
-                           SetVector<Operation*>& rhsClosed, IRMapping& m) {
+                           SetVector<Operation*>& rhsClosed, IRMapping& m,
+                           TensorMapping& tm) {
   if (lhs.getBlocks().size() != rhs.getBlocks().size()) {
     return false;
   }
 
   for (const auto [lhsBlock, rhsBlock] : llvm::zip_equal(lhs, rhs)) {
-    if (!compareBlocks(lhsBlock, rhsBlock, lhsClosed, rhsClosed, m)) {
+    if (!compareBlocks(lhsBlock, rhsBlock, lhsClosed, rhsClosed, m, tm)) {
       return false;
     }
-
     m.map(&lhsBlock, &rhsBlock);
   }
 
@@ -551,6 +661,10 @@ bool areModulesEquivalentWithPermutations(ModuleOp lhs, ModuleOp rhs) {
   IRMapping m;
   SetVector<Operation*> lhsClosed;
   SetVector<Operation*> rhsClosed;
+  TensorMapping tm{.lhsEquivGroups = getEquivGroup(lhs),
+                   .rhsEquivGroups = getEquivGroup(rhs),
+                   .equivGroupMapping = DenseMap<size_t, size_t>{}};
+
   return compareRegions(lhs.getBodyRegion(), rhs.getBodyRegion(), lhsClosed,
-                        rhsClosed, m);
+                        rhsClosed, m, tm);
 }

From bf9b4aef34cfd2afa7bee422f5227559384a6f82 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Fri, 12 Jun 2026 15:24:59 +0200
Subject: [PATCH 26/32] Remove unused imports

---
 mlir/lib/Support/IRVerification.cpp | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index 8f55eef92d..dade26bc0d 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -18,9 +18,7 @@
 #include <llvm/ADT/STLExtras.h>
 #include <llvm/ADT/SmallVector.h>
 #include <llvm/ADT/StringRef.h>
-#include <llvm/ADT/TypeSwitch.h>
 #include <llvm/Support/Casting.h>
-#include <llvm/Support/ErrorHandling.h>
 #include <mlir/Analysis/SliceAnalysis.h>
 #include <mlir/Dialect/QTensor/IR/QTensorOps.h>
 #include <mlir/Dialect/SCF/IR/SCF.h>
@@ -34,7 +32,6 @@
 #include <mlir/IR/Region.h>
 #include <mlir/IR/Value.h>
 #include <mlir/Support/LLVM.h>
-#include <mlir/Support/WalkResult.h>
 
 #include <cassert>
 #include <cmath>

From 645ea34265b09b52ef813a566347a58e65ccc938 Mon Sep 17 00:00:00 2001
From: burgholzer <burgholzer@me.com>
Date: Fri, 12 Jun 2026 17:07:38 +0200
Subject: [PATCH 27/32] :art: Minor cosmetic fixes

Signed-off-by: burgholzer <burgholzer@me.com>
---
 mlir/lib/Support/IRVerification.cpp | 32 ++++++++++++-----------------
 1 file changed, 13 insertions(+), 19 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index dade26bc0d..388d6878ea 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -81,8 +81,7 @@ static bool hasTypeQubitTensor(Value v) {
 /// Recursively initialize the equivalence group for a tensor value.
 static void initEquivGroup(TypedValue<RankedTensorType> v, size_t id,
                            DenseMap<Value, size_t>& group) {
-  qtensor::TensorIterator it(v);
-  for (; it != std::default_sentinel; ++it) {
+  for (qtensor::TensorIterator it(v); it != std::default_sentinel; ++it) {
     if (it.tensor() == nullptr) {
       continue;
     }
@@ -107,9 +106,9 @@ static void initEquivGroup(TypedValue<RankedTensorType> v, size_t id,
 
       initEquivGroup(cast<TypedValue<RankedTensorType>>(thenArg), id, group);
       initEquivGroup(cast<TypedValue<RankedTensorType>>(elseArg), id, group);
-    } else if (auto op = dyn_cast<scf::ForOp>(it.operation())) {
+    } else if (auto forOp = dyn_cast<scf::ForOp>(it.operation())) {
       const auto& arg =
-          op.getTiedLoopRegionIterArg(cast<OpResult>(it.tensor()));
+          forOp.getTiedLoopRegionIterArg(cast<OpResult>(it.tensor()));
       initEquivGroup(cast<TypedValue<RankedTensorType>>(arg), id, group);
     }
   }
@@ -293,21 +292,20 @@ static bool compareAttributes(Attribute lhs, Attribute rhs) {
       return false;
     }
   } else if (auto intAttrA = dyn_cast<IntegerAttr>(lhs)) {
-    auto intAttrB = dyn_cast<IntegerAttr>(rhs);
-    if (!intAttrB || intAttrA.getValue() != intAttrB.getValue()) {
+    if (auto intAttrB = dyn_cast<IntegerAttr>(rhs);
+        !intAttrB || intAttrA.getValue() != intAttrB.getValue()) {
       return false;
     }
   } else if (auto floatAttrA = dyn_cast<FloatAttr>(lhs)) {
-    auto floatAttrB = dyn_cast<FloatAttr>(rhs);
-
-    if (!floatAttrB ||
+    if (auto floatAttrB = dyn_cast<FloatAttr>(rhs);
+        !floatAttrB ||
         !approxCompareFloats(floatAttrA.getValue(), floatAttrB.getValue(),
                              floatAttrA.getType().getIntOrFloatBitWidth())) {
       return false;
     }
   } else if (auto strAttrA = dyn_cast<StringAttr>(lhs)) {
-    auto strAttrB = dyn_cast<StringAttr>(rhs);
-    if (!strAttrB || strAttrA.getValue() != strAttrB.getValue()) {
+    if (auto strAttrB = dyn_cast<StringAttr>(rhs);
+        !strAttrB || strAttrA.getValue() != strAttrB.getValue()) {
       return false;
     }
   } else if (auto symbolRefAttrA =
@@ -412,11 +410,9 @@ static SetVector<Operation*> getReadyOps(const SetVector<Operation*>& open,
       // If any of the inserts on the chain are ready, we consider the entire
       // chain ready because the ready operations could be moved to the front
       // of the chain.
-
       SmallVector<Operation*> chain;
-      qtensor::TensorIterator it(insert.getResult());
-
-      for (; it != std::default_sentinel; ++it) {
+      for (qtensor::TensorIterator it(insert.getResult());
+           it != std::default_sentinel; ++it) {
         auto chainInsert = dyn_cast<qtensor::InsertOp>(it.operation());
         if (!chainInsert) {
           break;
@@ -434,11 +430,9 @@ static SetVector<Operation*> getReadyOps(const SetVector<Operation*>& open,
     } else if (auto extract = dyn_cast<qtensor::ExtractOp>(op)) {
 
       // We apply the analogous logic to extracts.
-
       SmallVector<Operation*> chain;
-      qtensor::TensorIterator it(extract.getOutTensor());
-
-      for (; it != std::default_sentinel; ++it) {
+      for (qtensor::TensorIterator it(extract.getOutTensor());
+           it != std::default_sentinel; ++it) {
         auto chainExtract = dyn_cast<qtensor::ExtractOp>(it.operation());
         if (!chainExtract) {
           break;

From 018538b5266f43ee15c002a27445209133c6ed12 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Mon, 15 Jun 2026 07:39:36 +0200
Subject: [PATCH 28/32] Update repeatedControlledX test

---
 mlir/unittests/programs/qc_programs.cpp  |  6 +++---
 mlir/unittests/programs/qco_programs.cpp | 17 ++++++++++++-----
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/mlir/unittests/programs/qc_programs.cpp b/mlir/unittests/programs/qc_programs.cpp
index ab7d0da95b..300d259751 100644
--- a/mlir/unittests/programs/qc_programs.cpp
+++ b/mlir/unittests/programs/qc_programs.cpp
@@ -277,10 +277,10 @@ void trivialControlledX(QCProgramBuilder& b) {
 }
 
 void repeatedControlledX(QCProgramBuilder& b) {
-  auto q = b.allocQubitRegister(2);
+  auto q = b.allocQubitRegister(64);
   b.h(q[0]);
-  for (auto i = 0; i < 2; i++) {
-    b.cx(q[0], q[1]);
+  for (auto i = 1; i < 64; i++) {
+    b.cx(q[0], q[i]);
   }
 }
 
diff --git a/mlir/unittests/programs/qco_programs.cpp b/mlir/unittests/programs/qco_programs.cpp
index 1c3118d80b..ca6c5096aa 100644
--- a/mlir/unittests/programs/qco_programs.cpp
+++ b/mlir/unittests/programs/qco_programs.cpp
@@ -272,14 +272,21 @@ void trivialControlledX(QCOProgramBuilder& b) {
 }
 
 void repeatedControlledX(QCOProgramBuilder& b) {
+  auto tensor = b.qtensorAlloc(64);
+
   Value q0;
-  Value q1;
-  auto tensor = b.qtensorAlloc(2);
   std::tie(tensor, q0) = b.qtensorExtract(tensor, 0);
-  std::tie(tensor, q1) = b.qtensorExtract(tensor, 1);
+
+  SmallVector<Value> values(63);
+  for (auto i = 1; i < 64; i++) {
+    Value qi;
+    std::tie(tensor, qi) = b.qtensorExtract(tensor, i);
+    values[i - 1] = qi;
+  }
+
   q0 = b.h(q0);
-  for (auto i = 0; i < 2; i++) {
-    std::tie(q0, q1) = b.cx(q0, q1);
+  for (auto i = 1; i < 64; i++) {
+    std::tie(q0, values[i - 1]) = b.cx(q0, values[i - 1]);
   }
 }
 

From b01841a89ea8b00982e97a035575c7edaace9383 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Mon, 15 Jun 2026 08:28:58 +0200
Subject: [PATCH 29/32] Distinguish between index and integer types

---
 mlir/lib/Support/IRVerification.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index 388d6878ea..a6414f42ca 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -293,7 +293,8 @@ static bool compareAttributes(Attribute lhs, Attribute rhs) {
     }
   } else if (auto intAttrA = dyn_cast<IntegerAttr>(lhs)) {
     if (auto intAttrB = dyn_cast<IntegerAttr>(rhs);
-        !intAttrB || intAttrA.getValue() != intAttrB.getValue()) {
+        !intAttrB || intAttrA.getValue() != intAttrB.getValue() ||
+        (intAttrA.getType().isInteger() && !intAttrB.getType().isInteger())) {
       return false;
     }
   } else if (auto floatAttrA = dyn_cast<FloatAttr>(lhs)) {
@@ -642,6 +643,9 @@ static bool compareRegions(Region& lhs, Region& rhs,
     if (!compareBlocks(lhsBlock, rhsBlock, lhsClosed, rhsClosed, m, tm)) {
       return false;
     }
+
+    lhsBlock.dump();
+    rhsBlock.dump();
     m.map(&lhsBlock, &rhsBlock);
   }
 

From 3ae0daea7d9392f389289f5304f872d30c5477c7 Mon Sep 17 00:00:00 2001
From: Matthias Reumann <matthias.reumann@tum.de>
Date: Mon, 15 Jun 2026 08:46:52 +0200
Subject: [PATCH 30/32] Add alternative chain unit-test

---
 mlir/lib/Support/IRVerification.cpp           |  8 ++---
 .../Dialect/QTensor/IR/test_qtensor_ir.cpp    |  6 +++-
 mlir/unittests/programs/qco_programs.cpp      | 36 +++++++++++++++++++
 mlir/unittests/programs/qco_programs.h        |  9 +++++
 4 files changed, 52 insertions(+), 7 deletions(-)

diff --git a/mlir/lib/Support/IRVerification.cpp b/mlir/lib/Support/IRVerification.cpp
index a6414f42ca..a1700fa319 100644
--- a/mlir/lib/Support/IRVerification.cpp
+++ b/mlir/lib/Support/IRVerification.cpp
@@ -148,7 +148,6 @@ static void mapResults(Operation* lhs, Operation* rhs,
 /// Assumes that `permutation.size() == lhs.getNumArguments()`.
 static void mapArguments(Block& lhs, Block& rhs, ArrayRef<size_t> permutation,
                          IRMapping& m) {
-
   for (const auto& [i, lhsArg] : enumerate(lhs.getArguments())) {
     m.map(lhsArg, rhs.getArgument(permutation[i]));
   }
@@ -410,7 +409,8 @@ static SetVector<Operation*> getReadyOps(const SetVector<Operation*>& open,
 
       // If any of the inserts on the chain are ready, we consider the entire
       // chain ready because the ready operations could be moved to the front
-      // of the chain.
+      // of the chain. The analogous logic is applied to extracts.
+
       SmallVector<Operation*> chain;
       for (qtensor::TensorIterator it(insert.getResult());
            it != std::default_sentinel; ++it) {
@@ -429,8 +429,6 @@ static SetVector<Operation*> getReadyOps(const SetVector<Operation*>& open,
       }
 
     } else if (auto extract = dyn_cast<qtensor::ExtractOp>(op)) {
-
-      // We apply the analogous logic to extracts.
       SmallVector<Operation*> chain;
       for (qtensor::TensorIterator it(extract.getOutTensor());
            it != std::default_sentinel; ++it) {
@@ -644,8 +642,6 @@ static bool compareRegions(Region& lhs, Region& rhs,
       return false;
     }
 
-    lhsBlock.dump();
-    rhsBlock.dump();
     m.map(&lhsBlock, &rhsBlock);
   }
 
diff --git a/mlir/unittests/Dialect/QTensor/IR/test_qtensor_ir.cpp b/mlir/unittests/Dialect/QTensor/IR/test_qtensor_ir.cpp
index 27aeec9455..afa4ef68ed 100644
--- a/mlir/unittests/Dialect/QTensor/IR/test_qtensor_ir.cpp
+++ b/mlir/unittests/Dialect/QTensor/IR/test_qtensor_ir.cpp
@@ -506,7 +506,11 @@ INSTANTIATE_TEST_SUITE_P(
         QTensorIntegrationTestCase{
             "QTensorInsertExtractIndexMismatch",
             MQT_NAMED_BUILDER(qtensorInsertExtractIndexMismatch),
-            MQT_NAMED_BUILDER(qtensorInsertExtractIndexMismatch)}));
+            MQT_NAMED_BUILDER(qtensorInsertExtractIndexMismatch)},
+          QTensorIntegrationTestCase{
+            "QTensorAlternativeInsertChain",
+            MQT_NAMED_BUILDER(qtensorAlternativeChain),
+            MQT_NAMED_BUILDER(qtensorChain)}));
 /// @}
 
 } // namespace
diff --git a/mlir/unittests/programs/qco_programs.cpp b/mlir/unittests/programs/qco_programs.cpp
index ca6c5096aa..1fadf83eb2 100644
--- a/mlir/unittests/programs/qco_programs.cpp
+++ b/mlir/unittests/programs/qco_programs.cpp
@@ -2345,6 +2345,42 @@ void qtensorInsertExtractSameIndex(QCOProgramBuilder& b) {
   b.qtensorInsert(q2, extractOutTensor1, 0);
 }
 
+void qtensorChain(QCOProgramBuilder& b) {
+  Value q0;
+  Value q1;
+  Value q2;
+  auto qtensor = b.qtensorAlloc(3);
+  std::tie(qtensor, q0) = b.qtensorExtract(qtensor, 0);
+  std::tie(qtensor, q1) = b.qtensorExtract(qtensor, 1);
+  std::tie(qtensor, q2) = b.qtensorExtract(qtensor, 2);
+  q0 = b.h(q0);
+  q1 = b.h(q1);
+  std::tie(q1, q2) = b.cx(q1, q2);
+
+  qtensor = b.qtensorInsert(q2, qtensor, 2);
+  qtensor = b.qtensorInsert(q1, qtensor, 1);
+  qtensor = b.qtensorInsert(q0, qtensor, 0);
+  b.qtensorDealloc(qtensor);
+}
+
+void qtensorAlternativeChain(QCOProgramBuilder& b) {
+  Value q0;
+  Value q1;
+  Value q2;
+  auto qtensor = b.qtensorAlloc(3);
+  std::tie(qtensor, q0) = b.qtensorExtract(qtensor, 0);
+  q0 = b.h(q0);
+  std::tie(qtensor, q1) = b.qtensorExtract(qtensor, 1);
+  q1 = b.h(q1);
+  std::tie(qtensor, q2) = b.qtensorExtract(qtensor, 2);
+  std::tie(q1, q2) = b.cx(q1, q2);
+
+  qtensor = b.qtensorInsert(q0, qtensor, 0);
+  qtensor = b.qtensorInsert(q1, qtensor, 1);
+  qtensor = b.qtensorInsert(q2, qtensor, 2);
+  b.qtensorDealloc(qtensor);
+}
+
 void simpleWhileReset(QCOProgramBuilder& b) {
   auto q0 = b.allocQubit();
   auto q1 = b.h(q0);
diff --git a/mlir/unittests/programs/qco_programs.h b/mlir/unittests/programs/qco_programs.h
index 6f6323db22..28a8f5b2aa 100644
--- a/mlir/unittests/programs/qco_programs.h
+++ b/mlir/unittests/programs/qco_programs.h
@@ -1122,4 +1122,13 @@ void qtensorInsertExtractIndexMismatch(QCOProgramBuilder& b);
 /// Inserts a qubit into a tensor and extracts it immediately at the same index.
 void qtensorInsertExtractSameIndex(QCOProgramBuilder& b);
 
+/// Extracts three qubits with ascending index (0, 1, 2), performs a
+/// computation, and finally inserts the qubits in ascending order (0, 1, 2).
+void qtensorChain(QCOProgramBuilder& b);
+
+/// Performs the same computation as the `qtensorChain` function, but uses
+/// qubits immediately after the extract and inserts the qubits in descending
+/// order (0, 1, 2).
+void qtensorAlternativeChain(QCOProgramBuilder& b);
+
 } // namespace mlir::qco

From 263c7cca7962d16ed7ab8ba1eb6c2b1ed238ee73 Mon Sep 17 00:00:00 2001
From: "pre-commit-ci[bot]"
 <66853113+pre-commit-ci[bot]@users.noreply.github.com>
Date: Mon, 15 Jun 2026 06:47:25 +0000
Subject: [PATCH 31/32] =?UTF-8?q?=F0=9F=8E=A8=20pre-commit=20fixes?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 mlir/unittests/Dialect/QTensor/IR/test_qtensor_ir.cpp | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/mlir/unittests/Dialect/QTensor/IR/test_qtensor_ir.cpp b/mlir/unittests/Dialect/QTensor/IR/test_qtensor_ir.cpp
index afa4ef68ed..a76e20cc1a 100644
--- a/mlir/unittests/Dialect/QTensor/IR/test_qtensor_ir.cpp
+++ b/mlir/unittests/Dialect/QTensor/IR/test_qtensor_ir.cpp
@@ -507,10 +507,9 @@ INSTANTIATE_TEST_SUITE_P(
             "QTensorInsertExtractIndexMismatch",
             MQT_NAMED_BUILDER(qtensorInsertExtractIndexMismatch),
             MQT_NAMED_BUILDER(qtensorInsertExtractIndexMismatch)},
-          QTensorIntegrationTestCase{
-            "QTensorAlternativeInsertChain",
-            MQT_NAMED_BUILDER(qtensorAlternativeChain),
-            MQT_NAMED_BUILDER(qtensorChain)}));
+        QTensorIntegrationTestCase{"QTensorAlternativeInsertChain",
+                                   MQT_NAMED_BUILDER(qtensorAlternativeChain),
+                                   MQT_NAMED_BUILDER(qtensorChain)}));
 /// @}
 
 } // namespace

From 5481bc65f65e39f6aebba90704803f253ceebae9 Mon Sep 17 00:00:00 2001
From: matthias <matthias.reumann@tum.de>
Date: Mon, 15 Jun 2026 14:10:59 +0200
Subject: [PATCH 32/32] Update mlir/unittests/programs/qco_programs.h

Co-authored-by: Lukas Burgholzer <burgholzer@me.com>
Signed-off-by: matthias <matthias@bereumann.com>
---
 mlir/unittests/programs/qco_programs.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mlir/unittests/programs/qco_programs.h b/mlir/unittests/programs/qco_programs.h
index 28a8f5b2aa..1a5f5ce229 100644
--- a/mlir/unittests/programs/qco_programs.h
+++ b/mlir/unittests/programs/qco_programs.h
@@ -1128,7 +1128,7 @@ void qtensorChain(QCOProgramBuilder& b);
 
 /// Performs the same computation as the `qtensorChain` function, but uses
 /// qubits immediately after the extract and inserts the qubits in descending
-/// order (0, 1, 2).
+/// order (2, 1, 0).
 void qtensorAlternativeChain(QCOProgramBuilder& b);
 
 } // namespace mlir::qco