mut refs & type invariants

[tjhance]

I have started working out mut refs need to interact with type invariants. A really basic example is like:

struct Pair {
    a: u64,
    b: u64,
}

#[verifier::type_invariant]
spec fn inv(pair: Pair) -> bool {
    pair.a < pair.b
}

fn example1() {
    let mut p = Pair { a: 20, b: 30 };

    let a_ref = &mut p.a;
    let b_ref = &mut p.b;

    *a_ref = 50; 
    *b_ref = 70; 

    foo(p);
}

We'd ideally want this to pass; the invariant is temporarily "broken" when a_ref is set to 50, but it is restored by the time foo is called.

At present, we check that a type invariant is preserved on every mutation. This is overly restrictive even today, but it is clearly unworkable in the above situation. In the mut_ref encoding, the value of p is mutated as soon as the mut_ref is created.

Instead, we can have a policy of always restoring the type invariant "as late as possible", which in this case, would be right before the foo call. Here, I've annotated the function with the ideal locations to resolve the mut ref and assert the type invariant:

fn example1() {
    let mut p = Pair { a: 20, b: 30 };

    let a_ref = &mut p.a;
    let b_ref = &mut p.b;

    *a_ref = 50; 
    assume_resolved(a_ref);

    *b_ref = 70; 
    assume_resolved(a_ref);

    assert_type_invariant(p);
    foo(p);
}

Here, we have the assume_resolved directives inserted as early as possible, and the assert_type_invariant directive inserted as late as possible. This all works out nicely, since we need the resolution assumptions in order to prove the type invariant for p.

And you can see why this would work out nicely in the general case: the earliest possible spots for the resolutions will always be before the lifetime ends and p can be used again.

The problematic case is when we're working with reborrows, because in that case, the same location is subject to BOTH assume_resolved and assert_type_invariant at the same time, and these are in tension with each other. Let's look at a similar example, using a reborrow:

fn example2() {
    let mut p = Pair { a: 20, b: 30 };
    let mut p_ref = &mut p;

    let a_ref = &mut (*p_ref).a;
    let b_ref = &mut (*p_ref).b;

    *a_ref = 50; 
    *b_ref = 70;

    foo(p);
}

Again, let's annotate this with all the directives, putting assume_resolved as early as possible, and assert_type_invariant as late as possible:

fn example2() {
    let mut p = Pair { a: 20, b: 30 };
    let mut p_ref = &mut p;

    let a_ref = &mut (*p_ref).a;
    let b_ref = &mut (*p_ref).b;
    assume_resolved(p_ref);

    *a_ref = 50; 
    assume_resolved(a_ref);
    *b_ref = 70; 
    assume_resolved(b_ref);

    foo(p);

    assert_type_invariant(*p_ref);
}

This doesn't look good. The problem is that we aren't enforcing the type invariant until after foo has been called, which will assume the type invariant.

So we can add a rule, the assert_type_invariant must always go before the assume_resolved:

fn example2() {
    let mut p = Pair { a: 20, b: 30 };
    let mut p_ref = &mut p;

    let a_ref = &mut (*p_ref).a;
    let b_ref = &mut (*p_ref).b;
    assert_type_invariant(*p_ref);
    assume_resolved(p_ref);

    *a_ref = 50; 
    assume_resolved(a_ref);
    *b_ref = 70; 
    assume_resolved(b_ref);

    foo(p);
}

This is now sound, but now the assert_type_invariant directive is too early: we won't be able to prove the type invariant at this point. The best point, of course, is here:

fn example2() {
    let mut p = Pair { a: 20, b: 30 };
    let mut p_ref = &mut p;

    let a_ref = &mut (*p_ref).a;
    let b_ref = &mut (*p_ref).b;
    assume_resolved(p_ref);

    *a_ref = 50; 
    assume_resolved(a_ref);
    *b_ref = 70; 
    assume_resolved(b_ref);

    assert_type_invariant(*p_ref);

    foo(p);
}

However, there isn't an obvious (to me) way to infer this point. The descriptor I'd give this location would be something like "the latest possible point that doesn't break lifetime checking". However, this is difficult to calculate. One option would be to require an annotation from the user here.

Another option would be to take a step back and say, "no, actually, it's not the borrower's responsibility to maintain the type invariant, it's the lender's." (just like it would be if you were borrowing a field instead of the whole thing). Thus, we just assert the type invariant for p, not p_ref:

fn example2() {
    let mut p = Pair { a: 20, b: 30 };
    let mut p_ref = &mut p;

    let a_ref = &mut (*p_ref).a;
    let b_ref = &mut (*p_ref).b;
    assume_resolved(p_ref);

    *a_ref = 50; 
    assume_resolved(a_ref);
    *b_ref = 70; 
    assume_resolved(b_ref);

    assert_type_invariant(p);
    foo(p);
}

In some ways, this is metatheoretically the cleanest. It uses clean rules like "put assume_resolved as early as possible, and assert_type_invariant as late as possible". You don't even need to assert_type_invariant for the *p_ref at all, since p_ref is never used.

The problem is that it's also full of surprises, like if you call some_fn_taking_a_mut_ref(&mut p), you won't necessarily know that the type invariant holds for p afterwards, unless you explicitly put it in the postcondition for some_fn_taking_a_mut_ref.

[tjhance]

The problem is that it's also full of surprises, like if you call some_fn_taking_a_mut_ref(&mut p), you won't necessarily know that the type invariant holds for p afterwards, unless you explicitly put it in the postcondition for some_fn_taking_a_mut_ref.

This is obviously bad, not just because it's confusing but because it breaks API safety.

I think we want to use the approach I described within functions, but type invariants still need to be enforced at function boundaries.

So you just wouldn't be able to write this when Pair has a type invariant:

fn get_a(pair: &mut Pair) -> &mut u64 {
    &mut pair.a
}

Or, technically: You can still implement it if the validity of pair is independent of pair.a. Basically you'll be required to prove that the type invariant holds at the end of the function, and since the mutable reference is unresolved at that point, you have to prove that pair is valid for ANY possible future value of pair.a.

Still, I think the exact rules might be a little tricky to nail down ...

[Chris-Hawblitzel]

Assuming we have a way to temporarily break the type invariant, can we just require that programmers manually break the type invariant for p before doing any mutable borrows from p? Maybe get_a would only be legal if pair is type-invariant-broken (either before calling get_a, or get_a breaks it and keeps it broken when returning)?

[tjhance]

This doesn't solve backwards compatibility with the existing system, which allows you do foo(&mut p.a) as long as foo's invariant is restored after foo. I also think it'd be pretty cumbersome; whereas the direction of my proposal makes things less cumbersome (even for cases that don't involve explicit mut refs)

[Chris-Hawblitzel]

What if by default we require programmers manually break the type invariant, but we carve out exceptions for convenience in cases like foo(&mut p.a) where the semantics are clear and there are no surprises?

[tjhance]

Recent paper by the creusot folks has a bunch to say on this issue: https://inria.hal.science/hal-05244847v1/document