pith. sign in

arxiv: 2605.01008 · v1 · submitted 2026-05-01 · 💻 cs.SE · cs.CR· quant-ph

Semantics-Based Verification of an Implemented Shor Oracle for ECDLP in Qrisp

Lei Zhang , Zhiyuan Chen This is my paper

Pith reviewed 2026-05-09 19:03 UTC · model grok-4.3

classification 💻 cs.SE cs.CRquant-ph
keywords Shor's algorithmECDLPsemantic verificationquantum oraclequantum softwareverification obligationscontrolled execution
0
0 comments X

The pith

An implemented Shor oracle for ECDLP in Qrisp matches classical references on point updates but can violate control semantics under controlled execution.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper argues that Shor-style algorithms for the elliptic-curve discrete logarithm problem depend critically on the precise semantics of their oracles, where small implementation details can break the intended mathematical model. It proposes a semantics-first verification method for a complete, compilable ECDLP oracle built in the Qrisp quantum programming language by specifying the oracle in terms of program semantics and deriving refinement-style verification conditions for its main parts. The approach includes a complexity argument for the oracle family. A case study demonstrates that while the central point-update operation matches a classical reference on proper inputs, controlled execution can fail to obey the required control law even after a simple control check passes. This finding indicates that semantic auditing must precede any claim of correctness for quantum software targeting ECDLP.

Core claim

The implemented Shor oracle for ECDLP in Qrisp has its core point-update primitive agreeing with a classical reference on well-formed inputs. However, controlled execution of the oracle may violate the expected control law under the evaluated toolchain, even though a trivial control sanity check passes. The paper specifies the oracle at the program semantics level, derives refinement-style verification obligations for key components, and gives a high-level complexity argument for the oracle family.

What carries the argument

The semantics specification of the oracle at the program level together with refinement-style verification obligations derived for its components, particularly the point-update primitive.

If this is right

  • The core point-update primitive agrees with a classical reference on well-formed inputs.
  • Controlled execution may violate the expected control law despite passing a trivial control sanity check.
  • A high-level complexity argument holds for the resulting oracle family.
  • Semantic auditing is a practical prerequisite for trustworthy ECDLP-oriented quantum software.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar semantic violations could affect other quantum implementations of Shor's algorithm beyond this specific Qrisp ECDLP oracle.
  • Toolchains for quantum programming may require more rigorous semantic models to prevent such discrepancies from going undetected.
  • Applying the same verification approach to larger instances or full algorithm runs could uncover additional subtle errors.

Load-bearing premise

The program semantics used in the specification accurately represent the intended mathematical oracle model, and the observed behavior in the Qrisp toolchain corresponds to true execution semantics rather than an artifact of the compiler or simulator.

What would settle it

Running the controlled point-update primitive on a specific well-formed input and checking whether the output state satisfies the mathematical control law would directly test whether the reported violation occurs or if the implementation behaves as expected.

Figures

Figures reproduced from arXiv: 2605.01008 by Lei Zhang, Zhiyuan Chen.

Figure 1
Figure 1. Figure 1: Oracle composition in the implementation. The accumulator R is updated by two scalar-multiplication-and-add routines, controlled bitwise by x1 and x2, yielding R ⊕ x1G ⊕ x2P. Here ⊕ denotes the elliptic-curve group operation under the imple￾mentation’s point encoding, not bitwise XOR. where ⊕ denotes the elliptic-curve group operation as realized by the implemen￾tation’s point encoding. Substituting P = ℓG… view at source ↗
read the original abstract

Shor-style quantum algorithms for the elliptic-curve discrete logarithm problem (ECDLP) are highly sensitive to the exact semantics of their group-operation oracles. Consequently, minor implementation choices can invalidate the intended mathematical model and lead to misleading conclusions. This paper introduces a semantics-first verification perspective for an end-to-end, compilable ECDLP implementation built on Qrisp. We specify the implemented oracle at the level of program semantics, derive refinement-style verification obligations for its key components, and provide a high-level complexity argument for the resulting oracle family. A small case study highlights that (i) the core point-update primitive agrees with a classical reference on well-formed inputs, yet (ii) controlled execution may violate the expected control law under the evaluated toolchain, despite a passing trivial control sanity check. These results position semantic auditing as a practical prerequisite for trustworthy ECDLP-oriented quantum software.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces a semantics-first verification approach for an end-to-end, compilable Shor oracle implementation targeting the elliptic-curve discrete logarithm problem (ECDLP) in the Qrisp quantum framework. It specifies the oracle at the level of program semantics, derives refinement-style verification obligations for key components (including the point-update primitive), provides a high-level complexity argument for the resulting oracle family, and reports a case study in which the core point-update primitive matches a classical reference on well-formed inputs while controlled execution appears to violate the expected control law under the evaluated toolchain (despite a passing trivial control sanity check).

Significance. If the case-study findings are substantiated by explicit semantic specifications, machine-checked obligations, and independent confirmation that the observed discrepancy is not a toolchain artifact, the work would be significant for quantum software engineering. It demonstrates that minor implementation choices in group-operation oracles can invalidate the intended mathematical model for Shor-style ECDLP algorithms and positions semantic auditing as a practical prerequisite for trustworthy quantum implementations in this domain.

major comments (2)
  1. [Case study] Case study section: the central claim that controlled execution violates the expected control law (while the point-update primitive agrees with the classical reference) is load-bearing for the paper's argument that semantic auditing is necessary. However, the manuscript provides no explicit formal statement of the control-law predicate used in the refinement obligations, nor any machine-checked proof or cross-backend simulation (e.g., independent simulator or different lowering of the control qubit) to establish that the violation survives a change of backend rather than arising from a Qrisp compiler artifact in state representation or control handling.
  2. [Semantics specification and refinement obligations] Refinement obligations and semantics specification: the derivation of verification obligations for the oracle components rests on the assumption that the specified program semantics faithfully capture the intended ECDLP group oracle model. The paper should include the concrete semantic definitions (e.g., for the point-update operation and control law) and show how they relate to the mathematical oracle, so that readers can assess whether any discrepancy is semantic or merely an encoding artifact.
minor comments (2)
  1. [Complexity argument] The high-level complexity argument would benefit from explicit asymptotic bounds or a reference to a standard analysis of Shor oracles to make the practicality claim more precise.
  2. [Case study] Clarify the exact version of the Qrisp toolchain and simulator backend used in the case study, as this affects reproducibility of the observed control-law violation.

Simulated Author's Rebuttal

2 responses · 1 unresolved

We thank the referee for their insightful comments on our manuscript. These comments help clarify the presentation of our semantics-first verification approach for the Qrisp Shor oracle. We provide point-by-point responses to the major comments and indicate the revisions we will make.

read point-by-point responses

  1. Referee: [Case study] Case study section: the central claim that controlled execution violates the expected control law (while the point-update primitive agrees with the classical reference) is load-bearing for the paper's argument that semantic auditing is necessary. However, the manuscript provides no explicit formal statement of the control-law predicate used in the refinement obligations, nor any machine-checked proof or cross-backend simulation (e.g., independent simulator or different lowering of the control qubit) to establish that the violation survives a change of backend rather than arising from a Qrisp compiler artifact in state representation or control handling.

    Authors: We acknowledge that the control-law predicate should be stated more explicitly to support the case study findings. In the revised manuscript, we will add the formal definition of the control law as used in our refinement obligations. The case study is primarily empirical, comparing the implemented primitive against a classical reference for agreement on well-formed inputs and observing the control behavior. We do not claim a machine-checked proof of the violation in the current work; instead, we use it to illustrate the value of semantic auditing. Regarding cross-backend validation, we have not conducted simulations on alternative backends or simulators. We will add a discussion noting this as a limitation and explaining why the observed behavior is consistent with the Qrisp semantics rather than an artifact. This constitutes a partial revision. revision: partial

  2. Referee: [Semantics specification and refinement obligations] Refinement obligations and semantics specification: the derivation of verification obligations for the oracle components rests on the assumption that the specified program semantics faithfully capture the intended ECDLP group oracle model. The paper should include the concrete semantic definitions (e.g., for the point-update operation and control law) and show how they relate to the mathematical oracle, so that readers can assess whether any discrepancy is semantic or merely an encoding artifact.

    Authors: We agree that providing the concrete semantic definitions will improve the manuscript's clarity and allow better assessment of the results. We will include explicit definitions for the point-update operation and the control law in the revised version, along with their correspondence to the mathematical model of the ECDLP group oracle. This will address the concern about semantic versus encoding artifacts. revision: yes

standing simulated objections not resolved
  • Machine-checked proofs or cross-backend simulations to confirm that the control-law violation is not due to a Qrisp compiler artifact.

Circularity Check

0 steps flagged

No circularity in the derivation chain

full rationale

The abstract describes a semantics-first approach that specifies the oracle at the program-semantics level, derives refinement obligations, and offers a high-level complexity argument, followed by a case study comparing the point-update primitive to an external classical reference. No equations, self-referential definitions, fitted parameters renamed as predictions, or load-bearing self-citations are present in the provided text. The verification obligations and complexity argument are presented as derived from the specified semantics rather than presupposing the target result, and the case-study discrepancy is framed as an empirical observation against an independent reference. The derivation therefore remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review supplies no explicit free parameters, axioms, or invented entities; the central claim rests on unstated assumptions about oracle semantics and toolchain fidelity.

pith-pipeline@v0.9.0 · 5449 in / 1095 out tokens · 37281 ms · 2026-05-09T19:03:11.741607+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

17 extracted references · 17 canonical work pages

  1. [1]

    In: 2025 IEEE International Conference on Quantum Computing and Engineering (QCE)

    Ahmed, N., Zhang, L., Gangopadhyay, A.: A survey of post-quantum cryptogra- phy support in cryptographic libraries. In: 2025 IEEE International Conference on Quantum Computing and Engineering (QCE). vol. 1, pp. 906–917. IEEE (2025)

    work page 2025

  2. [2]

    In: 2022 14th International Conference on Computational Intelligence and Communication Networks (CICN)

    Albuainain, A., Alansari, J., Alrashidi, S., Alqahtani, W., Alshaya, J., Nagy, N.: Experimental implementation of Shor’s quantum algorithm to break RSA. In: 2022 14th International Conference on Computational Intelligence and Communication Networks (CICN). pp. 748–752. IEEE (2022)

    work page 2022

  3. [3]

    In: 2020 IEEE 5th international conference on computing communication and automation (ICCCA)

    Bhatia, V., Ramkumar, K.: An efficient quantum computing technique for crack- ing RSA using Shor’s algorithm. In: 2020 IEEE 5th international conference on computing communication and automation (ICCCA). pp. 89–94. IEEE (2020)

    work page 2020

  4. [4]

    In: International Conference on Informa- tion Security Applications

    Larasati, H.T., Kim, H.: Quantum cryptanalysis landscape of Shor’s algorithm for elliptic curve discrete logarithm problem. In: International Conference on Informa- tion Security Applications. pp. 91–104. Springer (2021)

    work page 2021

  5. [5]

    ACM Transactions on Quantum Computing5(1), 1–35 (2023)

    Lewis, M., Soudjani, S., Zuliani, P.: Formal verification of quantum programs: Theory, tools, and challenges. ACM Transactions on Quantum Computing5(1), 1–35 (2023)

    work page 2023

  6. [6]

    On the feasibility of quantum unit testing,

    Miranskyy, A., Campos, J., Mjeda, A., Zhang, L., de Guzmán, I.G.R.: On the feasibility of quantum unit testing. arXiv preprint arXiv:2507.17235 (2025)

    work page arXiv 2025

  7. [7]

    In: 2019 IEEE/ACM 41st International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER)

    Miranskyy, A., Zhang, L.: On testing quantum programs. In: 2019 IEEE/ACM 41st International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER). pp. 57–60. IEEE (2019)

    work page 2019

  8. [8]

    On testing and debugging quantum software,

    Miranskyy, A., Zhang, L., Doliskani, J.: On testing and debugging quantum soft- ware. arXiv preprint arXiv:2103.09172 (2021)

    work page arXiv 2021

  9. [9]

    Proceedings of the National Academy of Sciences120(21), e2218775120 (2023)

    Peng, Y., Hietala, K., Tao, R., Li, L., Rand, R., Hicks, M., Wu, X.: A formally certified end-to-end implementation of Shor’s factorization algorithm. Proceedings of the National Academy of Sciences120(21), e2218775120 (2023)

    work page 2023

  10. [10]

    arXiv preprint arXiv:2501.10228 (2025)

    Polimeni, D., Seidel, R.: End-to-end compilable implementation of quantum elliptic curve logarithm in Qrisp. arXiv preprint arXiv:2501.10228 (2025)

    work page arXiv 2025

  11. [11]

    pQCee Ltd: (2026), https://www.pqcee.com

    work page 2026

  12. [12]

    doi:10.48550/arxiv.2406.14792 , author =

    Seidel, R., Bock, S., Zander, R., Petrič, M., Steinmann, N., Tcholtchev, N., Hauswirth, M.: Qrisp: A framework for compilable high-level programming of gate- based quantum computers. arXiv preprint arXiv:2406.14792 (2024)

    work page arXiv 2024

  13. [13]

    Physical review letters86(9), 1889 (2001)

    Weinstein, Y.S., Pravia, M., Fortunato, E., Lloyd, S., Cory, D.G.: Implementation of the quantum Fourier transform. Physical review letters86(9), 1889 (2001)

    work page 2001

  14. [14]

    In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

    Yu, N., Palsberg, J.: Quantum abstract interpretation. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. pp. 542–558 (2021)

    work page 2021

  15. [15]

    https://doi.org/10.5281/zenodo.18865658

    Zhang, L.: Semantics-based verification pilot for ECDLP Shor oracle in Qrisp (2026). https://doi.org/10.5281/zenodo.18865658

    work page doi:10.5281/zenodo.18865658 2026

  16. [16]

    IEEE Software38(2), 80–87 (2020)

    Zhang, L., Miranskyy, A., Rjaibi, W.: Quantum advantage and the Y2K bug: A comparison. IEEE Software38(2), 80–87 (2020)

    work page 2020

  17. [17]

    Information and Software Technology161, 107249 (2023)

    Zhang, L., Miranskyy, A., Rjaibi, W., Stager, G., Gray, M., Peck, J.: Making exist- ing software quantum safe: A case study on IBM Db2. Information and Software Technology161, 107249 (2023)

    work page 2023