Refining Types

Types bring order to code. For example, if a variable i:usize then we know i is a number that can be used to index a vector. Similarly, if v: Vec<&str> then we can be sure that v is a collection of strings which may be indexed but of course, not used as an index. However, by itself usize doesn't tell us how big or small the number and hence the programmer must still rely on their own wits, a lot of tests, and a dash of optimism, to ensure that all the different bits fit properly at run-time.

Refinements are a promising new way to extend type checkers with logical constraints that specify additional correctness requirements that can be verified by the compiler, thereby entirely eliminating various classes of run-time problems.

To begin, lets see how flux lets you refine basic or primitive types like i32 or usize or bool with logical constraints that can be checked at compile time.

Indexed Types

The simplest kind of refinement type in flux is a type that is indexed by a logical value. For example

Flux Specifications

First off, we need to add some incantations that pull in the mechanisms for writing flux specifications as Rust attributes.

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

Post-Conditions

We can already start using these indexed types to start writing (and checking) code. For example, we can write the following specification which says that the value returned by mk_ten must in fact be 10

#[spec(fn() -> i32[10])]
pub fn mk_ten() -> i32 {
    5 + 4
}

Push Play Push the "run" button in the pane above. You will see a red squiggle that and when you hover over the squiggle you will see an error message

error[...]: refinement type error
  |
7 |     5 + 4
  |     ^^^^^ a postcondition cannot be proved

which says that that the postcondition might not hold which means that the output produced by mk_ten may not in fact be an i32[10] as indeed, in this case, the result is 9! You can eliminate the error by editing the body to 5 + 4 + 1 or 5 + 5 or just 10.

Pre-Conditions

You can use an index to restrict the inputs that a function expects to be called with.

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

The specification for assert says you can only call it with true as the input. So if you write

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

then flux will complain that

error[FLUX]: precondition might not hold
   |
12 |     assert(2 + 2 == 5); // fails to type check
   |     ^^^^^^^^^^^^^^^^^^

meaning at the second call to assert the input may not be true, as of course, in this case, it is not!

Can you edit the code of test to fix the error?

Index Parameters and Expressions

Its not terribly exciting to only talk about fixed values like 10 or true. To be more useful, flux lets you index types by refinement parameters. For example, you can write

#[spec(fn(n:i32) -> bool[0 < n])]
pub fn is_pos(n: i32) -> bool {
  if 0 < n {
    true
  } else {
    false
  }
}

Here, the type says that is_pos

• takes as input some i32 indexed by n
• returns as output the bool indexed by 0 < n

That is, is_pos returns true exactly when 0 < n.

We might use this function to check that:

pub fn test_pos(n: i32) {
  let m = if is_pos(n) { n - 1 } else { 0 };
  assert(0 <= m);
}

Existential Types

Often we don't care about the exact value of a thing -- but just care about some properties that it may have. For example, we don't care that an i32 is equal to 5 or 10 or n but that it is non-negative.

Flux allows such specifications by pairing plain Rust types with assertions ¹ that constrain the value.

Existential Output Types

For example, we can rewrite mk_10 with the output type i32{v:0<v} that specifies a weaker property: the value returned by mk_ten_pos is positive.

#[spec(fn() -> i32{v: 0 < v})]
pub fn mk_ten_pos() -> i32 {
    5 + 5
}

Example: absolute value

Similarly, you might specify that a function that computes the absolute value of an i32 with a type which says the result is non-negative and exceeds the input n.

#[spec(fn (n:i32) -> i32{v:0<=v && n<=v})]
pub fn abs(n: i32) -> i32 {
    if 0 <= n {
        n
    } else {
        0 - n
    }
}

Combining Indexes and Constraints

Sometimes, we want to combine indexes and constraints in a specification.

For example, suppose we have some code that manipulates scores which are required to be between 0 and 100. Now, suppose we want to write a function that adds k points to a score s. We want to specify that

• The inputs s and k must be non-negative,
• the inputs s + k <= 100, and
• The output equals s + k

#[spec(fn ({usize[@s] | s + k <= 100}, k:usize) -> usize[s + k])]
fn add_points(s: usize, k: usize) -> usize {
    s + k
}

fn test_add_points() {
    assert(add_points(20, 30) == 50);
    assert(add_points(90, 30) == 120); // fails to type check
}

Note that we use the @s to index the value of the s parameter, so that we can

1. constrain the inputs to s + k <= 100, and
2. refine the value of the output to be exactly usize[s + k].

EXERCISE Why does flux reject the second call to add_points?

Example: factorial

As a last example, you might write a function to compute the factorial of n

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

Here the specification says the input must be non-negative, and the output is at least as large as the input. Note, that unlike the previous examples, here we're actually changing the values of i and res.

Summary

In this post, we saw how Flux lets you

1. decorate basic Rust types like i32 and bool with indices and constraints that let you respectively refine the sets of values that inhabit that type, and

2. specify contracts on functions that state pre-conditions on the sets of legal inputs that they accept, and post-conditions that describe the outputs that they produce.

The whole point of Rust, of course, is to allow for efficient imperative sharing and updates, without sacrificing thread- or memory-safety. Next time, we'll see how Flux melds refinements and Rust's ownership to make refinements happily coexist with imperative code.

1. These are not arbitrary Rust expressions but a subset of expressions from logics that can be efficiently decided by SMT Solvers ↩