Flux is a refinement type checker plugin for Rust that lets you specify a range of correctness properties and have them be verified at compile time.
Flux works by extending Rust's types with refinements: logical assertions describing additional correctness requirements that are checked during compilation, thereby eliminating various classes of run-time problems.
You can try it on the online playground.
Better still, read the interactive tutorial, to learn how you can use Flux on your Rust code.
Installing and Running Flux
You can install and then run Flux either on a single file or on an entire crate.
Requirements
Be sure that the liquid-fixpoint
and z3
executables are in your $PATH
.
Install
The only way to use Flux is to build it from source.
First you need to clone the repository
git clone https://github.com/flux-rs/flux
cd flux
To build the source you need a nightly version of rustc
.
We pin the version using a toolchain file (more info here).
If you are using rustup
, no special action is needed as it should install the correct rustc
version and components based on the information on that file.
Next, run the following to build and install flux
binaries
cargo xtask install
This will install two binaries flux
and cargo-flux
in your cargo home. These two binaries should be used
respectively to run Flux on either a single file or on a project using cargo. The installation process will
also copy some files to $HOME/.flux
.
In order to use Flux refinement attributes in a Cargo project, you will need to add the following to your Cargo.toml
[dependencies]
flux-rs = { git = "https://github.com/flux-rs/flux.git" }
This will add the procedural macros Flux uses to your project; it is not a substitute for installing Flux, which must still be done.
Running on a File: flux
You can use flux
as you would use rustc
.
For example, the following command checks the file test.rs
.
flux path/to/test.rs
The flux binary accepts the same flags as rustc
.
You could for example check a file as a library instead of a binary like so
flux --crate-type=lib path/to/test.rs
Refinement Annotations on a File
When running flux on a file with flux path/to/test.rs
, refinement annotations should be prefixed with flux::
.
For example, the refinement below will only work when running flux
which is intended for use on a single file.
#![allow(unused)] fn main() { #[flux::sig(fn(x: i32) -> i32{v: x < v})] fn inc(x: i32) -> i32 { x - 1 } }
Running on a package: cargo-flux
See this an
Flux is integrated with cargo
and can be invoked in a package as follows:
cargo flux
By default, Flux won't verify a package unless it's explicitly enabled in the manifest.
To do so add the following to Cargo.toml
:
[package.metadata.flux]
enabled = true
Refinement Annotations on a Cargo Projects
Adding refinement annotations to cargo projects is simple. You can add flux-rs
as a dependency in Cargo.toml
[dependencies]
flux-rs = { git = "https://github.com/flux-rs/flux.git" }
Then, import attributes from flux_rs
and add the appropriate refinement annoations.
#![allow(unused)] fn main() { use flux_rs::*; #[sig(fn(x: i32) -> i32{v: x < v})] fn inc(x: i32) -> i32 { x - 1 } }
A tiny example
The following example declares a function inc
that returns an integer greater than the input.
We use the nightly feature register_tool
to register the flux
tool in order to
add refinement annotations to functions.
#![allow(unused)] fn main() { #[flux::sig(fn(x: i32) -> i32{v: x < v})] pub fn inc(x: i32) -> i32 { x - 1 } }
You can save the above snippet in say test0.rs
and then run
flux --crate-type=lib path/to/test0.rs
you should see in your output
error[FLUX]: postcondition might not hold
--> test0.rs:3:5
|
3 | x - 1
| ^^^^^
as indeed x - 1
is not greater than x
as required by the output refinement i32{v: x < v}
.
If you fix the error by replacing x - 1
with x + 1
, you should get no errors
in the output (the output may be empty, but in this case no output is a good
thing).
Read these chapters to learn more about what you specify and verify with flux
.
A note about the flux-driver binary
The flux-driver
binary is a rustc
driver
(similar to how clippy works) meaning it uses rustc as a library to "drive"
compilation performing additional analysis along the way. Running the binary
requires dynamically linking a correct version of librustc
. Thus, to avoid the
hassle you should never execute it directly. Instead, use flux
or cargo-flux
.
Editor Support
This section assumes you have installed cargo-flux
.
Rust-Analyzer in VSCode
Add this to the workspace settings i.e. .vscode/settings.json
{
"rust-analyzer.check.overrideCommand": [
"cargo",
"flux",
"--workspace",
"--message-format=json-diagnostic-rendered-ansi"
]
}
Note: Make sure to edit the paths in the above snippet to point to the correct locations on your machine.
Configuration
Flux Flags
The flux
binary accepts configuration flags in the format -Fname=value
. For boolean flags, the
value
can be one of y
, yes
, on
, true
, n
, no
, off
, false
. Alternatively, the value
can be omitted which will default to true
. For example, to set the solver to cvc5
and enable
qualifier scrapping:
flux -Fsolver=cvc5 -Fscrape-quals path/to/file.rs
For all available flags, see https://flux-rs.github.io/flux/doc/flux_config/flags/struct.Flags.html
Cargo Projects
When working with a Cargo project, some of the flags can be configured in the
[package.metadata.flux]
table in Cargo.toml
. For example, to enable query caching and set
cvc5
as the solver:
# Cargo.toml
[package.metadata.flux]
enabled = true
cache = true
solver = "cvc5"
Additionally, cargo flux
searches for a configuration file called flux.toml
with the same format
as the metadata table. The content of flux.toml
takes precedence and it's merged with the
content of the metadata
table. Note that the content of flux.toml
will override the metadata
for all crates, including dependencies. This behavior is likely to change in the future as we figure
out what configurations make sense to have per package and which should only affect the current execution
of cargo flux
.
You can see the format of the metadata
in https://flux-rs.github.io/flux/doc/flux_bin/struct.FluxMetadata.html.
FLUXFLAGS
Environement Variable
When running cargo flux
, flags defined in FLUXFLAGS
will be passed to all flux
invocations,
for example, to print timing information for all crates checked by Flux:
FLUXFLAGS="-Ftimings" cargo flux
About Flux
Team
Flux is being developed by
Code
Flux is open-source and available here
Publications
- Lehmann, Nico, Adam T. Geller, Niki Vazou, and Ranjit Jhala. "Flux: Liquid types for rust." PLDI (2023)
- Lehmann, Nico, Cole Kurashige, Nikhil Akiti, Niroop Krishnakumar, and Ranjit Jhala. "Generic Refinement Types." POPL (2025)
Talks
Thanks
This work was supported by the National Science Foundation, European Research Council, and by generous gifts from Microsoft Research.
Limitations
This is a prototype! Use at your own risk. Everything could break and it will break.
Refining Types
Types bring order to code. For example, if a variable i:usize
then we know i
is a number that can be used to index a vector.
Similarly, if v: Vec<&str>
then we can be sure that v
is a
collection of strings which may be indexed but of course,
not used as an index. However, by itself usize
doesn't
tell us how big or small the number and hence the programmer
must still rely on their own wits, a lot of tests, and a dash
of optimism, to ensure that all the different bits fit properly
at run-time.
Refinements are a promising new way to extend type checkers with logical constraints that specify additional correctness requirements that can be verified by the compiler, thereby entirely eliminating various classes of run-time problems.
To begin, lets see how flux lets you refine basic or primitive
types like i32
or usize
or bool
with logical constraints that
can be checked at compile time.
Indexed Types
The simplest kind of refinement type in flux is a type that is indexed by a logical value. For example
Type | Meaning |
---|---|
i32[10] | The (singleton) set of i32 values equal to 10 |
bool[true] | The (singleton) set of bool values equal to true |
Flux Specifications
First off, we need to add some incantations that pull in the mechanisms for writing flux specifications as Rust attributes.
#![allow(unused)] extern crate flux_rs; use flux_rs::attrs::*;
Post-Conditions
We can already start using these indexed types to start writing (and checking)
code. For example, we can write the following specification which says that
the value returned by mk_ten
must in fact be 10
#[spec(fn() -> i32[10])] pub fn mk_ten() -> i32 { 5 + 4 }
Push Play Push the "run" button in the pane above. You will see a red squiggle that and when you hover over the squiggle you will see an error message
error[...]: refinement type error
|
7 | 5 + 4
| ^^^^^ a postcondition cannot be proved
which says that that the postcondition might not hold which means
that the output produced by mk_ten
may not in fact be an i32[10]
as indeed, in this case, the result is 9
! You can eliminate the error
by editing the body to 5 + 4 + 1
or 5 + 5
or just 10
.
Pre-Conditions
You can use an index to restrict the inputs that a function expects to be called with.
#[spec(fn (b:bool[true]))] pub fn assert(b:bool) { if !b { panic!("assertion failed") } }
The specification for assert
says you can only call
it with true
as the input. So if you write
fn test(){ assert(2 + 2 == 4); assert(2 + 2 == 5); // fails to type check }
then flux
will complain that
error[FLUX]: precondition might not hold
|
12 | assert(2 + 2 == 5); // fails to type check
| ^^^^^^^^^^^^^^^^^^
meaning at the second call to assert
the input may not
be true
, as of course, in this case, it is not!
Can you edit the code of test
to fix the error?
Index Parameters and Expressions
Its not terribly exciting to only talk about fixed values
like 10
or true
. To be more useful, flux
lets you index
types by refinement parameters. For example, you can write
#[spec(fn(n:i32) -> bool[0 < n])] pub fn is_pos(n: i32) -> bool { if 0 < n { true } else { false } }
Here, the type says that is_pos
- takes as input some
i32
indexed byn
- returns as output the
bool
indexed by0 < n
That is, is_pos
returns true
exactly when 0 < n
.
We might use this function to check that:
pub fn test_pos(n: i32) { let m = if is_pos(n) { n - 1 } else { 0 }; assert(0 <= m); }
Existential Types
Often we don't care about the exact value of a thing -- but just
care about some properties that it may have. For example, we don't
care that an i32
is equal to 5
or 10
or n
but that it is
non-negative.
Type | Meaning |
---|---|
i32{v: 0 < v} | The set of i32 values that positive |
i32{v: n <= v} | The set of i32 values greater than or equal to n |
Flux allows such specifications by pairing plain Rust types with assertions 1 that constrain the value.
Existential Output Types
For example, we can rewrite mk_10
with the output type
i32{v:0<v}
that specifies a weaker property:
the value returned by mk_ten_pos
is positive.
#[spec(fn() -> i32{v: 0 < v})] pub fn mk_ten_pos() -> i32 { 5 + 5 }
Example: abs
olute value
Similarly, you might specify that a function that computes the absolute
value of an i32
with a type which says the result is non-negative and
exceeds the input n
.
#[spec(fn (n:i32) -> i32{v:0<=v && n<=v})] pub fn abs(n: i32) -> i32 { if 0 <= n { n } else { 0 - n } }
Combining Indexes and Constraints
Sometimes, we want to combine indexes and constraints in a specification.
For example, suppose we have some code that manipulates
scores which are required to be between 0
and 100
.
Now, suppose we want to write a function that adds k
points to a score s
. We want to specify that
- The inputs
s
andk
must be non-negative, - the inputs
s + k <= 100
, and - The output equals
s + k
#[spec(fn ({usize[@s] | s + k <= 100}, k:usize) -> usize[s + k])] fn add_points(s: usize, k: usize) -> usize { s + k } fn test_add_points() { assert(add_points(20, 30) == 50); assert(add_points(90, 30) == 120); // fails to type check }
Note that we use the @s
to index the value of the s
parameter,
so that we can
- constrain the inputs to
s + k <= 100
, and - refine the value of the output to be exactly
usize[s + k]
.
EXERCISE Why does flux reject the second call to add_points
?
Example: factorial
As a last example, you might write a function to compute the factorial of n
#[spec(fn (n:i32) -> i32{v:1<=v && n<=v})] pub fn factorial(n: i32) -> i32 { let mut i = 0; let mut res = 1; while i < n { i += 1; res = res * i; } res }
Here the specification says the input must be non-negative, and the
output is at least as large as the input. Note, that unlike the previous
examples, here we're actually changing the values of i
and res
.
Summary
In this post, we saw how Flux lets you
-
decorate basic Rust types like
i32
andbool
with indices and constraints that let you respectively refine the sets of values that inhabit that type, and -
specify contracts on functions that state pre-conditions on the sets of legal inputs that they accept, and post-conditions that describe the outputs that they produce.
The whole point of Rust, of course, is to allow for efficient imperative sharing and updates, without sacrificing thread- or memory-safety. Next time, we'll see how Flux melds refinements and Rust's ownership to make refinements happily coexist with imperative code.
-
These are not arbitrary Rust expressions but a subset of expressions from logics that can be efficiently decided by SMT Solvers ↩
Ownership in Flux
Previously we saw how to refine basic Rust
types like i32
and bool
with indices and constraints to
constrain the set of values described by those types. For instance, we
wrote the function assert
function which can only be called with true
#[flux_rs::spec(fn (bool[true]))] fn assert(b: bool) { if !b { panic!("assertion failed"); } } fn test_assert() { assert(2 + 2 == 4); assert(2 + 2 == 5); // fails to type check }
The whole point of Rust, of course, is to allow for efficient imperative sharing and updates, via the clever type system that keeps an eye on the ownership of resources to make sure that aliasing and mutation cannot happen at the same time.
Next, lets see how Flux melds refinements and Rust's ownership mechanisms to make refinements pleasant in the imperative setting.
Exclusive Ownership
Rust's most basic form of sharing is exclusive ownership,
in which exactly one variable in a function has the right to
mutate a memory location. When a location is exclusively
owned, we can be sure that there are no other references
to it. Consequently, flux
can update the type to precisely
track the value whenever the location is changed.
For example, consider the program
#[flux_rs::spec(fn () -> i32[3])] pub fn mk_three() -> i32 { let mut r = 0; // r: i32[0] r += 1; assert(r == 1); // r: i32[1] r += 1; assert(r == 2); // r: i32[2] r += 1; assert(r == 3); // r: i32[3] r }
The variable r
has different types at each point inside mk_three
.
It starts off as i32[0]
. The first increment changes it to i32[1]
,
then i32[2]
and finally, the returned type i32[3]
.
Exclusive Ownership and Loops
This exclusive ownership mechanism is at work in the factorial
example
we signed off with previously
#[flux_rs::spec(fn (n:i32{0 <= n}) -> i32{v:n <= v})] pub fn factorial(n: i32) -> i32 { let mut i = 0; // i: i32[0] let mut r = 1; // r: i32[1] while i < n { // i: i32{v:0 <= v <= n} // r: i32{v:1 <= v && i <= v} i += 1; r = r * i; } r }
In the above code, i
and r
start off at 0
and 1
but then
flux infers (a story for another day) that inside the while
-loop1
i
has typei32{v:0<=v && v < n}
r
has typei32{v:1<=v && i <= v}
and hence, upon exit since i == n
we get that the result is at least n
.
Borrowing: Shared References
Exclusive ownership suffices for simple local updates
like in factorial
. However, for more complex data,
functions must temporarily relinquish ownership to
allow other functions to mutate the data.
Rust cleverly allows this via the notion of borrowing using two kinds of references that give callee functions temporary access to memory location.
The simplest kind of references are &T
which denote read-only access to a value
of type T
. For example, we might write abs
to take
a shared reference to an i32
#[flux_rs::spec(fn (p: &i32[@n]) -> i32{v:0<=v && n<=v})] pub fn abs(p: &i32) -> i32 { let n = *p; if 0 <= n { n } else { 0 - n } }
Notice that the input type has changed. Now, the function
- accepts
p
, a reference to ani32
whose value isn
as denoted by@n
- returns an
i32
that is non-negative and larger thann
The @
marks the n
as a refinement parameter whose value
is automatically computed by flux during type checking.
Calling abs
with a reference
So, for example, Flux can check the below code by automatically
determining that the refinement parameter at the call-site is 10
.
pub fn test_abs() { let z = 10; assert(0 <= abs(&z)); assert(10 <= abs(&z)) }
Refinement Parameters
As an aside, we have secretly been using refinement parameters
like @n
all along. For example, Flux automatically desugars
the signature fn(n:i32{0 <= n} -> ...
that we wrote for factorial
into
fn ({i32[@n] : 0 <= n}) -> i32{v:n <= v}
where @n
is a refinement parameter that is implicitly determined
from the rust parameter n:i32
. However, explicit parameters are
essential to name the value of what a reference points to.
In abs
the rust
parameter p
names the reference but the
@n
names the (input) value and lets us use it to provide
more information about the output of abs
.
EXERCISE Flux is modular in that the
only information it knows about the
implementation of abs
is the signature.
For example, suppose we change the output type
of abs
to i32{v:0<=v}
, that is, we remove the
n <= v
conjunct. Can you predict which assert
will be rejected by flux?
Borrowing: Mutable References
References of type &mut T
denote mutable references that can be
used to (read and) write or update the contents of a T
value.
Crucially, Rust ensures that while there may be multiple read-only (shared)
references to a location, there is at most one active writeable (mutable)
reference at any point in time.
Flux exploits the semantics of &mut T
to treat T
as an invariant
of the underlying data. As an example, consider the following function
that decrements the value of a mutable reference while ensuring the
data is non-negative:
#[flux_rs::spec(fn(p: &mut i32{v:0 <= v}))] pub fn decr(p: &mut i32) { *p = *p - 1; }
Flux complains that
error[FLUX]: assignment might be unsafe
|
13 | *p = *p - 1;
| ^^^^^^^^^^^
as in fact, we may be writing a negative value into *p
for example, if the old value was zero. We can fix this
code by guarding the update with a test that ensures the
original contents are in fact non-zero
EXERCISE Can you modify the code for decr
so that flux verifies it?
Aliased References
Flux uses Rust's borrowing rules to track invariants even when there may be aliasing. As an example, consider the function
#[flux_rs::spec(fn (bool) -> i32{v:0 <= v})] fn test_alias(z: bool) -> i32 { let mut x = 1; // x: i32[1] let mut y = 2; // y: i32[2] let r = if z { &mut x } else { &mut y }; // r: &mut i32{v:0 <= v} decr(r); *r }
The reference r
could point to either x
or y
depending
on the (unknown) value of the boolean z
. Nevertheless, Flux
determines that both references &mut x
and &mut y
point
to values of the more general type i32{v:0<=v}
and hence,
infers r : &mut i32{v:0<=v}
which allows us it to then call
decr
with the reference and guarantee the result (after decr
)
is still non-negative.
Invariants are not enough!
In many situations, we want to lend a value to another function
that actually changes the value's (refinement) type upon exit.
For example, consider the following function to increment
a reference to a non-negative i32
#[flux_rs::spec(fn (p: &mut i32{v:0 <= v}))] fn incr_inv(p: &mut i32) { *p += 1 } fn test_incr_inv() { let mut z = 10; incr_inv(&mut z); assert(z == 11); }
The only information that flux
has about incr
what
it says in its spec
, namely, that p
remains non-negative.
Flux is blissfully unaware that incr
increments
the value of p
, and it cannot prove that after the
call, z == 11
and hence, complains that assert
may fail even though it will obviously succeed!
Borrowing: Updatable References
To verify test_incr
we need a signature for incr
that says
that its output is indeed one greater2 than its input.
Flux extends Rust &mut T
with the notion of updatable references
which additionally specify how the type is changed when
the function exits3, using an ensures
clause that specifies
the modified type of the reference.
#[flux_rs::spec(fn(p: &mut i32[@n]) ensures p:i32[n+1])] fn incr(p: &mut i32) { *p += 1 }
The Flux signature refines the plain Rust one to specify that
p
is a strong reference to ani32
,- the input type of
*p
isi32[n]
, and - the output type of
*p
isi32[n+1]
.
With this specification, Flux merrily checks test_incr
, by
determining that the refinement parameter @n
is 10
and
hence, that upon return x: i32[11]
.
fn test_incr() { let mut z = 10; incr_inv(&mut z); assert(z == 11); }
Summary
To sum up, Flux exploits Rust's ownership mechanisms
to track properties of shared (&T
) and mutable
(&mut T
) references, and additionally uses (ensures
)
clauses to specify when the type itself is changed by a call.
-
For those familiar with the term, these types are loop invariants ↩
-
Setting aside the issue of overflows for now ↩
-
Thereby allowing so-called strong updates in the type specifications ↩
Refining Structs
Previously, we saw how to slap refinements on existing built-in or primitive Rust types. For example,
i32[10]
specifies thei32
that is exactly equal to10
andi32{v: 0 <= v && v < 10}
specifies ani32
between0
and10
.
Next, lets see how to attach refinements to user-defined types, so we can precisely define the set of legal values of those types.
Positive Integers
Lets start with an example posted on the flux gitHub:
how do you create a Positivei32? I can think of two ways:
struct Positivei32 { val: i32, }
and structPositivei32(i32);
but I do not know how to apply the refinements for them. I want it to be an invariant that the i32 value is >= 0. How would I do this?
With flux, you can define the Positivei32
type as follows:
#[refined_by(n: int)] #[invariant(n > 0)] struct Positivei32 { #[field(i32[n])] val: i32 }
In addition to defining the plain Rust type Positivei32
,
the flux refinements say three distinct things.
- The
refined_by(n: int)
tells flux to refine eachPositivei32
with a specialint
-sorted index namedn
, - the
invariant(n > 0)
says that the indexn
is always positive, and, - the
field
attribute onval
says that the type of the fieldval
is ani32[n]
i.e. is ani32
whose exact value isn
.
Creating Positive Integers
Now, you would create a Positivei32
pretty much as you might in Rust:
#[spec(fn() -> Positivei32)] fn mk_positive_1() -> Positivei32 { Positivei32 { val: 1 } }
and flux will prevent you from creating an illegal Positivei32
, like
#[spec(fn() -> Positivei32)] fn mk_positive_0() -> Positivei32 { Positivei32 { val: 0 } }
A Constructor
EXERCISE Consider the following new
constructor for Positivei32
. Why does flux reject it?
Can you figure out how to fix the spec
for the constructor so flux will be appeased?
impl Positivei32 { pub fn new(val: i32) -> Self { Positivei32 { val } } }
A "Smart" Constructor
EXERCISE Here is a different, constructor that should work
for any input n
but which may return None
if the input is
invalid. Can you fix the code so that flux accepts new_opt
?
impl Positivei32 { pub fn new_opt(val: i32) -> Option<Self> { Some(Positivei32 { val }) } }
Tracking the Field Value
In addition to letting us constrain the underlying i32
to be positive,
the n: int
index lets flux precisely track the value of the Positivei32
.
For example, we can say that the following function returns a very specific Positivei32
:
#[spec(fn() -> Positivei32[{n:10}])] fn mk_positive_10() -> Positivei32 { Positivei32 { val: 10 } }
(When there is a single index, we can just write Positivei32[10]
.)
Since the field val
corresponds to the tracked index,
flux "knows" what val
is from the index, and hence lets us check that
#[spec(fn() -> i32[10])] fn test_ten() -> i32 { let p = mk_positive_10(); // p : Positivei32[{n: 10}] let res = p.val; // res : i32[10] res }
Tracking the Value in the Constructor
EXERCISE Scroll back up, and modify the spec
for new
so that the below code verifies. That is, modify the spec
so that it says what the value of val
is when new
returns
a Positivei32
. You will likely need to combine indexes
and constraints as shown in the example add_points
.
#[spec(fn() -> i32[99])] fn test_new() -> i32 { let p = Positivei32::new(99); let res = p.val; res }
Field vs. Index?
At this point, you might be wondering why, since n
is the value of the field val
,
we didn't just name the index val
instead of n
?
Indeed, we could have named it val
.
However, we picked a different name to emphasize that the index is distinct from the field. The field actually exists at run-time, but in contrast, the index is a type-level property that only lives at compile-time.
Integers in a Range
Of course, once we can index and constrain a single field, we can do so for many fields.
For instance, suppose we wanted to write a Range
type with two fields start
and end
which are integers such that start <= end
. We might do so as
#[refined_by(start: int, end: int)] #[invariant(start <= end)] struct Range { #[field(i32[start])] start: i32, #[field(i32[end])] end: i32, }
Note that this time around, we're using the same names for the index as the field names (even though they are conceptually distinct things).
Legal Ranges
Again, the refined struct
specification will ensure we only create legal Range
values.
fn test_range() { vec![ Range { start: 0, end: 10 }, // ok Range { start: 15, end: 5 }, // rejected! ]; }
A Range Constructor
EXERCISE Fix the specification of the new
constructor for Range
so that both new
and
test_range_new
are accepted by flux. (Again,
you will need to combine indexes and constraints
as shown in the example add_points
.)
impl Range { pub fn new(start: i32, end: i32) -> Self { Range { start, end } } } #[spec(fn() -> Range[{start: 0, end: 10}])] fn test_range_new() -> Range { let rng = Range::new(0, 10); assert(rng.start == 0); assert(rng.end == 10); rng }
Combining Ranges
Lets write a function that computes the union of two ranges.
For example, given the range from 10-20
and 15-25
, we might
want to return the the union is 10-25
.
fn min(x:i32, y:i32) -> i32 { if x < y { x } else { y } } fn max(x:i32, y:i32) -> i32 { if x < y { y } else { x } } fn union(r1: Range, r2: Range) -> Range { let start = min(r1.start, r2.start); let end = max(r2.end, r2.end); Range { start, end } }
EXERCISE Can you figure out how to fix the spec
for min
and max
so that flux will accept that union
only constructs legal Range
values?
Refinement Functions
When code get's more complicated, we like to abstract it into reusable
functions. Flux lets us do the same for refinements too. For example, we
can define refinement-level functions min
and max
which take int
(not i32
or usize
but logical int
) as input and return that as output.
defs! { fn min(x: int, y: int) -> int { if x < y { x } else { y } } fn max(x: int, y: int) -> int { if x < y { y } else { x } } }
We can now use refinement functions like min
and max
inside types.
For example, the output type of decr
precisely tracks the decremented value.
impl Positivei32 { #[spec(fn(&Self[@p]) -> Self[max(1, p.n - 1)])] fn decr(&self) -> Self { let val = if self.val > 1 { self.val - 1 } else { self.val }; Positivei32 { val } } } fn test_decr() { let p = Positivei32{val: 2}; // p : Positivei32[2] assert(p.val == 2); let p = p.decr(); // p : Positivei32[1] assert(p.val == 1); let p = p.decr(); // p : Positivei32[1] assert(p.val == 1); }
Combining Ranges, Precisely
EXERCISE The union
function that we wrote
above says some Range
is returned, but nothing
about what that range actually is! Fix the spec
for union
below, so that flux accepts test_union
below.
impl Range { #[spec(fn(&Self[@r1], &Self[@r2]) -> Self)] pub fn union(&self, other: &Range) -> Range { let start = if self.start < other.start { self.start } else { other.start }; let end = if self.end < other.end { other.end } else { self.end }; Range { start, end } } } fn test_union() { let r1 = Range { start: 10, end: 20 }; let r2 = Range { start: 15, end: 25 }; let r3 = r1.union(&r2); assert(r3.start == 10); assert(r3.end == 25); }
Summary
To conclude, we saw how you can use flux to refine user-defined struct
to track,
at the type-level, the values of fields, and to then constrain the sets of legal
values for those structs.
To see a more entertaining example, check out this code
which shows how we can use refinements to ensure that only legal Date
s can be constructed
at compile time!
Refining Enums
Previously we saw how to refine structs to constrain the space
of legal values, for example, to define a Positivei32
or a Range
struct
where
the start
was less than or equal to the end
. Next, lets see how the same mechanism
can be profitably used to let us check properties of enums
at compile time.
Failure is an Option
Rust's type system is really terrific for spotting all manner of bugs at compile time. However, that just makes it all the more disheartening to get runtime errors like
thread ... panicked at ... called `Option::unwrap()` on a `None` value
Lets see how to refine enum
's like Option
to
let us unwrap
without the anxiety of run-time failure.
A Refined Option
To do so, lets define a custom Option
type 1 that
is indexed by a bool
which indicates whether or not
the option is valid (i.e. Some
or None
):
#[refined_by(valid: bool)] enum Option<T> { #[variant((T) -> Option<T>[{valid: true}])] Some(T), #[variant(Option<T>[{valid: false}])] None, }
As with std::option::Option
, we have two variants
Some
, with the "payload"T
andNone
, without.
However, we have tricked out the type in two ways.
- First, we added a
bool
sorted index that aims to track whether the option isvalid
; - Second, we used the
variant
attribute to specify the value of the index for theSome
andNone
cases.
Constructing Options
The definition above tells flux that Some(...)
has the refined type Option<...>[{valid: true}]
,
and None
has the refined type Option<...>[{valid: false}]
.
NOTE When there is a single refinement index, we can skip the {valid:b}
and just write b
.
#[spec(fn () -> Option<i32>[true])] fn test_some() -> Option<i32> { Option::Some(12) } #[spec(fn () -> Option<i32>[false])] fn test_none() -> Option<i32> { Option::None }
Destructing Options by Pattern Matching
The neat thing about refining variants is that pattern matching
on the enum
tells flux what the variant's refinements are.
For example, consider the following implementation of is_some
impl<T> Option<T> { #[spec(fn(&Self[@valid]) -> bool[valid])] pub fn is_some(&self) -> bool { match self { Option::Some(_) => true, // self : &Option<..>[true] Option::None => false, // self : &Option<..>[false] } } }
Never Do This!
When working with Option
types, or more generally,
with enum
s, we often have situations in pattern-match
cases where we "know" that that case will not arise.
Typically we mark those cases with an unreachable!()
call.
With flux, we can do even more: we can prove, at compile-time, that those cases will never, in fact, be executed.
#[spec(fn () -> _ requires false)] fn unreachable() -> ! { assert(false); // flux will prove this is unreachable unreachable!(); // panic if we ever get here }
The precondition false
ensures that the only way that
a call to unreachable
can be verified is when flux can prove
that the call-site is "dead code".
fn test_unreachable(n: usize) { let x = 12; // x : usize[12] let x = 12 + n; // x : usize[12 + n] where 0 <= n if x < 12 { unreachable(); // impossible, as x >= 12 } }
Unwrap Without Anxiety!
Lets use our refined Option
to implement a safe unwrap
function.
impl <T> Option<T> { #[spec(fn(Self[true]) -> T)] pub fn unwrap(self) -> T { match self { Option::Some(v) => v, Option::None => unreachable(), } } }
The spec
requires that unwrap
is only called
with an Option
whose (valid
) index is true
,
i.e. Some(...)
.
The None
pattern is matched only when the index
is false
which is impossible, as it contradicts
the precondition.
Hence, flux concludes that pattern is dead code
(like the x < 12
branch is dead code in the
test_unreachable
above.)
Using unwrap
Next, lets see some examples of how to use refined options
to safely unwrap
.
Safe Division
Here's a safe divide-by-zero function that returns an Option<i32>
:
#[spec(fn(n:i32, k:i32) -> Option<i32>)] pub fn safe_divide(n: i32, k: i32) -> Option<i32> { if k > 0 { Option::Some(n / k) } else { Option::None } }
EXERCISE Why does the test below fail to type check?
Can you fix the spec
for safe_divide
so flux is happy
with test_safe_divide
?
fn test_safe_divide() -> i32 { safe_divide(10, 2).unwrap() }
Smart Constructors Revisited
Recall the struct Positivei32
and the smart constructor we wrote for it.
#[refined_by(n: int)] #[invariant(n > 0)] struct Positivei32 { #[field(i32[n])] val: i32 } impl Positivei32 { #[spec(fn(val: i32) -> Option<Self>)] pub fn new(val: i32) -> Option<Self> { if val > 0 { Option::Some(Positivei32 { val }) } else { Option::None } } }
EXERCISE The code below has a function that
invokes the smart constructor and then unwrap
s
the result. Why is flux complaining? Can you fix
the spec
of new
so that the test_unwrap
figure
out how to fix the spec
of new
so that test_new_unwrap
is accepted?
fn test_new_unwrap() { Positivei32::new(10).unwrap(); }
TypeStates: A Refined Timer
Lets look a different way to use refined enum
s.
On the flux zulip we were asked
if we could write an enum
to represent a Timer
with two variants:
Inactive
indicating that the timer is not running, andCountDown(n)
indicating that the timer is counting down fromn
seconds.
Somehow using refinements to ensure that the timer can only
be set to Inactive
when n < 1
.
Refined Timers
To do so, lets define the Timer
, refined with an int
index that tracks
the number of remaining seconds.
#[flux::refined_by(remaining: int)] enum Timer { #[flux::variant(Timer[0])] Inactive, #[flux::variant((usize[@n]) -> Timer[n])] CountDown(usize) }
The flux definitions ensure that Timer
has two variants
Inactive
, which has aremaining
index of0
, andCountDown(n)
, which has aremaining
index ofn
.
Timer Implementation
We can now implement the Timer
with a constructor and a method to set it to Inactive
.
impl Timer { #[spec(fn (n: usize) -> Timer[n])] pub fn new(n: usize) -> Self { Timer::CountDown(n) } #[spec(fn (self: &mut Self[0]))] fn deactivate(&mut self) { *self = Timer::Inactive } }
Deactivate the Timer
Now, you can see that flux will only let us set_inactive
a timer whose countdown is at 0
.
#![allow(unused)] fn main() { fn test_deactivate() { let mut t0 = Timer::new(0); t0.deactivate(); // verifies let mut t3 = Timer::new(3); t3.deactivate(); // rejected } }
Ticking the Timer
Here is a function to tick
the timer down by one second.
impl Timer { #[spec(fn (self: &mut Self[@s]) ensures self: Self)] fn tick(&mut self) { match self { Timer::CountDown(s) => { let n = *s; if n > 0 { *s = n - 1; } } Timer::Inactive => {}, } } }
EXERCISE Can you fix the spec
for tick
so that flux accepts the following test?
fn test_tick() { let mut t = Timer::new(3); t.tick(); // should decrement to 2 t.tick(); // should decrement to 1 t.tick(); // should decrement to 0 t.deactivate(); // should set to Inactive }
Summary
In this chapter, we saw how you refine an enum
with indices, and then specify
the values of the indices for each variant
. This let us, for example, determine
whether an Option
is Some
or None
at compile time, and to safely unwrap
the former, and to encode a "typestate" mechanism for a Timer
that tracks how
many seconds remain in a countdown, ensuring we only deactivate
when the timer
has expired.
You can do various other fun things, like
- track the length of a linked list or
- track the set of elements in the list, or
- determine whether an expression is in normal form, or
- ensure the layers of a neural network are composed correctly.
-
In the chapter on extern specifications we will explain how to "retrofit" these refinements onto the existing
std::option::Option
type. ↩
Opaque Types: Refined Vectors
While rustc
has a keen eye for spotting nasty bugs at
compile time, it is not omniscient. We've all groaned in
dismay at seeing deployed code crash with messages like
panicked at 'index out of bounds: the len is ... but the index is ...'
Next, lets see how flux's refinement and ownership mechanisms let us write a refined vector API whose types track vector sizes and ensure --- at compile time --- that vector accesses cannot fail at runtime.
Refining Vectors ...
To track sizes, lets define a struct
that
is just a wrapper around the std::vec::Vec
type, but with a refinement index that tracks
the size of the vector.
#[opaque] #[refined_by(len: int)] pub struct RVec<T> { inner: Vec<T>, }
... to Track their Size
As with other structs we're using refined_by
to index the RVec
with an int
value (that will represent
the vector's length.)
The idea is that
RVec<i32>[10]
represents a vector ofi32
size 10, andRVec<bool>{v:0 < v}
represents a non-empty vector ofbool
, andRVec<RVec<f32>[n]>[m]
represents a vector of vectors off32
of sizem
and each of whose elements is a vector of sizen
.
... but Opaquely
The opaque
attribute tells flux that we're not
going to directly connect the len
to any of
the RVec
's fields' values.
This is quite unlike Positivei32
example
where the index held the actual value of the field,
or the [Timer
example)(./04-enums.md) where the
index held the value of the countdown.
Instead, with an opaque struct
the idea is that the value
of the index will be tracked solely by the API for that struct.
Next, lets see how to build such an API for creating and
manipulating RVec
, where the length is precisely tracked
in the index.
Creating Vectors
I suppose one must start with nothing: the empty vector.
#[trusted] impl<T> RVec<T> { #[spec(fn() -> RVec<T>[0])] pub fn new() -> Self { Self { inner: Vec::new() } } }
The above implements RVec::new
as a wrapper around Vec::new
.
The #[trusted]
attribute tells flux to not check this code,
i.e. to simply trust that the specification is correct.
Indeed, flux cannot check this code.
If you remove the #trusted
(do it!) then flux will
complain that you cannot access the inner
field
of the opaque struct
!
So the only way to use an RVec
is to define a "trusted" API,
and then use that in client code, where for example, callers
of RVec::new
get back an RVec
indexed with 0
: the empty vector.
Pushing Values
An empty vector is a rather desolate thing.
To be of any use, we need to be able to push
values into it, like so
#[trusted] impl<T> RVec<T> { #[spec(fn(self: &mut RVec<T>[@n], T) ensures self: RVec<T>[n+1])] pub fn push(&mut self, item: T) { self.inner.push(item); } }
The refined type for push
says that it takes a updatable reference to an RVec<T>
of size n
and, a value T
and ensures that upon return, the size of self
is increased by 1
.
Creating a Vector with push
Lets test that the types are in fact tracking sizes.
#[spec(fn () -> RVec<i32>[3])] fn test_push() -> RVec<i32> { let mut v = RVec::new(); // v: RVec<i32>[0] v.push(1); // v: RVec<i32>[1] v.push(2); // v: RVec<i32>[2] v.push(3); // v: RVec<i32>[3] v }
EXERCISE: Can you correctly implement the code
for zeros
so that it typechecks?
#[spec(fn(n: usize) -> RVec<i32>[n])] fn zeros(n:usize) -> RVec<i32> { let mut v = RVec::new(); // v: RVec<i32>[0] let mut i = 0; while i <= n { v.push(0); // v: RVec<i32>[i] i += 1; } v }
Popping Values
Not much point stuffing things into a vector if we can't get them out again.
For that, we might implement a pop
method that returns the last element
of the vector.
Aha, but what if the vector is empty? You could return an
Option<T>
or since we're tracking sizes, we could
require that pop
only be called with non-empty vectors.
#[trusted] impl<T> RVec<T> { #[spec(fn(self: &mut {RVec<T>[@n] | 0 < n}) -> T ensures self: RVec<T>[n-1])] pub fn pop(&mut self) -> T { self.inner.pop().unwrap() } }
Note that unlike push
which works for any RVec<T>[@n]
, the pop
method requires that 0 < n
i.e. that the vector is not empty.
Using the push/pop
API
Now already flux
can start checking some code, for example if you push
two
elements, then you can pop
twice, but flux will reject the third pop
at
compile-time
fn test_push_pop() { let mut vec = RVec::new(); // vec: RVec<i32>[0] vec.push(10); // vec: RVec<i32>[1] vec.push(20); // vec: RVec<i32>[2] vec.pop(); // vec: RVec<i32>[1] vec.pop(); // vec: RVec<i32>[0] vec.pop(); // rejected! }
In fact, the error message from flux
will point to exact condition that
does not hold
#![allow(unused)] fn main() { error[FLUX]: precondition might not hold | 24 | v.pop(); | ^^^^^^^ call site | = note: a precondition cannot be proved at this call site note: this is the condition that cannot be proved | 78 | #[spec(fn(self: &mut{RVec<T>[@n] | 0 < n}) -> T | ^^^^^ }
Querying the Size
Perhaps we should peek at the size of the vector
to make sure its not empty before we pop
it.
We can do that by writing a len
method that returns
a usize
corresponding to (and hence, by indexed by)
the size of the input vector
#[flux_rs::trusted] impl<T> RVec<T> { #[spec(fn(&RVec<T>[@vec]) -> usize)] pub fn len(&self) -> usize { self.inner.len() } }
EXERCISE Can you fix the spec
for len
so that the code below
verifies, i.e. so that flux "knows" that
- after two
push
es, the value returned by.len()
is exactly2
, and - after two
pop
s the size is0
again.
fn test_len() { let mut vec = RVec::new(); vec.push(10); vec.push(20); assert(vec.len() == 2); vec.pop(); vec.pop(); assert(vec.len() == 0); }
Random Access
Of course, vectors are not just stacks, they also allow random access to their elements which is where those pesky panics occur, and where the refined vector API gets rather useful.
Now that we're tracking sizes, we can require
that the method to get
an element only be called
with a valid index less than the vector's size
impl<T> RVec<T> { #[spec(fn(&RVec<T>[@n], i: usize{i < n}) -> &T)] pub fn get(&self, i: usize) -> &T { &self.inner[i] } #[spec(fn(&mut RVec<T>[@n], i: usize{i < n}) -> &mut T)] pub fn get_mut(&mut self, i: usize) -> &mut T { &mut self.inner[i] } }
Summing the Elements of an RVec
EXERCISE Can you spot and fix the off-by-one error
in the code below which loops over the elements
of an RVec
and sums them up? 1
fn sum_vec(vec: &RVec<i32>) -> i32 { let mut res = 0; let mut i = 0; while i <= vec.len() { res += vec.get(i); i += 1; } sum }
Using the Index
trait
Its a bit of an eyesore to to use get
and get_mut
directly.
Instead lets implement the Index
and IndexMut
traits for RVec
which allows us to use the [..]
operator to access elements
impl<T> std::ops::Index<usize> for RVec<T> { type Output = T; #[spec(fn(&RVec<T>[@n], i:usize{i < n}) -> &T)] fn index(&self, index: usize) -> &T { self.get(index) } } impl<T> std::ops::IndexMut<usize> for RVec<T> { #[spec(fn(&mut RVec<T>[@n], i:usize{i < n}) -> &mut T)] fn index_mut(&mut self, index: usize) -> &mut T { self.get_mut(index) } }
Summing Nicely
Now the above vec_sum
example looks a little nicer
fn sum_vec_fixed(vec: &RVec<i32>) -> i32 { let mut res = 0; let mut i = 0; while i < vec.len() { res += vec[i] i += 1; } sum }
Memoization
Lets put the whole API to work in this "memoized" version of the fibonacci function which uses a vector to store the results of previous calls
pub fn fib(n: usize) -> i32 { let mut r = RVec::new(); let mut i = 0; while i < n { if i == 0 { r.push(0); } else if i == 1 { r.push(1); } else { let a = r[i - 1]; let b = r[i - 2]; r.push(a + b); } i += 1; } r.pop() }
EXERCISE Flux is unhappy with the pop
at the end of the function
which returns the last value as the result: it thinks the vector
may be empty and so the pop
call may fail ... Can you spot and fix
the problem?
#![allow(unused)] fn main() { error[FLUX]: precondition might not hold --> src/vectors.rs:40:5 | 40 | r.pop() | ^^^^^^^ }
Binary Search
As a last example, lets look at a simplified version of the
binary_search
method from std::vec
, into which
we've snuck a tiny little bug
pub fn binary_search(vec: &RVec<i32>, x: i32) -> Result<usize, usize> { let mut size = vec.len(); let mut left = 0; let mut right = size; while left <= right { let mid = left + size / 2; let val = vec[mid]; if val < x { left = mid + 1; } else if x < val { right = mid; } else { return Ok(mid); } size = right - left; } Err(left) }
Flux complains in two places
#![allow(unused)] fn main() { error[FLUX]: precondition might not hold --> src/vectors.rs:152:19 | 152 | let val = vec[mid]; | ^^^^^^^^ call site | = note: a precondition cannot be proved at this call site note: this is the condition that cannot be proved --> src/rvec.rs:189:44 | 189 | #[spec(fn(&RVec<T>[@n], usize{v : v < n}) -> &T)] | ^^^^^ error[FLUX]: arithmetic operation may overflow --> src/vectors.rs:160:9 | 160 | size = right - left; | ^^^^^^^^^^^^^^^^^^^ }
-
The vector access may be unsafe as
mid
could be out of bounds! -
The
size
variable may underflow asleft
may exceedright
!
EXERCISE Can you the spot off-by-one and figure out a fix?
Summary
Well then. We just saw how Flux's index and constraint mechanisms combine with Rust's ownership to let us write a refined vector API that ensures the safety of all accesses at compile time.
These mechanisms are compositional : we can use standard
type machinery to build up compound structures and APIs from
simple ones, as we will see when we use RVec
to implment
sparse matrices and a small
neural network library.
-
Why not use an iterator? We'll get there in due course! ↩
Const Generics
Rust has a built-in notion of arrays : collections of objects of
the same type T
whose size is known at compile time. The fact that
the sizes are known allows them to be allocated contiguously in memory,
which makes for fast access and manipulation.
When I asked ChatGPT what arrays were useful for, it replied
with several nice examples, including low-level systems programming (e.g.
packets of data represented as struct
s with array-valued fields), storing configuration data, or small sets of related values (e.g. RGB values for a pixel).
#![allow(unused)] fn main() { type Pixel = [u8; 3]; // RGB values let pix0: Pixel = [255, 0, 127]; let pix1: Pixel = [ 0, 255, 127]; }
Compile-time Safety...
As the size of the array is known at compile time, Rust can make sure that we don't create arrays of the wrong size, or access them out of bounds.
For example, rustc
will grumble if you try to make a Pixel
with 4 elements:
#![allow(unused)] fn main() { | 52 | let pix2 : Pixel = [0,0,0,0]; | ----- ^^^^^^^^^ expected an array with a fixed size of 3 elements, found one with 4 elements | | | expected due to this }
Similarly, rustc
will wag a finger if you try to access a Pixel
at an invalid index.
#![allow(unused)] fn main() { | 54 | let blue0 = pix0[3]; | ^^^^^^^ index out of bounds: the length is 3 but the index is 3 | }
... Run-time Panic!
However, the plain type system works only upto a point. For example, consider the
following function to compute the average color
value of a collection of &[Pixel]
#![allow(unused)] fn main() { fn average_color(pixels: &[Pixel], i: usize) -> u64 { let mut sum = 0; for p in pixels { sum += p[i] as u64; } sum / pixels.len() as u64 } }
Now, rustc
will not complain about the above code, even though it may panic if
color
is out of bounds (or of course, if the slice pixels
is empty!).
For example, the following code
fn main() { let pixels = [ [255, 0, 0], [0, 255, 0], [0, 0, 255] ]; let avg = average(&pixels, 3); println!("Average: {}", avg); }
panics at runtime:
thread 'main' panicked ... index out of bounds: the len is 3 but the index is 3
Refined Compile-time Safety
Fortunately, flux
knows about the sizes of arrays and slices. At compile time,
flux
warns about two possible errors in average_color

- The index
i
may be out of bounds when accessingp[i]
and - The division can panic as
pixels
may be empty (i.e. have length0
).
We can fix these errors by requiring that the input
i
be a valid color index, i.e.i < 3
andpixels
be non-empty, i.e. have sizen
wheren > 0
#![allow(unused)] fn main() { #[sig(fn(pixels: &[Pixel][@n], i:usize{i < 3}) -> u64 requires n > 0)] }

Const Generics
Rust also lets us write arrays that are generic over the size. For example,
suppose we want to take two input arrays x
and y
of the same size N
and
compute their dot product. We can write
#![allow(unused)] fn main() { fn dot<const N:usize>(x: [f32;N], y: [f32;N]) -> f32 { let mut sum = 0.0; for i in 0..N { sum += x[i] * y[i]; } sum } }
This is very convenient because rustc
will prevent us from calling dot
with
arrays of different sizes, for example we get a compile-time error
#![allow(unused)] fn main() { | 68 | dot([1.0, 2.0], [3.0, 4.0, 5.0]); | --- ^^^^^^^^^^^^^^^ expected an array with a fixed size of 2 elements, found one with 3 elements | | | arguments to this function are incorrect | }
However, suppose we wanted to compute the dot
product of just the first k
elements
#![allow(unused)] fn main() { fn dot_k<const N:usize>(x: [f32;N], y: [f32;N], k: usize) -> f32 { let mut sum = 0.0; for i in 0..k { sum += x[i] * y[i]; } sum } }
Now, unfortunately, rustc
will not prevent us from calling dot_k
with k
set to a value that is too large!
#![allow(unused)] fn main() { thread 'main' panicked at ... index out of bounds: the len is 2 but the index is 2 }
Yikes.
Refined Const Generics
Fortunately, flux
understands const-generics as well!
First off, it warns us about the fact that the accesses with the index may be out of bounds.

We can fix it in two ways.
- The permissive approach is to accept any
k
but restrict the iteration to the valid elements
#![allow(unused)] fn main() { fn dot_k<const N:usize>(x: [f32;N], y: [f32;N], k: usize) -> f32 { let mut sum = 0.0; let n = if k < N { k } else { N }; for i in 0..n { sum += x[i] * y[i]; } sum } }

- The strict approach is to require that
k
be less than or equal toN
#![allow(unused)] fn main() { #[sig(fn(x: [f32;N], y: [f32;N], k:usize{k <= N}) -> f32)] fn dot_k<const N:usize>(x: [f32;N], y: [f32;N], k: usize) -> f32 { let mut sum = 0.0; for i in 0..k { sum += x[i] * y[i]; } sum } }

Do you understand why
(1) Adding the type signature moved the error from the body of dot_k
into the call-site inside test
?
(2) Then editing test
to call dot_k
with k=2
fixed the error?
Summary
Rust's (sized) arrays are great, and flux
's refinements make them even better,
by ensuring indices are guaranteed to be within the arrays bounds. Const generics
let us write functions that are polymorphic over array sizes, and again, refinements
let us precisely track those sizes to prevent out-of-bounds errors!
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 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[a]
.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]
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::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
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]
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]
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;
}
#[extern_spec]
#[flux::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;
#[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.
#[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;
}
}
#[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);
}
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
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;
}
#[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
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;
}
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
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.
// 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());
}
// 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)]
#[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:
#![feature(step_trait)]
#![allow(unused)]
#[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(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)]
#[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)
}
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]
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]
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;
}
#[extern_spec]
#[flux::assoc(fn with_size(self: Self, n:int) -> bool { self.len == n })]
impl<T> FromIterator<T> for Vec<T> {}
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)]
#[refined_by(inner: I)]
struct Map<I, F>;
#[extern_spec]
#[flux::assoc(fn with_size(self: Self, n:int) -> bool { true })] // default: don't know!
trait FromIterator<A> {}
#[extern_spec(std::iter)]
#[flux::assoc(fn valid_item(self: Self, item: Self::Item) -> bool { true })]
#[flux::assoc(fn size(self: Self) -> int)]
#[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;
#[flux::sig(fn(Self[@s], f: F) -> Map<Self, F>[s] where F: FnMut(Self::Item{item: <Self as Iterator>::valid_item(s, item)}) -> B)]
fn map<B, F>(self, f: F) -> Map<Self, F>
where
Self: Sized,
F: FnMut(Self::Item) -> B;
#[flux::sig(fn(Self[@s], f: F) where F: FnMut(Self::Item{item: <Self as Iterator>::valid_item(s, item)}) -> () )]
fn for_each<F>(self, f: F)
where
Self: Sized,
F: FnMut(Self::Item);
#[flux::sig(fn (Self[@s]) -> B{v: <B as FromIterator<Self::Item>>::with_size(v, <Self as Iterator>::size(s))})]
fn collect<B: FromIterator<Self::Item>>(self) -> B
where
Self: Sized;
}
#[extern_spec(std::slice)]
#[flux::assoc(fn size(x: Iter) -> int { x.len - x.idx })]
#[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::assoc(fn size(x: Enumerate<I>) -> int { <I as Iterator>::size(x.inner) })]
#[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)>;
}
#[extern_spec(std::iter)]
#[flux::assoc(fn size(x: Map<I>) -> int { <I as Iterator>::size(x.inner) })]
#[flux::assoc(fn done(x: Map<I>) -> bool { <I as Iterator>::done(x.inner)})]
#[flux::assoc(fn step(x: Map<I>, y: Map<I>) -> bool { <I as Iterator>::step(x.inner, y.inner)})]
impl<B, I: Iterator, F: FnMut(I::Item) -> B> Iterator for Map<I, F> {} // orig: where F: FnMut(I::Item) -> B {}
// -------------------------------------------------------------------------------------------------------------------------------------
#[flux_rs::extern_spec(std::iter)]
trait IntoIterator {
#[flux_rs::sig(fn(self: Self) -> Self::IntoIter)]
fn into_iter(self) -> Self::IntoIter
where
Self: Sized;
}
#[flux_rs::extern_spec(core::ops)]
impl<I: Iterator> IntoIterator for I {
#[flux_rs::sig(fn(self: I[@s]) -> I[s])]
fn into_iter(self) -> I;
}
#![allow(unused)]
#![feature(allocator_api)]
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())
}
}
#[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 MaskBy15[&](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);
}
-
#[flux_rs::ignore]
(resp.#[flux_rs::trusted]
) is shorthand for#[flux_rs::ignore(yes)]
(resp.#[flux_rs::trusted(yes)]
). ↩
Developer's Guide
Backtraces
You can use the usual RUST_BACKTRACE=1
environment variable to enable backtraces.
With the regular release
build (cargo x install
) you get some backtraces, but
the dev
build, which you can install as shown below, gives more information e.g.
the source-spans of various calls in the backtrace.
$ cargo x install --profile dev
Regression Tests
You can run the various regression tests in the tests/pos
and tests/neg
directories using
cargo xtask test
This will build the flux binary and then run it against the entire test suite. You can optionally pass a filter to only run tests containing some substring. For example:
$ cargo xtask test impl_trait
Compiling xtask v0.1.0 (/path/to/flux/xtask)
Finished dev [unoptimized + debuginfo] target(s) in 0.29s
Running `target/debug/xtask test impl_trait`
$ cargo build
Finished dev [unoptimized + debuginfo] target(s) in 0.05s
$ cargo test -p tests -- --test-args impl_trait
Compiling fluxtests v0.1.0 (/path/to/flux/tests)
Finished test [unoptimized + debuginfo] target(s) in 0.62s
Running tests/compiletest.rs (target/debug/deps/compiletest-1241128f1f51caa4)
running 5 tests
test [ui] pos/surface/impl_trait04.rs ... ok
test [ui] pos/surface/impl_trait03.rs ... ok
test [ui] pos/surface/impl_trait01.rs ... ok
test [ui] pos/surface/impl_trait00.rs ... ok
test [ui] pos/surface/impl_trait02.rs ... ok
test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 191 filtered out; finished in 0.10s
running 2 tests
test [compile-fail] neg/surface/impl_trait00.rs ... ok
test [compile-fail] neg/surface/impl_trait02.rs ... ok
test result: ok. 2 passed; 0 failed; 0 ignored; 0 measured; 207 filtered out; finished in 0.09s
Testing Flux on a File
When working on Flux, you may want to test your changes by running it against a test file.
You can use cargo xtask run <input>
to run Flux on a single input file.
The command will set appropriate flags to be able to use custom Flux attributes and macros,
plus some extra flags useful for debugging.
For example:
$ cat test.rs
#[flux::sig(fn(x: i32) -> i32[x + 1])]
fn add1(x: i32) -> i32 {
x + 1
}
$ cargo xtask run test.rs
The command will use a super set of the flags passed when running regression tests.
Thus, a common workflow is to identify a failing test and run it directly with cargo xtask run
,
or alternatively copy it to a different file.
You may also find useful to create a directory in the root of the project and add it to
.git/info/exclude
.
You can keep files there, outside of version control, and test Flux against them.
I have a directory called attic/
where I keep a file named playground.rs
.
To run Flux on it, I do cargo xtask run attic/playground.rs
.
Reporting locations where errors are emitted
When you use cargo xtask run
you'll see that we report the location an error was emitted, e.g.,
error[FLUX]: refinement type error
--> attic/playground.rs:4:5
|
4 | 0
| ^ a postcondition cannot be proved
-Ztrack-diagnostics: created at crates/flux-refineck/src/lib.rs:114:15 <------- this
You can also pass -Ztrack-diagnostics=y
to enable it if you are not using cargo xtask run
Macro expansion
For example if you have code like in path/to/file.rs
#![allow(unused)] fn main() { #[extern_spec] #[flux::refined_by(elems: Set<T>)] struct HashSet<T, S = RandomState>; }
and you want to see what the extern_spec
macro expands it out to, then run
cargo x run -- -Zunpretty=expanded path/to/file.rs
Or you can run the xtask
command directly
cargo x expand path/to/file.rs
Reporting and dealing with bugs
As Flux is under active development, there are many aspects of Rust that Flux does not yet support, are only partially implemented, or where the implementation may contain bugs. These issues typically manifest as unreachable arms in a match statement (that turn out not to be unreachable) or preemtive assertions to guard against code we don't yet support. To help identify the code that triggers these bugs, there are a few recommended methods for reporting them:
QueryErr::bug
: Use this method to report a bug if the code already returns aQueryResult
. This approach is preferred because we will correctly recover from the error.span_bug!
: When you have aSpan
at hand, you can use this macro in place ofpanic!
to report the span before panicking.tracked_span_bug!
: This macro is similar tospan_bug!
, but it uses a span stored in a thread local variable (if one exists). To track a span in the thread local variable you can useflux_common::bug::track_span
.bug!
: For other cases where none of the above applies, you can use thebug!
macro. This behaves mostly likepanic!
but with nicer formatting.
When running Flux in a new code base, consider setting the flag FLUX_CATCH_BUGS=1
. If this flag is set,
Flux will try to catch and recover from panics emitted with one of the bug macros (using
std::panic::catch_unwind
). Bugs are caught at item boundaries. This may leave Flux or rustc
in an inconsistent state, so there are no guarantees that Flux will behave correctly after recovering
from a panic. However, this may still be useful to gather as many errors as possible. Code can
be selectively ignored later.
Dumping the Checker Trace
cargo x install --debug
FLUX_DUMP_CHECKER_TRACE=1 FLUX_CHECK_DEF=mickey cargo flux
python3 path/to/flux/tools/logreader.py
Debugging Extern Specs
To see the expanded code of an extern_spec
macro, you can do
cargo x expand path/to/file.rs
High-level Architecture
Flux is implemented as a compiler driver. We hook into the compiler by implementing the Callbacks
trait. The implementation is located is in the flux-driver
crate, and it is the main entry point to Flux.
Crates
crates/flux-bin
: Contains thecargo-flux
andflux
binaries used to launch theflux-driver
.crates/flux-common
: Common utility definitions used across all crates.crates/flux-config
: Crate containing logic associated with global configuration flags that change the behavior of Flux, e.g, to enable or disable overflow checking.crates/flux-desugar
: Implementation of name resolution and desugaring from Flux surface syntax into Flux high-level intermediate representation (fhir
). This includes name resolution.crates/flux-driver
: Main entry point to Flux. It contains theflux-driver
binary and the implementation of theCallbacks
trait.crates/flux-errors
: Utility definitions for user facing error reporting.crates/flux-fhir-analysis
: Implements the "analyses" performed in thefhir
, most notably well-formedness checking and conversion fromfhir
intorty
.crates/flux-fixpoint
: Code to interact with the Liquid Fixpoint binary.crates/flux-macros
: Procedural macros used internally to implement Flux.crates/flux-metadata
: Logic for saving Flux crate metadata that can be used to import refined signatures from external crates.crates/flux-middle
: This crate contains common type definitions that are used by the rest of Flux like therty
andfhir
intermediate representations. Akin torustc_middle
.crates/flux-refineck
: Implementation of refinement type checking.crates/flux-syntax
: Definition of the surface syntax AST and parser.tests
: Flux regression tests.lib/flux-attrs
: Implementation of user facing procedural macros for annotating programs with Flux specs.lib/flux-rs
: This is just a re-export of the macros implemented influx-attrs
. The intention is to eventually put Flux "standard library" here, i.e., a set of definitions that are useful when working with Flux.
Intermediate Representations
Flux has several intermediate representations (IR) for types. They represent a refined version of an equivalent type in some rustc
IR. We have picked a distinct verb to refer to the process of going between these different representations to make it easier to refer to them. The following image summarizes all the IRs and the process for going between them.
Surface
The surface IR represents source level Flux annotations. It corresponds to the rustc_ast
data structures in rustc
. The definition as well as the parser is located in the flux-syntax
crate.
Fhir
The Flux High-Level Intermediate Representation (fhir) is a refined version of rustc
's hir. The definition is located in the flux_middle
crate inside the fhir
module. The process of going from surface
to fhir
is called desugaring, and it is implemented in the flux-desugar
crate.
Rty
The definition in the flux_middle::rty
module correspond to a refined version of the main rustc
representation for types defined in rustc_middle::ty
. The process of going from fhir
to rty
is called conversion, and it is implemented in the flux_fhir_analysis::conv
module.
Simplified Rustc
The definition in the flux_middle::rustc
module correspond to simplified version of data structures in rustc
. They can be understood as the currently supported subset of Rust. The process of going from a definition in rustc_middle
into flux_middle::rustc
is called lowering and it is implemented in flux_middle::rustc::lowering
.
Lifting and Refining
Besides the different translation between Flux intermediate representations, there are two ways to get a refined version from a rust type. The process of going from a type in hir
into a type in fhir
is called lifting, and it is implemented in flux_middle::fhir::lift
. The process for going from a type in flux_middle::rustc::ty
into a flux_middle::rty
is called refining, and it is implemented flux_middle::rty::refining
.