1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
Return-Path: <dp@simplexum.com>
Received: from whitealder.osuosl.org (smtp1.osuosl.org [140.211.166.138])
by lists.linuxfoundation.org (Postfix) with ESMTP id 1E613C0176
for <bitcoin-dev@lists.linuxfoundation.org>;
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 <bitcoin-dev@lists.linuxfoundation.org>;
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 <bitcoin-dev@lists.linuxfoundation.org>;
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 <bitcoin-dev@lists.linuxfoundation.org>;
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 <bitcoin-dev@lists.linuxfoundation.org>;
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 <dp@simplexum.com>
To: Dmitry Petukhov via bitcoin-dev <bitcoin-dev@lists.linuxfoundation.org>
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 <bitcoin-dev.lists.linuxfoundation.org>
List-Unsubscribe: <https://lists.linuxfoundation.org/mailman/options/bitcoin-dev>,
<mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=unsubscribe>
List-Archive: <http://lists.linuxfoundation.org/pipermail/bitcoin-dev/>
List-Post: <mailto:bitcoin-dev@lists.linuxfoundation.org>
List-Help: <mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=help>
List-Subscribe: <https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev>,
<mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=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
|
