lifetime-generate wrongly ignored assignment to ghost field of tracked struct

[tjhance]

This should not pass:

tracked struct Z {
}

tracked struct Y {
    tracked z: Z,
}

tracked struct X {
    tracked y: Y,
    ghost a: int,
}

proof fn borrower<'a>(tracked x: &'a mut X) -> (tracked y: &'a Y) {
    &x.y
}

proof fn take_z_ref(tracked z: &Z) {
}

fn stuff() {
    let tracked mut x = X { y: Y { z: Z { } }, a: 0 };
    let tracked y_ref = borrower(&mut x);

    proof {
        x.a = 5;
        take_z_ref(&y_ref.z);
    }
}

The line x.a = 5 modifies x which is currently borrowed, and x is a tracked variable so should be subject to lifetime tracking.

However, since x.a is a ghost field, lifetime-generate treats this assignment as if it can be ignored.

[Chris-Hawblitzel]

This is interesting. We generally allow spec-mode reading from borrowed variables or variables whose values have moved, on the grounds that spec mode can read old copies of the data, and that this is sometimes convenient. For example:

struct S(u8);

fn f() {
    let a = S(1);
    let mut b = a;
    b.0 = b.0 + 1;
    assert(a.0 == 1);
}

We've also allowed assignments to spec values in the same way, which we also treat as assigning to old copies, though it's probably more an accident in the design than something intentional. At least, I don't see why it's useful:

struct S(Ghost<int>);

fn f() {
    let mut a = S(Ghost(1));
    let mut b = a;
    proof { b.0@ = b.0@ + 1; }
    assert(a.0@ == 1);
    proof { a.0@ = 0; }
    assert(a.0@ == 0);
    assert(b.0@ == 2);
}

Should we be more restrictive towards writes than reads here? As we add more support for mutable references, there's always a danger that we don't encode the correct "copying" semantics in the SMT queries and therefore become unsound. Is this already a soundness issue, or is this something we should change now to prevent unsoundness in the future?

[tjhance]

Y'know, I filed this because it seemed "obviously" unsound, but on second thought, I can't really think of a way to exploit it. After all, mutating the ghost state only ends up mutating anything in the encoding. Perhaps it's just confusing, not unsound. Not sure if the calculus changes when there's more general mutable reference support.