Verifying Logical Clifford Gadgets

Motivation: Logical Cliffords can have non-obvious implementations, especially for \(k>1\) codes. We want to be able to validate implementations and catch bugs in our logical gadgets.

For example, see Table 2 from Simple logical quantum computation with concatenated symplectic double codes. Below is a section of this table that shows the physical implementation and logical action for

  • The guppyft.verify module checks logical Clifford semantics against physical implementation, using the valid_clifford_implementation function.

  • The tool works for \(k>1\) codes and also operations between two code blocks.

  • This approach is fairly general and works for any stabilizer code. Includes non-CSS codes.

We will specify the logical semantics with a Guppy function which acts on an array of \(k\) qubits. Let’s see an example for the \([[7, 1, 3]]\) Steane code. The action of a logical Hadamard in the Steane code is as follows…

from guppylang import guppy
from guppylang.std.builtins import array
from guppylang.std.quantum import qubit, h


@guppy
def steane_specify_h(qs: array[qubit, 1]) -> None:
    h(qs[0])

We can provide the implementation of the logical operation as a function which acts on an array of \(n\) physical qubits.

@guppy
def steane_impl_h(block: array[qubit, 7]) -> None:
    for i in range(len(block)):
        h(block[i])

The verifier then calculates the Clifford tableau of both of them, and checks that they are equivalent. Since the logical specification is in terms of \(k\) logical qubits and the implementation is in terms of \(n\) physical qubits, we need to expand the tableau of \(k\) logical qubits to \(n\) physical, using the definition of the stabilizer code. The definition of the stabilizer code tells us how to replace a logical Pauli with its physical Pauli string realization, as well as which additional Pauli strings we need to introduce to account for the code’s stabilizer group.

Providing the stabilizer code definition

Before we can get to verifying logical Cliffords, we need a way to specify the key properties of a stabilizer code. We provide a StabilizerCode dataclass which specifies the \([[n, k, d]]\) code parameters as integers as well as the stabilizer generators and logical operators.

@dataclass(frozen=True)
class StabilizerCode:
    num_physical_qubits: int
    num_logical_qubits: int
    distance: int
    generators: pauli.SignTermSet
    x_logicals: pauli.SignTerms
    z_logicals: pauli.SignTerms

The stabilizer generators and logical operators are represented using types from Zixy, a library which provides memory efficient Pauli operator implementations in Rust.

A StabilizerCode definition can be given by specifying the fields directly. However its usually easier to use the from_python_strings utility method.

Let’s provide definitions for the Steane code.

from guppyft.code_def import StabilizerCode

STEANE_DEF = StabilizerCode.from_python_strings(
    num_physical_qubits=7,
    num_logical_qubits=1,
    distance=3,
    generators=["XXXXIII", "IXXIXXI", "IIXXIXX", "ZZZZIII", "IZZIZZI", "IIZZIZZ"],
    x_logicals=["XXXXXXX"],
    z_logicals=["ZZZZZZZ"],
)

We can also provide a code definition for the non-CSS \([[4, 2, 2]]\) code which is discussed in the paper entitled “Simple logical quantum computation with concatenated symplectic double codes” (N. Berthusen and E. Durso-Sabina - https://arxiv.org/pdf/2510.18753)

With non-CSS codes, each stabilizer generator can be made ofa mixture of \(X\) and \(Z\) operators. The same is true of the logical operators.

NON_CSS_4_2_2 = StabilizerCode.from_python_strings(
    num_physical_qubits=4,
    num_logical_qubits=2,
    distance=2,
    generators=["XZZX", "ZXXZ"],
    x_logicals=["ZIXI", "IZIX"],
    z_logicals=["IZZI", "ZIIZ"],
)

There is some basic __post_init__ validation to check we are providing reasonable StabilizerCode definitions.

For example, all of the stabilizer generators must commute with one another. If they do not mutually commute, then the code definition is rejected.

Verifying the implementation of logical Cliffords

Now we can get on to verifying logical operations. We’ll start by verifying some operations functions in the Steane code. This is done with the valid_clifford_implementation function.

from guppyft.verify import valid_clifford_implementation

Basic examples for the Steane code

First, let’s check the logical Hadamard implementation we defined above.

valid_clifford_implementation(
    steane_specify_h, steane_impl_h, STEANE_DEF
)  # True => implementation is valid

True

We can also verify operators between two code blocks. As an example, let’s verify the implementation of the transversal CX in the Steane code.

from guppylang.std.quantum import cx


@guppy
def steane_specify_cx(
    first_block: array[qubit, 1], second_block: array[qubit, 1]
) -> None:
    cx(first_block[0], second_block[0])


@guppy
def steane_impl_cx(first_block: array[qubit, 7], second_block: array[qubit, 7]) -> None:
    for i in range(len(first_block)):
        cx(first_block[i], second_block[i])

valid_clifford_implementation(
    steane_specify_cx, steane_impl_cx, STEANE_DEF
)  # Transversal CX impl is valid.

True

We can also detect invalid implementations. If we try to implement a logical \(S\) gate in the Steane code by applying physical \(S\) across across all seven physical qubits, we get False indicating that our implementation of logical \(S\) is wrong.

from guppylang.std.quantum import s


@guppy
def steane_specify_s(block: array[qubit, 1]) -> None:
    s(block[0])


@guppy
def steane_impl_s_incorrect(block: array[qubit, 7]) -> None:
    for i in range(len(block)):
        s(block[i])


valid_clifford_implementation(
    steane_specify_s, steane_impl_s_incorrect, STEANE_DEF
)  # Invalid!

False

It turns out the correct way to implement logical \(S\) in the Steane code is by applying \(S^\dagger\) across the physical qubits.

from guppylang.std.quantum import sdg


@guppy
def steane_impl_s_corrected(block: array[qubit, 7]) -> None:
    for i in range(len(block)):
        sdg(block[i])


valid_clifford_implementation(
    steane_specify_s, steane_impl_s_corrected, STEANE_DEF
)  # Now valid!

True

Examples for \(k>1\) codes

So far, the examples with the Steane code have just been simple transversal operations. However, logical Clifford operations for \(k > 1\) codes can also be verified. Let’s consider the \(k = 2\) CSS \([[ 4 , 2 , 2 ]]\) code to see this

CSS_4Q_DEF = StabilizerCode.from_python_strings(
    num_physical_qubits=4,
    num_logical_qubits=2,
    distance=2,
    generators=["XXXX", "ZZZZ"],
    x_logicals=["XXII", "XIXI"],
    z_logicals=["IZIZ", "IIZZ"],
)

In this \([[4, 2, 2]]\) code, we can implement a logical CX gate (intrablock) by simply swapping the physical qubits.

from guppylang.std.mem import mem_swap


@guppy
def specify_intra_block_cx(block: array[qubit, 2]) -> None:
    cx(block[0], block[1])


@guppy
def implement_intra_block_cx(block: array[qubit, 4]) -> None:
    mem_swap(block[3], block[1])

valid_clifford_implementation(
    specify_intra_block_cx, implement_intra_block_cx, CSS_4Q_DEF
)

True

We can also verify the implementation of logical SWAP in the non-CSS \([[4, 2, 2]]\) code. This is implemented by applying the Hadamard gate to all of the physical qubits.

@guppy
def specify_swap_non_css(block: array[qubit, 2]) -> None:
    mem_swap(block[0], block[1])


@guppy
def implement_swap_non_css(block: array[qubit, 4]) -> None:
    for i in range(len(block)):
        h(block[i])

valid_clifford_implementation(
    specify_swap_non_css,
    implement_swap_non_css,
    NON_CSS_4_2_2,
)

True

Verifying preparation of logical Pauli eigenstates

The testing framework also allows us to verify state preparation. For example we can check preparation of logical \(|0\rangle\) \(\big(|0\rangle_{L}\big)\) in the \([[4, 2, 2]]\) code as follows.

from guppyft.verify import valid_stabilizer_state_preparation


@guppy
def specify_zero_state() -> array[qubit, 2]:
    return array(qubit() for _ in range(2))


@guppy
def implement_non_ft_zero_state() -> array[qubit, 4]:
    block = array(qubit() for _ in range(4))

    h(block[0])
    cx(block[0], block[1])
    cx(block[0], block[2])
    cx(block[0], block[3])
    return block

valid_stabilizer_state_preparation(
    specify_zero_state, implement_non_ft_zero_state, CSS_4Q_DEF
)

True

Explaining the verifier step by step

Let’s go back to the logical Hadamard in Steane. How do we work out that logical Hadamard can be implemented by broadcasting a Hadamard gate across all seven physical qubits?

Firstly we calculate the stabilizers of a \(2k\) qubit Choi state which encodes the logical Hadamard.

from guppyft.verify._verify import _compute_stabilizers_single_block_unitary
from guppyft.verify._expansion import get_expanded_stabilizer_set
from guppyft.code_def import identity_code


# Get the 2k stabilizers for the 2k qubit Choi state encoding the logical operation.
semantic_choi_stabilizers = _compute_stabilizers_single_block_unitary(
    code=identity_code(k=1),
    clifford_func=steane_specify_h,
    num_selene_qubits=2 * STEANE_DEF.num_logical_qubits,
)
semantic_choi_stabilizers.to_dataframe()
Component Coefficient
0 X0 Z1 +1
1 Z0 X1 +1

Notice how the stabilizers are closely related to the stabilizers of the Bell state \(\{X_0X_1, Z_0Z_1\}\) but with a logical Hadamard applied to \(X_1\) and \(Z_1\).

Next, we expand the \(2k\) logical stabilizers to \(2k\) stabilizers of size \(2n\). We also add the \(2(n-k)\) stabilizer generators of our code. For each code block there are \(n-k\) generators, so \(2\) blocks give us \(2(n-k)\). We have \(2k + 2(n-k) = 2n\) stabilizers in total.

We perform this expansion using the definition of the logical operators for the particular StabilizerCode we are working with. For the Steane code, we do the following expansion:

\[ X_L \mapsto XXXXXXX\, \qquad Z_L \mapsto ZZZZZZZ\,. \]
expanded_semantic_stabilizers = get_expanded_stabilizer_set(
    semantic_choi_stabilizers, STEANE_DEF, num_blocks=2
)

expanded_semantic_stabilizers.to_dataframe()
Component Coefficient
0 X0 X1 X2 X3 X4 X5 X6 Z7 Z8 Z9 Z10 Z11 Z12 Z13 +1
1 Z0 Z1 Z2 Z3 Z4 Z5 Z6 X7 X8 X9 X10 X11 X12 X13 +1
2 X0 X1 X2 X3 +1
3 X1 X2 X4 X5 +1
4 X2 X3 X5 X6 +1
5 Z0 Z1 Z2 Z3 +1
6 Z1 Z2 Z4 Z5 +1
7 Z2 Z3 Z5 Z6 +1
8 X7 X8 X9 X10 +1
9 X8 X9 X11 X12 +1
10 X9 X10 X12 X13 +1
11 Z7 Z8 Z9 Z10 +1
12 Z8 Z9 Z11 Z12 +1
13 Z9 Z10 Z12 Z13 +1

In order test two tableaux for equality, we have to convert to a suitable normal form. This is because two tableaux which look different can be equivalent up to multiplication by a Pauli stabilizer. We canonicalize the tableaux using the SignTerms.canonicalize_all() method which uses a process similar to Gaussian elimination.

expanded_semantic_stabilizers.canonicalize_all()  # Canonicalize Clifford tableau
expanded_semantic_stabilizers.to_dataframe()
Component Coefficient
0 X0 X3 X6 Z11 Z12 Z13 +1
1 X1 X3 X5 Z11 Z12 Z13 +1
2 X2 X3 X5 X6 +1
3 X4 X5 X6 Z11 Z12 Z13 +1
4 Z4 Z5 Z6 X7 X10 X13 +1
5 Z4 Z5 Z6 X8 X10 X12 +1
6 X9 X10 X12 X13 +1
7 Z4 Z5 Z6 X11 X12 X13 +1
8 Z0 Z3 Z4 Z5 +1
9 Z1 Z3 Z4 Z6 +1
10 Z2 Z3 Z5 Z6 +1
11 Z7 Z10 Z11 Z12 +1
12 Z8 Z10 Z11 Z13 +1
13 Z9 Z10 Z12 Z13 +1

Now we calculate the \(2n\) stabilizers of the Choi state encoding the \(n\) qubit implementation of the logical operation. In this case, the physical Hadamard acts on seven qubits. Therefore we expect our implementation tableau to contain \(2*7 =14\) Pauli stabilizers.

# Calculate the 2n stabilizers of the Choi state encoding the physical operation.
implementation_stabilizers = _compute_stabilizers_single_block_unitary(
    STEANE_DEF, steane_impl_h, num_selene_qubits=2 * (STEANE_DEF.num_physical_qubits)
)
implementation_stabilizers.to_dataframe()
Component Coefficient
0 X0 X3 X6 Z11 Z12 Z13 +1
1 Z0 Z3 Z6 X11 X12 X13 +1
2 X1 X3 X5 Z11 Z12 Z13 +1
3 Z1 Z3 Z5 X11 X12 X13 +1
4 X2 X3 X5 X6 +1
5 Z2 Z3 Z5 Z6 +1
6 X4 X5 X6 Z11 Z12 Z13 +1
7 Z4 Z5 Z6 X11 X12 X13 +1
8 X7 X10 X11 X12 +1
9 Z7 Z10 Z11 Z12 +1
10 X8 X10 X11 X13 +1
11 Z8 Z10 Z11 Z13 +1
12 X9 X10 X12 X13 +1
13 Z9 Z10 Z12 Z13 +1

We now canonicalize these implementation stabilizers as we did above for the semantic stabilizers.

implementation_stabilizers.canonicalize_all()  # Canonicalize Clifford tableau
implementation_stabilizers.to_dataframe()
Component Coefficient
0 X0 X3 X6 Z11 Z12 Z13 +1
1 X1 X3 X5 Z11 Z12 Z13 +1
2 X2 X3 X5 X6 +1
3 X4 X5 X6 Z11 Z12 Z13 +1
4 Z4 Z5 Z6 X7 X10 X13 +1
5 Z4 Z5 Z6 X8 X10 X12 +1
6 X9 X10 X12 X13 +1
7 Z4 Z5 Z6 X11 X12 X13 +1
8 Z0 Z3 Z4 Z5 +1
9 Z1 Z3 Z4 Z6 +1
10 Z2 Z3 Z5 Z6 +1
11 Z7 Z10 Z11 Z12 +1
12 Z8 Z10 Z11 Z13 +1
13 Z9 Z10 Z12 Z13 +1

Now that we have two Clifford tableaux in a suitable normal form, we can test them for equality.

expanded_semantic_stabilizers == implementation_stabilizers

True

Summary of available features

The following features are available for verification of Clifford operations with valid_clifford_implementation

  • Works for \(k>1\) codes

  • Works for operations on a single logical block or between two logical blocks

  • Works for non-CSS codes (e.g. the \([[5, 1, 3]]\) code)

  • Ancilla qubits can be used in the implementation

The features above are also available in valid_stabilizer_state_preparation which can be used to verify the preparation of logical Pauli eigenstates (e.g. \(|0\rangle_L\), \(|+\rangle_L\))