Thanks for this! I can't comment on the correctness of your implementation, but I really appreciate the idea and effort.
By chance, did you come across any other spec definitions in alternate formal grammars? -Clark On Wed, Nov 25, 2020 at 5:35 AM Dmitry Petukhov via bitcoin-dev < [email protected]> wrote: > I have created a formal specification of Miniscript [1] using > the specification language of Alloy analyzer [2] > > Link: https://github.com/dgpv/miniscript-alloy-spec > > Possible uses for the spec: > > - Implementing Miniscript libraries, as additional reference that might > be easier to navigate than prose spec > > - Generating test cases for implementations, although currently this > will be a manual process due to the tools limitation (can be overcome > with GUI automation) > > - Checking the implementation against the spec, by writing a program > that would generate Alloy .als files from the data structures of the > implementation, and then checking these files in Alloy > > - Extending or amending Miniscript, if the need arise. Having > extenstions and changes checked (with bounds) against a spec should > help catch inconsistencies > > - Exploring the properties of Miniscript > > If you have an interest in Miniscript, please consider looking at the > spec and share your ideas. > > The spec may contain mistakes, as it was not yet checked against any > implementation, it was only checked for consistency using its own > predicates, with the scope of up to 8 nodes. > > If you notice a mistake or inconsistency, please submit an issue on > github (or communicate this in other ways) > > [1] http://bitcoin.sipa.be/miniscript/ > [2] https://alloytools.org/ > _______________________________________________ > bitcoin-dev mailing list > [email protected] > https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev >
_______________________________________________ bitcoin-dev mailing list [email protected] https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
