Returning mutable references

[utaal]

I'm looking into how to support functions that return mutable references. These are generally very useful for things like mutating (part of) an element of a vector, without having to move it out (which we had to do with Linear Dafny).

There are multiple parts to this feature:

• what the specification should look like, in particular to express what happens at the end of the mutable borrow;
• what the VC encoding should look like at the call site,
• what the VC encoding should look like for the function's body.

I've written up my current ideas for the specification here:

---

Support for returning mutable references

This concerns functions that return mutable references (e.g. fn index_mut(&mut self, idx: usize) -> &mut u64); it does not yet consider support for borrows without a function call (e.g. let a = &mut adt.field).

Function spec, from the perspective of the callers

Similarly to calling functions with an &mut parameter, we can treat (a) returning a mutable reference and (b) the borrow expiring as two "moves" of the borrowed value: once (a) out of and once (b) back to the lender (the lender is the &mut parameter with the same lifetime as the returned reference). This is justified because with mutable borrows an exclusive permission to the borrowed value is transferred for the duration of the borrow.

The intuition is to treat the caller's code from the call site to the end of the borrow roughly as if it was a function that takes the mutable reference as an &mut parameter. The specification of this ficticious function is provided in an after<'lifetime> block in the header of the borrowing function. In other words,

• regular requires and ensures apply to the function call site, and have the same semantics as for functions that don't return a mutable reference;
• an after<'lifetime> block is used to introduce a second pair of requires/ensures that refer to the point at which the borrow expires: requires expresses constraints on the borrowed value before the borrow ends (i.e. before it's returned to its lender), ensures is what's true after the end of the borrow. before(ref) where ref is the reference can be used to refer to the value of the borrowed references just after the call (at the very start of the borrow), whereas old has the same meaning as regular requires/ensures

In its unsugared form, after requires an explicit lifetime, to tie it to a specific lifetime being returned by the function. Despite being initially unsupported, a rust function may return multiple mutable references with different lifetimes. We can provide a version of after with an implicit lifetime, when only one lifetime is (implicitly or explicitly) declared for the function signature.

struct Vec<V>
impl<V> View for Vec<V> {
  type View = Seq<V>;
  
  #[spec]
  fn view(&self) -> Seq<V> { .. }
}
impl<V> Vec<V> {
  #[verifier(external_body)]
  pub fn index_mut_increasing<'a>(&'a mut self, idx: usize) -> &'a mut V {
    requires(idx < self.len());
    ensures(|ref: &mut V| *ref == old(self).index(idx));
    after<'a>(|ref: &mut V| {
      requires(*ref > *before(ref)); // what needs to be true of *ref at the end of the borrow
                      // before(ref) is the value of ref at the beginning of the borrow
      ensures([ // after the end of the borrow
        forall(|i: nat| i < self.len() >>= if i != idx {
          self.index(j) == old(self).index(j) // old(self) is the value of self before the call
        } else {
          self.index(j) == *ref // ref is the value of ref at the end of the borrow
        },
        sum(self.view()) > sum(old(self).view()),
      ]);
    });
  }
}

Caller code

In the caller code, the mutably borrowed value (the lender) is treated as "moved" for the duration of the borrow (the borrow-checker would prevent access to it): referencing its value in spec code results in the value before the move (i.e. the call). It is havoc-ed when the borrow ends.

One language design issue is the fact that generally speaking there's no code that directly corresponds to the end of a borrow, as shown in Example 3 and Example 4. To start (and in order to avoid having to extract information from the borrow checker), we can require the user to explicitly expire the borrow (with an expire/drop function), like in Example 4.

Example 1. Correct usage:

fn caller(v: Vec<u64>, v2: Vec<u64>) {
  requires([sum(v) >= 20, v.len() > 10, v2.len() == v1.len()]);
  #[spec] let v_prev = v;
  let e: &'a mut u64 = v.index_mut_increasing(4);
  e = e + v2.index(4);
  // mutable borrow 'a expires here
  // `v` havoc-ed, and after ensures clause applies
  sort(&'b mut v); // ensures elements are the same
  assert(sum(v) > 20);
  assert(exists(|i: nat| i < v.len() && v.index(i) == v_prev.index(i) + v2.index(4)));
}

Example 2. Error, after requires not satisfied:

fn caller(v: Vec<u64>, v2: Vec<u64>) {
  requires([sum(v) >= 20, v.len() > 10, v2.len() == v1.len()]);
  #[spec] let v_prev = v;
  let e: &'a mut u64 = v.index_mut_increasing(4);
  // mutable borrow 'a expires here
  // error: requires condition after the expiry of the borrow
  sort(&'b mut v); // ensures elements are the same
  assert(sum(v) >= 20);
  assert(exists(|i: nat| i < v.len() && v.index(i) == v_prev.index(i) + v2.index(4)));
}

Example 3. Error, after ensures only takes hold at the end of the borrow:

fn caller(v: Vec<u64>, v2: Vec<u64>) {
  requires([sum(v) >= 20, v.len() > 10, v2.len() == v1.len()]);
  #[spec] let v_prev = v;
  let e: &'a mut u64 = v.index_mut_increasing(4);
  e = e + v2.index(4);
  assert(sum(v) > 20); // error: v still has the old value (before the borrow)
                       // emit warning that there's a live mutable borrow?
  // mutable borrow 'a expires here
  sort(&'b mut v); // ensures elements are the same
  assert(exists(|i: nat| i < v.len() && v.index(i) == v_prev.index(i) + v2.index(4)));
}

Example 4. Example 3 fixed: explicitly drop the borrowing variable to terminate the borrow:

fn caller(v: Vec<u64>, v2: Vec<u64>) {
  requires([sum(v) >= 20, v.len() > 10, v2.len() == v1.len()]);
  #[spec] let v_prev = v;
  let e: &'a mut u64 = v.index_mut_increasing(4);
  e = e + v2.index(4);
  expire(e); // force the end of the borrow here
  assert(sum(v) > 20); // now verifies
  sort(&'b mut v); // ensures elements are the same
  assert(exists(|i: nat| i < v.len() && v.index(i) == v_prev.index(i) + v2.index(4)));
}

This discussed the general case of a borrow extending for potentially multiple statements. The special case of a single direct assignment to the mutable reference in the same statement as the function call can be handled using the same semantics as described above (but without the need for an explicit expire).

Example 5.

fn caller(v: Vec<u64>, v2: Vec<u64>) {
  requires([sum(v) >= 20, v.len() > 10, v2.len() == v1.len()]);
  let e = *v.index(4);
  #[spec] let v_prev = v;
  *v.index_mut_increasing(4) = e + v2.index(4); // single statement with direct assigment
  assert(sum(v) > 20);
  sort(&'b mut v);
  assert(exists(|i: nat| i < v.len() && v.index(i) == v_prev.index(i) + v2.index(4)));
}

Example 6. Option<&mut> brought up by @tjhance. A function on a hashtable to optionally obtain a mutable reference to a value, if the key is present:

impl HashTable<K, V> {
  pub fn borrow_mut<'a>(&'a mut self, key: K) -> (ref: Option<&'a mut V>) {
    ensures if self.contains(key) {
      ref.is_some() && ref.value() == old(self).get(key)
    } else {
      equal(*ref, None)
    }
    after<'a> {
      ensures self.view() == old(self).view().set(key, *ref.value()),
    }
    
    // ...
  }
}

This example depends on implementing enum .is_variant() and .field() , similar to Dafny's .Variant? (e.g. .Some?) and Dafny's field accessors (for enums).

Example 6b. Caller, without reborrows, but with helper functions on Option:

fn increment(ht: &mut HashTable<u64, i64>, key: u64) {
  requires(ht.contains(key));
  ensures(ht.view() == old(ht).view().set(key, old(ht).view().get(key) + 1),
  let val = ht.borrow_mut(key);
  if val.is_some() {
    val.put(val.value() + 1);
  }
  expire(val);
}

Example 6c. Caller, with reborrows

• do we want to support re-borrows right away? It's more complex, due to the relationship between the returned mutable reference and val bound in the match pattern:

fn increment(ht: &mut HashTable<u64, i64>, key: u64) {
  requires(ht.contains(key));
  ensures(ht.view() == old(ht).view().set(key, old(ht).view().get(key) + 1),
  if let Some(ref mut val) = ht.borrow_mut(key) {
    *val = *val + 1;
  }
}

Prusti¹'s pledges

The ensures clause in after is similar to Prusti's pledges, as it addresses the same issue, how to specify what happens due to the modification of the part of the lender that was returned by the function as a mutable borrow. The requires clause in after seems however to not have a direct equivalent in Prusti's pledges (it could however be encoded as an implication that would result in a weak postcondition if the antecedent encoding the required final value of the borrow is false).

Example. From the Prusti paper, adapted to Verus' syntax.

struct Point {
  x: i32,
  y: i32
}
struct Route {
  current: Point,
  rest: Option<Box<Route>>,
}
impl Route {
  fn view() -> Seq<Point> { .. }
}
fn length(r: &Route) -> u64 {
  ensures(|res: u64| res == r.view().len());
  1 + match r.rest {
    Some(box ref q) => length(q),
    None => 0,
  }
}
fn nth_x(r: &Route, n: usize) -> i32 {
  requires(n < r.view().len());
  ensures(|res: i32| res == r.view().index(n).x);
  if n == 0 { r.current.x } else {
    match r.rest {
      Some(box ref q) => nth_x(q, n - 1),
      None => unreached()
    }
  }
}
// following the Prusti example:
fn nth_point<'a>(r: &'a mut Route, n: usize) -> &'a mut Point {
  requires(n < r.view().len());
  ensures(|res: &mut Point| res.x == nth_x(old(r), n));
  after<'a>(|res: &mut Point| {
    ensures(r.view().len() == old(r).view().len());
    ensures(nth_x(r, n) == res.x)
    ensures(forall(|i: nat| i < r.view().len() && i != n >>= nth_x(r, i) == nth_x(old(r), i)))
  })
  
  // ...
}
// or, using the `.view()`:
fn nth_point<'a>(r: &'a mut Route, n: usize) -> &'a mut Point {
  requires(n < r.view().len());
  ensures(|res: &mut Point| res.x == nth_x(old(r), n));
  after<'a>(|res: &mut Point| {
    ensures(r.view() == old(r).view().update(n, *res));
  })
  
  // ...
}

Verification conditions for the function body

Given a

struct A {
  m: u64,
  n: u64,
}

we can write a function

impl A {
  pub fn borrow_either(&mut self, which: bool) -> &mut u64 {
    ensures(|ref: &mut u64| *ref == if which { self.m } else { self.n });
    after<'a>(|ref: &mut V| {
      ensures([ // after the end of the borrow
        if which [
          self.m == *ref && self.n == old(self).n
        ] else {
          self.m == old(self).m && self.n == *ref
        }
      ]);
    });
    if which {
      &mut self.m
    } else {
      &mut self.n
    }
  }
}

• only allow directly returning a borrow to avoid the issue of handling pointer variables?

Open questions

• allow re-assigning the pointer variable? What to do then? Phrophecy variables a-la RustHorn?

---

I believe that what I'm proposing is not too dissimilar from Prusti's "pledges" (but the encoding may turn out different).
I will be extending the doc with a bit more about my plans for the VC generation (initially, for the call-site).
The doc also has a stub regarding VC to check the function body, but I'm currently leaving that for later: this is because we have multiple immediate uses of functions returning &mut where the body is trusted (e.g. Vec's index_mut). It is important to keep in mind to avoid deciding on a specification language that ends up awkward for body VCs.

I would appreciate input on what you think about the usability of the function's specification constructs (after), and what you think of the semantics at the call site (borrow expiration, potentially required to be explicit initially)

I’m planning this in part to be an incremental path, where initially we, for example, do not support re-assigning to a pointer variable (a challenge that the RustHorn paper tries to address, I believe) and we do not support re-borrowing (i.e. constructing a mutable reference to a part of a value pointed by an existing mutable reference).

Footnotes

1. Leveraging Rust Types for Modular Specification and Verification -- http://pm.inf.ethz.ch/publications/getpdf.php?bibname=Own&id=AstrauskasMuellerPoliSummers19b.pdf ↩

[utaal]

"Re-assigning to a pointer variable" refers to cases like this:

let a = 13;
let b = 15;
let mut c = &mut a;
if (cond) {
  c = &mut b;
}
*c += 1;

Re-borrowing is cases like this:

if let Some(ref mut a) = hash_map.get_mut(key) { // the original borrow is the &mut returned by `get_mut`
  // `a` re-borrows the contents of the returned `&mut`
}

[tjhance]

So for the mem allocator, I'm starting to think it's going to be really helpful to have more &mut support. Especially things to get &mut references from pointers which requires functions that return &mut. @jaybosamiya also mentioned that additional &mut support would be helpful for whatever he's doing. I'd like to start moving forward on this.

Here's my perspective on the design:

The RustHorn encoding, which uses prophecy variables, is very clean. I think it's probably the encoding that will be easiest to implement VC generation for; it is very general (supporting containers that contain &mut types, or assigning to a reference variable, for example); it does not require much "special casing" of &mut T types compared with other types; VIR can continue to ignore everything related to lifetime variables.

One downside is that it might be a little more challenging for users to grok. I think the 'pledge' style, as @utaal illustrates in a bunch of examples above, may be a little easier to understand, and could possibly lead to better diagnostics (e.g., "This borrow expires on line XY, but the pledge at line ZW from this call is not satisfied"). However, since I think the RustHorn prophecy encoding makes for the most general foundation, I think it might be better to start there, and then if it's hard to use, add pledge-style specifications as a special syntax to aid diagnostics.

The other challenge for the prophecy encoding is that we need to implement prophecy variables soundly, although there are some other things I think prophecy variables might be useful for, so I don't see this as much of a downside.

The Prophecy Encoding

The prophecy encoding represents a &mut T as a pair (current_value, final_value): (T, T). The final_value is a prophecy value that represents the value the mutable reference will have later when the borrow expires.

For example, suppose you have a variable mut x: T and you mutably borrow from it, obtaining x_ref: &mut T.

• When the borrow begins, we create a fresh prophecy variable for the final value of the borrow, call it x_prophecy. We assign the pair (x, x_prophecy) as the encoded value of x_ref, and then we immediately update the value of x to x_prophecy. Initially, it seems weird to update x immediately, but by the next time the variable x is used, the mutable value will have expired, and x_prophecy by definition is the value it will have that point.
• When we update *x_ref, we update the first element of the tuple.
• When x_ref expires, we can assume current_value == final_final.

Here's a worked example:

                                    AIR-level encoding                        concrete values

let mut x = 5;                      assign x := 5                             x: 5

let mut x_ref = &mut x;             assign x_ref := (x, prophecy_x)               
                                    assign x := prophecy_x                    x: 20, x_ref: (5, 20) 

*x_ref = 7;                         assign x_ref := (7, x_ref.1)              x: 20, x_ref: (7, 20) 

*x_ref = 20;                        assign x_ref := (20, x_ref.1)             x: 20, x_ref: (20, 20) 

/* x_ref expires */                 assume (x_ref.0 == x_ref.1)

assert(x == 20);                    assert (x == 20);

The assert at the end follows because:

• x == prophecy_x == encoding(x_ref).1 (from the initial borrow)
• encoding(x_ref).1 == encoding(x_ref).0 (from the borrow expiration)
• encoding(x_ref).0 == 20 (from the last assignment to *x_ref)

Method calls with &mut as an argument.

An advantage of this encoding is that, since an encoded &mut T value is just a pair (T, T), we can basically treat mutable references as being a lot like any other type.

For example, today, when a function takes x: &mut T as an argument, we create an 'in' parameter x_old and an 'out' parameter x_new. We allow the user to reference x_old in the precondition, and we allow them to reference both in the postcondition.

fn example(a: &mut T)
    requires *old(a) < 10
    ensures *a == *old(a) + 5

With the prophecy encoding, where we encode a mutable reference as a pair, this would mean that the function takes (x_old, x_new) as input. Since x_new is already part of the input parameters, we don't need to create an extra out-parameter.
We just have the one input represented by its prophecy-encoded pair value, which I'll call encoding:

fn example(a: &mut T)
    requires encoding(a).0 < 10
    ensures encoding(a).1 == encoding(a).0 + 5

We can just define old(a) to be encoding(a).0 and perhaps new(a) (or future(a), or something) to be encoding(a).1.
Then we'd be able to write this spec in a similar way to how we do it today.

In principle, the specification can now talk about new(a) in the precondition, though this would probably be uncommon. (It's not possible for the caller to prove anything about new(a), because the "prophecy" hasn't resolved yet.)

The caller is going to end up generating VCs really similar to what it does now. The only difference is that x_new is treated as part of the input parameter that it happens to learn stuff about from the postcondition of the call.

Method calls that return &mut

The spec for a function that returns &mut don't need any extra clauses beyond the 'requires' and 'ensures' clause:

struct Animal {
  cat: u64,
  dog: u64,
}

fn get_cat_ref(animal: &mut Animal) -> (cat: &mut u64)
    ensures
        new(animal).dog == old(animal).dog,   // animal.dog isn't changed
        old(cat) == old(animal).cat,          // the value of `*cat` upon return
        new(cat) == new(animal).cat,          // tells how the value of `*cat` flows back to `animal.cat` upon expiration

More complex example, also illustrating a container with mutable references:

fn borrow_two_from_vec(v: &mut Vec<A>, i: usize, j: usize) -> (pair: (&mut A, &mut A))
    requires i != j
    ensures
        old(pair.0) == v[i],
        old(pair.1) == v[j],
        new(v) == old(v).update(i, new(pair.0)).update(j, new(pair.1))

The borrow_mut example from Andrea's post:

impl HashTable<K, V> {
    pub fn borrow_mut<'a>(&'a mut self, key: K) -> (ref: Option<&'a mut V>)
    ensures
        if self.contains(key) {
            ref.is_Some()
              && old(ref.get_Some_0()) == old(self).get(key)
              && new(self).view() == old(self).view().set(key, new(ref.get_Some_0())),
        } else {
            ref.is_None()
        } 
}

These are basically exactly the same conditions Andrea wrote in his example, except here they all go in the ensures clause, rather than putting some of them in a pledge.

Implementing prophecy variables

The difficulty with prophecy variables is we need to make sure there's no unsoundness by "making decisions" based on future
information.

For example:

let mut a = 0;
let ref = &mut a;

let future_value_of_a = new(ref); // look at the prophecy

if future_value_of_a == 3 {
    *ref = 20;
} else {
    *ref = 3;
}

/* let `ref` expire */

assert(a == 3 <==> a != 3);
assert(false);

This isn't an issue if we're borrow exec-mode state, since our mode-checking already makes sure that exec-code can't depend on spec-code, and prophecy variables are necessarily spec-code. However, we also want to support mutable-borrows of proof-mode (tracked) variables in ghost code. I'm guessing the other tools in this space haven't run into this problem, since they don't use the same techniques with tracked code. (Meanwhile, borrowing spec-variables is probably not as useful.)

Therefore, to make sure there isn't any unsoundness, we need to make sure that mutable-variable updates can't possibly depend on prophecy values. However, I think we can still get pretty far with a very simple solution: only allow accessing the prophecy variable new(...) in places where it very obviously can't have any 'effects' (e.g., requires and ensures clauses).

Concrete steps

If we go forward this route, I think we'd need to make the following changes:

• Remove special casing of &mut and instead treat it like any other type constructor.
• Encode a mutable-ref as a pair, implement the VCs as described
• change old to work as described above
• implement new as described above, but only allow it in specification clauses

[jaybosamiya]

Just making a quick note that calling it new can become confusing for new users to Verus (as the opposite of old); future/expiry/on_expire/... might be better?

[tjhance]

Proposal for resolving the current challenges with resolve

My proposal is to split Andrea's resolve into two things:

• finalize_mut_ref (applied to a &mut T). This is the mutref-bye rule in RustHornBelt
• regain_access (applied to a place that is borrowed from). This is the endlft rule in RustHornBelt

We can keep using the name resolve but I'm using hyper-explicit names here for clarity.

For user experience, we can:

• Ask the user to write regain_access except in very simple cases, similar to the way Andrea's current proposal works with the resolve keyword
• Aggressively infer the finalize_mut_ref locations

Example:

let mut a = 5;
let mut a_ref = &mut a;

*a_ref = 20;

finalize_mut_ref(a_ref);
// assert(a == 20); // not allowed because we haven't regained access to a yet
regain_access(a);

assert(a == 20);

If finalize_mut_ref is inferred, the user is only writing:

let mut a = 5;
let mut a_ref = &mut a;

*a_ref = 20;

regain_access(a);

assert(a == 20);

Soundness

Soundness factors into two things:

• finalize_mut_ref(a_ref) needs to be after every mutation of *a_ref (this includes re-borrows of *a_ref) and before the lifetime expires.
• regain_access needs to be after the lifetime expires.

Pretty sure these can all be checked using methodology similar to what we're doing now. Conceptually, finalize_mut_ref(a_ref) consumes the a_ref (preventing uses afterwards and demanding that its lifetimes be active) and regain_access just needs to check that a can be accessed.

Inferring the placement of finalize_mut_ref

This isn't quite the same thing as finding the 'drops' because drops always go at the end of the scope.

I think we can probably do our own analysis here. I don't know what information Rust gives us so maybe there's something helpful there. We basically just want to find the 'last use' of a reference in any given function. This requires us to be very careful about the distinction between moving a mutable reference and performing a re-borrow:

Examples:

fn test1(a_ref: &mut T) {
    *a_ref = 20;
                            // finalize_mut_ref(a_ref) goes here
    stuff();
}

fn test2(a_ref: &mut T) -> &mut T {
    *a_ref = 20;
    stuff();
    a_ref             // a_ref is moved here, so this function isn't responsible for finalizing this mut-ref
}

fn test3(a_ref: &mut T) -> &mut T {
    *a_ref = 20;
    stuff(Some(a_ref));  // a_ref is moved here, so this function isn't responsible for finalizing this mut-ref
}

fn test4(a_ref: &mut T) -> &mut X {
    let b_ref = &mut a_ref.b;      // This is a *reborrow* so a_ref is not moved (also in the prophecy encoding, this is considered to immediately update the value of `*a_ref`)
                                   // finalize_mut_ref(a_ref) goes here
    b_ref
}

[utaal]

Mechanics of regain_access:

fn regain_access<A>(a: &mut A) { }

fn main() {
    let mut a = 5;
    let mut a_ref = &mut a;
    
    *a_ref = 20;
    
    // finalize_mut_ref(a_ref);
    regain_access(&mut a);
    
    *a_ref = 40;
}

error[E0499]: cannot borrow `a` as mutable more than once at a time
  --> src/main.rs:13:19
   |
7  |     let mut a_ref = &mut a;
   |                     ------ first mutable borrow occurs here
...
13 |     regain_access(&mut a);
   |                   ^^^^^^ second mutable borrow occurs here
14 |     
15 |     *a_ref = 40;
   |     ----------- first borrow later used here

[utaal]

Mechanics of finalize_mut_ref at the rust source level:

fn regain_access<A>(a: &mut A) { }
fn finalize_mut_ref<A>(a: A) { }

fn main() {
    let mut a = 5;
    let mut a_ref = &mut a;
    
    *a_ref = 20;
    
    finalize_mut_ref(a_ref);
    finalize_mut_ref(a_ref);
    regain_access(&mut a);
    
    // *a_ref = 40;
}

[dewert99]

I read this discussion and think parts of my MSc thesis https://dx.doi.org/10.14288/1.0438326 are relevant and might be helpful.

Chapter 2 is about designs for a specification language which is largely expression-based and tries to "follow Rust rules", based on the syntax used in Prusti but with a lot more expressiveness than the tool supports (particularly w.r.t. mutable references). It ultimately presents a type system that classifies whether a specification is well-formed or not (essentially: whether expressions are being evaluated in a state that Rust would allow). This chapter also includes a translation of these well-typed specifications to Creusot's prophecy-based specification language. This would potentially enable a tool to allow users to interact with a Prusti-like (expression-based) syntax while giving a prophecy-based encoding to the SMT solver.

Chapter 3 deals with the soundness of combining the prophecy encoding used in Creusot with ghost state and shows that this can be made sound when limiting the operations allowed when creating ghost types. Following this proposal, Creusot ended up splitting its logic functions (the equivalent of Verus's spec functions) into regular logic functions which restrict the operations supported (mostly not allowing the final operator) but can be used to create ghost types, and logic(prophetic) functions which do support accessing the final value but are not allowed to be used when creating ghost types.
I'd be happy to answer any questions about this work if useful; I'm sure Alex Summers (who was my supervisor, although I've recently graduated) would also be interested in the topics if you'd like more opinions/discussion.

[keyboardDrummer]

@tjhance you gave the following example for how ensure clauses could be use to specify contracts involving mut:

struct Animal {
  cat: u64,
  dog: u64,
}

fn get_cat_ref(animal: &mut Animal) -> (cat: &mut u64)
    ensures
        new(animal).dog == old(animal).dog,   // animal.dog isn't changed
        old(cat) == old(animal).cat,          // the value of `*cat` upon return
        ^ Note: should't this be 'cat' instead of 'old cat', since the variable `cat` did not exist before the call?
        new(cat) == new(animal).cat,          // tells how the value of `*cat` flows back to `animal.cat` upon expiration

From a user perspective, that looks cumbersome to me, because I need to specify everything that's not changed by get_cat_ref. In this case it is only animal.dog that's the same, but it could be an arbitrary number of fields.

Also, shouldn't the ensure clause also specify the value of animal upon return, using clauses like the following?

  animal.cat == old(animal.cat),
  animal.dog == old(animal.dog),

My gut feeling is it would be good if by default the contract assumes that values in the contexts beforeCall(old), afterCall and afterBorrow(new) are equal to each other, unless otherwise specified.

I can imagine you would prefer to save discussion what's an optimal syntax to later, but for the sake of providing predictable verification time, I think there's value in having the size of the SMT encoding match the size of the specification provided by the user, so then the choice for syntax could influence the encoding as well.

For example, something which I question about the current limited support for mut, is that Verus code like:

struct S {
  a: u64,
  ...
  z: i64
}

fn updateA(s: &mut S)
{
  s.a = 1;
}

Generates AIR code for updateA that corresponds to the (large) size of S, not the (small) size of updateA

[keyboardDrummer]

old and new aren't referring to the pre-state and post-state of the variable w.r.t. to the method call. That's how they work now, but the proposal is to extend the to also apply to &mut variables in the return position (and other places). Admittedly, the names probably aren't great for this extended use-case; they're just place holders.
So:
old(cat) refers to the the value of the reference "now" (since this is the ensures clause, that means the point in time when the function call returns)
new(cat) refers to the value of the mutable reference when it expires.

Why not always use three different ways to refer to: before the call, after the call, and after the borrow? I thought you were using old to refer to before the call, new/future/next to refer to after the borrow, and neither old or new to refer to immediately after the call.

So new(cat) == new(animal).cat basically explains how the value of cat will flow back into the value of animal at the time that the borrows expire. If this still doesn't make sense, I suggest re-reading my post about prophecy variables.

That made sense.

I do kind of like the idea of a shorthand notation that would apply to both old and new states

Thanks. I think it's great to think about what the user experience should be, separately from how it would be encoded.

I'm not entirely sure what your moves ... -> notation is supposed to be getting at.

Given

fn choose_cat<'a>(use_x: bool, x: &'a mut Animal, y: &'a mut Animal) -> (r: &'a mut u64)
  modifies {} // implicit
  moves if use_x { x -> r, y -> y } else { y -> r, x -> x }
  ensures if use_x { r =&= x.cat  } else { r =&= y.cat } // =&= is reference equality. no need to use old, because nothing was mutated

then ensures if use_x { r =&= x.cat } else { r =&= y.cat } is shorthand for

ensures 
  if use_x { after_call(r) == after_call(x).cat && after_borrow(r) == after_borrow(x).cat }
  else { after_call(r) == after_call(y).cat && after_borrow(r) == after_borrow(y).cat }

and modifies {} is shorthand for:

ensures after_call(x) == before_call(x), after_call(y) == before_call(y) 

but then we're still missing

ensures 
  if use_x { after_call(y) == after_borrow(y) && after_call(x).dog == after_borrow(x).dog }
  else { after_call(x) == after_borrow(x) && after_call(y).dog == after_borrow(y).dog }

which I had hoped to get out of the combination of the moves clause and reference equality.

---

I'd like to talk about performance of the encoding as well. Have you read? "Aeneas: Rust Verification by Functional Translation" Their transformation turns a mutating Rust program into one without mutation. However, as I understand it, the translated code will, if you mutate a tiny part of a large tree, define the mutated tree by rebuilding each tree node between the root and the updated value.

Verus currently does something similar. If I create a tree of data using structs, and then update a leaf of that tree, Verus defines the new value by redefining every node between the lead and the tree root, where defining a node requires specifying the value of each of its fields.

Here's an example. Given

struct S {
  a: S2,
  b: S2,
  c: S2,
}

struct S2 {
  a: S3,
  b: S3,
  c: S3
}

struct S3 {
  a: i32,
  b: i32,
  c: i32
}

fn update_large_struct(s: &mut S) {
  s.b.b.c = 10;
}

the size of the encoding of update_large_struct is not linear in the size of its body, but in the surface of the path through which it mutates:

;; Function-Def testing::update_large_struct
;; /Users/rwillems/SourceCode/verus/source/rust_verify/example/prep/testing.rs:148:1: 148:34 (#0)
(check-valid
 (declare-var s! testing!S.)
 (axiom fuel_defaults)
 (axiom (has_type (Poly%testing!S. s!) TYPE%testing!S.))
 (block
  (snapshot snap%PRE)
  (snapshot snap%ASSIGN)
  (havoc s!)
  (assume
   (= (testing!S3./S3/c (%Poly%testing!S3. (Poly%testing!S3. (testing!S2./S2/b (%Poly%testing!S2.
         (Poly%testing!S2. (testing!S./S/b (%Poly%testing!S. (Poly%testing!S. s!))))
     ))))
    ) 10
  ))
  (assume
   (and
    (= (testing!S./S/a (old snap%ASSIGN s!)) (testing!S./S/a s!))
    (= (testing!S2./S2/a (testing!S./S/b (old snap%ASSIGN s!))) (testing!S2./S2/a (testing!S./S/b
       s!
    )))
    (= (testing!S3./S3/a (testing!S2./S2/b (testing!S./S/b (old snap%ASSIGN s!)))) (testing!S3./S3/a
      (testing!S2./S2/b (testing!S./S/b s!))
    ))
    (= (testing!S3./S3/b (testing!S2./S2/b (testing!S./S/b (old snap%ASSIGN s!)))) (testing!S3./S3/b
      (testing!S2./S2/b (testing!S./S/b s!))
    ))
    (= (testing!S2./S2/c (testing!S./S/b (old snap%ASSIGN s!))) (testing!S2./S2/c (testing!S./S/b
       s!
    )))
    (= (testing!S./S/c (old snap%ASSIGN s!)) (testing!S./S/c s!))
))))

My desire is that the performance of verification is predictable for the programmer, and my intuition is that for Verus to achieve that, the size of the generated encoding must correspond to the size of the input program. The above encoding violates that principle.

By using a Map to encode composite data, we can express updating a subcomponent of that data using a single quantifier:

type Ref
type Value
type Tree = Map[Ref, Value]
let tree_1: Tree
let tree_2: Tree
let updated_node: Ref
let updated_value: Value

assume forall node: Ref ::  
  if node = updated_node then tree_2[node] = updated_value
  else (node in domain(tree_1) => tree_2[node] = tree_1[node])

which would allow representing any update operation using a constant amount of SMT.

[tjhance]

Why not always use three different ways to refer to: before the call, after the call, and after the borrow? I thought you were using old to refer to before the call, new/future/next to refer to after the borrow, and neither old or new to refer to immediately after the call.

There are only two: 'old' and 'new'/'future'. In the discussion, I sometimes used 'future' and 'new' interchangeably since I wasn't sure what the best word to use was. To be honest, all these names can be remarkably confusing depending on the context.

For example, the word old makes sense from the user perspective, because it sounds like it means "the value of this variable at some previous point in time, right before the method was called". And this usually makes intuitive sense, but it's a totally nonsense interpretation from the perspective of the formal encoding. If you have an input argument like animal: &Animal, then (from the encoding's perspective) it already has all its 2-state data when it's input, and none of this data is mutated between the pre and post states.

From the perspective of the encoding, current and future would probably make the most sense, but then this has the opposite problem; it would be profoundly confusing from the user's perspective since you would be using 'current' to refer to the pre-state, even in the ensures clause!

I'd like to talk about performance of the encoding as well.

I agree the encoding is kind of bulky, but I don't think there's much evidence that it's a real problem right now. I think there are improvements we could make without having to introduce a ref map (and I'm skeptical that a ref map would be an improvement).
For example, we could have an update field function, and then the encoding would only mention the fields that get updated.

@parno I vaguely recall you had some wisdom-from-experience about this specific topic (updating fields in structs) - do you have anything to chime in?

[parno]

Once upon a time, in Dafny, if you wrote w.(x := 2).(y := 3).(z := 4), Dafny would create a version of w's type for each individual update, which could lead to exponential growth in term size. Specifically, it was originally the case that Dafny would rewrite an update of the form "dt[dtor := E]" to be "dtCtr(E, dt.dtor2, dt.dtor3,...)" but dt.dtor2 etc. were themselves updates. We changed it to be "let d' := dt in dtCtr(E, d'.dtor2, d'.dtor3,...)" instead. You can see the commit dafny-lang/dafny@1b309976dba09a49 for more details.

[dewert99]

Why not always use three different ways to refer to: before the call, after the call, and after the borrow? I thought you were using old to refer to before the call, new/future/next to refer to after the borrow, and neither old or new to refer to immediately after the call.

Thinking about this way of referring to program states would actually need a more general strategy for "after the borrow" since there may be multiple borrows with different lifetimes ending at the same time. In my thesis we used old for before the call, at::<'a> for after the borrow with lifetime 'a, and had ensures clauses refer to the state after the call by default.

Using the prophecy encoding, only two states of each mutable reference are encoded at the SMT level, the mutable reference's initial state (before the call for parameters, after the call for the returned value), and the state where where the mutable references lifetime expires (this may be the same as the state "after the call" if the lifetime is short lived). I believe that these two states are what @tjhance are referring as old and new/future respectively (Creusot uses * and ^).

Using the choose_cat example, the specification using the state based representation from my thesis would look like:

fn choose_cat<'a>(use_x: bool, x: &'a mut Animal, y: &'a mut Animal) -> (r: &'a mut u64)
    ensures
    if use_x { 
      at::<'a>(x.cat) == at::<'a>(*r) && // value of r flows back after the borrow
      at::<'a>(x.dog) == old(x.dog) && // dog is unchanged after the borrow
      at::<'a>(x.rat) == old(x.rat) && // rat is unchanged after the borrow
      at::<'a>(*y) == old(*y) && // y is unchanged after the borrow
      *r == old(x.cat) // the value of r upon return
    } else {
        ...
    }

would get translated to:

	old / before the call	/ after the call	at::<'a> / after the borrow
x	old	invalid	new
y	old	invalid	new
r	invalid	old	new

fn choose_cat<'a>(use_x: bool, x: &'a mut Animal, y: &'a mut Animal) -> (r: &'a mut u64)
    ensures
    if use_x { 
      new(x).cat == new(r) && // value of r flows back after the borrow
      new(x).dog == old(x).dog && // dog is unchanged after the borrow
      new(x).rat == old(x).rat && // rat is unchanged after the borrow
      new(y) == old(y) && // y is unchanged after the borrow
      old(r) == old(x).cat // the value of r upon return
    } else {
        ...
    }

I'm not convinced that there is value in stating that x is the same before and after the call (@keyboardDrummer 's modifies clause), since x cannot be access after the call until the borrow expires anyway.

[keyboardDrummer]

Hey @dewert99, thanks for chiming in.

Using the prophecy encoding, only two states of each mutable reference are encoded at the SMT level

That makes sense, but I would think that for the user it would be better to use different keywords to refer to either before or immediately after the call, even though a single keyword, such as old in your example, would suffice.

Using the choose_cat example, the specification using the state based representation from my thesis would look like:

fn choose_cat<'a>(use_x: bool, x: &'a mut Animal, y: &'a mut Animal) -> (r: &'a mut u64)
    ensures
    if use_x { 
      at::<'a>(x.cat) == at::<'a>(*r) && // value of r flows back after the borrow
      at::<'a>(x.dog) == old(x.dog) && // dog is unchanged after the borrow
      at::<'a>(x.rat) == old(x.rat) && // rat is unchanged after the borrow
      at::<'a>(*y) == old(*y) && // y is unchanged after the borrow
      *r == old(x.cat) // the value of r upon return
    } else {
        ...
    }

IMO we should be able to specify the behavior in a way that is at least as simple as the implementation, which in this case would be:

fn choose_cat<'a>(use_x: bool, x: &'a mut Animal, y: &'a mut Animal) -> &'a mut u64 {
  if use_x { &mut x.cat } else { &mut y.cat }
}

So if we could write a specification like:

fn choose_cat<'a>(use_x: bool, x: &'a mut Animal, y: &'a mut Animal) -> (r: &'a mut u64)
  ensures r == if use_x { &mut x.cat } else { &mut y.cat }

and interpret that as what you specified above, that would be ideal.

But, if we change the function so it does:

fn mutate_and_choose_cat<'a>(use_x: bool, x: &'a mut Animal, y: &'a mut Animal) -> &'a mut u64 {
  x.cat = x.cat + 1;
  if use_x { &mut x.cat } else { &mut y.cat }
}

Then I would like to specify only:

fn mutate_and_choose_cat<'a>(use_x: bool, x: &'a mut Animal, y: &'a mut Animal) -> (r: &'a mut u64)
  ensures 
    r == if use_x { &mut x.cat } else { &mut y.cat } &&
    after(x.cat) == before(x.cat) + 1
  modifies x.cat // I think something like this is needed. Maybe we could infer it based on the ensures clause
  // In the specification of `choose_cat` there was an implicit "modifies {}"

Note that I'm comparing the after and before state of x.cat, which you seem to state state is not useful since x is not accessible at the after time. However, I do think it is useful in this example, to provide a succinct specification.

Method

I think we can use the lifetime signature together with ensures r == if use_x { &mut x.cat } else { &mut y.cat } to infer:

ensures
if use_X {
      at::<'a>(x.cat) == at::<'a>(*r) && // value of r flows back after the borrow
      at::<'a>(x.dog) == after(x.dog) && // after the call, dog is unchanged until the borrow ends
      at::<'a>(x.rat) == after(x.rat) && // after the call, rat is unchanged until the borrow ends
      at::<'a>(*y) == after(*y) && // after the call, y is unchanged until the borrow ends
} else {
  ...
}

and modifies x.cat to infer:

before(x.dog) == after(x.dog) && // dog is unchanged during the call
before(x.rat) == after(x.rat) && // rat is unchanged during the call
before(*y) == after(*y) && // y is unchanged during the call

so that we get in total:

fn mutate_and_choose_cat<'a>(use_x: bool, x: &'a mut Animal, y: &'a mut Animal) -> (r: &'a mut u64)
  ensures
(if use_X {
      at::<'a>(x.cat) == at::<'a>(*r) && // value of r flows back after the borrow
      at::<'a>(x.dog) == after(x.dog) && // after the call, dog is unchanged until the borrow ends
      at::<'a>(x.rat) == after(x.rat) && // after the call, rat is unchanged until the borrow ends
      at::<'a>(*y) == after(*y) // after the call, y is unchanged until the borrow ends
} else {
  ...
}) &&
after(x.dog) == before(x.dog) && // dog is unchanged during the call
after(x.rat) == before(x.rat) && // rat is unchanged during the call
after(*y) == before(*y) && // y is unchanged during the call
after(x.cat) == before(x.cat) + 1

Which would be equivalent to what you specified.