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
|
Return-Path: <dp@simplexum.com>
Received: from silver.osuosl.org (smtp3.osuosl.org [140.211.166.136])
by lists.linuxfoundation.org (Postfix) with ESMTP id C2C6BC016F
for <bitcoin-dev@lists.linuxfoundation.org>;
Wed, 13 May 2020 17:05:05 +0000 (UTC)
Received: from localhost (localhost [127.0.0.1])
by silver.osuosl.org (Postfix) with ESMTP id BD99F2264A
for <bitcoin-dev@lists.linuxfoundation.org>;
Wed, 13 May 2020 17:05:05 +0000 (UTC)
X-Virus-Scanned: amavisd-new at osuosl.org
Received: from silver.osuosl.org ([127.0.0.1])
by localhost (.osuosl.org [127.0.0.1]) (amavisd-new, port 10024)
with ESMTP id 9z8L0isrp2KJ
for <bitcoin-dev@lists.linuxfoundation.org>;
Wed, 13 May 2020 17:05:04 +0000 (UTC)
X-Greylist: delayed 00:05:09 by SQLgrey-1.7.6
Received: from mail.ruggedbytes.com (mail.ruggedbytes.com [88.99.30.248])
by silver.osuosl.org (Postfix) with ESMTPS id 8148F22636
for <bitcoin-dev@lists.linuxfoundation.org>;
Wed, 13 May 2020 17:05:04 +0000 (UTC)
Received: from mail.ruggedbytes.com (localhost [127.0.0.1])
by mail.ruggedbytes.com (Postfix) with ESMTPS id 98380260020D
for <bitcoin-dev@lists.linuxfoundation.org>;
Wed, 13 May 2020 16:59:52 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=simplexum.com;
s=mail; t=1589389192;
bh=A3YNfH6wkAItyxXZH4nhnYPtlP3hrECPMFONZqVZzsE=;
h=Date:From:To:Subject;
b=DfJ6MxsCuJc7haYfdG7GH4AgqZToxvs5PQZY2KUaOazRJm36TNaAe6V8hCt9yLT2X
D+EUsnmQMHXwhWuf7AEuhaLsuC665FL7x8dkWyWUI4MDImtlY0KlEcobpL6Zlwppp0
t/JOkD28F+Fyfc3O13lTp+3afJszTb+KT7ar80Ec=
Date: Wed, 13 May 2020 22:02:22 +0500
From: Dmitry Petukhov <dp@simplexum.com>
To: bitcoin-dev@lists.linuxfoundation.org
Message-ID: <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: Wed, 13 May 2020 17:07:49 +0000
Subject: [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: Wed, 13 May 2020 17:05:05 -0000
The Succint Atomic Swap contract presented by Ruben Somsen recently has
drawn much interest.
I personally am interested in the smart contracts realizeable in the
UTXO model, and also interested in applying formal methods to the
design and implementation of such contracts.
I think that having formal specifications for the contracts and to be
able to machine-check the properties of these specifications is very
valuable, as it can uncover the corner cases that might be difficult to
uncover otherwise.
The SAS contract is complex enough that it may benefit from formal
specification and machine checking.
I created a specification in TLA+ [1] specification language based on
the explanation and the diagram given by Ruben.
The checking of the model encoded in the specification can successfully
detect the violation of 'no mutual secret knowledge' invariant when one
of the participant can bypass mempool and give the transaction directly
to the miner (this problem was pointed out by ZmnSCPxj in the original
SAS thread [2])
There's one transition that was unclear how to model, though: I did not
understand what the destination of Alice&Bob cooperative spend of
refund_tx#1 will be, so this transition is not modelled.
I believe there can be more invariants and temporal properties of the
model that can be checked. At the moment the temporal properties
checking does not work, as I didn't master TLA+ enough yet. The safety
invariants checking should work fine, though, but more work needed to
devise and add the invariants.
In the future, it would be great to have an established framework for
modelling of the behavior in Bitcoin-like blockchain networks.
In particular, having a model of mempool-related behavior would help to
reason about difficult RBF/CPFP issues. The specification I present
models the mempool, but in a simple way, without regards to the fees.
The specification can be found in this github repository:
https://github.com/dgpv/SASwap_TLAplus_spec
There could be mistakes or omissions in the specified model, I hope
that public review can help find these.
It would be great to receive comments, suggestions and corrections,
especially from people experienced in formal methods and TLA+, as this
is only my second finished TLA+ spec and only my third project using
formal methods (I created bitcoin transaction deserialization code in
Ada/SPARK before that [3]). Please use the github issues or off-list
mail to discuss if the matter is not interesting to the general
bitcoin-dev list audience.
[1] https://lamport.azurewebsites.net/tla/tla.html
[2]
https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2020-May/017846.html
[3] https://github.com/dgpv/spark-bitcoin-transaction-example
|
