Split (possible) Non-Terminating functions from terminating ones

[capt-hb]

By switching to total triples we need to split up non-terminating functions from terminating ones. This should only be applicable to the case studies (MinimalCaps, RiscvPmp), where we have the loop function that calls itself recursively. We already reason about loop outside of Katamaran (using the Iris instance directly), so we don't lose anything. Initially, we can opt to remove loop from being considered by Katamaran (i.e., removing it from Fun), or introduce a PartialFun that contains the non-terminating functions (not sure if there is currently a benefit for doing that).

[capt-hb]

The majority of functions part of the examples include some loop:

• test/Example.v: gcd, gcdloop, length
• test/SumMaxLen.v: summaxlen
• test/LinkedList.v: append, appendloop, length, copy, reverse, reverseloop