path: root/20/3185d78a9aa79bf69d39ac70d5ff37e330f241

Return-Path: <jlrubin@mit.edu>
Received: from smtp1.osuosl.org (smtp1.osuosl.org [140.211.166.138])
 by lists.linuxfoundation.org (Postfix) with ESMTP id 3A35EC000E
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Wed,  7 Jul 2021 17:26:56 +0000 (UTC)
Received: from localhost (localhost [127.0.0.1])
 by smtp1.osuosl.org (Postfix) with ESMTP id BCF4C83B03
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Wed,  7 Jul 2021 17:26:53 +0000 (UTC)
X-Virus-Scanned: amavisd-new at osuosl.org
X-Spam-Flag: NO
X-Spam-Score: -4.199
X-Spam-Level: 
X-Spam-Status: No, score=-4.199 tagged_above=-999 required=5
 tests=[BAYES_00=-1.9, HTML_MESSAGE=0.001, RCVD_IN_DNSWL_MED=-2.3,
 SPF_HELO_NONE=0.001, SPF_PASS=-0.001] autolearn=ham autolearn_force=no
Received: from smtp1.osuosl.org ([127.0.0.1])
 by localhost (smtp1.osuosl.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id uzCM-0fSnH5h
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Wed,  7 Jul 2021 17:26:52 +0000 (UTC)
X-Greylist: domain auto-whitelisted by SQLgrey-1.8.0
Received: from outgoing.mit.edu (outgoing-auth-1.mit.edu [18.9.28.11])
 by smtp1.osuosl.org (Postfix) with ESMTPS id 43E0A83B08
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Wed,  7 Jul 2021 17:26:52 +0000 (UTC)
Received: from mail-il1-f180.google.com (mail-il1-f180.google.com
 [209.85.166.180]) (authenticated bits=0)
 (User authenticated as jlrubin@ATHENA.MIT.EDU)
 by outgoing.mit.edu (8.14.7/8.12.4) with ESMTP id 167HQo9Z008730
 (version=TLSv1/SSLv3 cipher=AES128-GCM-SHA256 bits=128 verify=NOT)
 for <bitcoin-dev@lists.linuxfoundation.org>; Wed, 7 Jul 2021 13:26:50 -0400
Received: by mail-il1-f180.google.com with SMTP id o10so3679190ils.6
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Wed, 07 Jul 2021 10:26:50 -0700 (PDT)
X-Gm-Message-State: AOAM532FCwdIZ+Tesatl2YP2Oz5BYug/EgWql+EETs1+TeOnrCmIKm0z
 mBHnr3cBzdrhX0KubvlmIfT2fagu+w34siextW0=
X-Google-Smtp-Source: ABdhPJxlA9PgKjO58rdtI98cO0ab9PuDCcSYMW/s4iUFRRA/TLIhzhrYV4XcszP4A4aL1xafP96w6sYAVOZM1Y26SUE=
X-Received: by 2002:a92:d652:: with SMTP id x18mr18764330ilp.90.1625678809828; 
 Wed, 07 Jul 2021 10:26:49 -0700 (PDT)
MIME-Version: 1.0
References: <CAD5xwhjmu-Eee47Ho5eA6E6+aAdnchLU0OVZo=RTHaXnN17x8A@mail.gmail.com>
 <20210704011341.ddbiruuomqovrjn6@ganymede>
 <CAD5xwhimPBEV_tLpSPxs9B+XGUhvPx_dnhok=8=hyksyi4=B6g@mail.gmail.com>
 <20210704203230.37hlpdyzr4aijiet@ganymede>
 <5keA_aPvmCO5yBh_mBQ6Z5SwnnvEW0T-3vahesaDh57f-qv4FbG1SFAzDvT3rFhre6kFl282VsxV_pynwn_CdvF7fzH2q9NW1ZQHPH1pmdo=@protonmail.com>
 <CAMZUoKnuRXNG1pyupHrL+Wo80TXTbADVrexoB=+BKC633v-qMw@mail.gmail.com>
 <u2ETzW2-k7sjRKEz48C2n2QJvmWPVdhZIqtva_KvDNvxNDTVnR2zzYCL2Q8RUVkLm93OMJ2S2GOfUOxmdvNTaCIK1liebb4yvCCBBFB75f0=@protonmail.com>
 <CAMZUoK=rRDV4F7j64gTUqEB9EiBpwhZW6LP-FMR0FxR2Bc4iBw@mail.gmail.com>
 <CAMZUoK=yeb2Tc0GSfPs6ezS09gpXf=xgzkuiPrj905dfT5n6LA@mail.gmail.com>
In-Reply-To: <CAMZUoK=yeb2Tc0GSfPs6ezS09gpXf=xgzkuiPrj905dfT5n6LA@mail.gmail.com>
From: Jeremy <jlrubin@mit.edu>
Date: Wed, 7 Jul 2021 10:26:38 -0700
X-Gmail-Original-Message-ID: <CAD5xwhjfX+a3jSewCof4LUjcDR_dnffhnL7h-9dr4GZ53Jc2gA@mail.gmail.com>
Message-ID: <CAD5xwhjfX+a3jSewCof4LUjcDR_dnffhnL7h-9dr4GZ53Jc2gA@mail.gmail.com>
To: Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.org>
Content-Type: multipart/alternative; boundary="000000000000fa954305c68bd7ae"
Subject: Re: [bitcoin-dev] Unlimited covenants,
 was Re: CHECKSIGFROMSTACK/{Verify} BIP for Bitcoin
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, 07 Jul 2021 17:26:56 -0000

--000000000000fa954305c68bd7ae
Content-Type: text/plain; charset="UTF-8"

Hah -- ZmnSCPxj that post's a doozy -- but it more or less makes sense the
argument you're making in favor of permitting recursion at the transaction
level.

One part that's less clear is if you can make a case against being
recursive in Script fragments themselves -- ignoring bitcoin script for the
moment, what would be wrong with a small VM that a spender is able to
"purchase" a number of cycles and available memory via the annex, and the
program must execute and halt within that time? Then, per block/txn, you
can enforce a total cycle and memory limit. This still isn't quite the EVM,
since there's no cross object calling convention and the output is still
UTXOs. What are the arguments against this model from a safety perspective?

<new topic>

One of my general concerns with recursive covenants is the ability to "go
wrong" in surprising ways. Consider the following program (Sapio
<http://learn.sapio-lang.org>-pseudocode), which is a non recursive
covenant (i.e., doable today with presigning oracles) that demonstrates the
issue.

struct Pool {
    members: Vec<(Amount, Key)>,
}
impl Pool {
    then!{
        fn withdraw(self, ctx) {
            let mut builder = ctx.template();
            for (a, k) in self.members.iter() {
                builder = builder.add_output(a, k.into(), None)?;
            }
            builder.into()
        }
    }
    guard! {
        fn all_signed(self, ctx) {
            Clause::And(self.members.iter().map(|(a,k)|
Clause::Key(k.clone())).into())
        }
    }
    finish! {
        guarded_by: [all_signed]
        fn add_member(self, ctx, o_member: Option<(Amount, Key)>) {
            let member = o_member.into()?;
            let mut new_members = self.members.clone();
            new_members.push(member.clone());
            ctx.template().add_output(ctx.funds() + member.0,
                  Pool {members: new_members}, None)?.into()
        }
    }
}

Essentially this is a recursive covenant that allows either Complete via
the withdraw call or Continue via add_member, while preserving the same
underlying code. In this case, all_signed must be signed by all current
participants to admit a new member.

This type of program is subtly "wrong" because the state transition of
add_member does not verify that the Pool's future withdraw call will be
valid. E.g., we could add more than a 1MB of outputs, and then our program
would be "stuck". So it's critical that in our "production grade" covenant
system we do some static analysis before proceeding to a next step to
ensure that all future txns are valid. This is a strength of the CTV/Sapio
model presently, you always output a list of future txns to aid static
analysis.

However, when we make the leap to "automatic" covenants, I posit that it
will be *incredibly* difficult to prove that recursive covenants don't have
a "premature termination" where a state transition that should be valid in
an idealized setting is accidentally invalid in the actual bitcoin
environment and the program reaches a untimely demise.

For instance, OP_CAT has this footgun -- by only permitting 520 bytes, you
hit covenant limits at around 13 outputs assuming you are length checking
each one and not permitting bare script. We can avoid this specific footgun
some of the time by using SHA256STREAM instead, of course.

However, it is generally very difficult to avoid all sorts of issues. E.g.,
with the ability to generate/update tapscript trees, what happens when
through updating a well formed tapscript tree 128 times you bump an
important clause past the 129 depth limit?

I don't think that these sorts of challenges mean that we shouldn't enable
covenants or avoid enabling them, but rather that as we explore we should
add primitives in a methodical way and give users/toolchain builders
primitives that enable and or encourage safety and good program design.

My personal view is that CTV/Sapio with it's AOT compilation of automated
state transitions and ability to statically analyze is a concept that can
mature and be used in production in the near term. But the tooling to
safely do recursive computations at the txn level will take quite a bit
longer to mature, and we should be investing effort in producing
compilers/frameworks for emitting well formed programs before we get too in
the weeds on things like OP_TWEAK. (side note -- there's an easy path for
adding this sort of experimental feature to Sapio if anyone is looking for
a place to start)

--000000000000fa954305c68bd7ae
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div dir=3D"ltr"><div class=3D"gmail_default" style=3D"fon=
t-family:arial,helvetica,sans-serif;font-size:small;color:#000000"></div></=
div><div class=3D"gmail_quote"><div><div class=3D"gmail_default" style=3D"f=
ont-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">Hah=
 -- ZmnSCPxj that post&#39;s a doozy -- but it more or less makes sense the=
 argument you&#39;re making in favor of permitting recursion at the transac=
tion level.</div><div class=3D"gmail_default" style=3D"font-family:arial,he=
lvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><div class=
=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;font-siz=
e:small;color:rgb(0,0,0)">One part that&#39;s less clear is if you can make=
 a case against being recursive in Script fragments themselves -- ignoring =
bitcoin script for the moment, what would be wrong with a small VM that a s=
pender is able to &quot;purchase&quot; a number of cycles and available mem=
ory via the annex, and the program must execute and halt within that time? =
Then, per block/txn, you can enforce a total cycle and memory limit. This s=
till isn&#39;t quite the EVM, since there&#39;s no cross object calling con=
vention and the output is still UTXOs. What are the arguments against this =
model from a safety perspective?</div></div><div class=3D"gmail_default" st=
yle=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0=
,0)"><br></div><div class=3D"gmail_default" style=3D"font-family:arial,helv=
etica,sans-serif;font-size:small;color:rgb(0,0,0)">&lt;new topic&gt;</div><=
div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif=
;font-size:small;color:rgb(0,0,0)"><br></div><div class=3D"gmail_default" s=
tyle=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,=
0,0)">One of my general concerns with recursive covenants is the ability to=
 &quot;go wrong&quot; in surprising=C2=A0ways. Consider the following progr=
am (<a href=3D"http://learn.sapio-lang.org">Sapio</a>-pseudocode), which is=
 a non recursive covenant (i.e., doable today with presigning oracles) that=
 demonstrates the issue.</div><div class=3D"gmail_default" style=3D"font-fa=
mily:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div=
><div class=3D"gmail_default" style=3D"font-size:small;color:rgb(0,0,0)"><f=
ont face=3D"monospace">struct Pool {</font></div><div class=3D"gmail_defaul=
t" style=3D"font-size:small;color:rgb(0,0,0)"><font face=3D"monospace">=C2=
=A0 =C2=A0 members: Vec&lt;(Amount, Key)&gt;,</font></div><div class=3D"gma=
il_default" style=3D"font-size:small;color:rgb(0,0,0)"><font face=3D"monosp=
ace">}</font></div><div class=3D"gmail_default" style=3D"font-size:small;co=
lor:rgb(0,0,0)"><font face=3D"monospace">impl Pool {</font></div><div class=
=3D"gmail_default" style=3D"font-size:small;color:rgb(0,0,0)"><font face=3D=
"monospace">=C2=A0 =C2=A0 then!{</font></div><div class=3D"gmail_default" s=
tyle=3D"font-size:small;color:rgb(0,0,0)"><font face=3D"monospace">=C2=A0 =
=C2=A0 =C2=A0 =C2=A0 fn withdraw(self, ctx) {</font></div><div class=3D"gma=
il_default" style=3D"font-size:small;color:rgb(0,0,0)"><font face=3D"monosp=
ace">=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 let mut builder =3D ctx.temp=
late();</font></div><div class=3D"gmail_default" style=3D"font-size:small;c=
olor:rgb(0,0,0)"><font face=3D"monospace">=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0 for (a, k) in self.members.iter() {</font></div><div class=3D"gm=
ail_default" style=3D"font-size:small;color:rgb(0,0,0)"><font face=3D"monos=
pace">=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 builder =3D b=
uilder.add_output(a, k.into(), None)?;</font></div><div class=3D"gmail_defa=
ult" style=3D"font-size:small;color:rgb(0,0,0)"><font face=3D"monospace">=
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 }</font></div><div class=3D"gmail=
_default" style=3D"font-size:small;color:rgb(0,0,0)"><font face=3D"monospac=
e">=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 builder.into()</font></div><di=
v class=3D"gmail_default" style=3D"font-size:small;color:rgb(0,0,0)"><font =
face=3D"monospace">=C2=A0 =C2=A0 =C2=A0 =C2=A0 }</font></div><div class=3D"=
gmail_default" style=3D"font-size:small;color:rgb(0,0,0)"><font face=3D"mon=
ospace">=C2=A0 =C2=A0 }</font></div><div class=3D"gmail_default" style=3D"f=
ont-size:small;color:rgb(0,0,0)"><font face=3D"monospace">=C2=A0 =C2=A0 gua=
rd! {</font></div><div class=3D"gmail_default" style=3D"font-size:small;col=
or:rgb(0,0,0)"><font face=3D"monospace">=C2=A0 =C2=A0 =C2=A0 =C2=A0 fn all_=
signed(self, ctx) {</font></div><div class=3D"gmail_default" style=3D"font-=
size:small;color:rgb(0,0,0)"><font face=3D"monospace">=C2=A0 =C2=A0 =C2=A0 =
=C2=A0 =C2=A0 =C2=A0 Clause::And(self.members.iter().map(|(a,k)| Clause::Ke=
y(k.clone())).into())</font></div><div class=3D"gmail_default" style=3D"fon=
t-size:small;color:rgb(0,0,0)"><font face=3D"monospace">=C2=A0 =C2=A0 =C2=
=A0 =C2=A0 }</font></div><div class=3D"gmail_default" style=3D"font-size:sm=
all;color:rgb(0,0,0)"><font face=3D"monospace">=C2=A0 =C2=A0 }</font></div>=
<div class=3D"gmail_default" style=3D"font-size:small;color:rgb(0,0,0)"><fo=
nt face=3D"monospace">=C2=A0 =C2=A0 finish! {</font></div><div class=3D"gma=
il_default" style=3D"font-size:small;color:rgb(0,0,0)"><font face=3D"monosp=
ace">=C2=A0 =C2=A0 =C2=A0 =C2=A0 guarded_by: [all_signed]</font></div><div =
class=3D"gmail_default" style=3D"font-size:small;color:rgb(0,0,0)"><font fa=
ce=3D"monospace">=C2=A0 =C2=A0 =C2=A0 =C2=A0 fn add_member(self, ctx, o_mem=
ber: Option&lt;(Amount, Key)&gt;) {</font></div><div class=3D"gmail_default=
" style=3D"font-size:small;color:rgb(0,0,0)"><font face=3D"monospace">=C2=
=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 let member =3D o_member.into()?;</fo=
nt></div><div class=3D"gmail_default" style=3D"font-size:small;color:rgb(0,=
0,0)"><font face=3D"monospace">=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 le=
t mut new_members =3D self.members.clone();</font></div><div class=3D"gmail=
_default" style=3D"font-size:small;color:rgb(0,0,0)"><font face=3D"monospac=
e">=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 new_members.push(member.clone(=
));</font></div><div class=3D"gmail_default" style=3D"font-size:small;color=
:rgb(0,0,0)"><font face=3D"monospace">=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0 ctx.template().add_output(ctx.funds()=C2=A0+ member.0,</font></div><=
div class=3D"gmail_default" style=3D"font-size:small;color:rgb(0,0,0)"><fon=
t face=3D"monospace">=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0 Pool {members: new_members}, None)?.into()</font></div><div clas=
s=3D"gmail_default" style=3D"font-size:small;color:rgb(0,0,0)"><font face=
=3D"monospace">=C2=A0 =C2=A0 =C2=A0 =C2=A0 }</font></div><div class=3D"gmai=
l_default" style=3D"font-size:small;color:rgb(0,0,0)"><font face=3D"monospa=
ce">=C2=A0 =C2=A0 }</font></div><div class=3D"gmail_default" style=3D"font-=
size:small;color:rgb(0,0,0)"><font face=3D"monospace">}</font></div><div cl=
ass=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;font-=
size:small;color:rgb(0,0,0)"><br></div><div class=3D"gmail_default" style=
=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)=
">Essentially this is a recursive covenant that allows either Complete via =
the withdraw call or Continue via add_member, while preserving the same und=
erlying code. In this case, all_signed must be signed by all current partic=
ipants to admit a new member.</div><div class=3D"gmail_default" style=3D"fo=
nt-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br>=
</div><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,san=
s-serif;font-size:small;color:rgb(0,0,0)">This type of program is subtly &q=
uot;wrong&quot; because the state transition of add_member does not verify =
that the Pool&#39;s future withdraw call will be valid. E.g., we could add =
more than a 1MB of outputs, and then our program would be &quot;stuck&quot;=
. So it&#39;s critical that in our &quot;production grade&quot; covenant sy=
stem we do some static analysis before proceeding to a next step to ensure =
that all future txns are valid. This is a strength of the CTV/Sapio model p=
resently, you always output a list of future txns to aid static analysis.</=
div><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-=
serif;font-size:small;color:rgb(0,0,0)"><br></div><div class=3D"gmail_defau=
lt" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:r=
gb(0,0,0)">However, when we make the leap to &quot;automatic&quot; covenant=
s, I posit that it will be *incredibly* difficult to prove that recursive c=
ovenants don&#39;t have a &quot;premature termination&quot; where a state t=
ransition that should be valid in an idealized setting is accidentally inva=
lid in the actual bitcoin environment and the program reaches a untimely de=
mise.</div><div class=3D"gmail_default" style=3D"font-family:arial,helvetic=
a,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><div class=3D"gmai=
l_default" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;=
color:rgb(0,0,0)">For instance, OP_CAT has this footgun -- by only permitti=
ng 520 bytes, you hit covenant limits at around 13 outputs assuming you are=
 length checking each one and not permitting bare script. We can avoid this=
 specific footgun some of the time by using SHA256STREAM instead, of course=
.</div><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sa=
ns-serif;font-size:small;color:rgb(0,0,0)"><br></div><div class=3D"gmail_de=
fault" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;colo=
r:rgb(0,0,0)">However, it is generally very difficult to avoid all sorts of=
 issues. E.g., with the ability to generate/update tapscript trees, what ha=
ppens when through updating a well formed tapscript=C2=A0tree 128 times you=
 bump an important clause past the 129 depth limit?</div><div class=3D"gmai=
l_default" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;=
color:rgb(0,0,0)"><br></div><div class=3D"gmail_default" style=3D"font-fami=
ly:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">I don&#39;t=
 think that these sorts of challenges mean that we shouldn&#39;t enable cov=
enants or avoid enabling them, but rather that as we explore we should add =
primitives in a methodical way and give users/toolchain builders primitives=
 that enable and or encourage safety and good program design.</div><div cla=
ss=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;font-s=
ize:small;color:rgb(0,0,0)"><br></div><div class=3D"gmail_default" style=3D=
"font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">M=
y personal view is that CTV/Sapio with it&#39;s AOT compilation of automate=
d state transitions and ability to statically analyze is a concept that can=
 mature and be used in production in the near term. But the tooling to safe=
ly do recursive computations at the txn level will take quite a bit longer =
to mature, and we should be investing effort in producing compilers/framewo=
rks for emitting well formed programs before we get too in the weeds on thi=
ngs like OP_TWEAK. (side note -- there&#39;s an easy path for adding this s=
ort of experimental feature to Sapio if anyone is looking for a place to st=
art)</div><div class=3D"gmail_default" style=3D"font-family:arial,helvetica=
,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div></div></div>

--000000000000fa954305c68bd7ae--