From: <eric@voskuil.org>
To: "'Toby Sharp'" <toby@hornetnode.org>,
"'Bitcoin Development Mailing List'"
<bitcoindev@googlegroups.com>
Subject: RE: [bitcoindev] Hornet Update: A declarative executable specification of Bitcoin consensus rules
Date: Sat, 18 Apr 2026 17:15:07 -0400 [thread overview]
Message-ID: <00b401dccf78$6f5e7a00$4e1b6e00$@voskuil.org> (raw)
In-Reply-To: <zGGdGeFp__snuJMlaMKpM0br91-R0cWc1Igwz2eTdnu6TWSO3CySfSNgmU6hL-OyJQXBG1j6tOD66Dm_Llw35T9R5N_VgP8Y9wEdqKjC9_I=@hornetnode.org>
Hi Toby,
> Thanks for your thoughtful and encouraging comments, and for sharing some
> of the libbitcoin implementation.
Of course, you as well.
> The architectural distinction I'd note is in composition. Libbitcoin isolates rules
> as predicates but composes them inside phase-specific methods as if-chains.
> This is excellent for a clean and readable node implementation. Hornet goes
> further and composes them in a static declarative graph using an algebra of
> combinators (All, With, Each).
I wouldn't call this an architectural distinction given that it can be implemented over the set of rules in a matter of minutes. The design challenge is in properly identifying and functionally isolating each rule. The block/header/tx rules are the low hanging fruit. We implemented this well over 10 years ago, so I also don't know if I would consider it convergent:
https://github.com/libbitcoin/libbitcoin-system/commit/4c6cd2874f5e0b490dc1d7c020ace52858fb1b84#diff-d80e987b7f0628275c6e7318733e70848645f499b8a33c08f66d0f65b3f64e77R399
There are maybe two orders of magnitude more work in script evaluation alone (link to one part of it previously posted). And then there is at least deserialization, storage, and chain organization - all while making this fit architecturally into performance and public interface constraints. Providing meaningful formal verification across that space is a monumental task, which is why I'm encouraged that you are taking it on. But it does seem to me that you may be underestimating it, even within Hornet's limited design target.
> On widespread use: Hornet Node today is more of an experimental client for
> validation and IBD than a fully functional node. This is by design, as the main
> target at this stage is the neutral specification
This work can eventually produce a specification. The problem however will remain faith in the correctness of the specification itself. Verification cannot reasonably be applied to existing bitcoind implementations (and there are a lot of them both in versions and in forks), and modifying them to the point where this is feasible becomes a new architecture (which is what we have done). My prior comment on "widespread use" is about this specific problem. To solve this requires two things:
(1) at least one fully consensus-verifiable node implementation.
(2) the verified implementation(s) are predominant in economic use.
Once this is the case, the rules become useful in the verification of other implementations.
> Some suggestions on collaboration might include: cross-validating libbitcoin's
> predicate set against Hornet's 34 semantic invariants to identify and resolve
> any divergence; joint review of the DSL as it develops; discussion on how we
> might verify that libbitcoin exactly implements the specification; and sharing a
> corpus of edge-case test vectors.
This all sounds reasonable. However, for us to invest limited resources it requires that the outcome be meaningful. This small subset of the problem could provide a proof of concept, which we could use to measure scope across the entire surface. At that point we could balance further work on (1) above against also achieving (2).
>> Are there any rules that you believe are missing
From my reading of rule names and descriptions here:
https://github.com/tobysharp/hornet/blob/main/src/hornetlib/consensus/rules/rules.h
It appears that Hornet is missing the rule prohibiting forward references within a block.
https://github.com/libbitcoin/libbitcoin-system/blob/master/src/chain/block.cpp#L397-L417
This is a partial ordering constraint (is_forward_reference) that's easy to miss because it's just a bitcoind implementation artifact. By isolating this behavior to its own rule, not only does it not get missed, but rule evaluation also becomes order independent and therefore parallelizable.
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. There is also the rule prohibiting double spends, which can invalidate a context-free block (is_internal_double_spend), which would otherwise not be caught until contextual checks (so is more of an optimization and malleation guard).
https://github.com/libbitcoin/libbitcoin-system/blob/master/src/chain/block.cpp#L422-L434
We avoid applying redundant rules except in the case of unconfirmed tx validation, as it becomes necessary for DoS protection. But we label these as "guards" not "rules". In this case the rules are block-level but must be evaluated when accepting unconfirmed txs. The above is_internal_double_spend rule is a bit of an exception but it's context free, legitimately detects invalidity, precludes a type of malleation, and short-circuits a later more comprehensive/costly check.
Best,
Eric
--
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/00b401dccf78%246f5e7a00%244e1b6e00%24%40voskuil.org.
next prev parent reply other threads:[~2026-04-18 21:49 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 [this message]
2026-04-18 22:26 ` 'Toby Sharp' via Bitcoin Development Mailing List
2026-04-19 2:07 ` eric
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='00b401dccf78$6f5e7a00$4e1b6e00$@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