Crate creusot_contracts 

The “standard library” of Creusot.

To start using Creusot, you should always import that crate. The recommended way is to have a glob import:

use creusot_contracts::prelude::*;

Writing specifications

To start writing specification, use the requires and ensures macros:

use creusot_contracts::prelude::*;

#[requires(x < i32::MAX)]
#[ensures(result@ == x@ + 1)]
fn add_one(x: i32) -> i32 {
    x + 1
}

For a more detailed explanation, see the guide.

Module organization

1. Core features of Creusot

   • invariant: Type invariants
   • macros: #[requires], #[ensures], etc.
   • resolve: Resolve mutable borrows
   • snapshot: Snapshots

2. logic: Logical structures used in specifications

3. ghost: Ghost code

4. std: Specifications for the std crate

5. cell: Interior mutability

6. prelude: What you should import before doing anything with Creusot

Modules

cell

Interior mutability

ghost

Definitions for ghost code

invariant

Type invariants

logic

Definitions for pearlite code

macros

Specification are written using these macros

model

Logical models of types: View and DeepModel

peano

Peano integers

prelude

Re-exports available under the creusot_contracts namespace

resolve

Resolve mutable borrows

snapshot

Definition of Snapshot

std

Specifications for the std crate

Macros

ord_laws_impl

A macro to easily implements the various #[logic(law)]s of OrdLogic.

vec

Creusot-friendly replacement of vec!