PaperlayerView exact revision on arXiv

Source-linked AI summary

Connecting Quantum Proof Systems and Hoare Logic

Liyi Li, Zoukarneini Difaizi Tagba, Alex Potanin

arXiv:2610.34723v1cs.LOcs.PL

TL;DR

Quantum verification remains time-consuming, and runtime validation is virtually impossible to develop for large quantum programs. The paper translates Qafny proof obligations into Hoare logic with array theory and establishes the translation’s completeness and soundness. The embedding makes quantum proof obligations deterministic for classical automated verifiers, while the paper cautions that some programs remain hard to verify.

  • Problem

    Runtime validation is virtually impossible to develop for large quantum programs, and existing quantum verification frameworks remain time-consuming.

    Source: §1 · p. 1

  • Method

    The paper translates Qafny into Hoare logic with array theory using classical aggregate operations and mechanizes the completeness direction in Rocq.

    Source: §1 · p. 1, §9 · p. 26

  • Results

    Translation completeness preserves Qafny derivations in Hoare logic, while translation soundness ensures a valid translated triple corresponds to a Qafny derivation with semantically equivalent conditions.

    Source: §3 · p. 8, §9 · p. 26

  • Takeaways & Limitations

    The constructive embedding makes quantum proof obligations deterministic and enables classical automated verifiers to discharge them without quantum-specific infrastructure.

    Source: §9 · p. 26

    The compilation does not claim all quantum program verification is easy; programs based on statistical methods, such as quantum machine learning, can be hard to verify.

    Source: §9 · p. 26

Abstract

from arXiv · show

Verifying quantum programs today requires specialized proof systems built on interactive theorem provers such as Rocq, Lean, Isabelle, or Why3, and even modest quantum algorithms cost substantial human effort to verify. Because quantum programs cannot be effectively checked by runtime testing, formal verification is the only viable path to correctness, making the cost of these bespoke systems the chief barrier to scalable quantum software assurance. We show that verifying a quantum program should be no harder than verifying a classical array program, a paradigm commonly used in parallel programming: the Qafny quantum proof system translates into Hoare logic with array theory completely (every Qafny proof becomes a valid Hoare triple) and soundly (a valid translated triple certifies only true quantum specifications), and we mechanize the completeness direction in Rocq. The embedding determinizes quantum proof obligations and exposes the full machinery of classical automated verifiers (e.g. Dafny and SMT-based separation logic) to quantum code, removing the need for dedicated quantum proof system infrastructure. In particular, the embedding supplies the correctness argument that the existing compilation of Qafny into Dafny lacks.

1 Introduction

Quantum program verification remains time-consuming, and the paper asks whether it can be reduced to classical verification. It compiles quantum proof systems into Hoare logic and establishes translation-level soundness and completeness.

1 Introduction

  • Runtime validation is virtually impossible to develop for large quantum programs, while existing verification frameworks and proof automation remain time-consuming.The paper frames effective compilation into a classical framework as the question of whether quantum verification is harder than classical verification.Source: §1 · p. 1
  • Classical aggregate operations provide the compilation target for transforming Qafny into Hoare logic, using a symbolic representative of the quantum state.The paper also illustrates the approach for Quantum Hoare Logic (QHL) to show its generality.Source: §1 · p. 1
  • A direct post-condition transformation can expand the quantum state into a potentially exponential listing of singleton states.The described route transforms the post-condition into a state map, converts that state using a classical structure such as a list or array, and turns it back into a predicate.Source: §1 · p. 2
  • Translation completeness and soundness relate quantum-system derivability to Hoare-logic validity, up to semantic equivalence of assertions.The paper develops these theorems in the style of compiler correctness rather than relying on proof-system soundness and relative completeness.Source: §1 · p. 2

1.1 Contributions and Roadmap

  • Qafnyc compiles Qafny verification conditions into Dafny and reports 37 verified programs, but its compilation lacks a correctness argument.This paper supplies a translation foundation for Qafny; its contributions include HLIR and showing quantum separation conjunctions can be replaced by classical conjunctions.Source: §1.1 · pp. 2–3

2 Background

The background introduces quantum data and computation, then presents Hoare logic and array reasoning as the classical setting for the paper’s verification approach.

Quantum Data

  • Quantum data can be in superposition, and multi-qubit data can be entangled rather than separable into smaller tensor-product states.The GHZ state is an example of an entangled datum.Source: §2 · p. 3

Quantum Computation and Measurement

  • Quantum circuits apply gates to qubits; the GHZ circuit uses one Hadamard and n−1 CNOT gates, while measurement extracts classical information probabilistically.Gate matrices are unitary except for measurement gates, and partial measurement can have simultaneous effects due to entanglement.Source: §2 · pp. 3–4

High-level Operation Abstraction

  • Quantum conditionals can be viewed as array maps that apply a classical operation to each basis-ket of a quantum datum.The example conditionally flips a bit in the basis-ket where the control bit is 1.Source: §2 · p. 4

Hoare Logic with Array Theory

  • A Hoare triple relates a program command to pre- and post-conditions, and array assignment rules update the array in the pre-condition.The background presents array variables as valid in the general assignment rule and describes substitution of the updated array.Source: §2 · p. 4
  • The pointwise-update lemma lets a post-condition be pushed backward through an array-producing statement by substituting its pointwise-updated array.The paper notes that this step turns each HLIR primitive’s loop into a single substitution; Qlen predicates may be assumed without explicit mention.Source: §2 · pp. 4–5

3 Overview

Using Deutsch–Jozsa as a running example, the overview recasts Qafny proof steps as classical array operations and relates Qafny derivability to Hoare logic validity.

Overview

  • The Deutsch–Jozsa example initializes x and y in uniform superposition, applies the oracle and Hadamard gates, and verifies that a constant function yields v = 0 with probability 1.The stated precondition sets x to |0⟩ and y[0] to |1⟩.Source: §3 · p. 5

Relating quantum operations with classical ones in a proof triple

  • Nested linear sums become array dimensions, with locus information used to locate the relevant ket fragments even when qubit order does not match bitstring order.A simple state-to-array mapping alone may not handle operations such as flipping a specific bit.Source: §3 · p. 6
  • The translation represents quantum data in a multidimensional array, then uses locateN, mapN, and assignN to select, transform, and merge the relevant locus vectors.The array dimension corresponds to the EN(k) state type; mapN applies the oracle function to each selected element.Source: §3 · p. 7

Overview

  • The approach is illustrated for Quantum Hoare Logic, but its full translation is left to future work.The QHL example encodes locus ranges in the corresponding basis vectors.Source: §3 · pp. 7–8

The main theorems

  • Translation completeness carries every derivable Qafny triple to a valid Hoare triple; translation soundness links a valid translated triple to a Qafny derivation with semantically equivalent conditions.Together, these directions relate derivability in the two systems.Source: §3 · p. 8
  • At most 11 HLIR statements are generated per Qafny statement, while translated assertions and proof skeletons have polynomial size in the Qafny triple and array dimension.The size bound concerns verification-condition size, not solver time.Source: §3 · p. 8

4 The Source Proof System: Qafny

Qafny is presented as the source proof system for the compilation, with imperative quantum syntax and state predicates that represent qubit heaps and track state types.

4.1 Qafny Syntax and A Running Example

  • Qafny programs combine control flow and classical assignments with quantum measurement and heap mutations that apply operations to qubit loci.Quantum mutations include state preparation, Fourier-transform, and arithmetic-oracle operations.Source: §4.1 · pp. 8–9

4.2 Quantum State Predicates and Qafny Triples

  • A Qafny state predicate maps a locus of possibly entangled qubits to a quantum datum, while ⊎ separates unentangled groups for modular reasoning.Loci identify qubit ranges, including ranges that may be entangled; the separation is analogous to separation logic’s conjunction.Source: §4.2 · p. 9, Figure 5 · p. 10
  • Qafny’s type environment classifies quantum data and tracks type changes, enabling distinct verification strategies for different state representations.Entangled EN(n) data can be represented as a linear sum of basis-kets, with loci marking potentially entangled qubit regions.Source: §4.2 · p. 10

5 Embedding Separation Conjunction and the Frame Rule

The section shows that tracked disjointness makes tensor-based quantum separation conjunctions pure, allowing ordinary conjunctions in the translated Hoare logic and frame rule.

5 Embedding Separation Conjunction and the Frame Rule

  • The purity argument relies on Qafny’s disjoint loci; languages with qubit references or reference semantics must establish disjointness separately.Without this separation, aliasing can let a modification affect a predicate that does not explicitly mention the modified location.Source: §5 · p. 11
  • When state predicates describe disjoint qubit loci, their separation conjunction can become ordinary conjunction, so translation need not add separation conjunctions to Hoare logic.The translated frame rule uses the classical side condition FV(R) ∩ mod(trans(μ)) = ∅.Source: §5 · pp. 11–12
  • For tensor-based quantum separation conjunctions, tracking disjoint qubit regions makes the conjunctions pure and equivalent to ordinary conjunctions.The result is stated to generalize across tensor-based quantum separation conjunctions.Source: §5 · pp. 11–12

6 The Intermediate Representation Language based on Hoare Logic

HLIR expresses quantum verification in classical Hoare logic with array assignments, representing entangled states as arrays and defining translation operations from essential array primitives.

6 The Intermediate Representation Language based on Hoare Logic

  • An EN(n)-typed quantum state is modeled as an n-dimensional array of basis-ket records, with separate access to each element’s amplitude and vector.HLIR uses functions to update an element’s amplitude and selected vector positions.Source: Figure 6 · p. 12, §6 · p. 13
  • The locus map records which bit-sequence indices correspond to qubits in a locus fragment, preserving their positions in the array representation.For the example state, x[0] maps to index 0 and y[0] to index 1.Source: §6 · p. 13
  • The state-shrinking lemma establishes that executing a Qafny program yields a state whose domain is a subset of the input state’s domain.The account assumes a finite global universe containing all qubits in the input state.Source: §6 · p. 13
  • HLIR’s essential operations include array maps, filters, concatenation, dimension queries, amplitude norms, and element updates; compositional operations are defined from this set.The compositional set includes operations such as locateN, copyN, enumN, ampN, and upDim.Source: §6 · pp. 13–14

7 Translating Qafny Operations to HLIR

This section translates Qafny programs and specifications into IR code and Hoare assertions, giving validity arguments that connect derivable Qafny triples to valid Hoare triples. It covers measurement and classical control and establishes translation completeness and soundness, along with bounds on translation and proof-tree sizes.

7.1 Translating Oracle Operations

  • Oracle operations compile to locateN, mapN, and assignN, whose valid Hoare triples support the translation; the validity proof is mechanized in Rocq.mapN applies a function across array elements, while assignN updates amplitudes and selected basis-vector bits.Source: §7.1 · pp. 14–15

7.2 Translating Hadamard and QFT Operations

  • Hadamard and QFT operations add an array dimension using copyN, enumN, and ampN; their valid Hoare triples are proved, with mechanized proof in Rocq for Hadamard.QFT follows the Hadamard translation with phase multiplication; ampN can multiply amplitudes by functions of old and new basis vectors.Source: §7 · p. 14, §7.2 · pp. 16–17

7.3 Translating Quantum Conditionals

  • Quantum conditionals filter the array by the guard, translate the selected branch, then adjust dimensions and concatenate the results to form a valid Hoare triple.The proof uses that concatenating the guard and negated-guard partitions recovers the original array because quantum states are insensitive to ordering.Source: §7.3 · pp. 19–21

7.4 Translating Quantum Measurement

  • Measurement trims away the measured locus and assigns the nondeterministic measurement output and probability to variables; the array representation lets the rule select an index and sum squared amplitudes.The probability is the sum of squared amplitudes for entries whose basis vector matches the selected measurement result.Source: §7.4 · p. 22
  • Measurement binds outcome x and probability r; selecting an index once makes x classical in the continuation, so feed-forward becomes ordinary Hoare control without black-box probability distributions.Source: §7.4 · p. 22

7.5 Translating Classical Operations

  • Sequencing and for-loops translate compositionally to Hoare rules, with loop invariants parameterized by the index map and bounds as the locus grows.The translated invariant P(j) is an ordinary Hoare invariant whose preservation follows by translating the loop body from P(j) to P(j+1).Source: §7.5 · p. 23

7.6 Translation Completeness and Soundness

  • Every Qafny proof translates to a valid Hoare triple, so no Qafny-provable claim is lost; completeness and its component lemmas are mechanized in Rocq.Source: §7.6 · pp. 23–24
  • A valid translated Hoare triple implies a Qafny triple with semantically equivalent conditions, preventing a classical verifier from certifying a false quantum claim.Source: §7.6 · p. 24
  • At most eleven HLIR statements are generated per Qafny statement, while translated assertions and proof-tree skeletons have polynomial size.The size bounds use symbolic arrays, where a dimension of length 2^m is represented by one bound expression; they do not bound the time a classical verifier takes to discharge verification conditions.Source: §7.6 · pp. 24–25

8 Related Work

The paper distinguishes its proof-system translation from quantum systems built around quantum semantics and symbolic execution. Its contribution is a compilation to Hoare logic with guarantees in both directions, illustrated for Qafny and QHL.

8 Related Work

  • Other quantum proof systems use quantum semantics and states, such as superoperators or Dirac notation, as program-state syntax; this work instead translates a quantum proof system to classical Hoare logic.The related systems include Qafny, QBricks, and QHL [Feng and Ying 2021], among others.Source: §8 · p. 25
  • Translation completeness and soundness justify compiling quantum proof rules directly to Hoare logic, and the approach is illustrated for both Qafny and QHL.The paper also characterizes tensor-based separating conjunctions as pure.Source: §8 · p. 25
  • Unlike Qafnyc’s compilation of Qafny verification conditions into Dafny, which verifies 37 programs without proving the compilation correct, this work supplies the correctness foundation for trusting a Dafny verdict.The translation targets idealized Hoare logic with array theory, of which Dafny is one instance.Source: §8 · p. 25
  • Symbolic execution work decides properties of symbolic states, whereas this paper gives a meta-theoretic translation between proof systems with guarantees in both directions, with completeness mechanized in Rocq.The authors connect their approach to symbolic representation of superposition and identify pure separating conjunction, index mapping, and filter-and-renormalize measurement as supporting mechanisms.Source: §8 · p. 25

9 Conclusion, Future Work, and Limitations

The paper argues that Qafny verification can be translated completely and soundly into Hoare logic with array theory, with the completeness direction mechanized in Rocq. It identifies the translation’s scope and future extensions, and points to an appendix collecting proof-tree derivations.

9 Conclusion, Future Work, and Limitations

  • Qafny translates completely and soundly into Hoare logic with array theory, and the completeness direction is mechanized in Rocq.The embedding uses pure separation conjunctions, an n-dimensional array representation for EN(n) states, and array-aggregate primitives packaged as HLIR; generated verification conditions are polynomial in triple size and array dimension.Source: §9 · p. 26
  • The embedding makes quantum proof obligations deterministic and allows classical automated verifiers to discharge them without quantum-specific infrastructure.Future work includes richer quantum types, a concrete automated backend for end-to-end verification, and testing whether determinization generalizes to hybrid classical/quantum proof systems.Source: §9 · p. 26
  • The result is only that quantum verification is no harder than classical verification, not that every quantum program is easy to verify.The authors note that statistical quantum programs such as quantum machine learning can be hard to verify, as can classical AI and machine-learning programs.Source: §9 · p. 26

A Proof-Tree Derivations for the Translation Lemmas

  • The appendix collects Hoare-logic proof-tree derivations for the translation lemmas; the main text gives each lemma, translated triple, and reduction step.The right-hand column of each derivation names the Hoare rule applied at that step.Source: A Proof-Tree Derivations for the… · p. 29

A.1 Proof Tree for mapN

The mapN proof expands the array dimensions and constructs a Hoare proof tree using nested loops and loop invariants. The displayed derivation identifies the bounds maintained for the loop indices.

A.1 Proof Tree for mapN

  • The proof tree derives validity of the triple for A′ := mapN(A,m,f), continuing the proof of Lemma 7.2 via Lemma 2.1.The displayed sequence increments the innermost index and then the outer indices.Source: §A.1 · p. 29
  • The proof of mapN expands m into its component dimensions and derives a Hoare-logic proof tree using loop invariants at each level.The right-hand side indicates the Hoare rules to apply.Source: §A.1 · p. 29
  • The nested loops maintain an invariant bounding each index j_k within its corresponding dimension m_k.The displayed invariant includes j_0 in [0,m_0] through j_n-1 in [0,m_n-1].Source: §A.1 · p. 29

A.2 Proof Tree for assignN

The section derives a Hoare proof tree for assignN, using a program with assertions to establish the array update. The illustrated instance takes amplitudes from A1, while the general case substitutes a function of both arrays.

A.2 Proof Tree for assignN

  • The proof derives a Hoare logic tree by implementing assignN as a program with assertions.The displayed sequence includes incrementing the indices j0 through jn-1.Source: §A.2 · pp. 29–30
  • assignN updates A2 by inserting the selected bits from A1 at indices indφ(η), with the proof given in the Rocq mechanization.The illustrated proof uses f(u,v) = amp(v); the general case replaces that amplitude with f applied to the corresponding entries of A and A1.Source: §A.2 · pp. 29–30
  • The postcondition states that each processed entry of A2 equals the nested up_a and up_b update of A1.The quantified entries range over the prefixes ending at the current indices j0 through jn-1.Source: §A.2 · p. 30

A.3 Proof Tree for enumN

The section presents Hoare proofs for enumeration and amplitude multiplication, alongside a proof tree for the larger array transformation. The arguments use array-length conditions and loop assertions to establish the stated triples.

A.3 Proof Tree for enumN

  • The section continues the validity proof for the triple from Lemma 7.6 using Lemma 2.1.Source: §A.3 · p. 30
  • The larger proof tree applies locateN, mapN, and assignN to construct A2 from A1 and establish the stated up_b relation.The proof strengthens preconditions using Qlen axioms for arrays with the same bounds (m, 2|η|).Source: §A.3 · pp. 30–31
  • enum(n) generates an array whose entries A[k] equal k for all k in [0,n), with length n.The proof initializes A and uses j as a loop index, maintaining the property for the prefix [0,j).Source: §A.3 · p. 31
  • ampMult groups entries of A1 and A2 at indices B, then computes α′ as α times exp(2πi times their dot product).Its precondition bounds |B| by both array lengths and requires every B entry to be a valid index into each array.Source: §A.3 · p. 32

A.4 Proof Tree for Quantum Conditionals

The block presents proof trees for quantum conditionals and measurement, then gives a translation from CQHL through Qafny to classical Hoare logic. The translation handles classical commands directly and specifies mappings for quantum operations.

A.4 Proof Tree for Quantum Conditionals

  • The quantum-conditional proof uses filterN to split the array and upDim to align branch arrays before establishing the resulting concatenated state.The derivation invokes array-length axioms and the concat/filterN axiom; Qlen judgments are omitted in the measurement proof that follows.Source: §A.4 · pp. 32–33, §A.5 · p. 33

A.5 Proof Tree for Quantum Measurement

  • The measurement proof defines filtered entries and assigns x from the selected component of vector(A[i]) at indφ(η).It also defines an up_b update using the vector of the filtered entry and the index indφ(η′).Source: §A.5 · pp. 33–34

B Transformation for QHL

  • CQHL predicates combine classical conditions with quantum data predicates, and the paper translates CQHL to Qafny before applying the Qafny-to-Hoare translation.In CQHL, classical variables are bound by let-bindings, and quantum arrays denote groups of qubits.Source: B Transformation for QHL · pp. 34–35
  • Classical assignments, conditionals, calls, and sequencing map directly to Qafny, while quantum conditionals become two sequential Qafny conditionals.Oracle operations and Hadamard gates map to their Qafny counterparts; together they are universal, so other gates can be decomposed into them.Source: B Transformation for QHL · pp. 35–36
Loading 2610.34723v1…