From: "'Toby Sharp' via Bitcoin Development Mailing List" <bitcoindev@googlegroups.com>
To: Bitcoin Development Mailing List <bitcoindev@googlegroups.com>
Subject: Re: RE: [bitcoindev] Hornet Update: A declarative executable specification of Bitcoin consensus rules
Date: Sun, 19 Apr 2026 11:18:09 -0700 (PDT) [thread overview]
Message-ID: <a673244b-c76b-40c7-bad3-6afa2cac18e7n@googlegroups.com> (raw)
In-Reply-To: <000d01dccfa1$4e927e60$ebb77b20$@voskuil.org>
[-- Attachment #1.1: Type: text/plain, Size: 6017 bytes --]
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.
[-- Attachment #1.2: Type: text/html, Size: 7579 bytes --]
prev parent reply other threads:[~2026-04-19 18:21 UTC|newest]
Thread overview: 7+ messages / expand[flat|nested] mbox.gz Atom feed top
2026-04-15 22:42 'Toby Sharp' via Bitcoin Development Mailing List
2026-04-16 0:21 ` eric
2026-04-16 18:41 ` 'Toby Sharp' via Bitcoin Development Mailing List
2026-04-18 21:15 ` eric
2026-04-18 22:26 ` 'Toby Sharp' via Bitcoin Development Mailing List
2026-04-19 2:07 ` eric
2026-04-19 18:18 ` 'Toby Sharp' via Bitcoin Development Mailing List [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=a673244b-c76b-40c7-bad3-6afa2cac18e7n@googlegroups.com \
--to=bitcoindev@googlegroups.com \
--cc=toby.sharp%hotmail.com@gtempaccount.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox