Issues

New issue

An enum declared inside a trait-impl method or a closure produces ill-formed SMT-LIB (unknown sort 'A1_<S'), and two same-named local enums in one function share a datatype and panic: datatype symbols come from def_path_str
coord-e/thrust#316 · opened on Oct 2, 2026
1
Incompleteness: overwriting a &mut-carrying value through a reference (*x = y, *slot = None) never resolves the overwritten borrow's prophecy, so the lender is havoc'd — even writes made before the overwrite are lost
coord-e/thrust#310 · opened on Sep 29, 2026
An unsuffixed integer literal in a specification is typed i32, so requires(x > -9223372036854775807 - 1) on an i64 is rejected as out of range
coord-e/thrust#309 · opened on Sep 29, 2026
A promoted constant of unsigned or 128-bit integer type panics in const_bytes_ty (const bytes ty: u32, const int bytes len: 16)
coord-e/thrust#308 · opened on Sep 29, 2026
Reading a static panics with unimplemented!("const ptr alloc: Static(..)")
coord-e/thrust#306 · opened on Sep 29, 2026
Indexing a fixed-size array place (a[i] on [T; N]) panics: ProjectionElem::Index is handled neither in elaborate_place_for_borrow nor in Path::from
coord-e/thrust#304 · opened on Sep 29, 2026
for i in a..b panics with unknown def (resolved): into_iter and next on Range have no extern spec
coord-e/thrust#303 · opened on Sep 29, 2026
Shift and bitwise operators (<<, >>, &, |, ^) on integers abort with unimplemented!("ty=int, op=Shl")
coord-e/thrust#302 · opened on Sep 29, 2026
Panic inconsistent types in subtyping.rs when a ghost! parameter is typed differently from the live variable it names (|c: Counter, ..| for c: &mut Counter), instead of a diagnostic
coord-e/thrust#301 · opened on Sep 29, 2026
A Ghost<T> struct field cannot be used as its contents in ensures/ghost! (E0599 no method push/len, E0369 for ==), while a Ghost<T> parameter can
coord-e/thrust#300 · opened on Sep 29, 2026
The driver links whichever libthrust_macros-<hash> read_dir lists first, so after cargo clippy it can silently use a stale thrust-macros build
coord-e/thrust#299 · opened on Sep 29, 2026
u8/u16/i8/i16/u128/i128 have no Model impl, so any function using them panics with unrefined_ty in TypeBuilder::build
coord-e/thrust#298 · opened on Sep 29, 2026
False entry-value postcondition verifies with trusted Mut aliases and implicit drop resolution
coord-e/thrust#289 · opened on Sep 28, 2026
Regression from #270: any Vec<Vec<T>> (2-D grid, list of rows) is rejected as Unsat — a row read back with grid[i] has an unconstrained model, because seq.nth is not axiomatized at a sequence element sort in either supported solver; the same programs verified in 0.4 s before the native-Seq switch
coord-e/thrust#282 · opened on Sep 26, 2026
Slicing with a range (&v[1..], &v[..n], &v[a..b], &v[..]) ICEs: the refinement-spec table is keyed by DefId alone, so _extern_spec_slice_index's usize signature is applied to every I: SliceIndex instantiation of the one shared Index::index impl method
coord-e/thrust#281 · opened on Sep 24, 2026
Replacing a Box/&mut-typed struct or tuple field (c.page = Box::new(..)) is elaborated into a write *through* the old pointer, so the field's type in the env becomes its pointee and every later use of the struct aborts the analyzer
coord-e/thrust#267 · opened on Sep 18, 2026
A locally-declared struct/enum never gets a Model instance, so Vec<P>/Box<P>/&[P]/[P; N]/&mut P abort in TypeBuilder::build — Vec<P> dies inside alloc's private fields (*const u8), and a one-line impl Model for P { type Ty = Self; } makes every case verify
coord-e/thrust#266 · opened on Sep 17, 2026
Incompleteness: a &mut into an enum/Option whose payload is a Vec (any Seq-modeled container) defeats the default solver configuration — a five-line Option<Vec<i64>> program times out, while the same code with the container in a struct field, or moved out by value, verifies in 0.5 s
coord-e/thrust#263 · opened on Sep 11, 2026
1
Incompleteness: a refinement declared on any parameter but the last (#[param]/#[sig]) is never assumed in the body, so no multi-argument function can be given a refinement-typed signature
coord-e/thrust#261 · opened on Sep 7, 2026
Incompleteness: the hard-coded fp.spacer.global=true z3 option makes any nested loop whose inner body has a merging conditional unverifiable — an 11-clause system that z3 solves in 0.5s without it runs >5min with it
coord-e/thrust#260 · opened on Sep 6, 2026
Unsound: a crate with no main (any --crate-type lib/rlib/…) gets no entry-point anchor, so every inferred precondition is discharged as false and the whole crate — pub API functions that always panic included — verifies as safe
coord-e/thrust#259 · opened on Sep 5, 2026
No method of a trait impl can be specified: requires/ensures/param/ret/sig emit their formula_fn companions as items of the impl, so every trait-impl method dies with E0407 — and the only alternative (spec on the trait) forces one spec on all impls
coord-e/thrust#258 · opened on Sep 3, 2026
A loop bound that MIR folds into a debug-info constant cannot be named in invariant!: let n = 10; while i < n fatally errors with "not a live variable", and under shadowing the name silently binds to the wrong variable
coord-e/thrust#257 · opened on Sep 2, 2026
Support multi-crate projects (cargo)
coord-e/thrust#255 · opened on Sep 2, 2026
Panic (deref unbound var / borrowing unbound var): THRUST_ENUM_EXPANSION_DEPTH_LIMIT truncates every binding form, not just enum unfolding, so a &mut two enum layers deep (Result<Option<&mut T>, E>) gets no flow binding and any use of it aborts the compiler
coord-e/thrust#253 · opened on Sep 1, 2026

Navigation Menu

Issues

Issues

An `enum` declared inside a trait-impl method or a closure produces ill-formed SMT-LIB (`unknown sort 'A1_<S'`), and two same-named local enums in one function share a datatype and panic: datatype symbols come from `def_path_str`

Incompleteness: overwriting a `&mut`-carrying value through a reference (`x = y`, `slot = None`) never resolves the overwritten borrow's prophecy, so the lender is havoc'd — even writes made before the overwrite are lost

An unsuffixed integer literal in a specification is typed `i32`, so `requires(x > -9223372036854775807 - 1)` on an `i64` is rejected as out of range

A promoted constant of unsigned or 128-bit integer type panics in `const_bytes_ty` (`const bytes ty: u32`, `const int bytes len: 16`)

Reading a `static` panics with `unimplemented!("const ptr alloc: Static(..)")`

Indexing a fixed-size array place (`a[i]` on `[T; N]`) panics: `ProjectionElem::Index` is handled neither in `elaborate_place_for_borrow` nor in `Path::from`

`for i in a..b` panics with `unknown def (resolved)`: `into_iter` and `next` on `Range` have no extern spec

Shift and bitwise operators (`<<`, `>>`, `&`, `|`, `^`) on integers abort with `unimplemented!("ty=int, op=Shl")`

Panic `inconsistent types` in `subtyping.rs` when a `ghost!` parameter is typed differently from the live variable it names (`|c: Counter, ..|` for `c: &mut Counter`), instead of a diagnostic

A `Ghost<T>` struct field cannot be used as its contents in `ensures`/`ghost!` (`E0599` no method `push`/`len`, `E0369` for `==`), while a `Ghost<T>` parameter can

The driver links whichever `libthrust_macros-<hash>` `read_dir` lists first, so after `cargo clippy` it can silently use a stale `thrust-macros` build

`u8`/`u16`/`i8`/`i16`/`u128`/`i128` have no `Model` impl, so any function using them panics with `unrefined_ty` in `TypeBuilder::build`

False entry-value postcondition verifies with trusted Mut aliases and implicit drop resolution

Slicing with a range (`&v[1..]`, `&v[..n]`, `&v[a..b]`, `&v[..]`) ICEs: the refinement-spec table is keyed by `DefId` alone, so `_extern_spec_slice_index`'s `usize` signature is applied to every `I: SliceIndex` instantiation of the one shared `Index::index` impl method

Replacing a `Box`/`&mut`-typed struct or tuple field (`c.page = Box::new(..)`) is elaborated into a write through the old pointer, so the field's type in the env becomes its pointee and every later use of the struct aborts the analyzer

A locally-declared `struct`/`enum` never gets a `Model` instance, so `Vec<P>`/`Box<P>`/`&[P]`/`[P; N]`/`&mut P` abort in `TypeBuilder::build` — `Vec<P>` dies inside `alloc`'s private fields (`*const u8`), and a one-line `impl Model for P { type Ty = Self; }` makes every case verify

Incompleteness: a `&mut` into an `enum`/`Option` whose payload is a `Vec` (any `Seq`-modeled container) defeats the default solver configuration — a five-line `Option<Vec<i64>>` program times out, while the same code with the container in a struct field, or moved out by value, verifies in 0.5 s

Incompleteness: a refinement declared on any parameter but the last (`#[param]`/`#[sig]`) is never assumed in the body, so no multi-argument function can be given a refinement-typed signature

Incompleteness: the hard-coded `fp.spacer.global=true` z3 option makes any nested loop whose inner body has a merging conditional unverifiable — an 11-clause system that z3 solves in 0.5s without it runs >5min with it

Unsound: a crate with no `main` (any `--crate-type lib`/`rlib`/…) gets no entry-point anchor, so every inferred precondition is discharged as `false` and the whole crate — `pub` API functions that always panic included — verifies as `safe`

No method of a trait `impl` can be specified: `requires`/`ensures`/`param`/`ret`/`sig` emit their `formula_fn` companions as items of the `impl`, so every trait-impl method dies with `E0407` — and the only alternative (spec on the trait) forces one spec on all impls

A loop bound that MIR folds into a debug-info constant cannot be named in `invariant!`: `let n = 10; while i < n` fatally errors with "not a live variable", and under shadowing the name silently binds to the wrong variable

Support multi-crate projects (cargo)

Panic (`deref unbound var` / `borrowing unbound var`): `THRUST_ENUM_EXPANSION_DEPTH_LIMIT` truncates every binding form, not just enum unfolding, so a `&mut` two `enum` layers deep (`Result<Option<&mut T>, E>`) gets no flow binding and any use of it aborts the compiler