summaryrefslogtreecommitdiff
path: root/65/b30de3546b7f4f9a134763b7a944ea54bee998
blob: af03ee5a417d6f622fe03a53f945bec6290bd936 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
Return-Path: <jeremy.l.rubin@gmail.com>
Received: from smtp3.osuosl.org (smtp3.osuosl.org [IPv6:2605:bc80:3010::136])
 by lists.linuxfoundation.org (Postfix) with ESMTP id 33559C002C
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Tue, 12 Apr 2022 14:33:30 +0000 (UTC)
Received: from localhost (localhost [127.0.0.1])
 by smtp3.osuosl.org (Postfix) with ESMTP id 220D761031
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Tue, 12 Apr 2022 14:33:30 +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 hsqnqCLL7eqa
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Tue, 12 Apr 2022 14:33:28 +0000 (UTC)
X-Greylist: whitelisted by SQLgrey-1.8.0
Received: from mail-lj1-x22f.google.com (mail-lj1-x22f.google.com
 [IPv6:2a00:1450:4864:20::22f])
 by smtp3.osuosl.org (Postfix) with ESMTPS id 54DFB60093
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Tue, 12 Apr 2022 14:33:28 +0000 (UTC)
Received: by mail-lj1-x22f.google.com with SMTP id bn33so24307175ljb.6
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Tue, 12 Apr 2022 07:33:28 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
 h=mime-version:from:date:message-id:subject:to;
 bh=OfIaHFShKTIWzbq0oEARcd0E6f/dSCrZc6EUwVz94bM=;
 b=giZxAUnn5xINuTmMLXDE6AvZuOZds7Zt7GbRabPICfaek49dJssM3CFvN73wmcDHsY
 t0OYmP0m7g59TSeB0WYNNLIKQ2zhjq3bAZCmU1zxTgxLkwvMHAaB83UztBH5GrOYILqj
 uubaE6uIyaqVseUCDKeaiKq0Tfn5Q+pLUDjeSgmS/8pcRbAMhZfBsuN2sfreYK8wRRbt
 UjeO/6mSPD9TZzQ6KNF1cKqUW9TlP0JwJx4n89AQXplYIfU9ETKEcPE/1s9SzJJL2iyC
 FEcZsQQVYlJN81AXLHIkNoS4mLPcuqtgrvi8/fO8/l19klbqhXdvGPkadoDsuydIC9cO
 Nx5Q==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20210112;
 h=x-gm-message-state:mime-version:from:date:message-id:subject:to;
 bh=OfIaHFShKTIWzbq0oEARcd0E6f/dSCrZc6EUwVz94bM=;
 b=e33YTz/6kS8D3G486qsIHcp05WxWPjjDXGm/cacDOdKc+3OUEEHKdyxifqeMc3MRY5
 bAeBGLGYyWakq1J+Rb6bX9m1gkOhHJzD6sTb+1z0vDMEkhgufY4Fkm7o/Qd9Xk7JthHa
 cE4WYmpNdmo/bp7idWQt7kWaOtjWsLHpJjZAGkmALP6zl/eA4cM2uUc0er0P8FBMaw6/
 gASb+z9NTx3Q8pf/sMjg8gFOTzI8is3jHsJ+lb30qzMU7psryi/p2hgLs9PFtPSjyq6p
 IocgdKFFEk7UR/6ca9+9/sMFYTDg06cjYRHWwYvROuZl9E0ByXoi+fQ+pLRsY2N7lCd9
 VpwA==
X-Gm-Message-State: AOAM530T5IvMpsf9xNvDYkAP3AZ3cF6OYQco/eOBP8OXK4ePdAdPRuMW
 BkwdB/5xF3DknyrFLBQfKJN2vnCULQzhBRjCNr0PK2T2pLE=
X-Google-Smtp-Source: ABdhPJwNFaE5Qcf+IgyxNsTNNsT/OmXZClM4sovR/zzc1QrThxfVHy7MWt1wRxWP6O0GIaWnmbYvXw5AqVuARsuSO/o=
X-Received: by 2002:a2e:b0e3:0:b0:24b:53ec:9bf0 with SMTP id
 h3-20020a2eb0e3000000b0024b53ec9bf0mr12797650ljl.227.1649774005468; Tue, 12
 Apr 2022 07:33:25 -0700 (PDT)
MIME-Version: 1.0
From: Jeremy Rubin <jeremy.l.rubin@gmail.com>
Date: Tue, 12 Apr 2022 10:33:14 -0400
Message-ID: <CAD5xwhjBkKVuiPaRJZrsq+GcvSeht+SHvmmiH2MjnU2k1m_4gw@mail.gmail.com>
To: Bitcoin development mailing list <bitcoin-dev@lists.linuxfoundation.org>
Content-Type: multipart/alternative; boundary="0000000000008e411f05dc75f1af"
Subject: [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 <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: Tue, 12 Apr 2022 14:33:30 -0000

--0000000000008e411f05dc75f1af
Content-Type: text/plain; charset="UTF-8"

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>

--0000000000008e411f05dc75f1af
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">Sharing below a framework=
 for thinking about covenants. It is most useful for modeling local covenan=
ts, that is, covenants where only one coin must be examined, and not multi-=
coin covenants whereby you could have issues with protocol forking requirin=
g a more powerful stateful prover. It&#39;s the model I use in Sapio.</div>=
<div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-seri=
f;font-size:small;color:#000000"><br></div><div class=3D"gmail_default" sty=
le=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:#000000"=
>I define a covenant primitive as follows:</div><div class=3D"gmail_default=
" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:#00=
0000"><br></div><div class=3D"gmail_default" style=3D"font-family:arial,hel=
vetica,sans-serif;font-size:small;color:#000000">1) A set of sets of transa=
ction intents (a <i>family)</i>, 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.</div><div class=3D"gmail_default" style=3D"font-fami=
ly:arial,helvetica,sans-serif;font-size:small;color:#000000">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.</div><div class=3D"gmail_default" style=3D"font-family:aria=
l,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">3) A prover genera=
tor function that generates a function that takes an intent that is any ele=
ment of one member of the family and some extra data and returns either a n=
ew prover function, a finished proof, or a rejection (if not a valid intent=
).</div><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,s=
ans-serif;font-size:small;color:rgb(0,0,0)">4) A set of proofs that the Pro=
ver, Verifier, and a set of intents are &quot;impedance matched&quot;, that=
 is, all statements the prover can prove and all statements the verifier ca=
n 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 transacti=
ons) and no other.</div><div class=3D"gmail_default" style=3D"font-family:a=
rial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">5) A set of ass=
umptions under which the covenant is verified (e.g., a multi-sig covenant w=
ith at least 1-n honesty, a multisig 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;font-size:small;color:rgb(0,0,0)">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 se=
t of all balance adjusting transactions and redemptions. <i>Note, we can &#=
39;cleave&#39; covenants into separate bits -- e.g. one TLUV=C2=A0+ some ex=
tra CTV paths can be &#39;composed&#39;, but the composition is not guarant=
eed to be well formed.</i></div><div class=3D"gmail_default" style=3D"font-=
family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></d=
iv><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-s=
erif;font-size:small;color:rgb(0,0,0)">Once the user has a particular inten=
t, they then must generate a verifier which can receive any member of the s=
et of intents and accept it, and receive any transaction outside the intent=
s and reject it.</div><div class=3D"gmail_default" style=3D"font-family:ari=
al,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><div cl=
ass=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 generate a prover function that can make a proof for =
any intent that the verifier will accept. This could be modeled as a contin=
uation 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 un=
ambiguously sign all intents and reject all non intents, otherwise the cove=
nant is not well formed.</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-family:arial,helvetica,sans-ser=
if;font-size:small;color:rgb(0,0,0)">The proofs of validity of the first th=
ree parts and the assumptions for them should be clear, but do not require =
generation for use. However, covenants which do not easily permit proofs ar=
e less useful.</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 clas=
s=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;font-si=
ze:small;color:rgb(0,0,0)">We now can analyze three covenants under this, p=
lain CTV, 2-3 online multisig, 3-3 presigned + deleted.</div><div class=3D"=
gmail_default" style=3D"font-family:arial,helvetica,sans-serif;font-size:sm=
all;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)">CTV:</d=
iv><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-s=
erif;font-size:small;color:rgb(0,0,0)">1) Intent sets: the set of specific =
next transactions, with unbound inputs into it that can be mutated (but onc=
e the parent is known, can be filled in for all children).</div><div class=
=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;font-siz=
e: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,helveti=
ca,sans-serif;font-size:small;color:rgb(0,0,0)">3) Prover: The transaction =
itself and no other work</div><div class=3D"gmail_default" style=3D"font-fa=
mily:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">4) Proofs=
 of impedance: trivial.</div><div class=3D"gmail_default" style=3D"font-fam=
ily:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">5) Assumpt=
ions: sha256</div><div class=3D"gmail_default" style=3D"font-family:arial,h=
elvetica,sans-serif;font-size:small;color:rgb(0,0,0)">6) Composition: Any t=
wo CTVs can be OR&#39;d together as separate leafs</div><div class=3D"gmail=
_default" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;c=
olor:rgb(0,0,0)"><br></div><div class=3D"gmail_default" style=3D"font-famil=
y:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">2-3 Multisig=
:</div><div class=3D"gmail_default" style=3D"font-family:arial,helvetica,sa=
ns-serif;font-size:small;color:rgb(0,0,0)">1) Intent: All possible sets of =
transactions, one set selected per instance</div><div class=3D"gmail_defaul=
t" style=3D"font-family:arial,helvetica,sans-serif;font-size:small;color:rg=
b(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:sm=
all;color:rgb(0,0,0)">3) Prover: Receive some &#39;state&#39; in the form o=
f business logic to enforce, only sign if that is satisfied. Produce a sign=
ature.</div><div class=3D"gmail_default" style=3D"font-family:arial,helveti=
ca,sans-serif;font-size: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 reac=
h any other non-intent</div><div class=3D"gmail_default" style=3D"font-fami=
ly:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">5) Assumpti=
ons: at least 2 parties are &#39;honest&#39; for both liveness and for corr=
ectness, and the usual suspects (sha256, schnorr, etc)</div><div class=3D"g=
mail_default" style=3D"font-family:arial,helvetica,sans-serif;font-size:sma=
ll;color:rgb(0,0,0)">6) Composition: Any two groups can be OR&#39;d togethe=
r, if the groups have different signers, then the assumptions expand</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)">3-3 Presigned:</div><div class=3D"gmail_default" style=3D"font-family=
:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">Same as CTV e=
xcept:</div><div class=3D"gmail_default" style=3D"font-family:arial,helveti=
ca,sans-serif;font-size:small;color:rgb(0,0,0)"><div class=3D"gmail_default=
">5) Assumptions: at least one party deletes their key after signing</div><=
div class=3D"gmail_default"><br></div><div class=3D"gmail_default"><br></di=
v><div class=3D"gmail_default">=C2=A0You can also think through other coven=
ants like TLUV in this 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. Obviously, many of these are infinite sets, but if one set &#39;=
contains&#39; another then it is definitionally more powerful. Also, if a s=
et of transitions is &#39;bigger&#39; (work to do on what that means?) than=
 another it is potentially more powerful.</div><div class=3D"gmail_default"=
><br></div><div class=3D"gmail_default">Another question is around composit=
ion of different covenants inside of an intent -- e.g., a TLUV that has a b=
ranch with a CTV or vice versa. We consider this outside the model, analysi=
s 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">An=
other question is &#39;unrollability&#39;. Can the intents, and the intents=
 of the outputs of the intents, be unrolled into a representation for a spe=
cific 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">La=
st note on statefulness: The above has baked into it a notion of &#39;state=
lessness&#39;, but it&#39;s very possible and probably required that prover=
s 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&#39;t just deciding on what to do based on purely local =
information to an output descriptor is important.</div><div class=3D"gmail_=
default"><br></div><div class=3D"gmail_default"><br></div><div class=3D"gma=
il_default"><div class=3D"gmail_default">For Sapio in particular, this fram=
ework is useful because if you can answer the above questions on intents, a=
nd prover/verifier generators, then you would be able to generate tooling t=
hat could integrate your covenant into Sapio and have things work nicely. I=
f you can&#39;t answer these questions (in code?) then your covenant might =
not be &#39;well formed&#39;. 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.</div><br class=3D"gmail-Apple-interchange-newline"><=
/div><div class=3D"gmail_default"><br></div><div class=3D"gmail_default">Gr=
ateful for any and all feedback on this model and if there are examples tha=
t cannot be described within it,</div><div class=3D"gmail_default"><br></di=
v><div class=3D"gmail_default">Jeremy</div><br class=3D"gmail-Apple-interch=
ange-newline"></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 clas=
s=3D"gmail_default" style=3D"font-family:arial,helvetica,sans-serif;font-si=
ze:small;color:rgb(0,0,0)"><br></div><br></div><div><div dir=3D"ltr" class=
=3D"gmail_signature" data-smartmail=3D"gmail_signature"><div dir=3D"ltr">--=
<br><a href=3D"https://twitter.com/JeremyRubin" target=3D"_blank">@JeremyRu=
bin</a><br></div></div></div></div>

--0000000000008e411f05dc75f1af--