Document the top-level of creusot_contracts, and macros

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<i32> = 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([email protected]() == produced.len())]
+    /// // #[invariant(forall<j: Int> 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,45 +247,126 @@ 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<Int>) -> bool {
+    ///     // Allow access to `forall` and `==>` among other things
+    ///     pearlite! {
+    ///         forall<i: Int> 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.
     ///
     /// Generates a `requires` and `ensures` clause in the shape of the input expression, with
     /// `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;
 }