From: "'Toby Sharp' via Bitcoin Development Mailing List" <bitcoindev@googlegroups.com>
To: Bitcoin Development Mailing List <bitcoindev@googlegroups.com>
Subject: [bitcoindev] Hornet Update: A declarative executable specification of Bitcoin consensus rules
Date: Wed, 15 Apr 2026 15:42:45 -0700 (PDT) [thread overview]
Message-ID: <4cd864f3-96dd-4058-bfcd-b1bbf6cfa269n@googlegroups.com> (raw)
[-- Attachment #1.1: Type: text/plain, Size: 7885 bytes --]
In September 2025, I published a paper on my work towards a pure, formal
specification of Bitcoin's consensus rules.
> Hornet Node and the Hornet DSL: A minimal, executable specification of
Bitcoin consensus. T Sharp, September 2025.
https://hornetnode.org/paper.html
I have now completed the C++ executable declarative specification for
non-script block validation rules: 34 semantic invariants in total.
## Background
Hornet is a minimal, executable specification of Bitcoin's consensus rules,
expressed both in declarative C++ and in a purpose-built domain-specific
functional language.
It is implemented as a suite of modular, dependency-free, modern C++
libraries and includes a lightweight node capable of Initial Block Download
(IBD).
Hornet's concurrent, lock-free UTXO(1) engine achieves an 11× validation
speedup over Bitcoin Core on full-chain replay (discussed in Bitcoin Optech
Newsletter #391). All consensus logic is encapsulated by the declarative
specification described below.
## Update 2026-04-15
The question of whether a block is valid or invalid can -- and should -- be
expressed as a Boolean, pure function without state changes or side effects.
Hornet aims to specify this logic declaratively and semantically, both in
C++ and in a functional domain-specific language.
I have now completed the set of non-script block validation rules,
organized with one semantic invariant per rule, with a total of 34 rules
composed via a simple algebra. The first 15 rules are shown below.
```cpp
// BLOCK VALIDITY SPECIFICATION
static constexpr auto kConsensusRules = All{
With{MakeHeaderContext, All{ // ## Header Rules
Rule{ValidatePreviousHash}, // A header MUST reference
the hash of a valid parent block.
Rule{ValidateProofOfWork}, // A header's hash MUST
achieve its own proof-of-work target.
Rule{ValidateDifficultyAdjustment}, // A header's proof-of-work
target MUST satisfy the difficulty adjustment formula for the timechain.
Rule{ValidateMedianTimePast}, // A header timestamp MUST be
strictly greater than the median of its 11 ancestors' timestamps.
Rule{ValidateTimestampCurrent}, // A header timestamp MUST be
less than or equal to network-adjusted time plus 2 hours.
Rule{ValidateVersion} // A header's version number
MUST NOT have been retired by any activated soft fork.
}},
With{MakeEnvironmentContext, All{ All{ // ## Local Rules
Rule{ValidateNonEmpty}, // A block MUST contain at
least one transaction.
Rule{ValidateMerkleRoot}, // A block’s Merkle root
field MUST equal the unique Merkle root of its transactions.
Rule{ValidateOriginalSizeLimit}, // A block’s serialized size
excluding witness flags and data MUST NOT exceed 1,000,000 bytes.
Rule{ValidateCoinbase}, // A block's first
transaction MUST be its only coinbase transaction.
Rule{ValidateSignatureOps}, // The total legacy
signature-operation count over all input and output scripts MUST NOT exceed
20,000.
Each{TransactionsInBlock{}, All{
Rule{ValidateInputCount}, // A transaction MUST contain
at least one input.
Rule{ValidateOutputCount}, // A transaction MUST contain
at least one output.
Rule{ValidateTransactionSize}, // A transaction's serialized
size excluding witness flags and data MUST NOT exceed 1,000,000 bytes.
Rule{ValidateOutputsNonNegative}, // All transaction output
amounts MUST be non-negative.
...
```
The declarative specification separates *what must be true* from *how it is
computed*. Each `Rule` line names a C++ function that validates the
specific semantic rule in question, and also gives an English description
of the rule being enforced.
The above statically-typed declarative graph is the executable
specification of the semantic invariants that precisely determine consensus
validity of a block in the Bitcoin network. Each Rule node names a
validation function that returns a unique error code if and only if that
property fails to hold.
We can parse the same code to automatically generate an English table of
the semantic rules:
| ID | Rule |
|-|-|
||**Header Rules**
H01|A header MUST reference the hash of a valid parent block.
H02|A header's hash MUST achieve its own proof-of-work target.
H03|A header's proof-of-work target MUST satisfy the difficulty adjustment
formula for the timechain.
H04|A header timestamp MUST be strictly greater than the median of its 11
ancestors' timestamps.
H05|A header timestamp MUST be less than or equal to network-adjusted time
plus 2 hours.
H06|A header's version number MUST NOT have been retired by any activated
soft fork.
||**Local Rules**
L01|A block MUST contain at least one transaction.
L02|A block’s Merkle root field MUST equal the unique Merkle root of its
transactions.
L03|A block’s serialized size excluding witness flags and data MUST NOT
exceed 1,000,000 bytes.
L04|A block's first transaction MUST be its only coinbase transaction.
L05|The total legacy signature-operation count over all input and output
scripts MUST NOT exceed 20,000.
L06|A transaction MUST contain at least one input.
L07|A transaction MUST contain at least one output.
L08|A transaction's serialized size excluding witness flags and data MUST
NOT exceed 1,000,000 bytes.
L09|All transaction output amounts MUST be non-negative.
...
For the full declarative C++ spec, see
https://github.com/tobysharp/hornet/tree/main/src/hornetlib/consensus/rules/spec.h
For the resulting semantic summary table, see
https://hornetnode.org/spec.html.
To read more about Hornet and how it relates to other projects, see
https://hornetnode.org/overview.html.
## Future work
The spending rule S06: "A non-coinbase input MUST satisfy the spent
output's locking script" is correct, but on its own clearly doesn't capture
the internal complexity of script execution. I am working towards a
separate layer of specification for script rules.
The declarative C++ specification is a step towards a pure, functional
domain-specific language for a Bitcoin consensus spec. This will be
implemented in a future iteration, together with an interpreter and/or
compiler. Here is an example of the Hornet DSL:
```
// The total number of signature operations in a block MUST NOT exceed the
consensus maximum.
Rule SigOpLimit(block ∈ Block)
Let SigOpCost : (op ∈ OpCode) -> int32
|-> ⎧ 1 if op ∈ {Op_CheckSig, Op_CheckSigVerify },
⎨ 20 if op ∈ {Op_CheckMultiSig, Op_CheckMultiSigVerify},
⎩ 0 otherwise
Require Σ SigOpCost(inst.opcode)
∀ inst ∈ script.instructions
∀ script ∈ tx.inputs.scriptSig ⧺ tx.outputs.scriptPubKey
∀ tx ∈ block.transactions
≤ 20,000
```
## Conclusion
I welcome feedback from the developer community. In particular, do you
believe there is value in a formal specification of consensus rules? Are
there any aspects of Hornet that you like or dislike? Are there any rules
that you believe are missing, redundant, unclear, or incorrect? I also
welcome any bug reports. Thank you.
T#
--
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/4cd864f3-96dd-4058-bfcd-b1bbf6cfa269n%40googlegroups.com.
[-- Attachment #1.2: Type: text/html, Size: 8643 bytes --]
next reply other threads:[~2026-04-15 22:45 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2026-04-15 22:42 'Toby Sharp' via Bitcoin Development Mailing List [this message]
2026-04-16 0:21 ` eric
2026-04-16 18:41 ` 'Toby Sharp' via Bitcoin Development Mailing List
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=4cd864f3-96dd-4058-bfcd-b1bbf6cfa269n@googlegroups.com \
--to=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