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