{"id":"f2439af9-0dbf-4370-9956-d882d1e9ae35","arxiv_id":"2501.15238","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A sound and complete quantum relational Hoare logic (qOTL) for almost-surely terminating programs with bounded postconditions is obtained by adding a duality rule based on quantum optimal transport.","lead":"The paper introduces a relational Hoare logic for quantum programs and proves it sound and complete, using a quantum version of optimal transport duality. If correct, it gives a unified proof system for quantum program equivalence, privacy, and distance bounds.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Completeness rests on quantum Strassen with defects; SDP strong duality for the coupling polytope is asserted but not explicitly verified for singular marginals.","rationale":"The reader's weakest_assumption correctly identifies Theorem III.3 as the load-bearing step: the completeness theorem for bounded postconditions passes through the duality rule, which is justified by Theorem IV.4, which in turn relies on the quantum Strassen theorem with defects. Having reviewed the proof in Appendix B, I find the argument structurally sound: the reduction from Hermitian dual witnesses to PSD witnesses via shifts with nI is valid, and the use of the dual condition gives the correct bound. The main residual risk is the unverified assertion of SDP strong duality in a setting where the primal feasible set need not have an interior point. This is a standard concern in conic duality, but the existence of a dual Slater point (Y1=Y2=λI) makes it very likely that strong duality holds; the paper simply does not spell this out. I therefore do not see a demonstrated flaw, but I recommend a concrete numerical/analytical check to close the gap definitively. The reader's ACCEPT verdict with moderate confidence is appropriate; my concern does not change that verdict.","tokens_in":58965,"tokens_out":18370,"duration_ms":155734,"concrete_test":"Implement the primal and dual SDPs of Appendix B for small dimensions (d1=d2=2 and 3) with random PSD costs X and random partial density operators ρ1,ρ2 of equal trace, including singular (pure) marginals, and solve to verify zero duality gap and equality between primal and dual optima. For each instance, check the equivalence: (∃ coupling ρ with tr(Xρ) ≤ ε) iff (∀ PSD Y1,Y2 with X ⊒ Y1⊗I − I⊗Y2, tr(Y1ρ1) ≤ tr(Y2ρ2)+ε), for several ε values. If any instance violates the iff, Theorem III.3 is false; if all pass, the load-bearing step is confirmed.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The proof of Theorem VI.7 (completeness for bounded postconditions) reduces arbitrary judgments to split postconditions via the duality rule, whose soundness is Theorem IV.4, proved from Theorem III.3 (quantum Strassen with defects). The proof of Theorem III.3 in Appendix B sets up an SDP whose primal is max ⟨I-X,Z⟩ over couplings Z, with dual min ⟨B,Y⟩ over Hermitian Y satisfying Y1⊗I + I⊗Y2 ≥ I-X, and asserts strong duality. A gap would appear if the primal feasible set lacks an interior point: when ρ1 or ρ2 is singular, every coupling has support restricted to a subspace, so no full-rank feasible Z exists; strong duality then requires a Slater point on the dual side, which is plausible (e.g., Y1=Y2=λI for large λ) but not checked in the paper. Additionally, the step restricting dual witnesses to PSD operators relies on shifting arbitrary Hermitian Y by nI; while this shift is valid pointwise, the logic's duality rule quantifies the shift n over natural numbers, and one must confirm that no uniformity issue arises for the whole family Y in Theorem IV.4. If strong duality fails or the PSD restriction is lossy, Theorem IV.4 fails, the duality rule is unsound, and Theorem VI.7 collapses.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces qOTL, a quantitative relational Hoare logic for quantum while-programs, with assertions ranging over a new infinitary extension of PSD operators, judgments parameterized by logical variables, and validity based on partial quantum couplings. It proves soundness (Theorem VI.3) and two completeness results: completeness for split postconditions (Theorem VI.6) and completeness for bounded postconditions for almost surely terminating programs (Theorem VI.7), the latter obtained by reducing arbitrary bounded postconditions to universally quantified split postconditions through a duality rule. The duality rule is justified by a quantum Strassen theorem with defects (Theorem III.3) and a duality-under-data-processing theorem (Theorem IV.4). The paper also gives a complete semantic embedding of projective relational Hoare logic into qOTL using infinite-valued predicates, and derives characterizations of program equivalence, trace distance and diamond norm, quantum Wasserstein semi-distance, non-interference, and differential privacy. An extended appendix contains the main proofs, including SDP-based proofs of the duality theorems, and a probabilistic corollary establishing completeness of eRHL.","tokens_in":59197,"tokens_out":15047,"duration_ms":140464,"significance":"If the stated results hold, this is a substantial advance: it provides the first completeness theorem for a relational Hoare logic over quantum programs, and it does so by an elegant route that separates split-postcondition completeness from a Kantorovich-Rubinstein-style duality step. The introduction of infinite-valued PSD predicates is a useful unification of projective and quantitative assertions, and the embedding of pqRHL into qOTL (Proposition VII.2, Theorem VII.3) is a genuine contribution. The split-completeness proof (Lemmas VI.4 and VI.5, Theorem VI.6) is clean and detailed, and the applications in Section VIII are nontrivial. The main caveat is that the central Theorem III.3 depends on an asserted SDP strong-duality step that is not verified in the appendix; this is likely repairable, but it is currently a gap in the proof of the main completeness theorem. The paper is not machine-checked, but the appendix is unusually detailed and the proof structure is coherent.","major_comments":[{"comment":"The proof of direction (2 => 1) rests on the assertion that the coupling SDP 'can be shown to satisfy strong duality', but no proof, constraint qualification, or precise SDP duality theorem is supplied. This is load-bearing because the primal feasible set consists of couplings with fixed singular marginals and may lack a relative interior point; strong duality must then be established via a Slater point on the dual side. Such a point exists (e.g., Y1 = Y2 = λI for sufficiently large λ makes Φ†(Y) strictly greater than I - X), but this must be stated explicitly, together with the exact strong-duality theorem being invoked. Since Theorem IV.4, the duality rule, and hence Theorem VI.7 all depend on Theorem III.3, this missing verification is a substantive gap in the submitted proof, even though it appears readily fixable.","section":"Appendix B, proof of Theorem III.3"},{"comment":"The reduction from condition (1) to condition (2) in Theorem IV.4 is presented as a direct consequence of Theorem III.3, but the passage from arbitrary Hermitian witnesses to PSD witnesses via a shift by nI, and the restriction of n to natural numbers, is not explicitly verified. In finite dimension one can choose an integer n with Y2 ⊑ nI for any PSD Y2, and the shift argument in the proof of Theorem III.3 is pointwise, so no uniformity issue arises; however, the proof as written skips these steps. Because the side conditions of the duality rule in Figure 1 mirror exactly the set Y of Theorem IV.4, the completeness proof of Theorem VI.7 should spell out this correspondence.","section":"Theorem IV.4 and Appendix C, proof of Theorem C.7"}],"minor_comments":[{"comment":"The definition of X | A as A + ∞·X⊥ in Section II.C and the 'equivalently' formula in Definition A.6, namely ((X ∨ X_A⊥)P_A(X ∨ X_A⊥), X⊥ ∨ X_A), do not appear to coincide when A has a nontrivial infinite part and X does not commute with X_A. Please clarify the intended definition, since Lemma A.7 relies on these extended operations.","section":"Section II.C and Definition A.6"},{"comment":"The displayed line '⊢Z : {P} S1 ~ S2 {Q} ⇐⇒ ⊢Z,(Y1,Y2,n) ∈ Y : {P+nI} S1 ~ S2 {Y1⊗I + I⊗(nI−Y2)}' is not literally an equivalence of judgments; it describes the condition under which the duality rule applies. Replacing the biconditional with an implication or a stated 'it suffices to prove' would avoid confusion.","section":"Theorem VI.7, proof"},{"comment":"The statement contains a typo: 'tr(tr2(Y2))ρ2)' should read 'tr(tr2(Y2)ρ2)'. Please correct the parenthesis.","section":"Proposition IV.6"},{"comment":"In the proof of Theorem C.7, n is first treated as a real scalar in the shift argument and then as a natural number in the set Y. Since finite-dimensional operators have bounded spectra, the integer choice is always possible, but the proof should say this explicitly to avoid a perceived gap.","section":"Theorem C.7 / proof of Theorem IV.4"}],"recommendation":"major_revision","confidential_remarks":"The central completeness result is significant and the proof architecture is convincing overall. The missing SDP Slater verification in Theorem III.3 is the only real obstacle to recommending acceptance; it is likely patchable with a short argument. I also suggest the authors double-check Definition A.6 for X|A, as the two stated forms may be inconsistent when A has an infinite part."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Bottom line: this is the completeness result the field was missing. It builds a sound and complete relational Hoare logic for almost-surely terminating quantum programs with bounded postconditions, and it does so by a route that is clever but also checkable: split postconditions are handled by structural weakest preconditions, and arbitrary bounded postconditions are reduced to split ones by a duality rule derived from a quantum Strassen theorem with defects. The infinite-valued predicates and partial couplings are not just ornament; they are what allow projective preconditions and non-trace-preserving programs to fit in the same framework. The embeddings of projective-predicate logics and the characterizations of program equivalence, diamond norm, Wasserstein semi-distance, non-interference, and quantum differential privacy are useful dividends.\n\nThe proof is structurally coherent. The central load-bearing item is Theorem III.3, the defect version of Strassen's theorem, proved in Appendix B via SDP strong duality. The stress-test worry is that strong duality fails when the marginals are singular because the primal coupling polytope may lack an interior point. I think that worry does not land: the dual is strictly feasible by taking Y1=Y2=λI for large λ, so Slater holds on the dual side. The paper does not explicitly verify this, so it is worth a referee's attention, but it is a minor gap in presentation, not a flaw in the argument.\n\nThe soft spots are the usual ones for a paper of this density. The appendix is long and no part is machine-checked, so subtle bookkeeping errors are possible. The completeness proof for bounded postconditions goes through the duality rule with n quantified over naturals; since the underlying duality holds for reals, this is fine, but the mismatch is a little jarring. The two-sided rules are not needed for completeness and the presentation is brief; they are clearly marked as optional.\n\nWho this is for: researchers in quantum program logics, verification, and relational reasoning. It deserves a serious referee and will likely become a standard reference. Send it to review.","headline":"Completeness for coupling-based quantum relational Hoare logics is here; the SDP-duality worry is a presentation gap, not a flaw.","tokens_in":59708,"tokens_out":3020,"would_cite":true,"duration_ms":28468,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","68Q12","81P68"],"pacs":[],"model":"deepseek-v4-flash","headline":"Quantum relational Hoare logic is now sound and complete","keywords":["quantum relational Hoare logic","optimal transport duality","quantum couplings","Strassen theorem","almost-surely terminating programs","infinite-valued predicates","program equivalence","quantum differential privacy"],"falsifier":"Numerically solve the primal SDP for the quantum Strassen theorem—minimizing tr(Xρ) over couplings of two equal-trace states—and its dual for a two-qubit cost operator X such as the projector onto the singlet state with a small defect ε; a primal value strictly below the dual value would show strong duality fails and would invalidate the duality rule. A companion check is to test Theorem IV.4 on a pair of one-qubit AST programs where Q is a bounded non-split postcondition: if all the universal split judgments are derivable but the original judgment is not, completeness fails.","tokens_in":58755,"feed_emoji":"⚛️","tokens_out":7124,"duration_ms":64941,"temperature":0.7,"pith_summary":"This paper introduces qOTL, a relational Hoare logic for pairs of quantum while-programs, and proves that the logic is sound and complete for almost surely terminating programs with bounded quantitative postconditions. Validity is coupling-based: a judgment {P} S1 ~ S2 {Q} holds when the expected value of P on the input bounds the expected value of Q on some quantum coupling of the two outputs. The completeness proof sidesteps the hard problem of constructing couplings directly and instead uses a quantum version of optimal-transport duality to reduce any bounded postcondition to a split postcondition, for which ordinary compositional rules are already complete. A secondary contribution is an infinitary extension of positive semidefinite predicates that lets projective, subspace-based assertions be embedded completely into the quantitative logic. If correct, the paper turns relational verification of quantum programs from a search for witnesses into a proof-theoretic guarantee: every true bounded judgment has a derivation.","feed_headline":"Quantum relational Hoare logic is sound and complete","feed_subtitle":"A duality rule makes every valid judgment about terminating quantum programs provable, with applications to equivalence and privacy.","key_machinery":"The load-bearing mechanism is the quantum Strassen theorem with defects (Theorem III.3), a duality for quantum couplings proved by semidefinite programming. It characterizes the existence of a coupling with bounded cost through a universal dual inequality over positive semidefinite witnesses; the paper generalizes it from subspace liftings to arbitrary PSD costs and infinite-valued defects, and then to partial couplings so that non-trace-preserving programs are covered. On top of that sits the duality rule, which converts a judgment with an arbitrary bounded postcondition Q into universally quantified judgments with split postconditions Q1⊗I + I⊗Q2, and the one-sided weakest-precondition lemmas that prove split judgments by structural induction. Infinite-valued predicates in Pos∞ act as a separate mechanism: a predicate X|A = A + ∞·X⊥ enforces a projective precondition X inside the quantitative logic, which is what makes the complete embedding of projective assertions possible.","core_discovery":"On its own terms, the central claim is that a minimal set of Hoare rules—one-sided rules for initialization, unitaries, conditionals and loops, two-sided rules for skip and sequence, and a rule of consequence—becomes complete when augmented with a single duality rule. The duality rule is powered by a quantum Strassen theorem with defects: for equal-trace states, a coupling with tr(Xρ) ≤ ε exists exactly when every pair of positive semidefinite operators Y1, Y2 with X ⊒ Y1⊗I − I⊗Y2 satisfies tr(Y1ρ1) ≤ tr(Y2ρ2) + ε. Lifting this from states to quantum operations gives Theorem IV.4, which says that a pair of programs is monotone with respect to a cost Q if and only if it is monotone with respect to all split costs Y1⊗I + I⊗(nI − Y2) below Q. Hence any valid judgment with a bounded postcondition Q can be derived by proving universally quantified split-postcondition judgments, and those are handled by one-sided weakest preconditions. The result is Theorem VI.7: for almost surely terminating programs and bounded Q, validity implies derivability.","pith_inferences":["Because completeness is reduced to SDP duality, proof search could in principle be driven by solving the primal and dual semidefinite programs that define a postcondition's split witnesses; the paper does not develop such an algorithm.","The finiteness restriction on postconditions in the duality theorem suggests that completeness for genuinely infinite-valued postconditions would require a new duality allowing +∞ costs throughout; the current proof stops at bounded Q.","A separable-coupling analogue of the quantum Strassen duality is not known; if one existed, the same duality-rule architecture might yield completeness for separable-coupling relational logics, which the paper leaves open.","The probabilistic completeness result indicates the same optimal-transport duality pattern recurs classically, so one might expect a single cost-based relational logic generalizing both the quantum and probabilistic cases."],"forward_implications":["Any valid relational judgment about almost surely terminating quantum programs with a bounded PSD postcondition has a formal proof in qOTL, so relational verification is complete in principle.","The duality rule is the only structural rule needed; the standard one-sided rules for initialization, unitaries, conditionals and loops are already complete for split postconditions.","Infinite-valued predicates give a complete bridge between subspace-based projective predicates and quantitative PSD predicates, so the two styles of quantum Hoare logic can be used interchangeably.","Program equivalence, trace distance and diamond norm bounds, Wasserstein semi-distance, non-interference, and quantum differential privacy all receive complete characterizations as derivable judgments for AST programs.","By the same route, the probabilistic relational Hoare logic eRHL is complete for bounded postconditions and almost surely terminating programs."],"supporting_citations":[{"why":"Supplies the original SDP-based quantum Strassen theorem for subspace liftings that the paper generalizes to PSD costs and defects.","marker":"[7]"},{"why":"Provides the quantum optimal transport framework with cost operators and partial couplings that the paper's duality and monotonicity results build on.","marker":"[8]"},{"why":"Contributes the rqPD proof system and coupling-based validity that qOTL extends with logical variables, infinite-valued predicates, and the duality rule.","marker":"[2]"},{"why":"Introduces the projective quantum relational Hoare logic whose assertions the paper embeds completely via infinite-valued predicates.","marker":"[1]"},{"why":"Defines the probabilistic relational Hoare logic eRHL that the paper proves complete for bounded postconditions and AST programs.","marker":"[4]"},{"why":"Gives the syntax, denotational semantics, and AST notion of the qWhile language used for all program judgments.","marker":"[14]"},{"why":"Establishes the stabilized quantum optimal transport cost Ts and its identity with T(ρ⊗I/2, σ⊗I/2), used in the program-equivalence characterization.","marker":"[11]"},{"why":"Forms the classical Strassen theorem that the quantum lifting and duality results generalize.","marker":"[6]"},{"why":"Supplies Kantorovich duality used to derive the probabilistic completeness result for eRHL.","marker":"[56]"}],"fun_headline_variants":["Duality rule completes quantum relational Hoare logic","One duality rule: quantum Hoare logic becomes complete","Quantum Strassen duality yields complete Hoare logic","Full completeness for quantum Hoare logic via duality"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the semidefinite duality in the quantum Strassen theorem with defects is exact: existence of a coupling with cost at most ε is equivalent to the dual inequality over all positive-semidefinite witness pairs, with strong duality surviving arbitrary PSD costs and infinite-valued defects.","fun_headline_variants_meta":{"raw":{"variants":["Duality rule completes quantum relational Hoare logic","One duality rule: quantum Hoare logic becomes complete","Quantum Strassen duality yields complete Hoare logic","Full completeness for quantum Hoare logic via duality"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000183,"raw_usage":{"total_tokens":1262,"prompt_tokens":842,"completion_tokens":420,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":458,"completion_tokens_details":{"reasoning_tokens":360}},"tokens_in":458,"tokens_out":420,"duration_ms":4046,"temperature":1.0,"reasoning_tokens":360,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T14:29:20.013100+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Numerically solve the primal SDP for the quantum Strassen theorem—minimizing tr(Xρ) over couplings of two equal-trace states—and its dual for a two-qubit cost operator X such as the projector onto the singlet state with a small defect ε; a primal value strictly below the dual value would show strong duality fails and would invalidate the duality rule. A companion check is to test Theorem IV.4 on a pair of one-qubit AST programs where Q is a bounded non-split postcondition: if all the universal split judgments are derivable but the original judgment is not, completeness fails.","supporting_citations":[{"cited_title":"N OTATIONS AND PRELIMINARIES","cited_arxiv_id":null,"evidence_quote":"Supplies Kantorovich duality used to derive the probabilistic completeness result for eRHL."}],"review_version":1}