Re: [bitcoin-dev] A Calculus of Covenants

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

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

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