Creusot IDE

A VS Code extension providing support for Creusot, a deductive verifier for Rust code.

This project is work in progress. An official release is upcoming.

Install Creusot IDE

Creusot itself should be installed separately.

Creusot IDE consists of two parts:

1. The Creusot IDE extension, installed via VS Code: open VS Code > Extensions > Search "Creusot IDE".

2. The Creusot LSP language server, which must currently be installed separately:

    # First, install Creusot, Why3, and Why3find; see https://github.com/creusot-rs/creusot for instructions
   
    git clone https://github.com/creusot-rs/creusot-ide
    opam pin creusot-lsp creusot-ide/ -y
   

Features

Creusot IDE helps you nagivate between your Rust sources and the verification artifacts generated by Creusot and Why3find.

• Run and inspect proofs from within the editor.
  • Functions with proof obligations will have a button in the gutter to their left. Click to run the prover (why3find prove). Alt+click to start Why3 IDE (only if the prover fails).
• Diagnostics underline locations with failed proofs
• Syntax highlighting:
  • .rs files: Creusot-specific attributes and Pearlite expressions,
  • .coma files.

Commands

Available in the command palette (Ctrl+P):

• Restart language server
• Stop language server

Settings

• creusot.lspPath: Path to the creusot-lsp executable. Default: "", to find the executable in PATH.

Known issues

Compatibility with standard Rust tools (Rust analyzer, etc.)

• How to build projects verified by Creusot.

  Creusot implicitly enables some unstable features to verify programs. When building programs with cargo build, they must be enabled explicitly with the following attribute in the root lib.rs:

  #![cfg_attr(not(creusot),feature(stmt_expr_attributes,proc_macro_hygiene))]
  

  Linters will then warn that creusot is an unknown parameter. To silence the warning, add this option to Cargo.toml:

  [lints.rust]
  unexpected_cfgs = { level = "warn", check-cfg = ['cfg(creusot)'] }
  

  This issue is being tracked at https://github.com/creusot-rs/creusot/issues/1000

• Rust analyzer doesn't know how to parse Creusot specifications (attributes such as ensures, etc.), so they are underlined in red.

  Add this option in settings.json:

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