Some initial thoughts on liveness theorem, proved permutation swapper for calls
Proved Alloc, Move for permute swapping