Implement pruning

[uncomputable]

case nodes should be replaced with assertl or assertr if their left or right branches, respectively, are not used during execution. Pruning should happen during finalization.

Pruning is non-trivial in conjunction with sharing, since inferred types may change. Witness targets may shrink and IMRs may change, recursively leading to more sharing.

[apoelstra]

Can you elaborate? Pruning should not change any types or IMRs. It merely involves deleting nodes that are not executed.

I'm sure we could find some extra opportunities for sharing by messing around with type inference, but that's also unrelated to pruning.

[uncomputable]

Take witness △ unit; case consumeA consumeB where consumeX: X × 1 → 1. witness has type 1 → A + B. Slight variations of this construct can appear in the program, like this:

(witness △ unit; case consumeA consumeB); (witness △ unit; case consumeA consumeC)

We take the A path in both and prune, yielding:

(witness △ unit; assertl consumeA cmr(consumeB)); (witness △ unit; assertl consumeA cmr(consumeC))

The left assertl has the same signature as the previous case: (A + B) × 1 → 1, but B is now a free variable and bound to 1. Therefore the type of the left witness changes to 1 → A + 1. The same happens on the RHS. The assertl parts still have distinct CMRs, but the witness △ unit parts are now equal and must be shared.

Since the type of witness changed, its IMR also changes.

[apoelstra]

I'm still not following. witness does not have an IMR until its type is concretized (by binding all remaining free variables to 1) so its IMR doesn't "change".

Whatever its IMR winds up being, this will inform how sharing happens.

But still I don't see the problem with pruning and finalizing types (in either order) and then sharing (later, when serializing the program).

[uncomputable]

I think pruning first and sharing later works. My warning was mostly about a "what if" scenario that we should try to avoid.

My IMR example was wrong; thanks for pointing this out. I am trying to rationalize what Russell told me months ago.

Another attempt: witness △ unit; case (take consumeA) (take (witness △ iden; consumeB^2))

The first witness node has type 1 → A + B and the second has type 1 → B. Assume a left A value is assigned to the first node and a B value to the second. We have an IMR. Now we prune the second branch. The program's witness data shrinks and the type of the first witness node changes to 1 → A + 1. The IMR changes.

This is an artificial example, but there might be more realistic ones. Sharing still works, so we probably don't care. Still, it is interesting that the IMR may change.

[roconnor-blockstream]

Prune first and share later is correct. Sharing should simply be considered part of the serialization format, and thus must occur last/in tandem with serialization.

[apoelstra]

Yes, if you were to finalize the types of an unpruned program, some nodes would have different IMRs than they would after pruning. Similarly if you populate (or change) witness values, the IMRs will change. But prior to pruning the program is not valid, so the "IMR"s you comupte are basically just dummy values to assist in serializing the program.

I think I understand what you're saying -- that a different set of nodes will be shared based.on what you do with your witnesses -- but this is a trivial observation because the set of nodes period may be different, so of course the set of shared nodes may be different.