This repository contains the Alloy specification of Miniscript - a language for writing (a subset of) Bitcoin Scripts
It is based on the original specification in prose, with a bit of peeking into the source of C++ and Rust implementations.
The specification can be found in miniscript.als
The produced models are best viewed in Alloy viewer with the theme
found in the miniscript.thm file applied. Applying the theme will mask unnecessary objects and sets.
But please note that sometimes you want to see some of these hidden sets or objects in the model view.
Please use the 'Theme' menu in the viewer to customize.
The model is the tree of nodes, each node corresponds to the Miniscript fragment.
The nodes are combined according to the rules that govern correctness and non-malleability properties.
Timelocks are tracked across the node tree so that a predicate on the node can state if there is a conflict between blockheight- and blocktime-based timelocks
Witnesses Sig, Preimage and WitBool can have 'valid' and 'invalid' values, and the model instance can be analysed to understand what witnesses will be required for the particular spend of the script.
Witness configuration can result in some nodes being excluded from the execution (like in Or_i, only one branch will be executed depending on the WitBool in the witness). Nodes that are excluded from the execution with particular witness configuration will be in the IgnoredNode (directly ignored) and TransitivelyIgnoredNode (descendant of ignored) sets. The miniscript.thm theme uses gray color for ignored nodes.
The formal spec can be used as an additional reference to original spec. Navigating the formal spec may be easier after you get all the meanings from the prose spec
The model viewer of Ally has an ability to export the model instance to .dot file (of Graphviz DOT language). This file can be processed and converted, for example, to the script as a string, the properties of the script and the witnesses for the script. The properties and witnesses can then be compared to the ones generated by the implementation. The current problem is the inability of Alloy analyzer to automate generation of model instances, so you would need to hit 'Next' and then save via 'File/Export' for each instance. Maybe this can be overcome with desktop automation software. Alloy is open-source, so it also might happen in the future that there will be the option to automate instance generation and export to DOT files.
Write a program that uses certain implementation to generate checks for Alloy to check against. It will generate a file that starts with open miniscript, and then has a sequence of predicates each checking the validity of a certain model instance that is generated by that program. And then a check clause that checks all the predicates.
It should be much easier to extend or amend Miniscript when you can check the properties of the model. The Alloy analyzer is for bounded model checking, so the size of the checked model that can be practically checked is limited. Nevertheless, due to small scope hypothesis (which asserts that most bugs can be demonstrated with small counterexamples) checking the properties in Alloy can be valuable tool in addition to reasoning by the human
The visualisation of the model instances is excellent in Alloy. The spec can be easily changed and many properties to check against the model can be devised. This makes the spec a good tool to explore the properties of Miniscript
It might be possible to model the non-malleable satisfaction algorithm, but currently only the type system that can enforce the static properties of the script, and just satisfactions/dissatisfactions is modelled, without detection if particulare sat/dsat is malleable. With model of non-malleable satisfaction algorithm, it will be possible to check more properties of the runtime behavior of the signer.
Modelling resource limits would require to model the properties of Bitcoin script, while this specification is only concerned with Miniscript.
At the moment, the specification was only checked with its internal predicates. It was not checked against any real-world implementation, and even checking against the implementation does not give the ultimate guarantees, so reviews and corrections are always welcome!
Some of the predicates is checked with well_formed check, but there might be more ways to check for
the spec consistency, to check certain properties of the model, or to find interesting instances.
Please feel free to share ideas for new predicates to apply to the model !
This Miniscript specification in Alloy specification language was created by Dmitry Petukhov and released under a Creative Commons Attribution-ShareAlike 4.0 International License
Miniscript and its original specification in prose was designed and implemented by Pieter Wuille, Andrew Poelstra, and Sanket Kanjalkar at Blockstream Research, but is the result of discussions with several other people.