From 0a91412a513f7ff259cb6834e82dd37fe8ce4e6e Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Sat, 30 Nov 2024 21:24:12 +0100 Subject: [PATCH] Document the top-level of `creusot_contracts`, and macros --- creusot-contracts/src/lib.rs | 238 +++++++++++++++++++++++++++++++---- 1 file changed, 215 insertions(+), 23 deletions(-) diff --git a/creusot-contracts/src/lib.rs b/creusot-contracts/src/lib.rs index 2e6c85a2d..acabe8249 100644 --- a/creusot-contracts/src/lib.rs +++ b/creusot-contracts/src/lib.rs @@ -1,3 +1,28 @@ +//! The "standart 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::*; +//! ``` +//! +//! # Writing specifications +//! +//! To start writing specification, use the [`requires`] and [`ensures`] macros: +//! +//! ``` +//! use creusot_contracts::*; +//! +//! #[requires(x < i32::MAX)] +//! #[ensures(result@ == x@ + 1)] +//! fn add_one(x: i32) -> i32 { +//! x + 1 +//! } +//! ``` +//! +//! For a more detailled explanation, see the [guide](https://creusot-rs.github.io/creusot/guide). + #![cfg_attr( creusot, feature(unsized_locals, fn_traits), @@ -29,13 +54,64 @@ extern crate creusot_contracts_proc as base_macros; #[cfg(not(creusot))] extern crate creusot_contracts_dummy as base_macros; -mod macros { +/// Specification are written using these macros +pub mod macros { /// A pre-condition of a function or trait item + /// + /// The inside of a `requires` may look like Rust code, but it is in fact + /// [pearlite](https://creusot-rs.github.io/creusot/guide/pearlite). + /// + /// # Example + /// + /// ``` + /// # use creusot_contracts::*; + /// #[requires(x@ == 1)] + /// fn foo(x: i32) {} + /// ``` pub use base_macros::requires; /// A post-condition of a function or trait item + /// + /// The inside of a `ensures` may look like Rust code, but it is in fact + /// [pearlite](https://creusot-rs.github.io/creusot/guide/pearlite). + /// + /// # Example + /// + /// ``` + /// # use creusot_contracts::*; + /// #[ensures(result@ == 1)] + /// fn foo() -> i32 { 1 } + /// ``` pub use base_macros::ensures; + /// Create a new [`Snapshot`](crate::Snapshot) object. + /// + /// The inside of `snapshot` may look like Rust code, but it is in fact + /// [pearlite](https://creusot-rs.github.io/creusot/guide/pearlite). + /// + /// # Example + /// + /// ``` + /// # use creusot_contracts::*; + /// let mut x = 1; + /// let s = snapshot!(x); + /// x = 2; + /// proof_assert!(*s == 1i32); + /// ``` + /// + /// # `snapshot!` and ownership + /// + /// Snapshots are used to talk about the logical value of an object, and as such + /// they carry no ownership. This means that code like this is perfectly fine: + /// + /// ``` + /// # use creusot_contracts::{*, vec}; + /// let v: Vec = vec![1, 2]; + /// let s = snapshot!(v); + /// assert!(v[0] == 1); // ok, `s` does not have ownership of `v` + /// drop(v); + /// proof_assert!(s[0] == 1i32); // also ok! + /// ``` pub use base_macros::snapshot; /// Opens a 'ghost block'. @@ -46,13 +122,24 @@ mod macros { /// Note that ghost blocks are subject to some constraints, that ensure the behavior /// of the code stays the same with and without ghost blocks: /// - They may not contain code that crashes or runs indefinitely. In other words, - /// they can only call [`pure`] functions. + /// they can only call [`pure`] functions. /// - All variables that are read in the ghost block must either be [`Copy`], or a - /// [`GhostBox`](crate::ghost::GhostBox). + /// [`GhostBox`](crate::ghost::GhostBox). /// - All variables that are modified in the ghost block must be - /// [`GhostBox`](crate::ghost::GhostBox)s. + /// [`GhostBox`](crate::ghost::GhostBox)s. /// - The variable returned by the ghost block will automatically be wrapped in a - /// [`GhostBox`](crate::ghost::GhostBox). + /// [`GhostBox`](crate::ghost::GhostBox). + /// + /// # Example + /// + /// ``` + /// # use creusot_contracts::*; + /// let x = 1; + /// let mut g = ghost!(Seq::new()); // g is a zero-sized variable at runtime + /// ghost! { + /// g.push_back_ghost(x); + /// }; + /// ``` pub use base_macros::ghost; /// Indicate that the function terminates: fullfilling the `requires` clauses @@ -90,17 +177,39 @@ mod macros { pub use base_macros::pure; /// A loop invariant - /// The first argument should be a name for the invariant - /// The second argument is the Pearlite expression for the loop invariant + /// + /// The inside of a `invariant` may look like Rust code, but it is in fact + /// [pearlite](https://creusot-rs.github.io/creusot/guide/pearlite). + /// + /// # Produced + /// + /// If the loop is a `for` loop, you have access to a special variable `produced`, that + /// holds a [sequence](crate::Seq) of all the (logical representations of) items the + /// iterator yielded so far. + /// + /// # Example + /// + /// ``` + /// # use creusot_contracts::*; + /// let mut v = Vec::new(); + /// // For annoying reasons, examples cannot use invariants. Please imagine that they are uncommented :) + /// // #[invariant(v@.len() == produced.len())] + /// // #[invariant(forall 0 <= j && j < produced.len() ==> v@[j]@ == j)] + /// for i in 0..10 { + /// v.push(i); + /// } + /// ``` pub use base_macros::invariant; /// Declares a trait item as being a law which is autoloaded as soon another /// trait item is used in a function pub use base_macros::law; - /// Declare a function as being a logical function, this declaration must be pure and - /// total. It cannot be called from Rust programs, but in exchange it can use logical - /// operations and syntax with the help of the [`pearlite!`] macro. + /// Declare a function as being a logical function + /// + /// This declaration must be pure and total. It cannot be called from Rust programs, + /// but in exchange it can use logical operations and syntax with the help of the + /// [`pearlite!`] macro. /// /// # `prophetic` /// @@ -116,9 +225,11 @@ mod macros { /// called from a regular [`logic`] or [`predicate`] function. pub use base_macros::logic; - /// Declare a function as being a logical function, this declaration must be pure and - /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can - /// use logical operations and syntax with the help of the [`pearlite!`] macro. + /// Declare a function as being a predicate + /// + /// This declaration must be pure and total. It cannot be called from Rust programs, + /// but in exchange it can use logical operations and syntax with the help of the + /// [`pearlite!`] macro. /// /// It **must** return a boolean. /// @@ -136,28 +247,89 @@ mod macros { /// called from a regular [`logic`] or [`predicate`] function. pub use base_macros::predicate; - /// Inserts a *logical* assertion into the code. This assertion will not be checked at runtime - /// but only during proofs. However, it has access to the ghost context and can use logical operations - /// and syntax. + /// Inserts a *logical* assertion into the code + /// + /// This assertion will not be checked at runtime but only during proofs. However, + /// it can use [pearlite](https://creusot-rs.github.io/creusot/guide/pearlite) syntax. + /// + /// # Example + /// + /// ``` + /// # use creusot_contracts::{*, vec}; + /// let x = 1; + /// let v = vec![x, 2]; + /// let s = snapshot!(v); + /// proof_assert!(s[0] == 1i32); + /// ``` pub use base_macros::proof_assert; - /// Instructs Pearlite to ignore the body of a declaration, assuming any contract the declaration has is + /// Instructs Creusot to ignore the body of a declaration, assuming any contract the declaration has is /// valid. + /// + /// # Example + /// + /// ``` + /// # use creusot_contracts::*; + /// #[trusted] // this is too hard to prove :( + /// #[ensures(result@ == 1)] + /// fn foo() -> i32 { + /// // complicated code... + /// # 1 + /// } + /// ``` + /// + /// In practice you should strive to use this as little as possible. pub use base_macros::trusted; - /// Declares a variant for a function, this is primarily used in combination with logical functions + /// Declares a variant for a function + /// + /// This is primarily used in combination with recursive logical functions. + /// /// The variant must be an expression which returns a type implementing /// [`WellFounded`](crate::WellFounded). + /// + /// # Example + /// + /// ``` + /// # use creusot_contracts::*; + /// #[logic] + /// #[variant(x)] + /// #[requires(x >= 0)] + /// fn recursive_add(x: Int, y: Int) -> Int { + /// if x == 0 { + /// y + /// } else { + /// recursive_add(x - 1, y + 1) + /// } + /// } + /// ``` pub use base_macros::variant; - /// Enables Pearlite syntax, granting access to Pearlite specific operators and syntax + /// Enables [pearlite](https://creusot-rs.github.io/creusot/guide/pearlite) syntax, granting access to Pearlite specific operators and syntax + /// + /// This is meant to be used in [`logic`] functions. + /// + /// # Example + /// + /// ``` + /// # use creusot_contracts::*; + /// #[predicate] + /// fn all_ones(s: Seq) -> bool { + /// // Allow access to `forall` and `==>` among other things + /// pearlite! { + /// forall 0 <= i && i < s.len() ==> s[i] == 1 + /// } + /// } + /// ``` pub use base_macros::pearlite; /// Allows specifications to be attached to functions coming from external crates + /// /// TODO: Document syntax pub use base_macros::extern_spec; /// Allows specifying both a pre- and post-condition in a single statement. + /// /// Expects an expression in either the form of a method or function call /// Arguments to the call can be prefixed with `mut` to indicate that they are mutable borrows. /// @@ -165,16 +337,36 @@ mod macros { /// `mut` replaced by `*` in the `requires` and `^` in the ensures. pub use base_macros::maintains; - /// Allows the body of a logical definition to be made visible to provers. An optional visibility modifier can be - /// provided to restrict the context in whcih the obdy is opened. - /// By default, bodies are *opaque*: they are only visible to definitions in the same module (like `pub(self)` for visibility). + /// Allows the body of a logical definition to be made visible to provers + /// + /// By default, bodies are *opaque*: they are only visible to definitions in the same + /// module (like `pub(self)` for visibility). + /// An optional visibility modifier can be provided to restrict the context in which + /// the body is opened. /// /// A body can only be visible in contexts where all the symbols used in the body are also visible. /// This means you cannot `#[open]` a body which refers to a `pub(crate)` symbol. + /// + /// # Example + /// + /// ``` + /// mod inner { + /// use creusot_contracts::*; + /// #[logic] + /// #[open(self)] + /// #[ensures(result == x + 1)] + /// pub(super) fn foo(x: Int) -> Int { + /// // ... + /// # x + 1 + /// } + /// } + /// + /// // The body of `foo` is not visible here, only the `ensures`. + /// ``` pub use base_macros::open; /// This attribute can be used on a function or closure to instruct Creusot not to ensure as a postcondition that the - /// return value of the function satisfies its type invariant. + /// return value of the function satisfies its [type invariant](crate::Invariant). pub use base_macros::open_inv_result; }