Opaque Types: Refined Vectors
While rustc has a keen eye for spotting nasty bugs at
compile time, it is not omniscient. We've all groaned in
dismay at seeing deployed code crash with messages like
panicked at 'index out of bounds: the len is ... but the index is ...'
Next, lets see how flux's refinement and ownership mechanisms let us write a refined vector API whose types track vector sizes and ensure --- at compile time --- that vector accesses cannot fail at runtime.
Refining Vectors ...
To track sizes, lets define a struct that
is just a wrapper around the std::vec::Vec
type, but with a refinement index that tracks
the size of the vector.
#[opaque] #[refined_by(len: int)] pub struct RVec<T> { inner: Vec<T>, }
... to Track their Size
As with other structs we're using refined_by
to index the RVec with an int value (that will represent
the vector's length.)
The idea is that
RVec<i32>[10]represents a vector ofi32size 10, andRVec<bool>{v:0 < v}represents a non-empty vector ofbool, andRVec<RVec<f32>[n]>[m]represents a vector of vectors off32of sizemand each of whose elements is a vector of sizen.
... but Opaquely
The opaque attribute tells flux that we're not
going to directly connect the len to any of
the RVec's fields' values.
This is quite unlike Positivei32 example
where the index held the actual value of the field,
or the [Timer example)(./04-enums.md) where the
index held the value of the countdown.
Instead, with an opaque struct the idea is that the value
of the index will be tracked solely by the API for that struct.
Next, lets see how to build such an API for creating and
manipulating RVec, where the length is precisely tracked
in the index.
Creating Vectors
I suppose one must start with nothing: the empty vector.
#[trusted] impl<T> RVec<T> { #[spec(fn() -> RVec<T>[0])] pub fn new() -> Self { Self { inner: Vec::new() } } }
The above implements RVec::new as a wrapper around Vec::new.
The #[trusted] attribute tells flux to not check this code,
i.e. to simply trust that the specification is correct.
Indeed, flux cannot check this code.
If you remove the #trusted (do it!) then flux will
complain that you cannot access the inner field
of the opaque struct!
So the only way to use an RVec is to define a "trusted" API,
and then use that in client code, where for example, callers
of RVec::new get back an RVec indexed with 0 : the empty vector.
Pushing Values
An empty vector is a rather desolate thing.
To be of any use, we need to be able to push
values into it, like so
#[trusted] impl<T> RVec<T> { #[spec(fn(self: &mut RVec<T>[@n], T) ensures self: RVec<T>[n+1])] pub fn push(&mut self, item: T) { self.inner.push(item); } }
The refined type for push says that it takes a updatable reference to an RVec<T> of size n and, a value T
and ensures that upon return, the size of self is increased by 1.
Creating a Vector with push
Lets test that the types are in fact tracking sizes.
#[spec(fn () -> RVec<i32>[3])] fn test_push() -> RVec<i32> { let mut v = RVec::new(); // v: RVec<i32>[0] v.push(1); // v: RVec<i32>[1] v.push(2); // v: RVec<i32>[2] v.push(3); // v: RVec<i32>[3] v }
EXERCISE: Can you correctly implement the code
for zeros so that it typechecks?
#[spec(fn(n: usize) -> RVec<i32>[n])] fn zeros(n:usize) -> RVec<i32> { let mut v = RVec::new(); // v: RVec<i32>[0] let mut i = 0; while i <= n { v.push(0); // v: RVec<i32>[i] i += 1; } v }
Popping Values
Not much point stuffing things into a vector if we can't get them out again.
For that, we might implement a pop method that returns the last element
of the vector.
Aha, but what if the vector is empty? You could return an
Option<T> or since we're tracking sizes, we could
require that pop only be called with non-empty vectors.
#[trusted] impl<T> RVec<T> { #[spec(fn(self: &mut {RVec<T>[@n] | 0 < n}) -> T ensures self: RVec<T>[n-1])] pub fn pop(&mut self) -> T { self.inner.pop().unwrap() } }
Note that unlike push which works for any RVec<T>[@n], the pop
method requires that 0 < n i.e. that the vector is not empty.
Using the push/pop API
Now already flux can start checking some code, for example if you push two
elements, then you can pop twice, but flux will reject the third pop at
compile-time
fn test_push_pop() { let mut vec = RVec::new(); // vec: RVec<i32>[0] vec.push(10); // vec: RVec<i32>[1] vec.push(20); // vec: RVec<i32>[2] vec.pop(); // vec: RVec<i32>[1] vec.pop(); // vec: RVec<i32>[0] vec.pop(); // rejected! }
In fact, the error message from flux will point to exact condition that
does not hold
#![allow(unused)] fn main() { error[FLUX]: precondition might not hold | 24 | v.pop(); | ^^^^^^^ call site | = note: a precondition cannot be proved at this call site note: this is the condition that cannot be proved | 78 | #[spec(fn(self: &mut{RVec<T>[@n] | 0 < n}) -> T | ^^^^^ }
Querying the Size
Perhaps we should peek at the size of the vector
to make sure its not empty before we pop it.
We can do that by writing a len method that returns
a usize corresponding to (and hence, by indexed by)
the size of the input vector
#[flux_rs::trusted] impl<T> RVec<T> { #[spec(fn(&RVec<T>[@vec]) -> usize)] pub fn len(&self) -> usize { self.inner.len() } }
EXERCISE Can you fix the spec for len so that the code below
verifies, i.e. so that flux "knows" that
- after two
pushes, the value returned by.len()is exactly2, and - after two
pops the size is0again.
fn test_len() { let mut vec = RVec::new(); vec.push(10); vec.push(20); assert(vec.len() == 2); vec.pop(); vec.pop(); assert(vec.len() == 0); }
Random Access
Of course, vectors are not just stacks, they also allow random access to their elements which is where those pesky panics occur, and where the refined vector API gets rather useful.
Now that we're tracking sizes, we can require
that the method to get an element only be called
with a valid index less than the vector's size
impl<T> RVec<T> { #[spec(fn(&RVec<T>[@n], i: usize{i < n}) -> &T)] pub fn get(&self, i: usize) -> &T { &self.inner[i] } #[spec(fn(&mut RVec<T>[@n], i: usize{i < n}) -> &mut T)] pub fn get_mut(&mut self, i: usize) -> &mut T { &mut self.inner[i] } }
Summing the Elements of an RVec
EXERCISE Can you spot and fix the off-by-one error
in the code below which loops over the elements
of an RVec and sums them up? 1
fn sum_vec(vec: &RVec<i32>) -> i32 { let mut res = 0; let mut i = 0; while i <= vec.len() { res += vec.get(i); i += 1; } sum }
Using the Index trait
Its a bit of an eyesore to to use get and get_mut directly.
Instead lets implement the Index and IndexMut
traits for RVec which allows us to use the [..]
operator to access elements
impl<T> std::ops::Index<usize> for RVec<T> { type Output = T; #[spec(fn(&RVec<T>[@n], i:usize{i < n}) -> &T)] fn index(&self, index: usize) -> &T { self.get(index) } } impl<T> std::ops::IndexMut<usize> for RVec<T> { #[spec(fn(&mut RVec<T>[@n], i:usize{i < n}) -> &mut T)] fn index_mut(&mut self, index: usize) -> &mut T { self.get_mut(index) } }
Summing Nicely
Now the above vec_sum example looks a little nicer
fn sum_vec_fixed(vec: &RVec<i32>) -> i32 { let mut res = 0; let mut i = 0; while i < vec.len() { res += vec[i] i += 1; } sum }
Memoization
Lets put the whole API to work in this "memoized" version of the fibonacci function which uses a vector to store the results of previous calls
pub fn fib(n: usize) -> i32 { let mut r = RVec::new(); let mut i = 0; while i < n { if i == 0 { r.push(0); } else if i == 1 { r.push(1); } else { let a = r[i - 1]; let b = r[i - 2]; r.push(a + b); } i += 1; } r.pop() }
EXERCISE Flux is unhappy with the pop at the end of the function
which returns the last value as the result: it thinks the vector
may be empty and so the pop call may fail ... Can you spot and fix
the problem?
#![allow(unused)] fn main() { error[FLUX]: precondition might not hold --> src/vectors.rs:40:5 | 40 | r.pop() | ^^^^^^^ }
Binary Search
As a last example, lets look at a simplified version of the
binary_search method from std::vec, into which
we've snuck a tiny little bug
pub fn binary_search(vec: &RVec<i32>, x: i32) -> Result<usize, usize> { let mut size = vec.len(); let mut left = 0; let mut right = size; while left <= right { let mid = left + size / 2; let val = vec[mid]; if val < x { left = mid + 1; } else if x < val { right = mid; } else { return Ok(mid); } size = right - left; } Err(left) }
Flux complains in two places
#![allow(unused)] fn main() { error[FLUX]: precondition might not hold --> src/vectors.rs:152:19 | 152 | let val = vec[mid]; | ^^^^^^^^ call site | = note: a precondition cannot be proved at this call site note: this is the condition that cannot be proved --> src/rvec.rs:189:44 | 189 | #[spec(fn(&RVec<T>[@n], usize{v : v < n}) -> &T)] | ^^^^^ error[FLUX]: arithmetic operation may overflow --> src/vectors.rs:160:9 | 160 | size = right - left; | ^^^^^^^^^^^^^^^^^^^ }
-
The vector access may be unsafe as
midcould be out of bounds! -
The
sizevariable may underflow asleftmay exceedright!
EXERCISE Can you the spot off-by-one and figure out a fix?
Summary
Well then. We just saw how Flux's index and constraint mechanisms combine with Rust's ownership to let us write a refined vector API that ensures the safety of all accesses at compile time.
These mechanisms are compositional : we can use standard
type machinery to build up compound structures and APIs from
simple ones, as we will see when we use RVec to implment
sparse matrices and a small
neural network library.
-
Why not use an iterator? We'll get there in due course! ↩