Ownership in Flux

#![allow(unused)]
extern crate flux_rs;
use flux_rs::attrs::*;

Online demo

Previously we saw how to refine basic Rust types like i32 and bool with indices and constraints to constrain the set of values described by those types. For instance, we wrote the function assert function which can only be called with true

#[flux_rs::spec(fn (bool[true]))]
fn assert(b: bool) {
    if !b {
        panic!("assertion failed");
    }
}

fn test_assert() {
    assert(2 + 2 == 4);
    assert(2 + 2 == 5); // fails to type check
}

The whole point of Rust, of course, is to allow for efficient imperative sharing and updates, via the clever type system that keeps an eye on the ownership of resources to make sure that aliasing and mutation cannot happen at the same time.

Next, lets see how Flux melds refinements and Rust's ownership mechanisms to make refinements pleasant in the imperative setting.

Exclusive Ownership

Rust's most basic form of sharing is exclusive ownership, in which exactly one variable in a function has the right to mutate a memory location. When a location is exclusively owned, we can be sure that there are no other references to it. Consequently, flux can update the type to precisely track the value whenever the location is changed.

For example, consider the program

#[flux_rs::spec(fn () -> i32[3])]
pub fn mk_three() -> i32 {
  let mut r = 0;  // r: i32[0]
  r += 1;
  assert(r == 1); // r: i32[1]
  r += 1;
  assert(r == 2); // r: i32[2]
  r += 1;
  assert(r == 3); // r: i32[3]
  r
}

The variable r has different types at each point inside mk_three. It starts off as i32[0]. The first increment changes it to i32[1], then i32[2] and finally, the returned type i32[3].

Exclusive Ownership and Loops

This exclusive ownership mechanism is at work in the factorial example we signed off with previously

#[flux_rs::spec(fn (n:i32{0 <= n}) -> i32{v:n <= v})]
pub fn factorial(n: i32) -> i32 {
    let mut i = 0;  // i: i32[0]
    let mut r = 1;  // r: i32[1]
    while i < n {
                    // i: i32{v:0 <= v <= n}
                    // r: i32{v:1 <= v && i <= v}
        i += 1;
        r = r * i;
    }
    r
}

In the above code, i and r start off at 0 and 1 but then flux infers (a story for another day) that inside the while-loop¹

i has type i32{v:0<=v && v < n}
r has type i32{v:1<=v && i <= v}

and hence, upon exit since i == n we get that the result is at least n.

Borrowing: Shared References

Exclusive ownership suffices for simple local updates like in factorial. However, for more complex data, functions must temporarily relinquish ownership to allow other functions to mutate the data.

Rust cleverly allows this via the notion of borrowing using two kinds of references that give callee functions temporary access to memory location.

The simplest kind of references are &T which denote read-only access to a value of type T. For example, we might write abs to take a shared reference to an i32

#[flux_rs::spec(fn (p: &i32[@n]) -> i32{v:0<=v && n<=v})]
pub fn abs(p: &i32) -> i32 {
    let n = *p;
    if 0 <= n {
        n
    } else {
        0 - n
    }
}

Notice that the input type has changed. Now, the function

accepts p, a reference to an i32 whose value is n as denoted by @n
returns an i32 that is non-negative and larger than n

The @ marks the n as a refinement parameter whose value is automatically computed by flux during type checking.

Calling `abs` with a reference

So, for example, Flux can check the below code by automatically determining that the refinement parameter at the call-site is 10.

pub fn test_abs() {
    let z = 10;
    assert(0 <= abs(&z));
    assert(10 <= abs(&z))
}

As an aside, we have secretly been using refinement parameters like @n all along. For example, Flux automatically desugars the signature fn(n:i32{0 <= n} -> ... that we wrote for factorial into

fn ({i32[@n] : 0 <= n}) -> i32{v:n <= v}

where @n is a refinement parameter that is implicitly determined from the rust parameter n:i32. However, explicit parameters are essential to name the value of what a reference points to. In abs the rust parameter p names the reference but the @n names the (input) value and lets us use it to provide more information about the output of abs.

EXERCISE Flux is modular in that the only information it knows about the implementation of abs is the signature. For example, suppose we change the output type of abs to i32{v:0<=v}, that is, we remove the n <= v conjunct. Can you predict which assert will be rejected by flux?

Borrowing: Mutable References

References of type &mut T denote mutable references that can be used to (read and) write or update the contents of a T value. Crucially, Rust ensures that while there may be multiple read-only (shared) references to a location, there is at most one active writeable (mutable) reference at any point in time.

Flux exploits the semantics of &mut T to treat T as an invariant of the underlying data. As an example, consider the following function that decrements the value of a mutable reference while ensuring the data is non-negative:

#[flux_rs::spec(fn(p: &mut i32{v:0 <= v}))]
pub fn decr(p: &mut i32) {
    *p = *p - 1;
}

Flux complains that

error[FLUX]: assignment might be unsafe
   |
13 |         *p = *p - 1;
   |         ^^^^^^^^^^^

as in fact, we may be writing a negative value into *p for example, if the old value was zero. We can fix this code by guarding the update with a test that ensures the original contents are in fact non-zero

EXERCISE Can you modify the code for decr so that flux verifies it?

Aliased References

Flux uses Rust's borrowing rules to track invariants even when there may be aliasing. As an example, consider the function

#[flux_rs::spec(fn (bool) -> i32{v:0 <= v})]
fn test_alias(z: bool) -> i32 {
    let mut x = 1;  // x: i32[1]
    let mut y = 2;  // y: i32[2]
    let r = if z { &mut x } else { &mut y };
                    // r: &mut i32{v:0 <= v}
    decr(r);
    *r
}

The reference r could point to either x or y depending on the (unknown) value of the boolean z. Nevertheless, Flux determines that both references &mut x and &mut y point to values of the more general type i32{v:0<=v} and hence, infers r : &mut i32{v:0<=v} which allows us it to then call decr with the reference and guarantee the result (after decr) is still non-negative.

Invariants are not enough!

In many situations, we want to lend a value to another function that actually changes the value's (refinement) type upon exit. For example, consider the following function to increment a reference to a non-negative i32

#[flux_rs::spec(fn (p: &mut i32{v:0 <= v}))]
fn incr_inv(p: &mut i32) {
  *p += 1
}

fn test_incr_inv() {
  let mut z = 10;
  incr_inv(&mut z);
  assert(z == 11);
}

The only information that flux has about incr what it says in its spec, namely, that p remains non-negative. Flux is blissfully unaware that incr increments the value of p, and it cannot prove that after the call, z == 11 and hence, complains that assert may fail even though it will obviously succeed!

Borrowing: Updatable References

To verify test_incr we need a signature for incr that says that its output is indeed one greater² than its input.

Flux extends Rust &mut T with the notion of updatable references which additionally specify how the type is changed when the function exits³, using an ensures clause that specifies the modified type of the reference.

#[flux_rs::spec(fn(p: &mut i32[@n]) ensures p:i32[n+1])]
fn incr(p: &mut i32) {
  *p += 1
}

The Flux signature refines the plain Rust one to specify that

p is a strong reference to an i32,
the input type of *p is i32[n], and
the output type of *p is i32[n+1].

With this specification, Flux merrily checks test_incr, by determining that the refinement parameter @n is 10 and hence, that upon return x: i32[11].

fn test_incr() {
  let mut z = 10;
  incr_inv(&mut z);
  assert(z == 11);
}

Summary

To sum up, Flux exploits Rust's ownership mechanisms to track properties of shared (&T) and mutable (&mut T) references, and additionally uses (ensures) clauses to specify when the type itself is changed by a call.

For those familiar with the term, these types are loop invariants ↩
Setting aside the issue of overflows for now ↩
Thereby allowing so-called strong updates in the type specifications ↩

The Flux Book