Signature re-use and Miniscript

This is more of a blog post than an issue, but not sure where best to file it to get some comments.

In https://github.com/rust-bitcoin/rust-miniscript/pull/906#issuecomment-4878080548 Jeremy Rubin makes the interesting observation that the Miniscript

<bob> checksigverify IF 12 CSV <Alice> ELSE <Carol> ENDIF Checksig

has the semantic "Bob signs, then depending on circumstances, either Alice or Carol signs". However if we were to split this up into two tapbranches, the semantic is slightly changed: now Bob's signature is tied to one branch or the other, so to get the previous semantics, Bob would need to sign both branches. (And if he chose not to, he could hold funds hostage or otherwise potentially gum up a protocol.)

In many past private discussions, we've viewed this "signatures can be reused across branches" possibility as a sort of vulnerability, or at least an unintended consequence of Bitcoin's sighash algorithm, and we've speculated about adding a new pk_k-type fragment which included a CODESEPARATOR opcode. We've not done this because CODESEPARATOR is poorly supported by wallets, would waste an extra byte per key, and equivalent semantics can be obtained by just making sure each branch has a distinct key.

Indeed, our "sanity" rules forbid duplicate keys in both Miniscript and Policy. And we've considered that we should be able to relax this rule to allow duplicate keys as long as they appear in distinct tabbranches. But we haven't done this relaxation either because Policy currently lacks a way to indicate a "tapbranch or". Historically we've basically let the compiler do anything that's possible/well-typed, and trusted the Miniscript type system to prevent this from causing surprises. We knew, at least in principle, that CODESEP might mess this up. Jeremy's point is that even Taproot has messed this up.

My thought is that if we've already broken this seal, let's go ahead and add a pk variant with CODESEPARATOR. But curiously, this has weird/surprising semnatics and doesn't do what we want! Let's return to Jeremy's example to see why. Imagine now that Alice and Carol each use the codesep-bearing pk_k:

<bob> checksigverify IF 12 CSV <Alice> CODESEP ELSE <Carol> CODESEP ENDIF Checksig

Here we retain the original "Bob signs and walks away, and Alice and Carol figure out the rest of the witness" scenario. But if instead we swap the top-level or, we get

IF 12 CSV <Alice> CODESEP ELSE <Carol> CODESEP ENDIF Checksigverify <bob> checksig

Now Alice and Carol's codeseparators "leak out" and affect Bob's signature, and we have the Taproot semantics! This is particularly alarming because all I did was swap the two children of the top-level or, something the policy compiler currently does when attempting to optimize. I therefore believe that if we add CODESEPARATOR to Miniscript, we want to do it as part of our ors rather than as part of our pks, and we need to be careful when compiling them.

I believe we need to extend the policy language to somehow indicate a "tapbranch or", and while we're at it, I think we should extend Miniscript to add a variant of all four disjunctions that puts CODESEP before each child. When compiling to Taproot, these ors would become distinct Tapbranches. When compiling to pre-Taproot scripts, these would compile to ordinary

When compiling to Taproot, tapbranch ors" are required to be "top-level" combinator. That is, you cannot nest them inside any ands threshes or normal ors. Curiously, the same property needs to apply to the new CODESEP-orvariants! For example, if ouror(bob,or_tap(alice,csv+carol))` policy were compiled using CODESEPARATOR, it would look like one of

1. IF CODESEP 12 CSV <Alice> ELSE CODESEP <Carol> ENDIF Checksigverify <bob> checksig
2. <bob> checksigverify IF CODESEP 12 CSV <Alice> ELSE CODESEP <Carol> ENDIF Checksig

i.e. it might have Taproot semantics, might have legacy semantics, and the user can't easily predict which one they'll get.

But if only top-level ors were allowed to have CODESEPs, there's no problem! We will reliably get Taproot-like semantics, if and only if the user writes a policy with Taproot-ors in it.

Start with the policy compiler and Miniscript disjunction handling described in the issue, then compare the two example programs and their Taproot versus pre-Taproot semantics. A complete change would need a decided policy-language representation, top-level restrictions, and corresponding Miniscript and compilation behavior; this issue does not name implementation files or tests.