From mboxrd@z Thu Jan 1 00:00:00 1970 Delivery-date: Mon, 19 Oct 2026 09:43:22 -0700 Received: from mail-oo1-f57.google.com ([209.85.161.57]) by mail.fairlystable.org with esmtps (TLS1.3) tls TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 (Exim 4.94.2) (envelope-from ) id 1xIqSH-0004Y4-4m for bitcoindev@gnusha.org; Mon, 19 Oct 2026 09:43:22 -0700 Received: by mail-oo1-f57.google.com with SMTP id 006d021491bc7-704aee0b7b2sf1735612eaf.2 for ; Mon, 19 Oct 2026 09:43:20 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1792428195; cv=pass; d=google.com; s=arc-20260327; b=sFqlbDNbrz7OR4sU1gZxcDcNWqXyhYTJstXZhqdcchxPHImpmL7deOGj67lHGSIRs5 xob78acYCZW5Hnd94JeWGRN5vhuJPS0HtLEeqyJaHY3uOAZqrEJf18So+EEjBZwTLfns +7LrYjrvgywWAYwZWBPRt8UDZqxo0NdEba6KGhtV4c5X6rhxoMh7wcg5/QTdYxbi6H4S M2l7PS56o9xXf0K+J3mGwJ0qbuohzDQQVZk/PBZfLSrBLFht5zlkLSK9FkUgsT8OtTRU QZCS3/820S8twfEpUOHmc65b+ns60hrCRmB3LL7jvK/9azZ3F3q3D9J3wizzlwqq0pLa mniA== ARC-Message-Signature: i=3; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20260327; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=xfgHAaAvGJ/ps+WZzujF4m9z4d7QQj9ZGfag70Ux5WM=; fh=sJ2202ZXgxer5YAI6r9AY+UCm6zM27S5WACeETNtwVY=; b=IIBvG8YE0k9ptWXxMDeQfbYgbIrMSswmhX7corGmbxyqjqUYGJSkm2UQXncURvvOmy lt/dEjNkCx2WRjoh14OPqO85CzOv3BQd4phk7VU47iGsPEIIBNvPymLP2awzY095Msnt 490EF0ApCDDrd93JcG5Agm33Gn+NCFQFMkBGBCebYc08X9pIdma0cv8Sd/GJEBXmebZ1 VKZjoZE7+P69Um0yOByRoV8Taumy0iK8bdsXST29kb2oEXfvrLtAhl/DYxENPACNdg/S zuwjglj7m6j75erqNhigE04VBN7WLo0hq74kAcQbvuFOrrUt6mTu9T7a1BX3UFOEfvR6 Z6Tw==; darn=gnusha.org ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20251104 header.b=KkWhQiMX; arc=pass (i=1); spf=pass (google.com: domain of keagan.mcclelland@gmail.com designates 2607:f8b0:4864:20::631 as permitted sender) smtp.mailfrom=keagan.mcclelland@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com; dara=pass header.i=@googlegroups.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20251104; t=1792428195; x=1793032995; darn=gnusha.org; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:content-type:to:subject:message-id:date:from :mime-version:sender:from:to:cc:subject:date:message-id:reply-to :content-type; bh=xfgHAaAvGJ/ps+WZzujF4m9z4d7QQj9ZGfag70Ux5WM=; b=xITlrHSwHxMLnMjjN20vjhXfIMLzzJp8N0Qy+VCfEWtmr231pG/ocfpolzN0G52F0A kdPgVTMoe5LJSWmLapHjFeYbrBeu6EepXgxdOaw2NvTmQlDZ7UnHULYVgqThkK5N0gUi BBNI6WjbeGZaHDtVyFE73EAkbF13056Sb2nbtshe0Ea30Vmlny6UPkx7/9MuKw1hBP7Y +juM4vqPLjgtQ5WZEiQ3LwUigW+bfjNbFpTDCZpwa2DVQfMgv1Iv/YeYsZ3cYL5aDxnU RWbgXiTBsWP4jZDYKZMNNHfF9XjQ8vh7ktB21CSBkFvzAxkJHQnC9mmk/S2glM8s0lZ0 wfQQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20251104; t=1792428195; x=1793032995; darn=gnusha.org; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:content-type:to:subject:message-id:date:from :mime-version:from:to:cc:subject:date:message-id:reply-to :content-type; bh=xfgHAaAvGJ/ps+WZzujF4m9z4d7QQj9ZGfag70Ux5WM=; b=i6xZrtfjyAzGDu6UvrQJszdsKDErOgxeLpgTPk3csaG9YC2XXW5vOrQqs7X0ag70CN gHYt9sr8qp3Lr+nzH37Hvwx4JONk5RmvMLIEWWTsgNm6Z+xzrLFaMQkzd0lbsFK2ask1 Af+1SLaKzwghdp2hPLlqKobdfCiIqsXyx+iSreGkvLg15OiPefaNfps7GwLbMBIuIWxM zb+42loDY4BiiTtXoDvV6qrnI4jKwLqfryN+007iFUHCARycnXXZYJDZkTl69PF1CHzo cZl+GmRG5d4g93Fe3mXBI6USx9D27gGdWlvaEpkZzXcn6ur4ParaGLUmVH8rh0bUocfu 5MKw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20260707; t=1792428195; x=1793032995; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:content-type:to:subject:message-id:date:from :mime-version:x-gm-gg:x-beenthere:x-gm-message-state:sender:from:to :cc:subject:date:message-id:reply-to:content-type; bh=xfgHAaAvGJ/ps+WZzujF4m9z4d7QQj9ZGfag70Ux5WM=; b=U4akgrZGHtH+ctLz8KH3S/U1ihhCvQ/RzpBRcSwSdBQ6WlL3ZvyS4JQ3wJU9yo8lgv GaQ9zaLEyh2JCqIUoxYDC7kk24q9UYwjQKQbUUs9ksr1f+VYXE8SpKUupAk27uzjnTIH GZUliwIOqIZwZi/EXr1yUxFGkYlxlALm5zTPSTDkyKfDeZPhy6tvFbuRqgDG1ew3+QBA 2nP559TPZ613wc/IkyZH4r4t0kmBKTqCNJnPKtyfLJeU1cM9+ptZm9vXO4vg/OfiKTjc rtz5FZWal7s6MzfvGKkZwl9rWOam5CrfbgsaLBphzLBh7PL02dcQ8OlTThuRRJoVL+6e 6oOA== Sender: bitcoindev@googlegroups.com X-Forwarded-Encrypted: i=3; AKwUvByzjv+ML9rAR1/PNU76jnRHHf7pOoJxRBDh/e/biQzk4UqTmqitl3N0qsDZEr1vrMKEXLM8GiUCqZtb@gnusha.org X-Gm-Message-State: AFq9FYJof1qnsUoRtMftCj1LR+vwaVX9BVQZstTLK2jv7M1TK/nLO1uu ++mE7TZhM/T06rvGdjIQpuDdqZCwkUMMiUlLjMdp6n3ZhtEiEBRm/U/6 X-Received: by 2002:a05:6820:858f:10b0:6d7:c5f2:9c0b with SMTP id 006d021491bc7-7035769cf06mr4221295eaf.68.1792428194822; Mon, 19 Oct 2026 09:43:14 -0700 (PDT) X-BeenThere: bitcoindev@googlegroups.com; h="ATskLdeFR7z208Vd2xt9hZlzJkTpbG8nrD6SbRA0zOpo4jKm0Q==" Received: by 2002:a05:6820:8405:b0:6d9:cd31:7e07 with SMTP id 006d021491bc7-7055320b0b8ls1117369eaf.2.-pod-prod-05-us; Mon, 19 Oct 2026 09:43:07 -0700 (PDT) X-Received: by 2002:a05:6808:11c1:b0:53a:6769:c365 with SMTP id 5614622812f47-53cd1cbb033mr6802572b6e.12.1792428186925; Mon, 19 Oct 2026 09:43:06 -0700 (PDT) Received: by 2002:a05:6808:5d4:b0:4f2:82e8:c758 with SMTP id 5614622812f47-542cb51d7d1msb6e; Mon, 19 Oct 2026 09:33:49 -0700 (PDT) X-Received: by 2002:a05:6820:1693:b0:702:f890:e113 with SMTP id 006d021491bc7-70352296a0cmr5693844eaf.9.1792427628772; Mon, 19 Oct 2026 09:33:48 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1792427628; cv=pass; d=google.com; s=arc-20260327; b=QVv0qTLsloGPFFxZtmmZ4NF6NrZ5DjmjKSmuIz8BevyOqTAtiL8S9/0RUvsJxFiIzl RLeEehWGeSvB7EUzuIS1dKXMWeeWOlRzhSFhnq4yvkdVKIfYG0ujk3Qu2fI5pojImTpP tktvZ/vqOXB9bBuFgkSH9oxZq9UaNgDToDUXmpttYzOyY6XUwcNwVr91ye/AC0O6oWX0 sOoe7Zq03usb55Xy9m5iizC0gQkFNsM2XLr+nyl2oz++Rz1paRrGOArgTigExG5E6Kn0 kSeHdBtB8YnRZrD3KyablLuUODnS2s3DR0aX4u3jzQYEpQRMseqUwjYf1khAMU6Il8xO l0Aw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20260327; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=7CrHx7vCrknXo0T2aOyuGB7r4EVOhhuzyW3tVm0bbjc=; fh=DMP0F9ULS1guKiqimntQRCN8ZraraesEgQuVcn7F0Z0=; b=YShfEFZwTWroFPSG8U2aFdIL9SkDV6L5uKFdKQDrkSCGTeIgZPz9RO1/PE6H1LozA6 bJXVPOVwlJCYWTNqSUpUUGLUZl57s7nWwlztOVvDFUfaS16yprP2Sptu0lUGtp8w6nD5 LRLfXemFxSjWNfZMdwMDeMwiuvPZkxp/TFpsYzu5v4TkzU9K4ThsGYQQ0J0f40gNInE9 QPY7/lLNbFCWUvJLSZeZ6r3JlWvKP36xrlEs6c30i4OWxtcTkjCnDffhjhc7ELRbzwE/ nMVsESy/EP3r/wzP9UA1OM3Cw4XQCtLDvZosE5qu+FcZbPdyAGYlNCI2LHNXcNmbml2e 1BXQ==; dara=google.com ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20251104 header.b=KkWhQiMX; arc=pass (i=1); spf=pass (google.com: domain of keagan.mcclelland@gmail.com designates 2607:f8b0:4864:20::631 as permitted sender) smtp.mailfrom=keagan.mcclelland@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com; dara=pass header.i=@googlegroups.com Received: from mail-pl1-x631.google.com (mail-pl1-x631.google.com. [2607:f8b0:4864:20::631]) by gmr-mx.google.com with ESMTPS id 46e09a7af769-842a692e5c2si234473a34.8.2026.10.19.09.33.48 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 19 Oct 2026 09:33:48 -0700 (PDT) Received-SPF: pass (google.com: domain of keagan.mcclelland@gmail.com designates 2607:f8b0:4864:20::631 as permitted sender) client-ip=2607:f8b0:4864:20::631; Received: by mail-pl1-x631.google.com with SMTP id d9443c01a7336-2e8ad5b31c7so12882495ad.3 for ; Mon, 19 Oct 2026 09:33:48 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1792427628; cv=none; d=google.com; s=arc-20260327; b=XH8VPDsBiRdxd7j0baFZdcNwaZLAdFkblZHU7KUkM1+hRmrNOVP6WjrCnDpI7DEwl1 +xi1yzRkaNK/HUJR1cuZNeKHF/bL94Kyr5tWmnZbKNbrjk65jumUptX+1qiyFg8dJYYE ChpcIdPq4GMTrQLsnPXtYZyWtW/6lPgZ4+hPk6g/ogP2KJ7LyYdAzoTKPOlWH6D86y1C MFWhMmccJQdGkf+W6r5n3f5BsUOhhcVFryDrwM6ZSUDmx711lzKobVF9fLgVIKSI0HOO kRph46TES1g+iJrAwhAPFQCisdmFxuqqA9nRecwr7EevBWIQVoftpEqr9yF3NiNRLOtG MQvQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20260327; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=7CrHx7vCrknXo0T2aOyuGB7r4EVOhhuzyW3tVm0bbjc=; fh=DMP0F9ULS1guKiqimntQRCN8ZraraesEgQuVcn7F0Z0=; b=o40mSNy/KwzUqVakXtelun25kd7HFjHEm3ORUahe3SGbiGBdPhFnXV8AgN31GO10ue oyIR92NV8lKsnzq01IeO6Idt9jZeirbKuBGGENTq0Zh+fLmGOON69H6QU6KUQPjcQwFc ILHZdQBplVkmSx3ek/S2pnxpUkGCD0AahAEXpPzBOC1Z/jA3gWMffQcRSiOBSFev6tC5 rbj0F3sGpCtMqapeNPh8WthQLhAuChGG0sGLJxVxyToeTyKXJdRq4PJBX0UbTwOkQ0wR xgoFc+ljfACItGaPtWpSE30JIdLyMy8pxv5adse1hmjpVaYEWdPx4L4BbDM+SOLqOly6 DweA==; dara=google.com ARC-Authentication-Results: i=1; mx.google.com; arc=none X-Gm-Gg: AYBFou00uaJ0OWWK9qNNNU0BFZgXRF/E+9C0zov7TEQ5AXhmxluxHmqxksEkEpQGNVx eOa3zMgjWlF5lftk8V+zVEBRjMC/X3J0486P5TRn0sByw6y7mBcS2hCVjY5//A6RQsih15HU/Dc YWuxuN8ksj9j6SL+pwN/DoQ5dFnZKrwI+5/tCPY98qtKnfv1jvGtejc8bBMpPO8GPl8d62A+FgJ 0qtGZgYKTtRzrA0KOvgm3R0qnmT1+O1pTEAd0fnwT74aMfjDTbaI1DP2ADrN+UkwMFlKRTNTZmP f1xE2gOVCQsFxsBrxdaXiNdL6nlW2ikx087CfjTQYf9aH8WeCThMaeQEHu3qesBf28G3TjfnOrZ BpX45+fkZc+YOnTxbpmicjov9otfPftljAy/jZfxxlEZaJLrjVH5dbOvrZDB7DaW1FbLhGbyrCG Ha2NOcWUr1lV0uJmAqjR1XynD/IHkf+WI0g94/GWE= X-Received: by 2002:a17:903:1208:b0:2df:8382:918b with SMTP id d9443c01a7336-2e9a67067femr70354445ad.0.1792427627979; Mon, 19 Oct 2026 09:33:47 -0700 (PDT) MIME-Version: 1.0 From: Keagan McClelland Date: Mon, 19 Oct 2026 10:33:36 -0600 X-Gm-Features: AclHuK-lTXq976VppWmL2w0vKrw_Xwsirx0OXpGIYYdek4hp6-hApkJ717S01tw Message-ID: Subject: [bitcoindev] btc-verified October Update: Connecting Map to Territory To: Bitcoin Development Mailing List Content-Type: multipart/alternative; boundary="0000000000000d31f6065e3414de" X-Original-Sender: keagan.mcclelland@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20251104 header.b=KkWhQiMX; arc=pass (i=1); spf=pass (google.com: domain of keagan.mcclelland@gmail.com designates 2607:f8b0:4864:20::631 as permitted sender) smtp.mailfrom=keagan.mcclelland@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com; dara=pass header.i=@googlegroups.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.1 (/) --0000000000000d31f6065e3414de Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Originally published on my site . Replicating here because I think the Delving audience has an interest in this work. ------------------------------ >From the project=E2=80=99s inception until now, btc-verified has been focused on building up, layer by layer, a very minimal model of consensus. Last month=E2=80=99s= post talked about how we can discover hidden subtleties in how something works when we try to formalize it. However, even as we formalize things we have to resist the temptation to merely assume that the precise map we have created actually reflects the reality on the ground. This month, however, I decided to take a stab at anchoring this model to the Bitcoin network as it exists in the real world. It=E2=80=99s tricky to do this type of thing because it forces us to ask th= e question how do we know the map matches the territory? How close can we get= ? For most software that you want to verify it is an option on the table to simply write the software in a verifiable language, compile that down to code that actually runs on silicon and be on your merry way. Alternatively, if the code you=E2=80=99re trying to verify is pure C code, there are ways = to verify the C code directly since C=E2= =80=99s operational semantics are small enough to reason somewhat efficiently about= . The problem here is that Bitcoin Core , which on a practical level *defines* the Bitcoin protocol, is neither written in a verifiable language, nor is it written in pure C. Rather, it is written in modern C++ so verifying it directly, while possible on theoretical grounds is very far out of reach with my current resources. So what can we do instead? The main thing we are trying to establish is that our model does not differ from Bitcoin Core in any observable way with respect to its protocol semantics. Hypothetically, if we were able to come up with an implementation of the protocol in Lean that had no differences in behavior from Bitcoin Core, it would mean that the model, in a sense, IS Bitcoin Core. If the model predicts reality with 100% accuracy, we can say that the model is =E2=80=9Ccorrect=E2=80=9D. This seems like a simple enough thesis, but it is far from well defined enough to build something around. What constitutes a behavior? How can we observe the behavior? How can we tell if it=E2=80=99s different or not? Wha= t things are implementation details and what things are essential semantics? People have been trying for years to extract out Bitcoin consensus from the rest of Bitcoin Core and the most recent label for this effort is the libbitcoinkernel project . This carves out a chunk of Core inside of which is the consensus verification code and outside of which we can safely write all kinds of custom implementation experiments without compromising the safety of consensus. The original purpose of this project is actually to reduce the usage of non-Core implementations of consensus. However, it also gives us a natural entry point for our purposes here. To do this carve out, libbitcoinkernel must define an interface that preserves the essential invariants of consensus and for it to be usable, its interface must give us the ability to know whether something is consensus valid or not. What I have decided to do is to take advantage of the existence of this interface and ensure that btc-verified can serve as the implementation behind it. We are not doing this to encourage people to run btc-verified=E2= =80=99s consensus instead of Bitcoin Core=E2=80=99s. We are doing this to set up a benchmark of btc-verified=E2=80=99s faithfulness of matching Core=E2=80=99s= behavior on the faultline that has already been drawn by the Bitcoin Core team. Once we have established a trivial implementation of libbitcoinkernel=E2=80= =99s interface in the btc-verified project, then we can take advantage of another technique that has an established practice in the space: differential fuzzing. bitcoinfuzz is a project whose aim is differential fuzzing of different bitcoin implementations. The idea here is that we spew entropy at the kernel interface and ensure that for any given payload that Core=E2=80=99s kernel and btc-verified=E2=80=99s ker= nel report the same result, including any state changes that are made by the operation executed. bitcoinfuzz already has an established track record and has found numerous bugs in different implementations using this strategy. Indeed, short of proofs, the best we can do to establish equality is to do high-entropy sampling of the behavior of each implementation and ensure they never diverge. Of course, you never know if the next sample you take is the one that reveals a difference. This is the exact reason that formal verification even has a place, because you cannot establish universal laws through sampling alone, but it does have a practical benefit of reducing the probability of divergent behavior the more that the sample space saturates the control flow graph. Following this thread, I put together a standalone differential fuzzing harness for Bitcoin Core and btc-verified, specifically against the kernel interface, and we have nine of the kernel functions backed by a Lean implementation. These functions cover transaction creation, copying, serialization, checking, and the associated validation-state objects. The harness is built directly on libFuzzer . It gives the same transaction bytes to Core and btc-verified, then compares their observable behavior. As of right now btc-verified does not implement the entire kernel interface even trivially, but it does implement a subset of it with apparently correct semantics for the following behaviors: - Parsing: Given identical bytes, do both implementations accept them as a transaction object? This is distinct from accepting the transaction as valid. - Serialization: For accepted inputs, do both report the same serialization status and produce exactly the same bytes? - Transaction-local checking: Do they agree on the verdict for rules concerning input/output presence, duplicate or null input references, output-value and stripped-size limits, and the special coinbase conditio= ns? These checks don=E2=80=99t consult the UTXO set or execute scripts. - Reported validation state: Do they return the same validation mode and result category, beyond merely agreeing on acceptance or rejection? - State reuse: After checking a known-invalid transaction, does checking the next transaction replace that previous result consistently=E2=80=94i= ncluding clearing the invalid state when the next transaction passes? As of this writing these behaviors are identical between btc-verified and Bitcoin Core when observed over this battery: - 100,000 fuzz executions: this measures how many attempts for disagreement were made. Each execution feeds one byte sequence into the differential harness, which runs both implementations and compares their observations. This measures testing volume. It doesn=E2=80=99t count uni= que transactions: inputs can repeat, and malformed inputs may be rejected during parsing without reaching transaction checking. Mutations are also related to earlier inputs, rather than independent random samples. - 11 regression inputs: this measures how many pre-determined cases are explicitly replayed. These ensure particular cases are checked every tim= e, regardless of what mutation happens to discover. =E2=80=9CRegression=E2= =80=9D here doesn=E2=80=99t mean each input previously exposed a bug. The ones here include real leg= acy and SegWit transactions, malformed encodings, a transaction that parses = but fails checking, and three transactions immediately below, at, and above = the million-byte stripped-size boundary. Those large cases matter because th= e mutation campaign=E2=80=99s 4,096-byte limit prevents it from discoverin= g them. - 264 retained corpus inputs: this was the size of the working corpus at the end of the October 18 CI run . LibFuzzer keeps inputs that contribute useful coverage feedback and uses them as starting points for further mutations. The final corpus count describes that working collection, including retained starting seeds. This differential test additionally runs as a CI check before new code is merged allowing observed disagreement with Core to block changes to the code. There is a ton of work still to do to strengthen the link between btc-verified and Bitcoin Core but assuming we can establish a credible link between them it allows us to borrow some of the theorems and findings we can establish natively in btc-verified and use them to make statements about Bitcoin Core=E2=80=99s behavior. Over the coming month the plan is to push forwards on filling out the rest of the kernel interface so we can officially connect this map to this territory, at least tenuously for now, before pushing forwards on analyzing the map itself. Godspeed, Keags --=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/= CALeFGL04_h6212x9D0u7-uJSyDDAyie-cohBazYS3Yo9P36NVA%40mail.gmail.com. --0000000000000d31f6065e3414de Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Originally published=C2=A0on my site. Replicating here because I think the Delvin= g audience has an interest in this work.

From the project=E2=80=99s inception until now,= =C2=A0btc-= verified=C2=A0has been focused on building up, layer by layer, a very m= inimal model of consensus.=C2=A0Last month=E2= =80=99s post=C2=A0talked about how we can discover hidden subtleties in= how something works when we try to formalize it. However, even as we forma= lize things we have to resist the temptation to merely assume that the prec= ise map we have created actually reflects the reality on the ground. This m= onth, however, I decided to take a stab at anchoring this model to the Bitc= oin network as it exists in the real world.

It=E2=80=99s trick= y to do this type of thing because it forces us to ask the question how do = we know the map matches the territory? How close can we get?

F= or most software that you want to verify it is an option on the table to si= mply write the software in a verifiable language, compile that down to code= that actually runs on silicon and be on your merry way. Alternatively, if = the code you=E2=80=99re trying to verify is pure C code, there are ways to= =C2=A0verify= the C code directly=C2=A0since C=E2=80=99s operational semantics are s= mall enough to reason somewhat efficiently about.

The problem = here is that=C2=A0Bi= tcoin Core, which on a practical level=C2=A0defines=C2=A0the B= itcoin protocol, is neither written in a verifiable language, nor is it wri= tten in pure C. Rather, it is written in modern C++ so verifying it directl= y, while possible on theoretical grounds is very far out of reach with my c= urrent resources.

So what can we do instead?

The = main thing we are trying to establish is that our model does not differ fro= m Bitcoin Core in any observable way with respect to its protocol semantics= . Hypothetically, if we were able to come up with an implementation of the = protocol in=C2=A0Lean=C2=A0t= hat had no differences in behavior from Bitcoin Core, it would mean that th= e model, in a sense, IS Bitcoin Core. If the model predicts reality with 10= 0% accuracy, we can say that the model is =E2=80=9Ccorrect=E2=80=9D.

This seems like a simple enough thesis, but it is far from well defi= ned enough to build something around. What constitutes a behavior? How can = we observe the behavior? How can we tell if it=E2=80=99s different or not? = What things are implementation details and what things are essential semant= ics?

People have been trying for years to extract out Bitcoin = consensus from the rest of Bitcoin Core and the most recent label for this = effort is the=C2=A0libb= itcoinkernel project. This carves out a chunk of Core inside of which i= s the consensus verification code and outside of which we can safely write = all kinds of custom implementation experiments without compromising the saf= ety of consensus. The original purpose of this project is actually to reduc= e the usage of non-Core implementations of consensus. However, it also give= s us a natural entry point for our purposes here.

To do this c= arve out, libbitcoinkernel must define an interface that preserves the esse= ntial invariants of consensus and for it to be usable, its interface must g= ive us the ability to know whether something is consensus valid or not.

=

What I have decided to do is to take advantage of the existence o= f this interface and ensure that btc-verified can serve as the implementati= on behind it. We are not doing this to encourage people to run btc-verified= =E2=80=99s consensus instead of Bitcoin Core=E2=80=99s. We are doing this t= o set up a benchmark of btc-verified=E2=80=99s faithfulness of matching Cor= e=E2=80=99s behavior on the faultline that has already been drawn by the Bi= tcoin Core team.

Once we have established a trivial implementa= tion of libbitcoinkernel=E2=80=99s interface in the btc-verified project, t= hen we can take advantage of another technique that has an established prac= tice in the space: differential fuzzing.

bitcoinfuzz=C2=A0is a project= whose aim is differential fuzzing of different bitcoin implementations. Th= e idea here is that we spew entropy at the kernel interface and ensure that= for any given payload that Core=E2=80=99s kernel and btc-verified=E2=80=99= s kernel report the same result, including any state changes that are made = by the operation executed.

bitcoinfuzz already has an establis= hed track record and has=C2=A0found n= umerous bugs in different implementations=C2=A0using this strategy. Ind= eed, short of proofs, the best we can do to establish equality is to do hig= h-entropy sampling of the behavior of each implementation and ensure they n= ever diverge.

Of course, you never know if the next sample you= take is the one that reveals a difference. This is the exact reason that f= ormal verification even has a place, because you cannot establish universal= laws through sampling alone, but it does have a practical benefit of reduc= ing the probability of divergent behavior the more that the sample space sa= turates the control flow graph.

Following this thread, I put t= ogether a=C2=A0standalon= e differential fuzzing harness=C2=A0for Bitcoin Core and btc-verified, = specifically against the kernel interface, and we have=C2=A0nine of the kernel= functions=C2=A0backed by a Lean implementation. These functions cover = transaction creation, copying, serialization, checking, and the associated = validation-state objects. The harness is built directly on=C2=A0libFuzzer. It gives the= same transaction bytes to Core and btc-verified, then compares their obser= vable behavior.

As of right now btc-verified does not implemen= t the entire kernel interface even trivially, but it does implement a subse= t of it with apparently correct semantics for the following behaviors:

<= ul style=3D"margin:1em 0px 1em 1.25em;padding:0px;clear:both;font-family:Ar= ial,sans-serif;font-size:16px;font-variant-ligatures:none">
  • Parsing:=C2=A0Given identical bytes, do both= implementations accept them as a transaction object? This is distinct from= accepting the transaction as valid.
  • Serialization: For accepted in= puts, do both report the same serialization status and produce exactly the = same bytes?
  • Transaction-local ch= ecking:=C2=A0Do they agree on the verdict for rules concerning input= /output presence, duplicate or null input references, output-value and stri= pped-size limits, and the special coinbase conditions? These checks don=E2= =80=99t consult the UTXO set or execute scripts.
  • Reported validation state:=C2=A0Do they return the = same validation mode and result category, beyond merely agreeing on accepta= nce or rejection?
  • State reuse: After checking a known-invalid trans= action, does checking the next transaction replace that previous result con= sistently=E2=80=94including clearing the invalid state when the next transa= ction passes?

    • As of this writing these behaviors are ide= ntical between btc-verified and Bitcoin Core when observed over this batter= y:

    • 100,000 fuzz executions: this measures= how many attempts for disagreement were made. Each execution feeds one byt= e sequence into the differential harness, which runs both implementations a= nd compares their observations. This measures testing volume. It doesn=E2= =80=99t count unique transactions: inputs can repeat, and malformed inputs = may be rejected during parsing without reaching transaction checking. Mutat= ions are also related to earlier inputs, rather than independent random sam= ples.
    • 11 regression inputs:=C2=A0this measures how many pre-determined cases are explicitly replayed= . These ensure particular cases are checked every time, regardless of what = mutation happens to discover. =E2=80=9CRegression=E2=80=9D here doesn=E2=80= =99t mean each input previously exposed a bug. The ones here include real l= egacy and SegWit transactions, malformed encodings, a transaction that pars= es but fails checking, and three transactions immediately below, at, and ab= ove the million-byte stripped-size boundary. Those large cases matter becau= se the mutation campaign=E2=80=99s 4,096-byte limit prevents it from discov= ering them.
    • 264 retained corpus = inputs:=C2=A0this was the size of the working corpus at the end of t= he=C2=A0October 18 CI run. LibFuzzer ke= eps inputs that contribute useful coverage feedback and uses them as starti= ng points for further mutations. The final corpus count describes that work= ing collection, including retained starting seeds.

    This = differential test additionally runs as a=C2=A0CI check=C2=A0before new code = is merged allowing observed disagreement with Core to block changes to the = code.

    There is a ton of work still to do to strengthen the lin= k between btc-verified and Bitcoin Core but assuming we can establish a cre= dible link between them it allows us to borrow some of the theorems and fin= dings we can establish natively in btc-verified and use them to make statem= ents about Bitcoin Core=E2=80=99s behavior.

    Over the coming mo= nth the plan is to push forwards on filling out the rest of the kernel inte= rface so we can officially connect this map to this territory, at least ten= uously for now, before pushing forwards on analyzing the map itself.


    Godspeed,

    Keags

    --
    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/ms= gid/bitcoindev/CALeFGL04_h6212x9D0u7-uJSyDDAyie-cohBazYS3Yo9P36NVA%40mail.g= mail.com.
    --0000000000000d31f6065e3414de--