MBUndo: Sound, Automatic, and Efficient Measurement-Based Uncomputation for Quantum Circuits

Introduction

Like classical programs, quantum programs that implement quantum algorithms generate temporary values as part of execution. These values are stored in ancilla qubits alongside the data qubits that store the ultimate output of the computation. Classically, any temporary value can simply be discarded and destroyed once used. But in a quantum program, ancilla qubits are entangled with the data qubits they are computed from, meaning that destroying a temporary value can also corrupt the program state and jeopardize correctness of the program [40 §4].

The remedy for this problem is uncomputation [9], the process of undoing the computation of a temporary value to explicitly return it to zero and thereby eliminate all entanglement with the data qubits. Writing uncomputation by hand is common yet tedious and error-prone for programmers. Thus, researchers have developed techniques to automatically uncompute variables in programming languages [12, 26, 60] or qubits in the quantum circuits to which languages compile [35, 42, 44].

Unitary Uncomputation and Measurement-Based Uncomputation

Whether manual or automatic, uncomputation is typically [12, 26, 42, 44, 60, 67] implemented as a unitary operator — a series of quantum logic gates that do not perform measurement. This approach, which we will call unitary uncomputation, characteristically executes the inverse of every logic gate used to compute each ancilla qubit. Unitary uncomputation executes as many gates as the computation being undone, and thus accounts for up to half the runtime cost of a typical quantum circuit.

Measurement-based uncomputation (MBU) is an alternative to unitary uncomputation introduced by Gidney [ [21, 22] that can be far cheaper. Figure 1a depicts a unitary uncomputation circuit and the MBU it is equivalent to. Both circuits start with an ancilla $a$ holding a temporary $f(x)$, computed from data qubits $x$, that is no longer needed. The starting program state is $\sum_x \alpha_x \lvert x\rangle\lvert f(x)\rangle$, which uncomputation must transform to $\sum_x \alpha_x |x\rangle|0\rangle_a$, zeroing the ancilla while leaving the data qubits unaffected. To do so, unitary uncomputation runs the inverse of the circuit that computed $f(x)$. This operation, denoted $\oplus f(x)$, repeats the cost of the original computation of $f(x)$.

By contrast, MBU cleans up the ancilla $a$ by performing a destructive $X$-basis measurement — it applies a Hadamard gate and then measures $a$ in the computational basis. This $H$ gate transforms the state into $\frac{1}{\sqrt{2}}\left(\sum_x \alpha_x |x\rangle|0\rangle_a + \sum_x \alpha_x(-1)^{f(x)} |x\rangle|1\rangle_a\right)$, so measuring $a$ yields 0 or 1 with equal probability. Upon outcome 0, the state collapses to $\sum_x \alpha_x |x\rangle|0\rangle_a$, which is already the desired state. Upon outcome 1, the state collapses to $\sum_x \alpha_x(-1)^{f(x)} |x\rangle|1\rangle_a$, where the ancilla can be safely reset to zero, but the data qubits retain an unwanted phase $(-1)^{f(x)}$ that depends on $x$. MBU thus concludes with a phase correction, controlled on $x$ and outcome 1, to cancel this phase.

To see why MBU is often cheaper than unitary uncomputation, consider its simplest and best-known instantiation, which is for a Toffoli gate — the quantum analogue of AND. Figure 1b shows how when an ancilla holds $x_1x_2 = x_1 \land x_2$, unitary uncomputation executes a Toffoli gate controlled on $x_1$ and $x_2$ ($\oplus$ and Toffoli are self-inverse). MBU instead performs an $X$-basis measurement and then a single controlled-$Z$ (CZ) gate, when the outcome is 1, to cancel the phase $(-1)^{x_1x_2}$.

MBU is cheaper here because on a fault-tolerant quantum computer, a Toffoli gate costs much more than the measurement, $H$, and CZ gates that replace it. Toffoli is not a Clifford gate, meaning that realizing it on a quantum error-correcting code requires decomposing Toffoli into elementary gates including the $T$ gate, which is a major architectural bottleneck on hardware Beverland et al. [11]. Even after recent advances that substantially reduce the cost of $T$ gates, each $T$ gate is still expected to have cost equivalent to multiple lattice surgery operations on the surface code Gidney et al. [24], whereas Clifford gates and single-qubit measurements frequently require none Litinski [34]. One Toffoli gate costs between four to seven $T$ gates, depending on the decomposition Jones [29]; Selinger [51]. Hadamard and CZ gates are Clifford gates, which cost zero $T$ gates.

Moreover, the CZ gate is needed only half of the time, since with probability $\frac{1}{2}$ the measurement yields 0 and the uncomputation is complete. By applying MBU to an adder circuit, each of whose ancillas is computed by a Toffoli, Gidney [ [21] halves the $T$ count of quantum addition.

Automating Measurement-Based Uncomputation Soundly and Efficiently

To date, researchers have applied MBU to individual circuit designs Gidney [23]; Khattar et al. [30]; Yao et al. [65], including by generalizing Gidney’s rule (Figure 1b) to multiply-controlled-$X$ gates Amy and Ross [5]. Quantum programming frameworks such as Q# Svore et al. [56], Qualtran Harrigan et al. [25], and Qrisp Seidel et al. [50] automate MBU for Toffoli gates, via an AND primitive whose uncomputation is optimized as in Figure 1b for this three-qubit case.

But to date, no automatic transformation can take an arbitrary circuit, whose ancillas have been computed and uncomputed via the standard approach, and converts its unitary uncomputation into MBU. Such a transformation generalizes the benefit of MBU to circuits beyond those specifically designed and constructed to use it. In particular, it further enhances the value of existing synthesis methods for unitary uncomputation Liu et al. [35]; Paradis et al. [42, 44]; Venev et al. [60]. Making this transformation possible requires answering two fundamental questions:

Where does MBU apply? In complex circuits, either designed by hand or produced by uncomputation synthesizers, a physical ancilla wire is typically reused for several logical temporaries, each computed and uncomputed in turn, corresponding to multiple logical ancilla lifetimes. For example, given a 12-bit multiplier, the uncomputation synthesizer Unqomp [42] maps 144 ancilla lifetimes onto 23 physical ancilla wires. Each lifetime ends with the uncomputation of its temporary, so a wire offers several MBU opportunities rather than one. Correctly exploiting these opportunities requires reconstructing the lifetimes of each physical wire from an input circuit.

How is MBU realized in gates? Figure 1a specifies that MBU needs to realize $(-1)^{f(x)}$, but not how it can do so. For circuits [21, 65] where $f(x)$ is computed by one gate, one can apply Gidney’s rule in Figure 1b. When $f(x)$ needs many gates, Luongo et al. [ [37], Fig. 24 propose a different rule, shown in Figure 2. This rule, which we will call monolithic MBU, treats the unitary uncomputation circuit for $f(x)$ as an opaque block. In Figure 2, the block corresponds to the $\oplus f(x)$ component from Figure 1a. Instead of unconditionally executing this block, the rule performs an $X$-basis measurement and then conditionally executes the block. When the $X$-basis measurement of the ancilla yields 1, an $H$ gate brings the ancilla to $\lvert-\rangle$, the block kicks back the phase correction $(-1)^{f(x)}$ onto the data qubits, and subsequent $H$ and $X$ gates restore the ancilla to $\lvert0\rangle$.

Monolithic MBU has numerous shortcomings. First, only half the time does Figure 2 reduce the cost of the circuit at all. Unlike Gidney’s rule, it cannot exploit the structure of $f(x)$ to synthesize a phase correction that always has lower $T$ cost. Second, Figure 2 is only sound if the $\oplus f(x)$ block exists as a contiguous unit within the circuit, not interspersed with gates that affect other qubits. If the block included gates that modify the data $x$, then Figure 2 would corrupt the data. And if $f(x)$ is stored in multiple ancillas, Figure 2 fails to uncompute all but one. Both cases arise in practice.

This Work. In this paper, we answer the two fundamental questions above and establish the first automatic transformation from an arbitrary quantum circuit containing unitary uncomputation into one that uses measurement-based uncomputation and derives its performance benefits.

We answer the question of where to perform MBU in a circuit by presenting a static analysis that recovers the lifetimes of every ancilla via a symbolic execution tracking the basis value on each qubit. Using the analysis results, we answer how to realize MBU by incrementally constructing two circuit transformations to replace unitary uncomputation with MBU for each ancilla lifetime.

The first, endpoint MBU, directly automates the rule of Gidney [ [21] as generalized by Amy and Ross [ [5]. It converts the last uncomputation gate within each ancilla lifetime into a measurement and an appropriate phase correction gate. The second transformation, interval MBU, further turns a multi-gate unitary uncomputation for each ancilla into an efficient sequence of phase correction gates. Unlike the monolithic MBU of Luongo et al. [ [37], it replaces unitary uncomputation while guaranteeing soundness and minimizing $T$-gate cost. In § 2, we walk through examples to illustrate the challenges and insights behind the static analysis and both transformations.

We integrate our analyses and transformations into a tool, MBUndo, that programmers can use to automatically convert circuits to correct and efficient measurement-based uncomputation. MBUndo requires no user annotations on input circuits other than which qubits are ancillas – the same as required by existing uncomputation synthesizers such as Unqomp [42] and Recomp [44] – and can operate as a compiler pass on their output circuits.

We evaluate MBUndo using 22 benchmarks drawn from uncomputation synthesizers and quantum algorithms. Endpoint MBU reduces $T$ gates over Recomp by 36.5% in geomean. Interval MBU further reduces $T$ gates by another 2.3 to 18.4 percentage points for benchmarks containing multi-gate uncomputation. Moreover, MBUndo automatically matches 3 of 4 evaluated specialized MBU circuits from prior literature, and processes each benchmark within 43 ms on a laptop.

Contributions. In this work, we present the following contributions:

• § 3: A static analysis to identify the multiple logical lifetimes that exist on each physical ancilla in a circuit, maximizing opportunities to introduce measurement-based uncomputation.

• § 4.1: Endpoint MBU, a simple transformation that soundly automates the rule of Gidney [ [21] by converting the last uncomputation gate in each ancilla lifetime into a measurement.

• § 4.2: Interval MBU, a more advanced transformation that further converts a multi-gate unitary uncomputation for each ancilla into an efficient sequence of phase correction gates.

• § 5: MBUndo, a tool that integrates the analyses and transformations into a compiler pass that automatically enhances the output circuits of existing uncomputation synthesizers.

• § 6: An empirical evaluation of MBUndo’s performance on 22 benchmarks against uncomputation synthesizers, MBU circuits from prior work, and state-of-the-art circuit optimizers.

This work introduces into quantum compilers a powerful technique previously accessible only to expert circuit designers. As quantum programs become more complex and fault-tolerant devices come online, our contributions lower the barrier to practically executing them on hardware.

Overview and Examples

In this section, we explain the problem of transforming unitary uncomputation into measurement-based uncomputation. Using several example circuits, we illustrate the static analysis to determine ancilla lifetimes (§ 2.1) and the endpoint MBU transformation that soundly converts the final uncomputation gate in every ancilla lifetime to measurement (§ 2.2). We present the limitations of this method and associated challenges. Then, we present the interval MBU transformation that converts complex gate sequences to MBU (§ 2.3). We deliberately keep all examples simple, but they preview the structure of the practical applications that we evaluate in § 6.

Static Analysis for Ancilla Lifetimes: Discovering MBU Opportunities

We consider the circuit in Figure 3, which implements one round of a Feistel cipher [6], the structure underlying block ciphers such as DES. Given a function $F$, a round mixes half of its state into the other, mapping $(y,t)$ to $(t \oplus F,y)$. In this circuit, $F = y \oplus xy \oplus xyz$, and the implementation uses an ancilla wire $a$ as temporary scratch space to compute $F$.

Converting this circuit to MBU requires replacing with measurements the multiply-controlled X ($\mathrm{C}^{k}\mathrm{X}$; generalized Toffoli) gates that uncompute $a$ back to zero. The rule of Gidney [ [21] applies

to the final gate 8: its output leaves $a$ as zero, matching the rule in Figure 1b so that gate 8 can be soundly replaced by a measurement followed by an appropriate controlled-phase gate.

Lifetimes. Given the circuit as written, Gidney’s rule replaces gate 8 only. A second opportunity for MBU hides in the fact that Figure 3 uses $a$ to store two distinct temporaries in turn. Specifically, gate 1 computes $q=x\land y=xy$ into $a$, gate 3 uncomputes $q=xy$, gate 4 computes $p=xyz$, and gate 8 uncomputes $p=x'z't'$ (a different formula because $y$ is modified in the output).

Identifying that gate 3 also leaves $a$ as zero yields a second candidate for MBU, but this fact is invisible in Figure 3. Thus, in § 3 we present a static analysis that, given a circuit, soundly identifies MBU candidates for each distinct lifetime of a temporary value on each ancilla wire. This analysis requires no programmer input aside from which wires are zero when the circuit ends, i.e., which wires are ancillas. From this information, it performs a backward symbolic execution to find a conservative set of positions where ancillas are cleaned up to zero and are thus eligible for MBU.

Efficient Symbolic Values. To avoid the exponential blowup of explicit quantum states, our static analysis tracks the value of each qubit as a symbolic value, a Boolean function of data qubits. We define a symbolic value as a set of atoms joined by XOR ($\oplus$). The empty set represents 0, and a cheap symmetric difference of sets joins two values. Each atom is either a symbol for an unknown Boolean or a product of multiple symbolic values via $\land$. Our design is more compact than algebraic normal form (ANF) [69] as used by prior symbolic executors for quantum circuits [14]. It exploits usual algebraic laws of $\oplus$ and $\land$, such as $s\oplus s=0$ and $s\land s=ss=s$, but not the general distributivity of $\land$ over $\oplus$. Its number of atoms is linear in the number of gates, whereas ANF expands $(x\oplus y)(z\oplus w)\mapsto xz\oplus xw\oplus yz\oplus yw$ and is exponentially large in general.

Symbolic Execution. Our analysis starts from the end of the circuit, where the symbolic value of every ancilla is 0 and every data qubit has a fresh symbol for its unknown output (e.g., $y'$ and $t'$ for $y$ and $t$). It processes each gate from right to left. For a $C^kX$ gate, it XORs the product of symbolic values of the controls into the target; for a phase gate ($Z$, $S$, $T$), it leaves symbolic values unchanged; and for a basis-changing gate such as $H$, it conservatively replaces the target with a fresh symbol. Finally, the analysis delimits each lifetime of an ancilla by where its symbolic value is 0.

For the example, Figure 3 lists the symbolic values after each analysis step. Gate 8 XORs its controls $x$, $z$, and $t$ into $a$, which then stores the atom $p=x'z't'$. The CNOT gates 7 and 6 on $y$ and $t$ yield $t=t'\oplus y'$ and then $y=t'$. Gate 5 XORs $a=p$ into $t$. Gate 4 XORs its controls $x$, $y$, and $z$ into $a$, since $y=t'$, $xyz=x't'z'=p$ and the state of $a$ becomes $a=p\oplus p=0$. The analysis thus identifies a lifetime spanning gates 4–8, and continues on to identify a second lifetime from gates 1–3.

Result. Our static analysis soundly identifies, given an arbitrary circuit annotated only by which qubits are ancillas, a conservative set of lifetimes of distinct temporary values on each ancilla that each expose an opportunity for MBU to the transformations we present in the next section. Beyond the small example in Figure 3, our analysis can scalably handle more complex circuits. For instance, Figure 4 shows the 14 distinct lifetimes identified by our analysis on the polynomial Pauli rotation benchmark circuit constructed by Paradis et al. [ [42] in order to evaluate Unqomp.

Endpoint MBU: Soundly Applying Gidney’s Rule to Final Gates

Given lifetimes of each ancilla, one direct next step is to use Gidney’s rule at the end of each lifetime, as done manually by Gidney [ [21]; Yao et al. [ [65]. In § 4.1, we describe endpoint MBU, a circuit transformation that automates this rule in a simple and sound way. Figure 5 shows its result on the Feistel example from Figure 3, whose two unitary uncomputation gates are in purple.

Endpoint MBU converts the last gate of each lifetime into a measurement and phase correction. Amy and Ross [ [5] define the appropriate correction for any $C^{k}X$ gate, which generalizes Figure 1b into the correction $C^{k-1}Z$ gate over the $k$ controls. The $k=2$ case corresponds to Figure 1b, whereas in general, MBU uses one control fewer than the unitary uncomputation gate being replaced.

This transformation reduces the circuit’s $T$ count when it replaces $C^{k}X$ with $C^{k-1}Z$ gates. In Figure 5, the purple uncomputation gates CCX (gate 3) and CCCX (gate 8) are replaced by $X$-basis measurements followed by CZ and CCZ corrections in brown. CZ is Clifford and thus costs no $T$ gates, while CCZ differs from CCX only by Hadamard conjugation on its target and can therefore use the same decomposition as CCX, with equal $T$ count [51]. Even in the worst case when $m_1=m_2=1$, both corrections together cost no more than the original CCX uncomputation gate alone, thereby eliminating the entire $T$ cost of the CCCX unitary uncomputation gate.

Limitations. Endpoint MBU is most effective when each lifetime is uncomputed by a single gate, like the single Toffoli in Figure 1b. But in more complex circuits, an ancilla is often uncomputed by a sequence of gates, and uncomputing one ancilla can require using another as a control.

Figure 6 depicts a circuit for $t \mapsto t \oplus F$ where $F=x \lor y \lor z$, accumulated from three sub-cases $F=x \oplus x\bar{y} \oplus\bar{x}\bar{y}z$. Gates 1–6 compute $F$ into the ancilla $b$, where the ancilla $a$ holds $\bar{x}$ (gate 3) and then $\bar{x}\bar{y}$ (gate 5). Gate 7 adds $F$ to $t$, and gates 8–13 uncompute $b$ and $a$. The top right of Figure 6 shows the result of endpoint MBU, which replaces one CNOT per lifetime: gate 13 by measuring $b$ and correcting $Z(x)^{m_b}$, and gate 11 by measuring $a$ and correcting $Z(x)^{m_a}$. But since gates 13 and 11 are Clifford, the result saves zero $T$ gates, while the Toffoli gates 8, 9, and 10 remain.

Challenges to Generalization. Efficiently handling ancillas uncomputed by multiple gates or gates that depend on other ancillas requires a more generalized rule for MBU. The candidate in literature is the rule of Luongo et al. [ [37], which we presented in Figure 2 under the name monolithic MBU. The bottom of Figure 6 applies this rule to the three-bit OR circuit, revealing two fundamental issues:

• Unsoundness. Monolithic MBU conditionally applies the gates of unitary uncomputation, which in Figure 6 are gates 8–13 in purple. This is unsound when the circuit intersperses modification of the data (gate 2) with computation of the ancillas. Indeed, $x$ is left flipped with $\frac{1}{2}$ probability. Moreover, monolithic MBU measures only one ancilla but conditionally corrects all ancillas. In Figure 6, the result is that the unmeasured ancilla $a$ is left in a garbled nonzero state. And if it measured $a$, then the phase correction would be wrong for $b$ as gates 8 and 10 depend on $a$.

• Inefficiency. Monolithic MBU never decreases the $T$ cost of phase correction. Therefore, with $\frac{1}{2}$ probability, gates 8–13 execute in full and cost as much as the unitary uncomputation.

Interval MBU: Soundly and Efficiently Transforming Gate Sequences

In Section 4.2, we present interval MBU, the first circuit transformation that soundly and efficiently converts general sequences of multiple unitary uncomputation gates on multiple ancillas into MBU. We demonstrate its key insights in Figure 7 using the three-bit OR circuit from Figure 6.

Fundamentally, monolithic MBU fails because viewing unitary uncomputation as a contiguous block leads to that block entangling the measured ancilla with every other qubit it touches. Instead of marking such blocks, interval MBU considers the lifetime of an ancilla in isolation from the rest of the circuit. Figure 7 depicts these isolated lifetimes of $a$ and $b$ derived from the input circuit.

Given the isolated lifetime of an ancilla, any dependencies on other ancillas and data qubits can be considered independently of the decisions on this ancilla. Interval MBU is a policy for where to measure the ancilla and how to correct for the effect of each gate after the measurement:

Measure After Last Use. To find the earliest point to measure an ancilla, one idea is to identify the start of unitary uncomputation for that ancilla, which in Figure 6 is the first purple $\oplus$ in its lifetime, located at gate 8 for $b$ and gate 9 for $a$. But this choice is unsound: measuring $a$ at gate 9 destroys its value, and prevents gate 10 from continuing the uncomputation of $b$ using $a$ as a control.

Instead, the safe time to measure is right after the last gate that uses the ancilla in its isolated lifetime in Figure 7 — reads it as a control $\bullet$ ($Z$) or applies a gate other than $\oplus$ ($X$) such as $H$ to it. We call the suffix of an ancilla’s lifetime after its last use, which only contains $\oplus$-gates, its interval. For $b$, the last use is gate 7 and the interval is the gates 8, 10, and 13; for $a$, the last use is gate 10, and the interval consists of gate 11. After its last use, the only remaining operations on an ancilla are writes by $\oplus$-gates that restore it to zero, so measuring it cannot disturb any other qubit.

Correct in Place. Interval MBU measures $b$ at the start of its interval, after gate 7, and synthesizes the phase correction for each gate in a simple way. Each $\oplus$ constituting the interval disappears from the circuit, leaving a (potentially controlled) $Z$ gate spanning its old control qubits and classically controlled by the measurement outcome $m_b$ — like in endpoint MBU, but sound for a sequence of gates by the interval guarantee. Nothing else in the circuit changes, including irrelevant intervening gates such as gates 9 and 12 that do not touch $b$. The bottom of Figure 7 presents the result.

Result. Interval MBU effectively reduces the $T$ cost of the three-bit OR circuit. Whereas endpoint MBU replaces gates 11 and 13, interval MBU replaces gates 8, 10, 11, and 13 and retains only gate 9 for uncomputation. Counting seven $T$ gates per Toffoli, unitary uncomputation (gates 8–13) costs $3 \times7 = 21$ $T$ gates, endpoint MBU replaces only CNOTs and thus costs the same, and interval MBU leaves a single Toffoli, or 7 $T$ gates, with all phase corrections being Clifford CZ or $Z$ gates.

Static Analysis for Ancilla Lifetimes

In this section, we formalize MBUndo’s static analysis for ancilla lifetimes — the backward symbolic execution introduced informally in § 2.1. The input of the analysis is a circuit $C = g_1 \cdots g_n$ over unitary gates $g_i$ and a set $Q$ of qubits including the subset $A \subsetneq Q$ of ancillas, qubits promised to be $|0\rangle$ at the end of $C$. The output is, for every ancilla $a \in A$, the circuit positions where $a$ is found to hold $|0\rangle$, which we call its zero points; they cut the physical wire of the ancilla into lifetimes.

Definitions. The notations used in the analysis are defined below. We refer to the point in the circuit after gate $g_i$ as position $i$, so that position $0$ is the beginning of $C$ and position $n$ is its end. We write $\sigma_i$ for the symbolic state at position $i$, which maps each qubit to its symbolic value.

caption:

:::

We first present the main algorithm of the backward symbolic execution and its transfer rules, and then detail the symbolic values and how they are updated during the execution.

Alg. 1: Backward symbolic execution.

In: circuit $C = g_1 \cdots g_n$, ancillas $A \subseteq Q$

Out: $\mathcal{Z}(a) \subseteq\{0,\ldots,n\}$ for each $a \in A$

1. $\sigma(a) \leftarrow\varnothing$ for each $a \in A$;

2. $\sigma(q) \leftarrow\{\operatorname{fresh}()\}$ for each $q \in Q \setminus A$;

3. $\mathcal{Z}(a) \leftarrow\{n\}$ for each $a \in A$;

4. for $i \leftarrow n$ downto $1$ do

5. $\qquad\sigma\leftarrow\operatorname{Step}(\sigma,g_i)$;

6. $\qquad$ foreach $a \in A \cap\operatorname{qubits}(g_i)$ do

7. $\qquad\qquad$ if $\sigma(a)=\varnothing$ then

8. $\qquad\qquad\qquad\mathcal{Z}(a) \leftarrow\mathcal{Z}(a) \cup\{i-1\}$;

9. return $\mathcal{Z}$;

Main Algorithm. Given input circuit $C$ and ancillas $A$, Algorithm 1 outputs the set $\mathcal{Z}(a)$ of zero points of every ancilla $a$, the positions where $a$ is established to hold $0$. Conservatively, the gates between two consecutive zero points form a lifetime where $a$ holds a temporary value. In Figure 3 from the overview, the zero points of $a$ are $0$, $3$, and $8$, which yield the two shaded lifetimes.

Alg. 1 starts from the end of the circuit $C$. By definition of $A$, every ancilla holds $0$ as denoted by an empty symbolic value $\varnothing$ (line 1), and every data qubit holds an unknown final value denoted by a fresh symbol (line 2). Thus, $n$ is a zero point of every ancilla (line 3). The main loop (lines 4–8) processes the gates from $g_n$ down to $g_1$, computing $\sigma_{i-1} = \operatorname{Step}(\sigma_i,g_i)$ by the transfer rules that we define below. After each gate $g_i$ that touches $a$, the algorithm examines the value of $a$: if $\sigma_{i-1}(a) = \varnothing$, then $a$ is established to hold 0 immediately before $g_i$, and position $i-1$ is recorded as a zero point (lines 6–8).

Transfer Rules. The heart of the algorithm is the Step function, defined as follows:

Rule [XOR] handles a gate $\operatorname{XOR}(t;\ell_1,\ldots,\ell_k)$, where $k \ge0$, that XORs the product of its controls into its target $t$ and leaves controls unchanged. Such gates include $X$ and $C^kX$ gates with arbitrary control polarities, which dominate the circuits we study. Each control $\ell_j$ is either positive $c_j$ or negative $\bar{c}_j$ on a qubit $c_j \ne t$. Here, $\triangle$ is the symmetric difference of sets, $\sigma(q)$ is the symbolic value of qubit $q$, and $\sigma(\bar{c}) = \sigma(c) \mathbin{\triangle} \{1\}$ is that of a negative control. Product computes the symbolic value of a product ($\wedge$) of the controls via several $\triangle$ operations; it is defined below in Alg. 2.

Rule [Diag] handles a diagonal gate, e.g., $Z$, $S$, $T$, a phase rotation, or any controlled version of these. This rule leaves the state unchanged because diagonal gates change no basis values. Finally, rule [Forget] conservatively handles any other gate, including those that exit the computational basis such as $H$ and $Y$ rotations, by replacing the value of every qubit it writes by a fresh symbol recording that nothing is known about the value of that qubit before the unknown gate.

The [XOR] rule recognizes gates with one distinguished target qubit and zero or more control qubits, as is the case for Toffoli. Certain other well-known gates such as SWAP can be decomposed into such gates in advance. If such a decomposition is impossible, the [Forget] rule treats the gate conservatively as unknown. For unknown gates, $\operatorname{written}(g)$ is defined to be equal to $\operatorname{qubits}(g)$.

Symbolic Values and Updates. A symbolic value $V \in\mathit{Val}$ is a set of atoms and represents the XOR of its atoms; in particular, $\varnothing$ represents 0. An atom is the constant 1, a symbol $s$, or a product atom $\mathbf{p}_O$, the product of a set $O$ of two or more values built earlier. A symbol, created by $\operatorname{fresh}()$, stands for a basis value that the analysis does not know. A valuation function $\rho: \mathit{Sym} \to\{0,1\}$ assigns values to symbols, and under $\rho$, atoms $\alpha$ and values $V$ denote basis values as follows:

This definition is well-founded because the operands of a product atom are values built earlier in the analysis. When a valuation picks one basis state, a symbolic value gives the basis value of its qubit in that state as a function of the symbols. In particular, $\varnothing$, the empty XOR, denotes 0 under every valuation, and so the constant 0 needs no atom whereas the constant 1 is the atom 1. This set representation makes the rules, XOR and product, cheap. It also enables a temporary written twice by the same gate to cancel.

Specifically, the XOR of two values is computed by their symmetric difference, $V \oplus W := V \mathbin{\triangle} W$, which realizes cancellation $s \oplus s = 0$ by removing an atom on both sides. It realizes commutativity and associativity for free, as values are sets. The negation of a value follows as $V \mathbin{\triangle} \{1\}$.

The product of $k$ values is computed by Alg. 2, which first handles the two constant values $\varnothing$ and $\{1\}$, i.e., 0 and 1. If some operand is $\varnothing$, the product is $\varnothing$ (line 1). Operands equal to $\{1\}$ do not change the product and are removed (line 2). If no operand remains, the product is $\{1\}$ (line 3), and if exactly one operand remains, the product is that operand itself (line 4). Duplicate operands collapse automatically because the operands are kept as a set, realizing the law $s \wedge s = s$.

For two operands, the algorithm calls the subprocedure Product2 (line 5), which is defined in Appendix A. Product2 uses symmetric differences to apply a limited case of distributivity only to the constant $1$ of a negative control, ensuring that the representation is small yet precise.

Given three or more operands, none of which is $\emptyset$ or $\{1\}$ at this point, the algorithm performs hash-consing [20] (Ershov 1958) using a global memoization table $\Pi$ that associates operand sets $O$ with product atoms $p_O$. On line 6, Algorithm 2 looks up the operand set in the table $\Pi$. If $O$ has not been seen, $\Pi$ maps a fresh product atom $O \mapsto p_O$ and returns it.

Example. The circuit in Figure 8 has ancilla $a$. The table lists its symbolic states, where $V_x = \{x'\}$ and $V_y = \{y'\}$ are the final values of $x$ and $y$. Gate 7 XORs the value of its negative control, $V_y \mathbin{\triangle} \{1\} = \{y',1\}$, into $a$. Gate 6 preserves the symbolic state, since $T$ is diagonal. Gate 5 XORs the same value into $a$, which returns to $\emptyset$. Gate 4 replaces the value of $y$ by the fresh symbol $y''$. Gate 3 XORs Product$(V_x,\{y''\})$ into $a$, which creates the product atom $q$ for the operand set $\{V_x,\{y''\}\}$ and adds it to $\Pi$. Gate 2 preserves the symbolic state, and gate 1 XORs the same product into $a$, which is in $\Pi$, so $a$ becomes $\emptyset$. The zero points of $a$ are 0, 4, and 7, and its two lifetimes are 1–3 and 5–7 as shaded.

Precision. Values encode commutativity: when $V_x = \{x\}$ and $V_y = \{y\}$, Product$(V_x,V_y)$ and Product$(V_y,V_x)$ both yield the atom $p_{\{V_x,V_y\}}$ and their XOR is $\emptyset$. Meanwhile, Product$(V_x,\{y,z\})$ remains as one atom not expanded into $xy \oplus xz$, because we perform no distribution of $\land$ over $\oplus$ beyond the constant $1$ and no flattening of nested products. The values thus stay compact, at the price of precision: with $V_z = \{z\}$, Product$(V_x,\{y,z\})$ and $\{p_{\{V_x,V_y\}}\} \mathbin{\triangle} \{p_{\{V_x,V_z\}}\}$ denote the same function but differ as values. Thus, the analysis may miss a zero point, but never reports a wrong one:

Proof Sketch. Appendix B gives the full proof. The key idea is that the symbolic state describes a set of possible computational-basis bit strings as its symbols change. As an invariant, this set contains at least every string with nonzero amplitude in the actual quantum state. If every string this set contains has a given ancilla equal to 0, then that ancilla is also $|0\rangle$ in the actual state.

Given a bit string $b$, we write $b(q)$ for its bit at qubit $q$. We show by induction from position $n$ down to 0 that every basis state $|b\rangle$ with nonzero amplitude in $|\Psi_i\rangle$ is covered by $\sigma_i$: some valuation $\rho$ satisfies $b(q) = [\sigma_i(q)]_\rho$ for all $q \in Q$. Then, $\sigma_i(a) = \emptyset$ forces $b(a) = 0$ for every such $b$.

At position $n$, zero for every $a \in A$ and final values for data qubits provide this valuation. At each gate, rule [Xor] inverts the permutation of basis states by an XOR gate, rule [Diag] preserves the valuation, and rule [Forget] removes constraints on valuations on target qubits. □

Proof Sketch. Appendix C gives the full proof. Every atom comes from one qubit or by one gate, so there are $O(N)$ atoms, and every value (set of atoms) has size $O(N)$. A gate on $k$ qubits uses $O(k+1)$ set operations on values, which costs $O((k+1)N)$ and sums to $O(N^2)$ over the circuit. □

Automatic Transformations from Unitary to Measurement-Based Uncomputation

In this section, we present the two circuit transformations of MBUndo, endpoint MBU (§ 4.1) and interval MBU (§ 4.2), which were introduced informally in Sections 2.2 and 2.3.

Endpoint MBU for Final Uncomputation Gates

Endpoint MBU (Algorithm 3) automates the rule of Gidney [ [21] and Amy and Ross [ [5] that applies to any gate $g = \operatorname{XOR}(a; \ell_1, \ldots, \ell_k)$, i.e., a gate such as Toffoli that maps $|c\rangle|a\rangle$ to $|c\rangle|a \oplus f(c)\rangle$ for its controls $c_i$ or negations in the literals $\ell_i$.

Alg. 3 computes the lifetimes of every ancilla $a$ by Alg. 1 (line 1) and examines the last gate $g$ of each lifetime (lines 2–3). If $g$ is an XOR gate with target $a$ (line 4), Alg. 3 replaces it by an X-basis measurement of $a$ with outcome $m$ and a reset of $a$ to $|0\rangle$ (line 6) and, when $m = 1$, a correction of the phase $(-1)^{f(c)}$, which for $k \ge1$ corresponds to a $C^{k-1}Z$ gate on the qubits $c_1, \ldots, c_k$ of the controls (lines 7–8).

For a negative control $\bar{c}_j$, the correction is a $C^{k-1}Z$ gate conjugated by an $X$ gate on $c_j$ (line 8) to apply the phase when $\bar{c}_j = 1$, so whether a gate is replaced does not depend on its control polarity. Figure 9 gives an example, where a Toffoli with a negative control on $y$ is replaced by a $\operatorname{CZ}(x,y)$ gate between two $X$ gates on the negatively controlled $y$, which together apply the phase $(-1)^{x\bar{y}}$ when $m = 1$.

Alg. 3: Endpoint MBU.

In: circuit $C = g_1 \cdots g_n$, ancillas $A \subseteq Q$

Out: circuit $C$ after endpoint MBU

1. compute the lifetimes of every $a \in A$ by Alg. 1;

2. foreach lifetime of an ancilla $a \in A$ do

3. $g \gets$ the last gate of the lifetime;

4. if $g = \operatorname{XOR}(a; \ell_1, \ldots, \ell_k)$ then

5. replace $g$ in $C$ by

6. $H(a); \ m \gets\operatorname{Measure}(a); \ \operatorname{Reset}(a);$

7. if $m = 1$ then

8. $C^{k-1}Z(c_1, \ldots, c_k)$ conjugated by $X$ on the negative controls;

9. return $C$;

Interval MBU for Sequences of Multiple Uncomputation Gates

Instead of the last uncomputation gate, interval MBU (Alg. 4) finds in each lifetime of each ancilla $a$ a sound interval of gates to replace. Figure 10 depicts interval MBU on the suffix of a lifetime of $a$. After computing the lifetimes as Algorithm 3 does (line 1), Algorithm 4 processes each lifetime in three steps: it finds the last use of $a$ and its interval (lines 3–4), measures $a$ right after the last use (lines 5–6), and replaces every gate of the interval in place by its phase correction (lines 7–9).

Last Use and Interval. In its isolated lifetime, $a$ interacts with two kinds of gates: writes by $\oplus$ ($X$) gates and uses of $a$ as a control for $\bullet$ ($Z$) or as a subject of non-$\oplus$ gates such as $Y$ or $H$. In Figure 10, the last use $g^*$ of $a$ is as a control for $W$. Its interval consists of the $r$ writes after $g^*$, which restore $a$ back to $0$ (lines 3–4). The intervening gates $U_1, \ldots, U_{r-1}$ do not touch $a$, and $g^*$ is its last use.

Measurement After Last Use. Alg. 4 measures $a$ in the $X$ basis immediately after $g^*$, with outcome $m$, and resets $a$ to $|0\rangle$ (lines 5–6). The ancilla cannot be measured any earlier. If $a$ were measured before $g^*$, then $W$ in Figure 10 would instead need to be controlled on all bits that computed $a$, which kills any cost savings; the same occurs if $g^*$ were a $Z$ or $H$ gate on $a$. After $g^*$, the only gates on $a$ are $\oplus$-writes that turn into phase corrections. If $a$ has no use, its interval is its whole lifetime.

In-Place Phase Corrections. Algorithm 4 replaces each $\oplus$-gate $g$ that has controls $c_1, \ldots, c_k$ in the interval of $a$ by the correction $C^{k-1}Z(c_1, \ldots, c_k)$ classically conditioned on $m$ (lines 7–9). No gate is emitted if $k = 0$, as that error is an undetectable global phase, and negative controls are conjugated by $X$ gates. Nothing else changes, in particular $U_1, \ldots, U_{r-1}$ and all gates before $g^*$ in Figure 10.

Alg. 4: Interval MBU.

In : circuit $C = g_1 \cdots g_n$, ancillas $A \subseteq Q$

Out : circuit $C$ after interval MBU

1. compute the lifetimes of every $a \in A$ by Alg. 1;

2. foreach lifetime of an ancilla $a \in A$ do

3.     $g^{*} \leftarrow$ the last use of $a$ in the lifetime;

4.     $\mathit{interval} \leftarrow$ the XOR gates with target $a$ after $g^{*}$;

5.     insert immediately after $g^{*}$

6.         $H(a)$; $m \leftarrow\operatorname{Measure}(a)$; $\operatorname{Reset}(a)$;

7.     foreach $g = \operatorname{XOR}(a; \ell_1, \ldots, \ell_k)$ in interval do

8.         replace $g$ in $C$ by: if $m = 1$ then

9.             $C^{k-1}$-$Z(c_1, \ldots, c_k)$ conjugated by $X$ on the negative controls;

10. return $C$;

Proof. Soundness of endpoint MBU follows directly from the rule of Gidney [ [21] in Figure 1b, as generalized to multiply-controlled gates by Amy and Ross [ [5]. Algorithm 3 applies this rule precisely at the end of each lifetime, which satisfies the terminal $\lvert0\rangle_a$ condition in Figure 1b.

Soundness of interval MBU follows from a sequence of circuit equivalence rules, illustrated in Figure 11. Briefly, rule (1) follows from $X = HZH$ and rule (2) follows from $HH = I$. Rule (3) states that performing a unitary gate on a qubit and then (implicitly) measuring the qubit and discarding the outcome is equivalent to measuring the qubit immediately without performing the unitary gate. Rule (4) is the principle of deferred measurement [40].

Fix any given lifetime of ancilla $a$. As shown in Figure 10, the interval of $a$ consists of $\oplus$-gates with controls from qubits $c$ and intervening gates $U_i$ on $c$ that do not interact with $a$. By repeatedly applying rule (1) and cancelling adjacent Hadamard gates via rule (2), every $\oplus$ ($X$) on $a$ is replaced with a multiply-controlled-$Z$ gate that has $\bullet$ ($Z$) in place of $\oplus$ on $a$. This step corresponds to lines 7–9 in Algorithm 4. Now, each endpoint of the interval has an uncancelled Hadamard gate. Theorem 3.1 guarantees the terminal $\lvert0\rangle$ condition of rule (3), so by applying rule (3), the final Hadamard gate is replaced with a $Z$-basis measurement-and-reset gate. By repeating rule (4), this measurement commutes backwards through each $\bullet$ on $a$ by replacing quantum with classical control. The end of this process leaves one Hadamard gate and measurement-and-reset gate at the beginning of the interval — corresponding to lines 3–6 of Alg. 4. These rules do not change the basis state of any qubit other than $a$, and the gates they add do not touch any other ancilla between its last use and the end of its lifetime — the same argument repeats for the remaining ancillas. ▫

Proof. Consider a replaced gate $g$, whose $T$ cost is $e$. The MBU transformation removes $g$ and adds only its phase correction, an $H$ gate, and a measurement-and-reset gate for the whole interval. Only the correction can have nonzero $T$ cost. It consists of $X$ gates and a $C^{k-1}Z$ gate, which has a $T$ cost of at most $e$ by the assumption—which holds for standard decompositions [51]—and it executes only when $m=1$. Hence, no output executes more $T$ gates than the original. □

Complexity. Neither transformation increases the asymptotic complexity of the static analysis (Theorem 3.2). Once Alg. 1 has computed the zero points, one pass over the gates of each ancilla finds its lifetimes, their last gates for endpoint MBU, and their last uses and hence their intervals for interval MBU. This takes $O(N)$ time in total for the size $N$ of Thm. 3.2. Each replaced gate on $k+1$ qubits becomes $O(k)$ gates, namely one $C^{k-1}Z$ gate and at most $2k$ $X$ gates. Both transformations thus run in $O(N)$ time and output a circuit of size $O(N)$, so the total time of MBUndo stays at the expected $O(N^2)$ of Theorem 3.2, which remains dominated by the static analysis.

Implementation

We implement MBUndo as a compiler pass atop Qiskit 2.5.2 [27]. MBUndo takes as input a circuit and a list of ancillas that the circuit uncomputes unitarily. It performs the static analysis of § 3, followed by either the endpoint MBU (§ 4.1) or the interval MBU (§ 4.2) transformation. It then outputs a circuit in which ancillas are uncomputed by measurement.

This design enables MBUndo to be applied as a compilation pass to the output circuits of existing synthesizers for unitary uncomputation, thereby further enhancing their value. In this section, we detail several practical decisions made when implementing the techniques of § 3 and § 4:

Multi-Target Gate Normalization. Before the symbolic execution of § 3, MBUndo ensures that every gate falls into one of the categories handled by the rules of Step. Specifically, a multi-target gate of Qiskit whose definition consists of XOR gates only, e.g., SWAP, the Fredkin gate, and the double-CNOT gate, is decomposed into those XOR gates via its definition. Any other multi-target gate is conservatively treated as an unknown gate, which is handled by the [FORGET] rule.

Skipping Unprofitable Replacements. In its implementation of the transformations of § 4, MBUndo applies a filter to skip unprofitable replacements under the cost model of this paper. In particular, it leaves a lifetime unchanged if its last gate has fewer than two controls (i.e., an X or CNOT gate, which is Clifford) under endpoint MBU, or if its interval is a single such gate under interval MBU, as such a replacement is not profitable in either the $T$ or the Clifford count.

Relative-Phase Toffoli Gates. It is common for uncomputation synthesizers such as Unqomp [42] and ReQomp [44] to postprocess their output circuits by replacing each compute–uncompute pair of Toffoli gates on an ancilla with a pair of relative-phase Toffoli gates [7, 38], named RCCX in Qiskit. The RCCX gate $R$ controlled on $a$ and $b$ acts on target $t$ as $R\lvert a,b,t\rangle=i^{ab}(-1)^{a\oplus b} \lvert a,b,t\oplus ab\rangle$. This substitution is sound because RCCX is equal to Toffoli except for a phase that a paired RCCX on the same qubits cancels. It is profitable because an RCCX gate requires 4 $T$ gates, whereas Toffoli requires 7.

By nature, the RCCX substitution is orthogonal to our subject: turning unitary uncomputation into MBU. The practical wrinkle is that MBU is only conditionally applicable to RCCX gates. As we detail in Appendix § 14, the analogue of Gidney’s rule (Figure 1b) for the RCCX gate is sound under endpoint MBU for one RCCX, but is unsound under interval MBU for multiple RCCX gates.

To sidestep this unsoundness, MBUndo pre-processes its input circuit to restore RCCX pairs to Toffoli pairs, which does not change its semantics (Appendix § 14). After synthesizing MBU, it post-processes its output circuit to re-introduce RCCX in place of Toffoli gates whenever Unqomp or Reqomp would do the same. In brief, MBUndo first replaces every pair of Toffoli gates on an ancilla that the MBU transformation left intact with a pair of RCCX gates. This step mirrors Unqomp and Reqomp, but unlike them it misses the Toffoli gates whose partners were eliminated by MBU. To catch the benefit of RCCX for them as well, MBUndo replaces conservatively each such widowed Toffoli gate whose target is constant with an RCCX gate and a Clifford correction, which is sound by an analogue of Eq. (12) of Amy and Ross [ [5]. Neither pre- nor post-processing affects the asymptotic complexity of MBUndo, and for fairness we apply the above post-processing to every baseline in our evaluation. Overall, this approach matches existing practice, retains the $T$-count advantages of RCCX over Toffoli, and enables fair evaluation against existing systems.

Evaluation

In this section, we evaluate the performance of MBUndo via the following research questions:

RQ1. By how much do MBUndo’s automatic transformations, endpoint and interval MBU, reduce the gate costs of the circuits generated by synthesizers for unitary uncomputation?

RQ2. How do the results of MBUndo’s automatic transformations compare against baseline MBU constructions known in the literature for specific circuits?

RQ3. How well does MBUndo scale in compile time when given large circuits?

RQ4. How do gate savings from MBUndo compare against prior optimizers for quantum circuits?

RQ1: Enhancement Over Unitary Uncomputation Synthesizers

RQ1. By how much do MBUndo’s automatic transformations, endpoint and interval MBU, reduce the gate costs of the circuits generated by synthesizers for unitary uncomputation?

Benchmarks. We evaluate on 22 benchmark circuits, drawn from three sources:

• a) Unitary Uncomputation Circuits. All ten benchmarks evaluated by Reqomp [44], together with all three circuits evaluated by RwUn [35] that assume clean¹ ancillas, namely Incrementer, CondCleanMCS, and RiseCondCleanMCS.

• b) MBU Circuits. Six explicit circuits from the literature, to which MBU has been manually applied: GidneyAdder [21], TableLookup [23], GF8Multiply [30], TwoSidedComparator and VBEModAddition [Luong et al. 2025], and QLZOC [65]. We force MBUndo to rediscover the MBU opportunities in these benchmarks by removing all uncomputation from them and passing them to synthesizers for unitary uncomputation.

• c) Additional Circuits. Three other benchmarks for which MBU has not been previously explored, in which unitary uncomputation of an ancilla requires a sequence of gates: KeccakChi [4], SpeedySbox [54], and MatrixVectorEq [Pinto 2022].

Methodology. We evaluate against all existing circuit-level uncomputation synthesizers, namely Unqomp [42], Reqomp² [44], and RwUn [35] with its three clean-ancilla strategies Sequential, Reverse, and Jointly.³ For each benchmark, we run the synthesizer, obtain its output circuit and list of ancillas, and apply MBUndo. Following the methodology of Paradis et al. [ [41, 43], we decompose all $C^kX$ gates in the circuits into Toffoli ladders before synthesizing uncomputation. Uniquely, Reqomp can trade recomputation, i.e., more gates, for fewer ancillas on circuits that have specific dependency structures. We specify the default ancilla budget so that Reqomp does not unnecessarily incur additional gates.

As discussed in § 5, MBUndo applies RCCX post-processing analogous to Unqomp and Reqomp. For clarity, we report gate counts (i) without post-processing after any tool and (ii) with post-processing after each tool. For MBUndo, the worst-case gate counts assume that every phase correction executes, while expected counts use the fact that each measurement has an independent 50% probability of leaving no phase to correct and thus needing zero correction gates. The two usually differ only in Clifford count, as Toffolis require zero $T$ phase corrections under MBU.

Results. Table 1 reports results against Reqomp, while Appendix § 15 reports the remainder. We focus on Reqomp as it is the only baseline that does not timeout or crash on all 22 benchmarks, and on all but one it matches or outperforms Unqomp and RwUn in $T$ count. In the analysis below, we first compare endpoint MBU to Reqomp. Then, we compare interval to endpoint MBU on the benchmarks that compute ancillas using multiple gates, making endpoint MBU insufficient.

Benchmark	Q	A	LT	M			Reqomp		End. MBU		Int. MBU		Reqomp		End. MBU		Int. MBU
				End.	Int.		$T$	C	$T$	C	$T$	C	$T$	C	$T$	C	$T$	C
Adder	36	12	11	11	11		308	420	231	349	154	266	176	288	132	261	121	244
DeutschJozsa	19	8	8	8	8		119	158	63	106	63	106	71	110	39	90	39	90
Grover	9	3	20	20	20		336	479	196	349	196	349	216	359	136	309	136	309
IntegerComparator	24	11	11	6	10		147	199	105	160	77	125	87	139	63	124	47	109
MCX	23	10	10	10	10		147	168	77	103	77	103	87	108	47	83	47	83
MCRY†	24	11	11	11	11		154	178	77	107	77	107	88	112	44	85	44	85
Multiplier	24	9	65	65	65		770	970	315	548	245	473	440	640	180	438	170	423
PiecewiseLinearR†	13	6	42	21	36		1078	1530	931	1394	833	1277	868	1320	784	1268	728	1221
PolynomialPauliR†	9	3	45	45	45		630	780	315	488	315	488	360	510	180	398	180	398
WeightedAdder	25	9	77	74	74		1246	1499	728	1018	728	1013	832	1085	536	890	536	885
Incrementer	12	5	5	5	5		70	87	35	55	35	55	40	57	20	45	20	45
CondCleanMCS	121	68	93	93	93		1389	1602	738	998	738	998	795	1008	423	776	423	776
RiseCondCleanMCS	11	2	2	2	2		101	128	87	115	87	115	59	86	51	81	51	81
TwoSidedComparator	241	96	97	97	97		2674	3530	1995	2900	1344	2202	1534	2390	1146	2148	1053	2008
VBEModAddition	264	132	135	105	134		2800	3972	2065	3290	1379	2540	1600	2772	1180	2504	1082	2342
TableLookup	29	14	71	60	69		840	1224	420	834	364	763	480	864	240	714	208	659
GF8Multiply	12	3	3	2	3		126	153	112	140	63	87	72	99	64	94	57	83
KeccakChi	401	1	200	0	200		2800	4200	2800	4200	1400	2800	1600	3000	1600	3000	1400	2800
SpeedySbox	43	19	116	106	116		3108	3604	2366	2915	1554	2044	1776	2272	1352	2007	1236	1832
GidneyAdder	389	129	129	129	129		1806	2835	903	1997	903	1933	1032	2061	516	1739	516	1675
QLZOC	231	63	152	152	152		2177	3119	1113	2131	1113	2131	1265	2207	657	1827	657	1827
MatrixVectorEq	321	126	126	126	126		2667	3304	1785	2485	1337	1909	1527	2164	1023	1849	959	1657

Endpoint MBU vs. Reqomp. Figure 12 compares the gate counts of Reqomp and endpoint MBU. Without post-processing, endpoint MBU reduces $T$ gates over Reqomp by 37.5% and Clifford gates by 26.5% (in expectation) in geomean. After post-processing for both, endpoint MBU reduces $T$ gates by 36.5% and Clifford by 15.2% (in expectation). The Clifford reduction shrinks because MBU retains Clifford gates in phase corrections even as Reqomp decreases them in RCCX gates.

The only benchmark on which endpoint MBU performs no transformation is KeccakChi. Its last uncomputation phase in every lifetime is Clifford, which if replaced would save no $T$ gates but add Clifford corrections. MBUndo filters out such unprofitable candidates (see § 5).

Assuming that uncomputation makes up roughly half of a circuit, MBU should not be expected to reduce gate counts by more than half in general. Figure 12 depicts one exception, Multiplier, where MBUndo’s static analysis detects that certain Toffoli gates in the computation half of the circuit always leave their target as zero, and can thus also be replaced with measurement. MCRY, PiecewiseLinearR, and PolynomialPauliR use non-$T$ and non-Clifford rotation gates not relevant to uncomputation. MBUndo leaves them alone; we plot them for completeness.

Interval vs. Endpoint. Figure 13 compares the gate counts of interval and endpoint MBU for the 11 benchmarks where they differ, which contain ancillas that are uncomputed by multiple non-Clifford gates. Without post-processing, endpoint MBU reduces the $T$ and Clifford counts for these circuits by 28.9% and 19.8% over Reqomp, whereas interval MBU reduces them by 50.5% and 38.2%.

The results of interval and endpoint MBU are close for PiecewiseLinearR because the input to Reqomp accounts for 80.6%, not the typical $\sim50\%$, of the non-Clifford gates of Reqomp’s output. Excluding these, interval MBU eliminates all $T$ gates in the uncomputation of this circuit.

With RCCX post-processing, endpoint MBU reduces gates by 28.5% and 11.7%, as compared to 36.0% and 18.4% for interval MBU. The gap narrows after post-processing, as RCCX substitution (§ 5) is disproportionately effective for Toffoli gates not at the end of a lifetime. Even when not eliminated, Toffoli gates only cost 4 rather than 7 $T$ gates when replaced with RCCX. The remaining gap is largest for IntegerComparator (18.4%) and smallest for Multiplier (2.3%).

Over the full set of 22 benchmarks, interval MBU reduces $T$ gates by 47.9% and Clifford by 35.6% without post-processing, and by 40.0% and 18.7% with post-processing. Both interval and endpoint MBU reduce $T$ gates by 43.7% on the benchmarks not shown in Figure 13 with post-processing.

Other Synthesizers. The outputs of Unqomp and RwUn exhibit similar behavior (Appendix § 15). Over Unqomp, without post-processing, endpoint and interval MBU reduce $T$ gates by 38.6% and 48.4% and Clifford by 26.9% and 35.2%, respectively. The three strategies of RwUn succeed on 9, 13,

and 11 benchmarks, respectively, where endpoint MBU reduces $T$ gates by 18.4%, 17.8%, and 17.9%, and interval MBU by 59.0%, 55.5%, and 47.8%. The same pattern appears with post-processing.

These results are different from RwUn, which rewrites the entire circuit instead of replaying the computation gates — leading to fewer opportunities for endpoint MBU but more for interval MBU. Uniquely, RwUn uncomputes some ancillas via multi-controlled gates whose MBU phase corrections use $T$ gates. Its expected and worst-case $T$ counts differ: 216 vs. 282 for MCRY.

RQ2: Comparison with Existing MBU Constructions

RQ2. How do the results of MBUndo’s automatic transformations compare against baseline MBU constructions known in the literature for specific circuits?

Benchmarks. We group the known applications of MBU to individual circuits, to the best of our knowledge, into three categories: (i) circuits that apply Gidney’s rule to uncompute each ancilla computed by a Toffoli gate, including GidneyAdder [21] and QLZOC [65]; (ii) specialized constructions that exploit the structure of a particular computation, including that of TableLookup [23 Sec. 2] and of GF8Multiply [30 Appendix C.3]; and (iii) the monolithic MBU of Luongo et al. [ [37], which applies to an uncomputation block that operates on a single ancilla and neither modifies data qubits nor depends on other ancillas.

Methodology. For categories (i) and (ii), we compare three ways to construct each benchmark: via the unitary uncomputation synthesized by Reqomp, via the output of interval MBU in MBUndo, and via the published circuit. For category (iii), there currently exists no software tool to automatically transform a circuit by monolithic MBU. Instead, we optimistically calculate its best possible performance on the 22 benchmarks from RQ1. Specifically, we compute the number of unitary uncomputation gates for each benchmark by subtracting the number of gates input to Reqomp from the number of gates it outputs. We divide this number by two, as monolithic MBU executes each uncomputation block half the time, and add it to the number of input gates. Throughout this question, to isolate the effect of MBU itself, we apply no RCCX post-processing to any tool.

Results. In Table 2, we present the results for categories (i) and (ii). This table reports only the costs of uncomputation rather than the whole circuit. For category (i), MBUndo reproduces the manual constructions: it removes every $T$ uncomputation gate, introduces the same measurements, and matches the worst-case Clifford counts, with equal or lower expected Clifford count.

Benchmark	Uncomputation	$T$	C	M
GidneyAdder	Reqomp (unitary)	903	1160	0
	MBUndo (interval)	0	257.5 (386)	129
	Gidney [ [21]	0	321.5 (386)	129
QLZOC	Reqomp (unitary)	1064	1216	0
	MBUndo (interval)	0	228 (304)	152
	Yao et al. [ [65]	0	228 (304)	152
GF8Multiply	Reqomp (unitary)	63	75	0
	MBUndo (interval)	0	9 (15)	3
	Khattar et al. [ [30]	0	7.5 (10)	3
TableLookup	Reqomp (unitary)	448	636	0
	MBUndo (interval)	182	372 (405)	43
	Gidney [ [23]	49	127 (151)	19

For category (ii), on GF8Multiply, MBUndo similarly eliminates all $T$ gates. On TableLookup, MBUndo obtains 67% of the $T$ reduction of the specialized design, leaving 182 of 448 gates where the prior work leaves 49. This result is expected, as Gidney [ [23] performs a structural rewrite beyond a general-purpose transformation like MBUndo — measuring the lookup register and correcting the remaining phases with another lookup over a table of only $\sqrt{L}$ entries for $L$ addresses.

We present the results for (iii) in Appendix F. MBUndo surpasses the best possible performance of monolithic MBU on all 22 benchmarks, in $T$ and expected and worst-case Clifford counts. Relative to Reqomp, monolithic MBU reduces $T$ gates by at most 23.1% (geomean) and Clifford gates by at most 21.4%, whereas interval MBU reduces them by 47.9% and 35.6% (in expectation).

RQ3: Scalability of MBUndo

RQ3. How well does MBUndo scale in compile time when given large circuits?

Methodology. The 22 benchmarks of RQ1 span a variety of sizes, and MBUndo completes each within 43 ms on a laptop. To cover a wider range of sizes, we use the ten benchmarks of Reqomp, each of which is built from a scaling parameter $n$, e.g., the number of bits of the operands of Adder. RQ1 evaluates them at the smallest size used by Paradis et al. [ [44], Sec. 6.1; here we evaluate six sizes per benchmark. We report the running time and $T$ count of MBUndo applying interval MBU to the output of Reqomp, in the same setting of RQ1 with post-processing. We also report running times of Reqomp itself, to compare the time that MBUndo adds on top of its upstream tool.

As another baseline specific to the static analysis of Section 3, we compare against the symbolic executor of Carette et al. [ [14] for simulating quantum circuits over basis states. Like MBUndo, it tracks every qubit as a Boolean function of symbolic variables. However, it represents the function in algebraic normal form (ANF), which applies the full distributivity of $\land$ over $\oplus$ and can blow up in the size of a symbolic value. To compare the two representations, we run the tool of Carette et al. [ [14] on the outputs of Reqomp for the 15 of the 22 benchmarks of RQ1 that consist of XOR-based gates only (the tool does not support other gates). We obtain the ANF after each write to an ancilla to compare the zero points (see § 3) identified by that tool and by MBUndo.

Results. Figure 14 shows representative timing results on Adder; the other nine circuits (Appendix § 17) exhibit a similar pattern. MBUndo stays efficient even on large circuits: on Adder, its running time grows from 4 milliseconds at $n = 12$ to 0.10 seconds at $n = 400$. Over all benchmarks, it takes at most 1.0 second, on the largest instance of PolynomialPauliR. For reference, the upstream tool Reqomp takes 480 seconds to synthesize the uncomputation of Adder with $n = 400$.

When run on the 15 RQ1 benchmarks, the symbolic executor of Carette et al. [ [14] times out on five circuits after 1,000 seconds. On the ten benchmarks it completes, it identifies the same zero points as those found by MBUndo’s static analysis. This comparison indicates that MBUndo can precisely identify ancilla lifetimes on the evaluated circuits in time less than prior tools.

RQ4: Comparison with Circuit Optimizers

RQ4. How do gate savings from MBUndo compare against prior optimizers for quantum circuits?

Methodology. MBUndo is designed to reduce the gate cost of circuits that rely on unitary uncomputation. Among existing circuit optimizers, SPARE [52] is most similar in purpose: it targets the compute–use–uncompute structure of ancillas to optimize circuits.

Also relevant are optimizers such as Tzap [2] and Feynman [3] that perform rewrites unrelated to uncomputation such as phase folding. However, these tools currently handle circuits with measurements only by treating every measurement as opaque and ignoring the relationship between measured outcomes and classically controlled gates. This behavior significantly reduces their optimization opportunities on any circuit that uses MBU, so applying them to the outputs of both Reqomp and MBUndo would not compare the two on equal footing.

Instead, we take a conservative approach: give Reqomp the benefit of the optimizer and deny it to MBUndo. We obtain the gate counts of Reqomp followed by the Tzap optimizer with its recommended setting -O3 that includes phase folding to combine and cancel rotation gates. Feynman, which also uses phase folding, never leaves fewer T gates than Tzap on our benchmarks.

We provide to each optimizer the output circuit of Reqomp on the 22 benchmarks of RQ1. We apply the RCCX post-processing of RQ1 to the outputs of Reqomp and MBUndo; Tzap does not output any Toffoli gates to post-process, and SPARE performs its own RCCX post-processing that covers no fewer gates than ours. We give SPARE a time limit of 1,000 seconds per circuit.

Results. Appendix § 18 lists the gate counts and running times of the evaluated optimizers on all benchmarks. SPARE completes 18 of the 22 benchmarks without timing out or crashing. On those 18 cases, SPARE reduces the $T$ count of Reqomp’s output by 13.8% in geomean. MBUndo using interval MBU reduces the $T$ count by 41.4% on these 18 benchmarks, and uses fewer $T$ gates than SPARE on all but PolynomialPauliR, where SPARE trades $T$ gates for rotation gates. SPARE takes between 2.6 and 879 seconds, whereas MBUndo takes at most 43 milliseconds per circuit.

MBUndo produces fewer $T$ gates than Reqomp optimized by Tzap on 13 of the 22 benchmarks, even in this disadvantaged setting as explained above. On these 13 benchmarks, MBUndo reduces the $T$ count of Reqomp’s output by 44.5% in geomean, whereas Tzap reduces it by 10.2%; on the other nine, MBUndo reduces it by 32.8% and Tzap reduces it by 49.2%. These results suggest that transforming unitary uncomputation into MBU can by itself trade blows with a state-of-the-art circuit optimizer. We hope they motivate greater support for dynamic circuits in optimizers, which if combined with MBUndo can yield improvements beyond what either tool achieves alone.

Related Work

Uncomputation. The study of uncomputation originates in reversible computing [9]. For quantum programs, uncomputation has received architectural support [49], automation via type systems in languages [12, 26], and modular synthesis by compilers for languages [60, 62] and circuits [42, 44, 55]. For example, Tiwari et al. [ [59] uncompute ancillas by partial uncomputation when dependencies are cyclic, and RwUn [35] synthesizes uncomputation by rewrite rules that extend to dirty ancillas. All of these prior approaches synthesize circuits through unitary rather than measurement-based uncomputation.

Since its introduction, MBU has been applied by hand to numerous circuit designs [23, 30, 37, 65]. Programming frameworks such as Q# [56], Qualtran [25], and Qrisp [50] incorporate MBU as primitives taken from published circuit designs, and recent work furthers understanding of MBU from an error-correction perspective [28]. Our contribution of MBUndo complements these specific MBU constructions by automatically converting unitary uncomputation in arbitrary circuits to MBU, without requiring a specific circuit structure or uncomputed function.

Our work focuses on saving $T$ gates and not qubits. A rich body of work studies the time–space trade-offs of re-materializing temporary values, as shown in reversible pebble games [10, 31]. Spooky pebble games [22] similarly arise from MBU, with advantages in minimizing qubits at the cost of more gates [32, 48].

Symbolic Execution. Symbolic representations of quantum states have been applied to debugging [19], verification [Bauer-Marquart et al. 2023], and simulation [15] of quantum programs. Closest to our work, Carette et al. [ [14] simulate Hadamard–Toffoli circuits by tracking the basis value of each qubit as a Boolean formula in algebraic normal form. Our analysis instead tracks basis values conservatively as sets of XOR terms, which keeps them linear in the circuit size (Theorem 3.2) for scalability (§ 6.3). Our symbolic values share the spirit of XOR-AND graphs [39], which represent a Boolean function as a graph of XOR and AND nodes from which a compiler emits a circuit; our values differ in that they are updated gate by gate during symbolic execution, using cheap set operations and hash lookups.

Quantum Languages and Compilation. Other work in the programming languages community has furthered understanding of the implementation [13, 18, 61], compilation [46] (Tarabkha et al. 2025), optimization [16, 53, 63, 64, 68], and verification [1, 33, 36, 45, 57, 66] of quantum programs. MBUndo acts as an additional compilation pass that complements and enhances this work.

Limitations and Future Directions

Language-Level. MBUndo works at the circuit level, where it transforms arbitrary circuits with unitary uncomputation. A natural alternative direction is to automate MBU at the language level. For instance, a language in the spirit of Silq [12] and Qurrts [26] could decide by its type system when a program variable admits MBU, and then synthesize the measurement and phase corrections from a language-level specification of the function.

Architecture-Level. MBUndo measures cost mainly by $T$ count, the standard metric for fault-tolerant circuits, because $T$ gates are the major bottleneck on fault-tolerant hardware [11, 24] whereas Clifford gates and measurements are far cheaper [34]. In a concrete setting, the actual cost of each operation may depend on the architecture and its error-correction scheme, both of which are evolving rapidly. Future work could incorporate into the transformations a finer-grained cost model of a concrete architecture, which accounts for the cost of $T$ gates in terms of the production of magic states, as well as the cost of measurement and of the classical processing it requires such as decoding and feed-forward, to decide where MBU pays off for circuits on a specific architecture and error-correction scheme.

Conclusion

This work initiates the study of automatically and systematically transforming quantum circuits to use measurement-based uncomputation. Our efficient static analysis discovers opportunities for MBU in an input circuit, while our circuit transformations soundly replace unitary uncomputation gates by measurements and phase corrections that can be efficient on fault-tolerant hardware.

In the near term, our work brings the benefit of MBU to a broad class of quantum programs; in particular, it cuts the $T$-gate cost of the circuits output by existing uncomputation synthesizers and complements their methods. In the long run, we hope this work motivates compiler techniques for dynamic circuits, which combine unitary gates with measurement and classical feed-forward. Such directions reveal new ways to reduce cost that unitary gate optimization alone cannot reach.

AI Use The ideas of this work and the design of all of its analyses and transformations are due to the authors. The authors used Claude Fable 5.1 by Anthropic to implement the algorithms, to write tests for the implementation and evaluation, and to write scripts for running the experiments.

References

Algorithm for Product of Two Symbolic Values

Alg. 2 delegates the product of exactly two operands $V$ and $W$ to Product2, which is defined in Alg. 5. This algorithm distributes the constant $1$ out of $V$ and $W$ for precision.

To see its correctness, let $V' = V \setminus\{1\}$ and $W' = W \setminus\{1\}$ be the operands without the constant. Since $\bar{x}y = xy \oplus y$ and $\bar{x}\bar{y} = xy \oplus x \oplus y \oplus1$, the product of $V$ and $W$ is the product of $V'$ and $W'$, XORed with $W'$ if $V$ contains $1$, with $V'$ if $W$ does, and with $\{1\}$ if both do (lines 3–5). The product of $V'$ and $W'$ is looked up in $\Pi$ under $\{V', W'\}$ just like any other product in Alg. 2, or is $V'$ itself when $V' = W'$ (line 2).

The result of this method is that all four polarity combinations of two controls share one product atom, e.g., $\operatorname{Product}(V_x \mathbin{\triangle} \{1\}, V_y) = \{p_{\{V_x,V_y\}}\} \mathbin{\triangle} V_y$. This property makes the static analysis more precise on temporaries computed and uncomputed by Toffoli gates, the most common XOR gates, without incurring additional asymptotic cost. For instance, a circuit may compute a temporary by a Toffoli with a negative control $\bar{x}$ and uncompute it by a Toffoli with the positive control $x$ followed by a CNOT. Algorithm 5 ensures that these equivalent writes yield the same value.

Alg. 5: Product2$(V,W)$.
1	$V' \leftarrow V \setminus\{1\},\ W' \leftarrow W \setminus\{1\}$;
2	$P \leftarrow V'$ if $V'=W'$ else $P \leftarrow\{\Pi[\{V',W'\}]\}$;
3	if $1 \in V$ then $P \leftarrow P \mathbin{\triangle} W'$;
4	if $1 \in W$ then $P \leftarrow P \mathbin{\triangle} V'$;
5	if $1 \in V \cap W$ then $P \leftarrow P \mathbin{\triangle} \{1\}$;
6	return $P$;

Proof of Theorem 3.1

Proof of Theorem 3.1. The key idea is that the symbolic state may represent extra basis bit strings, but must include every string with nonzero amplitude in the actual state. If an ancilla has the empty symbolic value, all represented strings have that bit equal to $0$, so the actual state must also have that ancilla in $\lvert0\rangle$ and hence unentangled from the other qubits. Fix an input satisfying the final-zero promise on $A$. A basis bit string is a map $b : Q \to\{0,1\}$, with $b(q)$ its bit at qubit $q$; $b \in\operatorname{supp}\Psi_i$ means that $\lvert b\rangle$ has nonzero amplitude in $\lvert\Psi_i\rangle$. We prove the following invariant by backward induction on the position $i$:

Such a valuation covers $b$ in $\sigma_i$: it matches all qubits of $b$, although different strings may use different valuations, since the invariant chooses the valuation $\rho$ after the string $b$.

Base case. At position $n$, every supported string $b$ has $b(a)=0$ for all $a \in A$ by the promise on $A$. This matches $\sigma_n(a)=\varnothing$, which denotes $0$ under every valuation. Each data qubit $q \notin A$ has its own fresh symbol $s_q$, so setting $\rho(s_q)=b(q)$ gives a valuation covering $b$.

Inductive step. Assume the invariant at position $i$, and choose any $b \in\operatorname{supp}\Psi_{i-1}$. We construct a valuation covering $b$ in $\sigma_{i-1}=\operatorname{Step}(\sigma_i,g_i)$ for each transfer rule.

[XOR] An XOR gate permutes basis states, so $b'=g_i(b)$ belongs to $\operatorname{supp}\Psi_i$. By the induction hypothesis, some valuation $\rho$ covers $b'$. We first show the symbolic operations realize XOR and product under every valuation:

The first identity holds because $\triangle$ drops exactly the atoms common to $V$ and $W$, which cancel in the XOR. The second holds because every value that Alg. 2 returns denotes the product of its operands: the constants of lines 1 and 3, the sole operand of line 4, the atom $p_O$ of line 6, which denotes the product of $O$ by definition, and the value of Product2 (Appendix § 11); dropping operands equal to $\{1\}$ and duplicates (line 2) uses $1x=x$ and $xx=x$. For $g_i=\operatorname{XOR}(t;\ell_1,\ldots,\ell_k)$, the gate leaves the controls unchanged, and XORing into the target is self-inverse. Thus $\llbracket\sigma_{i-1}(t)\rrbracket_\rho=b'(t)\oplus\bigwedge_{j=1}^{k}b'(\ell_j)=b(t)$ by the two identities, with $b'(\bar{c}) = b'(c) \oplus1$ for a negative control, as in the symbolic rule. All other bits and symbolic values are unchanged, so $\rho$ covers $b$.

[Diag] A diagonal gate multiplies each amplitude by a nonzero phase, so the support is unchanged. As the rule also leaves $\sigma$ unchanged, coverage follows from the induction hypothesis.

[Forget] The rule keeps $\sigma_i(q)$ for $q \notin\operatorname{written}(g_i)$ and gives each $q \in\operatorname{written}(g_i)$ a fresh symbol $s_q$, which can be assigned any bit. It thus suffices to find some $b' \in\operatorname{supp}\Psi_i$ that agrees with $b$ outside $\operatorname{written}(g_i)$. Consider the group of all basis states that agree with $b$ outside $\operatorname{written}(g_i)$. By the definition of $\operatorname{written}(g_i)$, the gate maps this group into itself, and being unitary, it preserves the total probability of the group. That probability is positive before the gate, as it includes $b$, and hence after it, so some member $b'$ of the group is in $\operatorname{supp}\Psi_i$. Choose a valuation covering $b'$ by the induction hypothesis and extend it by $s_q \mapsto b(q)$ for each $q \in\operatorname{written}(g_i)$. The retained values contain no fresh symbol, so they still denote $b'(q)=b(q)$ for $q \notin\operatorname{written}(g_i)$. The resulting valuation covers $b$ in $\sigma_{i-1}$, which completes the induction.

Finally, Alg. 1 records $i \in Z(a)$ only when $\sigma_i(a)=\varnothing$, including its initialization at $i=n$. By the invariant, every $b \in\operatorname{supp}\Psi_i$ then satisfies $b(a)=\llbracket\varnothing\rrbracket_\rho=0$. Hence all amplitudes with $a=1$ vanish, and $|\Psi_i\rangle=|\psi\rangle\otimes|0\rangle_a$ for some state $|\psi\rangle$ of the other qubits, as required. □

Proof of Theorem 3.2

Proof of Theorem 3.2. Let $n_{\mathrm{XOR}}$ be the number of XOR gates and $F$ the set of gates handled by rule [Forget]. The symbolic execution creates one symbol per data qubit, one symbol per written qubit of each gate in $F$, and at most one product atom per XOR gate, whether by the general lookup (Alg. 2, line 6) or by Product$_2$ (Alg. 5, line 2), so the number of atoms is

Every value is a set of at most $B$ atoms. Processing an XOR gate with $k$ controls builds at most $k$ literal values (a negation is a symmetric difference with $\{1\}$), builds and hashes the operand set (which contains at most $k$ values of size at most $B$), performs at most one table lookup, and performs one symmetric difference on the target, which costs $O((k+1)B)$ in total.

With exactly two operands, Product$_2$ instead removes the constant 1 from both operands, compares the two results, hashes and looks up the constant-free pair, and performs at most three further symmetric differences, all on values of size at most $B$, which costs $O(B)$, so the bound per XOR gate is unchanged. The other rules cost $O(k)$ for a gate on $k$ qubits.

A gate $g_i$ has at most $|qubits(g_i)|$ controls, so its cost is $O((1+|qubits(g_i)|)\cdot B)$, and summing over the gates gives $O(B\cdot\sum_i(1+|qubits(g_i)|))$. We have $B=O(N)$ from above, and the sum is at most $N$ by the definition of $N$, so the total is $O(N\cdot B)=O(N^2)$ expected time under the usual assumptions on hashing. When the arity of the gates is bounded by a constant $c$, i.e., $|qubits(g_i)|\le c$ for all $i$, we have $N\le|Q|(1+c)\cdot n=O(n+|Q|)$, and the bound becomes $O(n+|Q|)^2$. Finally, Alg. 1 adds only a constant work per touched ancilla and a gate, namely the emptiness test of lines 6–8, i.e., $O(\sum_i |qubits(g_i)|)=O(N)$ in total, which does not affect the bound. □

Handling Relative-Phase Toffoli Gates in MBUndo

This appendix details how MBUndo treats relative-phase Toffoli gates [7, 38], named RCCX in Qiskit (§ 5). Recall that the RCCX gate $R$ with controls $a$ and $b$ acts on its target $t$ as $R|a,b,t\rangle=i^{ab}(-1)^{at}|a,b,t\oplus ab\rangle$, i.e., as a Toffoli gate up to the relative phase $i^{ab}(-1)^{at}$. The gate is self-inverse, so a pair of RCCX gates on the same qubits cancels like a pair of Toffoli gates when the controls hold the same values at both gates and the target holds the same value before the second gate as after the first. Uncomputation synthesizers such as Unqomp [42] and Reqomp [44] guarantee this for every Toffoli gate on an ancilla by construction, as they pair each gate that computes an ancilla with one that uncomputes it on the same controls with the same values, and thus substitute RCCX for all of them.

The Obstacle to MBU on a Sequence of RCCX Gates. Consider an ancilla $t$ that is computed by a sequence of RCCX gates, used, and uncomputed by the same sequence in reverse order. If $t$ is measured after its use as in interval MBU, the correction that replaces one uncomputing gate $R(a,b;t)$ must apply $(-1)^{mab}\cdot i^{ab}\cdot(-1)^{at}$, where $m$ is the measurement outcome, the first factor is the correction for a Toffoli gate (§ 4.2), and the other two factors reproduce the relative phase of $R$. The quantum value of $t$, however, is no longer available after the measurement. Only when $t$ is uncomputed by a single gate does $t$ hold $ab$ before it, so that the remaining phase reduces to $(-i)^{ab}$, which can be corrected without the value of $t$. MBU on one RCCX gate is thus sound, whereas it is unsound for a sequence of RCCX uncomputation gates.

Pre- and Post-Processing. To sidestep this obstacle while keeping the benefit of RCCX, MBUndo applies MBU to Toffoli gates only, with the following pre- and post-processing. The pre-processing restores every pair of RCCX gates in the input circuit to a pair of Toffoli gates. Unlike Unqomp and Reqomp, which can pair every Toffoli gate on an ancilla because their algorithms guarantee its partner by construction, MBUndo must handle input circuits in general and thus pairs gates by the static analysis of § 3: two gates form a pair when the symbolic execution gives the same symbolic values to their controls and target after the earlier gate and before the later gate, which proves that their relative phases cancel. The pairing is thus sound for every input circuit, not only for the outputs of the existing uncomputation synthesizers.

After the transformation of § 4, the post-processing rewrites the output circuit in two steps. First, every pair of Toffoli gates on an ancilla that the transformation left intact, paired as above, is replaced by a pair of RCCX gates. The symbolic execution handles the measurements, resets, and classically controlled gates that the transformation introduces conservatively: a measurement and a classically controlled gate are treated as unknown gates by the [Forget] rule, and a reset sets its qubit to $\varnothing$. This step alone, however, leaves every Toffoli gate whose partner was replaced by MBU as it is, whereas Unqomp and Reqomp substitute RCCX for both gates of a pair. To retain the benefit of RCCX for such gates as much as possible, the second step rewrites them individually: every remaining Toffoli gate on an ancilla whose partner was replaced by MBU is replaced by an RCCX gate and a Clifford correction, provided that its target has the symbolic value $\varnothing$ ($\lvert0\rangle$) or $\{1\}$ ($\lvert1\rangle$), as in Eq. (12) of Amy and Ross [ [5]. For $\lvert0\rangle$, the RCCX gate yields $i^{ab}\lvert a,b,ab\rangle$, and an $S^\dagger$ gate on the target cancels the phase, as it contributes $(-i)^t=(-i)^{ab}$:

For $\lvert1\rangle$, we have $R\lvert a,b,1\rangle=i^{ab}(-1)^a\lvert a,b,1\oplus ab\rangle$, and the phase is cancelled by an $S$ gate on the target, a $Z$ gate on $a$, and a global phase of $-\pi/2$:

as $i^{ab}i^{1\oplus ab}=i$ for either value of $ab$. In both cases, the $T$ count of the gate drops from 7 to 4, so the $T$-count reduction of the RCCX substitution is conservatively retained for the Toffoli gates that lose their partners to MBU. Neither the pre-processing nor the post-processing changes the complexity bound of Theorem 3.2, as both rely on the same symbolic execution.

Complete Results of RQ1

Table 3 lists the complete results of RQ1 (§ 6.1) for all uncomputation synthesizers, without and with the RCCX post-processing of § 5, including the worst-case counts of MBUndo.

Benchmark	Synthesizer	Post.	LT	Baseline $T$	Baseline $C$	Endpoint MBU $T$	Endpoint MBU $C$	Endpoint MBU $M$	Interval MBU $T$	Interval MBU $C$	Interval MBU $M$
Adder	Unqomp	no	11	308	420	231 (231)	348.5 (354)	11	154 (154)	266 (277)	11
		yes		176	288	132 (132)	260.5 (266)	11	121 (121)	244 (255)	11
	Reqomp	no	11	308	420	231 (231)	348.5 (354)	11	154 (154)	266 (277)	11
		yes		176	288	132 (132)	260.5 (266)	11	121 (121)	244 (255)	11
	RwUn-Seq						Timeout (>1000 s)
	RwUn-Rev	no	11	385	486	385 (385)	486 (486)	0	154 (154)	238.5 (266)	11
		yes		346	458	346 (346)	458 (458)	0	121 (121)	216.5 (244)	11
	RwUn-Join	no	11	385	486	385 (385)	486 (486)	0	154 (154)	238.5 (266)	11
		yes		346	458	346 (346)	458 (458)	0	121 (121)	216.5 (244)	11
DeutschJozsa	Unqomp	no	8	119	158	63 (63)	106 (110)	8	63 (63)	106 (110)	8
		yes		71	110	39 (39)	90 (94)	8	39 (39)	90 (94)	8
	Reqomp	no	8	119	158	63 (63)	106 (110)	8	63 (63)	106 (110)	8
		yes		71	110	39 (39)	90 (94)	8	39 (39)	90 (94)	8
	RwUn-Seq						Error
	RwUn-Rev						Error
	RwUn-Join						Error
Grover	Unqomp	no	20	336	479	196 (196)	349 (359)	20	196 (196)	349 (359)	20
		yes		216	359	136 (136)	309 (319)	20	136 (136)	309 (319)	20
	Reqomp	no	20	336	479	196 (196)	349 (359)	20	196 (196)	349 (359)	20
		yes		216	359	136 (136)	309 (319)	20	136 (136)	309 (319)	20
	RwUn-Seq						Error
	RwUn-Rev						Error
	RwUn-Join						Error
IntegerComparator	Unqomp	no	11	147	215	105 (105)	176 (179)	6	77 (77)	141 (146)	10
		yes		87	155	63 (63)	140 (143)	6	47 (47)	125 (130)	10
	Reqomp	no	11	147	199	105 (105)	160 (163)	6	77 (77)	125 (130)	10
		yes		87	139	63 (63)	124 (127)	6	47 (47)	109 (114)	10
	RwUn-Seq	no	36	17787	20361	16751 (17332)	19244.5 (19941)	35	6961.5 (13846)	8294.5 (16450)	35
		yes		17757	20342	16721 (17302)	19225.5 (19922)	35	6931.5 (13816)	8275.5 (16431)	35
	RwUn-Rev	no	11	147	197	105 (105)	158 (161)	6	77 (77)	127 (136)	10
		yes		99	154	75 (75)	139 (142)	6	47 (47)	108 (117)	10
	RwUn-Join	no	11	147	191	105 (105)	152 (155)	6	77 (77)	121 (128)	10
		yes		99	148	75 (75)	133 (136)	6	47 (47)	102 (109)	10
MCX	Unqomp	no	10	147	168	77 (77)	103 (108)	10	77 (77)	103 (108)	10
		yes		87	108	47 (47)	83 (88)	10	47 (47)	83 (88)	10
	Reqomp	no	10	147	168	77 (77)	103 (108)	10	77 (77)	103 (108)	10
		yes		87	108	47 (47)	83 (88)	10	47 (47)	83 (88)	10
	RwUn-Seq	no	30	2772	3168	1725.5 (2359)	2031.5 (2785)	30	1074.5 (2072)	1308 (2498)	30
		yes		2739	3144	1695.5 (2329)	2011.5 (2765)	30	1044.5 (2042)	1288 (2478)	30
	RwUn-Rev	no	10	147	168	77 (77)	103 (108)	10	77 (77)	103 (108)	10
		yes		87	108	47 (47)	83 (88)	10	47 (47)	83 (88)	10
	RwUn-Join	no	10	147	168	77 (77)	103 (108)	10	77 (77)	103 (108)	10
		yes		87	108	47 (47)	83 (88)	10	47 (47)	83 (88)	10
MCRY†	Unqomp	no	11	154	178	77 (77)	106.5 (112)	11	77 (77)	106.5 (112)	11
		yes		88	112	44 (44)	84.5 (90)	11	44 (44)	84.5 (90)	11
	Reqomp	no	11	154	178	77 (77)	106.5 (112)	11	77 (77)	106.5 (112)	11
		yes		88	112	44 (44)	84.5 (90)	11	44 (44)	84.5 (90)	11
	RwUn-Seq	no	1	296	342	215.5 (282)	252 (329)	1	215.5 (282)	252 (329)	1
		yes		296	342	215.5 (282)	252 (329)	1	215.5 (282)	252 (329)	1
	RwUn-Rev	no	1	296	342	215.5 (282)	252 (329)	1	215.5 (282)	252 (329)	1
		yes		296	342	215.5 (282)	252 (329)	1	215.5 (282)	252 (329)	1
	RwUn-Join	no	1	296	342	215.5 (282)	252 (329)	1	215.5 (282)	252 (329)	1
		yes		296	342	215.5 (282)	252 (329)	1	215.5 (282)	252 (329)	1
Multiplier	Unqomp	no	65	770	1010	315 (315)	587.5 (620)	65	245 (245)	512.5 (550)	65
		yes		440	680	180 (180)	477.5 (510)	65	170 (170)	462.5 (500)	65
	Reqomp	no	65	770	970	315 (315)	547.5 (580)	65	245 (245)	472.5 (510)	65
		yes		440	640	180 (180)	437.5 (470)	65	170 (170)	422.5 (460)	65
	RwUn-Seq						Timeout (>1000 s)
	RwUn-Rev						Timeout (>1000 s)
	RwUn-Join						Timeout (>1000 s)
PiecewiseLinearR†	Unqomp	no	44	1078	1564	931 (931)	1427.5 (1438)	21	833 (833)	1311 (1329)	36
		yes		868	1354	784 (784)	1301.5 (1312)	21	728 (728)	1255 (1273)	36
	Reqomp	no	42	1078	1530	931 (931)	1393.5 (1404)	21	833 (833)	1277 (1295)	36
		yes		868	1320	784 (784)	1267.5 (1278)	21	728 (728)	1221 (1239)	36
Benchmark	Synthesizer	Post.	LT	Baseline T	Baseline C	Endpoint MBU T	Endpoint MBU C	Endpoint MBU M	Interval MBU T	Interval MBU C	Interval MBU M
PolynomialPauliR†	Unqomp	no		45	630	780	315 (315)	487.5 (510)	45	315 (315)	487.5 (510)
		yes		360	510	180 (180)	397.5 (420)	45	180 (180)	397.5 (510)	45
	Reqomp	no		45	630	780	315 (315)	487.5 (510)	45	315 (315)	487.5 (510)	45
		yes		360	510	180 (180)	397.5 (420)	45	180 (180)	397.5 (510)	45
	RwUn-Seq					Error
	RwUn-Rev					Error
	RwUn-Join					Error
WeightedAdder	Unqomp	no		90	1386	1699	798 (798)	1153 (1195)	84	798 (798)	1148 (1195)
		yes		912	1225	576 (576)	1005 (1047)	84	576 (576)	1000 (1047)	84
	Reqomp	no		77	1246	1499	728 (728)	1018 (1055)	74	728 (728)	1013 (1055)	74
		yes		832	1085	536 (536)	890 (927)	74	536 (536)	885 (927)	74
	RwUn-Seq					Timeout (>1000 s)
	RwUn-Rev					Timeout (>1000 s)
	RwUn-Join					Timeout (>1000 s)
Incrementer	Unqomp	no		5	70	87	35 (35)	54.5 (57)	5	35 (35)	54.5 (57)
		yes		40	57	20 (20)	44.5 (47)	5	20 (20)	44.5 (47)	5
	Reqomp	no		5	70	87	35 (35)	54.5 (57)	5	35 (35)	54.5 (57)	5
		yes		40	57	20 (20)	44.5 (47)	5	20 (20)	44.5 (47)	5
	RwUn-Seq	no		9	2870	3322	2800 (2807)	3253.5 (3266)	7	658 (1281)	896.5 (1737)	9
		yes		2855	3312	2785 (2792)	3243.5 (3256)	7	643 (1266)	886.5 (1727)	9
	RwUn-Rev	no		5	70	94	70 (70)	94 (94)	0	35 (35)	57.5 (63)
		yes		55	84	55 (55)	84 (84)	0	20 (20)	47.5 (53)	5
	RwUn-Join	no		5	70	94	70 (70)	94 (94)	0	35 (35)	57.5 (63)
		yes		55	84	55 (55)	84 (84)	0	20 (20)	47.5 (53)	5
CondCleanMCS	Unqomp					Error
	Reqomp	no		93	1389	1602	738 (738)	997.5 (1044)	93	738 (738)	997.5 (1044)
		yes		795	1008	423 (423)	775.5 (822)	93	423 (423)	775.5 (822)	93
	RwUn-Seq	no		2	4105	4695	3720 (4077)	4259 (4669)	2	2649 (3979)	3041.5 (4571)	2
		yes		4105	4695	3720 (4077)	4259 (4669)	2	2649 (3979)	3041.5 (4571)	2
	RwUn-Rev	no		2	3398	3887	3034 (3370)	3475 (3861)	2	2302.5 (3286)	2644.5 (3777)	2
		yes		3398	3887	3034 (3370)	3475 (3861)	2	2302.5 (3286)	2644.5 (3777)	2
	RwUn-Join	no		2	3398	3887	3034 (3370)	3475 (3861)	2	2302.5 (3286)	2644.5 (3777)	2
		yes		3398	3887	3034 (3370)	3475 (3861)	2	2302.5 (3286)	2644.5 (3777)	2
RiseCondCleanMCS	Unqomp					Error
	Reqomp	no		2	101	128	87 (87)	115 (116)	2	87 (87)	115 (116)	2
		yes		59	86	51 (51)	81 (82)	2	51 (51)	81 (82)	2
	RwUn-Seq	no		10	766	888	559.5 (647)	670.5 (779)	10	286.5 (486)	370 (618)	10
		yes		727	850	523.5 (611)	636.5 (745)	10	250.5 (450)	336 (584)	10
	RwUn-Rev	no		2	633	736	608.5 (612)	711.5 (717)	2	241 (395)	307 (500)	2
		yes		594	698	572.5 (576)	677.5 (683)	2	205 (359)	273 (466)	2
	RwUn-Join	no		2	633	736	608.5 (612)	711.5 (717)	2	241 (395)	307 (500)	2
		yes		594	698	572.5 (576)	677.5 (683)	2	205 (359)	273 (466)	2
TwoSidedComparator	Unqomp	no		97	2674	3814	1995 (1995)	3318.5 (3232)	97	1344 (1344)	2485.5 (2581)	97
		yes		1534	2674	1146 (1146)	2431.5 (2480)	97	1053 (1053)	2291.5 (2387)	97
	Reqomp	no		97	2674	3530	1995 (1995)	2989.5 (2948)	97	1344 (1344)	2201.5 (2297)	97
		yes		1534	2674	1146 (1146)	2147.5 (2196)	97	1053 (1053)	2007.5 (2103)	97
	RwUn-Seq					Timeout (>1000 s)
	RwUn-Rev					Timeout (>1000 s)
	RwUn-Join					Timeout (>1000 s)
VBEModAddition	Unqomp					Error
	Reqomp	no		135	2800	3972	2065 (2065)	3289.5 (3342)	105	1379 (1379)	2540 (2656)	134
		yes			1600	2772	1180 (1180)	2503.5 (2556)	105	1082 (1082)	2342 (2458)	134
	RwUn-Seq					Timeout (>1000 s)
	RwUn-Rev	no		136	3290	4387	2961 (2961)	4081.5 (4105)	47	1379 (1379)	2344.5 (2580)	133
		yes			2804	4001	2490 (2490)	3709.5 (3733)	47	1082 (1082)	2146.5 (2382)	133
	RwUn-Join					Timeout (>1000 s)
TableLookup	Unqomp	no		71	840	1224	420 (420)	834 (864)	60	364 (364)	763 (817)	69
		yes		480	864	240 (240)	714 (744)	60	208 (208)	659 (713)	69
	Reqomp	no		71	840	1224	420 (420)	834 (864)	60	364 (364)	763 (817)	69
		yes		480	864	240 (240)	714 (744)	60	208 (208)	659 (713)	69
	RwUn-Seq	no		42	2478	2972	2110.5 (2149)	2615.5 (2683)	40	616 (1050)	983.5 (1585)	41
		yes		2388	2912	2020.5 (2059)	2555.5 (2623)	40	538 (972)	931.5 (1533)	41
Benchmark	Synthesizer	Post.	LT	Baseline $T$	Baseline C	Endpoint MBU $T$	Endpoint MBU C	Endpoint MBU M	Interval MBU $T$	Interval MBU C	Interval MBU M
	RwUn-Rev	no	40	2254	2716	1921.5 (1953)	2395.5 (2453)	38	588 (994)	937.5 (1495)	39
		yes		2164	2656	1831.5 (1863)	2335.5 (2393)	38	510 (916)	885.5 (1443)	39
	RwUn-Join	no	59	686	999	497 (497)	823.5 (837)	27	315 (315)	630 (686)	59
		yes		482	825	350 (350)	725.5 (739)	27	180 (180)	540 (596)	59
GF8Multiply	Unqomp	no	3	126	153	112 (112)	140 (141)	2	84 (84)	110 (114)	3
		yes		72	99	64 (64)	94 (95)	2	60 (60)	88 (92)	3
	Reqomp	no	3	126	153	112 (112)	140 (141)	2	63 (63)	87 (93)	3
		yes		72	99	64 (64)	94 (95)	2	57 (57)	83 (89)	3
	RwUn-Seq					Error
	RwUn-Rev					Error
	RwUn-Join	no	3	126	153	112 (112)	140 (141)	2	84 (84)	110 (114)	3
		yes		72	99	64 (64)	94 (95)	2	60 (60)	88 (92)	3
KeccakChi	Unqomp	no	200	2800	4600	2800 (2800)	4600 (4600)	0	1400 (1400)	3200 (3400)	200
		yes		1600	3400	1600 (1600)	3400 (3400)	0	1400 (1400)	3200 (3400)	200
	Reqomp	no	200	2800	4200	2800 (2800)	4200 (4200)	0	1400 (1400)	2800 (3000)	200
		yes		1600	3000	1600 (1600)	3000 (3000)	0	1400 (1400)	2800 (3000)	200
	RwUn-Seq	no	200	2800	4400	2800 (2800)	4400 (4400)	0	1400 (1400)	2900 (3200)	200
		yes		2800	4400	2800 (2800)	4400 (4400)	0	1400 (1400)	2900 (3200)	200
	RwUn-Rev	no	200	2800	4400	2800 (2800)	4400 (4400)	0	1400 (1400)	2900 (3200)	200
		yes		2800	4400	2800 (2800)	4400 (4400)	0	1400 (1400)	2900 (3200)	200
	RwUn-Join	no	200	2800	4400	2800 (2800)	4400 (4400)	0	1400 (1400)	2900 (3200)	200
		yes		2800	4400	2800 (2800)	4400 (4400)	0	1400 (1400)	2900 (3200)	200
SpeedySbox	Unqomp	no	116	3108	3604	2366 (2366)	2915 (2968)	106	1554 (1554)	2044 (2164)	116
		yes		1776	2272	1352 (1352)	2007 (2060)	106	1236 (1236)	1832 (1952)	116
	Reqomp	no	116	3108	3604	2366 (2366)	2915 (2968)	106	1554 (1554)	2044 (2164)	116
		yes		1776	2272	1352 (1352)	2007 (2060)	106	1236 (1236)	1832 (1952)	116
	RwUn-Seq	no	124	4060	4692	2786 (2982)	3427 (3728)	114	1750 (1946)	2316 (2700)	124
		yes		2788	3452	1736 (1932)	2483 (2784)	114	1432 (1628)	2104 (2488)	124
	RwUn-Rev	no	116	5852	6740	5110 (5110)	6051 (6104)	106	2198 (2842)	2884 (3844)	116
		yes		5222	6112	4792 (4792)	5839 (5892)	106	1880 (2524)	2672 (3632)	116
	RwUn-Join	no	116	3108	3604	2366 (2366)	2915 (2968)	106	1554 (1554)	2044 (2164)	116
		yes		1776	2272	1352 (1352)	2007 (2060)	106	1236 (1236)	1832 (1952)	116
GidneyAdder	Unqomp	no	129	1806	2835	903 (903)	1996.5 (2061)	129	903 (903)	1932.5 (2061)	129
		yes		1032	2061	516 (516)	1738.5 (1803)	129	516 (516)	1674.5 (1803)	129
	Reqomp	no	129	1806	2835	903 (903)	1996.5 (2061)	129	903 (903)	1932.5 (2061)	129
		yes		1032	2061	516 (516)	1738.5 (1803)	129	516 (516)	1674.5 (1803)	129
	RwUn-Seq					Timeout ($>1000$ s)
	RwUn-Rev	no	129	3598	5012	2702 (2702)	4180 (4244)	128	903 (903)	2125 (2446)	129
		yes		3211	4754	2315 (2315)	3922 (3986)	128	516 (516)	1867 (2188)	129
	RwUn-Join					Timeout ($>1000$ s)
QLZOC	Unqomp	no	152	2177	3119	1113 (1113)	2131 (2207)	152	1113 (1113)	2131 (2207)	152
		yes		1265	2207	657 (657)	1827 (1903)	152	657 (657)	1827 (1903)	152
	Reqomp	no	152	2177	3119	1113 (1113)	2131 (2207)	152	1113 (1113)	2131 (2207)	152
		yes		1265	2207	657 (657)	1827 (1903)	152	657 (657)	1827 (1903)	152
	RwUn-Seq					Timeout ($>1000$ s)
	RwUn-Rev					Timeout ($>1000$ s)
	RwUn-Join					Timeout ($>1000$ s)
MatrixVectorEq	Unqomp	no	126	2667	3304	1785 (1785)	2485 (2548)	126	1337 (1337)	1909 (2036)	126
		yes		1527	2164	1023 (1023)	1849 (1912)	126	959 (959)	1657 (1784)	126
	Reqomp	no	126	2667	3304	1785 (1785)	2485 (2548)	126	1337 (1337)	1909 (2036)	126
		yes		1527	2164	1023 (1023)	1849 (1912)	126	959 (959)	1657 (1784)	126
	RwUn-Seq					Timeout ($>1000$ s)
	RwUn-Rev	no	126	2667	3304	1785 (1785)	2485 (2548)	126	1337 (1337)	1909 (2036)	126
		yes		1527	2164	1023 (1023)	1849 (1912)	126	959 (959)	1657 (1784)	126
	RwUn-Join					Timeout ($>1000$ s)

Complete Results of RQ2

Table 4 lists, for every benchmark of RQ1, the $T$ and Clifford counts of the circuit of Reqomp, the lowest counts that monolithic MBU [37] can reach as explained in § 6.2, and the counts of the circuit that MBUndo produces from the output of Reqomp with interval MBU.

Benchmark	Reqomp input		Reqomp		Monolithic MBU (best case)				MBUndo (interval MBU)
	$T$	$C$	$T$	$C$	$T$	-Δ	$C$	-Δ	$T$	-Δ	$C$	-Δ
Adder	154	222	308	420	231	25.0%	321	23.6%	154	50.0%	266 (277)	36.7%
DeutschJozsa	63	94	119	158	91	23.5%	126	20.3%	63	47.1%	106 (110)	32.9%
Grover	196	319	336	479	266	20.8%	399	16.7%	196	41.7%	349 (359)	27.1%
IntegerComparator	77	114	147	199	112	23.8%	156.5	21.4%	77	47.6%	125 (130)	37.2%
MCX	77	88	147	168	112	23.8%	128	23.8%	77	47.6%	103 (108)	38.7%
MCRY	77	90	154	178	115.5	25.0%	134	24.7%	77	50.0%	106.5 (112)	40.2%
Multiplier	385	530	770	970	577.5	25.0%	750	22.7%	245	68.2%	472.5 (510)	51.3%
PiecewiseLinearR	833	1209	1078	1530	955.5	11.4%	1369.5	10.5%	833	22.7%	1277 (1295)	16.5%
PolynomialPauliR	315	420	630	780	472.5	25.0%	600	23.1%	315	50.0%	487.5 (510)	37.5%
WeightedAdder	763	937	1246	1499	1004.5	19.4%	1218	18.7%	728	41.6%	1013 (1055)	32.4%
Incrementer	35	47	70	87	52.5	25.0%	67	23.0%	35	50.0%	54.5 (57)	37.4%
CondCleanMCS	682	786	1389	1602	1035.5	25.4%	1194	25.5%	738	46.9%	997.5 (1044)	37.7%
RiseCondCleanMCS	87	112	101	128	94	6.9%	120	6.2%	87	13.9%	115 (116)	10.2%
TwoSidedComparator	1344	1916	2674	3530	2009	24.9%	2723	22.9%	1344	49.7%	2201.5 (2297)	37.6%
VBEModAddition	1400	2114	2800	3972	2100	25.0%	3043	23.4%	1379	50.8%	2540 (2656)	36.1%
TableLookup	420	617	840	1224	630	25.0%	920.5	24.8%	364	56.7%	763 (817)	37.7%
GF8Multiply	63	78	126	153	94.5	25.0%	115.5	24.5%	63	50.0%	87 (93)	43.1%
KeccakChi	1400	2400	2800	4200	2100	25.0%	3300	21.4%	1400	50.0%	2800 (3000)	33.3%
SpeedySbox	1554	1808	3108	3604	2331	25.0%	2706	24.9%	1554	50.0%	2044 (2164)	43.3%
GidneyAdder	903	1675	1806	2835	1354.5	25.0%	2255	20.5%	903	50.0%	1932.5 (2061)	31.8%
QLZOC	1113	1903	2177	3119	1645	24.4%	2511	19.5%	1113	48.9%	2131 (2207)	31.7%
MatrixVectorEq	1337	1656	2667	3304	2002	24.9%	2480	24.9%	1337	49.9%	1909 (2036)	42.2%

Complete Results of RQ3

Figure 15 shows the results of RQ3 (§ 6.3) on all ten benchmarks of Reqomp, in the format of Figure 14: for each benchmark, the running time and $T$ count of MBUndo applying interval MBU to the output of Reqomp, and those of Reqomp itself, at six sizes $n$.

Complete Results of RQ4

Table 5 lists, for every benchmark of RQ4 (§ 6.4), the gate counts of the output of Reqomp and of the circuits that SPARE, Feynman, and Tzap produce from it, together with the running time of each tool. The corresponding counts of MBUndo are those of interval MBU with RCCX post-processing.

Benchmark	Tool	Time (s)	$T$	R	Clifford	Benchmark	Tool	Time (s)	$T$	R	Clifford
Adder	Reqomp	–	176	0	288	CondCleanMCS	Reqomp	–	795	0	1008
	SPARE	9.0	180	0	264		SPARE	timeout (>1000 s)
	Feynman	0.006	88	0	242		Feynman	0.026	721	0	926
	Tzap	0.027	88	0	176		Tzap	0.027	721	0	930
DeutschJozsa	Reqomp	–	71	0	110	RiseCondCleanMCS	Reqomp	–	59	0	86
	SPARE	3.0	71	0	111		SPARE	Error
	Feynman	0.001	71	0	108		Feynman	0.001	59	0	86
	Tzap	0.024	71	0	108		Tzap	0.025	59	0	85
Grover	Reqomp	–	216	0	359	TwoSidedComparator	Reqomp	–	1534	0	2390
	SPARE	8.1	216	0	314		SPARE	305.8	1534	0	2488
	Feynman	0.005	178	0	302		Feynman	0.085	784	0	2107
	Tzap	0.026	178	0	292		Tzap	0.029	784	0	1873
IntegerComparator	Reqomp	–	87	0	139	VBEModAddition	Reqomp	–	1600	0	2772
	SPARE	3.1	79	0	137		SPARE	838.3	1567	0	3042
	Feynman	0.001	87	0	139		Feynman	0.105	1024	0	2516
	Tzap	0.025	87	0	139		Tzap	0.030	1016	0	2128
MCX	Reqomp	–	87	0	108	TableLookup	Reqomp	–	480	0	864
	SPARE	2.7	87	0	108		SPARE	85.7	320	0	589
	Feynman	0.001	87	0	108		Feynman	0.015	232	0	766
	Tzap	0.025	87	0	108		Tzap	0.029	172	0	500
MCRY	Reqomp	–	88	2	112	GF8Multiply	Reqomp	–	72	0	99
	SPARE	2.7	80	6	108		SPARE	2.6	84	0	96
	Feynman	0.001	88	2	112		Feynman	0.001	56	0	83
	Tzap	0.024	88	2	116		Tzap	0.025	52	0	83
Multiplier	Reqomp	–	440	0	640	KeccakChi	Reqomp	–	1600	0	3000
	SPARE	16.7	236	0	326		SPARE	Timeout (>1000 s)
	Feynman	0.009	248	0	568		Feynman	0.113	1600	0	3000
	Tzap	0.026	248	0	448		Tzap	0.028	882	0	3160
PiecewiseLinearR	Reqomp	–	868	182	1320	SpeedySbox	Reqomp	–	1776	0	2272
	SPARE	173.3	830	175	1341		SPARE	168.3	1726	0	2208
	Feynman	0.036	548	182	1255		Feynman	0.090	1008	0	1640
	Tzap	0.031	476	168	1216		Tzap	0.029	950	0	1584
PolynomialPauliR	Reqomp	–	360	61	510	GidneyAdder	Reqomp	–	1032	0	2061
	SPARE	13.3	80	131	260		SPARE	Timeout (>1000 s)
	Feynman	0.008	120	61	254		Feynman	0.057	1032	0	2061
	Tzap	0.025	120	31	358		Tzap	0.026	1032	0	2060
WeightedAdder	Reqomp	–	832	0	1085	QLZOC	Reqomp	–	1265	0	2207
	SPARE	35.7	831	0	1123		SPARE	878.7	1265	0	2511
	Feynman	0.022	678	0	945		Feynman	0.070	1087	0	2029
	Tzap	0.027	678	0	945		Tzap	0.027	1087	0	2028
Incrementer	Reqomp	–	40	0	57	MatrixVectorEq	Reqomp	–	1527	0	2164
	SPARE	3.6	39	0	54		SPARE	249.9	1527	0	2290
	Feynman	0.001	40	0	57		Feynman	0.077	1271	0	1908
	Tzap	0.024	40	0	57		Tzap	0.028	1271	0	1908