[Submitted on 4 Sep 2026 (v1), revised 4 Sep 2026 (this version, v2), latest revision 4 Sep 2026 (v4)]
Title:Windowed Euclidean Arithmetic in an 833-Qubit secp256k1 ECDLP Program
Abstract: We verify a secp256k1 elliptic-curve discrete-logarithm program with a fixed allocation of 833 logical qubits and exactly 588,551,462,912 Toffoli-class operations per execution. The program shares a temporary qubit between field-arithmetic and point-comparison stages. Round-indexed bounds on Euclidean coefficients shorten reversible endpoint searches, saving 192,739,491,840 Toffoli-class operations per complete execution. Lean 4 checks the generated arithmetic, workspace restoration, complete point translation, both semiclassical scalar loops, and the analytic recovery distribution. For every valid nonzero secp256k1 public key, 26 independent executions recover the private scalar with probability greater than 99 percent. The exact pathwise gate count also equals its expectation under the program’s semantic branch probabilities. The allocated width gives a peak-live upper bound.
| Subjects: | Logic in Computer Science (cs.LO); Computational Complexity (cs.CC) |
| Cite as: | marXiv:2609.00002 [cs.LO] (or marXiv:2609.00002v2 [cs.LO] for this version) |
Submission history
[v1] Fri, 4 Sep 2026 20:05:06 UTC (261 KB)
[v2] Fri, 4 Sep 2026 20:09:34 UTC (263 KB)
[v3] Fri, 4 Sep 2026 20:12:24 UTC (263 KB)
[v4] Fri, 4 Sep 2026 21:30:02 UTC (303 KB)
Named by
- marXiv:2609.00003
- Extends the 833-qubit construction with shared endpoint comparisons, scalar windows, initial lookup, and analytic one-run recovery.