flux
flux copied to clipboard
flux-rs
Refinement Types for Rust
Hello, it appears that using compile-time constants as array lengths. For example, the following code ```Rust #[flux::constant] const BUFLEN: usize = 100; type FixedSizeBuffer = [i32; BUFLEN]; ``` fails with...
The following should pass but do not. ```rust #![feature(allocator_api)] #![feature(associated_type_bounds)] use std::ops::Index; #[path = "../lib/vec.rs"] mod vec; #[flux::sig(fn(xs: &Vec 55}>[100]) -> i32{v:v > 55})] fn test_get(xs: &Vec) -> i32 {...
I want to prove [leftpad](https://github.com/hwayne/lets-prove-leftpad) with flux, and the corresponding property involves indexing into a vector and ensuring that the value at the index has a correct value. Is it...
The only way we have to relate types is via subtyping. This plays poorly with invariant type constructors because we must apply subtyping both ways. This is especially bad if...
The following currently crashes ```rust #![feature(register_tool)] #![register_tool(flux)] pub fn mk_ten() -> Vec { let v = vec![1,2]; v } ``` which currently crashes with ``` error[FLUX]: unsupported statement --> flux-tests/tests/todo/vec.rs:5:13...
Currently, `flux` happily verifies the below which seems dubious: ```rust pub trait Silly { #[flux::sig(fn(&Self) -> i32{v:100 < v})] fn bloop(&self) -> i32; } impl Silly for i32 { fn...
The only reason we need to check this is that we allow you to write the "return type" for a variant. If we instead had: ```rust #[flux::refined_by(b: bool)] enum Option...
The following is crashing with ``` error: internal compiler error: crates/flux-middle/src/rty/projections.rs:54:13: failed to resolve `AliasTy { args: [F, (T,)], refine_args: [], def_id: DefId(2:3046 ~ core[8a68]::ops::function::FnOnce::Output) }` in DefId(0:34 ~ flux_examples[6cad]::enums::option::{impl#0}::map)...
# unresolved import `time` When running `rustc-flux --crate-type=lib src/generic.rs` the system does not recognize the import of the `time` library and throws the following error: ```bash error[E0432]: unresolved import `time`...
The following code panics with ``` error: internal compiler error: crates/flux-refineck/src/constraint_gen.rs:597:18: `&'?8 &'?9 str` Vec