Flux Specification Guide
This is a WIP guide to writing specifications in flux
.
Refinement Types
-
Indexed Type: An indexed type
B[r]
is composed of a base Rust typeB
and a refinement indexr
. The meaning of the index depends on the type. Some examples arei32[n]
: denotes the (singleton) set ofi32
values 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
@n
syntax. For example, the following signature:fn(i32[@n]) -> i32[n + 1]
binds
n
over the entire scope of the function to specify that it takes ani32
equal ton
and returns ani32
equal 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 -> a
in Haskell is polymorphic on the typea
which 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 variablev
and a refinement predicater
onv
. Intuitively, a Rust valuex
has typeB{v: r(v)}
if there exists a refinement valuea
such thatr(a)
holds andx
has typeB[x]
.i32{v: v > 0}
: set of positivei32
values.List<T>{v: v > 0}
: set of non-empty lists.
-
Constraint Type: A constraint type has the form
{T | r}
whereT
is any type (not just a base type). Intuitively, a value has type{T | r}
if it has typeT
and alsor
holds. They can be used to constraint a refinement parameter. For example, the following signature constraint the refinement parametern
to 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
n
cannot 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]
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."
Flux right now has rudimentary support for extern specs: they are supported for
functions, impls, and structs. Impls are only supported for structs and if you
have multiple impls for a struct (such as &[T]
and [T]
), those may conflict.
Structs only support opaque refinements.
Import the procedural macros
In order to use an extern spec you need to add a dependency on
flux_rs
.
Right now this needs to be done as a local dependency since it is not published.
Below is an example of how you can include it, although the version may be
different.
[dependencies]
flux-rs = { path = "path-to-flux/flux/flux-rs", version = "0.1.0" }
Then in your code you will need to include the extern_spec
attribute macro.
use flux_rs::extern_spec;
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)]
#[flux::sig(fn(&mut i32[@a], &mut i32{v : a < v }) -> ())]
fn swap(a: &mut i32, b: &mut i32);
- 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
#[flux::sig(...)]
attribute. This is required for any extern spec on a function. This signature behaves as if the#[flux::trusted]
attribute was added, because we can't actually check the implementation. We just verify some simple things, like that the function arguments have compatible types. - Write a function stub that matches the external function.
If you do the above, you can use std::mem::swap
as if it were refined by the
above type.
You shouldn't need to know the details, but here's how the macro works. It
parses the std::mem
into a module path and then transforms the function into
#[flux::extern_spec]
#[flux::sig(fn(&mut i32[@a], &mut i32{v : a < v }) -> ())]
#[allow(unused, dead_code)]
fn __flux_extern_spec_swap(a: &mut i32, b: &mut i32) {
std::mem::swap(a, b)
}
It does this to get information about the function std::mem::swap
and its
arguments (this turns out to be difficult to do without giving the compiler
something to inspect and type check).
Extern structs and impls
An example of refining an extern struct and impl can be found here. A simpler example just involving structs can be found here.
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::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::refined_by(...)]
attribute. This is required for any extern spec on a struct. Right now these attributes behave as if they were opaque (#[flux::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::sig(fn() -> String[0])]
fn new() -> String;
#[flux::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
impl
block for the struct you want to refine. This struct does not need an extern spec, since by refining theimpl
you'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
self
parameter 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.
You shouldn't need to know the details, but here's how the above two macros expand.
For structs:
#[flux::extern_spec]
#[allow(unused, dead_code)]
#[flux::refined_by(len: int)]
struct __FluxExternSpecString(std::string::String);
For impls (this was translated manually so there might be some bugs):
#[allow(unused, dead_code)]
struct __FluxExternImplStructString;
#[allow(unused, dead_code)]
impl __FluxExternImplStructString {
#[flux::extern_spec]
#[flux::sig(fn() -> String[0])]
#[allow(unused, dead_code)]
fn __flux_extern_spec_new() -> String {
std::string::String::new::<>()
}
#[flux::extern_spec]
#[flux::sig(fn(&String[@n]) -> usize[n])]
#[allow(unused, dead_code)]
fn __flux_extern_spec_len(s: &String) -> usize {
std::string::String::len::<>(s)
}
}
Grammar of Refinements
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
Ignored and trusted code
Flux offers two attributes for controlling which parts of your code it analyzes: #[flux::ignore]
and #[flux::trusted]
.
#[flux::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::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::ignore]
, all its nested elements will also be ignored. This transitive behavior can be disabled by marking an item with #[flux::ignore(no)]
1, which will include all nested elements for analysis. Similarly,
the action of #[flux::trusted]
can be reverted using #[flux::trusted(no)]
.
Consider the following example:
#![allow(unused)] fn main() { #[flux::ignore] mod A { #[flux::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::ignore]
at the top of the crate) and then selectively include specific sections for analysis.
#[flux::ignore]
(resp. #[flux::trusted]
) is shorthand for #[flux::ignore(yes)]
(resp. #[flux::trusted(yes)]
).