### Quick Installation using INSTALL Script

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/installation.md

Clone the repository and run the INSTALL script for a quick setup. This script handles the installation of Creusot and its accompanying tools, including setting up a local Opam switch.

```sh
git clone https://github.com/creusot-rs/creusot
cd creusot
./INSTALL
```

--------------------------------

### Creusot Setup Commands

Source: https://github.com/creusot-rs/creusot/blob/master/CHANGELOG.md

Manage Creusot's installation, including checking status, installing, or getting help. Supports external prover configurations.

```bash
Setup and manage Creusot's installation

Usage: creusot setup <COMMAND>

Commands:
  status   Show the current status of the Creusot installation
  install  Setup Creusot or update an existing installation
  help     Print this message or the help of the given subcommand(s)

Options:
  -h, --help  Print help
```

--------------------------------

### Setup Development Environment

Source: https://github.com/creusot-rs/creusot/blob/master/CONTRIBUTING.md

Initialize the Creusot testsuite with the global configuration managed by `cargo creusot setup`. Ensure `./INSTALL` has been run.

```sh
eval $(cargo run --bin dev-env)
```

--------------------------------

### Manual Installation: Cargo Install

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/installation.md

Install the core Creusot components using Cargo. This includes installing the `cargo-creusot` binary, the `creusot-rustc` compiler wrapper, and the Creusot prelude.

```sh
# Install cargo-creusot
cargo install --path cargo-creusot

# Install creusot-rustc
TOOLCHAIN=$(grep "nightly-[0-9-]*" --only-matching rust-toolchain)
cargo install --path cargo-creusot --root $XDG_DATA_HOME/creusot/toolchain/$TOOLCHAIN/bin

# Install the Creusot prelude
cargo run --bin prelude-generator
mkdir -p $XDG_DATA_HOME/share/why3find
cp -rT target/creusot/packages $XDG_DATA_HOME/share/why3find/packages

# Copy why3find.json in the installation directory
cp cargo-install/why3find.json $XDG_DATA_HOME/creusot/why3find.json
```

--------------------------------

### Install cargo-release Tool

Source: https://github.com/creusot-rs/creusot/blob/master/CONTRIBUTING.md

Install the cargo-release tool, which automates various release tasks. This is a prerequisite for making a release.

```shell
cargo install cargo-release
```

--------------------------------

### Install Creusot

Source: https://github.com/creusot-rs/creusot/blob/master/README.md

Install Creusot after cloning the repository. This command assumes you are in the 'creusot' directory.

```sh
./INSTALL
```

--------------------------------

### Verify Creusot Installation

Source: https://github.com/creusot-rs/creusot/blob/master/README.md

Check if the Creusot installation was successful by running the help command.

```sh
cargo creusot --help
```

--------------------------------

### Lemma with Proof Body

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/logic_functions/lemma_law.md

Define a lemma with a body to guide the proof process. This example uses a conditional proof and an assertion.

```rust
#[logic]
#[requires(x + y > 0)]
#[ensures(x > 0 || y > 0)]
fn add_gt_zero(x: Int, y: Int) {
    if x > 0 {} else {
        proof_assert!(y >= x + y);
    }
}
```

--------------------------------

### Simple Final Reborrow Example

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/representation_of_types/mutable_borrows.md

Demonstrates a basic final reborrow where the original borrow is not used after the reborrow. This is a common and sound scenario.

```rust
let mut i = 0;
let borrow = &mut i;
let reborrow = &mut *borrow;
// Don't use `borrow` afterward
proof_assert!(reborrow == borrow);
```

--------------------------------

### Clone Creusot Repository

Source: https://github.com/creusot-rs/creusot/blob/master/README.md

Clone the Creusot repository and navigate into the directory to begin installation.

```sh
git clone https://github.com/creusot-rs/creusot
cd creusot
```

--------------------------------

### Nix Flake Configuration for Project Integration

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/installation.md

A sample `flake.nix` file demonstrating how to integrate Creusot as a dependency within your project using flake-parts. This setup provides a development environment with Creusot and other tools like `clippy` and `rust-analyzer`.

```nix
{ 
  inputs = {
    # Both `nixpkgs` and `flake-parts` are pinned to the same version as Creusot's
    nixpkgs.follows = "creusot/nixpkgs";
    flake-parts.follows = "creusot/flake-parts";

    creusot.url = "github:creusot-rs/creusot";
  };

  outputs =
    inputs@{
      creusot,
      flake-parts,
      nixpkgs,
      self,
    }:
    flake-parts.lib.mkFlake { inherit inputs; } {
      systems = [ 
        "aarch64-darwin"
        "x86_64-linux"
      ];

      perSystem =
        {
          pkgs,
          system,
          ...
        }:
        {
          # `pkgs` will also contain the `creusot` set, thanks to Creusot's overlay
          _module.args.pkgs = import nixpkgs {
            inherit system;
            overlays = [ creusot.overlays.default ];
          };

          # `nix fmt`
          formatter = pkgs.nixfmt-tree;

          # `nix develop`
          devShells.default = pkgs.mkShell {
            packages = [ 
              # `mkCreusotWrapped` produces a wrapped version of Creusot, along with all its dependencies (similar to `clang`).
              # The `isFree` argument allows switching between the free and non-free version of the solver `alt-ergo`.
              (pkgs.creusot.mkCreusotWrapped { 
                cargo = pkgs.cargo;  # Otherwise, the cargo needed to build Creusot will be used
                isFree = true;
              })

              # Further packages could be added
              pkgs.clippy
              pkgs.rust-analyzer
              pkgs.rustfmt
              # ...
            ];
          };
        };
    };
}

```

--------------------------------

### Logic Function Termination Example

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/termination.md

Demonstrates a non-terminating logic function that would lead to unsoundness if not checked.

```rust
#[logic]
#[ensures(false)]
fn falso() {
    falso()
}
```

--------------------------------

### Structural Invariants Examples

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/type_invariants.md

Provides examples of structural invariants for various Rust types, showing how Creusot derives invariants automatically based on type definitions.

```rust
struct Foo { f: Bar }

// Invariant `inv(x.f)`
```

```rust
enum Foo { A(Bar), B(Baz) }

// Invariant `match x { A(y) => inv(y), B(z) => inv(z) }`
```

```rust
Vec<Foo>

// Invariant `inv(x[0]) && ... && inv(x[x.len()-1])`
```

--------------------------------

### Ghost Data Structure Example

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/ghost.md

Illustrates a potential structure for managing ghost data, including a `Token` and a `Data` struct. The `Data` struct shows methods for creation and interaction with ghost data using `Ghost<Token>` access tokens.

```rust
struct Token;

struct Data {
    // ...
}

impl Data {
    fn new() -> (Data, Ghost<Token>) { /* */ }
    fn read(&self, token: &Ghost<Token>) -> T { /* */ }
    fn write(&self, t: T, token: &mut Ghost<Token>) { /* */ }
}
```

--------------------------------

### Create a new Creusot project

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/quickstart.md

Use this command to generate a new Rust project with Creusot integration. It sets up the basic structure and includes an example function with a contract.

```bash
cargo creusot new project-name
```

--------------------------------

### Unsound Code Example

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/representation_of_types/mutable_borrows.md

This example illustrates the type of unsound code that Creusot's mutable borrow model aims to prevent by using prophecies and final reborrows.

```rust
pub fn unsound() {
    let mut x: Snapshot<bool> = snapshot! { true };
    let xm: &mut Snapshot<bool> = &mut x;
    let b: &mut Snapshot<bool> = &mut *xm;
    let bg: Snapshot<&mut Snapshot<bool>> = snapshot! { b };
    proof_assert! { ***bg == true && *^*bg == true };
    let evil: &mut Snapshot<bool> = &mut *xm;
    proof_assert! { (evil == *bg) == (*^evil == true) };
    *evil = snapshot! { if evil == *bg { false } else { true } };
    proof_assert! { **evil == !*^evil };
    proof_assert! { **evil == !**evil };
}
```

--------------------------------

### Example Creusot function with contract

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/quickstart.md

An example of a Rust function annotated with Creusot's contract annotations (`requires` and `ensures`). This function adds one to an i64, with a precondition ensuring the input is not `i64::MAX`.

```rust
// src/lib.rs
use creusot_std::prelude::*;

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

--------------------------------

### Nix Shell for Interactive Subshell

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/installation.md

Enter an interactive Nix subshell that contains the Creusot project. This method is useful if you are using Nix and do not need a persistent installation.

```sh
nix shell "github:creusot-rs/creusot"
```

--------------------------------

### Loop Invariant Example

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/tutorial.md

Demonstrates the use of a loop invariant to assert a condition that holds true at every iteration of a while loop.

```rust
    #[invariant(i@ <= n@)]
    while i < n {
        i += 1;
        sum += i;
    }
```

--------------------------------

### Example: Verifying Functions with Ghost Code

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/erasure.md

Demonstrates how `#[erasure]` is used to verify functions that have been modified with Creusot annotations like ghost arguments and assertions. It shows the transformation process from the verified function (`h2`, `f2`, `g2`) back to the original function's behavior (`h`, `f`, `g`).

```rust
fn h(x: A) {
    g(f(x))
}

fn f(x: A) -> B { /* ... */ }
fn g(y: B) { /* ... */ }
```

```rust
#[erasure(h)]
#[requires(...)]
#[ensures(...)]
fn h2(x: A) {
    let (y, i) = f2(x);
    ghost!(...);
    g2(y, i)
}

#[erasure(f)]
fn f2(x: A) -> (B, Ghost<I>) { /* ... */ }

#[erasure(g)]
fn g2(y: B, i: Ghost<I>) { /* ... */ }
```

```rust
fn h2(x: A) {
    let (y, _) = f2(x);
    g2(y, _)
}
```

```rust
fn h2(x: A) {
    let y = f(x);
    g(y)
}
```

```rust
fn h(x: A) {
    let y = f(x);
    g(y)
}
```

--------------------------------

### Dependency Recursion Check Example

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/termination.md

Illustrates a scenario where a crate's implementation relies on a trait method from a dependency, leading to a termination check error because the dependency's function bodies are not visible.

```rust
// dependency/src/lib.rs
trait Tr {
    fn f();
}
fn g<T: Tr>() {
    // It does not matter if `<T as Tr>::f` is called or not, since we cannot see it
}

// lib.rs
impl Tr for i32 {
    fn f() {
        g::<i32>(); // Error !
    }
}
```

--------------------------------

### Ensures Clause with Irrefutable Pattern Binding

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/basic_concepts/requires_ensures.md

This example demonstrates using an irrefutable pattern within the `ensures` clause's closure notation to bind the result. This is shown with a function returning a tuple, asserting that the first element is less than or equal to the second.

```rust
#[ensures(|(fst, snd)| fst <= snd)]
pub fn apair() -> (i32, i32) {
    (0, 1)
}
```

--------------------------------

### Ensures Clause with Explicit Result Binding

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/basic_concepts/requires_ensures.md

This example shows an alternative syntax for the `ensures` clause where the result is explicitly bound using closure notation `|resultat|`. This can be useful for more complex assertions involving the return value.

```rust
#[ensures(|resultat| v@[0] == resultat)]
```

--------------------------------

### Launch Why3 IDE for All Functions

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/tutorial.md

Use this command to launch the Why3 IDE and inspect the proof state for all unverified functions in the project.

```bash
cargo creusot -i
```

--------------------------------

### Replay existing proof and open Why3 IDE

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/quickstart.md

This command skips the proof search and reuses the existing `proof.json` file. It's combined with `--ide-always` to open the Why3 IDE with the replayed proof results.

```bash
cargo creusot verif/[COMA_FILE] --ide-always --replay
```

--------------------------------

### Launch Why3 IDE

Source: https://github.com/creusot-rs/creusot/blob/master/CONTRIBUTING.md

Open the Why3 IDE for a specific test file to inspect or fix proofs.

```sh
./ide tests/should_succeed/cell/01
```

--------------------------------

### Launch Why3 IDE for a Specific Function

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/tutorial.md

Launch the Why3 IDE and focus on the proof state for a specific function by providing the path to its generated Coma file.

```bash
cargo creusot -i verif/creusot_tutorial_rlib/creusot_tutorial/sum_up_to.coma
```

--------------------------------

### Initialize a new Creusot project

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/command_line_interface.md

Use this command to create a new Rust project with Creusot support or to update an existing project for Creusot verification. It adds necessary dependencies and configuration files.

```bash
cargo creusot init [<NAME>] [--main]
```

--------------------------------

### Run Why3 IDE on Coma File or Session

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/command_line_interface.md

Launches the Why3 IDE for a specified Coma file or `why3session.xml`. This is intended for expert use or troubleshooting.

```bash
cargo creusot why3 ide <COMA_FILE|why3session.xml>
```

--------------------------------

### Legacy workflow: Launch Why3 IDE

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/quickstart.md

In the legacy workflow, this command launches the Why3 IDE with the necessary options to load Coma files. You must ensure the Coma files are up-to-date manually.

```bash
cargo creusot why3 ide [FILE]
```

--------------------------------

### Annotate Private Function for Erasure Check

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/erasure.md

Example of how to use the `private` keyword with `#[erasure]` to check a private function.

```rust
#[erasure(private crate_name::path::to::f)]
```

--------------------------------

### Run only the proof search

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/quickstart.md

This flag executes only the Why3find proof search on existing Coma files, skipping the compilation step. It's useful for re-running proofs without recompiling.

```bash
cargo creusot --only=prove
```

--------------------------------

### Perlite Exists Expression Translation

Source: https://github.com/creusot-rs/creusot/blob/master/ARCHITECTURE.md

An example of a Pearlite expression using `exists` being translated into a HOAS-like style in Rust using stub functions.

```rust
creusot_std :: stubs :: exists (| i : Int | { i == 0 })
```

--------------------------------

### Run proof search on a specific Coma file

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/quickstart.md

This command allows you to run the Why3find proof search on a specific Coma file within the `verif` directory. You can specify multiple files.

```bash
cargo creusot [--only=prove] verif/[COMA_FILE]
```

--------------------------------

### Annotate Ghost Function for Erasure

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/erasure.md

Example of annotating a ghost function using `#[erasure(_)]`. These functions are eraseable and typically used with ghost blocks.

```rust
#[trusted]
#[erasure(_)]
fn split<T, U>(g: Ghost<(T, U)>) -> (Ghost<T>, Ghost<U>) { /* ... */ }
```

--------------------------------

### Build Documentation with Creusot

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/command_line_interface.md

Builds documentation, including contracts and logic functions, using a variant of `cargo doc`.

```bash
cargo creusot doc
```

--------------------------------

### Non-Final Reborrow Due to Subsequent Use

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/representation_of_types/mutable_borrows.md

This example shows a non-final reborrow because the original borrow is used after the reborrow, making the prophecy unrelated.

```rust
let mut i = 0;
let borrow = &mut i;
let reborrow = &mut *borrow;
*borrow = 1;
proof_assert!(borrow == reborrow); // unprovable
                                   // Here the prophecy of `borrow` is `1`,
                                   // which is a value completely unrelated to the reborrow.
```

--------------------------------

### Using a Lemma Before Importing

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/logic_functions/lemma_law.md

Demonstrates that a lemma like commutativity must be explicitly imported into the proof context before its properties can be used.

```rust
#[logic]
fn foo<T: Commutative>(x: T, y: T) {
    let z = x.op(y);
    // let _ = x.commutative(y);
    proof_assert!(z == y.op(x)); // does not work without uncommenting the above line
}
```

--------------------------------

### Rust Function Accessing Slice Element

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/basic_concepts/requires_ensures.md

This is a basic Rust function that accesses the first element of a slice. It serves as an example for introducing preconditions.

```rust
fn head(v: &[i32]) -> i32 {
    v[0]
}
```

--------------------------------

### Mutual Recursion via Traits - Compiles

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/termination.md

This example compiles because Creusot checks recursion at instantiation time. The call to `g::<T>()` is generic and not yet instantiated.

```rust
trait Tr {
    fn f();
}
fn g<T: Tr>() {
    <T as Tr>::f();
}
```

--------------------------------

### Verify push_back in Linked List

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/tutorial/linked_list.md

This snippet demonstrates the verification of the `push_back` function for a linked list. It shows how to correctly use `Perm::from_box`, `Perm::as_mut`, and `ghost!` blocks for managing pointer permissions and ghost state.

```rust
pub fn push_back(&mut self, value: T) {
    let link = Box::new(Link { value, next: std::ptr::null() });
    let (link_ptr, link_own) = Perm::from_box(link);              // 1
    if self.last.is_null() {
        self.first = link_ptr;
        self.last = link_ptr;
    } else {
        let link_last = unsafe {
            Perm::as_mut(
                self.last as *mut Link<T>,
                ghost! {                                          // 2
                    let off = self.seq.len_ghost() - 1int;
                    self.seq.get_mut_ghost(off).unwrap()
                },
            )
        };
        link_last.next = link_ptr;
        self.last = link_ptr;
    }
    ghost! { self.seq.push_back_ghost(link_own.into_inner()) };   // 3
}
```

--------------------------------

### Pearlite Logical Implication Examples

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/pearlite.md

Demonstrates the usage of the logical implication operator (==>) in Pearlite. Note that 'true ==> false' is an invalid implication.

```rust
proof_assert!(true ==> true);
proof_assert!(false ==> true);
proof_assert!(false ==> false);
// proof_assert!(true ==> false); // incorrect
```

--------------------------------

### Run Unit Tests

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/tutorial.md

Execute the unit tests defined in the project using Cargo.

```bash
cargo test
```

--------------------------------

### Pearlite Predicate Functions

Source: https://github.com/creusot-rs/creusot/blob/master/CHANGELOG.md

Demonstrates defining predicate functions in Pearlite, showing basic Pearlite expressions and the use of the `pearlite!` macro for advanced syntax like quantifiers.

```Rust
#[predicate]
fn my_function(x: Int) -> bool { 
    x >= 0 // can use basic pearlite here
}

#[predicate]
fn exists_inverse(y : Int) -> bool { 
 pearlite! { exists< x : Int> x + y == 0 }
}
```

--------------------------------

### Create New Creusot Project

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/tutorial.md

Use this command to generate a new Rust project with the necessary configuration files for Creusot.

```bash
cargo creusot new creusot-tutorial
```

--------------------------------

### Mutual Recursion via Traits - Rejects

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/termination.md

This example does not compile because the instantiation `g::<i32>()` reveals a direct cycle: `g::<i32>` calls `<i32 as Tr>::f()`, which in turn calls `g::<i32>()`.

```rust
trait Tr {
    fn f();
}
fn g<T: Tr>() {
    <T as Tr>::f();
}

impl Tr for i32 {
    fn f() {
        g::<i32>();
    }
}
```

--------------------------------

### Compile and prove a Creusot project

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/quickstart.md

This command compiles the Rust crate to Coma and runs provers to verify that functions satisfy their contracts. A successful run guarantees that for all valid inputs, the function's output meets the specified postconditions.

```bash
cargo creusot
```

--------------------------------

### Update Proof JSON Files

Source: https://github.com/creusot-rs/creusot/blob/master/CONTRIBUTING.md

Update `proof.json` files for `why3find` tests. For tests with `why3session.xml`, minor changes are auto-updated, but substantial changes require manual editing.

```sh
./t why3 --update
```

--------------------------------

### Initialize List with Empty Ghost Sequence

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/tutorial/linked_list.md

Initializes a new List, setting the first and last pointers to null and initializing the ghost sequence with Seq::new().

```rust
impl<T> List<T> {
    pub fn new() -> List<T> {
        // Initialize the `seq` field with an empty `Seq`.
        List { first: std::ptr::null(), last: std::ptr::null(), seq: Seq::new() }
    }
}
```

--------------------------------

### Open Why3 IDE on proof failure

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/quickstart.md

When a proof fails, this option opens the Coma file in the Why3 IDE, allowing you to inspect the proof state and debug. The IDE is launched only if the proof fails.

```bash
cargo creusot verif/[COMA_FILE] -i
```

--------------------------------

### Always open Why3 IDE

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/quickstart.md

This option ensures the Why3 IDE is always launched after compilation and proof attempts, regardless of whether the proof succeeded or failed. Useful for continuous inspection.

```bash
cargo creusot verif/[COMA_FILE] --ide-always
```

--------------------------------

### Using proof_assert! Macro

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/basic_concepts/proof_assert.md

Insert an arbitrary verification condition into your code. The expression must evaluate to a boolean.

```Rust
fn f() {
    // ...
    let x = 1;
    let y = 2;
    proof_assert!(x@ + y@ == 3);
    // ...
}
```

--------------------------------

### Pin Why3-Tools

Source: https://github.com/creusot-rs/creusot/blob/master/CONTRIBUTING.md

Pin the `why3-tools` package to a specific git commit. This is part of upgrading a prover.

```sh
opam pin git+https://github.com/xldenis/why3-tools
```

--------------------------------

### Define a Simple Lemma

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/logic_functions/lemma_law.md

Define a lemma with preconditions and postconditions. This lemma can be proved by SMT solvers without an explicit body.

```rust
#[logic]
#[requires(x + y > 0)]
#[ensures(x > 0 || y > 0)]
fn add_gt_zero(x: Int, y: Int) {}
```

--------------------------------

### Using Snapshot for Insertion Sort

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/snapshots.md

Demonstrates how to use `snapshot!` to remember the original state of an array before sorting. This snapshot is then used in invariants to ensure the sorted array is a permutation of the original.

```rust
#[ensures(array@.permutation_of((^array)@))]
#[ensures(sorted((^array)@))]
pub fn insertion_sort(array: &mut [i32]) {
    let original = snapshot!(*array); // remember the original value
    let n = array.len();
    #[invariant(original@.permutation_of(array@))]
    #[invariant(...)]
    for i in 1..n {
        let mut j = i;
        #[invariant(original@.permutation_of(array@))]
        #[invariant(...)]
        while j > 0 {
            if array[j - 1] > array[j] {
                array.swap(j - 1, j);
            } else {
                break;
            }
            j -= 1;
        }
    }

    proof_assert!(sorted_range(array@, 0, array@.len()));
}
```

```rust
#[logic]
fn permutation_of(s1: Seq<i32>, s2: Seq<i32>) -> bool {
    // ...
}
```

```rust
#[logic]
fn is_sorted(s: Seq<i32>) -> bool {
    // ...
}
```

--------------------------------

### Create or Update Creusot Package

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/command_line_interface.md

Creates a new package directory and initializes it with Creusot project files. Supports options for main file, tests, and standard library usage.

```bash
cargo creusot new <NAME> [--main] [--tests] [--no-std] [--creusot-path <PATH>]
```

--------------------------------

### Verify pop_front in Linked List

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/tutorial/linked_list.md

This snippet shows the verification of the `pop_front` function. It illustrates the use of `ghost!` blocks with `Seq::pop_front_ghost` and `Perm::to_box` for safely deallocating and retrieving the first element of the linked list.

```rust
pub fn pop_front(&mut self) -> Option<T> {
    if self.first.is_null() {
        return None;
    }
    let own = ghost! { self.seq.pop_front_ghost().unwrap() };              // 1
    let link = unsafe { *Perm::to_box(self.first as *mut Link<T>, own) };  // 2
    self.first = link.next;
    if self.first.is_null() {
        self.last = std::ptr::null_mut();
    }
    Some(link.value)
}
```

--------------------------------

### Include Creusot Prelude

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/basic_concepts.md

Use this line to import necessary items from the `creusot_std` crate. This is required for Creusot to function correctly.

```rust
use creusot_std::prelude::*;
```

--------------------------------

### Run Default Tests

Source: https://github.com/creusot-rs/creusot/blob/master/CONTRIBUTING.md

Execute the default test suite for Creusot. For more options, refer to `./t all`.

```sh
./t
```

--------------------------------

### Using a Commutative Law

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/logic_functions/lemma_law.md

Shows that a property defined as a 'law' (like commutativity) is automatically available in the proof context, simplifying assertions.

```rust
#[logic]
fn foo<T: Commutative>(x: T, y: T) {
    let z = x.op(y);
    proof_assert!(z == y.op(x)); // Works!
}
```

--------------------------------

### Nix Shell with Experimental Features Enabled

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/installation.md

Use this command to enter the Nix subshell when experimental Nix features like 'nix-command' and 'flakes' are disabled. It temporarily enables them for the command.

```sh
nix --extra-experimental-features 'nix-command flakes' shell "github:creusot-rs/creusot"
```

--------------------------------

### Configure VS Code for Creusot

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/quickstart/editor_config.md

Add this configuration to your `.vscode/settings.json` file to enable Creusot's verification command within VS Code. This is useful for projects that utilize Creusot.

```json
{
  "rust-analyzer.check.overrideCommand": [
    "cargo",
    "creusot",
    "--",
    "--message-format=json"
  ]
}
```

--------------------------------

### Verify Proofs with Why3

Source: https://github.com/creusot-rs/creusot/blob/master/CONTRIBUTING.md

Validate Creusot's proofs by running tests that have changes compared to the master branch. This requires Why3 and supporting tools.

```sh
./t why3
```

```sh
cargo test --test why3
```

--------------------------------

### Configure Creusot for Why3

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/command_line_interface.md

Regenerates the `why3.conf` file, which is essential for Creusot to interact with Why3 SMT solvers. This command can also configure the parallelism for prover invocations.

```bash
cargo creusot why3-conf [--provers-parallelism <N>]
```

--------------------------------

### Configure Default Members in Cargo.toml (Standard)

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/command_line_interface.md

Specifies default members for the workspace in `Cargo.toml` using the standard Cargo field.

```toml
[workspace]
default-members = ["package1", "package2"]
```

--------------------------------

### Ghost Seq for Infinite Capacity

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/ghost/ghost-structures.md

Shows the correct way to handle potentially unbounded collections in ghost code using `Seq::push_ghost`, avoiding the contradictions seen with `Vec`.

```rust
use creusot_std::{proof_assert, ghost, Int, logic::Seq};
ghost! {
    let mut s: Seq<Int> = Seq::new();
    for _ in 0..=usize::MAX as u128 + 1 {
        s.push_ghost(0);
    }
    // proof_assert!(s.len() <= usize::MAX@); // fails
    proof_assert!(s.len() > usize::MAX@);
}
```

--------------------------------

### Configure and Run Erasure Checks

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/erasure.md

Commands to run erasure checks, including forcing a rebuild and enabling checks. Use this to ensure your erasure annotations are correctly verified.

```bash
cargo creusot --only=coma
rm -r target/creusot # Force rebuilding from scratch
cargo creusot --erasure-check
```

--------------------------------

### Run UI Tests

Source: https://github.com/creusot-rs/creusot/blob/master/CONTRIBUTING.md

Execute UI tests for Creusot's translation validation. Use patterns to run subsets of tests.

```sh
./t ui
```

```sh
cargo test --test ui
```

```sh
./t ui "pattern"
```

```sh
cargo test --test ui -- "pattern"
```

--------------------------------

### Regenerate Testsuite Session

Source: https://github.com/creusot-rs/creusot/blob/master/CONTRIBUTING.md

Completely regenerate a Why3 session from scratch using the provided script.

```sh
./testsuite_regenerate
```

--------------------------------

### Creusot-Generated Pre/Postconditions for Type Invariants

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/type_invariants.md

Illustrates how Creusot automatically generates preconditions for function arguments and postconditions for return values based on their type invariants.

```rust
// `inv` generically refers to the invariant of some value
#[requires(inv(x))] // generated by Creusot
#[ensures(inv(result))] // generated by Creusot
fn foo(x: SumTo10) -> SumTo10 {
    x
}
```

--------------------------------

### Configure Default Members in Cargo.toml

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/command_line_interface.md

Specifies default members for the Creusot workspace in `Cargo.toml`.

```toml
[workspace.metadata.creusot]
default-members = ["package1", "package2"]
```

--------------------------------

### Add Rust Source Component

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/erasure.md

Command to add the rust-src component to your toolchain, which is required for using core and std with erasure checks.

```bash
rustup component add rust-src --toolchain $MY_TOOLCHAIN
```

--------------------------------

### Check Creusot version

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/command_line_interface.md

Prints the version of Creusot and any accompanying tools. This is useful for ensuring compatibility and tracking updates.

```bash
cargo creusot version
```

--------------------------------

### Implementing View for MyPair<T, U>

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/view.md

This snippet demonstrates how to implement the `View` trait for a generic struct `MyPair<T, U>`. The `view` method maps the struct to a tuple `(T, U)`. The `#[ensures]` attribute on `my_pair` shows how the view is used in specifications.

```rust
struct MyPair<T, U> {
  fst: T,
  snd: U,
}

impl<T, U> View for MyPair<T, U> {
    type ViewTy = (T, U);

    #[logic(open)]
    fn view(self) -> Self::ViewTy {
        (self.fst, self.snd)
    }
}

#[ensures(result@ == (a, b))]
fn my_pair<T, U>(a: T, b: U) -> MyPair<T, U> {
    MyPair(a, b)
}
```

--------------------------------

### Complete sum_up_to Function (While Loop)

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/tutorial.md

The complete 'sum_up_to' function with all necessary annotations for verification using a while loop.

```rust
#[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
}
```

--------------------------------

### Upgrade Prover with External Tool

Source: https://github.com/creusot-rs/creusot/blob/master/CONTRIBUTING.md

Configure Creusot to use a newer prover version by specifying it as external and skipping version checks.

```sh
./INSTALL --no-check-version <PROVER> --external <PROVER>
```

--------------------------------

### Opaque Logic Function with `dead`

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/logic_functions/open.md

Shows how to declare a fully opaque logic function using `#[logic(opaque)]`. This function has no implementation and can use the `dead` keyword.

```rust
#[logic(opaque)]
fn generate_int() -> Int {
    dead
}
```

--------------------------------

### Indexing Ghost Containers with Int

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/ghost/int-in-ghost.md

Shows how to use `Int` values for indexing ghost containers. Ghost containers like `FMap` return their length as an `Int`, which can then be used to access elements in a `Seq`.

```rust
ghost! {
    let s: Seq<_> = ...;
    let m: FMap<_, _> = ...;
    let len: Int = m.len_ghost();
    let x = s[len + 3int];
};
```

--------------------------------

### Update All Why3 Tests

Source: https://github.com/creusot-rs/creusot/blob/master/CONTRIBUTING.md

Update all Why3 tests, not just those with changes from `origin/master`.

```sh
./t why3 --why3-all
```

--------------------------------

### Cargo config for development versions

Source: https://github.com/creusot-rs/creusot/blob/master/guide/src/command_line_interface.md

This configuration snippet is automatically added when initializing a project with a development version of Creusot. It patches `creusot-std` to point to a local path, enabling development workflows.

```toml
[patch.crates-io]
creusot-std = { path = "creusot/creusot-std" }
```