Qrisp中ECDLP Shor Oracle的语义化验证
软件工程
2026-05-05 v1 密码学与安全
量子物理
摘要
基于椭圆曲线离散对数问题（ECDLP）的Shor式量子算法对其群运算oracle的确切语义极为敏感。因此，微小的实现选择可能使原本的数学模型失效，导致误导性的结论。本文提出一种语义化验证视角，用于基于Qrisp构建的端到端、可编译ECDLP实现。我们以程序语义水平指定所实现的oracle，推导出其关键组件的细化式验证义务，并提供该oracle族的高层次复杂性论证。一个小型案例研究表明：（i）核心点更新原语在规范输入上的行为与经典参考一致，然而（ii）受控执行可能在所评估的工具链下违反预期的控制法则，尽管通过了平凡的控制自洽性检查。这些结果将语义审计定位为可信赖的ECDLP导向量子软件的实践前提。
引用
@article{arxiv.2605.01008,
title = {Semantics-Based Verification of an Implemented Shor Oracle for ECDLP in Qrisp},
author = {Lei Zhang and Zhiyuan Chen},
journal= {arXiv preprint arXiv:2605.01008},
year = {2026}
}
备注
7 pages, 1 figure, and 1 table; accepted by The 20th International Symposium on Theoretical Aspects of Software Engineering (TASE 2026)