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

TL;DR

This paper presents a semantics-first verification approach for a quantum implementation of Shor's algorithm targeting ECDLP, emphasizing the importance of semantic correctness for trustworthy quantum software.

Contribution

It introduces a semantics-based verification framework for quantum oracles in ECDLP, highlighting potential implementation pitfalls and the need for semantic auditing.

Findings

Core point-update primitive matches classical reference on well-formed inputs

Controlled execution can violate expected control law despite passing sanity checks

Semantic auditing is crucial for trustworthy quantum ECDLP software

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.