Creusot 0.14.0 release - Contracts for Rust, formally proved
15 points by lyxia
15 points by lyxia
This looks similar in goals to Verus. Is there a comparison somewhere of the two approaches?
I'm not aware of a comprehensive comparison. A recent paper about Creusot uses features first published in Verus's first paper, so it gives some comparison but it is quite technical.
The most distinguishing feature in Creusot is its first-class support for mutable borrows. It allows you to directly specify functions like index_mut(&mut [T], usize) -> Option<&mut T>. Other tools like Verus have historically had trouble with functions that return mutable borrows or wrap them in data structures (like Option), although I hear they have been catching up fast.
Creusot also supports using multiple SMT solvers, leveraging their respective strengths. On the other hand Verus is able to tune its goals to their solver to a greater extent. Verus has a more integrated architecture, which allows it, admittedly, to have nice IDE features and be quite fast. Creusot is really two tools in a trenchcoat (a custom Rust compiler and Why3 as the proof backend), and it takes more work to make the trenchcoat long enough to cover both well.
One last difference is the syntax. In Creusot, the syntax of programs is "Rust with attributes". Verus supports something similar, but the main advertised workflow is to write all your code in a verus! macro which thus takes more liberties in extending the syntax of Rust. How this affects usage is still up in the air.
That's a really gnarly problem to solve in that paper, but the solutions are quite legible.
#[ensures(forall<z> uf.in_domain(z) ==> (^uf).root(z) ==
if uf.root(z) == uf.root(x) ||
uf.root(z) == uf.root(y) {
result
} else { uf.root(z) })]
... is clear, considering what it's stating.
I'm not a super heavy rust guy, but this approach is fascinating to me:
pub fn union<T>(mut uf: Ghost<&mut UF<T>>, x: Elem<T>, y: Elem<T>) -> Elem<T>;
Using Ghost<T> as kind of a replacement for a manual PCM to construct a bespoke resource algebra (is that what's happening here? If i'm wrong, enlighten me) is very clever.
There is a resource algebra construction in Verus, it has most of the combinators that Iris provides! It usually goes into a Tracked<T>.
Ghost and Tracked are just ways to bridge the exec and proof worlds.
There is work in progress syntax work to change the ways that Ghost and Tracked work, so you could potentially augment functions with tracked and ghost arguments without changing the function signature in the unverified call site.
I'm not a formal methods practicioner (yet), I'm more of a fanboy right now, so this may be a silly question, but what is the benefit of a total resource algebra over a PCM? Why does it make your life easier if you're not trying to avoid partial functions for the sake of CIC?
I would guess it has something to do with automation, but I wouldn't know.
Resource algebras are still partial, the difference is the existence of a unit value (PCMs have them, resource algebras don't). The main problem of that is that unit values sometimes don't compose well.