From 8eefd1d47c7803f084537624f8a9fc44e9b3f69a Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 26 Jun 2025 11:23:33 -0700 Subject: [PATCH 1/5] Add Flux --- library/core/Cargo.toml | 6 ++++++ library/core/src/ascii/ascii_char.rs | 1 + library/core/src/convert/num.rs | 8 +++++--- library/core/src/flux_info.rs | 10 ++++++++++ library/core/src/lib.rs | 3 +++ 5 files changed, 25 insertions(+), 3 deletions(-) create mode 100644 library/core/src/flux_info.rs diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml index 440a6598aa487..0b6a00d24cda7 100644 --- a/library/core/Cargo.toml +++ b/library/core/Cargo.toml @@ -45,4 +45,10 @@ check-cfg = [ 'cfg(target_has_reliable_f16_math)', 'cfg(target_has_reliable_f128)', 'cfg(target_has_reliable_f128_math)', + 'cfg(kani)', + 'cfg(flux)' ] + +[package.metadata.flux] +enabled = true +include = [ "src/ascii/*" ] diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs index b7240840d2cca..856a8632f269d 100644 --- a/library/core/src/ascii/ascii_char.rs +++ b/library/core/src/ascii/ascii_char.rs @@ -529,6 +529,7 @@ impl AsciiChar { /// Gets this ASCII character as a byte. #[unstable(feature = "ascii_char", issue = "110998")] + #[cfg_attr(flux, flux::spec(fn(Self) -> u8{v: v <= 127}))] #[inline] pub const fn to_u8(self) -> u8 { self as u8 diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index 7fbf3301efe46..94b24e288d11e 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -69,19 +69,21 @@ macro_rules! impl_from { ), ); }; - ($Small:ty => $Large:ty, #[$attr:meta] $(,)?) => { + ($Small:ty => $Large:ty, #[$attr:meta] $(, #[$flux_attr:meta])? $(,)?) => { impl_from!( $Small => $Large, #[$attr], concat!("Converts [`", stringify!($Small), "`] to [`", stringify!($Large), "`] losslessly."), + $(#[$flux_attr],)? ); }; - ($Small:ty => $Large:ty, #[$attr:meta], $doc:expr $(,)?) => { + ($Small:ty => $Large:ty, #[$attr:meta], $doc:expr $(, #[$flux_attr:meta])? $(,)?) => { #[$attr] impl From<$Small> for $Large { // Rustdocs on the impl block show a "[+] show undocumented items" toggle. // Rustdocs on functions do not. #[doc = $doc] + $(#[$flux_attr])? #[inline(always)] fn from(small: $Small) -> Self { small as Self @@ -109,7 +111,7 @@ impl_from!(u8 => u16, #[stable(feature = "lossless_int_conv", since = "1.5.0")]) impl_from!(u8 => u32, #[stable(feature = "lossless_int_conv", since = "1.5.0")]); impl_from!(u8 => u64, #[stable(feature = "lossless_int_conv", since = "1.5.0")]); impl_from!(u8 => u128, #[stable(feature = "i128", since = "1.26.0")]); -impl_from!(u8 => usize, #[stable(feature = "lossless_int_conv", since = "1.5.0")]); +impl_from!(u8 => usize, #[stable(feature = "lossless_int_conv", since = "1.5.0")], #[cfg_attr(flux, flux::spec(fn(x:u8) -> usize[x]))]); impl_from!(u16 => u32, #[stable(feature = "lossless_int_conv", since = "1.5.0")]); impl_from!(u16 => u64, #[stable(feature = "lossless_int_conv", since = "1.5.0")]); impl_from!(u16 => u128, #[stable(feature = "i128", since = "1.26.0")]); diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs new file mode 100644 index 0000000000000..e58feaa4091d4 --- /dev/null +++ b/library/core/src/flux_info.rs @@ -0,0 +1,10 @@ +#[flux::defs { + property ShiftRightByFour[>>](x, y) { + 16 * [>>](x, 4) == x + } + + property MaskBy15[&](x, y) { + [&](x, y) <= y + } +}] +const _: () = {}; \ No newline at end of file diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs index 1adfcd255a3b3..7fe1a98aed591 100644 --- a/library/core/src/lib.rs +++ b/library/core/src/lib.rs @@ -421,3 +421,6 @@ pub mod simd { } include!("primitive_docs.rs"); + +#[cfg(flux)] +mod flux_info; From 325fccdca40404b92a37f5dbd98dc5aacc998cc1 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Fri, 27 Jun 2025 19:15:20 -0700 Subject: [PATCH 2/5] Add workflow --- .github/workflows/flux.yml | 77 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) create mode 100644 .github/workflows/flux.yml diff --git a/.github/workflows/flux.yml b/.github/workflows/flux.yml new file mode 100644 index 0000000000000..f9e342a4e79b1 --- /dev/null +++ b/.github/workflows/flux.yml @@ -0,0 +1,77 @@ +name: Flux + +on: + workflow_dispatch: + push: + branches: [main] + pull_request: + branches: [main] + +env: + FIXPOINT_VERSION: "556104ba5508891c357b0bdf819ce706e93d9349" + FLUX_VERSION: "192362760b73ea517d0349f7167661a02175b24f" + +jobs: + check-flux-on-core: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + submodules: true + + - name: Local Binaries + run: | + mkdir -p ~/.local/bin + echo ~/.cargo/bin >> $GITHUB_PATH + echo ~/.local/bin >> $GITHUB_PATH + + - name: Cache fixpoint + uses: actions/cache@v4 + id: cache-fixpoint + with: + path: ~/.local/bin/fixpoint + key: fixpoint-bin-${{ runner.os }}-${{ env.FIXPOINT_VERSION }} + + - name: Install Haskell + if: steps.cache-fixpoint.outputs.cache-hit != 'true' + uses: haskell-actions/setup@v2.7.0 + with: + enable-stack: true + stack-version: "2.15.7" + + - name: Install fixpoint + if: steps.cache-fixpoint.outputs.cache-hit != 'true' + run: | + git clone https://github.com/ucsd-progsys/liquid-fixpoint.git + cd liquid-fixpoint + git checkout $FIXPOINT_VERSION + stack install --fast --flag liquid-fixpoint:-link-z3-as-a-library + + - name: Install Z3 + uses: cda-tum/setup-z3@v1.6.1 + with: + version: 4.12.1 + platform: linux + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + + - name: Clone Flux + run: | + git clone https://github.com/flux-rs/flux.git + cd flux + git checkout $FLUX_VERSION + + - name: Rust Cache + uses: Swatinem/rust-cache@v2.7.8 + with: + workspaces: flux + + - name: Install Flux + run: | + cd flux + cargo x install + + - name: Verify Core + run: | + cd library + FLUXFLAGS="-Ftimings" cargo flux -p core From 57edee98846dfb3325904df8e0b82d59cbccfb0f Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Sun, 29 Jun 2025 09:34:07 -0700 Subject: [PATCH 3/5] Add Flux entry to the book --- doc/src/SUMMARY.md | 1 + doc/src/tools/flux.md | 239 ++++++++++++++++++++++++++++++++++++++++ library/core/Cargo.toml | 2 +- 3 files changed, 241 insertions(+), 1 deletion(-) create mode 100644 doc/src/tools/flux.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 7d38ba148f8cf..a453bee644970 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -10,6 +10,7 @@ - [Kani](./tools/kani.md) - [GOTO Transcoder](./tools/goto-transcoder.md) - [VeriFast](./tools/verifast.md) + - [Flux](./tools/flux.md) --- diff --git a/doc/src/tools/flux.md b/doc/src/tools/flux.md new file mode 100644 index 0000000000000..31fe74b0a1c3e --- /dev/null +++ b/doc/src/tools/flux.md @@ -0,0 +1,239 @@ +# Flux + +[Flux](https://flux-rs.github.io/flux) is a refinement type checker +that can be used to prove user-defined safety properties for Rust. +Users can write their own properties via refinement type contracts +(a generalization of pre- and post-conditions). Additionally, out of the +box, Flux checks for various issues such as + +- arithmetic overflows +- division by zero +- array bounds violations + +## Installation + +See the [installation section of the Flux book](https://flux-rs.github.io/flux/install.html) +to learn how to install and run Flux. + + +## Usage + +(Adapted from the Kani documentation; see [the Flux book](https://flux-rs.github.io/flux) +for many more examples.) + +Consider a Rust file `demo.rs` with a function that returns +the absolute value of the difference between two integers. +To *prove* that the function always returns a *non-negative* result, you write +a Flux specification—above the function definition—that says the output +is a refinement type `i32{v: 0 <= v}` denoting non-negative `i32` values. + + +``` rust +// demo.rs +#[allow(dead_code)] +#[cfg_attr(flux, flux::spec(fn(a: i32, b: i32) -> i32{v:0 <= v}))] +fn test_abs(a:i32, b:i32) -> i32 { + if a > b { + a - b + } else { + b - a + } +} +``` + +Now, if you run + +``` +$ flux --crate-type=lib demo.rs +``` + +Flux will return immediately with **no output** indicating the code is safe. + +This may be baffling for those with a keen understanding of arithmetic overflows: +what if `a` is `INT_MAX` and `b` is `INT_MIN`? Indeed, Flux has overflow checking +off by default but you can optionally switch it on for a function, module, or entire crate. + +``` rust +// demo.rs +#[allow(dead_code)] +#[cfg_attr(flux, flux::opts(check_overflow = true))] +#[cfg_attr(flux, flux::spec(fn(a: i32, b: i32) -> i32{v:0 <= v}))] +fn test_abs(a:i32, b:i32) -> i32 { + if a > b { + a - b + } else { + b - a + } +} +``` + +Now, when you run `flux` you see that + +``` +$ flux --crate-type=lib demo.rs +error[E0999]: arithmetic operation may overflow + --> demo.rs:9:9 + | +9 | b - a + | ^^^^^ + +error[E0999]: arithmetic operation may overflow + --> demo.rs:7:9 + | +7 | a - b + | ^^^^^ + +error: aborting due to 2 previous errors +``` + +You might *fix* the errors, i.e., prove the function have no overflows, +by requiring the *inputs* also be non-negative: + +```rust +#[allow(dead_code)] +#[cfg_attr(flux, flux::opts(check_overflow = true))] +#[cfg_attr(flux, flux::spec(fn(a: i32{0 <= a}, b: i32{0 <= b}) -> i32{v: 0 <= v}))] +fn test_abs(a:u32, b:u32) -> u32 { + if a > b { + a - b + } else { + b - a + } +} +``` + +This time `flux --crate-type=lib demo.rs` finishes swiftly without reporting any errors. + +For a more detailed online interactive tutorial, with many more examples, see [the Flux book](https://flux-rs.github.io/flux). + +## Using Flux to verify the (model-checking fork of) the Rust Standard Library + +Currrently, we have configured Flux to run on the +[model-checking fork](https://github.com/model-checking/verify-rust-std) +of the Rust Standard Library. You can run Flux on + +1. a single function, +2. a single file, +3. a set of files matching a glob-pattern, or +4. the entire crate. + +### Running on a Single Function + +Suppose the function is in a file inside `library/core/src/`, e.g., +`library/core/src/ascii/ascii_char.rs`. +For example, let's suppose `test_abs` was added to the end of that file, +*with* the `check_overflow = true` and *without* the `flux::spec` contract. +Then if you did + +```bash +$ cd library/core +$ FLUXFLAGS="-Fcheck-def=test_abs" cargo flux +``` + +you should get some output like + +``` + Checking core v0.0.0 (/verify-rust-std/library/core) + +error[E0999]: arithmetic operation may overflow + --> core/src/ascii/ascii_char.rs:635:9 + | +635 | b - a + | ^^^^^ + +error[E0999]: arithmetic operation may overflow + --> core/src/ascii/ascii_char.rs:633:9 + | +633 | a - b + | ^^^^^ + +error: could not compile `core` (lib) due to 2 previous errors + +Checking core v0.0.0 (/verify-rust-std/library/core) +Finished `flux` profile [unoptimized + debuginfo] target(s) in 5.54s +``` + + +You can now fix the error by adding the non-negative input specification above the definition +of `test_abs` + +```rust +#[cfg_attr(flux, flux::spec(fn(a: i32{0 <= a}, b: i32{0 <= b}) -> i32{v: 0 <= v})] +``` + +and when you re-run, it should finish with no warnings + +**NOTE** When checking inside `core`, we wrap the `flux` specification attributes +in `#[cfg_attr(flux,...)]` so they are only read by flux. + +### Running on a Single File + +To run on a single _file_ you can just pass the name of that file to flux (relative from the +crate root) as + +```bash +$ cd library/core +$ FLUXFLAGS="-Finclude=src/ascii/ascii_char.rs" cargo flux +``` + +### Running on a Globset of Files + +To run on a comma-separated _globset of files_, e.g., an entire module, you can just pass +the appropriate globset as + +```bash +$ cd library/core +$ FLUXFLAGS="-Finclude=src/ascii/*" cargo flux +``` + +### Configuring Flux via `Cargo.toml` + +Flux can also be configured in the `Cargo.toml` under the +`[package.metadata.flux]` section. + +You can add or remove things from the `include` declaration there +to check other files. Currently, it is configured to only run on a +tiny subset of the modules; you should comment out that line if you +want to run on _all_ of `core`. + +You can run flux on all the parts of the `core` crate specified in `include` +directive in the `Cargo.toml` by doing + +```bash +$ cd library/core +$ cargo flux +``` + +### Running on the Entire Crate + +Currently the `core/Cargo.toml` is configured (see the `[package.metadata.flux]`) to +only run on a tiny subset of the modules, you should comment out that line if you +really want to run on _all_ of `core`, and then run + +```bash +$ cd library/core +$ cargo flux +``` + +Sadly, various Rust features exercised by the crate are not currently supported by +Flux making it crash ignominously. + +You can tell it to do a "best-effort" analysis by ignoring those crashes +(as much as possible) by + +```bash +$ FLUXFLAGS="-Fcatch-bugs" cargo flux +``` + +in which case Flux will grind over the whole crate and point out nearly 300+ *possible* +warnings about overflows, array bounds accesses etc., +and also about 200+ ICE (places where it crashes!) To do this, you may also have +to tell Flux to not check certain modules, e.g. by adding +various `flux::trusted` annotations [as shown here](https://github.com/flux-rs/verify-rust-std/blob/fluxable/library/core/src/lib.rs) + + +## More details + +You can find more information on using Flux—especially on how to write different +kinds of specifications and configuration options—in [the Flux book](https://flux-rs.github.io/flux). +Happy proving! diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml index 0b6a00d24cda7..8fffe185ea146 100644 --- a/library/core/Cargo.toml +++ b/library/core/Cargo.toml @@ -51,4 +51,4 @@ check-cfg = [ [package.metadata.flux] enabled = true -include = [ "src/ascii/*" ] +include = [ "src/ascii{*.rs,/**/*.rs}" ] From 24f018298e64f868189e9d6a2a7488422666b9c5 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Wed, 2 Jul 2025 11:52:42 -0700 Subject: [PATCH 4/5] Add comments to flux_info.rs --- library/core/src/flux_info.rs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs index e58feaa4091d4..c1aa8f1506cff 100644 --- a/library/core/src/flux_info.rs +++ b/library/core/src/flux_info.rs @@ -1,3 +1,8 @@ +//! This file contains auxiliary definitions for Flux + +/// List of properties tracked for the result of primitive bitwise operations. +/// See the following link for more information on how extensible properties for primitive operations work: +/// #[flux::defs { property ShiftRightByFour[>>](x, y) { 16 * [>>](x, 4) == x @@ -7,4 +12,4 @@ [&](x, y) <= y } }] -const _: () = {}; \ No newline at end of file +const _: () = {}; From 374c2d455dca6ab0c7468201f2217e67bf38f3c7 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Sun, 6 Jul 2025 18:29:05 -0700 Subject: [PATCH 5/5] Add caveats section + ub vs panic --- doc/src/tools/flux.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/doc/src/tools/flux.md b/doc/src/tools/flux.md index 31fe74b0a1c3e..32a49420a9b84 100644 --- a/doc/src/tools/flux.md +++ b/doc/src/tools/flux.md @@ -10,6 +10,10 @@ box, Flux checks for various issues such as - division by zero - array bounds violations +Currently, Flux does not distinguish between logic errors (e.g., those that may cause a panic) +and errors that can lead to undefined behavior. They both manifest +as contract violations. + ## Installation See the [installation section of the Flux book](https://flux-rs.github.io/flux/install.html) @@ -237,3 +241,16 @@ various `flux::trusted` annotations [as shown here](https://github.com/flux-rs/v You can find more information on using Flux—especially on how to write different kinds of specifications and configuration options—in [the Flux book](https://flux-rs.github.io/flux). Happy proving! + +## Caveats and Current Limitations + +Flux is aimed to be a lightweight verifier that is predictable and fully automated. To achieve this, +it restricts refinement predicates to decidable fragments of first-order logic +(i.e., without quantifiers). As a result, some properties (such as sortedness of arrays) may be +hard to specify. + +Flux also has limited and conservative support for unsafe code. It can track properties of +pointers (e.g., alignment and provenance) but not the values of data written through +them. + +Lastly, Flux is under active development, and many Rust features are not yet supported.