[bitcoin-dev] A Calculus of Covenants

[Jeremy Rubin <jeremy.l.rubin@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 6687 bytes --]

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 #2: Type: text/html, Size: 12332 bytes --]