From mboxrd@z Thu Jan 1 00:00:00 1970 Delivery-date: Fri, 23 Oct 2026 17:59:11 -0700 Received: from mail-oa1-f62.google.com ([209.85.160.62]) by mail.fairlystable.org with esmtps (TLS1.3) tls TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 (Exim 4.94.2) (envelope-from ) id 1xKQ6I-0006UW-9e for bitcoindev@gnusha.org; Fri, 23 Oct 2026 17:59:11 -0700 Received: by mail-oa1-f62.google.com with SMTP id 586e51a60fabf-49dd26d6f07sf1488412fac.0 for ; Fri, 23 Oct 2026 17:59:09 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1792803544; cv=pass; d=google.com; s=arc-20260327; b=rT1TJNSrpViZECNHwzlRv+/JYpU4iMdeBKeS8iuukAcVtG9YrEz18/uZzBhSD9xg92 fxOCyDFltjJ+VnC9WSrKV0MgcCSSWEvAFVU1R8sS+GgRkur9P/BSstk+uLa+WSGm3kY3 AGZ/ZPO9uPlo91OgLX7QPAir79o18LDb1c4ZJjx2Ckc2b7wezBN26za+3y55I5eYhHHg WSbZHlIZmNrtu7vB1Euaq6MAUAUYi8MzgpLgZeDN/vBfAl/0eEfpeC0uK3hMrm01gMVF vwgTpFbxtnvjkWhahderwBSppgDTeDS46+Nkxo19i1fOk6n1N7W4ziXvm71QSdps6IPQ i3cg== ARC-Message-Signature: i=2; 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:in-reply-to:from:content-language :references:to:subject:mime-version:date:message-id:sender :dkim-signature; bh=fbkKPjWqPIpynUzJuBFDG+8hs07UFS2FVP+pm9pjmy0=; fh=rfvrlOk7ilh6LjZBW58NPWgkfJW9bTVu/A4iG245w2Q=; b=rwWCwCwFuBu95b3E/NKizvGtCZWGbZ/aZ2HFMgquwYeSesK/s/y2Ai56JdXyIZocII /BfjEipoqDFqS2pN3Kg0BjKt6ZP8z6iD02Lub6NG7IdC69+nj9F+qigj7X3O9rmTY2Lg 2y5AYU5OPO/yOTtHFN4s3AU4k7ZqgtNlIuNkxjaGMk87srRoPWEUbmn96n+uP0mt5LJv bcn0nqEi2y2sMhi7gGEL+W4clUugsBZePGAcTUdT27Ghx8SMWPdABNhvlGRjWG5IlLsI GICO5JrasCEXgxcgavauiyim6KYEUkyocNq2KlYIZcCKOhIK+uiZbZqIcpMxS73mBQTq YqnA==; darn=gnusha.org ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@mattcorallo.com header.s=1792800062 header.b=o8B0TbMi; dkim=pass header.i=@clients.mail.as397444.net header.s=1792800063 header.b=NdzSuz3V; spf=pass (google.com: domain of lf-lists@mattcorallo.com designates 2620:6e:a000:1::99 as permitted sender) smtp.mailfrom=lf-lists@mattcorallo.com; dmarc=pass (p=NONE sp=REJECT dis=NONE) header.from=mattcorallo.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20251104; t=1792803544; x=1793408344; 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:in-reply-to:from:content-language:references:to :subject:mime-version:date:message-id:content-type:sender:from:to:cc :subject:date:message-id:reply-to:content-type; bh=fbkKPjWqPIpynUzJuBFDG+8hs07UFS2FVP+pm9pjmy0=; b=S94mPnLs8qyXqq3YZSAucC8VUu0uI+P8mb59VerqVxIPXaqBU0WzcDRtJndfDrqzq/ FibbbHL65TYYBKB22lIBmiBk5ztx1yVytYYQQ6Wv0iHLe8P6cagEqFQbZNs8H+iw97Oy 2OwH4bPsYtnrB2Ac65sHSlWtwIONeZ7prNHVR4Wf4la13kMJNld+FziseIe/+UfBPHwt VvjfCiP1YlpZCCdIuD4j+DoMIWQnnuVcg51XwNJiBjKVMEO/WDsdy4XhyR+ohTnImxpk qyf2QYGO6csExmowfPSq5n07GAGJ3kdQdv86YnGFe7YNMq6hd3mLMus/2h7vPs7rGr6v h5xA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20260707; t=1792803544; x=1793408344; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:in-reply-to:from:content-language:references:to :subject:mime-version:date:message-id:content-type:x-beenthere :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to:content-type; bh=fbkKPjWqPIpynUzJuBFDG+8hs07UFS2FVP+pm9pjmy0=; b=Q1B3GsS2SucXj2m+XNWul5lhju1pLwwLtyIdBz/qkJFA1g6/Dtiem5dz9iFuRLiXXZ IiDufvircfh8FkGEbFveXH5JMx9oq8X2xLxREnKR4jyz+YFlgJ94mpP3Lnjc9Iv9Uxf9 xKJQyvZcsoKiTNtaza1lit4vPZsui9r5AHV88pa8thYUW3pvW6UyXtYi06SxZvsIoEtn N4GZEZopYnukrmJI57rdin8ylrEIYPoaifiE3M+DDBqDH/FsGvqc9pkPxfqBsAG55rOg Bg9uTXn4mCmMUibKzum0vgT7oDQ4UVT1/2yg36H6HzJUo0XGlXyyph+VOZZ8oL9XcvnT wppQ== Sender: bitcoindev@googlegroups.com X-Forwarded-Encrypted: i=2; AKwUvBzmOutDoy6ZWRpEJA5GBq3T3ZiBOGcJp/v+xcrM7LHv+O4XHkMx1v0fXRgrgOiYwp0GMQgIifbNwQK4@gnusha.org X-Gm-Message-State: AFq9FYK9xYS7DtcCy9tpFl22fHUJhQUmzC+73tbuqDlwwYTxKVNDkNdX m/ixbPZ40BUrg1dPbANyG4zqfRdV1TjO+zm1AkVLE7LJkYxquwDP4FtI X-Received: by 2002:a05:6870:c255:b0:49e:7c51:3b19 with SMTP id 586e51a60fabf-4a83f60f96emr687494fac.48.1792803543931; Fri, 23 Oct 2026 17:59:03 -0700 (PDT) X-BeenThere: bitcoindev@googlegroups.com; h="ATskLddwIIZfzeKQ+mBEwA+4NewM55VD3L6KyxMNJ+kdV4KrIg==" Received: by 2002:a05:687c:23cf:20b0:492:46f8:3965 with SMTP id 586e51a60fabf-4a81c2cac48ls1219407fac.0.-pod-prod-09-us; Fri, 23 Oct 2026 17:58:56 -0700 (PDT) X-Forwarded-Encrypted: i=2; AKwUvBwFc6zjCDDVOcjFgcvHRthTgbx8moczfXHA55+RSc5IGJkXV6/i5602DJp5QYT9KoYUafxqVpUgezTW@googlegroups.com X-Received: by 2002:a05:6808:c40e:b0:4e6:b6a1:5af2 with SMTP id 5614622812f47-55c0036416emr558069b6e.51.1792803536068; Fri, 23 Oct 2026 17:58:56 -0700 (PDT) Received: by 2002:a05:6808:985:b0:4eb:c749:9323 with SMTP id 5614622812f47-55be48c875dmsb6e; Fri, 23 Oct 2026 17:30:52 -0700 (PDT) X-Forwarded-Encrypted: i=2; AKwUvBzwa93g/w4SiRrWUAEvm0z5sDxnM5ISuXlfi115b6wd8FXr50iUqdOKeYmNxCJn7D7EFb/1JQV0r+Is@googlegroups.com X-Received: by 2002:a05:7301:1509:b0:359:818a:df2d with SMTP id 5a478bee46e88-369e84a88edmr1146342eec.31.1792801851090; Fri, 23 Oct 2026 17:30:51 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1792801851; cv=none; d=google.com; s=arc-20260327; b=sxN1Fm416i2Xy+MtBfjlYvfyFNNuuetCUCzhaRnOTHc+pIlzXxPLGjxthQNOYYiXU9 G8n+9vpPvbHL4VBplJ7MgKioPjNE8Gdp5ad8UEHNXAKcQ4IwuLy0ZUeXd+Kg0WMOX4S7 jrMWeEt5sMjzQTmFtZbwM5AfM/pybDBlyiM0uOOZEp8+mQkMJG5Yta/MdOuAuWNc2x4t LOIUQMSgLQozbsEq5sA0SHni2bJ3TIiDLYKWhQmzshwiYM2JMJ/rbMQAk8NYR3woAtBh cCdd8N10anMir48k+g9I6G6UX3KGRrGFhuEpvQHVeSTql6Y6Xp0nE4ThvPf+dk1mxKly hgpA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20260327; h=in-reply-to:from:content-language:references:to:subject :mime-version:date:message-id:dkim-signature:dkim-signature; bh=AOMsQPYT44+u48eoPHtthsknMQcO46O6/5es+4ex28A=; fh=EncpAHVDlgCAmq0byyzBmLhf9PwEJbhs/Ki6FDwBegI=; b=VuFJ6OOHgmgPj9WSjFZyUIMLRvsyXai2ln1lWMhC7eohqthygtEE2tPaCxF9YscV/6 2kvBt+V5fWTNAxqEAFwS9/YifJsTc6tgNHSDLnCzLvwmGhU1Jyb6FtYTcF7XwG+QoLiE 1NvEjulRKTpBpZ2npnEBy0YgeWjq3iEHHDhAvKaTOWvedAxaT4nZRPaIQq7t5osvwh+y fS4sALE4Vg2/xWALY3eBPL8PRDsrxp4oQqYcFfTHfSBk2d5jLSl0CcF8g8+xovC3Vxfx ZpWiOJXhE2XKYIWsJrBxyTABZXdIT6eXBUNz2TAvfZeL4lzwA31b+Hsvgzocbpyd9X6J 0cqA==; dara=google.com ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@mattcorallo.com header.s=1792800062 header.b=o8B0TbMi; dkim=pass header.i=@clients.mail.as397444.net header.s=1792800063 header.b=NdzSuz3V; spf=pass (google.com: domain of lf-lists@mattcorallo.com designates 2620:6e:a000:1::99 as permitted sender) smtp.mailfrom=lf-lists@mattcorallo.com; dmarc=pass (p=NONE sp=REJECT dis=NONE) header.from=mattcorallo.com Received: from mail.as397444.net (mail.as397444.net. [2620:6e:a000:1::99]) by gmr-mx.google.com with ESMTPS id 5a478bee46e88-369e8f0ba61si12693eec.9.2026.10.23.17.30.50 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 23 Oct 2026 17:30:50 -0700 (PDT) Received-SPF: pass (google.com: domain of lf-lists@mattcorallo.com designates 2620:6e:a000:1::99 as permitted sender) client-ip=2620:6e:a000:1::99; X-DKIM-Note: Keys used to sign are likely public at X-DKIM-Note: https://as397444.net/dkim/mattcorallo.com and X-DKIM-Note: https://as397444.net/dkim/clients.mail.as397444.net X-DKIM-Note: For more info, see https://as397444.net/dkim/ Received: by mail.as397444.net with esmtpsa (TLS1.3) (Exim) (envelope-from ) id 1xKPeq-000000060Am-3k77; Sat, 24 Oct 2026 00:30:49 +0000 Content-Type: multipart/alternative; boundary="------------uoPaKCdvbL0LJlH90DYe4IIo" Message-ID: <8bfb3bbc-0682-49c8-b461-676aa619688e@mattcorallo.com> Date: Fri, 23 Oct 2026 20:30:48 -0400 MIME-Version: 1.0 Subject: Re: [bitcoindev] btc-verified October Update: Connecting Map to Territory To: Keagan McClelland , Bitcoin Development Mailing List References: Content-Language: en-US From: Matt Corallo In-Reply-To: X-Original-Sender: lf-lists@mattcorallo.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@mattcorallo.com header.s=1792800062 header.b=o8B0TbMi; dkim=pass header.i=@clients.mail.as397444.net header.s=1792800063 header.b=NdzSuz3V; spf=pass (google.com: domain of lf-lists@mattcorallo.com designates 2620:6e:a000:1::99 as permitted sender) smtp.mailfrom=lf-lists@mattcorallo.com; dmarc=pass (p=NONE sp=REJECT dis=NONE) header.from=mattcorallo.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 (/) This is a multi-part message in MIME format. --------------uoPaKCdvbL0LJlH90DYe4IIo Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Figured you might find this interesting, Last week Rob had some tokens to spend so I asked him to see whether any pr= ogress could be made on=20 formal equivalence proofs of script engines. The agents didn't make much pr= ogress with the tokens=20 available, but there's a start at https://github.com/Rob1Ham/btc-lean/pull/= 29 that might be possible=20 to extend substantially. For lack of a more formal approach to C++, it is u= sing a proof system based=20 on equivalence of LLVM IR. Matt On 10/19/26 12:33 PM, Keagan McClelland wrote: > > Originally published on my site=20 > . Replicating here=20 > because I think the Delving audience has an interest in this work. > > -------------------------------------------------------------------------= --------------------------- > > From the project=E2=80=99s inception until now, btc-verified=20 > =C2=A0has been focused on b= uilding up, layer by layer, a=20 > very minimal model of consensus. Last month=E2=80=99s post=20 > =C2=A0talked about=20 > how we can discover hidden subtleties in how something works when we try = to formalize it. However,=20 > even as we formalize things we have to resist the temptation to merely as= sume that the precise map=20 > we have created actually reflects the reality on the ground. This month, = however, I decided to=20 > take a stab at anchoring this model to the Bitcoin network as it exists i= n the real world. > > It=E2=80=99s tricky to do this type of thing because it forces us to ask = the question how do we know the=20 > 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=20 > software in a verifiable language, compile that down to code that actuall= y runs on silicon and be=20 > on your merry way. Alternatively, if the code you=E2=80=99re trying to ve= rify is pure C code, there are=20 > ways to verify the C code directly =C2=A0since C=E2=80=99s=20 > operational semantics are small enough to reason somewhat efficiently abo= ut. > > The problem here is that Bitcoin Core , which on a practical=20 > level /defines/=C2=A0the Bitcoin protocol, is neither written in a verifi= able language, nor is it=20 > written in pure C. Rather, it is written in modern C++ so verifying it di= rectly, while possible on=20 > 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 diff= er from Bitcoin Core in=20 > any observable way with respect to its protocol semantics. Hypothetically= , if we were able to come=20 > up with an implementation of the protocol in Lean =C2=A0that had no differences=20 > in behavior from Bitcoin Core, it would mean that the model, in a sense, = IS Bitcoin Core. If the=20 > 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 e= nough to build something=20 > around. What constitutes a behavior? How can we observe the behavior? How= can we tell if it=E2=80=99s=20 > different or not? What things are implementation details and what things = are essential semantics? > > People have been trying for years to extract out Bitcoin consensus from t= he rest of Bitcoin Core=20 > and the most recent label for this effort is the libbitcoinkernel project= =20 > . This carves out a chunk of Core inside= of which is the=20 > consensus verification code and outside of which we can safely write all = kinds of custom=20 > implementation experiments without compromising the safety of consensus. = The original purpose of=20 > this project is actually to reduce the usage of non-Core implementations = of consensus. However, it=20 > also gives us a natural entry point for our purposes here. > > To do this carve out, libbitcoinkernel must define an interface that pres= erves the essential=20 > invariants of consensus and for it to be usable, its interface must give = us the ability to know=20 > whether something is consensus valid or not. > > What I have decided to do is to take advantage of the existence of this i= nterface and ensure that=20 > btc-verified can serve as the implementation behind it. We are not doing = this to encourage people=20 > to run btc-verified=E2=80=99s consensus instead of Bitcoin Core=E2=80=99s= . We are doing this to set up a benchmark=20 > of btc-verified=E2=80=99s faithfulness of matching Core=E2=80=99s behavio= r on the faultline that has already been=20 > drawn by the Bitcoin Core team. > > Once we have established a trivial implementation of libbitcoinkernel=E2= =80=99s interface in the=20 > btc-verified project, then we can take advantage of another technique tha= t has an established=20 > practice in the space: differential fuzzing. > > bitcoinfuzz =C2=A0is a projec= t whose aim is differential=20 > fuzzing of different bitcoin implementations. The idea here is that we sp= ew entropy at the kernel=20 > interface and ensure that for any given payload that Core=E2=80=99s kerne= l and btc-verified=E2=80=99s kernel=20 > 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 numerou= s bugs in different=20 > implementations=20 > =C2=A0using=20 > this strategy. Indeed, short of proofs, the best we can do to establish e= quality is to do=20 > high-entropy sampling of the behavior of each implementation and ensure t= hey never diverge. > > Of course, you never know if the next sample you take is the one that rev= eals a difference. This=20 > is the exact reason that formal verification even has a place, because yo= u cannot establish=20 > universal laws through sampling alone, but it does have a practical benef= it of reducing the=20 > probability of divergent behavior the more that the sample space saturate= s the control flow graph. > > Following this thread, I put together a standalone differential fuzzing h= arness=20 > =C2=A0for=20 > Bitcoin Core and btc-verified, specifically against the kernel interface,= and we have nine of the=20 > kernel functions=20 > =C2=A0backed=20 > by a Lean implementation. These functions cover transaction creation, cop= ying, serialization,=20 > checking, and the associated validation-state objects. The harness is bui= lt directly on libFuzzer=20 > . It gives the same transaction byt= es to Core and=20 > btc-verified, then compares their observable behavior. > > As of right now btc-verified does not implement the entire kernel interfa= ce even trivially, but it=20 > does implement a subset of it with apparently correct semantics for the f= ollowing behaviors: > > * Parsing:=C2=A0Given identical bytes, do both implementations accept t= hem as a transaction object? > This is distinct from accepting the transaction as valid. > * Serialization: For accepted inputs, do both report the same serializa= tion status and produce > exactly the same bytes? > * Transaction-local checking:=C2=A0Do they agree on the verdict for rul= es concerning input/output > presence, duplicate or null input references, output-value and stripp= ed-size limits, and the > special coinbase conditions? These checks don=E2=80=99t consult the U= TXO set or execute scripts. > * Reported validation state:=C2=A0Do they return the same validation mo= de and result category, beyond > merely agreeing on acceptance or rejection? > * State reuse: After checking a known-invalid transaction, does checkin= g the next transaction > replace that previous result consistently=E2=80=94including clearing = the invalid state when the next > transaction passes? > > As of this writing these behaviors are identical between btc-verified and= Bitcoin Core when=20 > observed over this battery: > > * 100,000 fuzz executions: this measures how many attempts for disagree= ment were made. Each > execution feeds one byte sequence into the differential harness, whic= h runs both > implementations and compares their observations. This measures testin= g volume. It doesn=E2=80=99t > count unique transactions: inputs can repeat, and malformed inputs ma= y be rejected during > parsing without reaching transaction checking. Mutations are also rel= ated to earlier inputs, > rather than independent random samples. > * 11 regression inputs:=C2=A0this measures how many pre-determined case= s are explicitly replayed. > These ensure particular cases are checked every time, regardless of w= hat 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 legacy and SegWit transactions, malformed encodings, a t= ransaction that parses > but fails checking, and three transactions immediately below, at, and= above the million-byte > stripped-size boundary. Those large cases matter because the mutation= campaign=E2=80=99s 4,096-byte > limit prevents it from discovering them. > * 264 retained corpus inputs:=C2=A0this was the size of the working cor= pus at the end of the October > 18 CI run > . > LibFuzzer keeps inputs that contribute useful coverage feedback and u= ses them as starting > points for further mutations. The final corpus count describes that w= orking collection, > including retained starting seeds. > > This differential test additionally runs as a CI check=20 > =C2=A0before=20 > new code is merged allowing observed disagreement with Core to block chan= ges to the code. > > There is a ton of work still to do to strengthen the link between btc-ver= ified and Bitcoin Core=20 > but assuming we can establish a credible link between them it allows us t= o borrow some of the=20 > theorems and findings we can establish natively in btc-verified and use t= hem to make statements=20 > about Bitcoin Core=E2=80=99s behavior. > > Over the coming month the plan is to push forwards on filling out the res= t of the kernel interface=20 > so we can officially connect this map to this territory, at least tenuous= ly for now, before=20 > pushing forwards on analyzing the map itself. > > > Godspeed, > > Keags > > --=20 > You received this message because you are subscribed to the Google Groups= "Bitcoin Development=20 > Mailing List" group. > To unsubscribe from this group and stop receiving emails from it, send an= email to=20 > bitcoindev+unsubscribe@googlegroups.com. > To view this discussion visit=20 > https://groups.google.com/d/msgid/bitcoindev/CALeFGL04_h6212x9D0u7-uJSyDD= Ayie-cohBazYS3Yo9P36NVA%40mail.gmail.com=20 > . --=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/= 8bfb3bbc-0682-49c8-b461-676aa619688e%40mattcorallo.com. --------------uoPaKCdvbL0LJlH90DYe4IIo Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Figured you might find this interesting,

Last week Rob had some tokens to spend so I asked him to see whether any progress could be made on formal equivalence proofs of script engines. The agents didn't make much progress with the tokens available, but there's a start at https://github.com/Rob1Ham/btc-lean/pull/29 that mig= ht be possible to extend substantially. For lack of a more formal approach to C++, it is using a proof system based on equivalence of LLVM IR.

Matt

On 10/19/26 12:33 PM, Keagan McClelland wrote:

Originally published=C2=A0on 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,=C2=A0btc-verified=C2=A0has been focused= on building up, layer by layer, a very minimal model of consensus.=C2=A0Last month=E2=80=99s post=C2=A0tal= ked 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 the 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 tryi= ng to verify is pure C code, there are ways to=C2=A0verify the C code directly=C2=A0si= nce C=E2=80=99s operational semantics are small enough to reason some= what efficiently about.

The problem here is that=C2=A0Bitcoin Core, which on a practical level=C2=A0defines=C2=A0the 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=C2=A0Lean=C2=A0that 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? What things are implementation det= ails 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=C2=A0libbitcoinkernel 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 be= havior 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=C2=A0is a project whos= e 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 kernel report th= e same result, including any state changes that are made by the operation executed.

bitcoinfuzz already has an established track record and has=C2=A0found numerous bugs in different implementations=C2=A0using 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=C2=A0standalone differential fuzzing harness=C2=A0for Bitcoin Core and btc-verified, specificall= y against the kernel interface, and we have=C2=A0nine of the kernel functions=C2=A0= 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=C2=A0<= a href=3D"https://llvm.org/docs/LibFuzzer.html" rel=3D"noopener nofollow ugc" style=3D"background-color:rgba(0,0,0,0);color:rgb(0,136,204);text-decoratio= n-line:initial;text-decoration-color:rgb(0,136,204)" moz-do-not-send=3D"true">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:=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 inputs, do both report the same serialization status and produce exactly the same bytes?
  • Transaction-local checking:=C2=A0Do 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 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 an= d 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=94including clearing the invalid stat= e 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 unique 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:=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 inp= ut previously exposed a bug. The ones here include real legacy 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 the mutation campaign=E2=80=99s 4,096-byte limit prevents it from discoverin= g them.
  • 264 retained corpus inputs:=C2=A0this was the size of the working corpus a= t the end of the=C2=A0October 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=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 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

--
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/bitcoind= ev/CALeFGL04_h6212x9D0u7-uJSyDDAyie-cohBazYS3Yo9P36NVA%40mail.gmail.com= .

--
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/bitcoindev= /8bfb3bbc-0682-49c8-b461-676aa619688e%40mattcorallo.com.
--------------uoPaKCdvbL0LJlH90DYe4IIo--