🐛 Kernel Crash During `verify` with Different Sized Circuits with Boundary `swap`)

[MattePalte]

Environment information

OS: Ubuntu 20.04
C++ Compiler: g++ (Ubuntu 9.4.0-1ubuntu1~20.04.2) 9.4.0
mqt.core version: 2.7.0
mqt.qcec version: 2.7.1

Description

Running a comparison between two circuits led to a kernel crash of QCEC.

Expected behavior

The comparison should complete without causing a kernel crash.

How to Reproduce

1. Create two QASM files with the following content:
   • qasm_a.qasm:

     OPENQASM 2.0;
     include "qelib1.inc";
     qreg q[1];
     rz(1) q[0];

   • qasm_b.qasm:

     OPENQASM 2.0;
     include "qelib1.inc";
     qreg q[3];
     swap q[1],q[2];

2. Save the QASM content to files:

   path_qasm_1 = "qasm_a.qasm"
   path_qasm_2 = "qasm_b.qasm"
   
   with open(path_qasm_1, 'w') as file:
       file.write(qasm_a)
   
   with open(path_qasm_2, 'w') as file:
       file.write(qasm_b)

3. Run the following code to verify the circuits:

   from mqt import qcec
   
   result = qcec.verify(
       str(path_qasm_1),
       str(path_qasm_2),
       transform_dynamic_circuit=True)
   equivalence = str(result.equivalence)

Additional Information

The kernel crashed while executing the code. The log has no interesting message:

23:38:10.947 [info] Restarted 55f0b765-eeab-41e1-a2d9-d71086dd5d5a
23:38:12.956 [error] Disposing session as kernel process died ExitCode: undefined, Reason:

[burgholzer]

Hey 👋🏻

Thanks for raising this issue.
I am on vacation right now (until end of next week) and don't have my laptop with me, but I am pretty sure this is a bug on our side.

If I had a guess it is a mixture between the two circuits having different numbers of qubits (and the assumptions we make because of that) and the fact that one of the circuits is a simple SWAP gate (which we typically optimize away by just storing it in form of a permutation, which effectively makes one of the circuits empty).
These kind of corner cases keep popping up from time to time. Eventually, we will get them all 😌

If you don't mind, could you check if you also get a segfault when you

• (1) make both circuits operate on two qubits (just using qreg q[2] in both cases)
• (2) append measurements to the end of the circuit (adding a creg c[2] and a measure q -> c; instruction at the end)
• (1)+(2)

And just to be really sure and since it has been a while since the last official release: could you try running with the latest version from main?

pip install "mqt.qcec @ git+https://github.com/cda-tum/mqt-qcec@main"

(Needs a C++17 compatible compiler on path)

This would save me some time while trying to debug this. Thanks 🙏

[MattePalte]

Short answer

Case 1: Make both circuits operate on two qubits
Equivalence for Two Qubits: not_equivalent

Case 2: Append measurements to the end of the circuit
malloc_consolidate(): invalid chunk size
Aborted

Case 1 + 2: Make both circuits operate on two qubits and append measurements
Equivalence for Two Qubits with Measurements: not_equivalent

Details: Reproducible Code

The output above was created by running this code:

# Case 1: Make both circuits operate on two qubits
qasm_a_two_qubits = """OPENQASM 2.0;
include "qelib1.inc";
qreg q[2];
rz(1) q[0];"""

qasm_b_two_qubits = """OPENQASM 2.0;
include "qelib1.inc";
qreg q[2];
swap q[0],q[1];"""

# Case 2: Append measurements to the end of the circuit
qasm_a_with_measurements = """OPENQASM 2.0;
include "qelib1.inc";
qreg q[1];
creg c[1];
rz(1) q[0];
measure q[0] -> c[0];"""

qasm_b_with_measurements = """OPENQASM 2.0;
include "qelib1.inc";
qreg q[3];
creg c[3];
swap q[1],q[2];
measure q[1] -> c[1];
measure q[2] -> c[2];"""

# Case 1 + 2: Make both circuits operate on two qubits and append measurements
qasm_a_two_qubits_with_measurements = """OPENQASM 2.0;
include "qelib1.inc";
qreg q[2];
creg c[2];
rz(1) q[0];
measure q[0] -> c[0];
measure q[1] -> c[1];"""

qasm_b_two_qubits_with_measurements = """OPENQASM 2.0;
include "qelib1.inc";
qreg q[2];
creg c[2];
swap q[0],q[1];
measure q[0] -> c[0];
measure q[1] -> c[1];"""

# Write the new QASM strings to files
path_qasm_a_two_qubits = "qasm_a_two_qubits.qasm"
path_qasm_b_two_qubits = "qasm_b_two_qubits.qasm"
path_qasm_a_with_measurements = "qasm_a_with_measurements.qasm"
path_qasm_b_with_measurements = "qasm_b_with_measurements.qasm"
path_qasm_a_two_qubits_with_measurements = "qasm_a_two_qubits_with_measurements.qasm"
path_qasm_b_two_qubits_with_measurements = "qasm_b_two_qubits_with_measurements.qasm"

with open(path_qasm_a_two_qubits, 'w') as file:
    file.write(qasm_a_two_qubits)

with open(path_qasm_b_two_qubits, 'w') as file:
    file.write(qasm_b_two_qubits)

with open(path_qasm_a_with_measurements, 'w') as file:
    file.write(qasm_a_with_measurements)

with open(path_qasm_b_with_measurements, 'w') as file:
    file.write(qasm_b_with_measurements)

with open(path_qasm_a_two_qubits_with_measurements, 'w') as file:
    file.write(qasm_a_two_qubits_with_measurements)

with open(path_qasm_b_two_qubits_with_measurements, 'w') as file:
    file.write(qasm_b_two_qubits_with_measurements)

# Define the content for the three Python files
content_case1 = f"""
from mqt import qcec

# Case 1: Make both circuits operate on two qubits
result_two_qubits = qcec.verify(
    str('{path_qasm_a_two_qubits}'),
    str('{path_qasm_b_two_qubits}'),
    transform_dynamic_circuit=True)
equivalence_two_qubits = str(result_two_qubits.equivalence)
print(f"Equivalence for Two Qubits: {{equivalence_two_qubits}}")
"""

content_case2 = f"""
from mqt import qcec

# Case 2: Append measurements to the end of the circuit
result_with_measurements = qcec.verify(
    str('{path_qasm_a_with_measurements}'),
    str('{path_qasm_b_with_measurements}'),
    transform_dynamic_circuit=True)
equivalence_with_measurements = str(result_with_measurements.equivalence)
print(f"Equivalence with Measurements: {{equivalence_with_measurements}}")
"""

content_case1_2 = f"""
from mqt import qcec

# Case 1 + 2: Make both circuits operate on two qubits and append measurements
result_two_qubits_with_measurements = qcec.verify(
    str('{path_qasm_a_two_qubits_with_measurements}'),
    str('{path_qasm_b_two_qubits_with_measurements}'),
    transform_dynamic_circuit=True)
equivalence_two_qubits_with_measurements = str(result_two_qubits_with_measurements.equivalence)
print(f"Equivalence for Two Qubits with Measurements: {{equivalence_two_qubits_with_measurements}}")
"""

# Write the content to the respective files
with open('verify_two_qubits.py', 'w') as file_two_qubits:
    file_two_qubits.write(content_case1)

with open('verify_with_measurements.py', 'w') as file_with_measurements:
    file_with_measurements.write(content_case2)

with open('verify_two_qubits_with_measurements.py', 'w') as file_two_qubits_with_measurements:
    file_two_qubits_with_measurements.write(content_case1_2)


# Run the three Python files and show the output

print("Case 1: Make both circuits operate on two qubits")
!python verify_two_qubits.py
print("\nCase 2: Append measurements to the end of the circuit")
!python verify_with_measurements.py
print("\nCase 1 + 2: Make both circuits operate on two qubits and append measurements")
!python verify_two_qubits_with_measurements.py

[MattePalte]

And also using the latest branch in a conda environment leads to the same result.

[burgholzer]

Thanks for running these! 🙏
That certainly helps to track down the error. Really seems like it is due to mismatch in the number of qubits in both computations and how we handle this at the moment.

To be fair, I don't think it's possible to always get the scenario right where the two circuits act on different numbers of qubits. QCEC should definitely not segfault anyhow. So this is still a bug that needs fixing.

I am tempted more and more to just hide the fact that QCEC can handle some specific cases where the circuits have a different amount of qubits behind an opt-in flag and introduce even stricter checks for the scenarios that we can handle.

[MattePalte]

I understand your concerns on the possible complexity of handling circuits of different sizes, however it is also a very valuable feature to have, especially when we want to verify the equivalence of two implementations (e.g. with and without ancilla) that implement the same operation (e.g., adder).

In those case I imagine we can either:

1. ask the user to configure which qubits of the smallest circuit should be compared with those in the bigger one,
2. simply assume that the ancillas of the larger ones are that come with largest indices (probably a reasonable default).

But the final decision is of course on your side.

[burgholzer]

I understand your concerns on the possible complexity of handling circuits of different sizes, however it is also a very valuable feature to have, especially when we want to verify the equivalence of two implementations (e.g. with and without ancilla) that implement the same operation (e.g., adder).

In those case I imagine we can either:

1. ask the user to configure which qubits of the smallest circuit should be compared with those in the bigger one,
2. simply assume that the ancillas of the larger ones are that come with largest indices (probably a reasonable default).

But the final decision is of course on your side.

Number 2 is actually what we kind of do in QCEC right now. And I agree that having this kind of functionality is useful out of the box.

I am now back from vacation and have started looking into this. I can reproduce the segfaults with v2.7.1 and v2.8.1. However, I can no longer reproduce them with the current main branch.
Specifically, running the following script

# /// script
# requires-python = ">=3.9"
# dependencies = [
#     "mqt-qcec",
# ]
#
# [tool.uv.sources]
# mqt-qcec = { git = "https://github.com/cda-tum/mqt-qcec", rev = "main" }
# ///

from __future__ import annotations

from pathlib import Path

from mqt.qcec import verify

if __name__ == "__main__":
    path_qasm_1 = Path("qasm_a.qasm")
    path_qasm_2 = Path("qasm_b.qasm")

    # write the first program to file qasm_a.qasm
    with path_qasm_1.open("w") as file:
        file.write(
            "OPENQASM 2.0;\n"
            'include "qelib1.inc";\n'
            "qreg q[1];\n"
            "rz(1) q[0];"
        )

    # write the second program to file qasm_b.qasm
    with path_qasm_2.open("w") as file:
        file.write(
            "OPENQASM 2.0;\n"
            'include "qelib1.inc";\n'
            "qreg q[3];\n"
            "swap q[1],q[2];"
        )

    result = verify(
        str(path_qasm_1),
        str(path_qasm_2))
    print(result.equivalence)

with uv run reproducer.py (checkout uv if you have noy yet: https://docs.astral.sh/uv/; gamechanger) simply prints

[QCEC] Warning: at least one of the circuits has garbage qubits, but partial equivalence checking is turned off. In order to take into account the garbage qubits, enable partial equivalence checking. Consult the documentation for moreinformation.
not_equivalent

which is the expected outcome in this case.

I am pretty sure this is because one of the updates that came with #531 or #534.
If you could somehow confirm the above, I am happy to cut a new patch release soon.

(Side note: I am currently working on the next major release in #432. the release will likely also include #443. No precise timeline yet)