From mboxrd@z Thu Jan 1 00:00:00 1970 Delivery-date: Sun, 19 Apr 2026 11:21:26 -0700 Received: from mail-oa1-f55.google.com ([209.85.160.55]) by mail.fairlystable.org with esmtps (TLS1.3) tls TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 (Exim 4.94.2) (envelope-from ) id 1wEWlp-0007Pu-E3 for bitcoindev@gnusha.org; Sun, 19 Apr 2026 11:21:26 -0700 Received: by mail-oa1-f55.google.com with SMTP id 586e51a60fabf-40a4d2264absf3218853fac.2 for ; Sun, 19 Apr 2026 11:21:25 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20251104; t=1776622879; x=1777227679; darn=gnusha.org; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:reply-to: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=c62oyMFhDzTqHXnyXlyEVv/R/ZxjFJL4xiCORUv2xCc=; b=JEHolaMskC5kdqAWDLqg1UJkkIr59UQH685O+vA5pzfHH/UOAx/zgfivPUEqFW3KUp YfrOxKqV5LAsXNwnNTFfWw4guFrMcqyAXRCe4Veto7s1HoWrFydUuZ/QDOJOCb/RvVRK Nehj5UhcKR/xIWssFLxsP9W8mkctA0LyRD/0oQDgqPn8k1efex44plUqcIHnk6oxE0gT qQXK9gKb0YV50luqLYjDNoXfUBy9AxafzNt0FgBHxhoxHrhpeRnAXAQstPkt+LAJkt9q PgNUsjo2tXZXQgAKKosNORsWZi49phbrcKd08n7rpTKt6ixefd35kHt+4HJNMWxJbzTx AWyA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1776622879; x=1777227679; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:reply-to:x-original-sender :mime-version:subject:references:in-reply-to:message-id:to:from:date :x-beenthere:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=c62oyMFhDzTqHXnyXlyEVv/R/ZxjFJL4xiCORUv2xCc=; b=XSLWG2wRcgy/MvWRllpT+jnM8zU/hCb9K6s2C4iNU8g1Q1Yu7qvX2TyN/C9a+vHeVJ iYhhHBVEJieFkMz+kzo+39NSNmBsiDarOybNrl2qOYhMezCyL5zpa1KV9NqZmdmfOzRD vd6UdtzqguwH6YZWhPz22P/IgI10G6RTgU83ok8YOSbeu6PUv2Fc02SdTbULnGlBNB0y 3Pd4klJWsVNskrzxxldYMj3OQ3s7r+mwA97UG6ZNvyzyfZecPlCktIXVpRioHOpBvDRL rokqoMwqPJoWtMcEOkDAhke8UXXM+QbpdTlhW5f46x1DeGf8btNMB4RmVUd1hb1ncWSJ E5GA== X-Forwarded-Encrypted: i=1; AFNElJ/mZljA7Mn4IUpzX1f76xvVl0/M2I8T6y2qg4S2Qwgr/EPnOw5THgenyopiWX7AI82fILiZpIgF4OyD@gnusha.org X-Gm-Message-State: AOJu0Yzg+wAtMaQj/9HmhsHla66fl9yJq9cvBrYHQtmAo5rJ7Dh4kZA9 bi6BGtfMWvB7zYXq0kSGydQCp9JPnnS4DlH+GbOFX4OGuE/eT3GpJ5In X-Received: by 2002:a05:6871:2ec2:b0:409:6862:aba5 with SMTP id 586e51a60fabf-42adecd0b41mr6416037fac.25.1776622879072; Sun, 19 Apr 2026 11:21:19 -0700 (PDT) X-BeenThere: bitcoindev@googlegroups.com; h="AYAyTiJLxG4fdYfCvCSOzutjY6lnsUyKpReBdCY5agGPoOuJ3Q==" Received: by 2002:a05:6870:2885:b0:423:8f08:b687 with SMTP id 586e51a60fabf-4280c6b8961ls1383072fac.2.-pod-prod-00-us; Sun, 19 Apr 2026 11:21:13 -0700 (PDT) X-Received: by 2002:a05:6808:3a06:b0:45f:103c:2483 with SMTP id 5614622812f47-4799c05e9d1mr5076189b6e.23.1776622873812; Sun, 19 Apr 2026 11:21:13 -0700 (PDT) Received: by 2002:a05:690c:920d:b0:7b3:13f7:5f3a with SMTP id 00721157ae682-7b9ed96da01ms7b3; Sun, 19 Apr 2026 11:18:11 -0700 (PDT) X-Received: by 2002:a05:690c:83:b0:7ba:ded4:df69 with SMTP id 00721157ae682-7baded4e93fmr40434037b3.1.1776622689972; Sun, 19 Apr 2026 11:18:09 -0700 (PDT) Date: Sun, 19 Apr 2026 11:18:09 -0700 (PDT) From: "'Toby Sharp' via Bitcoin Development Mailing List" To: Bitcoin Development Mailing List Message-Id: In-Reply-To: <000d01dccfa1$4e927e60$ebb77b20$@voskuil.org> References: <4cd864f3-96dd-4058-bfcd-b1bbf6cfa269n@googlegroups.com> <006501dccd36$ea035fd0$be0a1f70$@voskuil.org> <00b401dccf78$6f5e7a00$4e1b6e00$@voskuil.org> <--C53DoYZLFJgwz6T6jBLFNjx3dNCZRC06RK981Cj40XsyFGNMf2pX7eiUpG-hzsMXnEIxFFyEWjost7GyuM3xKkvpqj99ODyTQprnl-N1g=@hornetnode.org> <000d01dccfa1$4e927e60$ebb77b20$@voskuil.org> Subject: Re: RE: [bitcoindev] Hornet Update: A declarative executable specification of Bitcoin consensus rules MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_265554_406989032.1776622689474" X-Original-Sender: toby.sharp%hotmail.com@gtempaccount.com X-Original-From: Toby Sharp Reply-To: Toby Sharp 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 (-) ------=_Part_265554_406989032.1776622689474 Content-Type: multipart/alternative; boundary="----=_Part_265555_1319787265.1776622689474" ------=_Part_265555_1319787265.1776622689474 Content-Type: text/plain; charset="UTF-8" A couple of clarifications: > the query itself is not subject to verification. There is no formal verification here: that is not the claim. The claim is that the given set of semantic rules are logically necessary and sufficient to specify block validity. > The whole point is verifying implementation correctness. Calling it out of scope doesn't really solve the problem. It is not the point of this post; it is a set of larger goals that requires multiple preceding steps, of which this is one. Correctness can't be established if there is no description of what the correct behavior is. Any attempt at verification requires to first *separate intention from implementation*. That is what a semantic spec is for. Re the Hornet code enforcing spend ordering in a block, this is captured by S02, reworded for clarity to "MUST reference a preceding transaction output that remains unspent". That semantic rule is validated by the consensus function ValidateInputPrevoutsUnspent, which delegates to an abstract interface method UnspentOutputsView::QueryPrevoutsUnspent, whose contract respects the same semantics. Then Hornet's UTXO engine fulfills that interface contract on the data-layer side of the abstraction boundary. The behavior is by design to meet the semantic rule, and not a lurking side-effect. One could argue that S02 actually contains two semantic invariants: one regarding the ordering constraint, and one regarding the double-spend constraint. I'll give that some further consideration. I appreciate the engagement, and your historical examples are useful context for the road ahead. Best wishes, T# On Saturday, 18 April 2026 at 19:11:19 UTC-7 er...@voskuil.org wrote: > > > It appears that Hornet is missing the rule prohibiting forward > references > > within a block. > > > > This is implied by Rule S02: "A transaction input MUST reference a > previous > > transaction output that remains unspent." However, to make it clearer, I > will > > rewrite it as: > > > > "S02: A transaction input MUST reference a preceding transaction output > that > > remains unspent." > > As I understand it, the rule in question: > > // Returns success if every spending input in this block references an > existing unspent output. > consensus::Result QueryPrevoutsUnspent(const protocol::Block& block) const > override { > Assert(&block == joiner_->GetBlock().get()); > if (!joiner_->WaitForQuery()) return > consensus::Error::Spending_PrevoutNotUnspent; > return {}; > } > > can only fail if the query fails, and the query itself is not subject to > verification. In this case the consensus rule is implemented as a side > effect of the query (as it is in bitcoind), and the query itself is not > subject to verification. I would consider this a missing rule from the > perspective of verification. It is true that the store must provide > fidelity in any case (what goes in must come out). That alone presents > significant issues for verification. But at least it's straightforward to > define. But in this case the query is not just returning outputs that have > been stored in the block total ordering. > > The query is constructing a temporary map, accumulating block-internal > spends into that map in a specific order, populating the results, and > effectively enforcing the forward reference constraint as side effect of > the population implementation. These outputs are not placed into the utxo > store until after the block is validated. In other words, the consensus > rule is evaluated entirely within the scope of the query; it is not a > consequence of simple store fidelity, and is not a consequence of a > verified rule. It's lurking in an unverified query. If another > implementation was to populate prevouts differently (e.g., in parallel), > and with full fidelity, the ordering constraint easily disappears and is > not caught by verification. This has happened, and IIRC resulted in the > loss of a block by a miner. This is the type of consensus break that > verification presumes to preclude. > > > > Otherwise there are potential malleation issues to deal with depending > on > > how blocks/headers are being managed. This can affect consensus behavior > > (via archival) while not showing up as an issue in these rules. > > > > That would be an implementation correctness detail rather than part of a > > declarative spec. > > > > The intention here is to specify what must be true for consensus > validity rather > > than how it should be computed. > > The whole point is verifying implementation correctness. Calling it out of > scope doesn't really solve the problem. Merkle root malleation has resulted > in consensus failure (bitcoin core). Transaction deserialization has > resulted in consensus failure (btcd). Store infidelity has resulted in > consensus failure (bitcoind). Cryptographic library bugs have produced > consensus bugs that were preemptively patched (openssl). These types of > issues are more common in modern history than what one might consider > "rules". The so-called rules are actually much easier to deal with. > > Airing out some of these real difficulties has been worthwhile. In my > experience people have an overly optimistic view of what can be achieved by > both formal verification and the attempt to create a shared script > implementation. I'm hopeful, but I also try to stay grounded. I'll give > further responses offline. > > Best, > Eric > > https://nvd.nist.gov/vuln/detail/CVE-2022-39389 > https://nvd.nist.gov/vuln/detail/CVE-2012-2459 > https://nvd.nist.gov/vuln/detail/CVE-2013-3220 > > -- 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/a673244b-c76b-40c7-bad3-6afa2cac18e7n%40googlegroups.com. ------=_Part_265555_1319787265.1776622689474 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable A couple of clarifications:

> the query itself is not subject= to verification.

There is no formal verification here: that is = not the claim. The claim is that the given set of semantic rules are logica= lly necessary and sufficient to specify block validity.

> The= whole point is verifying implementation correctness. Calling it out of sco= pe doesn't really solve the problem.

It is not the point of this= post; it is a set of larger goals that requires multiple preceding steps, = of which this is one. Correctness can't be established if there is no descr= iption of what the correct behavior is. Any attempt at verification require= s to first *separate intention from implementation*. That is what a semanti= c spec is for.

Re the Hornet code enforcing spend ordering in a = block, this is captured by S02, reworded for clarity to "MUST reference a p= receding transaction output that remains unspent". That semantic rule is va= lidated by the consensus function ValidateInputPrevoutsUnspent, which deleg= ates to an abstract interface method UnspentOutputsView::QueryPrevoutsUnspe= nt, whose contract respects the same semantics. Then Hornet's UTXO engine f= ulfills that interface contract on the data-layer side of the abstraction b= oundary. The behavior is by design to meet the semantic rule, and not a lur= king side-effect.

One could argue that S02 actually contains tw= o semantic invariants: one regarding the ordering constraint, and one regar= ding the double-spend constraint. I'll give that some further consideration= .

I appreciate the engagement, and your historical examples are = useful context for the road ahead.

Best wishes,
T#
On Saturday, 18 Ap= ril 2026 at 19:11:19 UTC-7 er...@voskuil.org wrote:
> > It appears that Hornet is = missing the rule prohibiting forward references
> within a block.
>=20
> This is implied by Rule S02: "A transaction input MUST refere= nce a previous
> transaction output that remains unspent." However, to make it= clearer, I will
> rewrite it as:
>=20
> "S02: A transaction input MUST reference a preceding transact= ion output that
> remains unspent."

As I understand it, the rule in question:

// Returns success if every spending input in this block references a= n existing unspent output.
consensus::Result QueryPrevoutsUnspent(const protocol::Block& blo= ck) const override {
Assert(&block =3D=3D joiner_->GetBlock().get());
if (!joiner_->WaitForQuery()) return consensus::Error::Spending_= PrevoutNotUnspent;
return {};
}
=20
can only fail if the query fails, and the query itself is not subject t= o verification. In this case the consensus rule is implemented as a side ef= fect of the query (as it is in bitcoind), and the query itself is not subje= ct to verification. I would consider this a missing rule from the perspecti= ve of verification. It is true that the store must provide fidelity in any = case (what goes in must come out). That alone presents significant issues f= or verification. But at least it's straightforward to define. But in th= is case the query is not just returning outputs that have been stored in th= e block total ordering.

The query is constructing a temporary map, accumulating block-internal = spends into that map in a specific order, populating the results, and effec= tively enforcing the forward reference constraint as side effect of the pop= ulation implementation. These outputs are not placed into the utxo store un= til after the block is validated. In other words, the consensus rule is eva= luated entirely within the scope of the query; it is not a consequence of s= imple store fidelity, and is not a consequence of a verified rule. It's= lurking in an unverified query. If another implementation was to populate = prevouts differently (e.g., in parallel), and with full fidelity, the order= ing constraint easily disappears and is not caught by verification. This ha= s happened, and IIRC resulted in the loss of a block by a miner. This is th= e type of consensus break that verification presumes to preclude.

> > Otherwise there are potential malleation issues to deal with = depending on
> how blocks/headers are being managed. This can affect consensus be= havior
> (via archival) while not showing up as an issue in these rules.
>=20
> That would be an implementation correctness detail rather than par= t of a
> declarative spec.
>=20
> The intention here is to specify what must be true for consensus v= alidity rather
> than how it should be computed.

The whole point is verifying implementation correctness. Calling it out= of scope doesn't really solve the problem. Merkle root malleation has = resulted in consensus failure (bitcoin core). Transaction deserialization h= as resulted in consensus failure (btcd). Store infidelity has resulted in c= onsensus failure (bitcoind). Cryptographic library bugs have produced conse= nsus bugs that were preemptively patched (openssl). These types of issues a= re more common in modern history than what one might consider "rules&q= uot;. The so-called rules are actually much easier to deal with.

Airing out some of these real difficulties has been worthwhile. In my e= xperience people have an overly optimistic view of what can be achieved by = both formal verification and the attempt to create a shared script implemen= tation. I'm hopeful, but I also try to stay grounded. I'll give fur= ther responses offline.

Best,
Eric

https://nvd.nist.gov/vuln/detail/CVE-2022-39389
https://nvd.nist.gov/vuln/detail/CVE-2012-2459
https://nvd.nist.gov/vuln/detail/CVE-2013-3220

--
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/a673244b-c76b-40c7-bad3-6afa2cac18e7n%40googlegroups.com.
------=_Part_265555_1319787265.1776622689474-- ------=_Part_265554_406989032.1776622689474--