Return-Path: Received: from smtp3.osuosl.org (smtp3.osuosl.org [IPv6:2605:bc80:3010::136]) by lists.linuxfoundation.org (Postfix) with ESMTP id 53337C002D for ; Wed, 18 May 2022 17:08:59 +0000 (UTC) Received: from localhost (localhost [127.0.0.1]) by smtp3.osuosl.org (Postfix) with ESMTP id 3B9D161229 for ; Wed, 18 May 2022 17:08:59 +0000 (UTC) X-Virus-Scanned: amavisd-new at osuosl.org X-Spam-Flag: NO X-Spam-Score: -2.098 X-Spam-Level: X-Spam-Status: No, score=-2.098 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001, HTML_MESSAGE=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001] autolearn=ham autolearn_force=no Authentication-Results: smtp3.osuosl.org (amavisd-new); dkim=pass (2048-bit key) header.d=gmail.com Received: from smtp3.osuosl.org ([127.0.0.1]) by localhost (smtp3.osuosl.org [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id cusGFXqPG1yA for ; Wed, 18 May 2022 17:08:57 +0000 (UTC) X-Greylist: whitelisted by SQLgrey-1.8.0 Received: from mail-wr1-x433.google.com (mail-wr1-x433.google.com [IPv6:2a00:1450:4864:20::433]) by smtp3.osuosl.org (Postfix) with ESMTPS id 2D49160EED for ; Wed, 18 May 2022 17:08:57 +0000 (UTC) Received: by mail-wr1-x433.google.com with SMTP id h14so3600356wrc.6 for ; Wed, 18 May 2022 10:08:57 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:references:in-reply-to:from:date:message-id:subject:to; bh=oaSaofVGqLpAZdi9fakuu/Nr3Y5ktHfwn4yv0F/qNEs=; b=TTc1HEIVqHVF6bD3dfYRMuP7YR8fxyxUUzMZOFbIqrVQtGk+qozUA+ldKbM1sOV/Eo YUVV/XE0frcubzDe3rzlDNB/arNcqKcAnbFXStuViNJESytbcT2pc8p9xCqRm1Yxm4jw zi0UDNCLfmO3NcjHsKSjYE7PNGHEoAJ+wQ+JfvPdBJMb38oKOgKSWU8Cn6sTFvcTe4xk h749kyPvXh3GZ7AzIlJ2IAr1PmoIX9PTQQB7uRd54yMlsvw/H08cgU2ze59EP3ccA0ma I3pga0pzfIWHny1gvoWGOsvYEWBDQLHd5D2i9AfZjyYtW4cUmK/pBu7ErmmKgY/mTpoB yViA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to; bh=oaSaofVGqLpAZdi9fakuu/Nr3Y5ktHfwn4yv0F/qNEs=; b=vsuhtGxjfsPiFQXWfsA4sgcHeXu7ntJfkhNtdPoDl3h2fX2HAtBbKJ5LjnLW9Oo92M w7O9jmJEiWs+zROCyGsC4sBH3T7thNfoc29VRUvZUkNduJut6iJqKCINGjJKe7blcKq+ BCn84Vm09SxJlfER6F6aROS24FksnNN1lKY+wnG85WyTOh8pEI5UHDOTbBREeXlpCJIx bloDw0vSfPaO4StzZ/7CE574cpJF3j4Af/ISi6JPXRmOSfB9S70hIUGd+m/gIGuD6xMA ygWeddRemFL23ECHOoJnFAUhmBxmDUuZcAD80PxiCE9tzAHV/hIWtkRSogCzZ3KUtwDD f0SA== X-Gm-Message-State: AOAM530hbJQv/8qT+2L9TXHRuAzVKIh2Sn8xI3ZJm065cao58oGQDNu0 uaFGFIBkRDjQhf0VZZyK/WkOqiXRcM/0sZrZMpbuHP8aYR8= X-Google-Smtp-Source: ABdhPJx8KwkAwngJ+gWghGE6Cth7Ma3SSi0LfFpdEQQr3qHvfnfHL9psnhiXrbQ6JRozJmu+R/rBiViOCycQuKzr9fk= X-Received: by 2002:adf:ea11:0:b0:20d:768:da9f with SMTP id q17-20020adfea11000000b0020d0768da9fmr516690wrm.625.1652893734912; Wed, 18 May 2022 10:08:54 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Keagan McClelland Date: Wed, 18 May 2022 11:08:43 -0600 Message-ID: To: Jeremy Rubin , Bitcoin Protocol Discussion Content-Type: multipart/alternative; boundary="000000000000ebc80f05df4c4f4c" X-Mailman-Approved-At: Wed, 18 May 2022 17:44:47 +0000 Subject: Re: [bitcoin-dev] A Calculus of Covenants 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, 18 May 2022 17:08:59 -0000 --000000000000ebc80f05df4c4f4c Content-Type: text/plain; charset="UTF-8" > One must also analyze all the covenants that one *could* author using a primitive So as I've been contemplating this more, I'm realizing that a calculus of covenants themselves may not make as much sense as a broader calculus of Bitcoin transactions as a whole. I think this comment that you made in your followup solidified that position. If you have to analyze it in the context of all of the other opcodes that could potentially interact with it, you don't really have a closed algebra that you can really try to understand and evaluate. I'm still ruminating on what such a calculus would be, but it also makes me more convinced that Simplicity gets a lot right here. That said, there is probably an opportunity for a significantly more domain specific set of primitives than what simplicity offers that would allow you similar practical use cases but with a much more high level analysis. The way I think about this now is that most of the primitives in the Bitcoin script VM right now are constraints on the witness, you have a couple of opcodes that are constraints on the chain state, and then covenants are really a constraint on the body of the transaction that spends an input. I think most of the time we imagine covenants of output constraints but you can also imagine a hypothetical covenant that says, "this input may not be spent alongside any other inputs". This is still a constraint on the spending transaction despite the fact that it mentions nothing of the outputs, and I would still broadly think of this as a covenant. I think depending on how you define "family" and "state transition" it would tolerate this distinction. However, it definitely complicates the question of things like unrollability. Is a covenant that permits any output(s) but the input must be spent alone unrollable? Does the concept unrollable even make any sense when you aren't constraining the outputs? These thoughts aren't completely baked but I figured I'd jot them down while I was thinking about it. Keagan On Tue, Apr 12, 2022 at 9:04 AM Jeremy Rubin via bitcoin-dev < bitcoin-dev@lists.linuxfoundation.org> wrote: > note of clarification: > > this is from the perspective of a developer trying to build infrastructure > for covenants. from the perspective of bitcoin consensus, a covenant > enforcing primitve would be something like OP_TLUV and less so it's use in > conjunction with other opcodes, e.g. OP_AMOUNT. > > One must also analyze all the covenants that one *could* author using a > primitive, in some sense, to demonstrate that our understanding is > sufficient. As a trivial example, you could use > OP_DELETE_BITCOIN_ENTIRELY_IF_KNOWS_PREIMAGE_TO_X_OR_TLUV and just because > you could use it safely for TLUV would not mean we should add that opcode > if there's some way of using it negatively. > > Cheers, > > Jeremy > -- > @JeremyRubin > > > On Tue, Apr 12, 2022 at 10:33 AM Jeremy Rubin > wrote: > >> Sharing below a framework for thinking about covenants. It is most useful >> for modeling local covenants, that is, covenants where only one coin must >> be examined, and not multi-coin covenants whereby you could have issues >> with protocol forking requiring a more powerful stateful prover. It's the >> model I use in Sapio. >> >> I define a covenant primitive as follows: >> >> 1) A set of sets of transaction intents (a *family)*, potentially >> recursive or co-recursive (e.g., the types of state transitions that can be >> generated). These intents can also be represented by a language that >> generates the transactions, rather than the literal transactions >> themselves. We do the family rather than just sets at this level because to >> instantiate a covenant we must pick a member of the family to use. >> 2) A verifier generator function that generates a function that accepts >> an intent that is any element of one member of the family of intents and a >> proof for it and rejects others. >> 3) A prover generator function that generates a function that takes an >> intent that is any element of one member of the family and some extra data >> and returns either a new prover function, a finished proof, or a rejection >> (if not a valid intent). >> 4) A set of proofs that the Prover, Verifier, and a set of intents are >> "impedance matched", that is, all statements the prover can prove and all >> statements the verifier can verify are one-to-one and onto (or something >> similar), and that this also is one-to-one and onto with one element of the >> intents (a set of transactions) and no other. >> 5) A set of assumptions under which the covenant is verified (e.g., a >> multi-sig covenant with at least 1-n honesty, a multisig covenant with any >> 3-n honesty required, Sha256 collision resistance, DLog Hardness, a SGX >> module being correct). >> >> To instantiate a covenant, the user would pick a particular element of >> the set of sets of transaction intents. For example, in TLUV payment pool, >> it would be the set of all balance adjusting transactions and redemptions. *Note, >> we can 'cleave' covenants into separate bits -- e.g. one TLUV + some extra >> CTV paths can be 'composed', but the composition is not guaranteed to be >> well formed.* >> >> Once the user has a particular intent, they then must generate a verifier >> which can receive any member of the set of intents and accept it, and >> receive any transaction outside the intents and reject it. >> >> With the verifier in hand (or at the same time), the user must then >> generate a prover function that can make a proof for any intent that the >> verifier will accept. This could be modeled as a continuation system (e.g., >> multisig requires multiple calls into the prover), or it could be >> considered to be wrapped as an all-at-once function. The prover could be >> done via a multi-sig in which case the assumptions are stronger, but it >> still should be well formed such that the signers can clearly and >> unambiguously sign all intents and reject all non intents, otherwise the >> covenant is not well formed. >> >> The proofs of validity of the first three parts and the assumptions for >> them should be clear, but do not require generation for use. However, >> covenants which do not easily permit proofs are less useful. >> >> We now can analyze three covenants under this, plain CTV, 2-3 online >> multisig, 3-3 presigned + deleted. >> >> CTV: >> 1) Intent sets: the set of specific next transactions, with unbound >> inputs into it that can be mutated (but once the parent is known, can be >> filled in for all children). >> 2) Verifier: The transaction has the hash of the intent >> 3) Prover: The transaction itself and no other work >> 4) Proofs of impedance: trivial. >> 5) Assumptions: sha256 >> 6) Composition: Any two CTVs can be OR'd together as separate leafs >> >> 2-3 Multisig: >> 1) Intent: All possible sets of transactions, one set selected per >> instance >> 2) Verifier: At least 2 signed the transition >> 3) Prover: Receive some 'state' in the form of business logic to enforce, >> only sign if that is satisfied. Produce a signature. >> 4) Impedance: The business logic must cover the instance's Intent set and >> must not be able to reach any other non-intent >> 5) Assumptions: at least 2 parties are 'honest' for both liveness and for >> correctness, and the usual suspects (sha256, schnorr, etc) >> 6) Composition: Any two groups can be OR'd together, if the groups have >> different signers, then the assumptions expand >> >> 3-3 Presigned: >> Same as CTV except: >> 5) Assumptions: at least one party deletes their key after signing >> >> >> You can also think through other covenants like TLUV in this model. >> >> One useful question is the 'cardinality' of an intent set. The useful >> notion of this is both in magnitude but also contains. Obviously, many of >> these are infinite sets, but if one set 'contains' another then it is >> definitionally more powerful. Also, if a set of transitions is 'bigger' >> (work to do on what that means?) than another it is potentially more >> powerful. >> >> Another question is around composition of different covenants inside of >> an intent -- e.g., a TLUV that has a branch with a CTV or vice versa. We >> consider this outside the model, analysis should be limited to "with only >> these covenants what could you build". Obviously, one recursive primitive >> makes all primitives recursive. >> >> Another question is 'unrollability'. Can the intents, and the intents of >> the outputs of the intents, be unrolled into a representation for a >> specific instantiation? Or is that set of possible transactions infinite? >> How infinite? CTV is, e.g., unrollable. >> >> >> Last note on statefulness: The above has baked into it a notion of >> 'statelessness', but it's very possible and probably required that provers >> maintain some external state in order to prove (whether multisig or not). >> E.g., a multisig managing an account model covenant may need to track who >> is owed what. This data can sometimes be put e.g. in an op return, an extra >> tapleaf branch, or just considered exogenous to the covenant. But the idea >> that a prover isn't just deciding on what to do based on purely local >> information to an output descriptor is important. >> >> >> For Sapio in particular, this framework is useful because if you can >> answer the above questions on intents, and prover/verifier generators, then >> you would be able to generate tooling that could integrate your covenant >> into Sapio and have things work nicely. If you can't answer these questions >> (in code?) then your covenant might not be 'well formed'. The efficiency of >> a prover or verifier is out of scope of this framework, which focuses on >> the engineering + design, but can also be analyzed. >> >> >> Grateful for any and all feedback on this model and if there are examples >> that cannot be described within it, >> >> Jeremy >> >> >> >> >> -- >> @JeremyRubin >> > _______________________________________________ > bitcoin-dev mailing list > bitcoin-dev@lists.linuxfoundation.org > https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev > --000000000000ebc80f05df4c4f4c Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
>=C2=A0One must also analyze all the covenants that one=C2= =A0could=C2=A0author using a primitive

So as I= 've been contemplating this more, I'm realizing that a calculus of = covenants themselves may not make as much sense as a broader calculus of Bi= tcoin transactions as a whole. I think this comment that you made in your f= ollowup solidified that position. If you have to analyze it in the context = of all of the other opcodes that could potentially interact with it, you do= n't really have a closed algebra that you can really try to understand = and evaluate. I'm still ruminating on what such a calculus would be, bu= t it also makes me more convinced that Simplicity gets a lot right here. Th= at said, there is probably an opportunity for a significantly more domain s= pecific set of primitives than what simplicity offers that would allow you = similar practical use cases but with a much more high level analysis.

The way I think about this now is that most of = the primitives in the Bitcoin script VM right now are constraints on the wi= tness, you have a couple of opcodes that are constraints on the chain state= , and then covenants are really a constraint on the body of the transaction= that spends an input. I think most of the time we imagine covenants of out= put constraints but you can also imagine a hypothetical covenant that says,= "this input may not be spent alongside any other inputs". This i= s still a constraint on the spending transaction despite the fact that it m= entions nothing of the outputs, and I would still broadly think of this as = a covenant. I think depending on how you define "family" and &quo= t;state transition" it would tolerate this distinction. However, it de= finitely complicates the question of things like unrollability. Is a covena= nt that permits any output(s) but the input must be spent alone unrollable?= Does the concept unrollable even make any sense when you aren't constr= aining the outputs?

These thoughts aren= 9;t completely baked but I figured I'd jot them down while I was thinki= ng about it.

Keagan

=
On Tue, Ap= r 12, 2022 at 9:04 AM Jeremy Rubin via bitcoin-dev <bitcoin-dev@lists.linuxfoundation.org<= /a>> wrote:
<= div dir=3D"ltr">
note of clarification:<= /div>

this is from the perspective of a developer trying to build inf= rastructure for covenants. from the perspective of bitcoin consensus, a cov= enant enforcing primitve would be something like OP_TLUV and less so it'= ;s use in conjunction with other opcodes, e.g. OP_AMOUNT.

One= must also analyze all the covenants that one could=C2=A0author usin= g a primitive, in some sense, to demonstrate that our understanding is suff= icient. As a trivial example, you could use OP_DELETE_BITCOIN_ENTIRELY_IF_K= NOWS_PREIMAGE_TO_X_OR_TLUV and just because you could use it safely for TLU= V would not mean we should add that opcode if there's some way of using= it negatively.

Cheers,

Jeremy


On Tue, Apr 12= , 2022 at 10:33 AM Jeremy Rubin <jeremy.l.rubin@gmail.com> wrote:
Sharing below a framework for thinking about cove= nants. It is most useful for modeling local covenants, that is, covenants w= here only one coin must be examined, and not multi-coin covenants whereby y= ou could have issues with protocol forking requiring a more powerful statef= ul prover. It's the model I use in Sapio.

I define a covena= nt primitive as follows:

1) A set of sets of transaction intent= s (a family), potentially recursive or co-recursive (e.g., the types= of state transitions that can be generated). These intents can also be rep= resented by a language that generates the transactions, rather than the lit= eral transactions themselves. We do the family rather than just sets at thi= s level because to instantiate a covenant we must pick a member of the fami= ly to use.
2) A verifier generator= function that generates a function that accepts an intent that is any elem= ent of one member of the family of intents and a proof for it and rejects o= thers.
3) A prover generator funct= ion that generates a function that takes an intent that is any element of o= ne member of the family and some extra data and returns either a new prover= function, a finished proof, or a rejection (if not a valid intent).
<= div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif= ;font-size:small;color:rgb(0,0,0)">4) A set of proofs that the Prover, Veri= fier, and a set of intents are "impedance matched", that is, all = statements the prover can prove and all statements the verifier can verify = are one-to-one and onto (or something similar), and that this also is one-t= o-one and onto with one element of the intents (a set of transactions) and = no other.
5) A set of assumptions = under which the covenant is verified (e.g., a multi-sig covenant with at le= ast 1-n honesty, a multisig covenant with any 3-n honesty required, Sha256 = collision resistance, DLog Hardness, a SGX module being correct).

To instantiate a covena= nt, the user would pick a particular element of the set of sets of transact= ion intents. For example, in TLUV payment pool, it would be the set of all = balance adjusting transactions and redemptions. Note, we can 'cleave= ' covenants into separate bits -- e.g. one TLUV=C2=A0+ some extra CTV p= aths can be 'composed', but the composition is not guaranteed to be= well formed.

Once the user has a particular intent, they t= hen must generate a verifier which can receive any member of the set of int= ents and accept it, and receive any transaction outside the intents and rej= ect it.

With the verifier in hand (or at the same time), the us= er must then generate a prover function that can make a proof for any inten= t that the verifier will accept. This could be modeled as a continuation sy= stem (e.g., multisig requires multiple calls into the prover), or it could = be considered to be wrapped as an all-at-once function. The prover could be= done via a multi-sig in which case the assumptions are stronger, but it st= ill should be well formed such that the signers can clearly and unambiguous= ly sign all intents and reject all non intents, otherwise the covenant is n= ot well formed.

The proofs of validity of the first three parts= and the assumptions for them should be clear, but do not require generatio= n for use. However, covenants which do not easily permit proofs are less us= eful.

We now can analyze three covenants under this, plain CTV,= 2-3 online multisig, 3-3 presigned + deleted.

CTV:
1) Intent sets: the set of specific next tran= sactions, with unbound inputs into it that can be mutated (but once the par= ent is known, can be filled in for all children).
2) Verifier: The transaction has the hash of the intent
3) Prover: The transaction itself and= no other work
4) Proofs of impeda= nce: trivial.
5) Assumptions: sha2= 56
6) Composition: Any two CTVs ca= n be OR'd together as separate leafs

2-3 Multisig:
1) Intent: All possible sets of transactio= ns, one set selected per instance
2) Verifier: At least 2 signed the transition
3) Prover: Receive some 'state' in the form of busine= ss logic to enforce, only sign if that is satisfied. Produce a signature.
4) Impedance: The business logic mu= st cover the instance's Intent set and must not be able to reach any ot= her non-intent
5) Assumptions: at = least 2 parties are 'honest' for both liveness and for correctness,= and the usual suspects (sha256, schnorr, etc)
6) Composition: Any two groups can be OR'd together, if th= e groups have different signers, then the assumptions expand

3-= 3 Presigned:
Same as CTV except:
5) Ass= umptions: at least one party deletes their key after signing


=C2=A0You can also think through other covenants lik= e TLUV in this model.

One useful question is the 'cardinality' of an = intent set. The useful notion of this is both in magnitude but also contain= s. Obviously, many of these are infinite sets, but if one set 'contains= ' another then it is definitionally more powerful. Also, if a set of tr= ansitions is 'bigger' (work to do on what that means?) than another= it is potentially more powerful.

Another question is around composition of d= ifferent covenants inside of an intent -- e.g., a TLUV that has a branch wi= th a CTV or vice versa. We consider this outside the model, analysis should= be limited to "with only these covenants what could you build". = Obviously, one recursive primitive makes all primitives recursive.

Another qu= estion is 'unrollability'. Can the intents, and the intents of the = outputs of the intents, be unrolled into a representation for a specific in= stantiation? Or is that set of possible transactions infinite? How infinite= ? CTV is, e.g., unrollable.


Last note = on statefulness: The above has baked into it a notion of 'statelessness= ', but it's very possible and probably required that provers mainta= in some external state in order to prove (whether multisig or not). E.g., a= multisig managing an account model covenant may need to track who is owed = what. This data can sometimes be put e.g. in an op return, an extra tapleaf= branch, or just considered exogenous to the covenant. But the idea that a = prover isn't just deciding on what to do based on purely local informat= ion to an output descriptor is important.


For Sapio in particular, this framework is= useful because if you can answer the above questions on intents, and prove= r/verifier generators, then you would be able to generate tooling that coul= d integrate your covenant into Sapio and have things work nicely. If you ca= n't answer these questions (in code?) then your covenant might not be &= #39;well formed'. The efficiency of a prover or verifier is out of scop= e of this framework, which focuses on the engineering + design, but can als= o be analyzed.


Grateful for any and all feedback on this model and = if there are examples that cannot be described within it,

Jeremy

<= /div>



_______________________________________________
bitcoin-dev mailing list
= bitcoin-dev@lists.linuxfoundation.org
https://lists.linuxfoundation.org/mail= man/listinfo/bitcoin-dev
--000000000000ebc80f05df4c4f4c--