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 };
  |                        ^^^^^^^^^^