[Submitted on 11 Aug 2026]
Title:Lean Verification of Schrottenloher’s Optimized Elliptic-Curve Discrete-Logarithm Circuits: A Progress Report
Abstract: Schrottenloher proposed low-resource circuits for the elliptic-curve discrete logarithm problem (ECDLP) that combine a compressed binary Euclidean trace, reversed Bézout reconstruction, and approximate modular arithmetic. This report describes a Lean 4 formalization in VQ at artifact revision d090d5a. The checked development proves an exact 2n-round termination bound, reversible trace compression, complete basis-state semantics and cleanup for Algorithms 2–4, a secp256k1 instance, and syntax-derived logical resource bounds. Separate theorems specify success domains for Algorithms 6–7 and value correctness for Algorithms 9–11, while the Algorithm 1 work covers its affine value trace and first physical lookup–subtraction phase. The complete point-addition circuit, the probability of approximate-arithmetic failure, and the paper’s optimized resource totals remain unverified.
| Subjects: | Logic in Computer Science (cs.LO) |
| Cite as: | marXiv:2608.00035 [cs.LO] (or marXiv:2608.00035v1 [cs.LO] for this version) |
Submission history
[v1] Tue, 11 Aug 2026 17:09:11 UTC (338 KB)