Miniscript: Spending Policies You Can Reason About

In Bitcoin, spending policies are defined and enforced by means of a stack-based
programming language known as Bitcoin Script. While this language appears to
be designed with tractable analysis in mind (e.g. there are no looping or
jumping constructions), in practice this is extremely difficult. As a result,
typical wallet software supports only a small set of script templates, cannot
interoperate with other similar software, and each wallet contains
independently written ad-hoc manually verified code to handle these templates.
Users who require more complex spending policies, or who want to combine signing
infrastructure which was not explicitly designed to work together, are simply
out of luck.

In the first half of this talk we introduce Miniscript, a subset of Bitcoin
Script which eliminates the difficult-to-analyze parts of Script while retaining
sufficient expressivity to describe digital signatures, hash preimages and
timelock requirements in arbitrary combination. Using Miniscript, many
previously complex tasks become simple: determining the set of signatures
needed to satisfy a policy; encoding the satisfaction of any branch of the
policy; estimating the cost of satisfaction; determining the optimal
satisfaction when many are available. It is also possible to efficiently answer
more complex questions, such as ensuring a countersigner that his signature is
required in every branch of a complex policy, or ensuring a participant in a
swap protocol that his counterparty cannot back out of the protocol until a
timelock has expired.

In the second half of the talk, we reinterpret Miniscript not as a subset of
Script, but as a different language with an entirely different programming
paradigm. While Script (and other languages such as Ethereum's EVM) use an
``execution-centric'' paradigm in which instructions are listed and evaluated
in order, Miniscript uses a ``verification-centric'' paradigm in which coin-
spending conditions are directly described. Because Script does not have
unbounded loops, these apparently contradictory views are equivalent in a
theoretical sense. However, as we have seen, the verification-centric model
makes policies simpler to describe, use and reason about. We briefly discuss
how this model is also used in circuit-based zero-knowledge proof schemes such
as SNARKs and Bulletproofs, as well as in next-generation contracting languages
such as Simplicity.