Add support for `old`

[xldenis]

The specifications used in #83 critically depend on having a functioning version of old in pearlite. On the one hand this requires adding support for the syntax of old but also requires going a bit further and also discussing its semantics.

The old of why3 refers to the value of a variable at the previous label state or the entry of the function. If the variable doesn't exist at that state then it does nothing. This is a problem for us as it turns out none of our variables exist at entry of the function (at least to why3).

For example:

fn x(mut a: u32) {
a = a + 1;
assert! { old(a) != a }
}

actually is turned into something like

let rec cfg x (a : u32) {
var a_1 : u32;
{ a_1 <- a;
goto BB0;
}
BB0 {
assert { old(a_1) != a_1 }
}

But to why3 a_1 doesn't exist at the start of the function! and it is definitely not equal to a.

I'm not sure what the best solution to this is. I have a few ideas:

1. Each block implicitly declares its own label. Then old would work correctly here. However could this lead to counter intuitve behavior?
2. allow the header blocks to include an actual binding rather than just a declaration so we could write var a_1 : u32 = a; and add a specific label after all the var declarations (aka shift the entry down to the start of the code
3. Do a transformation in creusot where we rewrite old(a_1) into old(a) by detecting that a_1 is meant to refer to a.

[shiatsumat]

Do we really need old for benchmarks, especially #83? I'd like to know how we need old more in detail.

I think a workaround is to use a phantom variable that records a value at a specific point. We can give PhantomData<T> the model of T and define a ghost operation like the following.

#[trusted]
#[ensures(result.model() === a)]
fn record(a: &T) -> PhantomData<T> { PhantomData }

[xldenis]

Oh that is clever.

[xldenis]

I think it might be sufficient. I quite like this as i can then put off implementing old/labels.

[xldenis]

Hmm I've encountered two issues with this so far:

1. Rust type inference sucks and forgets the generic parameter of PhantomData :/
2. We really want record to take self not &self but this would require it to be actually ghost

[shiatsumat]

I can imagine the type inference problem (1.), but anyway adding type annotations works.

I wonder what you mean in (2.). Do you mean taking a: T instead of a: &T? That does not work when T is not Copy.

[xldenis]

Exactly, unless it were truly ghost and thus not subject to borrow checking restrictions.

[jhjourdan]

It's indeed a well-known fact that ghost variables and historical variables have the same expressiveness. That being said, in Creusot, I think we want both in the end. So the question is rather what is simpler for the PLDI submission.

I think that historical variables (i.e., old and `labels) are subject to fewer design decisions, and are perhaps simpler to implement. However, as you describe, it's unlikely that we will be able to use Why3's support for historical variables.

The implementation idea that comes to my mind is to systematically create historical variables as soon as a variable is created/or a label is crossed (i.e., for each variable x, create a variable old_x), and mutate it when relevant. The number of generated variable is then quadratic (number of variables in the source times numbers of labels). If this is an issue in the generated code, then a simple liveness analysis will do the job of removing the useless variables.

[shiatsumat]

I agree that it's better if we can implement and use true history variables. But anyway the ghost variable hack works (if very hacky) so it's OK for now I think. After all this part does not really affect the paper, I think.

[xldenis]

@jhjourdan I actually think that we will be able to fully benefit from why3's old mechanism and labels! it will take a bit of work on the MLCFG side but it should work just as well as for normal why3 code.

That being said, @shiatsumat's idea works for now, and allows us to move forward while we wait for a 'proper' solution.

[xldenis]

I was thinking about this again recently, especially now that Pearlite has old (used in closures for now). In theory old works 'out-of-the-box' in MLCFG (with stackify), but the way we translate rust programs breaks that.

In particular, old always refers to the value of a variable at function entry, but we do something which masks this, for example:

fn my_func(x: &mut T) { ... }

Becomes something like:

let cfg my_func (x : borrowed T) = 
var x_1 : borrowed T;
...
{
 x_1 <- x
 ...
 goto BB0;
}

In the rest of the program we use x_1 when we're referring to the function parameter x. Since x_1 technically didn't exist at function entry old doesn't work on it.

I think a 'simple' fix for this is to add a notion of label to MLCFG and systematically intro a Entry label at the start of each function, then translating old(x) in an invariant or proof_assert into x at Entry instead.