Flux Specifications
One day, this will be an actual user's guide, but for now,
it is a WIP guide to writing specifications in flux, as
illustrated by examples from the regression tests.
Refinement Types
-
Indexed Type: An indexed type
B[r]is composed of a base Rust typeBand a refinement indexr. The meaning of the index depends on the type. Some examples arei32[n]: denotes the (singleton) set ofi32values equal ton.List<T>[n]: values of typeList<T>of lengthn.
-
Refinement parameter: Function signatures can be parametric on refinement variables. Refinement parameters are declared using the
@nsyntax. For example, the following signature:fn(i32[@n]) -> i32[n + 1]binds
nover the entire scope of the function to specify that it takes ani32equal tonand returns ani32equal ton + 1. This is analogous to languages like Haskell where a lower case letter can be used to quantify over a type, e.g., the typea -> ain Haskell is polymorphic on the typeawhich is bound for the scope of the entire function type. -
Existential Type: An existential type
B{v: r(v)}is composed of a base typeB, a refinement variablevand a refinement predicateronv. Intuitively, a Rust valuexhas typeB{v: r(v)}if there exists a refinement valueasuch thatr(a)holds andxhas typeB[a].i32{v: v > 0}: set of positivei32values.List<T>{v: v > 0}: set of non-empty lists.
-
Constraint Type: A constraint type has the form
{T | r}whereTis any type (not just a base type). Intuitively, a value has type{T | r}if it has typeTand alsorholds. They can be used to constraint a refinement parameter. For example, the following signature constraint the refinement parameternto be less than10.fn({i32[@n] | n < 10}) -> i32[n + 1]Constraint types serve a similar role as existentials as they can also be used to constraint some refinement value with a predicate, but an existential type can only be used to constraint refinement variable that it bound locally, in contrast constraint types can be used to constraint a "non-local" parameter. This can be seen in the example above where the parameter
ncannot be bound locally because it has to be used in the return type.
Argument Syntax
The @n syntax used to declare refinements parameters can be hard to read sometimes. Flux also supports a syntax that let you bind refinement parameters using colons similar to the syntax used to declare arguments in a function. We call this argument syntax. This syntax desugars to one of the refinements forms discussed above. For example, the following signature
fn(x: i32, y: i32) -> i32[x + y]
desugars to
fn(i32[@x], i32[@y]) -> i32[x + y]
It is also possible to attach some constraint to the parameters when using argument syntax. For example,
to specify that y must be greater than x using argument syntax we can write:
fn(x: i32, y: i32{x > y}) -> i32[x + y]
This will desugar to:
fn(i32[@x], {i32[@y] | x > y}) -> i32[x + y]
Grammar of Refinements
The grammar of refinements (expressions that can appear as an index or constraint) is as follows:
r ::= n // numbers 1,2,3...
| x // identifiers x,y,z...
| x.f // index-field access
| r + r // addition
| r - r // subtraction
| n * e // multiplication by constant
| if r { r } else { r } // if-then-else
| f(r...) // function application
| true | false // booleans
| r == r // equality
| r != r // not equal
| r < r // less than
| r <= r // less than or equal
| r > r // greater than
| r >= r // greater than or equal
| r || r // disjunction
| r && r // conjunction
| r => r // implication
| !r // negation
Index Refinements
Of the form i32[e] (i32 equal to e) values.
#[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.
#[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
#[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
#[flux::sig(fn(x: &mut i32{v: 0 <= v}))]
pub fn test4(x: &mut i32) {
*x += 1;
}#[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
#[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
#[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.
#[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(dead_code)]
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
#[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_attributes)]
#[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
#[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
#[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;
}
}#[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::trusted]
#[flux::sig(fn(x: &[T][@n]) -> usize[n])]
fn len<T>(x: &[T]) -> usize {
x.len()
}
#[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];
i += 1;
}
}
#[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())
}Refined Vec
This uses extern_spec which is described below.
Standalone
#![feature(allocator_api)]
use std::alloc::{Allocator, Global};
use flux_rs::{assert, attrs::*, extern_spec};
#[extern_spec]
#[refined_by(len: int)]
#[invariant(len >= 0)]
struct Vec<T, A: Allocator = Global>;
#[extern_spec]
impl<T> Vec<T> {
#[spec(fn() -> Vec<T>[0])]
fn new() -> Vec<T>;
}
#[extern_spec]
impl<T, A: Allocator> Vec<T, A> {
#[spec(fn(self: &mut Vec<T, A>[@n], T) ensures self: Vec<T, A>[n+1])]
fn push(&mut self, value: T);
#[spec(fn(self: &Vec<T, A>[@n]) -> usize[n])]
fn len(&self) -> usize;
#[spec(fn(self: &Vec<T, A>[@n]) -> bool[n == 0])]
fn is_empty(&self) -> bool;
#[spec(fn(self: &mut Vec<T, A>[@n]) -> Option<T>
ensures self: Vec<T, A>[if n > 0 { n-1 } else { 0 }])]
fn pop(&mut self) -> Option<T>;
}
#[extern_spec]
impl<T> [T] {
#[spec(fn(self: Box<[T][@n], A>) -> Vec<T, A>[n])]
fn into_vec<A>(self: Box<[T], A>) -> Vec<T, A>
where
A: Allocator;
}
#[spec(fn() -> Vec<i32>[3])]
pub fn test_vec_macro() -> Vec<i32> {
vec![10, 20, 30]
}
#[spec(fn() -> Vec<i32>[4])]
pub fn test_push_macro() -> Vec<i32> {
let res = vec![10, 20, 30, 40];
assert(res.len() == 4);
res
}
#[spec(fn() -> Vec<i32>[2])]
pub fn test_push() -> Vec<i32> {
let mut res = Vec::new();
res.push(10);
res.push(20);
res.push(30);
let val = res.pop().unwrap();
assert(val >= 10);
res
}
#[spec(fn() -> usize[2])]
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
// #[spec(fn (Vec<i32{v:10 <= v}>))]
// pub fn test3(xs: Vec<i32>) {
// for x in &xs {
// assert(0 <= *x)
// }
// }
#[spec(fn (vec: &mut Vec<T>[@n]) -> Option<(T, T)>
requires n > 2
ensures vec: Vec<T>[n-2])]
pub fn pop2<T>(vec: &mut Vec<T>) -> Option<(T, T)> {
let v1 = vec.pop().unwrap();
let v2 = vec.pop().unwrap();
Some((v1, v2))
}Associated Refinements for indexing
use std::{
alloc::{Allocator, Global},
ops::{Index, IndexMut},
slice::SliceIndex,
};
use flux_attrs::*;
//---------------------------------------------------------------------------------------
#[extern_spec]
#[refined_by(len: int)]
#[invariant(0 <= len)]
struct Vec<T, A: Allocator = Global>;
//---------------------------------------------------------------------------------------
#[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> {
#[spec(fn(self: &mut Vec<T, A>[@n], T) ensures self: Vec<T, A>[n+1])]
fn push(v: &mut Vec<T, A>, value: T);
#[spec(fn(&Vec<T, A>[@n]) -> usize[n])]
fn len(v: &Vec<T, A>) -> usize;
#[spec(fn(self: &mut Vec<T, A>[@n]) -> Option<T> ensures self: Vec<T, A>[if n > 0 { n-1 } else { 0 }])]
fn pop(&mut self) -> Option<T>;
}
//---------------------------------------------------------------------------------------
#[extern_spec]
impl<T, I: SliceIndex<[T]>, A: Allocator> Index<I> for Vec<T, A> {
#[spec(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]
impl<T, I: SliceIndex<[T]>, A: Allocator> IndexMut<I> for Vec<T, A> {
#[spec(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<'a, T, A: Allocator> IntoIterator for &'a Vec<T, A> {
#[spec(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;
}
#[extern_spec]
#[assoc(fn with_size(self: Self, n:int) -> bool { self.len == n })]
impl<T> FromIterator<T> for Vec<T> {}#![feature(allocator_api)]
use std::ops::Index;
extern crate flux_alloc;
extern crate flux_core;
// ---------------------------------------------------------------------------------------
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.
#[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
#![flux::defs {
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
}#![flux::defs {
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
#[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
// 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
Flux offers an attribute opaque which can be used on structs. A module defining an opaque struct should define a trusted API, and clients of the API should not access struct fields directly. This is particularly useful in cases where users need to define a type indexed by a different type than the structs fields. For example, RMap (see below) defines a refined HashMap, indexed by a Map - a primitive sort defined by flux.
use flux_rs::*;
#[opaque]
#[refined_by(vals: Map<K, V>)]
pub struct RMap<K, V> {
inner: std::collections::HashMap<K, V>,
}Note that opaque structs can not have refined fields.
Now, we can define get for our refined map as follows:
impl<K, V> RMap<K, V> {
#[flux_rs::trusted]
#[flux_rs::sig(fn(&RMap<K, V>[@m], &K[@k]) -> Option<&V[map_select(m.vals, k)]>)]
pub fn get(&self, k: &K) -> Option<&V>
where
K: Eq + Hash,
{
self.inner.get(k)
}
}Note that if we do not mark these methods as trusted, we will get an error that looks like...
error[E0999]: cannot access fields of opaque struct `RMap`.
--> ../opaque.rs:22:9
|
22 | self.inner.get(k)
| ^^^^^^^^^^
-Ztrack-diagnostics: created at crates/flux-refineck/src/lib.rs:111:14
|
help: if you'd like to use fields of `RMap`, try annotating this method with `#[flux::trusted]`
--> ../opaque.rs:18:5
|
18 | / pub fn get(&self, k: &K) -> Option<&V>
19 | | where
20 | | K: Eq + std::hash::Hash,
| |________________________________^
= note: fields of opaque structs can only be accessed inside trusted code
Here is an example of how to use the opaque attribute:
#[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
#[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),
}
}#[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,
}
}
}#[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
#[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
#[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
#[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
#[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
#[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;
}
}#![flux::defs {
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;
}
}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>) {}#![flux::defs {
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.
pub struct Cow {}
impl Cow {
const GRASS: usize = 12;
#[flux_rs::sig(fn () -> usize[12])]
pub fn test() -> usize {
Self::GRASS
}
}#[repr(u32)]
pub enum SyscallReturnVariant {
Failure = 0,
}
#[flux_rs::sig(fn() -> u32[0])]
pub fn test() -> u32 {
SyscallReturnVariant::Failure as u32
}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.
#[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
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);
}Ignored and trusted code
Flux offers two attributes for controlling which parts of your code it analyzes: #[flux_rs::ignore] and #[flux_rs::trusted].
#[flux_rs::ignore]: This attribute is applicable to any item, and it instructs Flux to completely skip some code. Flux won't even look at it.#[flux_rs::trusted]: This attribute affects whether Flux checks the body of a function. If a function is marked as trusted, Flux won't verify its body against its signature. However, it will still be able to reason about its signature when used elsewhere.
The above means that an ignored function can only be called from ignored or trusted code, while a trusted function can also be called from analyzed code.
Both attributes apply recursively. For instance, if a module is marked as #[flux_rs::ignore], all its nested elements will also be ignored. This transitive behavior can be disabled by marking an item with #[flux_rs::ignore(no)]1, which will include all nested elements for analysis. Similarly,
the action of #[flux_rs::trusted] can be reverted using #[flux_rs::trusted(no)].
Consider the following example:
#[flux_rs::ignore]
mod A {
#[flux_rs::ignore(no)]
mod B {
mod C {
fn f1() {}
}
}
mod D {
fn f2() {}
}
fn f3() {}
}In this scenario, functions f2 and f3 will be ignored, while f1 will be analyzed.
A typical pattern when retroactively adding Flux annotations to existing code is to ignore an entire crate (using the inner attribute #![flux_rs::ignore] at the top of the crate) and then selectively include specific sections for analysis.
Here is an example
#![flux::ignore] // default to ignore for the entire crate
#[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.
// 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
// 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
#[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
#[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
- They are connected to an underlying Rust type,
- They may also be parameterized by refinements, e.g.
Lb - There are two different kinds of parametrizations
- early (
Nat) and - late (
Lb).
- early (
#[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
#![flux::defs {
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
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
#![flux::defs {
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.
#![flux::defs {
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
#![flux::defs {
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);
}
}#![flux::defs {
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.
#![flux::defs {
#[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
#[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
// 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
#[flux::alias(type Test = Vec<_>)]
type Test = Vec<i32>;
fn test(x: Test) -> Vec<i32> {
x
}Generic Args
#[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
use flux_rs::attrs::*;
#[trusted]
#[spec(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 })
}
// pub fn test0_buddy(x: i32) -> i32 {
// x + 1
// }
// #[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)
// }#[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)]
#[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)]
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)
}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
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
}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;
}
}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;
}
}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);
}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
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()
}#[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
// 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)
}#[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);
}#[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
// 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) {}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
}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
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
// 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
#![flux::defs(
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
#[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
#[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
Sometimes you may want to refine a struct or function that outside your code. We refer to such a specification as an "extern spec," which is short for "external specification."
Currently, Flux supports extern specs for functions, structs, enums, traits and impls.
The support is a bit rudimentary. For example, multiple impls for a struct (such as &[T]
and [T]) may conflict, and extern specs for structs only support opaque refinements.
Extern specs are given using extern_spec attribute macro, which is provided
by the procedural macros package flux_rs.
use flux_rs::extern_spec;
The extern_spec is used to provide flux signatures for functions defined in external crates. See the specifications guide for more details.
Extern Functions
An example of refining an extern function can be found here.
To define an extern spec on a function, you need to do three things, which happen to correspond to each of the below lines.
#[extern_spec(std::mem)]
#[spec(fn(x: &mut T[@vx], y: &mut T[@vy]) ensures x: T[vy], y: T[vx])]
fn swap<T>(a: &mut T, b: &mut T);- Add the
#[extern_spec]attribute. This attribute optionally takes a path; in the above example, this isstd::mem. You can use this path to qualify the function. So in the above example, the function we are targeting has the full path ofstd::mem::swap. - Add a
#[spec(...)](or equivalently#[flux_rs::sig(...)]) attribute, which is required for any extern spec on a function. This signature behaves as if the#[flux_rs::trusted]attribute was added, because we cannot actually check the implementation. Instead, flux just verifies some simple things, like that the function arguments have compatible types. - Write a function stub whose rust signature matches the external function.
If you do the above, you can use std::mem::swap as if it were refined by the
above type.
Here are two examples:
pub fn test_swap() {
let mut x = 5;
let mut y = 10;
swap(&mut x, &mut y); // actually calls `std::mem::swap`
assert(x == 10); // verified by flux
assert(y == 5); // verified by flux
assert(y == 10); //~ ERROR refinement type
}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
{{#include ../../../tests/tests/lib/option.rs}}use flux_rs::{assert, attrs::*};
extern crate flux_core;
#[flux::trusted]
#[spec(fn(i32{v: false}) -> T)]
pub fn never<T>(_: i32) -> T {
loop {}
}
#[spec(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),
}
}
#[spec(fn(T) -> Option<T>[true])]
fn my_some<T>(x: T) -> Option<T> {
Option::Some(x)
}
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);
}
pub fn test_opt_specs() {
let a = Some(42);
assert(a.is_some());
let b: Option<i32> = None;
assert(b.is_none());
let c = a.unwrap();
assert(c == 42);
}
#[spec(fn (numerator: u32, denominator: u32) -> Option<u32[numerator / denominator]>[denominator != 0])]
pub fn safe_div(numerator: u32, denominator: u32) -> Option<u32> {
if denominator == 0 { None } else { Some(numerator / denominator) }
}
pub fn test_safe_div() {
let res = safe_div(42, 2).unwrap();
assert(res == 21);
}Vec
{{#include ../../../tests/tests/lib/option.rs}}Extern Structs
Here is an example of refining an extern struct
use flux_rs::extern_spec;
#[extern_spec(std::string)]
#[flux::refined_by(len: int)]
struct String;
#[flux::sig(fn(String[@n]) requires n == 3)]
fn expect_string_len_3(s: String) {}
#[flux::sig(fn(String[2]))]
fn test_string_len_2(s: String) {
expect_string_len_3(s); //~ ERROR refinement type
}Here's a longer example of refining an extern struct as well as an impl
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: &mut String[@n], char) ensures s: String[n+1])]
fn push(s: &mut String, c: char);
#[flux::sig(fn(s: &mut 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());
}The syntax for an extern spec on a struct is very similar to that for a function. Once again, each line in the example happens to correspond to a step.
#[extern_spec(std::string)]
#[flux_rs::refined_by(len: int)]
struct String;
- Add the
#[extern_spec]attribute. This attribute optionally takes a path; in the above example, this isstd::string. You can use this path to qualify the function. So in the above example, the struct we are targeting has the full path ofstd::string::String. - Add a
#[flux_rs::refined_by(...)]attribute. This is required for any extern spec on a struct. Right now these attributes behave as if they were opaque (#[flux_rs::opaque]), although we may support non-opaque extern structs. - Write a stub for the extern struct.
If you do the above, you can use std::string::String as if it were refined by
an integer index.
The syntax for an extern impl is a little different than that for functions or structs.
#[extern_spec(std::string)]
impl String {
#[flux_rs::sig(fn() -> String[0])]
fn new() -> String;
#[flux_rs::sig(fn(&String[@n]) -> usize[n])]
fn len(s: &String) -> usize;
}
- You still need to add the
#[extern_spec]attribute, with the same optional argument of the path as above. - You need to write out the
implblock for the struct you want to refine. This struct does not need an extern spec, since by refining theimplyou're only refining its methods. - Write an extern spec for each function you wish to refine (this may be a
subset). This is written just like a function extern spec with the caveat
that the
selfparameter is not presently supported. So for example, instead of writingfn len(&self) -> usize;, you need to writefn len(s: &String) -> usize;.
If you do the above, you can use the above methods ofstd::string::String as if
they were refined.
// 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)]
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());
}// 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()
}Extern Impls
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: &mut String[@n], char) ensures s: String[n+1])]
fn push(s: &mut String, c: char);
#[flux::sig(fn(s: &mut 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());
}//@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()
}Extern Traits
use flux_rs::*;
#[extern_spec(std::cmp)]
#[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:
#![feature(step_trait)]
#![allow(unused)]
extern crate flux_core;
#[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(dead_code)]
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
// 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
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
use flux_rs::*;
#[extern_spec(std::cmp)]
#[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)
}use std::{
alloc::{Allocator, Global},
ops::{Index, IndexMut},
slice::SliceIndex,
};
use flux_attrs::*;
//---------------------------------------------------------------------------------------
#[extern_spec]
#[refined_by(len: int)]
#[invariant(0 <= len)]
struct Vec<T, A: Allocator = Global>;
//---------------------------------------------------------------------------------------
#[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> {
#[spec(fn(self: &mut Vec<T, A>[@n], T) ensures self: Vec<T, A>[n+1])]
fn push(v: &mut Vec<T, A>, value: T);
#[spec(fn(&Vec<T, A>[@n]) -> usize[n])]
fn len(v: &Vec<T, A>) -> usize;
#[spec(fn(self: &mut Vec<T, A>[@n]) -> Option<T> ensures self: Vec<T, A>[if n > 0 { n-1 } else { 0 }])]
fn pop(&mut self) -> Option<T>;
}
//---------------------------------------------------------------------------------------
#[extern_spec]
impl<T, I: SliceIndex<[T]>, A: Allocator> Index<I> for Vec<T, A> {
#[spec(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]
impl<T, I: SliceIndex<[T]>, A: Allocator> IndexMut<I> for Vec<T, A> {
#[spec(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<'a, T, A: Allocator> IntoIterator for &'a Vec<T, A> {
#[spec(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;
}
#[extern_spec]
#[assoc(fn with_size(self: Self, n:int) -> bool { self.len == n })]
impl<T> FromIterator<T> for Vec<T> {}{{#include ../../../tests/tests/lib/iter.rs}}#![allow(unused)]
#![feature(allocator_api)]
use std::{iter::Enumerate, slice::Iter};
extern crate flux_alloc;
extern crate flux_core;
#[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())
}
}
#[flux::sig(fn(&[usize][@n]) )]
pub fn test_enumer4(slice: &[usize]) {
for (idx, _) in slice.iter().enumerate() {
assert(idx < slice.len())
}
}Associated Types
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
}// 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
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
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
}#[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
}
}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
}
}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
}
}Extensible Properties for Primitive Ops
You can provide properties to be used when doing computations with
primitive operations like << or >>.
Given a primop op with signature (t1,...,tn) -> t we define
a refined type for op expressed as a [RuleMatcher]
op :: (x1: t1, ..., xn: tn) -> { t[op_val[op](x1,...,xn)] | op_rel[x1,...,xn] }that is, using two uninterpreted functions op_val and op_rel that respectively denote
- The value of the primop, and
- Some invariant relation that holds for the primop.
The latter can be extended by the user via a property definition,
which allows us to customize primops like << with extra "facts"
or lemmas. See tests/tests/pos/surface/primops00.rs for an example.
use flux_rs::{assert, attrs::*, defs};
defs! {
property ShiftByTwo[<<](x, y) {
[<<](x, 2) == 4*x
}
property ShiftRightByFour[>>](x, y) {
16 * [>>](x, 4) == x
}
property MaskBy[&](x, y) {
[&](x, y) <= y
}
}
pub fn test0() {
let x: usize = 1 << 2;
assert(x == 4);
}
pub fn test1() {
let x = 1;
let x = x << 2;
let x = x << 2;
assert(x == 16)
}
#[spec(fn (x: u32) -> u32[16*x])]
pub fn test2(x: u32) -> u32 {
let x = x << 2;
let x = x << 2;
x
}
#[spec(fn (byte: u8{byte <= 127}))]
pub fn test3(byte: u8) {
let tmp1 = byte >> 4;
let tmp2 = byte & 0xf;
assert(byte <= 127);
assert(tmp1 <= 0xf);
assert(tmp2 <= 0xf);
}
static POW10: [i32; 10] = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9];
pub fn test4(n: usize) -> i32 {
POW10[n & 7]
}Casting Sorts
You can convert refinements of different sorts -- e.g. int to char or int to bool --
using the cast internal function.
#![flux::defs {
fn is_ascii_digit(c: char) -> bool {
let i = cast(c);
48 <= i && i <= 57
}
fn is_ascii(c: char) -> bool {
let i = cast(c);
0 <= i && i <= 127
}
}]
use flux_rs::{assert, attrs::*};
// extern specs for is_ascii and is_ascii_digit
#[extern_spec]
impl char {
#[spec(fn (&Self[@c]) -> bool[is_ascii(c)])]
fn is_ascii(&self) -> bool;
#[spec(fn (&Self[@c]) -> bool[is_ascii_digit(c)])]
fn is_ascii_digit(&self) -> bool;
}
pub fn test_ok(x: char) {
if x.is_ascii_digit() {
assert(x.is_ascii())
}
}
#[spec(fn (char{v: '0' <= v && v <= '9'}))]
pub fn test_digit(x: char) {
assert(x.is_ascii_digit())
}-
#[flux_rs::ignore](resp.#[flux_rs::trusted]) is shorthand for#[flux_rs::ignore(yes)](resp.#[flux_rs::trusted(yes)]). ↩