Formal verification of secp256k1 modular scalar multiplication

[remix7531]

Hi all,

I have been lurking on this list for years. It is time for my first post.

This is my first result under my OpenSats grant [0]. Full writeup
with technical details and Rocq (formerly Coq) code examples is on
my blog [1].

Code and proofs are available on GitHub [2].

I produced a machine-checked proof that secp256k1_scalar_mul computes
r = a * b mod N correctly for all representable inputs, where N is the
secp256k1 group order. The proof covers arithmetic correctness, absence
of integer overflow in all intermediate computations, and memory safety.
Scalar multiplication sits on the critical path of every signature
operation.

Together with all supporting helpers, the verified code totals roughly
300 lines of C. The proof code totals ~6,400 lines in Rocq, giving a
proof-to-code ratio of roughly 21:1.

I verified the non-assembly, 64-bit only fallback path using the
Verified Software Toolchain (VST) [3]. The verified code differs
from upstream in two ways: assert statements are removed
(not present in production builds) and macros are converted to
inline functions. The algorithmic logic is unchanged. When compiled
with CompCert, the correctness guarantee extends from the
mathematical specification to assembly.

One mistake I made was a missing "mod 2^256" in a helper
specification, which made it unprovable. The code was correct,
the error was in my specification. The proof assistant caught it
because the proof cannot go through when the specification does
not match the code's behavior.

Next targets are porting to RefinedC for a framework comparison,
verifying Pippenger's algorithm for batch signature verification
(axiomatizing group operations), and evaluating Cryptol/SAW.

Feedback welcome.

remix7531

[0]
https://opensats.org/blog/sixteenth-wave-of-bitcoin-grants#advancing-formal-verification-for-bitcoin-cryptography
[1] https://remix7531.com/post/formal_verification_secp256k1_scalar_mul/
[2] https://github.com/remix7531/secp256k1-scalar-fv-test
[3] https://vst.cs.princeton.edu/