{"id":"arxiv/2605.01008","url":"https://arxiv.org/abs/2605.01008","tags":["cs.SE","cs.CR","quant-ph"],"score":0,"title":"Semantics-Based Verification of an Implemented Shor Oracle for ECDLP in Qrisp","domain":"cs.SE","source":"arxiv","authors":["Lei Zhang","Zhiyuan Chen"],"reviews":0,"subject":"cs.SE","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-05-01","reactions":{}}