Re: [bitcoin-dev] Unlimited covenants, was Re: CHECKSIGFROMSTACK/{Verify} BIP for Bitcoin

[Jeremy <jlrubin@mit.edu>]

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

Hah -- ZmnSCPxj that post's a doozy -- but it more or less makes sense the
argument you're making in favor of permitting recursion at the transaction
level.

One part that's less clear is if you can make a case against being
recursive in Script fragments themselves -- ignoring bitcoin script for the
moment, what would be wrong with a small VM that a spender is able to
"purchase" a number of cycles and available memory via the annex, and the
program must execute and halt within that time? Then, per block/txn, you
can enforce a total cycle and memory limit. This still isn't quite the EVM,
since there's no cross object calling convention and the output is still
UTXOs. What are the arguments against this model from a safety perspective?

<new topic>

One of my general concerns with recursive covenants is the ability to "go
wrong" in surprising ways. Consider the following program (Sapio
<http://learn.sapio-lang.org>-pseudocode), which is a non recursive
covenant (i.e., doable today with presigning oracles) that demonstrates the
issue.

struct Pool {
    members: Vec<(Amount, Key)>,
}
impl Pool {
    then!{
        fn withdraw(self, ctx) {
            let mut builder = ctx.template();
            for (a, k) in self.members.iter() {
                builder = builder.add_output(a, k.into(), None)?;
            }
            builder.into()
        }
    }
    guard! {
        fn all_signed(self, ctx) {
            Clause::And(self.members.iter().map(|(a,k)|
Clause::Key(k.clone())).into())
        }
    }
    finish! {
        guarded_by: [all_signed]
        fn add_member(self, ctx, o_member: Option<(Amount, Key)>) {
            let member = o_member.into()?;
            let mut new_members = self.members.clone();
            new_members.push(member.clone());
            ctx.template().add_output(ctx.funds() + member.0,
                  Pool {members: new_members}, None)?.into()
        }
    }
}

Essentially this is a recursive covenant that allows either Complete via
the withdraw call or Continue via add_member, while preserving the same
underlying code. In this case, all_signed must be signed by all current
participants to admit a new member.

This type of program is subtly "wrong" because the state transition of
add_member does not verify that the Pool's future withdraw call will be
valid. E.g., we could add more than a 1MB of outputs, and then our program
would be "stuck". So it's critical that in our "production grade" covenant
system we do some static analysis before proceeding to a next step to
ensure that all future txns are valid. This is a strength of the CTV/Sapio
model presently, you always output a list of future txns to aid static
analysis.

However, when we make the leap to "automatic" covenants, I posit that it
will be *incredibly* difficult to prove that recursive covenants don't have
a "premature termination" where a state transition that should be valid in
an idealized setting is accidentally invalid in the actual bitcoin
environment and the program reaches a untimely demise.

For instance, OP_CAT has this footgun -- by only permitting 520 bytes, you
hit covenant limits at around 13 outputs assuming you are length checking
each one and not permitting bare script. We can avoid this specific footgun
some of the time by using SHA256STREAM instead, of course.

However, it is generally very difficult to avoid all sorts of issues. E.g.,
with the ability to generate/update tapscript trees, what happens when
through updating a well formed tapscript tree 128 times you bump an
important clause past the 129 depth limit?

I don't think that these sorts of challenges mean that we shouldn't enable
covenants or avoid enabling them, but rather that as we explore we should
add primitives in a methodical way and give users/toolchain builders
primitives that enable and or encourage safety and good program design.

My personal view is that CTV/Sapio with it's AOT compilation of automated
state transitions and ability to statically analyze is a concept that can
mature and be used in production in the near term. But the tooling to
safely do recursive computations at the txn level will take quite a bit
longer to mature, and we should be investing effort in producing
compilers/frameworks for emitting well formed programs before we get too in
the weeds on things like OP_TWEAK. (side note -- there's an easy path for
adding this sort of experimental feature to Sapio if anyone is looking for
a place to start)

[-- Attachment #2: Type: text/html, Size: 10550 bytes --]