Creusot 0.14.0 adds partial order specs, snapshot VCs, and rust-analyzer navigation

Partial orders

Creusot 0.14.0 is a release of the formal verification tool for Rust. The release notes say that partial orders are a small selection of new features, with more items in the full changelog.

Earlier versions restricted the specification of PartialOrd to total orders. Since version 0.13.0, that restriction was relaxed to allow partial orders. The previous total order trait OrdLogic was based on cmp_log, the logic counterpart to cmp, which returns an Ordering. That made totality implicit: any two elements had to compare as Less, Equal, or Greater.

The new strict partial order trait PartialOrdLogic is instead based on lt_log, a boolean comparison function, with laws for irreflexivity and transitivity. Totality is now a separate law in OrdLogic, called lt_log_total, which ensures self < other || self == other || other < self. The developers note that none of the existing proofs were affected and that the automated provers handled the change.

Verification conditions for snapshots

Creusot now generates verification conditions for snapshots, which are logic expressions embedded in Rust programs. This improves the use of lemma functions, an idiom in verification tools similar to Creusot.

A lemma can be written as a logic function with requires and ensures clauses, amounting to the proposition that hyp(x) implies concl(x) for all x. Calling that lemma inside a snapshot! is now translated into an assertion that hyp(n) is true and an assumption that concl(n) is true, specialized to the argument n. This avoids asking provers to instantiate the universal quantifier.

The notes contrast this with calling a regular program lemma. That earlier style also has requires and ensures clauses, but it introduces a Rust function call and must pass the borrow checker, which may require boilerplate when the goal is only to state facts. Snapshots are erased, so they exist only for formal proof. Verification conditions were not generated for snapshot! before because they were not needed for soundness, though they help catch specification mistakes sooner, such as out of bounds indexing, and enable new techniques.

rust-analyzer support

Go to definition now works in Pearlite specifications. To enable this, specification macros such as requires, ensures, proof_assert!, and snapshot! are expanded for rust-analyzer instead of being erased as they are in normal compilation. Creusot provides guide settings for the needed rust-analyzer options.

The expanded Pearlite code is not meant for rustc because it passes the type checker but not the borrow checker. This was not a problem because rust-analyzer does not perform borrow checking. The remaining issue was that tokens from Pearlite macros carried spans that were too coarse. In an example, a + b expands to AddLogic::add_logic(a, b), and every generated token carried the span of the whole expression. As a result, Go to definition from anywhere inside that expression looked up definitions for creusot_std, logic, ops, AddLogic, and add_logic.

The fix gives add_logic the span of + and gives the other identifiers a zero-width span, which rust-analyzer ignores. Sarah Quiñones is credited with figuring this out. The developers say navigating specifications in Creusot is much more pleasant as a result.

Questions

Readers with questions about Creusot can join the project Zulip channel or open a discussion or issue in the Creusot repository.

Sources: Lobsters