Improve handling of idents when generating Why3 code

[jhjourdan]

My proposal: have an Ident type in the Why3 crate with a string and a unique identifier. The Why3 crates generates colision-free names when printing (while trying to use the string when possible), by maintaining the local environment. The Creusot crate needs to be audited to use this new API.

This is related with #108 .

[Lysxia]

While working on this I found a bug. It was probably to be expected given the current state of things. Now we have a concrete test case:

extern crate creusot_contracts;
use creusot_contracts::*;

#[open]
#[logic]
#[ensures(result == (1, 2))]
pub fn f() -> (Int, Int) {
    let x = 2;
    ({let x = 1; x}, x)
}

Translated VC:

goal vc_f'0 : let x = 2 in let x_1 = 1 in [%#sxxx0] (x_1, x_1) = (1, 2)

The VCGen is written in CPS. When it finishes translating the first component {let x = 1; x} of the pair, it calls a continuation to translate the second component x while the x = 1 binding is still in scope.

The add_bounds/pop_bounds calls here are basically just broken:

creusot/creusot/src/backend/logic/vcgen.rs

Lines 440 to 443 in f4b9eda

	self.add_bounds(bounds);
	// FIXME: this totally breaks the tail-call potential... which needs desparate fixing.
	let r = k(pat);
	self.pop_bounds();

The postcondition of build_vc should be a plain term instead of a function, with some delayed substitution trickery to avoid a quadratic time blow up.

[jhjourdan]

I see... good to know that we will not keep this mechanism.