`comp` and verifiable conjunctions

Structurally, Simplicity has many similarities to Miniscript, a combinator language built on top of Bitcoin Script and which allows complex spending policies to be defined in an analyzable way. (Miniscript borrowed many things, including the word “combinator”, from Simplicity.) Like Miniscript, Simplicity programs are trees – although thanks to sharing and pruning, they can be encoded and analyzed much more compactly than their tree structure would imply.

One use of this tree structure in Miniscript is that it’s easy to construct a verifiable cosigner structure. That is, if a cosigning service has a policy represented by a Miniscript M, it can look at any Miniscript and(M, _) and be assured that it will enforce all the same conditions as M, regardless of which particular form and takes (Miniscript has 4) and regardless of what else is in the _. So a user of the service can define their own arbitrary policy, stick it into the _, and use it without ever needing to explain or justify it to the service.

In Simplicity, we can implement Miniscript-like constructions in which each “base combinator” has the type 1->1 and operates by consuming some witness data then either aborting or passing. For example, a pk-like combinator could be defined as (witness &&& jet::sig_all_hash); jet::bip_0340_verify. The closest Miniscript type to 1->1 is Vz, but because Bitcoin Script has no witness combinators, you can’t do much within this type, so as a consequence Miniscript has a much more complicated type system than Simplicity.

Once we have our base combinators, we can then define conjunctions and disjunctions. Conjunctions are particularly easy: if you have two subprograms A and B of type 1->1 which check conditions and possibly abort, then their conjunction is just their composition: we use the comp combinator to get A; B and that’s our conjunction.

Then just like with Miniscript, we can define a “cosigner policy” where a cosigner has a fixed program C, and then can be assured that any program C; _ enforces the same conditions regardless of what the user sticks into the _. Miniscript takes pains to ensure that no well-formed expressions have “action at a distance” where the user might define a policy that somehow bypasses the cosigner’s policy, even though the underlying Bitcoin Script allows this in various ways. In Simplicity we get this same assurance thanks to its types and effect system.

But in Simplicity we can go even further than in Miniscript. In Miniscript it’s nice that a cosigner can observe a program and confirm it’s of the form and(C, _) before signing. In Simplicity you can do this same check in Simplicity code, meaning that covenants can enforce the same sort of “cosigning” relationship. They can do this because all Simplicity programs are uniquely identified by their Commitment Merkle Root (CMR) and CMRs are designed to be pretty cheaply-computable in Simplicity itself. In particular, given an expression 'A computing the CMR of an expression A, and similarly 'Bcomputing the CMR of B, the expression '(A; B) is (const_word(PAIR_IV) &&& 'A &&& 'B); jet::sha256_block. That is, we just prefix this fixed “pair IV” to the two input CMRs, run the whole thing through the SHA256 compression function, which has its own jet, and you’re done.

(By the way, this 'x notation for "expression that produces the CMR of x) is pronounced “quote” and is supposed to be evocative of the common Lisp quote operator. The idea is that it takes a Simplicity expression and gives you its representation in Simplicity, or rather the representation of its hash. In Simplicity, which has only finite types, we always want to represent variable-sized objects by their hash, if we can get away with it.)

In our example, where B is user-provided and irrelevant, we can simply use witness in place of 'B, and where A is some fixed cosigner script, we can use a const_word jet in place of 'A. So our construction becomes (const_word(PAIR_IV) &&& const_word(cmr(A)) &&& witness); jet::sha256_block. If we assert that an output has a unique Simplicity script whose CMR is the result of this expression, we’ve asserted that the output enforces the conditions of A, without putting any further constraints on the output’s logic. The cost is roughly 67 bytes – 64 for the two constant words plus just a couple bytes of overhead for the other combinators. Basically the same as a signature from a traditional cosigner.