User's Guide

One day, this will be an actual user's guide.

For now, it is a collection of various flux features as illustrated by examples from 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 five() -> 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);
}
}

NOTE: We use the sig(..) annotation to specify the refinement type of a function; you can optionally also add the name of the function as shown for fn five.

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
}
}

Mixing Mutable and Strong References

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

#[flux::sig(fn (x: &mut i32{v: 0<=v}))]
pub fn client_safe(z: &mut i32) {
    incr(z);
}
}

Refined Arrays

flux supports refined arrays of the form [i32{v: 0 <= v}; 20] denoting arrays of size 20 of non-negative i32 values.

#![allow(unused)]
fn main() {
#[flux::sig(fn() -> [i32{v : v >= 0}; 2])]
pub fn array00() -> [i32; 2] {
    [0, 1]
}

pub fn read_u16() -> u16 {
    let bytes: [u8; 2] = [10, 20];
    u16::from_le_bytes(bytes)
}

#[flux::sig(fn() -> i32{v : v > 10})]
pub fn write() -> i32 {
    let bytes: [i32; 2] = [10, 20];
    bytes[0] + bytes[1]
}
}

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
}
}

Refined Slices

#![allow(unused)]
fn main() {
#[flux::sig(fn(&[i32{v : v > 0}]) -> &[i32{v : v >= 0}])]
fn first_half(slice: &[i32]) -> &[i32] {
    let mid = slice.len() / 2;
    let (fst, snd) = slice.split_at(mid);
    fst
}

#[flux::sig(fn(&[i32{v : v > 0}]) -> Option<&i32{v : v >= 0}>)]
fn first(slice: &[i32]) -> Option<&i32> {
    slice.first()
}

#[flux::sig(fn(&mut [i32{v : v > 0}]))]
fn inc_fst(slice: &mut [i32]) {
    if let Some(x) = slice.first_mut() {
        *x += 1;
    }
}
}

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

#[flux::sig(fn(&mut RVec<T>[10]))]
fn test00<T>(vec: &mut RVec<T>) {
    let mut s = RSlice::from_vec(vec);
    let s1 = s.subslice(0, 3);
    let s2 = s.subslice(4, 5);
}

#[flux::sig(fn(&mut {RVec<i32>[@n] | n % 2 == 0 && n > 0}))]
fn test01(vec: &mut RVec<i32>) {
    let n = vec.len();
    let mut s = RSlice::from_vec(vec);
    let mut s1 = s.subslice(0, n / 2 - 1);
    let s2 = s.subslice(n / 2, n - 1);
    add(s1.as_mut_slice(), s2.as_slice())
}

#[flux::sig(fn(&mut [i32][@n], &[i32][n]))]
fn add(x: &mut [i32], y: &[i32]) {
    let mut i = 0;
    while i < len(x) {
        x[i] += y[i];
    }
}

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

Refined Vec

This uses extern_spec which is described in the specifications guide.

Standalone

#![allow(unused)]
#![feature(allocator_api)]

fn main() {
use std::alloc::{Allocator, Global};

use flux_rs::extern_spec;

#[extern_spec]
#[refined_by(len: int)]
struct Vec<T, A: Allocator = Global>;

#[extern_spec]
impl<T> Vec<T> {
    #[sig(fn() -> Vec<T>[0])]
    fn new() -> Vec<T>;
}

#[extern_spec]
impl<T, A: Allocator> Vec<T, A> {
    #[sig(fn(self: &strg Vec<T, A>[@n], T) ensures self: Vec<T, A>[n+1])]
    fn push(&mut self, value: T);

    #[sig(fn(&Vec<T, A>[@n]) -> usize[n])]
    fn len(&self) -> usize;

    #[sig(fn(&Vec<T, A>[@n]) -> bool[n == 0])]
    fn is_empty(&self) -> bool;
}

#[extern_spec]
impl<T> [T] {
    #[sig(fn(self: Box<[T][@n], A>) -> Vec<T, A>[n])]
    fn into_vec<A>(self: Box<[T], A>) -> Vec<T, A>
    where
        A: Allocator;
}

#[flux::sig(fn(bool[true]))]
fn assert(_: bool) {}

#[flux::sig(fn() -> Vec<i32>[3])]
pub fn test_vec_macro() -> Vec<i32> {
    vec![10, 20, 30]
}

#[flux::sig(fn() -> Vec<i32>[3])]
pub fn test_push() -> Vec<i32> {
    let mut res = Vec::new();
    res.push(10);
    res.push(20);
    res.push(30);
    res
}

#[flux::sig(fn() -> usize[3])]
pub fn test_len() -> usize {
    let res = test_push();
    res.len()
}

pub fn test_is_empty() {
    let res = test_push();
    assert(!res.is_empty())
}

// TODO: https://github.com/flux-rs/flux/issues/578
// #[flux::sig(fn (Vec<i32{v:10 <= v}>))]
// pub fn test3(xs: Vec<i32>) {
//     for x in &xs {
//         assert(0 <= *x)
//     }
// }
}

Associated Refinements for indexing

#![allow(unused)]
fn main() {
use std::{
    alloc::{Allocator, Global},
    ops::{Index, IndexMut},
    slice::{Iter, SliceIndex},
};

use flux_rs::extern_spec;

#[extern_spec]
#[flux::refined_by(len: int)]
struct Vec<T, A: Allocator = Global>;

#[extern_spec]
#[flux::assoc(fn in_bounds(idx: Self, v: T) -> bool)]
trait SliceIndex<T>
where
    T: ?Sized,
{
}

#[extern_spec]
#[flux::assoc(fn in_bounds(idx: int, len: int) -> bool {idx < len} )]
impl<T> SliceIndex<[T]> for usize {}

#[extern_spec]
#[flux::generics(I as base)]
impl<T, I: SliceIndex<[T]>, A: Allocator> Index<I> for Vec<T, A> {
    #[flux::sig(fn(&Vec<T, A>[@len], {I[@idx] | <I as SliceIndex<[T]>>::in_bounds(idx, len)}) -> _)]
    fn index(z: &Vec<T, A>, index: I) -> &<I as SliceIndex<[T]>>::Output;
}

#[extern_spec]
#[flux::generics(I as base)]
impl<T, I: SliceIndex<[T]>, A: Allocator> IndexMut<I> for Vec<T, A> {
    #[flux::sig(fn(&mut Vec<T,A>[@len], {I[@idx] | <I as SliceIndex<[T]>>::in_bounds(idx, len)}) -> _)]
    fn index_mut(z: &mut Vec<T, A>, index: I) -> &mut <I as SliceIndex<[T]>>::Output;
}

//---------------------------------------------------------------------------------------

#[extern_spec]
impl<T> Vec<T> {
    #[flux::sig(fn() -> Vec<T>[0])]
    fn new() -> Vec<T>;
}

#[extern_spec]
impl<T, A: Allocator> Vec<T, A> {
    #[flux::sig(fn(self: &strg Vec<T, A>[@n], T) ensures self: Vec<T, A>[n+1])]
    fn push(v: &mut Vec<T, A>, value: T);

    #[flux::sig(fn(&Vec<T, A>[@n]) -> usize[n])]
    fn len(v: &Vec<T, A>) -> usize;
}

#[extern_spec]
impl<'a, T, A: Allocator> IntoIterator for &'a Vec<T, A> {
    #[flux::sig(fn (&Vec<T, A>[@n]) -> <&Vec<T, A> as IntoIterator>::IntoIter[0,n])]
    fn into_iter(v: &'a Vec<T, A>) -> <&'a Vec<T, A> as IntoIterator>::IntoIter;
}
}

#![allow(unused)]
#![feature(allocator_api)]

fn main() {
use std::ops::Index;

#[path = "../../lib/option.rs"]
mod option;

#[path = "../../lib/slice.rs"]
mod slice;

#[path = "../../lib/vec.rs"]
mod vec;

#[path = "../../lib/iter.rs"]
mod iter;

// ---------------------------------------------------------------------------------------

pub fn test_get0(xs: &Vec<i32>) -> &i32 {
    <Vec<i32> as Index<usize>>::index(xs, 10) //~ ERROR refinement type
}

pub fn test_get1(xs: &Vec<i32>) -> i32 {
    xs[10] //~ ERROR refinement type
}

#[flux::sig(fn (&Vec<i32>[100]) -> &i32)]
pub fn test_get2(xs: &Vec<i32>) -> &i32 {
    <Vec<i32> as Index<usize>>::index(xs, 99)
}

#[flux::sig(fn (&Vec<i32>[100]) -> i32)]
pub fn test_get3(xs: &Vec<i32>) -> i32 {
    xs[99]
}

pub fn test_set0(xs: &mut Vec<i32>) {
    xs[10] = 100; //~ ERROR refinement type
}

#[flux::sig(fn (&mut Vec<i32>[100]))]
pub fn test_set1(xs: &mut Vec<i32>) {
    xs[99] = 100;
}

pub fn test1() {
    let mut xs = Vec::<i32>::new();
    xs.push(10);
    xs.push(20);
    xs.push(30);

    xs[0] = 100;
    xs[1] = 100;
    xs[2] = 100;
    xs[10] = 100; //~ ERROR refinement type
}

pub fn test2(xs: Vec<i32>, i: usize) {
    if i < xs.len() {
        let _ = xs[i];
        let _ = xs[i + 1]; //~ ERROR refinement type
    }
}
}

Named Function Signatures

You can also write named function signatures using the spec annotation (instead of the anonymous sig annotation).

Requires Clauses

Used to specify preconditions in a single spot, if needed.

#![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
}
}

Refining Structs

#![allow(unused)]
#![flux::defs {
fn main() {
    qualifier Sub2(x: int, a: int, b:int) { x == a - b }
}]
#[path = "../../lib/rvec.rs"]
pub mod rvec;

use rvec::RVec;

#[flux::refined_by(x: int, y:int)]
pub struct Pair {
    #[flux::field(i32[x])]
    pub x: i32,
    #[flux::field(i32[y])]
    pub y: i32,
}

#[flux::sig(fn(a: i32) -> RVec<Pair{v : v.x + v.y <= a }>)]
pub fn mk_pairs_with_bound(a: i32) -> RVec<Pair> {
    let mut i = 0;
    let mut res = RVec::new();
    while i < a {
        let p = Pair { x: i, y: a - i };
        res.push(p);
        i += 1;
    }
    res
}
}

#![allow(unused)]
#![flux::defs {
fn main() {
    fn is_btwn(v:int, lo:int, hi: int) -> bool { lo <= v && v <= hi }
    fn ok_day(d:int) -> bool { is_btwn(d, 1, 31) }
    fn is_month30(m:int) -> bool { m == 4 || m == 6 || m == 9 || m == 11 }
    fn ok_month(d:int, m:int) -> bool { is_btwn(m, 1, 12) && (is_month30(m) => d <= 30) }
    fn is_leap_year(y:int) -> bool { y % 400 == 0 || (y % 4 == 0 && (y % 100) > 0) }
    fn is_feb_day(d:int, y:int) -> bool { d <= 29 && ( d == 29 => is_leap_year(y) ) }
    fn ok_year(d:int, m:int, y:int) -> bool { 1 <= y && (m == 2 => is_feb_day(d, y)) }
}]

// https://github.com/chrisdone/sandbox/blob/master/liquid-haskell-dates.hs

#[allow(dead_code)]
#[flux::refined_by(d:int, m:int, y:int)]
pub struct Date {
    #[flux::field({ usize[d] | ok_day(d) })]
    day: usize,
    #[flux::field({ usize[m] | ok_month(d, m)})]
    month: usize,
    #[flux::field({ usize[y] | ok_year(d, m, y)})]
    year: usize,
}

pub fn test() {
    let _ok_date = Date { day: 9, month: 8, year: 1977 };
}

// TODO: Tedious to duplicate the definitions if you want to use them in rust code.
// Maybe some macro magic can unify?

#[flux::sig(fn(m:usize) -> bool[is_month30(m)])]
fn is_month30(m: usize) -> bool {
    m == 4 || m == 6 || m == 9 || m == 11
}

#[flux::sig(fn(y:usize) -> bool[is_leap_year(y)])]
fn is_leap_year(y: usize) -> bool {
    y % 400 == 0 || (y % 4 == 0 && y % 100 != 0)
}

#[flux::sig(fn(d:usize, y:usize) -> bool[is_feb_day(d, y)])]
fn is_feb_day(d: usize, y: usize) -> bool {
    d <= 29 && (d != 29 || is_leap_year(y))
}

pub fn mk_date(day: usize, month: usize, year: usize) -> Option<Date> {
    if 1 <= year && 1 <= month && month <= 12 && 1 <= day && day <= 31 {
        if !is_month30(month) || day <= 30 {
            if month != 2 || is_feb_day(day, year) {
                return Some(Date { day, month, year });
            }
        }
    }
    return None;
}
}

Invariants on Structs

#![allow(unused)]
fn main() {
#[flux::refined_by(a: int, b: int)]
#[flux::invariant(a > 0)]
#[flux::invariant(b > 0)]
pub struct S {
    #[flux::field({i32[a] | a > 0})]
    fst: i32,
    #[flux::field({i32[b] | b >= a})]
    snd: i32,
}
}

with const generics

#![allow(unused)]
fn main() {
// Test that const generics in invariants are properly instantiated

use flux_rs::attrs::*;

#[invariant(N > 0)]
struct S<const N: usize> {}

#[sig(fn(_) -> usize{v : v > 0})]
fn foo<const M: usize>(x: S<M>) -> usize {
    M
}
}

Opaque Structs

See the specifications guide for more about the opaque annotation.

#![allow(unused)]
fn main() {
#[flux::opaque]
#[flux::refined_by(a: int, b: int)]
#[flux::invariant(a <= b)]
pub struct Range {
    a: i32,
    b: i32,
}

impl Range {
    #[flux::trusted]
    #[flux::sig(fn(a: i32, b: i32{b >= a}) -> Range[a, b])]
    pub fn new(a: i32, b: i32) -> Range {
        Range { a, b }
    }

    #[flux::trusted]
    #[flux::sig(fn(&Range[@r]) -> i32[r.a])]
    pub fn fst(&self) -> i32 {
        self.a
    }

    #[flux::trusted]
    #[flux::sig(fn(&Range[@r]) -> i32[r.b])]
    pub fn snd(&self) -> i32 {
        self.b
    }
}

#[flux::sig(fn(Range) -> bool[true])]
fn test(r: Range) -> bool {
    r.snd() - r.fst() >= 0
}
}

Refining Enums

#![allow(unused)]
fn main() {
#[flux::refined_by(b:bool)]
pub enum Opt<T> {
    #[flux::variant(Opt<T>[false])]
    None,
    #[flux::variant({T} -> Opt<T>[true])]
    Some(T),
}

#[flux::sig(fn(Opt<T>[@b]) -> bool[b])]
pub fn is_some<T>(x: Opt<T>) -> bool {
    match x {
        Opt::None => false,
        Opt::Some(_) => true,
    }
}

#[flux::sig(fn(Opt<T>[@b]) -> bool[b])]
pub fn is_some_flip<T>(x: Opt<T>) -> bool {
    match x {
        Opt::Some(_) => true,
        Opt::None => false,
    }
}

#[flux::sig(fn(i32{v:false}) -> T)]
pub fn never<T>(_x: i32) -> T {
    loop {}
}

#[flux::sig(fn(Opt<T>[true]) -> T)]
pub fn unwrap<T>(x: Opt<T>) -> T {
    match x {
        Opt::Some(v) => v,
        Opt::None => never(0),
    }
}
}

#![allow(unused)]
fn main() {
#[flux::refined_by(n: int)]
#[flux::invariant(n > 0)]
pub enum Pos {
    #[flux::variant({Box<Pos[@n]>} -> Pos[2*n])]
    XO(Box<Pos>),
    #[flux::variant({Box<Pos[@n]>} -> Pos[2*n + 1])]
    XI(Box<Pos>),
    #[flux::variant(Pos[1])]
    XH,
}

impl Pos {
    #[flux::spec(fn(&Pos[@n]) -> i32[n])]
    pub fn to_i32(&self) -> i32 {
        match self {
            Pos::XH => 1,
            Pos::XI(rest) => 2 * rest.to_i32() + 1,
            Pos::XO(rest) => 2 * rest.to_i32(),
        }
    }

    #[flux::sig(fn(&Pos[@n]) -> bool[n == 1])]
    pub fn is_one(&self) -> bool {
        match self {
            Pos::XH => true,
            Pos::XI(_) => false,
            Pos::XO(_) => false,
        }
    }
}
}

#![allow(unused)]
fn main() {
#[flux::sig(fn(i32{v: false}) -> T)]
pub fn never<T>(_: i32) -> T {
    loop {}
}

#[flux::refined_by(n:int)]
#[flux::invariant(n >= 0)]
pub enum List {
    #[flux::variant(List[0])]
    Nil,
    #[flux::variant((i32, Box<List[@n]>) -> List[n+1])]
    Cons(i32, Box<List>),
}

#[flux::sig(fn(&List[@n]) -> bool[n == 0])]
pub fn empty(l: &List) -> bool {
    match l {
        List::Nil => true,
        List::Cons(_, _) => false,
    }
}

#[flux::sig(fn(&List[@n]) -> i32[n])]
pub fn len(l: &List) -> i32 {
    match l {
        List::Nil => 0,
        List::Cons(_, tl) => 1 + len(tl),
    }
}

#[flux::sig(fn({&List[@n] | 0 < n}) -> i32)]
pub fn head(l: &List) -> i32 {
    match l {
        List::Nil => never(0),
        List::Cons(h, _) => *h,
    }
}

#[flux::sig(fn({&List[@n] | 0 < n}) -> &List)]
pub fn tail(l: &List) -> &List {
    match l {
        List::Nil => never(0),
        List::Cons(_, t) => t,
    }
}

#[flux::sig(fn(i32, n: usize) -> List[n])]
pub fn clone(val: i32, n: usize) -> List {
    if n == 0 {
        List::Nil
    } else {
        List::Cons(val, Box::new(clone(val, n - 1)))
    }
}

#[flux::sig(fn(List[@n1], List[@n2]) -> List[n1+n2])]
pub fn append(l1: List, l2: List) -> List {
    match l1 {
        List::Nil => l2,
        List::Cons(h1, t1) => List::Cons(h1, Box::new(append(*t1, l2))),
    }
}

#[flux::sig(fn(l1: &strg List[@n1], List[@n2]) ensures l1: List[n1+n2])]
pub fn mappend(l1: &mut List, l2: List) {
    match l1 {
        List::Nil => *l1 = l2,
        List::Cons(_, t1) => mappend(&mut *t1, l2),
    }
}

#[flux::sig(fn(&List[@n], k:usize{k < n} ) -> i32)]
pub fn get_nth(l: &List, k: usize) -> i32 {
    match l {
        List::Cons(h, tl) => {
            if k == 0 {
                *h
            } else {
                get_nth(tl, k - 1)
            }
        }
        List::Nil => never(0),
    }
}
}

Invariants on Enums

#![allow(unused)]
fn main() {
#[flux::refined_by(n: int)]
#[flux::invariant(n >= 0)]
pub enum E {
    #[flux::variant({{i32[@n] | n > 0}} -> E[n])]
    Pos(i32),
    #[flux::variant({i32[0]} -> E[0])]
    Zero(i32),
}

#[flux::sig(fn(E[@n], i32[n]) -> i32{v: v > 0})]
pub fn is_zero(_: E, x: i32) -> i32 {
    x + 1
}
}

Reflecting Enums

#![allow(unused)]
fn main() {
#[flux::reflect]
pub enum State {
    On,
    Off,
}

#[flux_rs::sig(fn () -> State[State::On])]
pub fn test00() -> State {
    State::On
}

#[flux_rs::sig(fn () -> State[State::Off])]
pub fn test01() -> State {
    State::Off
}

#[flux::sig(fn () -> State[State::Off])]
pub fn test02() -> State {
    State::On //~ ERROR refinement type
}

#[flux::sig(fn (State[State::On]) -> usize[1])]
pub fn test03(s: State) -> usize {
    match s {
        State::On => 1,
        State::Off => 0,
    }
}

#[flux::sig(fn (State[@squig], zig: usize, tag: Day) -> usize[tag])]
pub fn test04(s: State, _zig: usize, tag: Day) -> usize {
    match s {
        State::On => 1,  //~ ERROR refinement type
        State::Off => 0, //~ ERROR refinement type
    }
}

#[flux::refined_by(day: int)]
pub enum Day {
    #[flux::variant(Day[0])]
    Mon,
    #[flux::variant(Day[1])]
    Tue,
    #[flux::variant(Day[2])]
    Wed,
}

#[flux::sig(fn (s:State, zig: usize, tag: Day) -> usize[tag])]
pub fn test05(s: State, _zig: usize, _tag: Day) -> usize {
    match s {
        State::On => 1,  //~ ERROR refinement type
        State::Off => 0, //~ ERROR refinement type
    }
}
}

Field Syntax for Indices

Structs

#![allow(unused)]
fn main() {
#[flux::refined_by(x: int, y: int)]
pub struct X {
    #[flux::field(u32[x])]
    x: u32,
    #[flux::field(u32[y])]
    y: u32,
}

#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 2, x: 1 }])]
fn f(mut x: X) -> X {
    x.x = 1;
    x.y = 2;
    x
}
}

Enums

#![allow(unused)]
fn main() {
#[flux::refined_by(x: int, y: int)]
pub enum E {
    #[flux::variant(E[0, 1])]
    Variant1,
    #[flux::variant(E[1, 2])]
    Variant2,
    #[flux::variant(E[2, 3])]
    Variant3,
}

#[flux::sig(fn (e: E[@old_enum]) -> E[E { x: 1, y: 2 }])]
fn f(e: E) -> E {
    E::Variant2
}
}

Updates

#![allow(unused)]
fn main() {
#[flux::refined_by(x: int, y: int)]
pub struct S {
    #[flux::field(u32[x])]
    x: u32,
    #[flux::field(u32[y])]
    y: u32,
}

impl S {
    #[flux::sig(fn (self: &strg S[@old_x]) ensures self: S[S { x: 1, ..old_x }])]
    pub fn update(&mut self) {
        self.x = 1;
    }
}
}

#![allow(unused)]
#![flux::defs {
fn main() {
    fn some_computation(s: S) -> S { s }
}]

#[flux::refined_by(x: int, y: int)]
pub struct S {
    #[flux::field(u32[x])]
    x: u32,
    #[flux::field(u32[y])]
    y: u32,
}

impl S {
    #[flux::sig(fn (self: &strg S[@old_x]) ensures self: S[S { x: 1, ..some_computation(old_x) }])]
    pub fn update(&mut self) {
        self.x = 1;
    }

    #[flux::sig(fn (self: &strg S[@old_x]) ensures self: S[S { x: 1, ..S { x: 2, ..old_x } }])]
    pub fn update2(&mut self) {
        self.x = 1;
    }
}
}

#![allow(unused)]
fn main() {
use flux_rs::*;

#[refined_by(start: T, end: T)]
pub struct Range<T> {
    #[flux::field(T[start])]
    pub start: T,
    #[flux::field(T[end])]
    pub end: T,
}

#[sig(fn(r: Range<T>[@old]) -> Range<T>[ Range { ..old } ])]
pub fn foo<T>(r: Range<T>) -> Range<T> {
    r
}

#[sig(fn(r: Range<i32>{v: v == Range { start: 0, end: 0 } }))]
pub fn foo2(_r: Range<i32>) {}

#[sig(fn(r: Range<i32>[Range { start: 0, end: 0 } ]))]
pub fn foo3(_r: Range<i32>) {}
}

#![allow(unused)]
#![flux::defs {
fn main() {
    fn some_computation(s: S) -> S { s }
}]

#[flux::refined_by(x: int, y: int)]
pub struct S {
    #[flux::field(u32[x])]
    x: u32,
    #[flux::field(u32[y])]
    y: u32,
}

impl S {
    #[flux::sig(fn (self: &strg S[@old_x]) ensures self: S[{ x: 1, ..some_computation(old_x) }])]
    pub fn update(&mut self) {
        self.x = 1;
    }

    #[flux::sig(fn (self: &strg S[@old_x]) ensures self: S[{ x: 1, ..S { x: 2, ..old_x } }])]
    pub fn update2(&mut self) {
        self.x = 1;
    }
}
}

Const

You can use int-ish const in refinements e.g.

#![allow(unused)]
fn main() {
pub struct Cow {}

impl Cow {
    const GRASS: usize = 12;

    #[flux_rs::sig(fn () -> usize[12])]
    pub fn test() -> usize {
        Self::GRASS
    }
}
}

#![allow(unused)]
fn main() {
#[repr(u32)]
pub enum SyscallReturnVariant {
    Failure = 0,
}

#[flux_rs::sig(fn() -> u32[0])]
pub fn test() -> u32 {
    SyscallReturnVariant::Failure as u32
}
}

#![allow(unused)]
fn main() {
pub struct Cow {}

const GRASS: usize = 12;
impl Cow {
    #[flux_rs::sig(fn () -> usize[12])]
    fn test() -> usize {
        GRASS
    }
}
}

Requires with forall

We allow a forall on the requires clauses, e.g.

#![allow(unused)]
fn main() {
#[flux::sig(fn(bool[true]))]
fn assert(_: bool) {}
#[flux::sig(
    fn(x: i32)
    requires forall y. y >= 0 => y > x
)]
fn requires_negative(x: i32) {
    assert(x + 1 == 1 + x); // make sure there's something to check to avoid optimizing the entire constraint away
}

fn test2() {
    requires_negative(-1);
}
}

Refined Associated Types

#![allow(unused)]
fn main() {
use flux_rs::*;

#[sig(fn(bool[true]))]
fn assert(_: bool) {}

trait MyTrait {
    type Assoc;

    #[sig(fn(Self::Assoc[@x]) -> Self::Assoc[x])]
    fn f0(x: Self::Assoc) -> Self::Assoc;

    #[sig(fn(x: Self::Assoc) -> Self::Assoc{ v: v == x })]
    fn f1(x: Self::Assoc) -> Self::Assoc;
}

impl MyTrait for () {
    type Assoc = i32;

    #[sig(fn(x: i32) -> i32[x])]
    fn f0(x: i32) -> i32 {
        x
    }

    #[sig(fn(x: i32) -> i32[x])]
    fn f1(x: i32) -> i32 {
        x
    }
}

fn test00() {
    let x = <() as MyTrait>::f0(0);
    assert(x == 0);
}

fn test01() {
    let x = <() as MyTrait>::f1(0);
    assert(x == 0);
}
}

Pragma: ignore

Used to tell flux to ignore (checking) a bunch of definitions.

#![allow(unused)]
#![flux::ignore] // default to ignore for the entire crate

fn main() {
#[flux::ignore(no)] // include this module
mod included {
    #[flux::sig(fn(bool[true]))]
    pub fn assert(_: bool) {}

    pub fn test1() {
        // we are indeed checking this code
        assert(20 < 10); //~ ERROR refinement type error
    }

    pub fn test2() {
        // we cannot use an ignored function in included code
        crate::ignored_fun(); //~ERROR use of ignored function
    }
}

// bad refinement, but no error since we are ignoring this function
#[flux::sig(fn(i32, i32))]
pub fn malformed(_: i32) {}

// an ignored function that cannot be used in included code
pub fn ignored_fun() {}
}

Pragma: should_fail

Used to tell flux to expect a failure when checking a function.

#![allow(unused)]
fn main() {
// This function has an error
// but it's marked as should_fail so that ok.
// flux would yell if instead it verified!

#[flux::should_fail]
#[flux::sig(fn(x: i32) -> i32[x + 1])]
fn test00(x: i32) -> i32 {
    x + 2
}
}

Const Generics

flux lets you use Rust's const-generics inside refinements.

Refining Array Lengths

#![allow(unused)]
fn main() {
// https://github.com/flux-rs/flux/issues/625

const BUFLEN: usize = 100;

pub struct Blob {
    data: [i32; BUFLEN],
}

pub fn test(buf: &[i32; BUFLEN]) -> i32 {
    let x0 = buf[0];
    let x1 = buf[10];
    let x2 = buf[BUFLEN - 1];
    let xbad = buf[BUFLEN]; //~ ERROR assertion might fail
    x0 + x1 + x2 + xbad
}

pub fn test_blob(blob: Blob) -> i32 {
    let x0 = blob.data[0];
    let x1 = blob.data[10];
    let x2 = blob.data[BUFLEN - 1];
    let xbad = blob.data[BUFLEN]; //~ ERROR assertion might fail
    x0 + x1 + x2 + xbad
}
}

Refining Struct Fields

#![allow(unused)]
fn main() {
#[flux::invariant(N > 0)]
pub struct MPU<const N: usize> {
    #[flux::field({ i32 | N > 0 })]
    field: i32,
}

pub fn foo<const N: usize>(x: usize, _mpu: MPU<N>) {
    let _x = x % N;
}

#[flux::invariant(N > 0)]
pub struct MPUGOOD<const N: usize> {
    field: i32,
}

pub fn bar<const N: usize>(x: usize, _mpu: MPUGOOD<N>) {
    let _x = x % N;
}

pub fn baz<const N: usize>() -> i32 {
    if N > 0 {
        let mpu = MPUGOOD::<N> { field: 12 };
        mpu.field
    } else {
        0
    }
}
}

Refining Function Signatures

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

/// A statically sized matrix represented with a linear vector
struct Matrix<const N: usize, const M: usize> {
    #[flux::field(RVec<i32>[N * M])]
    inner: RVec<i32>,
}

impl<const N: usize, const M: usize> Matrix<N, M> {
    fn new() -> Matrix<N, M> {
        Matrix { inner: RVec::from_elem_n(0, N * M) }
    }

    #[flux::sig(fn(&mut Self, i: usize{ i < N }, j: usize{ j < M }, v: i32))]
    fn set(&mut self, i: usize, j: usize, v: i32) {
        self.inner[i * M + j] = v
    }

    #[flux::sig(fn(&Self, i: usize{ i < N }, j: usize{ j < M }) -> i32)]
    fn get(&self, i: usize, j: usize) -> i32 {
        self.inner[i * M + j]
    }
}
}

Type Aliases

You can define refined type aliases for Rust types.

Note

1. They are connected to an underlying Rust type,
2. They may also be parameterized by refinements, e.g. Lb
3. There are two different kinds of parametrizations
   • early (Nat) and
   • late (Lb).

#![allow(unused)]
fn main() {
#[flux::alias(type Nat[n: int] = {i32[n] | 0 <= n})]
type Nat = i32;

#[flux::alias(type Lb(n: int)[v: int] = {i32[v] | n <= v})]
type Lb = i32;

#[flux::sig(fn(x: Nat) -> Nat)]
pub fn test1(x: Nat) -> Nat {
    x + 1
}

#[flux::sig(fn(x: Lb(10)) -> Lb(10))]
pub fn test2(x: Lb) -> Lb {
    x + 1
}
}

Spec Function Definitions

You can define spec functions that abstract complicated refinements into refinement-level functions, which can then be used in refinements.

Plain Expressions

#![allow(unused)]
#![flux::defs {
fn main() {
    fn is_btwn(v:int, lo:int, hi: int) -> bool { lo <= v && v <= hi }
    fn ok_day(d:int) -> bool { is_btwn(d, 1, 31) }
    fn is_month30(m:int) -> bool { m == 4 || m == 6 || m == 9 || m == 11 }
    fn ok_month(d:int, m:int) -> bool { is_btwn(m, 1, 12) && (is_month30(m) => d <= 30) }
    fn is_leap_year(y:int) -> bool { y % 400 == 0 || (y % 4 == 0 && (y % 100) > 0) }
    fn is_feb_day(d:int, y:int) -> bool { d <= 29 && ( d == 29 => is_leap_year(y) ) }
    fn ok_year(d:int, m:int, y:int) -> bool { 1 <= y && (m == 2 => is_feb_day(d, y)) }
}]

// https://github.com/chrisdone/sandbox/blob/master/liquid-haskell-dates.hs

#[allow(dead_code)]
#[flux::refined_by(d:int, m:int, y:int)]
pub struct Date {
    #[flux::field({ usize[d] | ok_day(d) })]
    day: usize,
    #[flux::field({ usize[m] | ok_month(d, m)})]
    month: usize,
    #[flux::field({ usize[y] | ok_year(d, m, y)})]
    year: usize,
}

pub fn test() {
    let _ok_date = Date { day: 9, month: 8, year: 1977 };
}

// TODO: Tedious to duplicate the definitions if you want to use them in rust code.
// Maybe some macro magic can unify?

#[flux::sig(fn(m:usize) -> bool[is_month30(m)])]
fn is_month30(m: usize) -> bool {
    m == 4 || m == 6 || m == 9 || m == 11
}

#[flux::sig(fn(y:usize) -> bool[is_leap_year(y)])]
fn is_leap_year(y: usize) -> bool {
    y % 400 == 0 || (y % 4 == 0 && y % 100 != 0)
}

#[flux::sig(fn(d:usize, y:usize) -> bool[is_feb_day(d, y)])]
fn is_feb_day(d: usize, y: usize) -> bool {
    d <= 29 && (d != 29 || is_leap_year(y))
}

pub fn mk_date(day: usize, month: usize, year: usize) -> Option<Date> {
    if 1 <= year && 1 <= month && month <= 12 && 1 <= day && day <= 31 {
        if !is_month30(month) || day <= 30 {
            if month != 2 || is_feb_day(day, year) {
                return Some(Date { day, month, year });
            }
        }
    }
    return None;
}
}

let binders

#![allow(unused)]
fn main() {
use flux_rs::attrs::*;

defs! {
    fn times2(x: int) -> int {
        x * 2
    }

    fn test(x: int) -> int {
        let y = times2(x);
        let z = times2(y);
        z * z * y
    }
}

#[sig(fn() -> i32[test(10)])]
fn test() -> i32 {
    32000
}
}

Bounded Quantification

#![allow(unused)]
#![flux::defs {
fn main() {
    fn magic(xing:int, yonk:int) -> bool;

    fn magic_all(noob:int) -> bool {
        forall i in 0 .. 4 {
            magic(i, noob)
        }
    }

    fn magic_ex(n:int) -> bool {
        exists i in 0 .. 4 {
            i == n
        }
    }
}]

#[flux::trusted]
#[flux::sig(fn(x:i32, y:i32) ensures magic(x, y))]
pub fn do_magic(_x: i32, _y: i32) {}

// forall tests ----------------------------------------------------------------

#[flux::sig(fn({i32[@n] | magic_all(n)}) ensures magic(3, n))]
pub fn test_all_l(_x: i32) {}

#[flux::sig(fn(n:i32) ensures magic_all(n))]
pub fn test_all_r(n: i32) {
    do_magic(0, n);
    do_magic(1, n);
    do_magic(2, n);
    do_magic(3, n);
}

// exists tests ----------------------------------------------------------------
#[flux::sig(fn({i32[@n] | magic_ex(n)}) -> bool[true])]
pub fn test_exi_l(n: i32) -> bool {
    n == 0 || n == 1 || n == 2 || n == 3
}

#[flux::sig(fn(n:i32) -> bool[magic_ex(n)])]
pub fn test_exi_r(n: i32) -> bool {
    n == 0 || n == 1 || n == 2 || n == 3
}
}

No Cycles!

However, there should be no cyclic dependencies in the function definitions.

#![allow(unused)]
#![flux::defs {
fn main() {
    fn even(x: int) -> bool { x == 0 || odd(x-1) }
    fn odd(x: int) -> bool { x == 1 || even(x-1) } //~ ERROR cycle
}]

#[flux::sig(fn(x:i32) -> i32[x+1])]
pub fn test(x: i32) -> i32 {
    x + 1
}
}

Uninterpreted Function Declarations

You can also declare uninterpreted functions -- about which flux knows nothing other than the congruence property -- and then use them in refinements. Note that in this case you have to use a trusted annotation for the function (e.g. is_valid) that asserts facts over the uninterpreted function

#![allow(unused)]
#![flux::defs {
fn main() {
    fn valid(x:int) -> bool;
}]

#[flux::trusted]
#[flux::sig(fn(x:i32) -> bool[valid(x)])]
fn is_valid(x: i32) -> bool {
    0 <= x && x <= 100
}

#[flux::sig(fn (i32{v:valid(v)}) -> i32)]
fn bar(a: i32) -> i32 {
    return a;
}

#[flux::sig(fn(i32))]
pub fn test(n: i32) {
    let ok = is_valid(n);
    if ok {
        bar(n);
    }
}
}

#![allow(unused)]
#![flux::defs {
fn main() {
    fn foo(x:int, y:int) -> int;
}]

#[flux::trusted]
#[flux::sig(fn(x: i32, y:i32) -> i32[foo(x, y)])]
fn foo(x: i32, y: i32) -> i32 {
    x + y
}

#[flux::sig(fn (i32[foo(10, 20)]) -> i32)]
fn bar(a: i32) -> i32 {
    return a;
}

#[flux::sig(fn())]
pub fn test() {
    let a = 10;
    let b = 20;
    let c = foo(a, b);
    bar(c);
}
}

Hiding and Revealing Function Definitions

By default all the function definitions are either inlined or sent to the SMT solver as define-fun (when run with FLUX_SMT_DEFINE_FUN=1). Sometimes we want to hide the definition because reasoning about those functions can kill the solver -- or the function is super complex and we just want to reason about it via congruence. For that you can

• use the #[hide] attribute at the spec function definition, to make the function uninterpreted by default, and
• use the #[reveal] attribute at specific Rust function definition, to indicate you want to use the actual definition when checking that Rust function.

#![allow(unused)]
#![flux::defs {
fn main() {
    #[hide]
    fn mod33(n:int) -> int {
        n % 33
    }

    #[hide]
    fn foo(n:int, k:int) -> bool {
      mod33(n) == k
    }

}]

#[flux::sig(fn (a:i32) requires foo(a, 7))]
pub fn assert_foo(_a: i32) {}

#[flux::reveal(foo, mod33)]
pub fn use_foo(n: i32) {
    if n == 40 {
        assert_foo(n)
        // without `reveal(foo)` we want to see an error in the above line.
    }
}

#[flux::sig(fn (xs: &[i32{v: foo(v, 7)}][100]) -> i32{v : foo(v, 7)})]
pub fn bar(xs: &[i32]) -> i32 {
    xs[0] // `foo` as uninterpreted works fine
}
}

Spec Functions in SMTLIB

By default flux inlines all such function definitions.

Monomorphic functions may optionally be encoded as functions in SMT by using the FLUX_SMT_DEFINE_FUN=1 environment variable.

Type Holes

You can (sometimes!) use _ in the flux signatures to omit the Rust components, e.g.

Function Signatures

#![allow(unused)]
fn main() {
#[flux::sig(fn(_) -> Option<_>)]
fn test00(x: i32) -> Option<i32> {
    Some(x)
}

#[flux::sig(fn(x: &strg _) ensures x: i32[0])]
fn test01(x: &mut i32) {
    *x = 0;
}

#[flux::sig(fn(x: &strg i32) ensures x: _)]
fn test02(x: &mut i32) {
    *x = 0;
}
}

Structs and Enums

#![allow(unused)]
fn main() {
// Type holes in structs and enums

pub struct S {
    #[flux::field(Option<_>)]
    x: Option<i32>,
}

pub fn test_s(s: S) -> Option<i32> {
    s.x
}

pub enum E {
    #[flux::variant((_) -> E)]
    A(i32),
}

pub fn test_e(e: E) -> i32 {
    match e {
        E::A(x) => x,
    }
}
}

Type Aliases

#![allow(unused)]
fn main() {
#[flux::alias(type Test = Vec<_>)]
type Test = Vec<i32>;

fn test(x: Test) -> Vec<i32> {
    x
}
}

Generic Args

#![allow(unused)]
fn main() {
#[flux_rs::refined_by(m: Map<int, int>)]
#[flux_rs::opaque]
pub struct S1<const N: usize> {
    _arr: [usize; N],
}

const MY_N: usize = 10;

#[flux_rs::refined_by(gloop: S1)]
pub struct S2 {
    #[field(S1<_>[gloop])]
    pub s1: S1<MY_N>,
}

#[flux_rs::refined_by(zoo: S1)]
pub struct S3<const M: usize> {
    #[field(S1<_>[zoo])]
    pub s1: S1<M>,
}
}

Closures

#![allow(unused)]
fn main() {
#[flux::sig(fn(c: Option<bool>) -> Option<i32{v:0 <= v}>)]
pub fn test0(c: Option<bool>) -> Option<i32> {
    c.map(|b| if b { 1 } else { 2 })
}

#[flux::sig(fn(c: Option<bool>) -> Option<i32{v:1 <= v}>)]
pub fn test1(c: Option<bool>) -> Option<i32> {
    c.map(|b| if b { 1 } else { 2 })
}

#[flux::sig(fn(c: Option<bool[true]>) -> Option<i32[1]>)]
pub fn test2(c: Option<bool>) -> Option<i32> {
    c.map(|b| if b { 1 } else { 2 })
}

#[flux::sig(fn(n:usize) -> usize[n + 2])]
pub fn test3(n: usize) -> usize {
    checked_add(n, 1)
        .and_then(|m| Some(m + 1))
        .expect("overflow")
}

#[flux::trusted]
#[flux::sig(fn(n:usize, m:usize) -> Option<usize[n + m]>)]
pub fn checked_add(n: usize, m: usize) -> Option<usize> {
    n.checked_add(m)
}
}

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

#[flux::trusted]
fn smap<S, F, A, B>(s: S, v: Vec<A>, f: F) -> Vec<B>
where
    F: Fn(S, A) -> B,
    S: Copy,
{
    v.into_iter().map(|x| f(s, x)).collect()
}

#[flux::sig(fn(vs: Vec<i32{v:0<=v}>) -> Vec<i32{v:3<=v}>)]
pub fn test1_old(vs: Vec<i32>) -> Vec<i32> {
    let st = 3;
    smap(st, vs, |s, x| s + x)
}

#[flux::sig(fn(vs: Option<i32{v:0<=v}>) -> Option<i32{v:3<=v}>)]
pub fn test2_old(vs: Option<i32>) -> Option<i32> {
    let y = 1;
    let z = 2;
    vs.map(|x| x + y + z)
}

pub struct Foo {
    #[flux::field(i32{v: 10 <= v})]
    pub val: i32,
}

pub fn test1(c: Option<bool>) -> Option<Foo> {
    let x = 6;
    let y = 10;
    c.map(|b| if b { Foo { val: x + y } } else { Foo { val: 20 } })
}

#[flux::sig(fn(vec:&RVec<i32{v: 10 <= v}>{v: 0 < v}) -> Foo)]
fn bob(vec: &RVec<i32>) -> Foo {
    Foo { val: vec[0] }
}

pub fn test2(c: Option<bool>) -> Option<Foo> {
    let vec = rvec![100, 200, 300];
    c.map(|b| if b { bob(&vec) } else { Foo { val: 20 } })
}

#[flux::trusted]
fn frob(_vec: &RVec<RVec<i32>>) -> Foo {
    todo!()
}

pub fn test3(c: Option<bool>, vec: RVec<RVec<i32>>) -> Option<Foo> {
    // let mut vec = rvec![rvec![100, 200, 300]];
    c.map(|b| if b { frob(&vec) } else { Foo { val: 20 } })
}
}

Function Pointers

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

fn main() {
#[flux::sig(fn (x:usize) -> usize[x+1])]
fn inc(x: usize) -> usize {
    x + 1
}

#[flux::sig(fn(c: Option<usize[99]>) -> Option<usize[100]>)]
pub fn test_ok(c: Option<usize>) -> Option<usize> {
    c.map(inc)
}
}

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

fn main() {
fn id<T>(x: T) -> T {
    x
}

#[flux::sig(fn(c: Option<usize[99]>) -> Option<usize[99]>)]
pub fn test_ok(c: Option<usize>) -> Option<usize> {
    c.map(id)
}

#[flux::sig(fn(Option<i32[99]>) -> Option<i32[99]>)]
fn test_also_ok(x: Option<i32>) -> Option<i32> {
    let f = id;
    x.map(f)
}
}

#![allow(unused)]
fn main() {
use flux_rs::*;

#[sig(fn(x: i32{x != 0}) -> i32[1/x])]
fn div(x: i32) -> i32 {
    1 / x
}

fn apply<A, B>(f: impl FnOnce(A) -> B, x: A) -> B {
    f(x)
}

#[sig(fn() -> i32[0])]
fn test() -> i32 {
    apply(div, 10)
}
}

Traits and Implementations

#![allow(unused)]
fn main() {
pub trait MyTrait {
    fn foo() -> i32;
    fn bar();
}

pub struct MyTy;

impl MyTrait for MyTy {
    #[flux::sig(fn () -> i32[10])]
    fn foo() -> i32 {
        10
    }

    fn bar() {}
}

#[flux::sig(fn () -> i32[10])]
pub fn test() -> i32 {
    let n = MyTy::foo();
    MyTy::bar();
    n
}
}

#![allow(unused)]
fn main() {
pub trait Mono {
    #[flux::sig(fn (zing: &strg i32[@n]) ensures zing: i32{v:n < v})]
    fn foo(z: &mut i32);
}

pub struct Tiger;

impl Mono for Tiger {
    #[flux::sig(fn (pig: &strg i32[@m]) ensures pig: i32{v:m < v})]
    fn foo(pig: &mut i32) {
        *pig += 1;
    }
}

pub struct Snake;

impl Mono for Snake {
    #[flux::sig(fn (pig: &strg i32[@m]) ensures pig: i32[m+1])]
    fn foo(pig: &mut i32) {
        *pig += 1;
    }
}
}

#![allow(unused)]
fn main() {
pub trait Mono {
    #[flux::sig(fn (zing: &strg i32[@n])
                  requires 100 < n
                  ensures zing: i32{v:n < v})]
    fn foo(z: &mut i32);
}

pub struct Tiger;

impl Mono for Tiger {
    #[flux::sig(fn (pig: &strg i32[@m])
                  requires 0 < m
                  ensures pig: i32{v:m < v})]
    fn foo(pig: &mut i32) {
        *pig += 1;
    }
}

pub struct Snake;

impl Mono for Snake {
    #[flux::sig(fn (pig: &strg {i32[@m] | 0 < m})
                ensures pig: i32[m+1])]
    fn foo(pig: &mut i32) {
        *pig += 1;
    }
}
}

#![allow(unused)]
fn main() {
#[flux::generics(Self as base)]
pub trait MyTrait {
    #[flux::sig(fn[hrn p: Self -> bool](&Self{v: p(v)}) -> Self{v: p(v)})]
    fn foo1(&self) -> Self;

    fn foo2(&self) -> Self;
}

impl MyTrait for i32 {
    // TODO: error-message when below is missing (currently: fixpoint crash!) see tests/tests/todo/trait13.rs
    #[flux::sig(fn[hrn p: Self -> bool](&Self{v: p(v)}) -> Self{v: p(v)})]
    fn foo1(&self) -> Self {
        *self
    }

    #[flux::sig(fn[hrn q: Self -> bool](&Self{v: q(v)}) -> Self{v: q(v)})]
    fn foo2(&self) -> Self {
        *self
    }
}

#[flux::sig(fn[hrn q: T -> bool](&T{v:q(v)}) -> T{v: q(v)})]
pub fn bar1<T: MyTrait>(x: &T) -> T {
    x.foo1()
}

#[flux::sig(fn(bool[true]))]
fn assert(_b: bool) {}

pub fn test() {
    let x = 42;
    assert(bar1(&x) == 42);
    assert(x.foo2() == 42);
}
}

#![allow(unused)]
fn main() {
pub trait Silly<A> {
    #[flux::sig(fn(&Self, z: A) -> i32{v:100 < v})]
    fn bloop(&self, z: A) -> i32;
}

impl Silly<bool> for i32 {
    #[flux::sig(fn(&Self, b : bool) -> i32[2000])]
    fn bloop(&self, _b: bool) -> i32 {
        2000
    }
}

#[flux::sig(fn(i32) -> i32{v: 100 < v})]
pub fn client(x: i32) -> i32 {
    let y = x.bloop(true);
    y + 1
}

#[flux::sig(fn(_, _) -> i32{v:100 < v})]
pub fn client2<A, B: Silly<A>>(x: B, y: A) -> i32 {
    x.bloop(y)
}
}

Impl Trait

#![allow(unused)]
fn main() {
pub fn test1() -> impl Iterator<Item = i32> {
    Some(10).into_iter()
}

#[flux::sig(fn () -> impl Iterator<Item = i32{v:1<=v}>)]
pub fn test2() -> impl Iterator<Item = i32> {
    Some(10).into_iter()
}

#[flux::sig(fn () -> impl Iterator<Item = i32{v:1<=v}>)]
pub fn test_lib() -> impl Iterator<Item = i32> {
    Some(10).into_iter()
}

#[flux::sig(fn () -> Option<i32{v:0<=v}>)]
pub fn test_client() -> Option<i32> {
    let mut it = test_lib();
    it.next()
}
}

#![allow(unused)]
fn main() {
#[flux::sig(fn (x:i32) -> impl Iterator<Item = i32{v:x<=v}>)]
pub fn lib(x: i32) -> impl Iterator<Item = i32> {
    Some(x).into_iter()
}

#[flux::sig(fn (k:i32) -> Option<i32{v:k<=v}>)]
pub fn test_client(k: i32) -> Option<i32> {
    let mut it = lib(k);
    it.next()
}
}

Dynamic Trait Objects

#![allow(unused)]

// ------------------------------------------------------

trait Shape {
    #[flux::sig(fn(self: _) -> i32{v: 0 <= v})]
    fn vertices(&self) -> i32;
}

// ------------------------------------------------------

struct Circle {}

impl Shape for Circle {
    #[flux::sig(fn(self: _) -> i32{v: 0 <= v})]
    fn vertices(&self) -> i32 {
        0
    }
}

// ------------------------------------------------------

#[flux::sig(fn(shape: _) -> i32{v: 0 <= v})]
fn count(shape: &dyn Shape) -> i32 {
    shape.vertices()
}

#[flux::sig(fn(shape: _) -> i32{v: 10 <= v})]
fn count_bad(shape: &dyn Shape) -> i32 {
    shape.vertices() //~ ERROR: refinement type
}

fn main() {
    let c = Circle {};
    count(&c);
    count_bad(&c);
}

Generic Refinements

flux supports generic refinements see this paper for details

Horn Refinements

#![allow(unused)]
fn main() {
// Define a function whose type uses the Horn generic refinement `p`
#[flux::sig(
    fn[hrn p: int -> bool](x: i32, y: i32) -> i32{v: p(v) && v >= x && v >= y}
    requires p(x) && p(y)
)]
fn max(x: i32, y: i32) -> i32 {
    if x > y { x } else { y }
}

// A client of `max` where the generic is instantiated to `|v| {v % 2 == 0}`
#[flux::sig(fn() -> i32{v: v % 2 == 0})]
pub fn test00() -> i32 {
    max(4, 10)
}

// A client of `max` where the generic is instantiated to `|v| {v == 4 || v == 10}`
#[flux::sig(fn() -> i32[10])]
pub fn test01() -> i32 {
    max(4, 10)
}
}

#![allow(unused)]
fn main() {
#[flux::refined_by(a: int, b: int, hrn p: (int, int) -> bool)]
struct Pair {
    #[flux::field(i32[a])]
    fst: i32,
    #[flux::field({i32[b] | p(a, b)})]
    snd: i32,
}

#[flux::sig(fn() -> Pair)]
fn test00() -> Pair {
    Pair { fst: 0, snd: 1 }
}

#[flux::sig(fn(Pair[@a, @b, |a, b| a < b]) -> i32{v: v > 0})]
fn test01(pair: Pair) -> i32 {
    pair.snd - pair.fst
}

fn test02() {
    let pair = Pair { fst: 0, snd: 1 };
    let x = test01(pair);
}

#[flux::sig(fn(x: i32, Pair[@a, @b, |a, b| a > x]) -> i32{v: v > x})]
fn test03(x: i32, pair: Pair) -> i32 {
    pair.fst
}

fn test04() {
    let pair = Pair { fst: 10, snd: 0 };
    test03(0, pair);
}
}

#![allow(unused)]
fn main() {
#[derive(Clone, Copy)]
#[flux::refined_by(hrn p: int -> bool)]
pub struct S;

#[flux::sig(fn(x: i32) -> S[|y| y > x])]
pub fn gt(x: i32) -> S {
    S
}

#[flux::sig(fn(x: i32) -> S[|y| y < x])]
pub fn lt(x: i32) -> S {
    S
}

#[flux::sig(fn(S[@p1], S[@p2]) -> S[|x| p1(x) || p2(x)])]
pub fn or(_: S, _: S) -> S {
    S
}

#[flux::sig(fn(S[@p], x: i32{ p(x) }))]
pub fn check(_: S, x: i32) {}

pub fn test() {
    let s = or(gt(10), lt(0));
    check(s, 11);
    check(s, -1);
}
}

Hindley Refinements

TODO

Bitvector Refinements

Operators

#![allow(unused)]
fn main() {
// https://github.com/flux-rs/flux/issues/1010

use flux_rs::{attrs::*, bitvec::BV32};

#[sig(fn (x:BV32{x == 1}) ensures (bv_shl(x, 3) == 8))]
pub fn test_shl_a(_x: BV32) {}

#[sig(fn (x:BV32{x == 1}) ensures (x << 3 == 8))]
pub fn test_shl_b(_x: BV32) {}

#[sig(fn (x:BV32{x == 8}) ensures (bv_lshr(x, 3) == 1))]
pub fn test_shr_a(_x: BV32) {}

#[sig(fn (x:BV32{x == 8}) ensures (x >> 3 == 1))]
pub fn test_shr_b(_x: BV32) {}

#[sig(fn (x:BV32{x == 8}) ensures (bv_or(x, 3) == 11))]
pub fn test_or_a(_x: BV32) {}

#[sig(fn (x:BV32{x == 8}) ensures (x | 3 == 11))]
pub fn test_or_b(_x: BV32) {}

#[sig(fn (x:BV32{x == 10}) ensures (bv_and(x, 3) == 2))]
pub fn test_and_a(_x: BV32) {}

#[sig(fn (x:BV32{x == 10}) ensures (x & 3 == 2))]
pub fn test_and_b(_x: BV32) {}
}

#![allow(unused)]
fn main() {
use flux_rs::{attrs::*, bitvec::BV32};

#[sig(fn(x: BV32) -> BV32[bv_add(x, bv_int_to_bv32(1))])]
pub fn test_00(x: BV32) -> BV32 {
    x + BV32::new(1)
}

#[sig(fn(x: BV32) -> BV32[x + bv_int_to_bv32(1)])]
pub fn test_01(x: BV32) -> BV32 {
    x + BV32::new(1)
}

#[sig(fn(x: BV32) -> BV32[x + 1])]
pub fn test_02(x: BV32) -> BV32 {
    x + BV32::new(1)
}

#[sig(fn(x: i32) -> i32[x + (1 + 2)])]
pub fn test_03(x: i32) -> i32 {
    x + 3
}

#[sig(fn() -> BV32[bv_int_to_bv32(0x5)])]
pub fn test_04() -> BV32 {
    BV32::new(0x5)
}

#[sig(fn() -> BV32[5])]
pub fn test_05() -> BV32 {
    BV32::new(0x5)
}

#[sig(fn(x: BV32, y:BV32) -> bool[x + y > 5])]
pub fn test_06(x: BV32, y: BV32) -> bool {
    x + y > BV32::new(5)
}

#[sig(fn(x: BV32, y:BV32) -> bool[x + y > x - y])]
pub fn test_07(x: BV32, y: BV32) -> bool {
    x + y > x - y
}
}

#![allow(unused)]
fn main() {
use std::ops::{Add, Sub};

#[flux::opaque]
#[flux::refined_by(x: bitvec<32>)]
pub struct BV32(u32);

impl BV32 {
    #[flux::trusted]
    #[flux::sig(fn (u32[@x]) -> BV32[bv_int_to_bv32(x)])]
    pub fn new(x: u32) -> Self {
        BV32(x)
    }
}

impl Add for BV32 {
    type Output = BV32;

    #[flux_rs::trusted]
    #[flux_rs::sig(fn (BV32[@val1], BV32[@val2]) -> BV32[bv_add(val1, val2)])]
    fn add(self, rhs: Self) -> BV32 {
        BV32(self.0 + rhs.0)
    }
}

impl Sub for BV32 {
    type Output = BV32;

    #[flux_rs::trusted]
    #[flux_rs::sig(fn (BV32[@val1], BV32[@val2]) -> BV32[bv_sub(val1, val2)])]
    fn sub(self, rhs: Self) -> BV32 {
        BV32(self.0.wrapping_add(!rhs.0))
    }
}

impl PartialEq for BV32 {
    #[flux::trusted]
    #[flux::sig(fn (&BV32[@val1], &BV32[@val2]) -> bool[val1 == val2])]
    fn eq(&self, other: &Self) -> bool {
        self.0 == other.0
    }

    #[flux::trusted]
    #[flux::sig(fn (&BV32[@val1], &BV32[@val2]) -> bool[val1 != val2])]
    fn ne(&self, other: &Self) -> bool {
        self.0 != other.0
    }
}

impl PartialOrd for BV32 {
    #[flux::trusted]
    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
        self.0.partial_cmp(&other.0)
    }

    #[flux::trusted]
    #[flux::sig(fn (&BV32[@x], &BV32[@y]) -> bool[bv_ule(x, y)])]
    fn le(&self, other: &Self) -> bool {
        self.0 <= other.0
    }

    #[flux::trusted]
    #[flux::sig(fn (&BV32[@x], &BV32[@y]) -> bool[bv_ult(x, y)])]
    fn lt(&self, other: &Self) -> bool {
        self.0 < other.0
    }

    #[flux::trusted]
    #[flux::sig(fn (&BV32[@x], &BV32[@y]) -> bool[bv_uge(x, y)])]
    fn ge(&self, other: &Self) -> bool {
        self.0 >= other.0
    }

    #[flux::trusted]
    #[flux::sig(fn (&BV32[@x], &BV32[@y]) -> bool[bv_ugt(x, y)])]
    fn gt(&self, other: &Self) -> bool {
        self.0 > other.0
    }
}

#[flux::sig(fn (BV32[@x]) -> bool[bv_ule(x, x)])]
pub fn trivial_le(x: BV32) -> bool {
    x <= x
}

#[flux::sig(fn (BV32[@x]) -> bool[bv_ult(x, x)])]
pub fn trivial_lt(x: BV32) -> bool {
    x < x
}

#[flux::sig(fn (BV32[@x]) -> bool[bv_uge(x, x)])]
pub fn trivial_ge(x: BV32) -> bool {
    x <= x
}

#[flux::sig(fn (BV32[@x]) -> bool[bv_ugt(x, x)])]
pub fn trivial_gt(x: BV32) -> bool {
    x < x
}

#[flux::sig(fn (BV32[@x], BV32[@y]) -> bool[
    bv_ule(x, bv_int_to_bv32(10))
    && 
    bv_uge(y, bv_int_to_bv32(20))
    &&
    bv_ult(x, bv_int_to_bv32(11))
    &&
    bv_ugt(y, bv_int_to_bv32(21))
])]
pub fn real_example(x: BV32, y: BV32) -> bool {
    x <= BV32::new(10) && y >= BV32::new(20) && x < BV32::new(11) && y > BV32::new(21)
}


#[flux_rs::sig(fn (BV32[@x], BV32[@y]) -> bool[true] requires bv_ult(x, y) && bv_ugt(x, bv_int_to_bv32(0x20)) && bv_ult(y, bv_int_to_bv32(0xFF)))]
fn lt_imp(x: BV32, y: BV32) -> bool {
    x - BV32::new(0x20) < y + BV32::new(0x20)
}

#[flux_rs::sig(fn (BV32[@x], BV32[@y]) -> bool[true] requires bv_ule(x, y) && bv_uge(x, bv_int_to_bv32(0x20)) && bv_ule(y, bv_int_to_bv32(0xFF)))]
fn le_imp(x: BV32, y: BV32) -> bool {
    x - BV32::new(0x20) <= y + BV32::new(0x20)
}

#[flux_rs::sig(fn (BV32[@x], BV32[@y]) -> bool[true] requires bv_ugt(x, y) && bv_ugt(y, bv_int_to_bv32(0x20)) && bv_ult(x, bv_int_to_bv32(0xFF)))]
fn gt_imp(x: BV32, y: BV32) -> bool {
    x + BV32::new(0x20) > y - BV32::new(0x20)
}

#[flux_rs::sig(fn (BV32[@x], BV32[@y]) -> bool[true] requires bv_uge(x, y) && bv_uge(y, bv_int_to_bv32(0x20)) && bv_ule(x, bv_int_to_bv32(0xFF)))]
fn ge_imp(x: BV32, y: BV32) -> bool {
    x + BV32::new(0x20) >= y - BV32::new(0x20)
}
}

Specification functions

#![allow(unused)]
fn main() {
use flux_rs::{attrs::*, bitvec::BV32};

defs! {
    fn is_pow2(x: bitvec<32>) -> bool {
        (x > 0) && ((x & x - 1) == 0)
    }
}

#[sig(fn(x: BV32) requires is_pow2(x) && 8 <= x ensures x % 8 == 0)]
fn theorem_pow2_octet(x: BV32) {}
}

Extensions

#![allow(unused)]
fn main() {
// https://github.com/flux-rs/flux/issues/686

#[allow(dead_code)]
#[flux::sig(fn(x: bool[true]))]
pub fn assert(_x: bool) {}

#[flux::opaque]
#[flux::refined_by(v: bitvec<32>)]
struct Register {
    inner: u32,
}

impl Register {
    #[flux::sig(fn(u32[@n]) -> Register[bv_int_to_bv32(n)])]
    #[flux::trusted]
    fn new(v: u32) -> Self {
        Register { inner: v }
    }

    #[flux::sig(fn(&Register[@n]) -> u64[bv_bv64_to_int(bv_zero_extend_32_to_64(n))])]
    #[flux::trusted]
    fn zero_extend(&self) -> u64 {
        self.inner as u64
    }

    #[flux::sig(fn(&Register[@n]) -> u64[bv_bv64_to_int(bv_sign_extend_32_to_64(n))])]
    #[flux::trusted]
    fn sign_extend(&self) -> u64 {
        self.inner as i32 as i64 as u64
    }
}

pub fn test_bv_extensions() {
    let r = Register::new(u32::MAX);
    assert(r.zero_extend() == u32::MAX as u64);
    assert(r.zero_extend() == 12); //~ ERROR refinement type
    assert(r.sign_extend() == u64::MAX);
    assert(r.sign_extend() == 12); //~ ERROR refinement type
}
}

Bitvector Constants

#![allow(unused)]
#![flux::defs(
fn main() {
    fn is_start(x:bitvec<32>) -> bool { x == START }
)]

#[flux::opaque]
#[flux::refined_by(val: bitvec<32>)]
pub struct BV32(u32);

impl BV32 {
    #[flux::trusted]
    #[flux::sig(fn (x:u32) -> BV32[bv_int_to_bv32(x)])]
    const fn new(val: u32) -> Self {
        BV32(val)
    }
}

#[flux_rs::constant(bv_int_to_bv32(0x4567))]
pub const START: BV32 = BV32::new(0x4567);

#[flux_rs::sig(fn () -> BV32[START])]
pub fn test1() -> BV32 {
    BV32::new(0x4567)
}

#[flux_rs::sig(fn () -> BV32{v: is_start(v)})]
pub fn test2() -> BV32 {
    BV32::new(0x4567)
}

#[flux_rs::sig(fn () -> BV32{v: is_start(v)})]
pub fn test3() -> BV32 {
    BV32::new(0x4568) //~ ERROR: refinement type
}
}

char Literals

#![allow(unused)]
fn main() {
#[flux::sig(fn() -> char['a'])]
pub fn char00() -> char {
    'a'
}

#[flux::sig(fn(c: char{v: 'a' <= v && v <= 'z'}) -> bool[true])]
pub fn lowercase(c: char) -> bool {
    'c' == 'c'
}
}

String Literals

#![allow(unused)]
fn main() {
#[flux::sig(fn (&str["cat"]))]
fn require_cat(_x: &str) {}

pub fn test_cat() {
    require_cat("cat");
    require_cat("dog"); //~ ERROR refinement type
}

#[flux::sig(fn (&str[@a], &{str[@b] | a == b}))]
fn require_eq(_x: &str, _y: &str) {}

pub fn test_eq() {
    require_eq("a", "a");
    require_eq("a", "b"); //~ ERROR refinement type
}
}

Extern Specs

The extern_spec is used to provide flux signatures for functions defined in external crates. See the specifications guide for more details.

Functions

#![allow(unused)]
fn main() {
use std::slice::from_ref;

use flux_rs::extern_spec;

#[extern_spec]
#[flux::sig(fn(&T) -> &[T][1])]
fn from_ref<T>(s: &T) -> &[T];

#[flux::sig(fn(&i32) -> &[i32]{n: n > 0})]
pub fn test(x: &i32) -> &[i32] {
    from_ref(x)
}
}

Options

#![allow(unused)]
fn main() {
use flux_rs::extern_spec;

#[extern_spec]
#[flux::refined_by(b:bool)]
enum Option<T> {
    #[flux::variant(Option<T>[false])]
    None,
    #[flux::variant({T} -> Option<T>[true])]
    Some(T),
}

#[extern_spec]
impl<T> Option<T> {
    #[sig(fn(&Option<T>[@b]) -> bool[b])]
    const fn is_some(&self) -> bool;

    #[sig(fn(&Option<T>[@b]) -> bool[!b])]
    const fn is_none(&self) -> bool;
}
}

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

#[flux::trusted]
#[flux::sig(fn(i32{v: false}) -> T)]
pub fn never<T>(_: i32) -> T {
    loop {}
}

#[flux::sig(fn(x:Option<T>[true]) -> T)]
pub fn my_unwrap<T>(x: Option<T>) -> T {
    match x {
        Option::Some(v) => v,
        Option::None => never(0),
    }
}

#[flux::sig(fn(T) -> Option<T>[true])]
fn my_some<T>(x: T) -> Option<T> {
    Option::Some(x)
}

#[flux::sig(fn(bool[true]))]
fn assert(_b: bool) {}

pub fn test1() {
    let x = my_some(42);
    let y = my_unwrap(x);
    assert(y == 42);
}

pub fn test3() {
    let x = Option::Some(42);
    let y = my_unwrap(x);
    assert(y == 42);
}
}

Vec

#![allow(unused)]
fn main() {
use flux_rs::extern_spec;

#[extern_spec]
#[flux::refined_by(b:bool)]
enum Option<T> {
    #[flux::variant(Option<T>[false])]
    None,
    #[flux::variant({T} -> Option<T>[true])]
    Some(T),
}

#[extern_spec]
impl<T> Option<T> {
    #[sig(fn(&Option<T>[@b]) -> bool[b])]
    const fn is_some(&self) -> bool;

    #[sig(fn(&Option<T>[@b]) -> bool[!b])]
    const fn is_none(&self) -> bool;
}
}

Structs

#![allow(unused)]
fn main() {
// Testing we can add external specs to "transparent" structs.

use flux_rs::extern_spec;

#[extern_spec(std::ops)]
#[refined_by(start: Idx, end: Idx)]
struct Range<Idx> {
    #[field(Idx[start])]
    start: Idx,
    #[field(Idx[end])]
    end: Idx,
}

#[extern_spec(std::ops)]
#[generics(Idx as base)]
impl<Idx: PartialOrd<Idx>> Range<Idx> {
    // This specification is actually unsound for `Idx`s where the `PartialOrd` implementation doesn't
    // match the logical `<`.
    #[sig(fn(&Range<Idx>[@r]) -> bool[!(r.start < r.end)])]
    fn is_empty(&self) -> bool;
}

#[flux::sig(fn(bool[true]))]
fn assert(_: bool) {}

fn test00() {
    let r = 0..1;
    assert(!r.is_empty());
}
}

#![allow(unused)]
fn main() {
// Extern spec of a type with a lifetime

use std::slice::Iter;

use flux_rs::*;

#[extern_spec]
#[refined_by(len: int)]
struct Iter<'a, T>;

#[extern_spec]
impl<'a, T> Iter<'a, T> {
    #[spec(fn as_slice(&Iter<T>[@n]) -> &[T][n])]
    fn as_slice(v: &Iter<'a, T>) -> &'a [T];
}

#[extern_spec]
impl<T> [T] {
    #[spec(fn iter(&[T][@n]) -> Iter<T>[n])]
    fn iter(v: &[T]) -> Iter<'_, T>;
}

#[spec(fn test00(x: &[i32][@n]) -> &[i32][n])]
fn test00(x: &[i32]) -> &[i32] {
    x.iter().as_slice()
}
}

Impls

#![allow(unused)]
fn main() {
use flux_rs::extern_spec;

#[extern_spec]
#[flux::refined_by(len: int)]
struct String;

#[extern_spec]
impl String {
    #[flux::sig(fn() -> String[0])]
    fn new() -> String;

    #[flux::sig(fn(&String[@n]) -> usize[n])]
    fn len(s: &String) -> usize;

    #[flux::sig(fn(&String[@n]) -> bool[n == 0])]
    fn is_empty(s: &String) -> bool;

    #[flux::sig(fn(s: &strg String[@n], char) ensures s: String[n+1])]
    fn push(s: &mut String, c: char);

    #[flux::sig(fn(s: &strg String[@n]) -> Option<char>
                requires n > 0
                ensures s: String[n-1])]
    fn pop(s: &mut String) -> Option<char>;

    #[flux::sig(fn(&String[@n]) -> &[u8][n])]
    fn as_bytes(s: &String) -> &[u8];
}

#[extern_spec]
impl<T> [T] {
    #[flux::sig(fn(&[T][@n]) -> usize[n])]
    fn len(v: &[T]) -> usize;

    #[flux::sig(fn(&[T][@n]) -> bool[n == 0])]
    fn is_empty(v: &[T]) -> bool;
}

#[flux::sig(fn(bool[@b]) requires b)]
pub fn assert_true(_: bool) {}

pub fn test_string() {
    let mut s = String::new();
    assert_true(s.is_empty());
    assert_true(s.as_bytes().is_empty());
    s.push('h');
    s.push('i');
    assert_true(s.len() == 2);
    s.pop();
    assert_true(s.len() == 1);
    s.pop();
    assert_true(s.is_empty());
    assert_true(s.as_bytes().is_empty());
}
}

#![allow(unused)]
fn main() {
//@aux-build:extern_spec_impl01_aux.rs

extern crate extern_spec_impl01_aux;

use extern_spec_impl01_aux::MyTrait;
use flux_rs::extern_spec;

#[extern_spec]
impl<T> MyTrait for Vec<T> {
    #[flux::sig(fn() -> i32[10])]
    fn foo() -> i32;
}

#[flux::sig(fn () -> i32[10])]
pub fn test_ok() -> i32 {
    <Vec<i32> as MyTrait>::foo()
}
}

Traits

#![allow(unused)]
fn main() {
use flux_rs::*;

#[extern_spec(std::cmp)]
#[generics(Self as base, Rhs as base)]
#[assoc(fn eq_rel(lhs: Self, rhs: Rhs) -> bool)]
trait PartialEq<Rhs> {
    #[sig(fn(&Self[@lhs], &Rhs[@rhs]) -> bool[<Self as PartialEq<Rhs>>::eq_rel(lhs, rhs)])]
    fn eq(&self, other: &Rhs) -> bool;
}

#[refined_by(n: int)]
struct MyInt(#[field(i32[n])] i32);

#[assoc(fn eq_rel(lhs: MyInt, rhs: MyInt) -> bool { lhs == rhs })]
impl PartialEq for MyInt {
    #[sig(fn(&Self[@lhs], &MyInt[@rhs]) -> bool[<MyInt as PartialEq<MyInt>>::eq_rel(lhs, rhs)])]
    fn eq(&self, other: &MyInt) -> bool {
        self.0 == other.0
    }
}

#[sig(fn(x: T, y: T) -> bool[<T as PartialEq<T>>::eq_rel(x, y)])]
fn test00<T: PartialEq>(x: T, y: T) -> bool {
    x == y
}

#[sig(fn(x: MyInt, y: MyInt) -> bool[x == y])]
fn test01(x: MyInt, y: MyInt) -> bool {
    test00(x, y)
}
}

for loops with range i..j

To see how flux handles for i in 0..n style loops:

#![allow(unused)]
#![feature(step_trait)]
#![allow(unused)]

fn main() {
#[path = "../../lib/iterator.rs"]
mod iterator;

#[flux_rs::sig(fn (bool[true]))]
fn assert(b: bool) {}

fn donald() {
    let n: i32 = 10;
    let mut thing = 0..n;
    let a = thing.next().unwrap();
    assert(a == 0);
    let b = thing.next().unwrap();
    assert(b == 1);
    let c = thing.next().unwrap();
    assert(c == 2);
}

#[flux_rs::sig(fn (n:i32{n == 99}))]
fn goofy(n: i32) {
    let mut thing = 0..n;
    let a0 = thing.end;
    assert(a0 == n);
    while let Some(i) = thing.next() {
        assert(0 <= i);
        assert(i < n);
    }
}

#[flux_rs::sig(fn (n:i32{n == 99}))]
fn mickey(n: i32) {
    for i in 0..n {
        assert(0 <= i);
        assert(i < n);
    }
}

#[flux_rs::trusted]
fn cond() -> bool {
    todo!()
}

fn test(len: i32) {
    if len >= 0 {
        let mut del = 0;
        for i in 0..len {
            assert(del <= i);
            if cond() {
                del += 1;
            }
        }
        assert(del <= len)
    }
}
}

Associated Refinements

Basic

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

fn main() {
use flux_rs::attrs::*;

trait MyTrait {
    #![reft(fn f(x: int) -> int)]
    //
}

struct Add1;

impl MyTrait for Add1 {
    #![reft(fn f(x: int) -> int { x + 1 })]
    //
}

#[sig(fn(x: i32{v: v == <Add1 as MyTrait>::f(0) }))]
fn test00(_x: i32) {}

fn test01() {
    test00(1);
}
}

Check Subtyping at Impl

#![allow(unused)]
fn main() {
// test that implementations with extra const generics work as expected

use flux_rs::attrs::*;

#[reft(fn p(x: int) -> bool)]
trait MyTrait {
    #[sig(fn() -> i32{ v: <Self as MyTrait>::p(v) })]
    fn method() -> i32;
}

struct MyStruct<const N: i32>;

// This implementation requires proving `x == N => x >= N`
#[reft(fn p(x: int) -> bool { x >= N })]
impl<const N: i32> MyTrait for MyStruct<N> {
    #[sig(fn() -> i32{v: v == N})]
    fn method() -> i32 {
        N
    }
}
}

Default

#![allow(unused)]
fn main() {
use flux_rs::attrs::*;

pub trait MyTrait {
    #![reft(fn f(x: int) -> int { x + 1 })]
    //
}

// -----------------------------------------------------------------------------

pub struct Add1;

// Use the "default" assoc reft for Add1
impl MyTrait for Add1 {}

#[flux::sig(fn() -> i32{v: v == <Add1 as MyTrait>::f(0)})]
pub fn test1_ok() -> i32 {
    1
}

#[flux::sig(fn() -> i32{v: v == <Add1 as MyTrait>::f(0)})]
pub fn test1_fail() -> i32 {
    99 //~ ERROR: refinement type error
}

// -----------------------------------------------------------------------------

pub struct Add2;

// Specify a custom assoc reft for Add2
impl MyTrait for Add2 {
    #![reft(fn f(x: int) -> int { x + 2 })]
    //
}

#[flux::sig(fn() -> i32{v: v == <Add2 as MyTrait>::f(0)})]
pub fn test2() -> i32 {
    2
}
}

Use in Extern Spec

#![allow(unused)]
fn main() {
use flux_rs::*;

#[extern_spec(std::cmp)]
#[generics(Self as base, Rhs as base)]
#[assoc(fn eq_rel(lhs: Self, rhs: Rhs) -> bool)]
trait PartialEq<Rhs> {
    #[sig(fn(&Self[@lhs], &Rhs[@rhs]) -> bool[<Self as PartialEq<Rhs>>::eq_rel(lhs, rhs)])]
    fn eq(&self, other: &Rhs) -> bool;
}

#[refined_by(n: int)]
struct MyInt(#[field(i32[n])] i32);

#[assoc(fn eq_rel(lhs: MyInt, rhs: MyInt) -> bool { lhs == rhs })]
impl PartialEq for MyInt {
    #[sig(fn(&Self[@lhs], &MyInt[@rhs]) -> bool[<MyInt as PartialEq<MyInt>>::eq_rel(lhs, rhs)])]
    fn eq(&self, other: &MyInt) -> bool {
        self.0 == other.0
    }
}

#[sig(fn(x: T, y: T) -> bool[<T as PartialEq<T>>::eq_rel(x, y)])]
fn test00<T: PartialEq>(x: T, y: T) -> bool {
    x == y
}

#[sig(fn(x: MyInt, y: MyInt) -> bool[x == y])]
fn test01(x: MyInt, y: MyInt) -> bool {
    test00(x, y)
}
}

#![allow(unused)]
fn main() {
use std::{
    alloc::{Allocator, Global},
    ops::{Index, IndexMut},
    slice::{Iter, SliceIndex},
};

use flux_rs::extern_spec;

#[extern_spec]
#[flux::refined_by(len: int)]
struct Vec<T, A: Allocator = Global>;

#[extern_spec]
#[flux::assoc(fn in_bounds(idx: Self, v: T) -> bool)]
trait SliceIndex<T>
where
    T: ?Sized,
{
}

#[extern_spec]
#[flux::assoc(fn in_bounds(idx: int, len: int) -> bool {idx < len} )]
impl<T> SliceIndex<[T]> for usize {}

#[extern_spec]
#[flux::generics(I as base)]
impl<T, I: SliceIndex<[T]>, A: Allocator> Index<I> for Vec<T, A> {
    #[flux::sig(fn(&Vec<T, A>[@len], {I[@idx] | <I as SliceIndex<[T]>>::in_bounds(idx, len)}) -> _)]
    fn index(z: &Vec<T, A>, index: I) -> &<I as SliceIndex<[T]>>::Output;
}

#[extern_spec]
#[flux::generics(I as base)]
impl<T, I: SliceIndex<[T]>, A: Allocator> IndexMut<I> for Vec<T, A> {
    #[flux::sig(fn(&mut Vec<T,A>[@len], {I[@idx] | <I as SliceIndex<[T]>>::in_bounds(idx, len)}) -> _)]
    fn index_mut(z: &mut Vec<T, A>, index: I) -> &mut <I as SliceIndex<[T]>>::Output;
}

//---------------------------------------------------------------------------------------

#[extern_spec]
impl<T> Vec<T> {
    #[flux::sig(fn() -> Vec<T>[0])]
    fn new() -> Vec<T>;
}

#[extern_spec]
impl<T, A: Allocator> Vec<T, A> {
    #[flux::sig(fn(self: &strg Vec<T, A>[@n], T) ensures self: Vec<T, A>[n+1])]
    fn push(v: &mut Vec<T, A>, value: T);

    #[flux::sig(fn(&Vec<T, A>[@n]) -> usize[n])]
    fn len(v: &Vec<T, A>) -> usize;
}

#[extern_spec]
impl<'a, T, A: Allocator> IntoIterator for &'a Vec<T, A> {
    #[flux::sig(fn (&Vec<T, A>[@n]) -> <&Vec<T, A> as IntoIterator>::IntoIter[0,n])]
    fn into_iter(v: &'a Vec<T, A>) -> <&'a Vec<T, A> as IntoIterator>::IntoIter;
}
}

#![allow(unused)]
fn main() {
use flux_rs::extern_spec;

// Specs for std::slice::Iter and Enumerate
#[extern_spec(std::slice)]
#[refined_by(idx: int, len: int)]
struct Iter<'a, T>;

#[extern_spec(std::iter)]
#[refined_by(idx: int, inner: I)]
struct Enumerate<I>;

#[extern_spec(std::iter)]
#[flux::generics(Self as base)]
#[flux::assoc(fn done(self: Self) -> bool )]
#[flux::assoc(fn step(self: Self, other: Self) -> bool )]
trait Iterator {
    #[flux::sig(fn(self: &strg Self[@curr_s]) -> Option<Self::Item>[!<Self as Iterator>::done(curr_s)] ensures self: Self{next_s: <Self as Iterator>::step(curr_s, next_s)})]
    fn next(&mut self) -> Option<Self::Item>;

    #[flux::sig(fn(Self[@s]) -> Enumerate<Self>[0, s])]
    fn enumerate(self) -> Enumerate<Self>
    where
        Self: Sized;
}

#[extern_spec(std::slice)]
#[flux::assoc(fn done(x: Iter) -> bool { x.idx >= x.len })]
#[flux::assoc(fn step(x: Iter, y: Iter) -> bool { x.idx + 1 == y.idx && x.len == y.len})]
impl<'a, T> Iterator for Iter<'a, T> {
    #[flux::sig(fn(self: &strg Iter<T>[@curr_s]) -> Option<_>[curr_s.idx < curr_s.len] ensures self: Iter<T>{next_s: curr_s.idx + 1 == next_s.idx && curr_s.len == next_s.len})]
    fn next(&mut self) -> Option<&'a T>;
}

#[extern_spec(std::iter)]
#[flux::generics(I as base)]
#[flux::assoc(fn done(x: Enumerate<I>) -> bool { <I as Iterator>::done(x.inner)})]
#[flux::assoc(fn step(x: Enumerate<I>, y: Enumerate<I>) -> bool { <I as Iterator>::step(x.inner, y.inner)})]
impl<I: Iterator> Iterator for Enumerate<I> {
    #[flux::sig(fn(self: &strg Enumerate<I>[@curr_s]) -> Option<(usize[curr_s.idx], _)>[!<I as Iterator>::done(curr_s.inner)]
    ensures self: Enumerate<I>{next_s: curr_s.idx + 1 == next_s.idx && <I as Iterator>::step(curr_s.inner, next_s.inner)})]
    fn next(&mut self) -> Option<(usize, <I as Iterator>::Item)>;
}
}

#![allow(unused)]
#![allow(unused)]
#![feature(allocator_api)]

fn main() {
use std::{iter::Enumerate, slice::Iter};

#[path = "../../lib/option.rs"]
mod option;

#[path = "../../lib/slice.rs"]
mod slice;

#[path = "../../lib/vec.rs"]
mod vec;

#[path = "../../lib/iter.rs"]
mod iter;

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

// Tests
#[flux::sig(fn(slice: &[u8]{n: n > 0}))]
fn test_iter1(slice: &[u8]) {
    let mut iter = slice.iter();
    let next = iter.next();
    assert(next.is_some());
}

#[flux::sig(fn(slice: &[u8]{n: n > 1}))]
fn test_enumerate1(slice: &[u8]) {
    assert(slice.len() > 0);
    let mut enumer = slice.iter().enumerate();

    let next = enumer.next();
    assert(next.is_some());
    let (idx, _) = next.unwrap();
    assert(idx == 0);

    let next_next = enumer.next();
    assert(next_next.is_some());
    let (idx, _) = next_next.unwrap();
    assert(idx == 1);
}

#[flux::sig(fn(&[usize][1]) )]
pub fn test_enumer2(slice: &[usize]) {
    assert(slice.len() == 1);
    let mut enumer = slice.iter().enumerate();

    let next = enumer.next();
    assert(next.is_some());

    let next_next = enumer.next();
    assert(next_next.is_none())
}

#[flux::sig(fn(&[usize][@n]) )]
pub fn test_enumer3(slice: &[usize]) {
    let mut e = slice.iter().enumerate();
    while let Some((idx, _)) = e.next() {
        assert(idx < slice.len())
    }
}
}

Associated Types

#![allow(unused)]
fn main() {
use flux_rs::attrs::*;

trait MyTrait {
    #![reft(fn f(x: int) -> int)]
    //
}

struct Add1;

#[assoc(fn f(x: int) -> int { x + 1 })]
impl MyTrait for Add1 {}

#[sig(fn(x: i32{v: v == <Add1 as MyTrait>::f(0) }))]
fn test00(x: i32) {}

fn test01() {
    test00(0); //~ ERROR refinement type error
}
}

#![allow(unused)]
fn main() {
// Testing that we properly map generics in trait's default associated refinement
// body into the impl.

use flux_rs::attrs::*;

trait MyTrait {
    #![reft(fn p(x: Self) -> bool { true })]

    #[sig(fn(&Self{v: <Self as MyTrait>::p(v)}))]
    fn method(&self);
}

impl MyTrait for i32 {
    #[sig(fn(&Self{v: <Self as MyTrait>::p(v)}))]
    fn method(&self) {}
}

impl<T> MyTrait for S<T> {
    #[sig(fn(&Self{v: <Self as MyTrait>::p(v)}))]
    fn method(&self) {}
}

struct S<T> {
    f: T,
}
}

Refined Associated Types

#![allow(unused)]
fn main() {
use flux_rs::*;

#[assoc(fn can_fit(self: Self, animal: Self::Animal) -> bool)]
trait Barn {
    type Animal;

    #[sig(fn(self: &mut Self[@barn], animal: Self::Animal{ <Self as Barn>::can_fit(barn, animal) }))]
    fn put_animal_in_house(&mut self, animal: Self::Animal);
}

#[refined_by(size: int)]
struct Horse {
    #[field(i32[size])]
    size: i32,
}

#[refined_by(max_size: int)]
struct HorseBarn {
    #[field(i32[max_size])]
    max_size: i32,
}

#[assoc(fn can_fit(self: HorseBarn, horse: Horse) -> bool { horse.size <= self.max_size })]
impl Barn for HorseBarn {
    type Animal = Horse;

    #[trusted]
    #[sig(fn(self: &mut Self[@barn], horse: Horse { horse.size <= barn.max_size}))]
    fn put_animal_in_house(&mut self, horse: Horse) {}
}

fn test00() {
    let mut barn = HorseBarn { max_size: 20 };
    let horse = Horse { size: 10 };

    barn.put_animal_in_house(horse);
}
}

Checking Overflows

You can switch on overflow checking

• globally with a flag or
• locally with an attribute as shown below

#![allow(unused)]
fn main() {
const MAX: u32 = std::u32::MAX;

// Error on this as it may overflow
#[flux::opts(check_overflow = true)]
#[flux::sig(fn (u32[@x], u32[@y], u32[@z]) -> u32[x + y + z] requires x + y + z <= MAX)]
fn add_three(x: u32, y: u32, z: u32) -> u32 {
    x + y + z
}
}

#![allow(unused)]
fn main() {
#[flux::opts(check_overflow = true)]
mod my_mod {
    const MAX: u32 = std::u32::MAX;

    #[flux::sig(fn(u32[@x], u32[@y]) -> u32[x + y] requires x + y <= MAX)]
    fn add(x: u32, y: u32) -> u32 {
        x + y
    }

    #[flux::sig(fn(u32[@x]) -> u32[x + 2] requires x + 2 <= MAX)]
    fn add2(x: u32) -> u32 {
        x + 2
    }
}
}

#![allow(unused)]
fn main() {
const MAX: u32 = std::u32::MAX;

#[flux_rs::refined_by(inner: int)]
struct MyStruct {
    #[field(u32[inner])]
    inner: u32,
}

impl MyStruct {
    fn add1(&self) -> u32 {
        self.inner + 1
    }

    // Error as this may overflow
    #[flux::opts(check_overflow = true)]
    #[flux::sig(fn (&MyStruct[@inner]) -> u32[inner + 2] requires inner + 2 <= MAX)]
    fn add2(&self) -> u32 {
        self.inner + 2
    }
}
}

#![allow(unused)]
fn main() {
const MAX: u32 = std::u32::MAX;

struct MyStruct {
    inner: u32,
}

#[flux::opts(check_overflow = true)]
trait MyTrait {
    #[flux::sig(fn(u32[@x], { u32[@y] | x + y <= MAX }) -> u32[x + y] )]
    fn add(x: u32, y: u32) -> u32;
}

impl MyTrait for MyStruct {
    #[flux::sig(fn(u32[@x], { u32[@y] | x + y <= MAX }) -> u32[x + y] )]
    fn add(x: u32, y: u32) -> u32 {
        x + y
    }
}
}