Return-Path: Received: from smtp2.osuosl.org (smtp2.osuosl.org [140.211.166.133]) by lists.linuxfoundation.org (Postfix) with ESMTP id 99B14C002C for ; Tue, 12 Apr 2022 15:04:13 +0000 (UTC) Received: from localhost (localhost [127.0.0.1]) by smtp2.osuosl.org (Postfix) with ESMTP id 8647C40AFD for ; Tue, 12 Apr 2022 15:04:13 +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: smtp2.osuosl.org (amavisd-new); dkim=pass (2048-bit key) header.d=gmail.com Received: from smtp2.osuosl.org ([127.0.0.1]) by localhost (smtp2.osuosl.org [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 4tKk6MaLOuF0 for ; Tue, 12 Apr 2022 15:04:12 +0000 (UTC) X-Greylist: whitelisted by SQLgrey-1.8.0 Received: from mail-lf1-x136.google.com (mail-lf1-x136.google.com [IPv6:2a00:1450:4864:20::136]) by smtp2.osuosl.org (Postfix) with ESMTPS id B364540AFC for ; Tue, 12 Apr 2022 15:04:11 +0000 (UTC) Received: by mail-lf1-x136.google.com with SMTP id bu29so32813168lfb.0 for ; Tue, 12 Apr 2022 08:04:11 -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=ycBi3NH0THsDn7GPbGuN71Z9OZQa1V89SZvCtmI/UZA=; b=oUufCnYWWcK7sDO9Uum1JZ8ypwyTVBpZkIX8xqLbk2bOsdpxQl3nFSfZsO/4SBiWb8 1+BSgJg06dgBVysUW5hinUi+6/r/oaQS8IzYPXow8FBkhibO17pya6njbF8hkjWQdL0r nZHPTl/d954eTrruXNsRf9wEDyJrlCqE6rywNofTUvMVPiXGw6NdiUcTfKjqGmMXbTBD PkqKg7lXZfPyUzbC8khjCdxlbB7cJ1jrw3JUVkus2ATGdt1EMmo8fMqzfaPkCi10iOgn r/gp7eFKEXMSC028fnk2iRREHxGMZa43Ib0EZN53LFpIgZgPkI9FhOhfmQA1BaBnAd4D RZHA== 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=ycBi3NH0THsDn7GPbGuN71Z9OZQa1V89SZvCtmI/UZA=; b=6Fs1BTmkuA0ZHicJBO3tPqMcYRXlMELnA6ASFSV9E/K5Cs9renpMo6we6/PcHA93gT MCxUxE/GjV3loKqmvS/B3jdoJUJdZ8uQ4B0AqNcjyfsmnSoKJHfoc/J7oAbuvK2oFDxn NoSZ6yhSraKJfJuZh5B588tqd+sGxvhChXPf763Ev2xmfYAtb3nrMPNTnsM6a2eXTl9n tkOF3wSuoxt9EYCR6W7lKV3j+5loxRgbsdOE6H0zyaJUumgwnm8SVYNnAgttDyQ3MCP1 D6G4Les1VBcMC3lp3FZsnClzwvfD2RBqhbhsJ39IWRSTQHQV0p+gvZ+e4AKi95wSFjnY zXPw== X-Gm-Message-State: AOAM533NNctoU7oOQcMv9M3kZTdy6eR7wXJqMu1jXorxBDjg80Vj19yh iL+r6fHLIkiveZh6VlN5EmZlK4Ry6GsSh9aJLI3IM+/v X-Google-Smtp-Source: ABdhPJyRBIIQsV4gXsaPuhXV1ag2s3M0dZFX5Hw75XaGTkvNSlfvK3JQQWHIz2At4qGF1hjJ9a22nLPIOBkcd8pFHu0= X-Received: by 2002:ac2:4c41:0:b0:46b:8bc6:4607 with SMTP id o1-20020ac24c41000000b0046b8bc64607mr13923002lfk.516.1649775849135; Tue, 12 Apr 2022 08:04:09 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Jeremy Rubin Date: Tue, 12 Apr 2022 11:03:57 -0400 Message-ID: To: Bitcoin development mailing list Content-Type: multipart/alternative; boundary="00000000000072633305dc765fe9" 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: Tue, 12 Apr 2022 15:04:13 -0000 --00000000000072633305dc765fe9 Content-Type: text/plain; charset="UTF-8" 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 > --00000000000072633305dc765fe9 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
note of clarification:

this is from the perspective of a developer trying to build infrastruct= ure for covenants. from the perspective of bitcoin consensus, a covenant en= forcing primitve would be something like OP_TLUV and less so it's use i= n conjunction with other opcodes, e.g. OP_AMOUNT.

One must also analy= ze all the covenants that one could=C2=A0author using a primitive, i= n some sense, to demonstrate that our understanding is sufficient. As a tri= vial 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.<= /div>

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 covenants. It is most us= eful for modeling local covenants, that is, covenants where only one coin m= ust 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 foll= ows:

1) A set of sets of transaction intents (a family),= potentially recursive or co-recursive (e.g., the types of state transition= s that can be generated). These intents can also be represented by a langua= ge that generates the transactions, rather than the literal transactions th= emselves. We do the family rather than just sets at this level because to i= nstantiate a covenant we must pick a member of the family to use.
2) A verifier generator function that gener= ates 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 fam= ily and some extra data and returns either a new prover function, a finishe= d proof, or a rejection (if not a valid intent).
4) A set of proofs that the Prover, Verifier, and a set of i= ntents are "impedance matched", that is, all statements the prove= r can prove and all statements the verifier can verify are one-to-one and o= nto (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 cove= nant is verified (e.g., a multi-sig covenant with at least 1-n honesty, a m= ultisig covenant with any 3-n honesty required, Sha256 collision resistance= , DLog Hardness, a SGX module being correct).

To instantiate a covenant, the user would p= ick a particular element of the set of sets of transaction intents. For exa= mple, in TLUV payment pool, it would be the set of all balance adjusting tr= ansactions and redemptions. Note, we can 'cleave' covenants into= separate bits -- e.g. one TLUV=C2=A0+ some extra CTV paths can be 'com= posed', 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 gener= ate a prover function that can make a proof for any intent that the verifie= r will accept. This could be modeled as a continuation system (e.g., multis= ig requires multiple calls into the prover), or it could be considered to b= e 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 intent= s and reject all non intents, otherwise the covenant is not well formed.

The proofs of validity of the first three parts and the assumptio= ns 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 mult= isig, 3-3 presigned + deleted.
CTV:
1) Intent sets: the set of specific next transactions, with u= nbound inputs into it that can be mutated (but once the parent is known, ca= n be filled in for all children).
2) Verifier: The transaction has the hash of the intent
3) Prover: The transaction itself and no other wo= rk
4) Proofs of impedance: trivial= .
5) Assumptions: sha256
6) Composition: Any two CTVs can be OR'= d together as separate leafs

<= /div>
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-inte= nt
5) Assumptions: at least 2 part= ies are 'honest' for both liveness and for correctness, and the usu= al suspects (sha256, schnorr, etc)
6) Composition: Any two groups can be OR'd together, if the groups ha= ve different signers, then the assumptions expand

3-3 Presigned= :
Same as CTV except:
5) Assumptions: a= t least one party deletes their key after signing


=C2=A0You can also think through other covenants like TLUV in t= his model.

One useful question is the 'cardinality' of an intent set.= The useful notion of this is both in magnitude but also contains. Obviousl= y, many of these are infinite sets, but if one set 'contains' anoth= er then it is definitionally more powerful. Also, if a set of transitions i= s 'bigger' (work to do on what that means?) than another it is pote= ntially more powerful.

Another question is around composition of different co= venants 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 &= #39;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 stateful= ness: The above has baked into it a notion of 'statelessness', but = it's very possible and probably required that provers maintain some ext= ernal state in order to prove (whether multisig or not). E.g., a multisig m= anaging 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&= #39;t just deciding on what to do based on purely local information to an o= utput descriptor is important.

=

For Sapio in particular, this framework is useful bec= ause 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 ans= wer these questions (in code?) then your covenant might not be 'well fo= rmed'. The efficiency of a prover or verifier is out of scope of this f= ramework, which focuses on the engineering + design, but can also be analyz= ed.


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

Jeremy


<= br>

--00000000000072633305dc765fe9--