Confusing difference in behavior when creating tracked struct

[matthias-brun]

The following code works fine when we initialize the field b with a constant 3u64 but if we try to use the u64 from the argument, Verus emits an error about the expression's mode. This behavior is very confusing and in fact, seeing the mode error message had lead me to believe that values of tracked type can only be created in trusted code.

use vstd::prelude::*; verus! {

struct A { b: u64 }

proof fn new(b: u64) -> tracked A {
    // only works if we declare the field `b` to be `ghost`:
    let tracked a: A = A { b: b };
    // works:
    // let tracked a: A = A { b: 3u64 };
    a
}

}

error: expression has mode spec, expected mode proof
 --> linear.rs:7:24
  |
7 |     let tracked a: A = A { b: b };
  |                        ^^^^^^^^^^

[tjhance]

This is technically by design:

• b has mode spec
• Thus A { b: b } has mode spec
• But you're trying to assign to a 'tracked' variable

However:

• In principle, we could coerce spec-mode integers to tracked-mode integers. Tracked mode integers aren't very common, but they have no actual "proof content", so this coercion would be sound. This is true for many other types as well.
• The mode error messages in general are not very good.

[matthias-brun]

Thanks for the comment.

The mode error messages in general are not very good.

Yeah, that's the actually problematic part, I think. I find it very hard to make sense of error messages while doing tracked things. It's often not clear to me whether I'm trying to do something that isn't possible or whether a tiny change is sufficient to make it work, as is the case in this example.