[prev in list] [next in list] [prev in thread] [next in thread]
List: bitcoin-dev
Subject: Re: [bitcoin-dev] A Calculus of Covenants
From: Jeremy Rubin via bitcoin-dev <bitcoin-dev () lists ! linuxfoundation ! org>
Date: 2022-04-12 15:03:57
Message-ID: CAD5xwhggbrg0tvjs4Pc6p7LWuy4RDcSfTHaGZ0U-KV6Wyn+CXQ () mail ! gmail ! com
[Download RAW message or body]
[Attachment #2 (multipart/alternative)]
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>
>
[Attachment #5 (text/html)]
<div dir="ltr"><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:#000000">note of \
clarification:</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:#000000"><br></div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:#000000">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.</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:#000000"><br></div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:#000000">One must \
also analyze all the covenants that one <i>could</i> 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.</div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:#000000"><br></div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:#000000">Cheers,</div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:#000000"><br></div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:#000000">Jeremy</div><div><div \
dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div \
dir="ltr">--<br><a href="https://twitter.com/JeremyRubin" \
target="_blank">@JeremyRubin</a><br></div></div></div><br></div><br><div \
class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Apr 12, 2022 at 10:33 \
AM Jeremy Rubin <<a \
href="mailto:jeremy.l.rubin@gmail.com">jeremy.l.rubin@gmail.com</a>> \
wrote:<br></div><blockquote class="gmail_quote" style="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="ltr"><div class="gmail_default" \
style="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 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.</div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">I \
define a covenant primitive as follows:</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color: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 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="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">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="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size: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 family and some extra data and returns either a new \
prover function, a finished proof, or a rejection (if not a valid intent).</div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">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.</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">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).</div><div><br></div><div><div class="gmail_default" \
style="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 set of all \
balance adjusting transactions and redemptions. <i>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.</i></div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(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 class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><div \
class="gmail_default" \
style="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 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.</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">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.</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><div \
class="gmail_default" \
style="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 multisig, 3-3 \
presigned + deleted.</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">CTV:</div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;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 once the parent is known, can be filled in for all \
children).</div><div class="gmail_default" \
style="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="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">3) \
Prover: The transaction itself and no other work</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">4) \
Proofs of impedance: trivial.</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">5) \
Assumptions: sha256</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">6) \
Composition: Any two CTVs can be OR'd together as separate leafs</div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">2-3 \
Multisig:</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">1) \
Intent: All possible sets of transactions, one set selected per instance</div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">2) \
Verifier: At least 2 signed the transition</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">3) \
Prover: Receive some 'state' in the form of business logic to enforce, only \
sign if that is satisfied. Produce a signature.</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">4) \
Impedance: The business logic must cover the instance's Intent set and must not \
be able to reach any other non-intent</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">5) \
Assumptions: at least 2 parties are 'honest' for both liveness and for \
correctness, and the usual suspects (sha256, schnorr, etc)</div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">6) \
Composition: Any two groups can be OR'd together, if the groups have different \
signers, then the assumptions expand</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">3-3 \
Presigned:</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)">Same \
as CTV except:</div><div class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><div \
class="gmail_default">5) Assumptions: at least one party deletes their key after \
signing</div><div class="gmail_default"><br></div><div \
class="gmail_default"><br></div><div class="gmail_default"> You can also think \
through other covenants like TLUV in this model.</div><div \
class="gmail_default"><br></div><div class="gmail_default">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.</div><div class="gmail_default"><br></div><div \
class="gmail_default">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.</div><div class="gmail_default"><br></div><div \
class="gmail_default">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.</div><div class="gmail_default"><br></div><div \
class="gmail_default"><br></div><div class="gmail_default">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.</div><div \
class="gmail_default"><br></div><div class="gmail_default"><br></div><div \
class="gmail_default"><div class="gmail_default">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.</div><br></div><div class="gmail_default"><br></div><div \
class="gmail_default">Grateful for any and all feedback on this model and if there \
are examples that cannot be described within it,</div><div \
class="gmail_default"><br></div><div class="gmail_default">Jeremy</div><br></div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><div \
class="gmail_default" \
style="font-family:arial,helvetica,sans-serif;font-size:small;color:rgb(0,0,0)"><br></div><br></div><div><div \
dir="ltr"><div dir="ltr">--<br><a href="https://twitter.com/JeremyRubin" \
target="_blank">@JeremyRubin</a><br></div></div></div></div> </blockquote></div>
_______________________________________________
bitcoin-dev mailing list
bitcoin-dev@lists.linuxfoundation.org
https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic