Hi Antoine,
It appears that my explanation of the relationship between the covenant and the bisection protocol is still unclear; I'll do my best to clarify.

The bisection's Merkle tree never ends up on-chain, in any form. Therefore, a bigger computation does not end up in a bigger witness size, which is key to the scalability of the approach. Only in the case of a challenge, it will result in a (logarithmically) longer chain of transactions to resolve it. This chain of transactions could be mapped to a root-to-leaf path in the Merkle tree of the computation trace.

The actual computation trace (and the corresponding Merkle tree) is only computed by the parties when they execute the computation.
What's in the tapleaves is only the valid transitions at the current state of the protocol; that is, the valid transitions in the Finite State Machine (and possibly other valid exit conditions that remove the covenant encumbrance, if any).

The bisection protocol only makes sense as a step in a larger protocol that makes use of it.

Perhaps presenting the protocol in a less-than-general case might help to understand it. So let's play a simpler game using a protocol that includes a fraud proof.

Alice claims that she knows how to multiply by 256, while Bob doesn't believe her. So they make a bet: they each commit 1 coin; then Bob choses a number x; then Alice computes y = 256*x by doubling x eight times (expensive multiplications were disabled in a tragic DDoS accident), and publishes the result y. Bob independently computes 256 * x (he has a friend who is a mathematician, he'll know how to do it). If the result is not y, Bob will start a challenge; otherwise, Alice wins and takes the money.

(The example is of course artificial, as redoing the computation in Script is cheaper than executing the fraud proof in this case!)

What follows is an actual execution of the protocol. In the following, each [Si] is a UTXO corresponding to some possible FSM node, starting with the S0, the UTXO with 1+1 = 2 coins. Each line with "-" is a possible transition (script in the taptree), specifying what is the next FSM node after the "==>" symbol; the encumbrance in the scripts enforce that the state of the next UTXO is updated correctly (details omitted below), and any other necessary conditions to ensure the integrity of the protocol.

=====

[S0]: Initial UTXO
- only Bob can spend, he must choose his number x ==> S1

[S1; state: x]:
- only Alice can spend, she publishes her answer y ==> S2

[S2. state: x, y]:
- after 1 day: Alice won, she can take the money // Happy case! Usually that's the end
- Bob disagrees with the answer, post z as his answer. ==> S3

The challenge starts here! Let's put some actual numbers. x = 2; y = 508; z = 512.

This is what Alice computed:

2 => 4 => 8 => 16 => 32 => 64 => 127 => 254 => 508

This is what Bob computed:

2 => 4 => 8 => 16 => 32 => 64 => 128 => 256 => 512

At this time, we don't know who is right. They both built a tree that looks like this (ASCII art only working in fixed-width font):

___H18___
/ \
/ \
H14 H58
/ \ / \
/ \ / \
/ \ / \
H12 H34 H56 H78
/ \ / \ / \ / \
H1 H2 H3 H4 H5 H6 H7 H8

Remember that each internal node commits to: the state of the computation before the leftmost leaf in the subtree, the state after the rightmost leaf, and the hash of sub-trace for the sub-tree. Each leaf just commits to that intermediate computation step (and the operation, which here is always "double the input"). For example, H4 commits to "16 => 32" according to both Alice's and Bob's computation traces.

(From our privileged point of view, we can foresee that the earliest disagreement is on the 6th step of the computation: "64 => 127" according to Alice, "64 => 128" according to Bob).

Let's denote h_{A;18} (resp. h_{B;18}) all the information committed to in the node H18, according to Alice (resp. Bob). Similarly for all the other nodes.

[S3. state: x, y, z]: Challenge starts!
- Alice posts the root of her computation trace h_{A;18} ==> S4

[S4. state: x, y, z, h_{A;18}]
- Bob posts the root of her computation trace h_{B;18} ==> S5

Since they disagree, it must be the case that h_{A;18} != h_{B;18}.

[S5. state: x, y, z, h_{A;18}, h_{B;18}]
- Alice opens the commitment h_{A;18}, by revealing H14 and H58 (according to her) ==> S6

Note that in this last transition (going to S6), the covenant enforces that the child commitments are compatible: the transition is only valid if the starting state of the computation according to h_{A;14} is compatible with h_{A;18} (that is, it's equal to x); similarly the end state of the computation in h_{A;58} must be y, and h_{A;18} can be recomputed from the data provided (ensuring the integrity of the Merkle tree).
This is true for all the commitment openings below.

[S6. state: x, y, z, (h_{A;14}, h_{A;58}), h_{B;18}]
- Bob opens the commitment h_{B;18}, by revealing H14 and H58 (according to him) ==> S7

[S7. state: x, y, z, (h_{A;18}, h_{A;14}, h_{A;58}), (h_{B;18}, h_{B;14}, h_{B;58})]
// We now need to choose a child where there is disagreement.
// If both children don't match, iterate on the left child.
- Anyone: if h_{A;14} == h_{B;14} ==> S8
- Anyone: if h_{A;14} != h_{B;14} ==> Continue challenge on H14 // Non-executed FSM cases omitted for brevity

At this point, the disagreement over the root is settled: Alice and Bob agree on the first half of the computation, but they disagree over the second half. Therefore, in S8 the protocol continues over H58.

[S8. state: h_{A;58}, h_{B;58}]
// This is analogous to S5, just with half of the computation steps.
- Alice opens the commitment h_{A;58}, by revealing H56 and H78 (according to her) ==> S9

[S9. state: (h_{A;56}, h_{A;78}), h_{B;58}]
- Bob opens the commitment h_{B;58}, by revealing H56 and H78 (according to him) ==> S10

[S10. state: (h_{A;56}, h_{A;78}), (h_{B;56}, h_{B;78})]
// Like S7, iterate on a disagreeing child
- Anyone: if h_{A;56} == h_{B;56} ==> continue challenge on H78 // Non-executed FSM cases omitted for brevity
- Anyone: if h_{A;56} != h_{B;56} ==> S11

Getting there! The subtree now commits to just two computation steps.

[S11. state: h_{A;56}, h_{B;56}]
// This is analogous to S5 and S8.
- Alice opens the commitment h_{A;56}, by revealing H5 and H6 (according to her) ==> S12

[S12. state: (h_{A;5}, h_{A;6}), h_{B;56}]
- Bob opens the commitment h_{B;56}, by revealing H5 and H6 (according to him) ==> S13

[S13. state: (h_{A;5}, h_{A;6}), (h_{B;5}, h_{B;6})]
// Like S7 and S10, iterate on a disagreeing child
- Anyone: if h_{A;5} == h_{B;5} ==> S14
- Anyone: if h_{A;5} != h_{B;5} ==> continue challenge on H5 // Non-executed FSM cases omitted for brevity

We are now at the crucial stage: the commitment corresponds to a leaf of the computation trace Merkle tree.

[S14. state: h_{A;6}, h_{B;6}]
- Alice can take all the money if she can open h_{A;6} to a correct "n => n + n" computation step
- Bob can take all the money if he can open h_{B;6} to a correct "n => n + n" computation step

The challenge now ends quickly: Bob's hash commits to the computation step "64 => 128".
Instead, Alice's step is the incorrect "64 => 127".

It's not difficult to convince oneself that, as long as the hash function is collision-free and the computation is deterministic, only the honest party can provide correct data for this final step.
(The bisection protocol can't do anything useful if both parties provide incorrect data; arguably, that is not a very interesting scenario!)

Crucially, the operation in the single step is so simple that Script can verify it.

=====

If you read until here: thank you, this was the first execution of a challenge in MATT covenants!

Of course, there are a few things missing in the above protocol:
- Bonds should be added in order to incentivize cooperation.
- The omitted FSM steps (corresponding to branches of the challenge that were never taken) need to be computed nonetheless when preparing the covenant.
- Additional transitions should be added at every step (always allow cooperative behavior; forfait after a timeout if it's the other party's turn).
- Some of those consecutive "forced" steps can be contracted in a single step; I felt this sequence is more logical to explain the protocol, but implementations would want to optimize it.

Yet, _all_ the code and scripts of the bisection protocol are independent of the actual execution, and can be precomputed (bottom up, starting from the leaves) before the initial covenant is created - therefore, before x, y and z are chosen and committed to.

While here each leaf is doing the same operation (doubling a number), it is well-known that arbitrary computation can be decomposed in very simple elementary functions (like NAND gates, if we want to be minimalistic).

I hope this helps in clarifying the role of the bisection protocol in smart contracts using MATT covenants.

Best,

Salvatore