Creusot Verification Skill

Creusot is a deductive verification tool for safe Rust. It translates Rust + Pearlite specifications to Why3/Coma and uses SMT solvers to prove correctness.

Quick Reference

Imports

use creusot_contracts::prelude::*;  // Current (creusot_std in newer versions)

Core Attributes

Attribute	Purpose
#[requires(P)]	Precondition - must hold when function called
#[ensures(P)]	Postcondition - guaranteed when function returns
#[invariant(P)]	Loop invariant - true at every iteration
#[variant(E)]	Termination measure - must decrease each iteration
#[logic]	Pure logical function (not callable from Rust)
#[predicate]	Logical function returning bool
#[trusted]	Skip verification (assume contract holds)

Key Operators

Operator	Meaning
x@	View/model operator - converts Rust value to logical type (e.g., i64 → Int)
^x	Final value of mutable borrow (prophecy)
*x	Current value of borrow
==>	Logical implication (in pearlite!{})
forall<x: T>	Universal quantifier (in pearlite!{})
exists<x: T>	Existential quantifier (in pearlite!{})

Logical Types

• Int - Unbounded mathematical integers (no overflow)
• Seq<T> - Mathematical sequences
• Set<T>, FSet<T> - Sets (infinite/finite)
• Map<K, V> - Mathematical functions
• Ghost<T> - Ghost values (exist only in proofs)
• Snapshot<T> - Immutable snapshot of a value

Workflow

Project Setup

cargo creusot new project-name
cd project-name

Verification Commands

cargo creusot              # Compile to Coma only
cargo creusot prove        # Compile and prove
cargo creusot prove -i     # Open Why3 IDE on failure
cargo creusot prove --ide-always  # Always open IDE

Writing Specifications

Basic Contract

#[requires(x@ < i64::MAX@)]           // Precondition
#[ensures(result@ == x@ + 1)]         // Postcondition
pub fn add_one(x: i64) -> i64 {
    x + 1
}

Loop Invariants

Loops MUST have invariants to be verified. The invariant must:

1. Hold on loop entry
2. Be preserved by each iteration
3. Combined with negated condition, imply postcondition

#[requires(n@ * (n@ + 1) / 2 <= u64::MAX@)]
#[ensures(result@ == n@ * (n@ + 1) / 2)]
pub fn sum_up_to(n: u64) -> u64 {
    let mut sum = 0;
    let mut i = 0;
    #[invariant(i@ <= n@)]
    #[invariant(sum@ == i@ * (i@ + 1) / 2)]
    while i < n {
        i += 1;
        sum += i;
    }
    sum
}

For Loop Pattern

For loops use produced variable (sequence of yielded elements):

#[invariant(sum@ * 2 == produced.len() * (produced.len() + 1))]
for i in 1..=n {
    sum += i;
}

Logic Functions and Predicates

#[predicate]
fn sorted<T: Ord>(s: Seq<T>) -> bool {
    pearlite! {
        forall<i: Int, j: Int> 0 <= i && i < j && j < s.len()
            ==> s[i] <= s[j]
    }
}

#[logic]
fn sum_seq(s: Seq<Int>) -> Int {
    if s.len() == 0 { 0 }
    else { s[0] + sum_seq(s.tail()) }
}

Mutable References with Prophecies

Use ^ (final) to specify the value at end of borrow lifetime:

#[ensures(^x == *x + 1)]  // Final value equals current + 1
pub fn increment(x: &mut i32) {
    *x += 1;
}

Ghost Code

Ghost code exists only during verification:

let old_v = ghost!(v);  // Snapshot for invariant
#[invariant([email protected]_of(old_v@))]

Type Invariants

pub struct OPair(pub u64, pub u64);

impl Invariant for OPair {
    #[logic]
    fn invariant(self) -> bool {
        pearlite! { self.0 <= self.1 }
    }
}

Common Patterns

Overflow Prevention

Always specify bounds to prevent overflow verification failures:

#[requires(x@ + y@ <= i64::MAX@)]
#[requires(x@ + y@ >= i64::MIN@)]

Vec Operations

#[requires(i@ < [email protected]())]           // Bounds check
#[ensures(result@ == v@[i@])]        // Element access
#[ensures((^v)@.len() == [email protected]())]  // Length preserved

Termination Variants

#[logic]
#[variant(x)]  // x must decrease (implement WellFounded)
#[requires(x >= 0)]
fn factorial(x: Int) -> Int {
    if x == 0 { 1 } else { x * factorial(x - 1) }
}

Debugging Failed Proofs

1. Run with IDE: cargo creusot prove -i verif/[FILE].coma
2. Check unproved goals: Yellow = hypothesis, Green = proved
3. Common issues:
   • Missing loop invariant clause
   • Invariant too weak (doesn't imply postcondition)
   • Missing overflow bounds
   • SMT solver timeout (try simplifying formulas)
4. Avoid division in invariants - SMT solvers struggle; multiply both sides instead

File Locations

• Coma output: verif/[crate]_rlib/[module]/[function].coma
• Config: why3find.json, Cargo.toml

Further Reference

For detailed Pearlite syntax, common specification patterns, and advanced features, see references/pearlite-syntax.md.