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 1E613C0176 for ; Mon, 1 Jun 2020 11:36:17 +0000 (UTC) Received: from localhost (localhost [127.0.0.1]) by whitealder.osuosl.org (Postfix) with ESMTP id 0BEBB85149 for ; Mon, 1 Jun 2020 11:36:17 +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 NghUOtG52Rtj for ; Mon, 1 Jun 2020 11:36:16 +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 0522481091 for ; Mon, 1 Jun 2020 11:36:15 +0000 (UTC) Received: from mail.ruggedbytes.com (localhost [127.0.0.1]) by mail.ruggedbytes.com (Postfix) with ESMTPS id 49F5E260022D for ; Mon, 1 Jun 2020 11:36:13 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=simplexum.com; s=mail; t=1591011373; bh=elmS8wES5aOxjgVLPs4/mQbpCeIdoXyTucni41p80aw=; h=Date:From:To:Subject:In-Reply-To:References; b=h1AtoX55O6atHximEIXI+q1LOEGF6BBZwE/36FX7QeCU8CebkK6cFEt2Ii94IW+M5 zP5BzwNG3HjULtbGc/Y+rjU//0l3V3ZFipJVSwwlJ0n1fFiUewGoUcufQ8P7hNuApu kQLJ8NcvrplQKndDa+DbOXRbskFhrGpjmnYDgLAY= Date: Mon, 1 Jun 2020 16:38:54 +0500 From: Dmitry Petukhov To: Dmitry Petukhov via bitcoin-dev Message-ID: <20200601163854.17594845@simplexum.com> In-Reply-To: <20200513220222.24953c0a@simplexum.com> References: <20200513220222.24953c0a@simplexum.com> Organization: simplexum.com MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Mailman-Approved-At: Mon, 01 Jun 2020 11:52:46 +0000 Subject: Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap 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: Mon, 01 Jun 2020 11:36:17 -0000 I've finished specifying the full Succint Atomic Swap contract in TLA+. I believe the specification [1] now covers all relevant behaviors of the participants. It even has an option to enable 'non-rational' behavior, so that it can be shown that the transactions that are there to punish bad behavior can actually be used. If you examine the spec and find that I failed to specify some relevant behavior, please tell. The specification can be used to exhaustively check safety properties of the model (such as no participant can take both coins, unless in explicitly specified circumstances), and temporal properties (such as contract always end up in an explicitly specified 'finished' state). The specification can also be used to *show* (but not automatically check at the moment) the hyperproperties of the model, such as what transactions can ever be confirmed in at least one the execution path, max/min/avg values for various stats, etc. The information on these hyperproperties can be printed out during model checking, and can be examined manually or with help of additional scripts (if one willing to write some). The model has some limitations, like only having one miner, and not modelling fees and mempool priorities. More than one miner needed to introduce reorgs in the model, but I believe that reorgs are relevant only if we cannot say that "one block in the model means 6 bitcoin blocks" (or whatever reorg safety limit is acceptable). I also believe that the fees and mempool priorities are a lower-level concern, because the task to confirm the transaction in time is the same for different stages of the contract and for different transactions, and therefore this can be modelled separately. The goal of creating this specification was to evaluate the suitability of TLA+ for modelling of the smart contracts in UTXO-based blockchain systems. I believe that the presented spec shows that it is indeed feasible to do such modelling and TLA+ is a suitable tool for specifying and for checking such specifications (Although having ability to automatically check hyperproperties using TLA+ expressions would be nice). I hope that this spec can be used as a basis for specs for other contracts, and that using TLA+ can make designing safe contracts for UTXO-based systems easier. I also hope that this will help to increase interest in using formal methods in this area. I tried to make the parts of the spec that deal with things like mining and mempool to not depend on the concrete contract logic, in expectation that this logic can be reused afterwards for the specs of other contracts. I did not make specific effort to factor out this generic logic into separate module though, because I think that more various contract specifications need to be designed and analyzed to understand what is really generic and what should lay with concrete contract logic. When more knowledge is created regarding this, there could be a module that contract specifications can use to avoid explicitly specifying the generic blockchain-related logic. Thanks to Ruben Somsen for designing this contract and providing helpful description and diagram that made it possible to create this formal specification. [1] https://github.com/dgpv/SASwap_TLAplus_spec