User's Guide

A list of various flux features as illustrated by examples in the regression tests.

Index Refinements

Of the form i32[e] (i32 equal to e) values.

#![allow(unused)]
fn main() {
#[flux::sig(fn(bool[true]))]
pub fn assert(_b: bool) {}

pub fn test00() {
    let x = 1;
    let y = 2;
    assert(x + 1 == y);
}

#[flux::sig(fn() -> usize[5])]
pub fn five() -> usize {
    let x = 2;
    let y = 3;
    x + y
}

#[flux::sig(fn(n:usize) -> usize[n+1])]
pub fn incr(n: usize) -> usize {
    n + 1
}

pub fn test01() {
    let a = five();
    let b = incr(a);
    assert(b == 6);
}
}

Existential Refinements

Of the form i32{v: 0 <= v} (non-negative i32) values.

#![allow(unused)]
fn main() {
#[flux::sig(fn(x:i32) -> i32{v: v > x})]
pub fn inc(x: i32) -> i32 {
    x + 1
}

#[flux::sig(fn(x:i32) -> i32{v: v < x})]
pub fn dec(x: i32) -> i32 {
    x - 1
}
}

Combining Index and Existential Refinements

#![allow(unused)]
fn main() {
#[flux::sig(fn(k: i32{0 <= k}) -> i32[0])]
pub fn test(mut k: i32) -> i32 {
    while toss() && k < i32::MAX - 1 {
        k += 1;
    }
    while k > 0 {
        k -= 1;
    }
    k
}
}

Mutable References

#![allow(unused)]
fn main() {
#[flux::sig(fn(x: &mut i32{v: 0 <= v}))]
pub fn test4(x: &mut i32) {
    *x += 1;
}
}

#![allow(unused)]
fn main() {
#[flux::sig(fn(x: &mut i32{v: 0 <= v}))]
pub fn test4(x: &mut i32) {
    *x -= 1; //~ ERROR assignment might be unsafe
}
}

Strong References

Like &mut T but which allow strong updates via ensures clauses

#![allow(unused)]
fn main() {
#[flux::sig(fn(x: &strg i32[@n]) ensures x: i32[n+1])]
pub fn inc(x: &mut i32) {
    *x += 1;
}

#[flux::sig(fn() -> i32[1])]
pub fn test_inc() -> i32 {
    let mut x = 0;
    inc(&mut x);
    x
}
}

Refined Vectors rvec

RVec specification

#![allow(unused)]
#![allow(dead_code)]

fn main() {
pub mod rslice;

#[macro_export]
macro_rules! rvec {
    () => { RVec::new() };
    ($($e:expr),+$(,)?) => {{
        let mut res = RVec::new();
        $( res.push($e); )*
        res
    }};
    ($elem:expr; $n:expr) => {{
        RVec::from_elem_n($elem, $n)
    }}
}

#[flux::opaque]
#[flux::refined_by(len: int)]
#[flux::invariant(0 <= len)]
pub struct RVec<T> {
    inner: Vec<T>,
}

impl<T> RVec<T> {
    #[flux::trusted]
    #[flux::sig(fn() -> RVec<T>[0])]
    pub fn new() -> Self {
        Self { inner: Vec::new() }
    }

    #[flux::trusted]
    #[flux::sig(fn(self: &strg RVec<T>[@n], T) ensures self: RVec<T>[n+1])]
    pub fn push(&mut self, item: T) {
        self.inner.push(item);
    }

    #[flux::trusted]
    #[flux::sig(fn(&RVec<T>[@n]) -> usize[n])]
    pub fn len(&self) -> usize {
        self.inner.len()
    }

    #[flux::trusted]
    #[flux::sig(fn(&RVec<T>[@n]) -> bool[n == 0])]
    pub fn is_empty(&self) -> bool {
        self.inner.is_empty()
    }

    #[flux::trusted]
    #[flux::sig(fn(&RVec<T>[@n], i: usize{i < n}) -> &T)]
    pub fn get(&self, i: usize) -> &T {
        &self.inner[i]
    }

    #[flux::trusted]
    #[flux::sig(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]
    }

    #[flux::trusted]
    #[flux::sig(fn(self: &strg RVec<T>[@n]) -> T
    		requires n > 0
            ensures self: RVec<T>[n-1])]
    pub fn pop(&mut self) -> T {
        self.inner.pop().unwrap()
    }

    #[flux::trusted]
    #[flux::sig(fn(&mut RVec<T>[@n], a: usize{a < n}, b: usize{b < n}))]
    pub fn swap(&mut self, a: usize, b: usize) {
        self.inner.swap(a, b);
    }

    #[flux::trusted]
    #[flux::sig(fn(&mut RVec<T>[@n]) -> &mut [T][n])]
    pub fn as_mut_slice(&mut self) -> &mut [T] {
        self.inner.as_mut_slice()
    }

    #[flux::trusted]
    #[flux::sig(fn(arr:_) -> RVec<T>[N])]
    pub fn from_array<const N: usize>(arr: [T; N]) -> Self {
        Self { inner: Vec::from(arr) }
    }

    #[flux::trusted]
    #[flux::sig(fn(xs:&[T][@n]) -> RVec<T>[n])]
    pub fn from_slice(xs: &[T]) -> Self
    where
        T: Clone,
    {
        Self { inner: Vec::from(xs) }
    }

    #[flux::trusted]
    #[flux::sig(fn(T, n: usize) -> RVec<T>[n])]
    pub fn from_elem_n(elem: T, n: usize) -> Self
    where
        T: Copy,
    {
        let mut vec = Self::new();
        let mut i = 0;
        while i < n {
            vec.push(elem);
            i += 1;
        }
        vec
    }

    #[flux::trusted]
    #[flux::sig(fn(&RVec<T>[@n]) -> RVec<T>[n])]
    pub fn clone(&self) -> Self
    where
        T: Clone,
    {
        Self { inner: self.inner.clone() }
    }

    #[flux::trusted]
    #[flux::sig(fn(self: &strg RVec<T>[@n], other: &[T][@m]) ensures self: RVec<T>[n + m])]
    pub fn extend_from_slice(&mut self, other: &[T])
    where
        T: Clone,
    {
        self.inner.extend_from_slice(other)
    }

    #[flux::trusted]
    #[flux::sig(fn (&RVec<T>[@n], F) -> RVec<U>[n])]
    pub fn map<U, F>(&self, f: F) -> RVec<U>
    where
        F: Fn(&T) -> U,
    {
        RVec { inner: self.inner.iter().map(f).collect() }
    }

    #[flux::trusted]
    pub fn fold<B, F>(&self, init: B, f: F) -> B
    where
        F: FnMut(B, &T) -> B,
    {
        self.inner.iter().fold(init, f)
    }
}

#[flux::opaque]
pub struct RVecIter<T> {
    vec: RVec<T>,
    curr: usize,
}

impl<T> IntoIterator for RVec<T> {
    type Item = T;
    type IntoIter = RVecIter<T>;

    // TODO: cannot get variant of opaque struct
    #[flux::trusted]
    #[flux::sig(fn(RVec<T>) -> RVecIter<T>)]
    fn into_iter(self) -> RVecIter<T> {
        RVecIter { vec: self, curr: 0 }
    }
}

impl<T> Iterator for RVecIter<T> {
    type Item = T;

    // TODO: cannot get variant of opaque struct
    #[flux::trusted]
    #[flux::sig(fn(&mut RVecIter<T>) -> Option<T>)]
    fn next(&mut self) -> Option<T> {
        self.vec.inner.pop()
    }
}

impl<T> std::ops::Index<usize> for RVec<T> {
    type Output = T;

    #[flux::trusted_impl]
    #[flux::sig(fn(&RVec<T>[@n], usize{v : v < n}) -> &T)]
    fn index(&self, index: usize) -> &T {
        self.get(index)
    }
}

impl<T> std::ops::IndexMut<usize> for RVec<T> {
    #[flux::trusted_impl]
    #[flux::sig(fn(&mut RVec<T>[@n], usize{v : v < n}) -> &mut T)]
    fn index_mut(&mut self, index: usize) -> &mut T {
        self.get_mut(index)
    }
}
}

RVec clients

#![allow(unused)]
fn main() {
#[path = "../../lib/rvec.rs"]
mod rvec;
use rvec::RVec;

#[flux::sig(fn() -> RVec<i32>[0])]
pub fn test0() -> RVec<i32> {
    let mv = rvec![];
    mv
}

#[flux::sig(fn() -> RVec<i32>[5])]
pub fn test1() -> RVec<i32> {
    rvec![ 12; 5 ]
}

#[flux::sig(fn(n:usize) -> RVec<i32>[n])]
pub fn test2(n: usize) -> RVec<i32> {
    rvec![ 12; n ]
}

pub fn test3() -> usize {
    let v = rvec![0, 1];
    let r = v[0];
    let r = r + v[1];
    r
}
}

Binary Search

#![allow(unused)]
#![allow(unused_attributes)]

fn main() {
#[path = "../../lib/rvec.rs"]
pub mod rvec;
use rvec::RVec;

// CREDIT: https://shane-o.dev/blog/binary-search-rust

#[flux::sig(fn(i32, &RVec<i32>) -> usize)]
pub fn binary_search(k: i32, items: &RVec<i32>) -> usize {
    let size = items.len();
    if size <= 0 {
        return size;
    }

    let mut low: usize = 0;
    let mut high: usize = size - 1;

    while low <= high {
        // SAFE   let middle = (high + low) / 2;
        // UNSAFE let middle = high + ((high - low) / 2);
        let middle = low + ((high - low) / 2);
        let current = items[middle];
        if current == k {
            return middle;
        }
        if current > k {
            if middle == 0 {
                return size;
            }
            high = middle - 1
        }
        if current < k {
            low = middle + 1
        }
    }
    size
}
}

Heapsort

#![allow(unused)]
fn main() {
#[path = "../../lib/rvec.rs"]
mod rvec;
use rvec::RVec;

#[flux::sig(fn(&mut RVec<i32>[@n]) -> i32)]
pub fn heap_sort(vec: &mut RVec<i32>) -> i32 {
    let len = vec.len();

    if len <= 0 {
        return 0;
    }

    let mut start = len / 2;
    while start > 0 {
        start -= 1;
        shift_down(vec, start, len - 1);
    }

    let mut end = len;
    while end > 1 {
        end -= 1;
        vec.swap(0, end);
        shift_down(vec, 0, end - 1);
    }
    0
}

#[flux::sig(fn(&mut RVec<i32>[@len], usize{v : v < len}, usize{v : v < len}) -> i32)]
pub fn shift_down(vec: &mut RVec<i32>, start: usize, end: usize) -> i32 {
    let mut root = start;
    loop {
        let mut child = root * 2 + 1;
        if child > end {
            break;
        } else {
            if child + 1 <= end {
                let a = vec[child];
                let b = vec[child + 1];
                if a < b {
                    child += 1;
                }
            }
            let a = vec[root];
            let b = vec[child];
            if a < b {
                vec.swap(root, child);
                root = child;
            } else {
                break;
            }
        }
    }
    0
}
}

Requires Clauses

#![allow(unused)]
fn main() {
#[path = "../../lib/rvec.rs"]
mod rvec;
use rvec::RVec;

#[flux::sig(
    fn(&mut RVec<i32>[@n], b:bool) -> i32[0]
    requires 2 <= n
)]
pub fn test1(vec: &mut RVec<i32>, b: bool) -> i32 {
    let r;
    if b {
        r = &mut vec[0];
    } else {
        r = &mut vec[1];
    }
    *r = 12;
    0
}
}