tools-creusot-init

This skill takes a cargo project directory and configures it for Creusot verification.

Input

The user must provide the target project directory as an argument (e.g. /tools-init-creusot components/dispatch-map).

If no argument is provided, show the hint and stop.

Prerequisites

• Creusot must already be installed (cargo creusot version should succeed)
• If not installed, inform the user to run the tools-install-creusot skill first, then stop

Steps

1. Verify the target directory contains a Cargo.toml. If not, inform the user and stop.

2. Check that Creusot is installed by running cargo creusot version. If it fails, tell the user to run /tools-install-creusot first and stop.

3. Modify Cargo.toml:

   • Add creusot-std = "0.12.0-dev" under [dependencies] (if not already present)
   • Add a [patch.crates-io] section pointing to the local creusot-std (use a relative path from the project to the certus repo's tools/creusot/creusot/creusot-std, or use ~ notation for shell expansion):

     [patch.crates-io]
     creusot-std = { path = "<relative-path-to>/tools/creusot/creusot/creusot-std" }
     

     Compute the correct relative path from the target project directory to certus/tools/creusot/creusot/creusot-std.
   • Add the cfg(creusot) lint configuration under [lints.rust]:

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

   • If the project is inside another workspace but should be standalone, add an empty [workspace] table

4. Create why3find.json in the project root (if not already present):

   {
     "fast": 0.2,
     "time": 1,
     "depth": 6,
     "packages": [ "creusot" ],
     "provers": [ "alt-ergo", "z3", "cvc5", "cvc4" ],
     "tactics": [ "compute_specified", "split_vc" ],
     "drivers": [],
     "warnoff": [ "unused_variable", "axiom_abstract" ]
   }
   

5. Add use creusot_std::prelude::*; to src/lib.rs or src/main.rs (if not already present). If the file has existing functions, add a commented example showing how to annotate:

   // Example Creusot annotations:
   // #[requires(precondition)]
   // #[ensures(postcondition)]
   // pub fn verified_function(...) { ... }
   

6. Run cargo clean to remove any stale build artifacts that would block Creusot's translation pass.

7. Verify the setup works by running:

   export PATH="$HOME/.local/share/creusot/bin:$PATH"
   cargo creusot --only coma
   

   This should compile without errors. If there are no annotated functions yet, it will produce no .coma files — that's expected.

8. Report success and tell the user:

   • Add #[requires(...)] and #[ensures(...)] annotations to functions they want to verify
   • Run cargo creusot to build and prove
   • Run why3find prove verif/<crate_name>_rlib/*.coma to prove individual files
   • Reference certus/tools/creusot/creusot-test-example/src/lib.rs for annotation examples

Notes

• Always run cargo clean before the first cargo creusot if the project was previously built with plain cargo build
• The [patch.crates-io] section assumes Creusot was cloned to certus/tools/creusot/creusot per the install skill
• If the project uses edition = "2024", it works with Creusot's required nightly toolchain