Return-Path: Received: from smtp1.osuosl.org (smtp1.osuosl.org [140.211.166.138]) by lists.linuxfoundation.org (Postfix) with ESMTP id 3A35EC000E for ; 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 ; 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 ; 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 ; 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 ; Wed, 7 Jul 2021 13:26:50 -0400 Received: by mail-il1-f180.google.com with SMTP id o10so3679190ils.6 for ; 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: <20210704011341.ddbiruuomqovrjn6@ganymede> <20210704203230.37hlpdyzr4aijiet@ganymede> <5keA_aPvmCO5yBh_mBQ6Z5SwnnvEW0T-3vahesaDh57f-qv4FbG1SFAzDvT3rFhre6kFl282VsxV_pynwn_CdvF7fzH2q9NW1ZQHPH1pmdo=@protonmail.com> In-Reply-To: From: Jeremy Date: Wed, 7 Jul 2021 10:26:38 -0700 X-Gmail-Original-Message-ID: Message-ID: To: Bitcoin Protocol Discussion 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 List-Unsubscribe: , List-Archive: List-Post: List-Help: List-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? One of my general concerns with recursive covenants is the ability to "go wrong" in surprising ways. Consider the following program (Sapio -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
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 transac= tion 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 s= pender is able to "purchase" 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't quite the EVM, since there's no cross object calling con= vention and the output is still UTXOs. What are the arguments against this = model from a safety perspective?

<new topic>
<= div class=3D"gmail_default" style=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= "go wrong" in surprising=C2=A0ways. Consider the following progr= am (Sapio-pseudocode), which is= a non recursive covenant (i.e., doable today with presigning oracles) that= demonstrates the issue.

struct Pool {
=C2= =A0 =C2=A0 members: Vec<(Amount, Key)>,
}
impl Pool {
=C2=A0 =C2=A0 then!{
=C2=A0 = =C2=A0 =C2=A0 =C2=A0 fn withdraw(self, ctx) {
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 let mut builder =3D ctx.temp= late();
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 for (a, k) in self.members.iter() {
=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)?;
= =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 }
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 builder.into()
=C2=A0 =C2=A0 =C2=A0 =C2=A0 }
=C2=A0 =C2=A0 }
=C2=A0 =C2=A0 gua= rd! {
=C2=A0 =C2=A0 =C2=A0 =C2=A0 fn all_= signed(self, ctx) {
=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())
=C2=A0 =C2=A0 =C2= =A0 =C2=A0 }
=C2=A0 =C2=A0 }
=
=C2=A0 =C2=A0 finish! {
=C2=A0 =C2=A0 =C2=A0 =C2=A0 guarded_by: [all_signed]
=C2=A0 =C2=A0 =C2=A0 =C2=A0 fn add_member(self, ctx, o_mem= ber: Option<(Amount, Key)>) {
=C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 let member =3D o_member.into()?;
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 le= t mut new_members =3D self.members.clone();
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 new_members.push(member.clone(= ));
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 ctx.template().add_output(ctx.funds()=C2=A0+ member.0,
<= div class=3D"gmail_default" style=3D"font-size:small;color:rgb(0,0,0)">=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Pool {members: new_members}, None)?.into()
=C2=A0 =C2=A0 =C2=A0 =C2=A0 }
=C2=A0 =C2=A0 }
}

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.

=
This type of program is subtly &q= uot;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 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.

However, when we make the leap to "automatic" covenant= s, I posit that it will be *incredibly* difficult to prove that recursive c= ovenants don't have a "premature termination" 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.

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

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?

I don't= think that these sorts of challenges mean that we shouldn'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.

M= y personal view is that CTV/Sapio with it'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's an easy path for adding this s= ort of experimental feature to Sapio if anyone is looking for a place to st= art)

--000000000000fa954305c68bd7ae--