From: <eric@voskuil.org>
To: "'Toby Sharp'" <toby@hornetnode.org>,
"'Bitcoin Development Mailing List'"
<bitcoindev@googlegroups.com>
Subject: RE: RE: [bitcoindev] Hornet Update: A declarative executable specification of Bitcoin consensus rules
Date: Sat, 18 Apr 2026 22:07:42 -0400 [thread overview]
Message-ID: <000d01dccfa1$4e927e60$ebb77b20$@voskuil.org> (raw)
In-Reply-To: <--C53DoYZLFJgwz6T6jBLFNjx3dNCZRC06RK981Cj40XsyFGNMf2pX7eiUpG-hzsMXnEIxFFyEWjost7GyuM3xKkvpqj99ODyTQprnl-N1g=@hornetnode.org>
> > 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/000d01dccfa1%244e927e60%24ebb77b20%24%40voskuil.org.
prev parent reply other threads:[~2026-04-19 2:11 UTC|newest]
Thread overview: 6+ 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 [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='000d01dccfa1$4e927e60$ebb77b20$@voskuil.org' \
--to=eric@voskuil.org \
--cc=bitcoindev@googlegroups.com \
--cc=toby@hornetnode.org \
/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