Improve error message about bottoms

[shaoweilin]

I have the following simplified code

struct UU(u32);
const z : UU = UU(0u32);
fn f(_ : UU) {}
fn g() {
  let x = z;
  f(x);
  f(x);
}

which charon translates successfully without complaining. After running aeneas on the LLBC output, I get the message

[Error] There should be no bottoms in the value

It wasn't clear to me what "bottoms" mean in this context.

It would have been useful to know, from the error message, that bottoms are "Aeneas representations of values that are not accessible anymore (e.g., moved values)." (see here). For example, my code above "does not actually compile in Rust: the first call f(x) moves the value x, which is therefore not usable anymore for the second call."

There is another issue here of charon not complaining when there is an error in the code, but the issue here is only about improving the error message for bottoms.

[sonmarcho]

Thanks for the issue! I've actually been thinking about this for a while.
What I have in mind so far is that we should keep some meta information in the bottom value pertaining to the reason why it was introduced. In the case above, we would remember that x has been invalidated because it was moved in the first call to f(x), and we would use this information to print an informative error message when reaching the second call and trying to consume x again.
As a side note: if we update Charon so that it doesn't accept invalid Rust code, then in most situations improving the error messages shouldn't be necessary (because if you try to move a value twice then the program is not valid Rust in the first place).