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.

翻译：针对椭圆曲线离散对数问题（ECDLP）的 Shor 型量子算法，其群运算预言机的具体语义高度敏感。因此，微小的实现选择可能导致预期数学模型失效，并得出误导性结论。本文针对基于 Qrisp 构建的端到端可编译 ECDLP 实现，提出一种语义优先的验证视角。我们以程序语义级别对已实现预言机进行规约，为其关键组件推导精化风格验证义务，并给出结果预言机族的高层次复杂度论证。一个小型案例研究表明：（i）核心的点更新原语在格式良好的输入上与经典参考实现一致，然而（ii）在所评估的工具链下，经过控制执行时可能违反预期的控制律，尽管其已通过简单的控制正确性检查。这些结果将语义审计定位为构建可信赖的面向 ECDLP 的量子软件的实用先决条件。