summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRuben Somsen <rsomsen@gmail.com>2020-05-13 21:03:17 +0200
committerbitcoindev <bitcoindev@gnusha.org>2020-05-13 19:03:34 +0000
commit0b902affca089fff770582714ce6ec949e128f65 (patch)
treeeb3c1f7242d98e71457df9cd46cfefab87f0f06b
parentc7cf3e028e534b29a6518ac75dca5008bd9d5c8f (diff)
downloadpi-bitcoindev-0b902affca089fff770582714ce6ec949e128f65.tar.gz
pi-bitcoindev-0b902affca089fff770582714ce6ec949e128f65.zip
Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap
-rw-r--r--f5/54cdf5861b5fbbf5e20659f64addeac2a88084326
1 files changed, 326 insertions, 0 deletions
diff --git a/f5/54cdf5861b5fbbf5e20659f64addeac2a88084 b/f5/54cdf5861b5fbbf5e20659f64addeac2a88084
new file mode 100644
index 000000000..051282d36
--- /dev/null
+++ b/f5/54cdf5861b5fbbf5e20659f64addeac2a88084
@@ -0,0 +1,326 @@
+Return-Path: <rsomsen@gmail.com>
+Received: from hemlock.osuosl.org (smtp2.osuosl.org [140.211.166.133])
+ by lists.linuxfoundation.org (Postfix) with ESMTP id A2CB7C016F
+ for <bitcoin-dev@lists.linuxfoundation.org>;
+ Wed, 13 May 2020 19:03:34 +0000 (UTC)
+Received: from localhost (localhost [127.0.0.1])
+ by hemlock.osuosl.org (Postfix) with ESMTP id 8ACCB89438
+ for <bitcoin-dev@lists.linuxfoundation.org>;
+ Wed, 13 May 2020 19:03:34 +0000 (UTC)
+X-Virus-Scanned: amavisd-new at osuosl.org
+Received: from hemlock.osuosl.org ([127.0.0.1])
+ by localhost (.osuosl.org [127.0.0.1]) (amavisd-new, port 10024)
+ with ESMTP id T-AwSgbHIITs
+ for <bitcoin-dev@lists.linuxfoundation.org>;
+ Wed, 13 May 2020 19:03:31 +0000 (UTC)
+X-Greylist: domain auto-whitelisted by SQLgrey-1.7.6
+Received: from mail-ej1-f48.google.com (mail-ej1-f48.google.com
+ [209.85.218.48])
+ by hemlock.osuosl.org (Postfix) with ESMTPS id 61208892AC
+ for <bitcoin-dev@lists.linuxfoundation.org>;
+ Wed, 13 May 2020 19:03:31 +0000 (UTC)
+Received: by mail-ej1-f48.google.com with SMTP id e2so422485eje.13
+ for <bitcoin-dev@lists.linuxfoundation.org>;
+ Wed, 13 May 2020 12:03:31 -0700 (PDT)
+DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
+ h=mime-version:references:in-reply-to:from:date:message-id:subject:to
+ :cc; bh=ByJxDnKZi4TtjZZKEld0PhoezZYTxk1pEna+TkZ+irc=;
+ b=oZGUcxRyqID0wOTkNf3r3VqyJPr/PFk0RxCmN5L5avLATh8ysBHwuqSbvEPuH4CIWy
+ QA/aZGAofdn+VvBS/b3UGzE2f34UN065DzLFkCA27MeNSIt0awC7LWhoSvFmJteBXJuu
+ bv8ImdnF7m87i6GLPUBsD0pV8EvEjF95mXQuJhrAYwHEa0PusGzWNqhZvFq44uXXr/gm
+ 0QwHxaEGXiqrCeMHWiCbQaNd9yZQV/nFsfPJGCgAZgLFHk8xdScNNVlkifiZQN4LeXBU
+ McuSnltvIC1k73xoqr8ljvDt8fkfEzWb4Xvl0PwDfMUKXnYQkhOUbSfG6k+p5sGunnev
+ aayQ==
+X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
+ d=1e100.net; s=20161025;
+ h=x-gm-message-state:mime-version:references:in-reply-to:from:date
+ :message-id:subject:to:cc;
+ bh=ByJxDnKZi4TtjZZKEld0PhoezZYTxk1pEna+TkZ+irc=;
+ b=DEAlWQ34+7tkKcT+kPu8qXuj7RXxgJE6rhbdIWpSRqkHMZUkK/VFmn+sNXPxfDqyhB
+ /Qntirx2dMWcy8trHfIxw9vyHk/DyX11POxYE7dWJR117v2foG7sH0iDbGGsXySMJVCM
+ KezMyLTz93/uhb0SYOVkD+2d2LpmhoEznmoOspIL16zvnsx53AL3yTBLvaqOmSayE1hD
+ vtHmjhTaeTN94WiZ9oYtO/9XFbx2z0LbYzrRMwol9fEHq5rySbObw9fmVQLawKo8pVgl
+ m8kd+sfT1j1xmRQ9i9/PxREo9iAqZB8IG4r9RdiDBuvPO+cp2LP7UYaQ3CNrRHVmVzLP
+ F62Q==
+X-Gm-Message-State: AOAM5324EJfHcL8pI1wyjjyT3wllHQ7vhDKLTC9uXlYogCwXPhtAqQ44
+ F7hwnNLQayvh5osm3mxsyMvawKlpGXuqBGKQCmXNzM+V
+X-Google-Smtp-Source: ABdhPJzeJmURk8E5vlxYa+1NX0qapLtaKxCxbjH4MtI+IlUPnSZOz0m55Cww0DlwxQ/n62gDa22RoHuK9c8/gRmgc5s=
+X-Received: by 2002:a17:906:7f0d:: with SMTP id
+ d13mr465780ejr.312.1589396609615;
+ Wed, 13 May 2020 12:03:29 -0700 (PDT)
+MIME-Version: 1.0
+References: <20200513220222.24953c0a@simplexum.com>
+In-Reply-To: <20200513220222.24953c0a@simplexum.com>
+From: Ruben Somsen <rsomsen@gmail.com>
+Date: Wed, 13 May 2020 21:03:17 +0200
+Message-ID: <CAPv7TjbZVYTztQLd2dxjzFajhPTg23iWtapkVBzz+z0q=pH2rw@mail.gmail.com>
+To: Dmitry Petukhov <dp@simplexum.com>
+Content-Type: multipart/alternative; boundary="00000000000052cd5705a58c3ccf"
+X-Mailman-Approved-At: Wed, 13 May 2020 19:06:29 +0000
+Cc: Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.org>
+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: Wed, 13 May 2020 19:03:34 -0000
+
+--00000000000052cd5705a58c3ccf
+Content-Type: text/plain; charset="UTF-8"
+
+Hi Dmitry,
+
+Thanks for creating a specification for testing, I appreciate the interest!
+
+>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])
+
+I'm not sure if I follow. The issue ZmnSCPxj described about bypassing the
+mempool was not a violation. It was merely a "nuisance" strategy that
+causes Alice to have to abort in three transactions. Also note that I
+subsequently pointed out in the thread that this strategy does not work,
+because Alice is supposed to abort sooner than that if Bob still has not
+locked up any funds.
+
+Or perhaps you're referring to the issue ZmnSCPxj pointed out after that,
+where refund transaction #1 and the success transaction could both become
+valid at the same time. It would make sense for the test to pick up on
+that, but I believe that is ultimately also not an issue (see my last reply
+in the thread).
+
+>I did not understand what the destination of Alice&Bob cooperative spend
+of refund_tx#1 will be
+
+This transaction can be spent by Alice & Bob right away or by Alice a day
+later (in relative time, so the tx has to confirm first). The Alice & Bob
+condition is there purely to ensure that Bob can spend the money before
+Alice once he receives her key at the end of the protocol.
+
+If it helps, you could model this transaction as two separate transactions
+instead:
+txA: 1 day absolute timelock to Alice & Bob (reveals secretAlice), which
+can then be spent by
+txB: +1 day relative timelock to Alice
+
+This should be functionally equivalent. Also note that the protocol should
+fully function if refund tx #1 did not exist at all. It merely serves to
+save block space in certain refund scenarios.
+
+>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
+
+A laudable goal. Good luck with your efforts.
+
+Cheers,
+Ruben
+
+On Wed, May 13, 2020 at 7:07 PM Dmitry Petukhov via bitcoin-dev <
+bitcoin-dev@lists.linuxfoundation.org> wrote:
+
+> 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
+> _______________________________________________
+> bitcoin-dev mailing list
+> bitcoin-dev@lists.linuxfoundation.org
+> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
+>
+
+--00000000000052cd5705a58c3ccf
+Content-Type: text/html; charset="UTF-8"
+Content-Transfer-Encoding: quoted-printable
+
+<div dir=3D"ltr">Hi Dmitry,<div><br></div><div>Thanks for creating a specif=
+ication for testing, I appreciate the interest!</div><div><br></div><div>&g=
+t;The checking of the model encoded in the specification can successfully d=
+etect the violation of &#39;no mutual secret knowledge&#39; 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])</div><div><br></div><div>I&#39;m not sure if I follow. The iss=
+ue ZmnSCPxj described about bypassing the mempool was not a violation. It w=
+as merely a &quot;nuisance&quot; strategy that causes Alice to have to abor=
+t in three transactions. Also note that I subsequently pointed out in the t=
+hread that this strategy does not work, because Alice is supposed to abort =
+sooner than that if Bob still has not locked up any funds.</div><div><br></=
+div><div>Or perhaps you&#39;re referring to the issue=20
+
+ZmnSCPxj
+
+ pointed out after that, where refund transaction #1 and the success transa=
+ction could both become valid at the same time. It would make sense for the=
+ test to pick up on that, but I believe that is ultimately also not an issu=
+e (see my last reply in the thread).</div><div><br></div><div>&gt;I did not=
+ understand what the destination of Alice&amp;Bob cooperative spend of refu=
+nd_tx#1 will be<br></div><div><br></div><div>This transaction can be spent =
+by Alice &amp; Bob right away or by Alice a day later (in relative time, so=
+ the tx has to confirm first). The Alice &amp; Bob condition is there purel=
+y to ensure that Bob can spend the money before Alice once he receives her =
+key at the end of the protocol.</div><div><br></div><div>If it helps, you c=
+ould model this transaction as two separate transactions instead:</div><div=
+>txA: 1 day absolute timelock to Alice &amp; Bob (reveals secretAlice), whi=
+ch can then be spent by</div><div>txB: +1 day relative timelock to Alice</d=
+iv><div><br></div><div>This should be functionally equivalent. Also note th=
+at the protocol should fully function if refund tx #1 did not exist at all.=
+ It merely serves to save block space in certain refund scenarios.</div><di=
+v><br></div><div>&gt;it would be great to have an established framework for=
+ modelling of the behavior in Bitcoin-like blockchain networks. In particul=
+ar, having a model of mempool-related behavior would help to reason about d=
+ifficult RBF/CPFP issues<br></div><div><br></div><div>A laudable goal. Good=
+ luck with your efforts.</div><div><br></div><div>Cheers,</div><div>Ruben</=
+div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_at=
+tr">On Wed, May 13, 2020 at 7:07 PM Dmitry Petukhov via bitcoin-dev &lt;<a =
+href=3D"mailto:bitcoin-dev@lists.linuxfoundation.org">bitcoin-dev@lists.lin=
+uxfoundation.org</a>&gt; wrote:<br></div><blockquote class=3D"gmail_quote" =
+style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);pa=
+dding-left:1ex">The Succint Atomic Swap contract presented by Ruben Somsen =
+recently has<br>
+drawn much interest.<br>
+<br>
+I personally am interested in the smart contracts realizeable in the<br>
+UTXO model, and also interested in applying formal methods to the<br>
+design and implementation of such contracts.<br>
+<br>
+I think that having formal specifications for the contracts and to be<br>
+able to machine-check the properties of these specifications is very<br>
+valuable, as it can uncover the corner cases that might be difficult to<br>
+uncover otherwise.<br>
+<br>
+The SAS contract is complex enough that it may benefit from formal<br>
+specification and machine checking.<br>
+<br>
+I created a specification in TLA+ [1] specification language based on<br>
+the explanation and the diagram given by Ruben.<br>
+<br>
+The checking of the model encoded in the specification can successfully<br>
+detect the violation of &#39;no mutual secret knowledge&#39; invariant when=
+ one<br>
+of the participant can bypass mempool and give the transaction directly<br>
+to the miner (this problem was pointed out by ZmnSCPxj in the original<br>
+SAS thread [2])<br>
+<br>
+There&#39;s one transition that was unclear how to model, though: I did not=
+<br>
+understand what the destination of Alice&amp;Bob cooperative spend of<br>
+refund_tx#1 will be, so this transition is not modelled.<br>
+<br>
+I believe there can be more invariants and temporal properties of the<br>
+model that can be checked. At the moment the temporal properties<br>
+checking does not work, as I didn&#39;t master TLA+ enough yet. The safety<=
+br>
+invariants checking should work fine, though, but more work needed to<br>
+devise and add the invariants.<br>
+<br>
+In the future, it would be great to have an established framework for<br>
+modelling of the behavior in Bitcoin-like blockchain networks.<br>
+In particular, having a model of mempool-related behavior would help to<br>
+reason about difficult RBF/CPFP issues. The specification I present<br>
+models the mempool, but in a simple way, without regards to the fees.<br>
+<br>
+The specification can be found in this github repository:<br>
+<a href=3D"https://github.com/dgpv/SASwap_TLAplus_spec" rel=3D"noreferrer" =
+target=3D"_blank">https://github.com/dgpv/SASwap_TLAplus_spec</a><br>
+<br>
+There could be mistakes or omissions in the specified model, I hope<br>
+that public review can help find these.<br>
+<br>
+It would be great to receive comments, suggestions and corrections,<br>
+especially from people experienced in formal methods and TLA+, as this<br>
+is only my second finished TLA+ spec and only my third project using<br>
+formal methods (I created bitcoin transaction deserialization code in<br>
+Ada/SPARK before that [3]). Please use the github issues or off-list<br>
+mail to discuss if the matter is not interesting to the general<br>
+bitcoin-dev list audience.<br>
+<br>
+[1] <a href=3D"https://lamport.azurewebsites.net/tla/tla.html" rel=3D"noref=
+errer" target=3D"_blank">https://lamport.azurewebsites.net/tla/tla.html</a>=
+<br>
+<br>
+[2]<br>
+<a href=3D"https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2020-May=
+/017846.html" rel=3D"noreferrer" target=3D"_blank">https://lists.linuxfound=
+ation.org/pipermail/bitcoin-dev/2020-May/017846.html</a><br>
+<br>
+[3] <a href=3D"https://github.com/dgpv/spark-bitcoin-transaction-example" r=
+el=3D"noreferrer" target=3D"_blank">https://github.com/dgpv/spark-bitcoin-t=
+ransaction-example</a><br>
+_______________________________________________<br>
+bitcoin-dev mailing list<br>
+<a href=3D"mailto:bitcoin-dev@lists.linuxfoundation.org" target=3D"_blank">=
+bitcoin-dev@lists.linuxfoundation.org</a><br>
+<a href=3D"https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev" =
+rel=3D"noreferrer" target=3D"_blank">https://lists.linuxfoundation.org/mail=
+man/listinfo/bitcoin-dev</a><br>
+</blockquote></div>
+
+--00000000000052cd5705a58c3ccf--
+