Composition of progams

[uncomputable]

We should implement the composition of two finalized programs (1 → 1). How should this be done?

Approach 1: Unfinalize, combine, refinalize

Trivially correct. The type of witness nodes may change if there were any free variables (that were mapped to unit) in either program. This could confuse users.

Approach 2: Unify finalized programs

Potentially more efficient. Should work if the type pointers of both programs don't overlap (they come from different Contexts)? What are the conditions that this works? Do we refuse to unify if these conditions are not satisfied?

What happens if unification fails? AFAIU, the current algorithm tries to greedily unify until it gets stuck. Any bindings that are created in the process stay. Unification for composition should be atomic.

[apoelstra]

I think we should only allow composition of unfinalized programs CommitNodes .... I think once you have a RedeemNode this should basically be an immutable object.

If we support composing redeemnodes we also need to think about what to do with witnesses.