The Heapster any permission

[eddywestbrook]

This PR adds a new false / inconsistent permission any, which translates to the SAW core unit type. This is as opposed to the false permission, which translates to the inconsistent False type. The reason we need any is in order to combine inconsistent permissions whose translations are not inconsistent types. For instance, if we have permissions

x : eq(llvmword(0)) or ptr((W,0) |-> p1) , x:ptr((W,8) |-> p2)

we know in the Heapster type system that x cannot have permission eq(0), because the second permission ensures x is a pointer. The translation of these permissions is the type (unit + [| p1 |]) * [| p2 |], however, where the second element of the pair does not in any way guarantee the the first element is not a left-hand element of the sum type. This sort of situation comes up in Rust functions with Option of reference return values, like this one:

pub fn list64_head_mut <'a> (l:&'a mut List64) -> Option<&'a mut u64> {
    match l {
        List64::Nil64 => None,
        List64::Cons64 (h,_) => Some (h),
    }
}

The input lifetime ownership permission for this function is something like a:lowned (l:List64 -o l:List64), while the output permission is a:lowned (ret: eq(0) or ptr((W,0) |-> u64) -o l:List64). In order to prove the output lifetime ownership permission from the input one in the Some case, we have a situation like the above for the contravariant implication needed for the input permissions of the lowned permissions, where we have to prove ret: eq(0) or ptr(...) plus the ptr permission for ret implies l:List64.

[ChrisEPhifer]

Totally a minor nitpick - the double-negative phrasing in the error message ("not unequal") seems awkward here. At the same time, though, I see the intent... I'm not sure how to make it clearer. Maybe "expected unequal expressions"? It probably doesn't really matter since this is a halt-and-catch-fire situation anyway.

[eddywestbrook]

Huh, I see what you mean. I hadn't thought about "unequal" as a negative thing, because in this context it is a positive, in that we are trying to prove unequality and in this case that proof failed. In the end, though, I think you're right, it probably doesn't really matter. The main content of the error message is actually just the name of the rule that failed...

[ChrisEPhifer]

Looks good to me - I left a comment on an error message that maybe could have been phrased better, but approved the changes since it doesn't matter that much / the intent behind the original phrasing is clear.