Heapster fix lowned proofs

[eddywestbrook]

This PR fixes how lowned permissions are proved, especially with regards to those lowned permissions like

l:lowned (x:p_in -o x:p_out)

which contain variables like x that have equality permissions on them. Previously, the implication prover would cast the lowned permissions using these equality permissions, in order to remove any variables with equality permissions; e.g., if x:eq(y), the above permission would be cast to

l:lowned (y:p_in -o y:p_out)

The issue was when x was equal to a non-variable expression, which yields an lowned containing an implication on non-variable expressions. Instead, the new approach implemented in this PR finds all relevant equality permissions and incorporates them into the local implications used to prove one lowned permission from another.

This uncovered a number of lifetime-related bugs that were fixed, including:

1. localProveVars was changed so that, when it builds a local proof of ps1 -o ps2, it recombines the input permissions ps1 in reverse order, since these permissions are created (by the implication prover for lowned permissions) with the equality permissions first, and these need to be recombined first.

2. instantiateLifetimeVars was changed to only instantiate lifetimes that require lowned permissions

3. implEndLifetimeRecM was tweaked so that it now removes any lifetimes that have been ended from any other lowned permissions

4. simplify1PermForDetVars was fixed so that if a determined variable has an lowned permission that contains an indetermined lifetime variable, that indetermined lifetime is ended and removed from the lowned so that it no longer has that indetermined lifetime free

[m-yac]

I feel very out of my depth trying to review changes to the implication prover, so I can't say I really understand solveForPermListImpl or most of the changes to proveVarAtomicImpl, for example. But from just a pure Haskell perspective, it looks OK to me.

[glguy]

Suggested change

	let mb_ps_inL = fmap (const ps_inL) mb_ps_inR in
	let mb_ps_inL = ps_inL <$ mb_ps_inR in

[eddywestbrook]

Using some of these special-purpose operators sometimes just looks like line noise to me. I know <$> and <*>, but when it starts getting more complex I would rather just be verbose about what the operator is doing. It's just like using the lens library: if you don't know all those operators, it can be really hard to read code that uses them.