path: root/f5/54cdf5861b5fbbf5e20659f64addeac2a88084

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--