klab-prove: traverse and prove called specs

[asymmetric]

Whenever one wants to prove a spec A that calls another spec B, one has to manually:

1. klab prove --dump B_pass_rough
2. klab get-gas B_pass_rough
3. klab build
4. klab prove B_pass

This has to be repeated for each called spec. This is n o t f u n.

It would be nice if klab-prove could automate all of these steps, something like

klab prove --recurse A

I guess there are some facilities for this in prove-all, since it takes care of all the steps listed above, so the matter is just making them available more modularly.

[d-xo]

This would be awesome.

[mhhf]

One can dream...