From d31f9de9c173fb1149906ffd006886fccb04d115 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 14 Aug 2026 10:11:30 -0700 Subject: [PATCH 1/5] add test for Take --- .../pos/extern_specs/flux_core_iter00.rs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/tests/tests/with_deps/pos/extern_specs/flux_core_iter00.rs b/tests/tests/with_deps/pos/extern_specs/flux_core_iter00.rs index 5c176d220d..20a7e9faa9 100644 --- a/tests/tests/with_deps/pos/extern_specs/flux_core_iter00.rs +++ b/tests/tests/with_deps/pos/extern_specs/flux_core_iter00.rs @@ -16,3 +16,19 @@ pub fn test_position_safe_index(xs: &[i32]) { let _ = xs[i]; } } + +// --- take --- + +#[flux_rs::spec(fn(target: &mut [i32][@len], n: usize{n <= len}, iter: I))] +pub fn test_take(target: &mut [i32], n: usize, iter: I) +where + I: IntoIterator, +{ + let mut iter = iter.into_iter(); + let mut pushed = n; + let to_take = target.len() - pushed; + for element in iter.by_ref().take(to_take) { + target[pushed] = element; + pushed += 1; + } +} From ab12b1914b739768a5f4082a282f5b5cbcb365ad Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 14 Aug 2026 12:47:16 -0700 Subject: [PATCH 2/5] add neg test --- lib/flux-core/src/iter/adapters/mod.rs | 1 + lib/flux-core/src/iter/traits/iterator.rs | 5 ++++ .../neg/extern_specs/extern_spec_iter00.rs | 15 +++++++++++ .../pos/extern_specs/flux_core_iter00.rs | 26 ++++++++++++++++--- 4 files changed, 43 insertions(+), 4 deletions(-) diff --git a/lib/flux-core/src/iter/adapters/mod.rs b/lib/flux-core/src/iter/adapters/mod.rs index 805b80bdd3..bfb1967087 100644 --- a/lib/flux-core/src/iter/adapters/mod.rs +++ b/lib/flux-core/src/iter/adapters/mod.rs @@ -1,3 +1,4 @@ mod enumerate; mod map; mod skip; +mod take; diff --git a/lib/flux-core/src/iter/traits/iterator.rs b/lib/flux-core/src/iter/traits/iterator.rs index 7d386d28b0..42cf129eb4 100644 --- a/lib/flux-core/src/iter/traits/iterator.rs +++ b/lib/flux-core/src/iter/traits/iterator.rs @@ -40,6 +40,11 @@ trait Iterator { where Self: Sized; + #[spec(fn(Self[@s], n: usize) -> Take[n, s])] + fn take(self, n: usize) -> Take + where + Self: Sized; + #[spec(fn(Self[@s], f: F) where F: FnMut(Self::Item{item: ::valid_item(s, item)}) -> () )] fn for_each(self, f: F) where diff --git a/tests/tests/with_deps/neg/extern_specs/extern_spec_iter00.rs b/tests/tests/with_deps/neg/extern_specs/extern_spec_iter00.rs index b4b0b088e1..c9ab74b6ef 100644 --- a/tests/tests/with_deps/neg/extern_specs/extern_spec_iter00.rs +++ b/tests/tests/with_deps/neg/extern_specs/extern_spec_iter00.rs @@ -146,3 +146,18 @@ pub fn find_index_of_3(slice: &[usize]) -> Option { } // TODO: implement IntoIter so I can use these with `for` loops + +#[flux_rs::spec(fn(target: &mut [i32][4], iter: I))] +pub fn test_take_easy(target: &mut [i32], iter: I) +where + I: IntoIterator, +{ + let iter = iter.into_iter(); + let mut pushed = 0; + for element in iter.take(5) { + // Relates `pushed` to the `Take`'s remaining count, which the `for` desugaring hides. + qualifier!(pushed: int, k: int ; pushed + k == 5); + target[pushed] = element; + pushed += 1; //~ ERROR: refinement type + } +} diff --git a/tests/tests/with_deps/pos/extern_specs/flux_core_iter00.rs b/tests/tests/with_deps/pos/extern_specs/flux_core_iter00.rs index 20a7e9faa9..93beead287 100644 --- a/tests/tests/with_deps/pos/extern_specs/flux_core_iter00.rs +++ b/tests/tests/with_deps/pos/extern_specs/flux_core_iter00.rs @@ -1,5 +1,5 @@ extern crate flux_core; -use flux_rs::assert; +use flux_rs::{assert, macros::qualifier}; // --- position --- @@ -19,15 +19,33 @@ pub fn test_position_safe_index(xs: &[i32]) { // --- take --- +#[flux_rs::spec(fn(target: &mut [i32][100], iter: I))] +pub fn test_take_easy(target: &mut [i32], iter: I) +where + I: IntoIterator, +{ + let iter = iter.into_iter(); + let mut pushed = 0; + for element in iter.take(5) { + // Relates `pushed` to the `Take`'s remaining count, which the `for` desugaring hides. + qualifier!(pushed: int, k: int ; pushed + k == 5); + target[pushed] = element; + pushed += 1; + } +} + #[flux_rs::spec(fn(target: &mut [i32][@len], n: usize{n <= len}, iter: I))] -pub fn test_take(target: &mut [i32], n: usize, iter: I) +pub fn test_take_loop(target: &mut [i32], n: usize, iter: I) where I: IntoIterator, { - let mut iter = iter.into_iter(); + let iter = iter.into_iter(); let mut pushed = n; let to_take = target.len() - pushed; - for element in iter.by_ref().take(to_take) { + for element in iter.take(to_take) { + // As above, but the sum is `len` rather than a literal: `pushed` starts at `n` and + // `to_take` is `len - n`. + qualifier!(pushed: int, k: int, len: int ; pushed + k == len); target[pushed] = element; pushed += 1; } From c03bef4031bccd4f0dd6ac4383d5bb7feb827ee7 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 14 Aug 2026 13:00:36 -0700 Subject: [PATCH 3/5] add neg test --- .../with_deps/neg/extern_specs/extern_spec_iter00.rs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/tests/tests/with_deps/neg/extern_specs/extern_spec_iter00.rs b/tests/tests/with_deps/neg/extern_specs/extern_spec_iter00.rs index c9ab74b6ef..23cba53fdb 100644 --- a/tests/tests/with_deps/neg/extern_specs/extern_spec_iter00.rs +++ b/tests/tests/with_deps/neg/extern_specs/extern_spec_iter00.rs @@ -1,6 +1,8 @@ #![allow(unused)] use std::slice::Iter; +use flux_rs::{assert, macros::qualifier}; + extern crate flux_core; #[flux_rs::extern_spec(std::slice)] @@ -24,9 +26,6 @@ trait Iterator { Self: Sized; } -#[flux_rs::sig(fn (bool[true]))] -fn assert(_b: bool) {} - #[flux_rs::extern_spec] #[flux_rs::assoc(fn done(x: Iter) -> bool { x.idx >= x.len })] #[flux_rs::assoc(fn step(x: Iter, y: Iter) -> bool { x.idx + 1 == y.idx && x.len == y.len})] @@ -157,7 +156,7 @@ where for element in iter.take(5) { // Relates `pushed` to the `Take`'s remaining count, which the `for` desugaring hides. qualifier!(pushed: int, k: int ; pushed + k == 5); - target[pushed] = element; - pushed += 1; //~ ERROR: refinement type + target[pushed] = element; //~ ERROR: assertion might fail + pushed += 1; } } From bb6bcf139a00a4614de48e0ac44bcfe2358bebb6 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 14 Aug 2026 13:25:15 -0700 Subject: [PATCH 4/5] add take --- CLAUDE.md | 120 ++++++++++++++++++++++++ lib/flux-core/src/iter/adapters/take.rs | 29 ++++++ 2 files changed, 149 insertions(+) create mode 100644 CLAUDE.md create mode 100644 lib/flux-core/src/iter/adapters/take.rs diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 0000000000..bcaba58eea --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,120 @@ +# CLAUDE.md + +This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository. + +## Project Overview + +Flux is a refinement type checker for Rust. It extends Rust's type system with logical predicates that are verified using SMT solvers (Z3 via liquid-fixpoint). + +## Build Commands + +```bash +# Run regression tests (builds flux-driver and sysroot automatically) +cargo xtask test [filter] # filter is optional substring match + +# Run flux on a single file +cargo xtask run +cargo xtask run file.rs -- -Zdump-mir=ghost # with extra flags + +# Expand macros (e.g., extern_spec) +cargo xtask expand + +# Install binaries to ~/.cargo/bin and libs to ~/.flux +cargo xtask install # release profile (default) +cargo xtask install --profile dev # dev profile with debug info + +# Rebuild library artifacts (flux-core, flux-rs, etc.) +cargo xtask build-sysroot + +# Format and lint +cargo fmt --check +cargo clippy +``` + +## Testing + +Tests are in `tests/tests/`: +- `pos/` - tests that should pass type checking +- `neg/` - tests that should fail (expected errors in `.stderr` files) +- `lib/` - auxiliary library code for other tests +- `todo/` - known failing tests + +Run specific tests: `cargo xtask test impl_trait` runs all tests containing "impl_trait". + +## Architecture + +Flux is a rustc [compiler driver](https://rustc-dev-guide.rust-lang.org/rustc-driver.html) that hooks into compilation via the `Callbacks` trait. + +### Crate Structure + +**Compiler crates** (`crates/`): +- `flux-driver` - Main entry point, rustc callbacks +- `flux-syntax` - LALRPOP-based parser for surface syntax +- `flux-desugar` - Desugars surface syntax to FHIR +- `flux-middle` - Core types: `fhir` and `rty` IRs (like `rustc_middle`) +- `flux-fhir-analysis` - FHIR analysis, conversion to `rty` +- `flux-refineck` - Refinement type checker (main analysis) +- `flux-infer` - Type/refinement inference +- `flux-bin` - CLI wrappers (`flux`, `cargo-flux`) + +**Library crates** (`lib/`): +- `flux-rs` - User-facing macros and attributes +- `flux-core` - Extern specs for stdlib +- `liquid-fixpoint` - SMT solver interface + +### Intermediate Representations + +``` +Surface → FHIR → rty + (parse) (desugar) (convert) +``` + +- **Surface** (`flux-syntax`): Source-level annotations +- **FHIR** (`flux-middle::fhir`): Flux High-Level IR, analogous to rustc's HIR +- **rty** (`flux-middle::rty`): Refined types, analogous to `rustc_middle::ty` + +### Compilation Flow + +1. Rustc calls `FluxCallbacks` during compilation +2. Flux parses `#[flux::sig(...)]` annotations (flux-syntax) +3. Desugars to FHIR with explicit refinement parameters (flux-desugar) +4. Converts to rty (flux-fhir-analysis) +5. Refinement type checking generates SMT queries (flux-refineck) +6. Queries sent to Z3 via liquid-fixpoint + +## Debugging + +```bash +# Enable backtraces with source spans +cargo xtask install --profile dev +RUST_BACKTRACE=1 cargo xtask run test.rs + +# Show where errors are emitted +cargo xtask run test.rs # automatically includes -Ztrack-diagnostics + +# Dump MIR for inspection +cargo xtask run test.rs -- -Zdump-mir=ghost + +# Dump checker trace +FLUX_DUMP_CHECKER_TRACE=1 FLUX_CHECK_DEF=fn_name cargo flux +python3 tools/logreader.py + +# Catch panics and continue (for exploring new codebases) +FLUX_CATCH_BUGS=1 cargo flux +``` + +## Code Conventions + +**Bug reporting in code** - use these instead of `panic!`: +- `QueryErr::bug` - when returning `QueryResult` +- `span_bug!` - when you have a `Span` +- `tracked_span_bug!` - uses thread-local span +- `bug!` - fallback with nice formatting + +**DefId handling** - clippy is configured to disallow direct `DefId::is_local`, `DefId::expect_local`, `DefId::as_local`. Use `MaybeExternId` or `ResolvedDefId` instead to properly handle extern specs. + +## Requirements + +- Nightly rustc (pinned in `rust-toolchain`) +- [liquid-fixpoint](https://github.com/ucsd-progsys/liquid-fixpoint) binary in PATH +- [Z3](https://github.com/Z3Prover/z3) 4.15+ in PATH diff --git a/lib/flux-core/src/iter/adapters/take.rs b/lib/flux-core/src/iter/adapters/take.rs new file mode 100644 index 0000000000..08ebc01e68 --- /dev/null +++ b/lib/flux-core/src/iter/adapters/take.rs @@ -0,0 +1,29 @@ +use flux_attrs::*; + +defs! { + fn min(a: int, b: int) -> int { if a < b { a } else { b } } +} + +/// `Take` is refined by the number of elements left to take (`n`) together with the inner +/// iterator, so that `done` can be stated exactly: a `Take` is exhausted when it has taken its +/// quota *or* the inner iterator has run out. Refining by `n` alone would let `next` claim a +/// `Some` that the inner iterator cannot supply. +#[extern_spec(core::iter)] +#[refined_by(n: int, inner: I)] +struct Take; + +#[extern_spec(core::iter)] +#[assoc( + fn size(x: Take) -> int { min(x.n, ::size(x.inner)) } + fn done(x: Take) -> bool { x.n <= 0 || ::done(x.inner) } + fn step(x: Take, y: Take) -> bool { + y.n == x.n - 1 && ::step(x.inner, y.inner) + } +)] +impl Iterator for Take { + #[spec( + fn(self: &mut Self[@curr_s]) -> Option<_>[!::done(curr_s)] + ensures self: Self{next_s: ::step(curr_s, next_s)} + )] + fn next(&mut self) -> Option; +} From e58631c550fb162d5fa91eb547e1a24e815ee84e Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 14 Aug 2026 13:25:36 -0700 Subject: [PATCH 5/5] add take --- CLAUDE.md | 120 ------------------------------------------------------ 1 file changed, 120 deletions(-) delete mode 100644 CLAUDE.md diff --git a/CLAUDE.md b/CLAUDE.md deleted file mode 100644 index bcaba58eea..0000000000 --- a/CLAUDE.md +++ /dev/null @@ -1,120 +0,0 @@ -# CLAUDE.md - -This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository. - -## Project Overview - -Flux is a refinement type checker for Rust. It extends Rust's type system with logical predicates that are verified using SMT solvers (Z3 via liquid-fixpoint). - -## Build Commands - -```bash -# Run regression tests (builds flux-driver and sysroot automatically) -cargo xtask test [filter] # filter is optional substring match - -# Run flux on a single file -cargo xtask run -cargo xtask run file.rs -- -Zdump-mir=ghost # with extra flags - -# Expand macros (e.g., extern_spec) -cargo xtask expand - -# Install binaries to ~/.cargo/bin and libs to ~/.flux -cargo xtask install # release profile (default) -cargo xtask install --profile dev # dev profile with debug info - -# Rebuild library artifacts (flux-core, flux-rs, etc.) -cargo xtask build-sysroot - -# Format and lint -cargo fmt --check -cargo clippy -``` - -## Testing - -Tests are in `tests/tests/`: -- `pos/` - tests that should pass type checking -- `neg/` - tests that should fail (expected errors in `.stderr` files) -- `lib/` - auxiliary library code for other tests -- `todo/` - known failing tests - -Run specific tests: `cargo xtask test impl_trait` runs all tests containing "impl_trait". - -## Architecture - -Flux is a rustc [compiler driver](https://rustc-dev-guide.rust-lang.org/rustc-driver.html) that hooks into compilation via the `Callbacks` trait. - -### Crate Structure - -**Compiler crates** (`crates/`): -- `flux-driver` - Main entry point, rustc callbacks -- `flux-syntax` - LALRPOP-based parser for surface syntax -- `flux-desugar` - Desugars surface syntax to FHIR -- `flux-middle` - Core types: `fhir` and `rty` IRs (like `rustc_middle`) -- `flux-fhir-analysis` - FHIR analysis, conversion to `rty` -- `flux-refineck` - Refinement type checker (main analysis) -- `flux-infer` - Type/refinement inference -- `flux-bin` - CLI wrappers (`flux`, `cargo-flux`) - -**Library crates** (`lib/`): -- `flux-rs` - User-facing macros and attributes -- `flux-core` - Extern specs for stdlib -- `liquid-fixpoint` - SMT solver interface - -### Intermediate Representations - -``` -Surface → FHIR → rty - (parse) (desugar) (convert) -``` - -- **Surface** (`flux-syntax`): Source-level annotations -- **FHIR** (`flux-middle::fhir`): Flux High-Level IR, analogous to rustc's HIR -- **rty** (`flux-middle::rty`): Refined types, analogous to `rustc_middle::ty` - -### Compilation Flow - -1. Rustc calls `FluxCallbacks` during compilation -2. Flux parses `#[flux::sig(...)]` annotations (flux-syntax) -3. Desugars to FHIR with explicit refinement parameters (flux-desugar) -4. Converts to rty (flux-fhir-analysis) -5. Refinement type checking generates SMT queries (flux-refineck) -6. Queries sent to Z3 via liquid-fixpoint - -## Debugging - -```bash -# Enable backtraces with source spans -cargo xtask install --profile dev -RUST_BACKTRACE=1 cargo xtask run test.rs - -# Show where errors are emitted -cargo xtask run test.rs # automatically includes -Ztrack-diagnostics - -# Dump MIR for inspection -cargo xtask run test.rs -- -Zdump-mir=ghost - -# Dump checker trace -FLUX_DUMP_CHECKER_TRACE=1 FLUX_CHECK_DEF=fn_name cargo flux -python3 tools/logreader.py - -# Catch panics and continue (for exploring new codebases) -FLUX_CATCH_BUGS=1 cargo flux -``` - -## Code Conventions - -**Bug reporting in code** - use these instead of `panic!`: -- `QueryErr::bug` - when returning `QueryResult` -- `span_bug!` - when you have a `Span` -- `tracked_span_bug!` - uses thread-local span -- `bug!` - fallback with nice formatting - -**DefId handling** - clippy is configured to disallow direct `DefId::is_local`, `DefId::expect_local`, `DefId::as_local`. Use `MaybeExternId` or `ResolvedDefId` instead to properly handle extern specs. - -## Requirements - -- Nightly rustc (pinned in `rust-toolchain`) -- [liquid-fixpoint](https://github.com/ucsd-progsys/liquid-fixpoint) binary in PATH -- [Z3](https://github.com/Z3Prover/z3) 4.15+ in PATH