Skip to content

Conversation

@zhenrongliew
Copy link
Contributor

@zhenrongliew zhenrongliew commented Nov 7, 2025

no-cloning validation analysis with a validation framework to compose multiple validation analyses. Implemented using a lattice for tracking definite and potential cloning violations. Addresses this issue.

    Linear ordering (more precise --> less precise):
      Bottom (proven safe / never occurs)  ⊑ Must (definitely occurs) ⊑ May (possibly occurs) ⊑ Top (unknown / no information)

For example this kernel has 1 definite and 1 potential violation of the no-cloning theorem.

@squin.kernel
def kernel(a: int):
    q = squin.qalloc(5)
    squin.cx(q[0], q[1])
    squin.cx(q[1], q[1])  # definite violation
    squin.cx(q[a], q[2])  # potential violation

IR printing:

func.func kernel(!py.int) -> !py.NoneType {
  ^0(%kernel_self, %a):
  │   %kernel_self --> ⊥ (No Errors)
  │   %a --> ⊤ (Unknown)
  │  %0 = py.constant.constant 5 : !py.int # ---> ⊥ (No Errors)
  │  %q = func.invoke qalloc(%0) : !py.IList[!py.Qubit, !Any] maybe_pure=False # ---> ⊥ (No Errors)
  │  %1 = py.constant.constant 0 : !py.int # ---> ⊥ (No Errors)
  │  %2 = py.indexing.getitem(%q, %1) : !py.Qubit # ---> ⊥ (No Errors)
  │  %3 = py.constant.constant 1 : !py.int # ---> ⊥ (No Errors)
  │  %4 = py.indexing.getitem(%q, %3) : !py.Qubit # ---> ⊥ (No Errors)
  │  %5 = func.invoke cx(%2, %4) : !py.NoneType maybe_pure=False # ---> ⊥ (No Errors)
  │  %6 = py.constant.constant 1 : !py.int # ---> ⊥ (No Errors)
  │  %7 = py.indexing.getitem(%q, %6) : !py.Qubit # ---> ⊥ (No Errors)
  │  %8 = py.constant.constant 1 : !py.int # ---> ⊥ (No Errors)
  │  %9 = py.indexing.getitem(%q, %8) : !py.Qubit # ---> ⊥ (No Errors)
  │ %10 = func.invoke cx(%7, %9) : !py.NoneType maybe_pure=False # ---> Must(frozenset({'Qubit[1] on CX Gate'}))
  │ %11 = py.indexing.getitem(%q, %a : !py.int) : !py.Qubit # ---> ⊥ (No Errors)
  │ %12 = py.constant.constant 2 : !py.int # ---> ⊥ (No Errors)
  │ %13 = py.indexing.getitem(%q, %12) : !py.Qubit # ---> ⊥ (No Errors)
  │ %14 = func.invoke cx(%11, %13) : !py.NoneType maybe_pure=False # ---> May(frozenset({'CX Gate, with unknown argument a'}))
  │ %15 = func.const.none() : !py.NoneType # ---> ⊥ (No Errors)
  │       func.return %15
} // func.func kernel

Validation reporting:

Error: Cloning qubit [1] at CX gate
  File "/Users/Documents/kirin-workspace/bloqade-circuit/test/analysis/validation/test_no_cloning.py", line 159, col 4
     │  q = squin.qalloc(5)
     │  squin.cx(q[0], q[1])
  159│  squin.cx(q[1], q[1])
     │  ^^^^^^^^^^^^^^^^^^^^
     │  squin.cx(q, q[2])


Warning: Potential cloning at CX gate, with unknown argument a
  File "/Users/Documents/kirin-workspace/bloqade-circuit/test/analysis/validation/test_no_cloning.py", line 160, col 4
     │  squin.cx(q[0], q[1])
     │  squin.cx(q[1], q[1])
  160│  squin.cx(q, q[2])
     │  ^^^^^^^^^^^^^^^^^^^^

No-Cloning Validation Analysis Implementation

  • Added a new NoCloningValidation class in analysis.py that tracks qubit usage and detects cloning violations, distinguishing between definite (Must) and potential (May) errors.
  • Defined a QubitValidation lattice in lattice.py with four states (Bottom, Must, May, Top), supporting precise tracking and merging of violation information.

Testing

  • Added tests in test_no_cloning.py to verify detection of cloning violations in various scenarios, including various control gates, conditionals, and parallel gates,.

Composite Validation Framework Usage:

suite = ValidationSuite(
    [
        NoCloningValidation,
        SomeValidation,
        AnotherValidation,
    ]
)
result = suite.validate(my_kernel)

@zhenrongliew zhenrongliew linked an issue Nov 7, 2025 that may be closed by this pull request
@zhenrongliew zhenrongliew self-assigned this Nov 7, 2025
@codecov
Copy link

codecov bot commented Nov 7, 2025

@github-actions
Copy link
Contributor

github-actions bot commented Nov 7, 2025

☂️ Python Coverage

current status: ✅

Overall Coverage

Lines Covered Coverage Threshold Status
10524 9176 87% 0% 🟢

New Files

File Coverage Status
src/bloqade/analysis/validation/nocloning/_init_.py 100% 🟢
src/bloqade/analysis/validation/nocloning/analysis.py 94% 🟢
src/bloqade/analysis/validation/nocloning/impls.py 80% 🟢
src/bloqade/analysis/validation/nocloning/lattice.py 41% 🟢
src/bloqade/analysis/validation/validationpass.py 84% 🟢
TOTAL 80% 🟢

Modified Files

No covered modified files...

updated for commit: b572471 by action🐍

@zhenrongliew zhenrongliew marked this pull request as ready for review November 7, 2025 16:03
@zhenrongliew zhenrongliew marked this pull request as draft November 10, 2025 15:23
@zhenrongliew
Copy link
Contributor Author

@zhenrongliew zhenrongliew marked this pull request as ready for review November 12, 2025 17:23
self, frame: ForwardFrame[QubitValidation], node: ir.Statement
) -> tuple[QubitValidation, ...]:
"""Check for qubit usage violations and return lattice values."""
if not isinstance(node, func.Invoke):
Copy link
Collaborator

Choose a reason for hiding this comment

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

Just some questions for my understanding:

Why is this not a method impl for func.Invoke?

Also, this seems to be assuming that all func.Invoke are stdlib functions. What if a user calls their own subroutine? If I understand correctly, this will result in an error for that if the user-defined function has any qubit arguments whose addresses overlap. Is that correct and expected?

Just to be clear: I don't really see a (valid) use-case when a user would do that, but then again it's very simple to write a kernel function that is perfectly valid even when called with overlapping qubit arguments.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Currently, the analysis is able to distinguish between safe user-defined functions and unsafe ones.
e.g. foo is called with overlapping qubit 1 but it's implementation is safe:

@squin.kernel
def kernel(a: int):
    q = squin.qalloc(4)
    squin.cx(q[0], q[0])  # definite cloning error
    def foo(q1, q2):
        squin.cx(q1,q[3])
    foo(q[1], q[1]) 

This is the reported error:

Validation failed with 1 violation(s):

No-Cloning Validation:
  - Qubit[0] cloned at CX gate.
      File "/Users/Documents/kirin-workspace/bloqade-circuit/test/analysis/validation/test_compose_validation.py", line 12, col 4
    │  def kernel(a: int):
    │      q = squin.qalloc(4)
  12│      squin.cx(q[0], q[0])  # definite cloning error
    │      ^^^^^^^^^^^^^^^^^^^^
    │      def foo(q1, q2):
    │          squin.cx(q1,q[3])
    │      foo(q[1], q[1]) 
 (1 sub-exception)

And here is an unsafe user defined function:

@squin.kernel
def kernel(a: int):
   q = squin.qalloc(4)
   squin.cx(q[0], q[0])  # definite cloning error
   def foo(q1, q2):
       squin.cx(q1,q2)
   foo(q[1], q[1]) 

The report:

Validation failed with 2 violation(s):

No-Cloning Validation:
 - Qubit[0] cloned at CX gate.
     File "/Users/Documents/kirin-workspace/bloqade-circuit/test/analysis/validation/test_compose_validation.py", line 12, col 4
   │  def bad_kernel(a: int):
   │      q = squin.qalloc(4)
 12│      squin.cx(q[0], q[0])  # definite cloning error
   │      ^^^^^^^^^^^^^^^^^^^^
   │      def foo(q1, q2):
   │          squin.cx(q1,q2)
   │      foo(q[1], q[1]) 

 - Qubit[1] cloned at FOO gate.
     File "/Users/Documents/kirin-workspace/bloqade-circuit/test/analysis/validation/test_compose_validation.py", line 15, col 4
   │  def foo(q1, q2):
   │      squin.cx(q1,q2)
 15│  foo(q[1], q[1]) 
   │  ^^^
(2 sub-exceptions)

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Granted this error message might be a little misleading: "Qubit[1] cloned at FOO gate."

Copy link
Collaborator

Choose a reason for hiding this comment

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

I understand, but what I mean is this: if I change foo in the above to e.g.

def foo(q1, q2):
    squin.x(q1)
    squin.x(q2)

then calling foo(q[0], q[0]) is fine since there's no overlapping operation. Still, this will be reported as an error.
Again, I don't see a valid use case for this (why would you want to write something like the above?), but I just wanted to make sure this behavior was expected.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Oh I see what you mean now. No, that behavior is not expected.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I guess we could introduce some heuristic to define what function is a stdlib function and only then apply the analysis. @Roger-luo is there a way to do this via modules in kirin as of yet?

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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Qubits violating linear type

4 participants