new-mut-ref: move/copy info for struct update tails

[tjhance]

This calculates fine-grained move information for struct-update expressions (structs with the .., like in {a: x, ..foo}) in order to support such expressions in new-mut-ref.

As a side-effect, mode-checking for these expressions is now a bit more fine-grained, as in, we now allow this corner case:

tracked struct Foo {
    tracked tr: X,
    ghost gh: X,
}

proof fn test(foo: Foo, tracked x: X) {
    // This is ok because we only need the ghost field off of foo
    let tracked foo2 = Foo { tr: x, .. foo };
}