From mboxrd@z Thu Jan 1 00:00:00 1970 Delivery-date: Tue, 07 Apr 2026 05:13:08 -0700 Received: from mail-oi1-f188.google.com ([209.85.167.188]) by mail.fairlystable.org with esmtps (TLS1.3) tls TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 (Exim 4.94.2) (envelope-from ) id 1wA5Ip-00069z-UC for bitcoindev@gnusha.org; Tue, 07 Apr 2026 05:13:08 -0700 Received: by mail-oi1-f188.google.com with SMTP id 5614622812f47-467dc3431cbsf3844715b6e.0 for ; Tue, 07 Apr 2026 05:13:07 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1775563982; cv=pass; d=google.com; s=arc-20240605; b=HUGNpHhopuC7Rg8u6uR3xzuxo/mckfVdP1EJwRIqd560NwOC3i4dXypjTF+mx47/rL /v0WQcXjHCwLSa5IhTDnHo27IjztZf+aLpjF34DNdwJBUf8063h727PtRz3GfNjYYmzL dch+6L+RxTqw666tm6GqbqioLJgucv5WpUjy5B5o/cgGDslDGt5AFg7peHovC7hsVd35 KYE//4SDS3zFWq8XJwk9k6KJE/dLNY7YTxM7oW7vKs6jorFy9bjHNW4GEsQLT1+m/Wd6 HDLJ5Qe6lKiVcS1tznrEOoEmXugkJa68m6vVDpGRPmMwqzRE8p9phK66+Akbnxjp6bo+ pHgg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20240605; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:reply-to:content-language:to :subject:from:mime-version:date:message-id:dkim-signature; bh=9QL7E7axSshy4zSLdEGQJ+Y/UOI+BRSIC2kxQ3F7v/g=; fh=0HCotRiTxkV4/YywYpGsD6OhpbUnsd6r66NcmvfouS0=; b=Kth4sSAjIc/4p10SGcUaCFR/mtaCuVO0bwEiAuZIF4WNbSUeEy0C7Jg9KY+3SMOz/j Ic9KBpylyRfEna7zJUJC/jjSLm2scCw5t2YGInrYVSfMCG4+b0K8vWE2+N/jJkRaSfcw 2qlbDTVSnBa5Zh/0aCvKps+nH5DRGRA3Ay4j1fcWmZv5xxEb3WRmsUXsKeEpaQYsiFHH g5O10gMTrxi9VwcbpSMhSVaUFRR72DTZCxbqbuOCm6/Zt+9BZcSOVoXrLmF4mEOPBMLi g5pGuqqO1FsgYgEHdaHOSgoAJL/K5AqYWRWWOHa+tOKPkc3vuDxKibAqRiqh+i/yusk3 BGuw==; darn=gnusha.org ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@mailbox.org header.s=mail20150812 header.b=kkSzODnT; spf=pass (google.com: domain of remix7531@mailbox.org designates 2001:67c:2050:0:465::202 as permitted sender) smtp.mailfrom=remix7531@mailbox.org; dmarc=pass (p=REJECT sp=REJECT dis=NONE) header.from=mailbox.org DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20251104; t=1775563982; x=1776168782; darn=gnusha.org; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:reply-to :x-original-authentication-results:x-original-sender :content-language:to:subject:from:mime-version:date:message-id:from :to:cc:subject:date:message-id:reply-to; bh=9QL7E7axSshy4zSLdEGQJ+Y/UOI+BRSIC2kxQ3F7v/g=; b=epPkVH+m3xdg1sDwNATMfrCgKxXoF5cnz1sB374O/n/R/1mA3NKmbcfsABBPrbeMGh Zoh/9QSoLw62NF3tvzae5cBx/3PZZh8kqYsVlkLGCd7963KrdL3aeFCQOJReluz3BvF9 vTUltNtsIb1gfMPSVMfclcC/kF0aU4YW1T4/wNuMwnVJrNyAU34+pki3f7NFWTBE4nAQ sJ/LL45+YE/aUPwK0i0QhMkhUU6baVqT/RrnE9I/EYu6/qL2d3KSIBCc0Ap/KUvQkg9W vlb/3vPtrBewRZaHEzr9OkDR3SZucYri+w9xrHy2avvn52///4eNyt8V7+5+q35qzbEF rAgA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1775563982; x=1776168782; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:reply-to :x-original-authentication-results:x-original-sender :content-language:to:subject:from:mime-version:date:message-id :x-beenthere:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=9QL7E7axSshy4zSLdEGQJ+Y/UOI+BRSIC2kxQ3F7v/g=; b=pg8xiy/Z4XO3UOVLDNQuWUJi9oXTsnmk7/Mx80xcFIfCJdtWegoCfIG/S7N3r0+dbv s9GM8IAwUJS8QzqSd6Fs2KHFvbSbCoRGh7CI2/v8axtKvUThPH192kBG4VZN2z9LsOeD 3lOJ8gqSQGy8ndkl9rXlEOwCLvh/E5Yv2BhqTgWP2wEJ7VYy1nXLJ1HbFfTMowh1iGV3 qeV9KS8lvNY02QgtEM4s7IyEVV9CTvwK9aAmdQpmcEip5Sd95WantqCutI/SPurERclr AlaWy8WE9qYR7bG0zn6fVyb37EoJUq2hKcewMcFUwze37FRP6IxD6MD9NPdcaUC+28H4 YHtA== X-Forwarded-Encrypted: i=2; AJvYcCVtMxQR1sFNzGpveAMHRoAyr2+4vWOX7FsTneQfsVVHM1JbSBVQFQjCHYjtz7fBdxHdKQb/v0gsRWNS@gnusha.org X-Gm-Message-State: AOJu0YwNWhrI4qCz8QWQRSCQRGykM/ByV3tyBtmmtjzW81dn3aDvTzgJ 2Vwo80O75v40+pquuN6z3E4a1AK+99LP4KZpEZ7mrg9Xf9li5gqrySQK X-Received: by 2002:a05:6808:2213:b0:45e:91ea:89fc with SMTP id 5614622812f47-46ef5002b1cmr8767422b6e.2.1775563981511; Tue, 07 Apr 2026 05:13:01 -0700 (PDT) X-BeenThere: bitcoindev@googlegroups.com; h="AYAyTiIyR116fMzF51nPIK2L39/nRtgIEhEfH1TsjAG3M2dnqw==" Received: by 2002:a05:6870:63a8:b0:41c:24d9:eb8b with SMTP id 586e51a60fabf-422ee09828dls1749875fac.0.-pod-prod-02-us; Tue, 07 Apr 2026 05:12:55 -0700 (PDT) X-Received: by 2002:a05:6808:2395:b0:466:f3a2:dc2f with SMTP id 5614622812f47-46ef8017dfamr8253326b6e.48.1775563975604; Tue, 07 Apr 2026 05:12:55 -0700 (PDT) Received: by 2002:ab3:18a:0:b0:2e5:dca6:8eb2 with SMTP id a1c4a302cd1d6-2f65b8e9048msc7a; Tue, 7 Apr 2026 04:56:47 -0700 (PDT) X-Received: by 2002:a05:6512:1391:b0:5a3:e016:979c with SMTP id 2adb3069b0e04-5a3e0169812mr1015867e87.36.1775563006055; Tue, 07 Apr 2026 04:56:46 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1775563006; cv=none; d=google.com; s=arc-20240605; b=lhbaAN7aI/U6wxdFfxbp6wS9RRY0qIpAIg8Iz6gFxSIMRUtX9vWpYgNJYajRSw6X4A 2NHo53Qj7DHHBbrPk28/6dzitrPWwY3urK1XJZWEkLV63gYFOe7yehSId5qTP8HEf2lD kecvXT/Bb+vrd+9Wjot6EUzQVvUZZiBsnOtpQKm9epFiN9/nPafYFwzgSyCQFFLnD9iP o4jEvAdagzYpdGQyCR2Woe06qmPb/d1FU1zETXxo/iaK4NT8c5283+ZLMjOKk8e7V4Gx a4wcvMjLUYFWY181MMjoGDtyeZXpeajhqc+CWRMW2Ln14S+xB7m/eG89lf5+uf44JfnI 6gUQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20240605; h=content-transfer-encoding:content-language:to:subject:from :mime-version:date:message-id:dkim-signature; bh=s9U8fALQX4sYk57/s12cAMZLOcdCDblBjw50SwK5y7o=; fh=VcGcg+Zjs9gw1uDcHbxsAILhBAcecnbJzZRdxgKVDIc=; b=FRUjdi6sd4GIKutzxo6ekgjNzfyhSUZOLG8YZvSAG4H8colPeALT9b5iBMe1E97CWk idMtLSSw1cZFonfImKtOXIuM1i7D8GkAaRj9lVA4prfksf7Wh5DlXzlz0BrJ7i3FqEeE Ld+Rrude8kvMXXnZ6dfLG1VcprLBScQFcAoiIWk25WNvqssqE67NhgxFqNLVTtVbwPoV n/u27iGz6xhWsBXWqRa6Hbga0AIiAlL1jxdaL3g04wjnAc2V0SfdnnwPIMd712pWtdlg nOxN8QwO6Ct0/CHBo5tEDVZvQzBwVMJNpVSJ6IsFs1cbrmT6Vcao/wsO4ogQysuFEl94 EGaw==; dara=google.com ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@mailbox.org header.s=mail20150812 header.b=kkSzODnT; spf=pass (google.com: domain of remix7531@mailbox.org designates 2001:67c:2050:0:465::202 as permitted sender) smtp.mailfrom=remix7531@mailbox.org; dmarc=pass (p=REJECT sp=REJECT dis=NONE) header.from=mailbox.org Received: from mout-p-202.mailbox.org (mout-p-202.mailbox.org. [2001:67c:2050:0:465::202]) by gmr-mx.google.com with ESMTPS id 38308e7fff4ca-38cd212d19bsi3148041fa.4.2026.04.07.04.56.45 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 07 Apr 2026 04:56:46 -0700 (PDT) Received-SPF: pass (google.com: domain of remix7531@mailbox.org designates 2001:67c:2050:0:465::202 as permitted sender) client-ip=2001:67c:2050:0:465::202; Received: from smtp2.mailbox.org (smtp2.mailbox.org [IPv6:2001:67c:2050:b231:465::2]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) by mout-p-202.mailbox.org (Postfix) with ESMTPS id 4fql6N5vVLz9tTR for ; Tue, 7 Apr 2026 13:56:44 +0200 (CEST) Message-ID: <09b8adf7-0faa-4efa-b53a-7d29a5f40c12@mailbox.org> Date: Tue, 7 Apr 2026 13:56:44 +0200 MIME-Version: 1.0 From: "'remix7531' via Bitcoin Development Mailing List" Subject: [bitcoindev] Formal verification of secp256k1 modular scalar multiplication To: bitcoindev@googlegroups.com Content-Language: en-US Content-Type: text/plain; charset="UTF-8"; format=flowed X-MBO-RS-ID: 6a94445e958326c5ed7 X-MBO-RS-META: jnqgtngcy7pkgu8a8o1qgi7uzeuy1xwo X-Original-Sender: remix7531@mailbox.org X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@mailbox.org header.s=mail20150812 header.b=kkSzODnT; spf=pass (google.com: domain of remix7531@mailbox.org designates 2001:67c:2050:0:465::202 as permitted sender) smtp.mailfrom=remix7531@mailbox.org; dmarc=pass (p=REJECT sp=REJECT dis=NONE) header.from=mailbox.org X-Original-From: remix7531 Reply-To: remix7531 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: -1.0 (-) 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/ -- 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 email to bitcoindev+unsubscribe@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/bitcoindev/09b8adf7-0faa-4efa-b53a-7d29a5f40c12%40mailbox.org.