2026-02-24: Creusot 0.9.0

Author: Lysxia

content/2026-02-24.md

@@ -0,0 +1,156 @@
++++
+title = "Creusot 0.10.0: February update"
+date = 2026-02-24
+author = "The Creusot Team"
+description = "Assumptions, workspaces, and nightly shenanigans"
++++
+
+## What's new in Creusot?
+
+This February's release brings a couple of QOL improvements.
+
+### Assume (trusted asserts)
+
+The `proof_assert!` macro now supports the `#[trusted]` attribute.
+
+```rust
+#[trusted]
+proof_assert! { answer == 42 };
+```
+
+It removes the proof obligation that would come from the assertion,
+so it effectively becomes an *assumption* available to
+the rest of the program after it.
+
+We could have called it `assume!` or `proof_assume!`,
+but reusing `#[trusted]` makes it convenient to grep for all
+assumptions in a project.
+
+This is useful as a placeholder à la `todo!()`, letting you
+stub out parts of a proof while you're focusing on other aspects
+of it.
+
+### Wildcard patterns on integers
+
+In `match` expressions with integer patterns,
+the wildcard branch now remembers the values that
+the integer does **not** equal.
+
+```rust
+match n {
+    42 => proof_assert! { n == 42 },
+    _ => proof_assert! { n != 42 }, // FIXED
+}
+```
+
+Thanks to Eric Jackson for [the contribution](https://github.com/creusot-rs/creusot/pull/1899)!
+
+### Multi-package workspaces
+
+We added options to select packages in workspaces.
+
+The command line option `-p` (or `--package`) selects a package to build
+with `cargo creusot` and to run provers on with `cargo creusot prove`.
+This is basically the same option as in `cargo build`, but to call `why3find`
+and run provers, we must additionally find the output Coma files corresponding
+to these packages. 
+
+As the Creusot compiler is basically a modified `rustc`, the unit of compilation is a crate.
+A package defines multiple crates, and `cargo` does not build all of them by default:
+only libraries and binaries, excluding tests, examples, and benches.
+Creusot only supports that default target selection for now (that is libraries and binaries),
+until the need for others arises.
+
+You can also choose a default set of packages to build with `cargo creusot`,
+using the `default-member` field in the `[workspace.metadata.creusot]`
+section of your workspace `Cargo.toml`:
+
+```toml
+[workspace.metadata.creusot]
+default-members = ["PKG1", "PKG2"]
+```
+
+This falls back to the existing `default-member` field in `[workspace]`
+for regular `cargo build`. Having a separate field for Creusot lets you
+designate packages specifically as targets for formal verification,
+next to other buildable but unverified packages.
+
+### Story of a toolchain update
+
+Creusot depends on a nightly Rust toolchain. With this release,
+we upgraded our toolchain from nightly-2025-11-13 to nightly-2026-01-29.
+
+We do toolchain upgrades regularly to keep up with the fast-moving
+`rustc` API. Ideally we do this at the beginning of each release cycle
+to give time to potentially subtle issues to surface by the next release.
+
+This time, there was one change that required a bit of thinking to deal with:
+the orphan check now panics when it encounters an unnameable type
+(typically, a function type).
+
+#### The orphan check and unnameable types
+
+The orphan check is what enforces "trait coherence" in Rust: that there is at most
+one implementation of a trait for any given type. The orphan check basically answers
+the question "might another crate implement this trait `Tr` for this type `Ty`?"
+
+In `rustc`, this check is performed whenever you implement a trait.
+Since you must spell out the type for the `impl` block,
+there is normally no way to encounter an unnameable type there 
+(unnameable types are types of functions, closures, and coroutines).
+However `rustc` did have an experimental feature "`typeof`" which could
+cause the orphan check to encounter unnameable types, allegedly
+(I'm not familiar with the details).
+[That feature was removed](https://github.com/rust-lang/rust/pull/148256)
+in late November, and the now unreachable code in the orphan check
+that dealt with unnameable types was replaced with panics.
+
+In Creusot, we use the orphan check in the implementation of *type invariants*.
+This feature lets you specify a property that should be satisfied by all values of a type.
+For example, you can define a type of integers bounded by 42 as a `struct` with
+an `Invariant` impl:
+
+```rust
+struct Bounded42(usize);
+
+impl Invariant for Bounded42 {
+    #[logic]
+    fn invariant(self) -> bool {
+        pearlite! { self.0 <= 42usize } 
+    }
+}
+```
+
+All functions that take a `Bounded42` argument can assume the type invariant,
+and all functions that return a `Bounded42` must prove the type invariant.
+
+Any type `Ty` has a type invariant, which we determine as follows:
+
+- if there is an instance `Ty: Invariant`, that is a *user-provided* type invariant;
+- if there is definitely no such instance, then we fall back to a *structural* type invariant
+    derived from the type definition (it basically says that all fields satisfy
+    their type invariant);
+- if there is no instance `Ty: Invariant` in this context,
+    but we cannot rule it out definitely
+    (an instance may appear after instantiating some type variables,
+    possibly using implementations provided by an unknown crate),
+    then the type invariant is an undefined predicate.
+
+The orphan check is what distinguishes between the last two cases.
+Furthermore, because type invariants apply to all types, this also concerns
+unnameable types: for example if you pass a closure as an argument to a function,
+then Creusot will look for its type invariant, involving an orphan check.
+
+The update to the orphan check caused it to panic in this case.
+
+The fix is simple in hindsight: we replace unnameable types (function types)
+with the unit type `()` before invoking the orphan check.
+Indeed, these types should behave the same as far as the orphan check
+is concerned: both the unit type and function types from the current crate
+or its dependencies are "external types" from the point of view of a
+sibling or descendant crate.
+
+It is also possible to fix the orphan check in `rustc` itself to not
+panic in those cases even though they don't happen within `rustc`.
+But our workaround works and we just don't have an incentive to tinker
+with it further, at least until that becomes a bigger issue.

content/_index.md

@@ -0,0 +1,4 @@
++++
+sort_by = "date"
+paginate_by = 5
++++