From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from whitealder.osuosl.org (smtp1.osuosl.org [140.211.166.138]) by lists.linuxfoundation.org (Postfix) with ESMTP id 0B395C0052 for ; Wed, 25 Nov 2020 11:11:13 +0000 (UTC) Received: from localhost (localhost [127.0.0.1]) by whitealder.osuosl.org (Postfix) with ESMTP id E570986DCD for ; Wed, 25 Nov 2020 11:11:12 +0000 (UTC) X-Virus-Scanned: amavisd-new at osuosl.org Received: from whitealder.osuosl.org ([127.0.0.1]) by localhost (.osuosl.org [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id eHjzPCJvGv5z for ; Wed, 25 Nov 2020 11:11:11 +0000 (UTC) X-Greylist: from auto-whitelisted by SQLgrey-1.7.6 Received: from mail.ruggedbytes.com (mail.ruggedbytes.com [88.99.30.248]) by whitealder.osuosl.org (Postfix) with ESMTPS id 9525786DCB for ; Wed, 25 Nov 2020 11:11:11 +0000 (UTC) Received: from mail.ruggedbytes.com (localhost [127.0.0.1]) by mail.ruggedbytes.com (Postfix) with ESMTPS id A18C0260023D for ; Wed, 25 Nov 2020 11:11:08 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=simplexum.com; s=mail; t=1606302668; bh=EpTEgoHWbuyjg8732WvUSwATpGUDD1MizU02ojc3+WU=; h=Date:From:To:Subject; b=kyYcJQYOyetBzBz5LR6AH2i0nmDQnhXmzjdz1t9FgGJPmUdvsyJpsH//WScRGbIUe +Yp4Hi1LeARSb/ZztoqlCZmtDjSDLU7FMnlQ6I45t3NKAtdoniNpeWuJQ86urO/f3u QHjKV4x94mQGtC2cW33WJRgxEhVdepW8YwsB0s40= Date: Wed, 25 Nov 2020 12:15:55 +0100 From: Dmitry Petukhov To: bitcoin-dev@lists.linuxfoundation.org Message-ID: <20201125121555.49565b3c@simplexum.com> Organization: simplexum.com MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Mailman-Approved-At: Wed, 25 Nov 2020 11:35:49 +0000 Subject: [bitcoin-dev] Formal specification of Miniscript in Alloy X-BeenThere: bitcoin-dev@lists.linuxfoundation.org X-Mailman-Version: 2.1.15 Precedence: list List-Id: Bitcoin Protocol Discussion List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 25 Nov 2020 11:11:13 -0000 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/