MIME-Version: 1.0
References: <CAD5xwhjBkKVuiPaRJZrsq+GcvSeht+SHvmmiH2MjnU2k1m_4gw@mail.gmail.com>
In-Reply-To: <CAD5xwhjBkKVuiPaRJZrsq+GcvSeht+SHvmmiH2MjnU2k1m_4gw@mail.gmail.com>
From: Jeremy Rubin <jeremy.l.rubin@gmail.com>
Date: Tue, 12 Apr 2022 11:03:57 -0400
Message-ID: <CAD5xwhggbrg0tvjs4Pc6p7LWuy4RDcSfTHaGZ0U-KV6Wyn+CXQ@mail.gmail.com>
To: Bitcoin development mailing list <bitcoin-dev@lists.linuxfoundation.org>
Content-Type: multipart/alternative; boundary="00000000000072633305dc765fe9"
Subject: Re: [bitcoin-dev] A Calculus of Covenants
Precedence: list

--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 <https://twitter.com/JeremyRubin>


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 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 <https://twitter.com/JeremyRubin>
>

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

<div dir=3D"ltr"><div class=3D"gmail_default" style=3D"font-family:arial,he=
lvetica,sans-serif;font-size:small;color:#000000">note of clarification:</d=
iv><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-s=
erif;font-size:small;color:#000000"><br></div><div class=3D"gmail_default" =
style=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:#0000=
00">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&#39;s use i=
n conjunction with other opcodes, e.g. OP_AMOUNT.</div><div class=3D"gmail_=
default" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;co=
lor:#000000"><br></div><div class=3D"gmail_default" style=3D"font-family:ar=
ial,helvetica,sans-serif;font-size:small;color:#000000">One must also analy=
ze all the covenants that one <i>could</i>=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&#39;s some way of using it negatively.<=
/div><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans=
-serif;font-size:small;color:#000000"><br></div><div class=3D"gmail_default=
" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:#00=
0000">Cheers,</div><div class=3D"gmail_default" style=3D"font-family:arial,=
helvetica,sans-serif;font-size:small;color:#000000"><br></div><div class=3D=
"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;font-size:s=
mall;color:#000000">Jeremy</div><div><div dir=3D"ltr" class=3D"gmail_signat=
ure" data-smartmail=3D"gmail_signature"><div dir=3D"ltr">--<br><a href=3D"h=
ttps://twitter.com/JeremyRubin" target=3D"_blank">@JeremyRubin</a><br></div=
></div></div><br></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" clas=
s=3D"gmail_attr">On Tue, Apr 12, 2022 at 10:33 AM Jeremy Rubin &lt;<a href=
=3D"mailto:jeremy.l.rubin@gmail.com">jeremy.l.rubin@gmail.com</a>&gt; wrote=
:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.=
8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204=
,204,204);padding-left:1ex"><div dir=3D"ltr"><div class=3D"gmail_default" s=
tyle=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,=
0,0)">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&#39;s =
the model I use in Sapio.</div><div class=3D"gmail_default" style=3D"font-f=
amily:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></di=
v><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-se=
rif;font-size:small;color:rgb(0,0,0)">I define a covenant primitive as foll=
ows:</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" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;c=
olor:rgb(0,0,0)">1) A set of sets of transaction intents (a <i>family)</i>,=
 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.</div><div=
 class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;fo=
nt-size:small;color:rgb(0,0,0)">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.</div><div cla=
ss=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;font-s=
ize:small;color:rgb(0,0,0)">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).</div><div class=3D"gmail_d=
efault" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;col=
or:rgb(0,0,0)">4) A set of proofs that the Prover, Verifier, and a set of i=
ntents are &quot;impedance matched&quot;, 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.</div><div =
class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;fon=
t-size:small;color:rgb(0,0,0)">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).</div><div><br></div><div><div=
 class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;fo=
nt-size:small;color:rgb(0,0,0)">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. <i>Note, we can &#39;cleave&#39; covenants into=
 separate bits -- e.g. one TLUV=C2=A0+ some extra CTV paths can be &#39;com=
posed&#39;, but the composition is not guaranteed to be well formed.</i></d=
iv><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-s=
erif;font-size:small;color:rgb(0,0,0)"><br></div><div class=3D"gmail_defaul=
t" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:rg=
b(0,0,0)">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.</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)=
">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.</d=
iv><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-s=
erif;font-size:small;color:rgb(0,0,0)"><br></div><div class=3D"gmail_defaul=
t" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:rg=
b(0,0,0)">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.</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)=
">We now can analyze three covenants under this, plain CTV, 2-3 online mult=
isig, 3-3 presigned + deleted.</div><div class=3D"gmail_default" style=3D"f=
ont-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,sa=
ns-serif;font-size:small;color:rgb(0,0,0)">CTV:</div><div class=3D"gmail_de=
fault" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;colo=
r:rgb(0,0,0)">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).</div><div class=3D"gmail_default" style=
=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)=
">2) Verifier: The transaction has the hash of the intent</div><div class=
=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;font-siz=
e:small;color:rgb(0,0,0)">3) Prover: The transaction itself and no other wo=
rk</div><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,s=
ans-serif;font-size:small;color:rgb(0,0,0)">4) Proofs of impedance: trivial=
.</div><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sa=
ns-serif;font-size:small;color:rgb(0,0,0)">5) Assumptions: sha256</div><div=
 class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;fo=
nt-size:small;color:rgb(0,0,0)">6) Composition: Any two CTVs can be OR&#39;=
d together as separate leafs</div><div class=3D"gmail_default" style=3D"fon=
t-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)">2-3 Multisig:</div><div class=3D"g=
mail_default" style=3D"font-family:arial,helvetica,sans-serif;font-size:sma=
ll;color:rgb(0,0,0)">1) Intent: All possible sets of transactions, one set =
selected per instance</div><div class=3D"gmail_default" style=3D"font-famil=
y:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">2) Verifier:=
 At least 2 signed the transition</div><div class=3D"gmail_default" style=
=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)=
">3) Prover: Receive some &#39;state&#39; in the form of business logic to =
enforce, only sign if that is satisfied. Produce a signature.</div><div cla=
ss=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;font-s=
ize:small;color:rgb(0,0,0)">4) Impedance: The business logic must cover the=
 instance&#39;s Intent set and must not be able to reach any other non-inte=
nt</div><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,s=
ans-serif;font-size:small;color:rgb(0,0,0)">5) Assumptions: at least 2 part=
ies are &#39;honest&#39; for both liveness and for correctness, and the usu=
al suspects (sha256, schnorr, etc)</div><div class=3D"gmail_default" style=
=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)=
">6) Composition: Any two groups can be OR&#39;d together, if the groups ha=
ve different signers, then the assumptions expand</div><div class=3D"gmail_=
default" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;co=
lor: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)">3-3 Presigned=
:</div><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sa=
ns-serif;font-size:small;color:rgb(0,0,0)">Same as CTV except:</div><div cl=
ass=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;font-=
size:small;color:rgb(0,0,0)"><div class=3D"gmail_default">5) Assumptions: a=
t least one party deletes their key after signing</div><div class=3D"gmail_=
default"><br></div><div class=3D"gmail_default"><br></div><div class=3D"gma=
il_default">=C2=A0You can also think through other covenants like TLUV in t=
his model.</div><div class=3D"gmail_default"><br></div><div class=3D"gmail_=
default">One useful question is the &#39;cardinality&#39; 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 &#39;contains&#39; anoth=
er then it is definitionally more powerful. Also, if a set of transitions i=
s &#39;bigger&#39; (work to do on what that means?) than another it is pote=
ntially more powerful.</div><div class=3D"gmail_default"><br></div><div cla=
ss=3D"gmail_default">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 &quot;with only these covenants what could you build&quot;. Obviously, =
one recursive primitive makes all primitives recursive.</div><div class=3D"=
gmail_default"><br></div><div class=3D"gmail_default">Another question is &=
#39;unrollability&#39;. 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.</div><div class=3D"gmail_default"><br></div><div class=3D"=
gmail_default"><br></div><div class=3D"gmail_default">Last note on stateful=
ness: The above has baked into it a notion of &#39;statelessness&#39;, but =
it&#39;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.</div><div class=3D"gmail_default"><br></div>=
<div class=3D"gmail_default"><br></div><div class=3D"gmail_default"><div cl=
ass=3D"gmail_default">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&#39;t ans=
wer these questions (in code?) then your covenant might not be &#39;well fo=
rmed&#39;. 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.</div><br></div><div class=3D"gmail_default"><br></div><div class=3D"gma=
il_default">Grateful for any and all feedback on this model and if there ar=
e examples that cannot be described within it,</div><div class=3D"gmail_def=
ault"><br></div><div class=3D"gmail_default">Jeremy</div><br></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)"><=
br></div><br></div><div><div dir=3D"ltr"><div dir=3D"ltr">--<br><a href=3D"=
https://twitter.com/JeremyRubin" target=3D"_blank">@JeremyRubin</a><br></di=
v></div></div></div>
</blockquote></div>

--00000000000072633305dc765fe9--