Skip to content

binana: simplicity #22

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
delta1 wants to merge 1 commit into
base: master
Choose a base branch
from
Open

binana: simplicity #22

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
272 changes: 272 additions & 0 deletions 2026/BIN-2026-0003.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,272 @@
| BIN-2026-0003 | `SIMPLICITY`
| :------------ | :-------
| Revision | 000 (2026-06-08)
| Author | Byron Hambly `<bhambly@blockstream.com>`
| |
| Layer | Consensus (soft fork)
| Status | Draft
| License | BSD-3-CLAUSE
| |
| Discussion | https://delvingbitcoin.org/t/delving-simplicity-part-three-fundamental-ways-of-combining-computations/1902
| Aliases | n/a

## Abstract

This document introduces **TapSimplicity**, a new taproot leaf version that enables
[Simplicity](https://blockstream.com/simplicity.pdf) programs to be used in place of
Bitcoin script.

Simplicity is a typed, combinator-based, functional language without loops or recursion.

Simplicity has formal denotational semantics defined in Coq, and operational semantics
defined with an abstract machine we call the Bit Machine. Simplicity is amenable to
static analysis, capable of deriving upper bounds on required computational resources
before execution. Even though Simplicity is Turing incomplete, it can express any
finitary function.

Simplicity was designed by Russell O'Connor at Blockstream Research, and has been live
on [Liquid](https://liquid.net) since July 2025.

## Motivation

Since Taproot activation in November 2021, no soft fork adding new script functionality
has achieved sufficient consensus to be deployed on Bitcoin mainnet. Numerous proposals
have each been the subject of years of review and debate, each
demonstrating useful functionality that Script's limited, ad hoc instruction set cannot
otherwise express. Yet each must independently attempt to find consensus, while being too
narrowly scoped for some to commit to a deployment.

Simplicity takes a different approach: rather than adding opcodes one at a time, it
provides a small, fixed set of combinators with formal denotational semantics, machine
checked in Coq, from which any finitary function can be built. Once this general-purpose
foundation is in consensus, functionality that would otherwise require a new opcode and
a new soft fork can typically be expressed directly as a Simplicity program — or
accelerated via jets, verified native implementations of common sub-expressions, without
any further change to consensus rules. This turns the slow, recurring cycle of
opcode-by-opcode soft forks into a one-time investment in an audited, general-purpose
new script interpreter.

Since Simplicity has no loops or unbounded recursion, the computation and memory cost
of any program can be statically bounded before execution. This removes the need for
ad hoc, per-opcode cost accounting and closes off the resource-exhaustion concerns that
have made past interpreter changes contentious. Combined with its machine-checked
semantics, this makes Simplicity programs far more amenable to formal analysis,
tooling, and reasoning about correctness than hand-written Script.

Simplicity has been running in production on the
Liquid sidechain since July 2025, giving it a track record of real-world usage,
implementation experience, and tooling. TapSimplicity brings this same, audited
language to Bitcoin by defining a new taproot leaf version following the upgrade path
established by BIP-341 and BIP-342, allowing Simplicity programs to authorise spends
alongside ordinary Tapscript without disturbing any existing consensus rules.

Deploying TapSimplicity on a Bitcoin Inquisition signet offers a venue to
exercise this integration on Bitcoin: wallets, miners, and full nodes can gain
hands-on experience constructing, relaying, and validating Simplicity-secured spends,
the budget and padding rules can be stress-tested under realistic conditions, and the
wider community can build confidence in the design ahead of any discussion of mainnet
activation.

## Specification

### Definitions

The following terms are used:

- **Script:** The 32-byte script field of a taproot leaf, which for TapSimplicity
contains the CMR.
- **CMR:** The Commitment Merkle Root of the Simplicity program, a 32-byte value.
- **TapSimplicity leaf:** A taproot leaf with leaf version `0xbe`.
- **Simplicity program bytes:** The serialised Simplicity DAG.
- **Simplicity witness bytes:** The serialised witness values consumed by `witness`
nodes in the DAG.
- **Jet:** A verified native implementation of a common Simplicity sub-expression,
identified by its CMR, that may be executed in place of the sub-expression it
represents without altering semantics or consensus meaning.
- **Padding:** An optional stack item of zero bytes used to adjust the validation budget.
- **Budget:** The maximum allowed execution cost, a non-negative integer measured in
abstract weight units.
- **minCost:** The minimum execution cost that the program must consume, used to
enforce padding minimality.
- **`GetSerializeSize(stack)`:** The total byte length of the serialised witness stack,
including the compact-size length prefix for each item.

### TapSimplicity Leaf Version

A taproot leaf version is identified by applying the Taproot leaf mask `0xfe` to the first byte of the
control block. TapSimplicity uses leaf version `0xbe`:

```
TAPROOT_LEAF_MASK = 0xfe
TAPROOT_LEAF_TAPSCRIPT = 0xc0 (BIP-342)
TAPROOT_LEAF_TAPSIMPLICITY = 0xbe (this spec)
```

### Script Field

For a TapSimplicity leaf, the script field **must** be exactly 32 bytes. This field is
the CMR of the Simplicity program that authorises spending.

If the script field is not exactly 32 bytes, the script path spend is invalid.

### Witness Stack Format

After the standard taproot witness processing defined in BIP-341 (removal of an
optional annex, removal of the control block, removal of the script), the remaining
witness stack items are interpreted as follows.

The remaining stack **must** contain exactly 2 or 3 items. Any other count is
invalid.

Items are consumed from the top of the stack (last item first):

1. **`simplicity_program`** (top of remaining stack): The serialised Simplicity DAG.
There is no length constraint beyond what is imposed by the validation budget.

2. **`simplicity_witness`** (next item): The serialised witness values for all
`witness` nodes in the DAG, in a canonical order defined by the Simplicity
specification.

3. **`padding`** (bottom item, optional): If a third item is present, it **must**
consist entirely of zero bytes. It **must** be minimal: the same budget would not
be achievable with one fewer byte of padding (see Budget Calculation below).

Visually, the full witness stack for a TapSimplicity spend without padding is:

```
index item
───── ────────────────────────────────────
0 simplicity_witness
1 simplicity_program
2 script (32-byte CMR) ← popped as taproot script
3 control_block ← popped as taproot control block
[annex] ← popped if present (optional, index 4 or 3)
```

With optional padding:

```
index item
───── ────────────────────────────────────
0 padding (n bytes, all 0x00)
1 simplicity_witness
2 simplicity_program
3 script (32-byte CMR)
4 control_block
[annex] ← optional
```

### Budget Calculation

The validation budget is computed from the **full** witness stack (all items,
including control block, script, program, witness, and optional padding) before
any items are removed:

```
VALIDATION_WEIGHT_OFFSET = 50

budget = GetSerializeSize(witness.stack) + VALIDATION_WEIGHT_OFFSET
```

`GetSerializeSize` returns the byte length of the witness stack as it appears on the
wire, including compact-size integer prefixes for each item and for the item count.

#### Padding minimality

When padding is present with byte length `n`:

```
size_n = GetSerializeSize(n-byte zero item)
size_n1 = GetSerializeSize((n−1)-byte zero item) # 0 when n = 0 (no item to reduce to)

minCost = budget − size_n + size_n1
```

For `n = 0` (empty padding item, 0 bytes), `size_n = 1` (compact-size prefix only) and
`size_n1 = 0`, so the formula gives `minCost = budget − 1`.

For `n ≥ 1`, removing one byte of padding decreases the serialised size by exactly 1 byte
(compact-size does not change until crossing a boundary), so `minCost = budget − 1` in
the common case as well.

The executor **must** reject the spend if the program's actual execution cost is less
than `minCost`. This ensures that padding cannot be used to allocate more budget than
the program requires: given the program's actual cost, the smallest valid padding
length produces a budget just sufficient for that cost.

#### Budget constraint

The executor **must** reject the spend if the program's execution cost exceeds
`budget`.

### Validation Algorithm

Given the inputs extracted from the witness stack, a TapSimplicity spend is validated
as follows:

1. **Witness stack count check.** After removing the control block and script from the
witness stack, verify that exactly 2 or 3 items remain. Fail with
`SIMPLICITY_WRONG_LENGTH` otherwise.

2. **Budget calculation.** Compute `budget` from the full (unmodified) witness stack as
described above.

3. **Padding check.** If a third item is present, pop it as the padding item. Verify
that all its bytes are `0x00`; fail with `SIMPLICITY_PADDING_NONZERO` otherwise.
Compute `minCost` from `budget` and the padding length as described above. If no
padding item is present, `minCost = 0`.

4. **Taproot environment construction.** From the control block and script:
- Extract the internal public key (bytes 1–32 of the control block).
- Extract the merkle path (remaining bytes of the control block, in 32-byte chunks).
- Record the path length `pathLen`.
- The CMR is the 32-byte script field.
- Compute `tapLeafHash`, `tappathHash`, `tapEnvHash` per the Simplicity
specification.

5. **Execution.** Pass `simplicity_program`, `simplicity_witness`, the taproot
environment, `minCost`, and `budget` to the Simplicity evaluator. The evaluator:

a. Rejects the spend if `budget` exceeds the evaluator's internal maximum allowed
value. Fail with `SIMPLICITY_OVERWEIGHT`.

b. Decodes the bitstream into a Simplicity DAG. Fail on any parse error.

c. Performs type inference. Fail if type inference fails or if the inferred type of
the root is not a valid program type.

d. Verifies that the CMR of the decoded root node matches the 32-byte script field.
Fail with `SIMPLICITY_CMR` otherwise.

e. Evaluates the program with the Bitcoin transaction environment, tracking
execution cost (computation) and memory cost (frame stack depth).
Fail if execution cost exceeds `budget` (`SIMPLICITY_EXEC_BUDGET`) or memory
exceeds its limit (`SIMPLICITY_EXEC_MEMORY`). Verify that every node in the
DAG is executed at least once (i.e. the program must be pruned); fail otherwise.
Verify that every bit of `simplicity_witness` is consumed, excluding any trailing
padding bits at the end of the witness bitstring; fail otherwise.

f. Verifies that execution cost is at least `minCost`. Fail with
`SIMPLICITY_ANTIDOS` otherwise.

g. Verification succeeds if and only if the evaluator returns without error.

## Reference Implementation

Reference implementations for Simplicity and its Bitcoin integration are here:

https://github.com/roconnor-blockstream/bitcoin/tree/simplicity

https://github.com/BlockstreamResearch/simplicity/tree/bitcoin

## Backward Compatibility

Simplicity is a soft fork. Unupgraded nodes treat leaf version `0xbe` as an unknown taproot leaf version, which succeeds unconditionally as per BIP-341.

## Acknowledgements

Simplicity was designed by Russell O'Connor at Blockstream Research, and presented at [PLAS '17](https://dl.acm.org/doi/10.1145/3139337.3139340).

## Copyright

This document is licensed under the 3-clause BSD license.