🐛 MLIR Module equivalence verifier fails for equivalent circuits with different insertion order

[li-mingbao]

System and Environment Information

• mlir/llvm version 22.1.5
• OS: Ubuntu 22.04

Bug Description

The current module equivalence checker in the MLIR tests fail if the insertion order of qubits to the registers are different at the end. The areModulesEquivalentWithPermutations function should still succeed even if the insertion order at the end is different, as the resulting circuit is still equivalent.

Steps to Reproduce

The following two modules are not equivalent according to the verifier:

 module {                                                                                                             
   func.func @main() -> i64 attributes {passthrough = ["entry_point"]} {                                              
     %c0_i64 = arith.constant 0 : i64                                                                                 
     %c1 = arith.constant 1 : index                                                                                   
     %c0 = arith.constant 0 : index                                                                                   
     %c2 = arith.constant 2 : index                                                                                   
     %0 = qtensor.alloc(%c2) : tensor<2x!qco.qubit>                                                                   
     %out_tensor, %result = qtensor.extract %0[%c0] : tensor<2x!qco.qubit>                                            
     %out_tensor_0, %result_1 = qtensor.extract %out_tensor[%c1] : tensor<2x!qco.qubit>                               
     %1 = qco.alloc : !qco.qubit                                                                                      
     %2 = qco.h %1 : !qco.qubit -> !qco.qubit                                                                         
     %controls_out, %targets_out = qco.ctrl(%2) targets (%arg0 = %result) {                                           
       %5 = qco.x %arg0 : !qco.qubit -> !qco.qubit                                                                    
       qco.yield %5 : !qco.qubit                                                                                      
     } : ({!qco.qubit}, {!qco.qubit}) -> ({!qco.qubit}, {!qco.qubit})                                                 
     %controls_out_2, %targets_out_3 = qco.ctrl(%controls_out) targets (%arg0 = %result_1) {                          
       %5 = qco.x %arg0 : !qco.qubit -> !qco.qubit                                                                    
       qco.yield %5 : !qco.qubit                                                                                      
     } : ({!qco.qubit}, {!qco.qubit}) -> ({!qco.qubit}, {!qco.qubit})                                                 
     qco.sink %controls_out_2 : !qco.qubit                                                                            
     %3 = qtensor.insert %targets_out_3 into %out_tensor_0[%c1] : tensor<2x!qco.qubit>                                
     %4 = qtensor.insert %targets_out into %3[%c0] : tensor<2x!qco.qubit>                                             
     qtensor.dealloc %4 : tensor<2x!qco.qubit>                                                                        
     return %c0_i64 : i64                                                                                             
   }                                                                                                                  
 } 

module {                                                                                                             
   func.func @main() -> i64 attributes {passthrough = ["entry_point"]} {                                              
     %c0_i64 = arith.constant 0 : i64                                                                                 
     %c1 = arith.constant 1 : index                                                                                   
     %c0 = arith.constant 0 : index                                                                                   
     %c2 = arith.constant 2 : index                                                                                   
     %0 = qtensor.alloc(%c2) : tensor<2x!qco.qubit>                                                                   
     %out_tensor, %result = qtensor.extract %0[%c0] : tensor<2x!qco.qubit>                                            
     %out_tensor_0, %result_1 = qtensor.extract %out_tensor[%c1] : tensor<2x!qco.qubit>                               
     %1 = qco.alloc : !qco.qubit                                                                                      
     %2 = qco.h %1 : !qco.qubit -> !qco.qubit                                                                         
     %controls_out, %targets_out = qco.ctrl(%2) targets (%arg0 = %result) {                                           
       %5 = qco.x %arg0 : !qco.qubit -> !qco.qubit                                                                    
       qco.yield %5 : !qco.qubit                                                                                      
     } : ({!qco.qubit}, {!qco.qubit}) -> ({!qco.qubit}, {!qco.qubit})                                                 
     %controls_out_2, %targets_out_3 = qco.ctrl(%controls_out) targets (%arg0 = %result_1) {                          
       %5 = qco.x %arg0 : !qco.qubit -> !qco.qubit                                                                    
       qco.yield %5 : !qco.qubit                                                                                      
     } : ({!qco.qubit}, {!qco.qubit}) -> ({!qco.qubit}, {!qco.qubit})                                                 
     qco.sink %controls_out_2 : !qco.qubit                                                                            
     %3 = qtensor.insert %targets_out into %out_tensor_0[%c0] : tensor<2x!qco.qubit>                                  
     %4 = qtensor.insert %targets_out_3 into %3[%c1] : tensor<2x!qco.qubit>                                           
     qtensor.dealloc %4 : tensor<2x!qco.qubit>                                                                        
     return %c0_i64 : i64                                                                                             
   }                                                                                                                  
 } 

[burgholzer]

@MatthiasReumann do you maybe have some capacity to look at this?

[MatthiasReumann]

@MatthiasReumann do you maybe have some capacity to look at this?

Will do!

[MatthiasReumann]

The verifier also fails for the following IR

// Canonicalized Converted QCO IR
module {
  func.func @main() -> i64 attributes {passthrough = ["entry_point"]} {
    %c0_i64 = arith.constant 0 : i64
    %c1 = arith.constant 1 : index
    %c0 = arith.constant 0 : index
    %c2 = arith.constant 2 : index
    %0 = qtensor.alloc(%c2) : tensor<2x!qco.qubit>
    %out_tensor, %result = qtensor.extract %0[%c0] : tensor<2x!qco.qubit>
    %out_tensor_0, %result_1 = qtensor.extract %out_tensor[%c1] : tensor<2x!qco.qubit>
    %1 = qco.h %result : !qco.qubit -> !qco.qubit // ← Hadamard after both extracts
    %controls_out, %targets_out = qco.ctrl(%1) targets (%arg0 = %result_1) {
      %4 = qco.x %arg0 : !qco.qubit -> !qco.qubit
      qco.yield %4 : !qco.qubit
    } : ({!qco.qubit}, {!qco.qubit}) -> ({!qco.qubit}, {!qco.qubit})
    %controls_out_2, %targets_out_3 = qco.ctrl(%controls_out) targets (%arg0 = %targets_out) {
      %4 = qco.x %arg0 : !qco.qubit -> !qco.qubit
      qco.yield %4 : !qco.qubit
    } : ({!qco.qubit}, {!qco.qubit}) -> ({!qco.qubit}, {!qco.qubit})
    %2 = qtensor.insert %targets_out_3 into %out_tensor_0[%c1] : tensor<2x!qco.qubit>
    %3 = qtensor.insert %controls_out_2 into %2[%c0] : tensor<2x!qco.qubit>
    qtensor.dealloc %3 : tensor<2x!qco.qubit>
    return %c0_i64 : i64
  }
}

// Canonicalized Reference QCO IR
module {
  func.func @main() -> i64 attributes {passthrough = ["entry_point"]} {
    %c0_i64 = arith.constant 0 : i64
    %c1 = arith.constant 1 : index
    %c0 = arith.constant 0 : index
    %c2 = arith.constant 2 : index
    %0 = qtensor.alloc(%c2) : tensor<2x!qco.qubit>
    %out_tensor, %result = qtensor.extract %0[%c0] : tensor<2x!qco.qubit>
    %1 = qco.h %result : !qco.qubit -> !qco.qubit  // ← Hadamard after first extract
    %out_tensor_0, %result_1 = qtensor.extract %out_tensor[%c1] : tensor<2x!qco.qubit>
    %controls_out, %targets_out = qco.ctrl(%1) targets (%arg0 = %result_1) {
      %4 = qco.x %arg0 : !qco.qubit -> !qco.qubit
      qco.yield %4 : !qco.qubit
    } : ({!qco.qubit}, {!qco.qubit}) -> ({!qco.qubit}, {!qco.qubit})
    %controls_out_2, %targets_out_3 = qco.ctrl(%controls_out) targets (%arg0 = %targets_out) {
      %4 = qco.x %arg0 : !qco.qubit -> !qco.qubit
      qco.yield %4 : !qco.qubit
    } : ({!qco.qubit}, {!qco.qubit}) -> ({!qco.qubit}, {!qco.qubit})
    %2 = qtensor.insert %targets_out_3 into %out_tensor_0[%c1] : tensor<2x!qco.qubit>
    %3 = qtensor.insert %controls_out_2 into %2[%c0] : tensor<2x!qco.qubit>
    qtensor.dealloc %3 : tensor<2x!qco.qubit>
    return %c0_i64 : i64
  }
}

For the given example, the verifier builds unequal independent groups and consequently the areIndependentGroupsEquivalent check fails.

Analogously for the following IRs:

module {
  func.func @main() -> i64 attributes {passthrough = ["entry_point"]} {
    %c2 = arith.constant 2 : index
    %0 = qtensor.alloc(%c2) : tensor<2x!qco.qubit>
    %c0 = arith.constant 0 : index
    %out_tensor, %result = qtensor.extract %0[%c0] : tensor<2x!qco.qubit>
    %c1 = arith.constant 1 : index
    %out_tensor_0, %result_1 = qtensor.extract %out_tensor[%c1] : tensor<2x!qco.qubit>
    %1 = qco.h %result : !qco.qubit -> !qco.qubit
    %2 = qco.reset %1 : !qco.qubit -> !qco.qubit
    %3 = qco.h %result_1 : !qco.qubit -> !qco.qubit
    %4 = qco.reset %3 : !qco.qubit -> !qco.qubit
    %c0_2 = arith.constant 0 : index // ← LHS
    %5 = qtensor.insert %2 into %out_tensor_0[%c0_2] : tensor<2x!qco.qubit>
    %c1_3 = arith.constant 1 : index
    %6 = qtensor.insert %4 into %5[%c1_3] : tensor<2x!qco.qubit>
    qtensor.dealloc %6 : tensor<2x!qco.qubit>
    %c0_i64 = arith.constant 0 : i64
    return %c0_i64 : i64
  }
}

module {
  func.func @main() -> i64 attributes {passthrough = ["entry_point"]} {
    %c2 = arith.constant 2 : index
    %0 = qtensor.alloc(%c2) : tensor<2x!qco.qubit>
    %c0 = arith.constant 0 : index
    %out_tensor, %result = qtensor.extract %0[%c0] : tensor<2x!qco.qubit>
    %c1 = arith.constant 1 : index
    %out_tensor_0, %result_1 = qtensor.extract %out_tensor[%c1] : tensor<2x!qco.qubit>
    %1 = qco.h %result : !qco.qubit -> !qco.qubit
    %2 = qco.reset %1 : !qco.qubit -> !qco.qubit
    %3 = qco.h %result_1 : !qco.qubit -> !qco.qubit
    %4 = qco.reset %3 : !qco.qubit -> !qco.qubit
    %c1_2 = arith.constant 1 : index // ← RHS
    %5 = qtensor.insert %4 into %out_tensor_0[%c1_2] : tensor<2x!qco.qubit>
    %c0_3 = arith.constant 0 : index
    %6 = qtensor.insert %2 into %5[%c0_3] : tensor<2x!qco.qubit>
    qtensor.dealloc %6 : tensor<2x!qco.qubit>
    %c0_i64 = arith.constant 0 : i64
    return %c0_i64 : i64
  }
}

In the above example, the left independent group consists of %c0_2 = arith.constant 0 : index while its counterpart consists of %c1_2 = arith.constant 1 : index. These are not equivalent, and thus, the verification fails.