1 Introduction↩︎

Hybrid quantum–classical programs execute a quantum circuit whose measurement outcomes are consumed by a classical host program to compute the final result [1]–[7]. Although every measured qubit is typically read and its value flows through the host code, not all of those values truly influence the final return of the program. Contributions of these values could be semantically neutralized. As exemplified by 1, a value may cancel algebraically with others, vanish under an \(\texttt{int}(\cdot)\) truncation, or appear inside a sub-expression whose effect is later overwritten.

The standard liveness analysis [8], [9] is not enough to detect the semantic deadness of \(\texttt{a}\) in 1, as the liveness analysis is syntactic-based: \(\texttt{a}\) appears in the branch condition if(a), in the right-hand side of assignments in both branches, all of which syntactically contribute to the returned variables u, v, w, so a must be classified as potentially live.

From the hardware perspective, measuring qubits whose outcomes are later neutralized increases readout traffic [10], [11] and adds readout error [12], [13] without any benefit to the final result. Performing gates that only influence those qubits is likewise unnecessary: they deepen the circuit, extend the required coherence window, and accumulate error across extra operations, which lowers overall fidelity despite contributing nothing to the result of calculation. For example, in the hybrid program 1, given \(o_0\) (feeding \(\texttt{a}\)) being non-contributory, the gates highlighted by the red dashed boxes are therefore dead and can be removed without changing the distribution of the contributory outcomes, i.e., \(o_1\) and \(o_2\), or the host program’s returned result.

As quantum stacks mature, cross‑disciplinary teams prototype quickly across library abstractions and mixed toolchains [14]–[17], and small but regular host‑side edits that obscure data flow could turn a seemingly used measurement into a non‑contributory one, of which effects are brittle under iteration and hard to catch in review, but the cost of leaving them in is paid on every shot of execution. Therefore, identifying as a compilation step semantically non-contributory measurement outcomes, and removing redundant operations accordingly, is crucial to improving quantum circuit efficiency and reliability.

Prior works. Existing methods address this problem only in part. Dead gate elimination (DGE) provides a rigorous circuit-level framework: if the action of a gate does not affect the probability distribution of contributory measurement outcomes, it can be removed without altering observable behaviour [18], but DGE assumes that the set of non-contributory outcomes is already known and cannot infer which ones semantically contribute to the host’s return value. In general, deciding semantic liveness at a program point—whether there exists an execution whose observable behaviour depends on the current value of a variable—is undecidable [19], [20], so classical liveness analyses are conservative static approximations computed via backward data-flow or abstract interpretation [21], [22]. Remme et al.optimize hybrid Quil programs using standard compiler analyses, but their liveness is a purely syntactic is-read notion and cannot establish result-invariance of measurement outcomes [23]. Static analyzers such as LintQ and QChecker provide AST-driven checks for suspicious Qiskit patterns, yet focus on syntactic use rather than host-semantic non-contribution and do not drive circuit pruning [24], [25]. Partial equivalence checking can certify that a simplified circuit preserves a user-chosen subset of outputs, but does not identify which outputs are irrelevant nor perform simplification automatically [26]; similarly, QuTracer prunes gates that do not affect a user-specified subset of measured qubits, but cannot discover that subset in a hybrid setting [27]. Extending code property graphs to quantum code enables cross-domain analysis and can detect measurements whose results are never used [28], but it cannot prove that syntactically used results are nonetheless semantically non-contributory. Quantum constant propagation exploits contextual host information to fold gates and simplify unitary blocks [29]; however, information flows only from host to circuit and does not track how measurement results are subsequently consumed, so it cannot prove semantic non-contribution of syntactically used outcomes. Finally, while it is well known that the outcome of a measured qubit depends only on operations in its causal light cone [30], there is no systematic approach that exploits this insight for hybrid program optimization when non-contributory qubits are obscured by complex classical post-processing.

Our contribution i. We present a semantics-aware host-side static analysis for hybrid quantum programs that identifies measurement outcomes that are syntactically read by the host but semantically non-contributory to the host return. The analysis is formulated as an abstract interpretation over the classical host program, tracking data and control contribution of measurement-bound initial values with exact symbolic reasoning when possible and conservative dependency information otherwise. We formalize semantic contribution and prove soundness: every reported non-contributory outcome is irrelevant to the host program’s returned value. We evaluate the analysis on \(24\) application-faithful hybrid workloads across four domains, with host computations derived from upstream application artifacts, and include a standard syntactic liveness analysis as baseline. We show that the result of the host-side analysis enables around \(38\%\) mean total-gate reduction standalone, and still removes about \(31\%\) of the post-optimized gates after SOTA circuit optimizers Qiskit [31], t|ket\(\rangle\) [32], and PyZX [33] have already run. Besides, our method detects \(4\times\) as many non-contributory measurements as a baseline standard syntactic liveness analysis. This indicates that the host-semantic simplifications exposed by our analysis are not subsumed by by either widely used circuit-local optimizers or standard syntactic liveness analysis.

A scalability challenge. The host-side static analysis introduced by our method is the main semantic phase that goes beyond circuit-only optimisation and, therefore, a primary source of compile-time cost in our flow. Accelerating this phase is appealing, but it is not straightforward: in its original form, the analysis exposes irregular dependences and limited explicit parallel structure, making it a poor match for CUDA’s SIMT execution model [34], [35]. This motivates an SSA-style reformulation. SSA makes definitions and data dependences explicit [36], and prior work has studied both the connection between SSA translation and abstract interpretation, and the semantics preservation of SSA-based compiler middle ends [37]–[39]. Inspired by this line of work, we use SSA in a narrower setting: to expose level-wise independent abstract-transfer tasks while preserving the host-side analysis result. Indeed, as shown empirically in the last report in 3.2, directly moving the source-order analysis to the GPU is ineffective. This observation motivates a dedicated reformulation of the host-side analysis for GPU execution, which we describe next.

Our contribution ii. We introduce an SSA-style, levelized intermediate representation for the host program to expose sufficient parallel structure for effective GPU acceleration of the host-side analysis. We prove that this lowering preserves the set of non-contributory outcomes computed by the host-side analysis. On top of this lowered representation, we implement a CUDA-based backend and evaluate the resulting GPU-accelerated host-side analysis, showing that the lowered backend achieves substantial speedups over a sequential baseline.

Overview of optimization flow. 2 provides an overview of the full flow of using our analysis to guide circuit optimization.

2 Method↩︎

2.0.0.1 Scope and assumptions

In this manuscript, we restrict our consideration to the following host program fragment: \[\begin{array}{rcl} S &::=& \texttt{skip} \mid \texttt{x} := e \mid \texttt{return}\;e \mid S;S \mid \texttt{if}\;(e)\;\texttt{then}\;S\;\texttt{else}\;S,\\[1mm] e &::=& \texttt x \mid c \mid -e \mid e_1 \odot e_2 \mid \texttt{int}(e) \mid \texttt{random}(L,U) \mid \texttt{f}(e_1,\ldots,e_n), \end{array}\] where \(\texttt x\) is a program variable, \(\odot \in \{+,-,\times,\div,\%\}\), and rational constants are interpreted exactly. Throughout the paper, \(\mathbb{Q}\) denotes the set of rational numbers. The operation \(\texttt{int}(\cdot)\) denotes truncation toward zero. \(\texttt{random}(L,U)\) has measurement-independent constant bounds. Function calls are assumed to be total, pure, and side-effect free. The grammar supports runtime-dependent structured conditionals, including nested conditionals. Arbitrary loops and recursion are outside the current implementation scope. Standard CFG-based fixpoint iteration with joins/widening, optionally combined with bounded unrolling, can extend the analysis to loops.

Next, we design abstract interpretation with a custom domain to symbolically evaluate the program.

2.1 Abstract domain↩︎

\(\mathcal{V}\) denotes the set of all program variables. \(\mathbf{M}\subseteq\mathcal{V}\) is a set of variables that take measurement outcome as initial value. Our goal is to perform a forward analysis on the host program to track which initial values of variables in \(\mathbf{M}\) influence the final return. \(\Sigma_0=\{\texttt{x}@0 \mid \texttt{x}\in \mathcal{V}\}\) denotes the set of symbols representing initial values: for each variable \(\texttt{x}\), \(\texttt{x}@0\) denotes its initial value.

2.1.0.1 Program state

An abstract state of the program is a mapping \(\rho : \mathcal{V}\cup\{\texttt{return}\} \rightarrow \mathcal{A}\) that maps each program variable to an abstract value. We reserve a distinguished symbol \(\texttt{return}\notin \mathbf{M}\) to hold the abstract return value, i.e., we use \(\rho(\texttt{return})\) to denote the abstract return value after executing the current statement. With \(\rho(\texttt{return}) = \bot\), it means current statement has no return. Besides, we maintain two auxiliary maps \(\mathbf{Dom}: \Sigma \rightarrow \{\boldsymbol{bin}, \boldsymbol{int}, \boldsymbol{real}\}\), and \(\mathbf{B}: \Sigma \rightarrow \{\bigcup_k[L_k, U_k] \mid L, U \in \mathbb{Q}\}\), where \(\Sigma\) is the set of all symbols, \(\mathbf{Dom}\) records the type/domain of each symbol, \(\mathbf{B}\) records the value range for every symbol. We maintain \(C_{\texttt{ctrl}} \subseteq \mathbf{M}\) as the set of measurement-bound variables whose initial values affect the evaluation of at least one conditional branch in a way that changes the observable post-conditional result, in particular the eventual abstract return.

2.1.0.2 Abstract value

An abstract value \(\mathcal{A}\) is either a polynomial form \(\langle p\rangle\) or a dependence form \(\langle D\rangle\): \[\mathcal{A} \mathrel{::=} \langle p\rangle \mid \langle D\rangle,\] where \(p\in\mathcal{P}\) is a multivariate polynomial over symbols in \(\Sigma\) with rational coefficients, and \(D\subseteq\Sigma\) is a set of symbols the abstract value may depend on.

In our analysis, an abstract value is either an exact polynomial, if we can precisely compute it within our domain (see 2) or a set of symbols it may depend on, if exact arithmetic is not feasible (see 3). The dependence form is a conservative fallback recording initial inputs that might influence the value. The polynomial form preserves more information: when \(\mathcal{A} = \langle p\rangle\), \(\mathcal{A}\) exactly depends on all symbols contained in the polynomial \(p\).

2.1.0.3 Exact abstract equality

Two abstract values are treated as equal only when they are both exact polynomial forms with the same normalized polynomial: \[\mathsf{Eq}_{\mathrm A}(A,B) = \begin{cases} \texttt{true}, & A=\langle p\rangle,\; B=\langle q\rangle,\; \mathrm{norm}(p-q)=0,\\[1mm] \texttt{true}, & A=B=\bot,\\[1mm] \texttt{false}, & \text{otherwise,} \end{cases}\] where \(\mathrm{norm}\) is a canonical polynomial simplification which collects like terms, orders monomials canonically, and drops zero terms. For example, \(\mathrm{norm}((\texttt{a}@0+\texttt{b}@0)-(\texttt{b}@0+\texttt{a}@0))=0\) and \(\mathrm{norm}(2\,\texttt{a}@0\cdot\texttt{b}@0+3\,\texttt{b}@0\cdot\texttt{a}@0)=5\,\texttt{a}@0\cdot\texttt{b}@0\).

2.2 Abstract evaluation↩︎

We define abstract evaluation of expressions. \([\![e]\!]^{\sharp}\) denotes the abstract evaluation of an expression \(e\) under environment \(\rho\). In the following, we use the notation \(\mathbf{Sym}(\cdot)\) very often: given any abstract value \(\mathcal{A}\), \(\mathbf{Sym}(\mathcal{A})\) is the set of all symbols occurring in \(\mathcal{A}\), including symbols in \(\Sigma_0\) and any fresh symbols introduced by random(\(\cdot,\cdot\)), for example, \(\mathbf{Sym}\!\left(\,\big\langle 2\,\texttt{a}@0 \;+\; 4\texttt{b}@0 \;-\; 3 \big\rangle\,\right) \;=\; \{\, \texttt{a}@0,\;\texttt{b}@0 \,\}\), \(\mathbf{Sym}\!\left(\,\big\langle \{\texttt{a}@0, \texttt{b}@0, \texttt{c}@0\} \big\rangle\,\right) \;=\; \{\, \texttt{a}@0,\;\texttt{b}@0,\;\texttt{c}@0 \,\}\). We set \(\mathbf{Sym}(\bot)\) to \(\varnothing\).

2.2.0.1 Base case

\[\frac{\texttt{x}\in\mathcal{V}}{[\![\texttt{x}]\!]^{\sharp}=\rho (\texttt{x})} \quad \frac{c\in\mathbb{Q}}{[\![c]\!]^{\sharp}=\langle c\rangle} \quad \frac{c\notin\mathbb{Q}}{[\![c]\!]^{\sharp}=\langle \varnothing\rangle}\]

2.2.0.2 Binary and unary arithmetic

When both operands have exact polynomial form, we compute the result exactly in the polynomial ring, using \(+\), \(-\), \(\times\), and then apply canonical polynomial simplification \(\mathrm{norm}\): \[\frac{[\![e_1]\!]^{\sharp}=\langle p\rangle \wedge [\![e_2]\!]^{\sharp}=\langle q\rangle\wedge p, q\in \mathcal{P}\wedge \odot\in\{+,-,\times\}}{[\![e_1 \odot e_2]\!]^{\sharp}=\langle \mathrm{norm}(p\;\odot\;q)\rangle}\] To keep the analysis efficient, we use a simplified polynomial domain: since division and modulo are not closed, we drop the polynomial form for these operators and return a dependence form: \[\frac{\mathcal{A}_1=[\![e_1]\!]^{\sharp}\wedge \mathcal{A}_2=[\![e_2]\!]^{\sharp}\wedge \odot\in\{\div, \%\}}{[\![e_1 \odot e_2]\!]^{\sharp}=\langle \mathbf{Sym}(\mathcal{A}_1)\cup \mathbf{Sym}(\mathcal{A}_2)\rangle}\] Similarly, if either operand is already in dependence form \(\langle D\rangle\): \[\frac{\mathcal{A}_1=[\![e_1]\!]^{\sharp}=\langle D\rangle\wedge D \subseteq \Sigma\wedge \mathcal{A}_2=[\![e_2]\!]^{\sharp} }{[\![e_1 \odot e_2]\!]^{\sharp}=[\![e_2 \odot e_1]\!]^{\sharp}=\langle \mathbf{Sym}(\mathcal{A}_1)\cup \mathbf{Sym}(\mathcal{A}_2)\rangle}\] Unary minus is value-preserving on dependencies: \[\frac{[\![e]\!]^{\sharp}=\langle p\rangle\wedge p\in\mathcal{P}}{[\![-e]\!]^{\sharp}=\langle -p\rangle} \qquad \frac{[\![e]\!]^{\sharp}=\langle D\rangle\wedge D\subseteq\Sigma}{[\![-e]\!]^{\sharp}=\langle D\rangle}\]

2.2.0.3 Operator int\((\cdot)\)

In this manuscript, int\((\cdot)\) is truncating toward zero: it discards the fractional part, and is not a flooring (e.g., \(\texttt{int}(1.2)=1\), \(\texttt{int}(-1.5)=-1\), \(\texttt{int}(-0.3)=0\)). If \([\![e]\!]^{\sharp}\) evaluates to an exact polynomial that is integer-valued under the domain map \(\mathbf{Dom}\), then \([\![\texttt{int}(e)]\!]^{\sharp}\) returns the same polynomial: \[\frac{C_{int}^1(e) \;\equiv\; [\![e]\!]^{\sharp}=\langle p\rangle \wedge \mathrm{IsInt}(p,\mathbf{Dom}) = \texttt{true}}{[\![\texttt{int}(e)]\!]^{\sharp}=\langle p\rangle}\] where \(\mathrm{IsInt}(p,\mathbf{Dom})\) holds iff all coefficients of \(p\) are integers and \(p\) mentions no symbol whose domain is real.

If \([\![e]\!]^{\sharp}\) evaluates to an exact polynomial \(p\) whose evaluation gives a value range \(I\) under the bound map \(\mathbf{B}\), and this value range lies entirely within a single truncation bin, then \([\![\texttt{int}(e)]\!]^{\sharp}\) constant-folds to an integer: \[\frac{C_{int}^2(e) \;\equiv\; [\![e]\!]^{\sharp}=\langle p\rangle \wedge \mathrm{eval}(p,\mathbf{B})=I \wedge \mathrm{trunc}(I)=c}{[\![\texttt{int}(e)]\!]^{\sharp}=\langle c\rangle}\] where the operator \(\mathrm{eval}(p,\mathbf{B})\) is the value range of \(p\) evaluated under the bounds of variables given by \(\mathbf{B}\); \(\forall i\in \mathbb{Z}: \mathrm{trunc}(S)=i\) iff \(\forall v\in S:\texttt{int}(v)=i\).

We further use the following integer-carrier rule: if an exact polynomial can be decomposed into an integer-valued part plus a residual whose feasible range cannot push the value across any truncation boundary, then truncation preserves the integer-valued part: \[\frac{ \begin{array}{l} C_{int}^3(e) \;\equiv\; [\![e]\!]^{\sharp}=\langle r\rangle \wedge \exists p,q\in\mathcal{P}:\; r=\mathrm{norm}(p+q)\wedge\mathrm{IsInt}(p,\mathbf{Dom})=\texttt{true} \wedge\\ \mathrm{eval}(p,\mathbf{B})=I_p \wedge \mathrm{eval}(q,\mathbf{B})=I_q \wedge \mathrm{NoCarry}(I_p,I_q)=\texttt{true} \end{array} }{[\![\texttt{int}(e)]\!]^{\sharp}=\langle p\rangle}\] where \(\mathrm{NoCarry}(I_p,I_q)\) holds iff \(\forall k\in (I_p\cap\mathbb{Z}),\;\forall \delta\in I_q:\;\texttt{int}(k+\delta)=k\).

A common sufficient pattern is \(I_q\subseteq [0,1)\) with \(I_p\subseteq [0,\infty)\), or symmetrically \(I_q\subseteq (-1,0]\) with \(I_p\subseteq (-\infty,0]\). In particular, if \(\eta\in(0.1,0.5)\) and \(\texttt{a},\texttt{b},\texttt{c}\in\{0,1\}\), then for \(p=\texttt{b}\cdot\texttt{c}\) and \(q=\eta\cdot\texttt{a}\), we have \(I_p\cap\mathbb{Z}=\{0,1\}\) and \(I_q\subseteq [0,0.5]\), so \(\mathrm{NoCarry}(I_p,I_q)\) holds and \[[\![\texttt{int}(\eta\cdot\texttt{a}+\texttt{b}\cdot\texttt{c})]\!]^{\sharp} = \langle \texttt{b}\cdot\texttt{c}\rangle.\] If none of the three cases holds, then: \[\frac{\neg C_{int}^1(e) \wedge \neg C_{int}^2(e) \wedge \neg C_{int}^3(e)}{[\![\texttt{int}(e)]\!]^{\sharp}=\langle \mathbf{Sym}([\![e]\!]^{\sharp})\rangle }\]

2.2.0.4 Operator random\((\cdot, \cdot)\)

Each occurrence of \(\texttt{random}(L,U)\) is abstracted as a fresh real-valued symbol \(\texttt r\) with bounds \([L,U]\). This rule is used only when \(L,U\in\mathbb{Q}\) are constants independent of all measurement-bound inputs. The generated symbol does not coincide with any symbol already used in the current analysis and carries no measurement dependency: \[\frac{ \begin{array}{c} L, U\in\mathbb{Q} \wedge \texttt{r}=\mathrm{gen}\text{-}\mathrm{fresh}()\wedge \mathbf{Dom}(\texttt{r})=\boldsymbol{real} \wedge \mathbf{B}(\texttt{r})=[L,U] \end{array} }{[\![\texttt{random}(L,U)]\!]^{\sharp}=\langle \texttt{r}\rangle}\] where \(\mathrm{gen}\text{-}\mathrm{fresh}()\) picks a fresh symbol for this particular occurrence of \(\texttt{random}\).

2.2.0.5 Function calls

We assume that function calls appearing in expressions are total, pure, and side-effect free, and the return can depend only on the values of arguments. We conservatively track the union of the argument supports: \[\frac{ n\in\mathbb{N} \wedge \bigcup_{i=1}^{n} \mathbf{Sym}([\![\texttt{a}_i]\!]^{\sharp}) = D_{\texttt{f}} }{ [\![ \texttt{f}(\texttt{a}_1,\dots,\texttt{a}_n) ]\!]^{\sharp} = \langle D_{\texttt{f}}\rangle }\]

2.3 Abstract effects↩︎

Abstract effects define how statements change the abstract state. We write \((\rho,C_{\texttt{ctrl}})\;\xRightarrow{\;S_b\;}\;(\rho',C_{\texttt{ctrl}}')\) for the abstract execution of a statement block \(S_b\) from state \((\rho,C_{\texttt{ctrl}})\) to \((\rho',C_{\texttt{ctrl}}')\), where \(S_b\) could be an empty statement, a single statement, or sequential composition of multiple statements. For conciseness, we omit the rules defining abstract effects on \(\mathbf{Dom}\) and \(\mathbf{B}\).

2.3.0.1 Sequencing

For statements \(S\), \(T\), we write \(S;T\) for sequencing: \[\frac{ (\rho,C_{\texttt{ctrl}}) \xRightarrow{ S } (\rho_1,C_{\texttt{ctrl}}^1) \wedge (\rho_1,C_{\texttt{ctrl}}^1) \xRightarrow{ T }(\rho_2,C_{\texttt{ctrl}}^2) }{ (\rho,C_{\texttt{ctrl}})\;\xRightarrow{\;S;T\;}\;(\rho_2,C_{\texttt{ctrl}}^2) }\]

2.3.0.2 Assignments and returns

Evaluate the expression and update \(\rho\): \[\frac{\rho'=\rho\oplus\{\texttt{x}\mapsto [\![e]\!]^{\sharp}\}}{(\rho, C_{\texttt{ctrl}}) ~\xRightarrow{\;\texttt{x := }e } (\rho', C_{\texttt{ctrl}})}\; \frac{ \rho'=\rho\oplus\{\texttt{return}\mapsto [\![e]\!]^{\sharp}\} }{ (\rho,C_{\texttt{ctrl}})\;\xRightarrow{\;\texttt{return }e }\;(\rho',C_{\texttt{ctrl}}) }\] where \(\oplus\) denotes updating the environment with the information in its second/right operand.

2.3.0.3 Conditionals

For \(S_{\texttt{cond}}\equiv\texttt{if (cond) then }S_t\texttt{ else }S_e\), we simulate both of the branches from the same input state and then merge their outputs variable-wise: if both branches yield the same abstract value for a variable, we keep it; otherwise we conservatively union their dependencies. If the abstract return values differ or some variable either differs between branches or appears in dependence form, then any measurement input that can affect cond is added to \(C_{\texttt{ctrl}}\): \[\frac{ (\rho,C_{\texttt{ctrl}}) \xRightarrow{S_t}(\rho_t,C_{\texttt{ctrl}}^t)\wedge (\rho,C_{\texttt{ctrl}}) \xRightarrow{ S_e\;} (\rho_e,C_{\texttt{ctrl}}^e) }{ (\rho,C_{\texttt{ctrl}})\;\xRightarrow{S_{\texttt{cond}} }\;(\rho_t \sqcup_{\mathrm{env}} \rho_e, C_{\texttt{ctrl}}') }\] where \[(\rho_a \sqcup_{\mathrm{env}} \rho_b)(\texttt{x}) = \begin{cases} \rho_a(\texttt{x}), & \mathsf{Eq}_{\mathrm A}(\rho_a(\texttt{x}),\rho_b(\texttt{x})),\\[1mm] \big\langle \mathbf{Sym}(\rho_a(\texttt{x})) \cup \mathbf{Sym}(\rho_b(\texttt{x})) \big\rangle, & \text{otherwise,} \end{cases}\] and \[C_{\texttt{ctrl}}' = C_{\texttt{ctrl}}^t \cup C_{\texttt{ctrl}}^e \cup \begin{cases} \{\texttt{m}\in\mathbf{M}\mid \texttt{m}@0\in\mathbf{Sym}([\![\texttt{cond}]\!]^{\sharp})\}, & \text{Diff}_{\rho_t,\rho_e},\\[1mm] \varnothing, & \text{otherwise,} \end{cases}\] where \(\text{Diff}_{\rho_t,\rho_e} = \exists \texttt{x}\in\mathcal{V}\cup\{\texttt{return}\}:\; \neg \mathsf{Eq}_{\mathrm A}(\rho_t(\texttt{x}),\rho_e(\texttt{x}))\).

2.3.0.4 Bounded lookahead for a common post-conditional return

A common pattern in hybrid host code is a structured conditional with return-free branches followed by one common return: \(S_{\texttt{if-ret}} \;\equiv\; \texttt{if (cond) then } S_t \texttt{ else } S_e \texttt{; return } e\), where \(S_t\) and \(S_e\) contain no return. We first analyze the two branches from the same input state, and then evaluate the common return expression once under each branch environment: \[\frac{ (\rho,C_{\texttt{ctrl}}) \xRightarrow{S_t} (\rho_t,C_{\texttt{ctrl}}^t) \;\wedge\; (\rho,C_{\texttt{ctrl}}) \xRightarrow{S_e} (\rho_e,C_{\texttt{ctrl}}^e) \;\wedge\; R_t = [\![e]\!]^{\sharp}_{\rho_t} \;\wedge\; R_e = [\![e]\!]^{\sharp}_{\rho_e} }{ (\rho,C_{\texttt{ctrl}}) \;\xRightarrow{S_{\texttt{if-ret}}}\; \bigl(\rho', C_{\texttt{ctrl}}'\bigr) }\] where \[\rho' = (\rho_t \sqcup_{\mathrm{env}} \rho_e) \oplus \{\texttt{return} \mapsto (R_t \sqcup_{\mathrm{A}} R_e)\},\] \[R_t \sqcup_{\mathrm{A}} R_e = \begin{cases} R_t, & \mathsf{Eq}_{\mathrm A}(R_t,R_e),\\[1mm] \bigl\langle \mathbf{Sym}(R_t)\cup \mathbf{Sym}(R_e)\bigr\rangle, & \text{otherwise,} \end{cases}\] and \[C_{\texttt{ctrl}}' = C_{\texttt{ctrl}}^t \cup C_{\texttt{ctrl}}^e \cup \begin{cases} \{\texttt{m}\in \mathbf{M}\mid \texttt{m}@0 \in \mathbf{Sym}([\![\texttt{cond}]\!]^{\sharp}_{\rho})\}, & \neg \mathsf{Eq}_{\mathrm A}(R_t,R_e),\\[1mm] \varnothing, & \text{otherwise.} \end{cases}\] Here the subscript in \([\![e]\!]^{\sharp}_{\rho_t}\) indicates that the abstract evaluation of \(e\) is performed under environment \(\rho_t\), and similarly for \(\rho_e\).

2.4 Detection of non-contributory values↩︎

After running the above stated static analysis on the host program, let \((\rho^\star, C_{\texttt{ctrl}}^\star)\) be the final abstract state produced by the host-side analysis. The set of symbols that are measurement-originated and may affect the observable host return is \[\mathbf{Obs}(\rho^\star, C_{\texttt{ctrl}}^\star) = \bigl(\mathbf{Sym}(\rho^\star(\texttt{return})) \cap \{\texttt{m}@0 \mid \texttt{m}\in\mathbf{M}\}\bigr) \cup \{\texttt{m}@0 \mid \texttt{m}\in C_{\texttt{ctrl}}^\star\}.\] Accordingly, the set of non-contributory measurement-bound variables is \[\mathbf{M}_{\mathrm{nc}} = \{\texttt{m}\in\mathbf{M}\mid \texttt{m}@0 \notin \mathbf{Obs}(\rho^\star, C_{\texttt{ctrl}}^\star)\}.\] 10 summarizes this procedure.

2.5 Soundness of Host-side Analysis↩︎

We summarize the formal connection between the concrete host semantics and the abstract analysis; detailed proofs are given in 5.4.

2.5.0.1 Concrete and abstract states.

For the proof, we use instrumented concrete states \(s=(\nu,\sigma,\delta)\), where \(\nu\) is a valuation of symbols in \(\Sigma\) respecting \(\mathbf{Dom}\) and \(\mathbf{B}\), \(\sigma\) maps variables in \(\mathcal{V}\cup\{\texttt{return}\}\) to concrete runtime values, and \(\delta:\mathcal{V}\cup\{\texttt{return}\}\to 2^{\mathbf{M}}\) records the exact set of measurement-bound variables on which each current runtime value semantically depends. The component \(\delta\) is ghost state used only in the proof; erasing it yields the ordinary concrete execution. The concrete collecting domain is \(2^{\mathcal{S}_{\mathrm c}}\), ordered by set inclusion.

The abstract states are the ones used by the analysis above: a state has the form \((\rho,C_{\texttt{ctrl}})\), together with the auxiliary maps \(\mathbf{Dom}\) and \(\mathbf{B}\), where \(\rho:\mathcal{V}\cup\{\texttt{return}\}\to\mathcal{A}\), \(C_{\texttt{ctrl}}\subseteq\mathbf{M}\). Here \(\mathcal{A}\) is the abstract-value domain from 2.1.

2.5.0.2 Description relation and concretization.

For an abstract value \(A\), define its measurement support as \(\mathbf{MSym}_{\mathbf{M}}(A) = \{\,\texttt{m}\in\mathbf{M} \mid \texttt{m}@0\in\mathbf{Sym}(A)\,\}\). A concrete value-dependency pair \((v,S_D)\) is described by \(A\) under \(C_{\texttt{ctrl}}\), written \((v,S_D)\Delta(A,C_{\texttt{ctrl}})\), if \(S_D\subseteq \mathbf{MSym}_{\mathbf{M}}(A)\cup C_{\texttt{ctrl}}\), and additionally, when \(A=\langle p\rangle\) is a polynomial form, \(v=\nu(p)\). For \(A=\bot\), we require that no concrete return value has been produced yet and \(S_D=\varnothing\). We lift \(\Delta\) pointwise to states. We write \(s\Delta(\rho,C_{\texttt{ctrl}})\) iff for every \(\texttt{x}\in\mathcal{V}\cup\{\texttt{return}\}\), \((\sigma(\texttt{x}),\delta(\texttt{x})) \Delta (\rho(\texttt{x}),C_{\texttt{ctrl}})\). The concretization of an abstract state is therefore \(\gamma(\rho,C_{\texttt{ctrl}}) = \{\,s\in\mathcal{S}_{\mathrm c} \mid s\Delta(\rho,C_{\texttt{ctrl}})\,\}\). We order abstract states by the concrete states they describe: \[(\rho_1,C_{\texttt{ctrl}}^1)\sqsubseteq_{\gamma} (\rho_2,C_{\texttt{ctrl}}^2) \quad\Longleftrightarrow\quad \gamma(\rho_1,C_{\texttt{ctrl}}^1) \subseteq \gamma(\rho_2,C_{\texttt{ctrl}}^2).\] Thus smaller concretizations are more precise.

2.5.0.3 Transfer soundness.

Let \(F_{S_b}\) be the concrete transfer of a statement block \(S_b\): \(F_{S_b}(X) = \{\,s'\mid \exists s\in X:\;s\xrightarrow{\;S_b\;}s'\,\}\). If the abstract transfer defined in 2.3 derives \((\rho,C_{\texttt{ctrl}}) \xRightarrow{\;S_b\;} (\rho',C_{\texttt{ctrl}}')\), then \[F_{S_b}\bigl(\gamma(\rho,C_{\texttt{ctrl}})\bigr) \subseteq \gamma(\rho',C_{\texttt{ctrl}}'). \] The proof is by induction over expressions and statements, using the rules in [subsec:abs-eval] [subsec:abs-effect]; see 5.4.

Applying \((\mathrm{AI}\text{-}\mathrm{S})\) to the whole host program \(H\) shows that the final abstract state \((\rho^\star,C_{\texttt{ctrl}}^\star)\) over-approximates the exact measurement dependencies of the concrete host return. Therefore \(\mathbf{Obs}(\rho^\star,C_{\texttt{ctrl}}^\star)\) over-approximates all measurement-originated symbols that can affect the return, and every \(\texttt{m}\in\mathbf{M}_{\mathrm{nc}}\) reported by find_nc is semantically non-contributory to the host return.

2.6 Examples↩︎

The following examples illustrate how our static analysis detects non-contributory measurement outcomes. Each example is presented in a step-by-step form: after every program statement, we show, on the comment line beginning with //, the corresponding abstract state produced by our static analysis.

2.7 Integration with circuit-level simplification↩︎

\(\mathbf{M}_{\mathrm{nc}}\) denotes the set of measurement outcomes identified as non-contributory by our analysis. In this section, we integrate the analysis into the circuit simplification pipeline so that every gate acting solely within the causal cones of \(\mathbf{M}_{\mathrm{nc}}\) is safely removed. \(Q\) denotes the set of circuit qubits, and the measurement map \(\mu:Q\rightharpoonup\mathcal{V}\) maps each measured qubit to the host variable that stores its outcome. For a measured qubit \(q\), its backward causal cone is the set of gates and wire segments that can reach the terminal measurement of \(q\) by following the circuit forward through wires and multi-qubit gates. A gate whose forward influence reaches only qubits mapped to \(\mathbf{M}_{\mathrm{nc}}\) is dead.

The workflow is 9. \(\mathrm{\small find\_nc}\) runs the host-side analysis to compute \(\mathbf{M}_{\mathrm{nc}}\), whose elements we map back to their qubits and treat as dead in the DGE sense. Any gate whose effects propagate only to dead qubits cannot change observable behaviour, so we sweep the circuit, delete such gates, and grow the dead-qubit set backwards along causal cones.

2.8 Asymptotic analysis↩︎

1 shows that, for typical hybrid programs with bounded abstract value sizes, our static analysis scales linearly in program size, enabling fast optimization on large codes. 2 provides the corresponding efficiency guarantee for the host-aware circuit optimization in 9, and 1 states its worst-case time complexity of our static analysis.

Let \(n\) be the number of operators in the host program, counting arithmetic, int\((\cdot)\), random\((\cdot,\cdot)\), conditionals, and function calls. Let \(|\mathcal{V}|\) be the number of variables tracked in the abstract environment, \(\mathcal{N}\) the maximum number of monomials appearing in any polynomial-form abstract value, and \(|D|\) the maximum size of any dependence-form symbol set. Detailed proofs are in 5.5.

2.9 Levelized SSA for GPU Acceleration↩︎

9 invokes find_nc to compute \(\mathbf{M}_{\mathrm{nc}}\), which, in this subsection, we discuss how to accelerate with GPUs. However, the challenge is, as confirmed later in the last report in 3.2, that directly applying GPU acceleration to the original host-side static analysis brings no practical benefit.

To expose parallel work, we lower the host program \(H\) to an SSA-style, levelized intermediate representation \(\widehat{H} = (\mathcal{L}_0,\mathcal{L}_1,\ldots,\mathcal{L}_{K-1})\), where each instruction writes a fresh destination and each level \(\mathcal{L}_k\) contains instructions that can be evaluated in static analysis in parallel. Writing \(\mathrm{Def}(\mathcal{L}_k)\) for the set of destinations defined in level \(\mathcal{L}_k\), and \(\mathrm{Use}(s)\) for the operands read by instruction \(s\), the lowering satisfies \(\forall s \in \mathcal{L}_k:\mathrm{Use}(s) \subseteq \Sigma_0 \cup \bigcup_{j<k}\mathrm{Def}(\mathcal{L}_j)\). Hence, two instructions in the same level never have read-after-write, write-after-read, or write-after-write hazards.

The host program \(H\) is lowered in two steps. First, it performs a semantics-preserving SSA/three-address expansion. Each assignment or return expression is decomposed into primitive operators already supported by our transfer functions, namely binary arithmetic, int\((\cdot)\), random\((\cdot,\cdot)\), conservative unknown calls, and branch merges. Every definition is rewritten to a fresh destination name. Nested expressions are flattened so that each lowered instruction contains only one primitive operator, and the final returned value is still written to the distinguished variable \(\texttt{return}\). For a structured conditional, we lower the two branches recursively and make the merge explicit by an instruction of the form \(u := \phi_{\mathrm{if}}(c,v_t,v_e)\), where \(c\) is the value of the condition, and \(v_t,v_e\) are the values produced by the then/else branches.

Second, the resulting SSA program is levelized. Let \(\lambda(v)\) denote the level at which the SSA value \(v\) becomes available. For any SSA value whose current SSA version is not defined by another lowered instruction we set \(\lambda(v)=-1\). For each lowered instruction \(s\), we then assign its level \(\ell(s)\) by the earliest-ready rule \(\ell(s)= 1+\max\bigl(\{-1\}\cup\{\lambda(v)\mid v\in \mathrm{Use}(s)\}\bigr)\), and define \(\mathcal{L}_k=\{\,s \mid \ell(s)=k\,\}\).

To make the levelized lowering concrete, see 7.

The GPU backend processes one level at a time: for each \(\mathcal{L}_k\), it launches \(|\mathcal{L}_k|\) threads, one thread per instruction, and synchronizes only between consecutive levels. As destinations within a level are disjoint and every source operand comes from an earlier level, the result is independent of the intra-level execution order.

Preservation of the lowered analysis. The GPU backend changes the representation and schedule of the host-side analysis, but it should not change the analysis result. 5.6 gives more details in showing that the above lowering is semantics-preserving with respect to our host-side analysis.

3 Evaluation↩︎

Our evaluation serves two complementary goals. (i) Effectiveness in 3.1: we evaluate whether the implemented host-aware optimization exposes circuit reductions missed by circuit-only optimizers. We first run \(3\) diagnostic workloads as smoke tests, then measure \(24\) upstream-artifact-driven workloads across quantum chemistry, quantum optimization, quantum machine learning, and quantum finance, with four controls checking the expected dead-set behavior. We compare our pass against Qiskit, t\(\ket{\text{ket}}\), and PyZX, and compose it before and after each optimizer, to quantify the benefit beyond reach of optimizers not taking host programs into account. We also compare against a syntactic host-liveness baseline, which distinguishes dead measurements detectable by syntactic liveness from those exposed only by our semantic reasoning. (ii) GPU acceleration in 3.2: we isolate the host-side static analysis \(\mathrm{\small find\_nc}(\cdot,\cdot)\) and compare a sequential baseline against a CUDA backend on controlled synthetic host programs with tunable structural parallelism. In addition, we verify that directly accelerating the original host-side static analysis on GPUs is ineffective, motivating the levelized-SSA lowering introduced in 2.9.

3.1 Effectiveness↩︎

We evaluate whether the host-side analysis exposes optimizations that are missed by circuit-only optimizers. We use the following pipelines:

• Pipeline q: Qiskit’s transpile at optimization level 3, using its default target-agnostic configuration.

• Pipeline t: t\(\ket{\text{ket}}\) backend-agnostic optimization sequence DecomposeBoxes \(\rightarrow\) PeepholeOptimise2Q \(\rightarrow\) KAKDecomposition \(\rightarrow\) CommuteThroughMultis \(\rightarrow\) CliffordSimp \(\rightarrow\) RemoveRedundancies \(\rightarrow\) FullPeepholeOptimise. We invoke CliffordSimp with qubit permutations/SWAP introduction disabled when supported, so that this pipeline remains hardware agnostic.

• Pipeline p: PyZX’s full_optimize, which converts the circuit to a ZX graph, applies ZX rewrites, and extracts a simplified circuit.

• Pipeline h: our host-aware optimization. It first runs the host-side dependency analysis to compute which measurement variables can affect the host return value. Measurements outside this dependency set are mapped back to quantum wires, and the corresponding dead backward cones are removed.

• Pipeline l: a syntactic host-liveness baseline. Following the standard backward live-variable/data-flow formulation for imperative programs [8], [9], it starts from the host return expression and propagates liveness backward through assignments and branch guards. The baseline is control-dependence-aware, but purely syntactic: it does not simplify arithmetic expressions, zero coefficients, equivalent branches, or bounded int/floor residuals. 13 summarizes its implementation.

• Pipelines qh, hq, th, ht, ph, and hp: compositions of the above pipelines, where the concatenation “XY” means “run X, then Y”.

Smoke test. We first run our method on three small but realistically designed diagnostic workloads. Its setup and results are in 5.1.

The main effectiveness evaluation uses \(24\) upstream-artifact-driven workloads, six each from quantum chemistry, quantum optimization, quantum machine learning, and quantum finance. Each main workload is paired with a workload-specific quantum kernel derived from the MQTBench benchmark templates [40] and stored as an OpenQASM. The host program consumes measurement variables produced by the quantum kernel and computes an application-level quantity, such as an energy estimate, a QUBO objective value, a classifier score, or a financial payoff/risk quantity. The upstream artifacts model application-side preprocessing outputs like screened Hamiltonian terms, symmetry-sector certificates, QUBO presolve reports, sparse trained-model weights, portfolio exposures, and risk-reporting policies. A detailed description of the workloads is in 5.3. These artifacts define the host-side computation, and our host-side analysis computes which measurement variables are semantically irrelevant to the final host return value, driving DGE to prune quantum circuits.

We additionally run \(4\) control workloads. These controls are excluded from aggregate effectiveness numbers in 1. They are used only to validate the analysis: two all-live negative controls, one positive control with an expected screened chemistry tail, and one zero-weight trap control in which a locally zero coefficient does not make the corresponding measurement dead because the same feature is still used by an auxiliary live term.

Before recording metrics, each resulting circuit is canonicalized to the common basis \(\{\texttt{rz},\texttt{sx},\texttt{x},\texttt{cx}\}\). Here rz is a rotation around the \(Z\) axis, sx is the square-root of the Pauli-\(X\) gate, x is the Pauli-\(X\) bit flip, and cx is controlled-\(X\)/CNOT. We use this basis only to canonicalize gate counts across toolchains, not as a hardware target model. For each resulting circuit, we record the number of one-qubit gates, two-qubit gates, and circuit depth, excluding terminal measurements from the gate counts and depth. We also record total-gate percentage reduction, where total gates are defined as the sum of one- and two-qubit gates. The experiments run with Python 3.8.10 under WSL2 with Qiskit 0.46.3, pytket 1.3.0, PyZX 0.7.3.

Results. 1 summarizes the aggregate total-gate reductions on the \(24\) main workloads. Running our host-aware pass alone reduces total gate count by \(38.0\%\) on average. More importantly, the host-side analysis remains effective when composed with standard circuit-only optimizers. When applied after the circuit optimizer, it yields an additional \(31.6\%\) mean total-gate reduction after Qiskit, \(31.1\%\) after t\(\ket{\text{ket}}\), and \(31.1\%\) after PyZX. We also observe essentially the same reductions when the host-aware pass is applied before Qiskit or t\(\ket{\text{ket}}\) and the resulting circuit is then optimized, with means of \(31.6\%\) and \(31.1\%\), respectively. For PyZX, the pre-optimization composition is slightly less favorable but still gives a \(30.8\%\) mean reduction relative to PyZX alone.

4pt

3 breaks down the post-optimizer reductions per workload. The benefits appear across all four application families rather than being concentrated in a single domain. Chemistry and finance workloads exhibit more moderate but still consistently positive reductions, reflecting smaller or more localized dead backward cones than other workloads.

As a side check closer to the novelty of the host analysis, we also compare against the syntactic liveness baseline l. To isolate the contribution of the host-side dead-measurement discovery from the circuit-pruning backend, we feed the dead measurements found by l and by our semantic analysis h into the same DGE backend. 2 reports both the measurement-level dead sets and the resulting circuit-level reductions. The baseline l identifies \(21\) dead measurement variables and reduces total gate count by \(5.06\%\) on average, while h identifies \(92\) dead measurement variables and reduces total gate count by \(37.98\%\) on average under the same DGE backend. Hence \(71\) dead measurements are semantic-only opportunities not recovered by the syntactic baseline.

3pt

As shown in 3, both all-live negative controls produce an empty dead-measurement set and zero host-induced savings. The positive control recovers exactly the expected screened measurements, while the zero-weight trap control also produces an empty dead set because the zero-weighted feature remains live through an auxiliary term.

4pt

Overall, these results show that host-side semantic information is complementary to circuit-only optimization. Circuit optimizers can simplify the quantum circuit structure, but they do not know which measured values are semantically consumed by the host computation. Our analysis exposes this information and enables additional dead-gate elimination even after Qiskit, t\(\ket{\text{ket}}\), and PyZX have optimized the same circuits. Combined with the result from 5.1, the best composition order is workload-dependent: in some cases applying h after a circuit-only optimizer is better, in some cases applying h first exposes more downstream simplification, and in other cases the order has little or no effect.

3.2 GPU acceleration of host-side analysis↩︎

Our goal in this subsection is to quantify the practical effect of GPU acceleration on the host-side static analysis find_nc\((\cdot,\cdot)\) (10). To this end, we compare a sequential baseline against a GPU backend over a family of synthetic host programs whose size, source-level parallel structure, and symbolic coupling can be varied independently.

Setting. Each generated input is an imperative host program with exactly \(|\mathbf{M}|\) measurement-bound inputs and \(s_h\) source statements. As illustrated in 4, generation is organized around active chains, each of which maintains its own current frontier value and advances mostly independently before the final reduction to return. A structural-parallelism knob \(p \in [0,1]\) determines the number of chains. Given \(|\mathbf{M}|\) and \(s_h\), we compute \(n_{\max}= \min\!\left( |\mathbf{M}|, \left\lfloor \frac{s_h+1}{2} \right\rfloor \right), n_{\mathrm{chain}}= 1+\left\lfloor p\,(n_{\max}-1)\right\rfloor\). This reserves \(n_{\mathrm{chain}}-1\) statements for the final reduction and leaves \(s_{\mathrm{body}} = s_h - (n_{\mathrm{chain}}-1)\) statements for the body. Round by round, each chain with remaining budget emits one statement that overwrites one variable in its small working set. Statements are sampled from the primitive operator family in 2; each non-constant operand is drawn from the same chain with probability \(1-\chi\) and from a different chain with probability \(\chi\), where \(\chi \in [0,1]\) controls cross-chain reads.

The sequential baseline analyzes the original host program directly on CPU, in source order, using a serial implementation of the host-side analysis. The GPU backend first lowers the host program on the CPU to the levelized SSA representation of 2.9 and then executes the resulting parallel analysis tasks on the GPU using CUDA. Both executables are compiled with nvcc 12.8.93. All experiments are run on the same node, where two NVIDIA H100 NVL devices are visible to the process. For every design point, both implementations analyze exactly the same program. Each point is instantiated by one deterministic source program from a fixed seed and timed over \(10\) repetitions after \(3\) warmup runs. The reported running time of the GPU backend includes both the CPU-side lowering time and the GPU execution time.

Results. Across all tested design points, the CUDA backend produced the same analysis result as the sequential baseline. We first summarize the speedup landscape in (a) of 5. Using the experimental setup described above, we sweep \(|\boldsymbol{M}|\in\{32,64,128,256\}\) and \(s_h\in\{1024,2048,4096,8192\}\), and evaluate the speedup as \(T_{\mathrm{seq}}/T_{\mathrm{gpu}}\) for several representative source-level parallelism settings. The trend is clearly visible: GPU acceleration becomes stronger as either the number of measurement-bound inputs \(|\boldsymbol{M}|\) or the host-program size \(s_h\) increases, and this trend is amplified by larger \(p\). This directly supports the intuition that, once lowering exposes sufficient structural parallelism in the host-side analysis, the analysis admits substantial parallel execution.

We next make the break-even behavior explicit in (b) of 5. This figure uses the same experimental sweep, but now keeps a larger set of parallelism settings \(p\in\{0,0.125,0.25,0.5,0.75,1.0\}\) and groups the results by the source host size \(s_h\). Each cell is still annotated by the measured speedup, but the background color indicates whether the GPU backend wins (\(\mathrm{speedup}>1\)) or loses (\(\mathrm{speedup}<1\)). The resulting phase diagram shows a clear break-even boundary. For the smallest host size (\(s_h=1024\)), the GPU backend requires moderate structural parallelism to become worthwhile. As the source host size increases, this boundary shifts leftward. By \(s_h=4096\) or \(8192\), the GPU backend already wins on all tested combinations.

Why lowering matters. We also examine what happens if the host-side analysis is moved to the GPU directly on the original host program, without first applying the levelized SSA lowering of 2.9. We compare two implementations of the same host-side analysis: the first, which we call the source-order CUDA implementation, analyzes the original host program directly on GPUs; the second remains the sequential baseline we used in our previous experiments. For each design point \((|\boldsymbol{M}|, s_h)\), we try all tested values of the requested structural parallelism \(p\) and record the best speedup over the sequential baseline observed for that design point. Across all tested design points, the source-order CUDA implementation remains far below break-even: even the best observed speedup lies only in the range \(0.026\times\)–\(0.035\times\). This is expected: in its original form, the analysis exposes too little regular parallel work for SIMT execution, so kernel-launch overheads, irregular memory access, and synchronization costs dominate the useful computation. Thus, useful GPU acceleration requires the lowering step of 2.9 to expose additional parallelism first.

4 Conclusion↩︎

We present a static analysis to identify non-contributory measurement outcomes in hybrid quantum-classical programs and drive DGE circuit optimization. Our pass is orthogonal to existing circuit optimizers, yielding substantial circuit simplification both on its own and in composition with Qiskit, t\(\ket{\text{ket}}\), and PyZX. We further showed that, after lowering exposes sufficient level-wise parallelism, the host-side analysis admits an efficient GPU backend.

5 Appendix↩︎

5.1 Evaluation on diagnostic workloads↩︎

In addition to the application-faithful workloads in 3.1, we also implement three small diagnostic workloads with VQE-style and QPE-style kernels. These workloads are intentionally small and inspectable: the expected non-contributory measurements can be checked manually, which makes them useful for validating individual transfer rules, measurement-to-qubit mappings, and the end-to-end dead-gate elimination pipeline. They also serve as lightweight smoke tests for reproducing our artifact: before running the full application-faithful suite, one can run these diagnostic instances to check that the host analysis, circuit optimizers, canonicalization step, and pipeline compositions produce the expected behavior. These workloads are not intended to establish workload representativeness, and we therefore exclude them from the aggregate statistics and main effectiveness claims in 3.1. We run the same experimental setup as in 3.1 and report the diagnostic results in [table:resulting-circuits-metrics-toy,table:relative-optimization-toy].

Results. The results on our diagnostic workloads also give supportive evidence. Our host-aware pass h is effective on its own and yields orthogonal gains when composed with state-of-the-art optimizers (Qiskit, t\(\ket{\text{ket}}\), PyZX). As 4 shows, applying h already simplifies the circuits substantially: on 6 it prunes all gates; on 7 it reduces the metrics from \((82,26,61)\) to \((12,0,6)\), eliminating all two-qubit gates; on 8 it shrinks these metrics from \((40,16,37)\) to \((31,9,31)\). 5 further shows that inserting h around Qiskit/t\(\ket{\text{ket}}\)/PyZX yields large additional reductions over each optimizer’s standalone output. Running h before the optimizer sometimes exposes more simplifications (e.g., \(\hyperlink{passsettings}{\boldsymbol{q}}\!\to\!\hyperlink{passsettings}{\boldsymbol{hq}}\) achieves \((100\%,100\%,100\%)\) extra savings on 6 and \((83\%,100\%,90\%)\) on 7), while running h afterwards remains quite beneficial. The only minor adverse effect is for t\(\ket{\text{ket}}\) on 8 when applied after h\(\,\): single-qubit gates increase by 13%, but two-qubit gates drop by 40%, a favourable trade-off. Overall, these results corroborate: our host-semantics-aware optimization prunes result-invariant gates that host-unaware optimizers cannot, and composing h with existing toolchains amplifies simplification beyond their reach.

5.2 Pseudo-code implementations↩︎

In 11, InitAbsState creates the initial abstract environment and marks measurement-bound variables as binary inputs. In 12, AnalyzeBlock performs one forward abstract execution of the host block, using the expression transfer rules in 2.2 and the statement effects in 2.3. In 10, find_nc further uses the outcome of 11 12 to compute a set of non-contributory measurement outcomes.

13 14 describe a standard backward live-variable analysis over the host program, augmented only with conservative control dependence through branch guards. The operator \(\mathrm{Vars}(e)\) returns variables syntactically occurring in \(e\); it does not perform algebraic simplification. Thus, for example, \(\mathrm{Vars}(0\cdot\texttt{m})=\{\texttt{m}\}\) and equivalent branch returns are not identified as equal.

In 9, \(Q\) denotes the set of qubits. The call \(C_{\text{opt}}.\boldsymbol{frontier}()\) returns the current output-side frontier: the operators adjacent to terminal measurements. The procedure CloseUnderCones\((C_{\text{opt}},\mathbf{Q}_{\text{dead}})\) propagates deadness backward through the remaining circuit: whenever all output-side wire segments of a operator lead only to qubits in \(\mathbf{Q}_{\text{dead}}\), the input-side wire segments are also marked dead.

5.3 Application-faithful workload descriptions↩︎

5.3.0.1 Quantum chemistry workloads.

These workloads model VQE-style molecular-estimator post-processing. The quantum kernels prepare parameterized Ansatz states and measure Pauli-style observable groups. The host programs map measured bits to Pauli eigenvalue variables, aggregate weighted Pauli products, and return an energy or selected molecular-property estimate. Such host-side Hamiltonian averaging and measurement aggregation are standard in VQE and near-term quantum chemistry workflows [41]–[43].

C1-pauli.

This workload represents a VQE energy-estimation step after Hamiltonian coefficient thresholding. The quantum kernel is an irregular RealAmplitudes VQE-style ansatz followed by measurements for Pauli-estimator groups. The host program converts each measurement bit into a Pauli eigenvalue and computes a weighted sum of Pauli products. The upstream chemistry artifact contains a screened low-magnitude Hamiltonian tail term; therefore, the measurements used only by that screened term no longer affect the returned energy. This models the common situation in which a chemistry workflow discards small Hamiltonian coefficients or measurement terms to reduce estimator cost [41], [42], [44].

C2-symmetry.

This workload models an estimator that uses known symmetry or tapering-sector information. The quantum kernel is an EfficientSU2/two-local VQE-style ansatz with nonuniform measurement groups. The host program first applies upstream constant replacements for measurements whose Pauli eigenvalues are fixed by a symmetry-sector certificate, and then evaluates the remaining energy terms. The quantum and host sides cooperate as follows: the quantum circuit still produces measurement variables, but the application-level host computation knows that some variables are fixed by the physical sector and therefore overwrites them with constants. This reflects symmetry-based qubit reduction and tapering techniques used in fermionic Hamiltonian simulation [43], [45].

C3-active-space.

This workload models active-space chemistry with frozen-orbital constants. The quantum kernel is an active-space VQE-style ansatz with an irregular tail corresponding to frozen or inactive orbital lines. The host program aggregates active-space Pauli terms but replaces selected frozen-orbital measurements by constants supplied by the upstream active-space artifact. Thus, the host return value depends only on the active-space portion of the measurement record. This reflects standard chemistry preprocessing in which inactive orbitals are treated classically while only the active space is handled by the quantum computation [43], [46].

C4-screened-obs.

This workload represents grouped observable evaluation after screening low-weight Pauli blocks. The quantum kernel contains heterogeneous grouped VQE observable blocks. The host program forms a molecular estimator by summing the retained observable groups. The upstream artifact records that one low-weight observable block was removed by application-level screening, so measurements used only by that block become semantically irrelevant. This captures the common VQE practice of grouping and filtering observable terms to reduce measurement overhead [42], [44].

C5-property-report.

This workload models a shared quantum estimator used for multiple molecular properties, where the application reports only a selected property subset. The quantum kernel measures heterogeneous observable blocks that could support several property reports. The host program aggregates only the observable blocks requested by the current report. A block corresponding to an unreported property is still present in the shared quantum kernel, but its measurements do not contribute to the host return value. This is application-faithful for chemistry workflows that reuse estimator templates across related observables while reporting only selected quantities [43], [44].

C6-lowrank-tail.

This workload models a low-rank chemistry estimator with a screened tail factor. The quantum kernel follows an irregular VQE-style estimator template with nonuniform groups corresponding to retained and tail factors. The host program computes the estimator by summing the retained low-rank terms. The upstream artifact records that a small low-rank tail factor was removed, so measurements used only by that tail factor are dead with respect to the final energy estimate. This reflects low-rank Hamiltonian decompositions and truncation strategies used to reduce the resource cost of electronic-structure simulation [43], [47].

5.3.0.2 Quantum optimization workloads.

These workloads model QAOA/QUBO-style workflows. The quantum kernels prepare candidate binary assignments using irregular QAOA-style circuits. The host program interprets measurement bits as decision variables and evaluates an application objective, typically a weighted QUBO expression. The upstream artifacts model presolve, component selection, fixed variables, disabled constraints, or scenario filtering. QAOA and QUBO formulations are standard near-term optimization models [48], [49].

O1-inactive-var.

This workload models a QUBO objective after preprocessing removes all objective terms incident to one decision variable. The quantum kernel is a QAOA/QUBO circuit that still measures all candidate variables. The host program evaluates the preprocessed objective by summing the nonzero weighted edges. The inactive variable may still be measured by the quantum kernel, but because all of its incident objective coefficients are zero in the upstream presolve artifact, it cannot affect the returned score. This reflects optimization pipelines in which classical presolve removes inactive variables before objective evaluation [48], [49].

O2-component-select.

This workload models a disconnected QUBO instance where the application reports only a selected connected component. The quantum kernel prepares and measures variables for both the selected component and an omitted component. The host program evaluates only the selected component’s objective edges. Measurements belonging solely to the unreported disconnected component are irrelevant to the returned objective value. This captures the application pattern in which a decomposed optimization model is solved or reported component-wise [48], [49].

O3-penalty-filter.

This workload represents a QUBO objective with disabled penalty or constraint blocks. The quantum kernel measures variables that would support both the main objective and several penalty terms. The host program evaluates the objective using the active upstream penalty configuration. Penalty blocks with zero weights are excluded from the returned score, so variables used only inside disabled blocks do not influence the host return value. This models application workflows in which constraints, soft penalties, or regularizers are conditionally enabled or disabled by a model export [48], [49].

O4-fixed-vars.

This workload models QUBO presolve with fixed decision variables. The quantum kernel measures a full candidate assignment, but the upstream artifact records that selected variables have been fixed by classical preprocessing. The host program first overwrites those variables with constants and then evaluates the QUBO objective. A measured variable that is fixed before the objective is computed no longer contributes semantically to the returned score. This reflects standard optimization presolve, where variables can be fixed before the remaining subproblem is evaluated [48], [49].

O5-multiobj.

This workload models a multi-objective QAOA/QUBO report in which the application queries only one objective component. The quantum kernel measures variables for heterogeneous objective components. The host program returns the selected objective score and omits the unqueried component from the current report. Measurements used only by the omitted component are therefore dead with respect to the current host return value. This is faithful to optimization workflows that share a quantum candidate generator across several objectives but report only a selected objective for a particular query [48], [49].

O6-robust-scen.

This workload models robust or scenario-weighted optimization. The quantum kernel prepares a QAOA-style assignment over variables that participate in several scenario components. The host program evaluates a robust objective using only scenarios retained by the upstream scenario filter. Measurements associated solely with filtered scenarios do not affect the returned robust score. This captures application workflows where a QUBO-style objective is evaluated under a subset of active scenarios or risk cases [48], [49].

5.3.0.3 Quantum machine learning workloads.

These workloads model quantum machine learning pipelines. The quantum kernels compute feature channels, support-vector/kernel estimates, ensemble features, or class-head features. The host program aggregates these measured features using a trained classical readout, such as a sparse linear head, an SVM-style decision function, an ensemble weight vector, or a selected class query. Quantum feature maps and quantum kernel methods are standard QML patterns, and support-vector models naturally produce sparse decision functions through zero dual coefficients [50]–[52].

M1-sparse-readout.

This workload models a QNN feature extractor followed by a sparse linear readout head. The quantum kernel consists of batched, nonuniform QNN feature-channel circuits. The host program converts measurements into channel features and computes a linear logit using trained readout weights. The upstream trained-model artifact contains a zero weight for one feature channel, as would arise from sparsity-inducing training or feature selection. That channel is still produced by the quantum kernel, but it does not affect the returned logit [50], [51], [53].

M2-kernel-svm.

This workload models a quantum-kernel/SVM decision function. The quantum kernel computes heterogeneous quantum feature or kernel-estimator blocks associated with candidate support vectors. The host program evaluates an SVM-style decision score by weighting these quantum features with exported dual coefficients. Non-support vectors have zero dual coefficients in the upstream model export, so measurements used only for those entries are irrelevant to the final decision score. This follows the standard SVM structure, where the decision function is sparse in support vectors [50]–[52].

M3-ensemble.

This workload models an ensemble of QNN submodels. The quantum kernel contains batched feature-extraction blocks for several submodels. The host program computes an ensemble score by summing submodel outputs with exported ensemble weights. The upstream artifact assigns zero weights to pruned submodels, so their corresponding measured features do not affect the final ensemble score. This reflects a common inference pattern in which an ensemble or model-selection stage keeps only a subset of candidate predictors [50], [51], [53].

M4-sensor-drop.

This workload models sensor or feature-channel selection before QML inference. The quantum kernel computes nonuniform feature channels, each representing a different input sensor or feature group. The host program aggregates only the channels included in the upstream sensor manifest. A dropped sensor channel may still be present in the shared quantum kernel template, but its feature is not consumed by the host return value. This captures application pipelines in which low-quality or unavailable feature channels are excluded at inference time [50], [51].

M5-multiclass.

This workload models a multiclass QNN with several class heads, where the application queries only a subset of class scores. The quantum kernel computes heterogeneous feature blocks that can feed multiple class heads. The host program evaluates only the requested class score or subset of scores. Measurements used exclusively by unqueried class heads are therefore semantically irrelevant to the current return value. This models selective inference in multiclass QML pipelines [50], [51].

M6-calib-filter.

This workload models calibrated QNN inference with feature-channel quality filtering. The quantum kernel produces several feature channels, including an auxiliary channel marked by the upstream calibration artifact as low quality. The host program computes the calibrated readout using only channels that pass the exported calibration filter. Measurements used only by the excluded channel do not contribute to the returned logit. This is faithful to QML pipelines where calibration, data quality, or confidence filters determine which quantum features are consumed by the classical readout [50], [51].

5.3.0.4 Quantum finance workloads.

These workloads model amplitude-estimation-style finance kernels followed by classical payoff, exposure, or risk-reporting logic. The quantum kernels encode price, payoff, scenario, or risk-factor information into measured registers. The host program decodes those registers and computes a portfolio value, payoff bin, VaR-style threshold, or sensitivity report. This matches the standard quantum-finance pattern in which quantum amplitude estimation or state-preparation circuits are followed by classical post-processing for pricing and risk metrics [54]–[56].

F1-zero-exposure.

This workload models a batched portfolio payoff computation with one zero-exposure asset or scenario. The quantum kernel contains AE-style scenario/payoff blocks, and the host program decodes each measured block into a payoff value. It then multiplies each payoff by an exposure exported by the portfolio artifact and returns the portfolio sum. A scenario with zero net exposure is still measured by the quantum kernel but does not affect the portfolio value. This reflects portfolio netting or exposure filtering in financial risk and pricing workflows [54], [55].

F2-coarse-binning.

This workload models coarse-binned option payoff evaluation. The quantum kernel produces a price register. The host program decodes the register with application-level bit weights, applies integer/floor-style binning, and returns a payoff derived from the coarse bin. Low-order residual bits that cannot change the selected bin are irrelevant to the returned payoff. This captures payoff policies where only coarse price buckets matter for the reported financial quantity [55], [56].

F3-scenario-filter.

This workload models scenario-weighted risk aggregation. The quantum kernel contains batched AE-style risk-scenario blocks. The host program decodes each scenario payoff and multiplies it by an eligibility or scenario weight from the upstream risk artifact. Scenarios filtered by zero eligibility weights do not contribute to the returned risk quantity. This matches risk-analysis workflows where only selected scenarios are included in a particular report [54], [57].

F4-hedged-leg.

This workload models a basket or hedge payoff computation where one leg is hedged out. The quantum kernel prepares and measures payoff registers for multiple basket or hedge legs. The host decodes each leg and combines them using net exposure coefficients. The upstream portfolio artifact records that one hedge leg has zero net coefficient after preprocessing, so measurements used only for that leg are dead. This reflects portfolio netting and hedging logic in option-pricing and risk workflows [54], [55].

F5-var-bucket.

This workload models a VaR-style threshold report after coarse risk bucketing. The quantum kernel produces a risk-score register. The host decodes the register, applies coarse bucketization, and returns an indicator of whether the bucket crosses a risk threshold. Low-order bits below the bucket resolution cannot affect the threshold outcome, and therefore do not contribute to the host return value. This is faithful to risk analysis workflows that report thresholded risk quantities such as Value at Risk [54], [57].

F6-greek-filter.

This workload models a sensitivity or Greek report with filtered risk factors. The quantum kernel computes batched AE-style estimators for several factor groups. The host program decodes each factor output and aggregates only the risk factors retained by the upstream sensitivity report. Factors that are hedged, inactive, or excluded from the report have zero host weights and their measurements do not affect the returned sensitivity. This follows the finance pattern of combining quantum-estimated payoff or risk quantities with classical exposure and reporting logic [54], [55].

5.3.0.5 Control workloads.

The control workloads are designed to validate the host-side analysis rather than to measure effectiveness. They are excluded from aggregate effectiveness statistics. Their purpose is to check that the analysis finds the expected dead set in a positive case and, more importantly, does not prune live measurements in all-live or zero-weight-trap cases.

CTRL1-all-live-qml.

This negative control reuses the QML feature-channel structure of M1, but the upstream trained-model artifact assigns nonzero readout weights to every feature channel. The quantum kernel therefore produces features that are all consumed by the host readout. The expected dead set is empty, and the host-aware pass should not reduce the circuit.

CTRL2-all-live-opt.

This negative control reuses a QAOA/QUBO-style kernel, but every measured decision variable participates in at least one nonzero objective edge. The host program evaluates a fully live QUBO objective, so each measurement can affect the returned score. The expected dead set is empty, and any pruning would indicate a false positive.

CTRL3-derived-screened-chem.

This positive control reuses a VQE-style Pauli-estimator kernel and applies the same upstream screening logic as the chemistry workloads. The upstream artifact removes a small tail observable, and the expected dead set is known in advance. The control checks that the host-side analysis can recover the screened measurements exactly.

CTRL4-zero-weight-live-escape.

This negative trap control reuses the QML feature-channel structure of M1. The upstream artifact contains a zero primary readout weight for one feature, but the same feature is also used by an auxiliary live calibration term. The correct result is therefore an empty dead set. This control demonstrates that the analysis is semantic: it does not prune a measurement merely because the measurement appears in one zero-weighted term.

5.4 Soundness of the host-side static analysis↩︎

2.5 summarizes the concrete domain, the abstract-state order, the description relation \(\Delta\), and the concretization \(\gamma\). We now give the detailed proofs.

5.5 Proof details in 2.8↩︎

1. In the worst case, the proposed host-side static analysis runs in \(\mathcal{O}\!\left(n\cdot\mathcal{N}^2 + n\cdot|\mathcal{V}|\cdot|D|\right)\).

1. When \(\max\big(\;\mathcal{N}, |\mathcal{V}|, |D|\;\big)\) is bounded by a constant value, the worst-case time complexity of the static analysis on the host program is \(\mathcal{O} \big(n \big)\).

2. Let \(G\) be the number of gates in the input quantum circuit. The worst-case time complexity of the workflow in 9 is \(\mathcal{O}(n\cdot\mathcal{N}^2 +n\cdot|\mathcal{V}|\cdot|D| + G^2)\), and when \(\max\big(\;\mathcal{N}, |\mathcal{V}|, |D|\;\big)\) is bounded by a constant value, the complexity becomes \(\mathcal{O}(n + G^2)\).

5.6 Proof details in 2.9↩︎

During lowering, we maintain a representative map \[\kappa:\mathcal{V}\cup\{\texttt{return}\}\to \widehat{\mathcal{V}}\cup\{\texttt{return}\},\] which maps each source-level variable to its current SSA representative in the lowered program. The initial map \(\kappa_0\) maps each source variable to its incoming SSA version and maps return to return. For the whole program, we write \[(\widehat H,\kappa^\star)=\mathrm{\small lowerBlock}(H,\kappa_0),\] where \(\kappa^\star\) is the final representative map produced by the lowering.

Given a lowered abstract environment \(\widehat{\rho}\), its projection back to source-level variables under a representative map \(\kappa\) is \[\pi_\kappa(\widehat{\rho})(\texttt{x}) = \widehat{\rho}(\kappa(\texttt{x})) \qquad \text{for all } \texttt{x}\in\mathcal{V}\cup\{\texttt{return}\}.\] This projection forgets lowering-introduced temporaries and keeps only the abstract values of source-level representatives.

Let \((\rho_0,\mathbf{Dom},\mathbf{B}) = \mathrm{\small InitAbsState}(H,\mathbf{M})\). The initial lowered environment \(\widehat{\rho}_0\) is defined by \[\widehat{\rho}_0(\kappa_0(\texttt{x}))=\rho_0(\texttt{x}) \qquad \text{for all } \texttt{x}\in\mathcal{V}\cup\{\texttt{return}\}.\] The maps \(\mathbf{Dom}\) and \(\mathbf{B}\) are shared by the source and lowered analyses.

The following proposition shows that, after projecting the lowered environment back to source-level variables, the lowered analysis produces the same abstract return value and the same control-dependency set \(C_{\texttt{ctrl}}\), and therefore the same output of find_nc (10).

References↩︎