From mboxrd@z Thu Jan 1 00:00:00 1970 Delivery-date: Wed, 15 Apr 2026 11:47:59 -0700 Received: from mail-oo1-f59.google.com ([209.85.161.59]) by mail.fairlystable.org with esmtps (TLS1.3) tls TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 (Exim 4.94.2) (envelope-from ) id 1wD5HL-0000uz-5U for bitcoindev@gnusha.org; Wed, 15 Apr 2026 11:47:59 -0700 Received: by mail-oo1-f59.google.com with SMTP id 006d021491bc7-6826de8e284sf1228734eaf.0 for ; Wed, 15 Apr 2026 11:47:58 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20251104; t=1776278873; x=1776883673; darn=gnusha.org; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:references:in-reply-to:message-id:to:from:date:sender:from :to:cc:subject:date:message-id:reply-to; bh=IR+kqLjcdjQ3Cnx/nM9TBDgnoEBdJXnIvv10Za2aX0s=; b=Pgjka+ywUu86cTiqEtN3vXt/iygaOh7t1v89oAxhxPwdd68+7Jsu6GJ1X6zSftxWIt lioTxieCd+qEasQ3plLVczq4YQ8lonZaySEL/ARx3VVyHLi+YrS2H1aj1DEacQiuMUkV /32beua+HibcW+g82YdR7/L7UuP+w1C6ypgulh7y+FoWtM7WV5tJ5RnamQQqOqQI5+4d TVYtsOB1sO08jJuKc2bv46iwPrBFHBNGuFIJPy+JJ1dJyXLzdlIMFVRuxlTL0KljLuPa UK1PFIykP0SW7sx2bX7r/DTlr4OpewZXEmWBk7+pTL2nyePK6vvsFiovyvEJBbXW20RF ooHw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20251104; t=1776278873; x=1776883673; darn=gnusha.org; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:references:in-reply-to:message-id:to:from:date:from:to:cc :subject:date:message-id:reply-to; bh=IR+kqLjcdjQ3Cnx/nM9TBDgnoEBdJXnIvv10Za2aX0s=; b=tKSvg3D3C19HEIWge+LcdbdqzMT3eWfskM0/uBkvOSQi+Lekj0BFDyJGa4BHahRPae V+RG2TlAh3DKtvZOU1vnGqNulq8QwaLcmg+w55xRfOswIizb2Onyglmn5fhFx1BQNvFt qUACHiTeIHB0jq4UGX2WEROiQdF7vLEo8/iWzmQDWGG/mHe0o+L2bUBGPfng03eAxlYj WxgSgWxlSd2WpFZcsW+lQzROdstXvQMQfNA7lKLwaNLEDm3wqkgsb7m2Is15hF9mh2na e9v43hQXWxcCcCL+yo/SpG2rnNBqkiUJIrDxn3kYaoknAgzggenmsWj+37EBwLJPAr1q OA9g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1776278873; x=1776883673; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:references:in-reply-to:message-id:to:from:date:x-beenthere :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=IR+kqLjcdjQ3Cnx/nM9TBDgnoEBdJXnIvv10Za2aX0s=; b=IDIP1yYjbTSvAwPM4HGETpWlGULyc3Ux8dmyNJHzQ4VuIaO3vCHyuW07jymU1whjy1 z4ZwysTjRNgKEHgk4KFwV0WpJ89yS3KIlF2knwWjuIRfU4ewlpVdnvoVKo5KvLc9yv30 SG5E/OqrzwAK+FkcL3/roJHW6EHJ5EdqcCNcl3HDRssH3oFEBiaeDJiyLkvb6RPKdyUa 9u8+3tKuQ20wDyahJP3EtqF9fS5TCF6iy9mV+xcqvJ+6EswVQjq1iAHn1lEBOb2lYzGv mYQqo0ay3N+RqEMcMfmT3brzY8pgtmblyrlRiZYsNdLxWxHjuziPMoomzlivDahpb9Bo Cp7Q== Sender: bitcoindev@googlegroups.com X-Forwarded-Encrypted: i=1; AFNElJ9HOvNPZ9g7b2Rl8uqKxeNmO4u+1AH7nDb+VnFaWATCwU3NfOgYPTTROXJaWXvpxs4IF14XSh2zXV2I@gnusha.org X-Gm-Message-State: AOJu0YxHVb1vcudVOhO7RI5jTBKLZz+HnDFrLFM4doHgFZ3D3ZZo7w8a vPLKEfkAfvCIyzT8Wbt6hiL3kP8BxT+bkJ+/SogTUuGxFGnGeKcfcB/X X-Received: by 2002:a05:6820:1b15:b0:67c:2b8f:48ec with SMTP id 006d021491bc7-693293e3476mr1191495eaf.1.1776278872960; Wed, 15 Apr 2026 11:47:52 -0700 (PDT) X-BeenThere: bitcoindev@googlegroups.com; h="AYAyTiIMFKhOlYkAIRIp6Pn3/yQcoKrKbSgA7W5b4yTDu6VDTQ==" Received: by 2002:a05:6820:f033:b0:691:e93c:b93b with SMTP id 006d021491bc7-6943c8d8408ls65040eaf.2.-pod-prod-09-us; Wed, 15 Apr 2026 11:47:47 -0700 (PDT) X-Received: by 2002:a05:6808:2213:b0:46a:ccae:5517 with SMTP id 5614622812f47-4789f9ff61amr13721254b6e.28.1776278867865; Wed, 15 Apr 2026 11:47:47 -0700 (PDT) Received: by 2002:a05:690c:628a:b0:7b3:443:26a9 with SMTP id 00721157ae682-7b7135fd0d9ms7b3; Wed, 15 Apr 2026 11:39:43 -0700 (PDT) X-Received: by 2002:a05:690c:110:b0:79a:6249:a046 with SMTP id 00721157ae682-7af6f03b5femr228636687b3.9.1776278382241; Wed, 15 Apr 2026 11:39:42 -0700 (PDT) Date: Wed, 15 Apr 2026 11:39:41 -0700 (PDT) From: jeremy To: Bitcoin Development Mailing List Message-Id: <531d1095-435c-4e8f-b8d1-8fdc26aeab2cn@googlegroups.com> In-Reply-To: <09b8adf7-0faa-4efa-b53a-7d29a5f40c12@mailbox.org> References: <09b8adf7-0faa-4efa-b53a-7d29a5f40c12@mailbox.org> Subject: [bitcoindev] Re: Formal verification of secp256k1 modular scalar multiplication MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_112364_1453506790.1776278381825" X-Original-Sender: Jeremy.L.Rubin@gmail.com Precedence: list Mailing-list: list bitcoindev@googlegroups.com; contact bitcoindev+owners@googlegroups.com List-ID: X-Google-Group-Id: 786775582512 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , X-Spam-Score: -0.5 (/) ------=_Part_112364_1453506790.1776278381825 Content-Type: multipart/alternative; boundary="----=_Part_112365_1157841501.1776278381825" ------=_Part_112365_1157841501.1776278381825 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable This is really neat! For my purify impl[0], I've also had some success with using CBMC on a toy= =20 curve prime to "prove" correctness, but an actually Rocq proof is obviously= =20 better. [0] https://judica.org/purify On Tuesday, April 7, 2026 at 8:13:01=E2=80=AFAM UTC-4 remix7531 wrote: > 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 =3D 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]=20 > > https://opensats.org/blog/sixteenth-wave-of-bitcoin-grants#advancing-form= al-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/ > > --=20 You received this message because you are subscribed to the Google Groups "= Bitcoin Development Mailing List" group. To unsubscribe from this group and stop receiving emails from it, send an e= mail to bitcoindev+unsubscribe@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/bitcoindev/= 531d1095-435c-4e8f-b8d1-8fdc26aeab2cn%40googlegroups.com. ------=_Part_112365_1157841501.1776278381825 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable This is really neat!

For my purify impl[0], I've also = had some success with using CBMC on a toy curve prime to "prove" correctnes= s, but an actually Rocq proof is obviously better.


[0] https://judica.org/purify

On Tue= sday, April 7, 2026 at 8:13:01=E2=80=AFAM UTC-4 remix7531 wrote:
=
Hi all,

I have been lurking on this list for years. It is time for my first pos= t.

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 =3D a * b mod N correctly for all representable inputs, where N is th= e
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]=20
https://opensat= s.org/blog/sixteenth-wave-of-bitcoin-grants#advancing-formal-verification-f= or-bitcoin-cryptography
[1] https://remix7531.com/post/fo= rmal_verification_secp256k1_scalar_mul/
[2] https://github.com/remix7531/secp256k1-scalar-fv-test
[3] https://vst.cs.princeton.edu/

--
You received this message because you are subscribed to the Google Groups &= quot;Bitcoin Development Mailing List" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to bitcoind= ev+unsubscribe@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/bitcoind= ev/531d1095-435c-4e8f-b8d1-8fdc26aeab2cn%40googlegroups.com.
------=_Part_112365_1157841501.1776278381825-- ------=_Part_112364_1453506790.1776278381825--