flux
flux copied to clipboard
flux-rs
Refinement Types for Rust
Inspired by the Flux paper's usage of the std library `swap(&mut T, &mut T)` function, I was curious why/how Flux was able to pass refinements through the function. I think...
The second call to `foo` fails to verify. Looking at the `mir` the location's value is defined using a `const _` so perhaps something is lost there? ```rust #[flux::sig(fn(&i32[5]))] fn...
Why is the following program considered not safe ? ```rust struct A { val: u32, } impl A { fn f(&mut self) -> () { if self.val == 0 {...
```rust #[flux::sig(fn(i32[@n]) -> bool[0 < n])] fn is_positive(x: i32) -> bool { match x { ..=0 => false, 1.. => true, } } ``` Flux is able to verify the...
(via: https://github.com/flux-rs/flux/pull/481#discussion_r1297422785) So this is the hard part. I've been thinking for a while about generic consts appearing in refinements. I think supporting that would be very cool. This is...
Would be rather nice to be able to write stuff like ```rust #[flux] fn assert(b:bool[true]) {} #[flux] fn inc(x: &mut i32{v:0 f32 { let mut res = 0.0; for i...
The following code panic when trying to update `centers[i]` ```rust #[flux::sig(fn(&RVec[@n], usize) -> RVec[n])] fn normal(x: &RVec, w: usize) -> RVec { let mut i = 0; let mut res...
Sooner rather than later we will want to allow "assuming" types for functions from other crates /stdlib that are _not_ part of `flux`. For example, we want to allow some...