.env.example

# Verification tool paths

# Path to Verus binary (for 'just verify-verus' and 'elicitation prove --verus')
VERUS_PATH=~/repos/verus/source/target-verus/release/verus

# Path to Creusot installation (for custom commands if needed)
# CREUSOT_PATH=~/repos/creusot

# Database URL for elicit_sqlx integration tests
# Create with: createdb elicitation_test
DATABASE_URL=postgresql://elicitation:elicitation@localhost/elicitation_test

# ─── elicitation prove ─────────────────────────────────────────────────────────
# All settings below are used by `elicitation prove --kani/--verus/--creusot`.
# CLI flags always override these values.  Unset keys fall back to defaults.

# Default Cargo package to run proofs against (used when --package is not given)
# PROVE_PACKAGE=my_proofs

# --- Kani ---
# elicit_proofs contains the generated Kani harnesses
KANI_PACKAGE=elicit_proofs
# Extra flags forwarded verbatim to `cargo kani` (space-separated).
# elicit_proofs needs the `kani` feature plus unstable contracts/stubbing flags.
KANI_FLAGS="--lib --features kani -Z function-contracts -Z stubbing"

# --- Verus ---
# Already declared above: VERUS_PATH
# Verus runs against the dedicated elicitation_verus crate, not elicit_proofs.
# Source file to pass to Verus (required for `prove --verus`)
VERUS_FILE=crates/elicitation_verus/src/lib.rs
# Extra flags forwarded verbatim to the Verus binary
# VERUS_FLAGS=--no-auto-recommends-check

# --- Creusot ---
# elicit_proofs contains the generated Creusot companions
CREUSOT_PACKAGE=elicit_proofs
# Directory for per-backend log files (default: current directory)
# PROVE_LOG_DIR=.
# Directory containing `cargo-creusot` / `creusot-rustc` binaries
# (default: ~/.local/share/creusot/bin)
# CREUSOT_BIN_DIR=~/.local/share/creusot/bin
# Path to Why3 config file
# WHY3_CONFIG=~/.why3.conf
# Space-separated list of extra Why3 dune-project directories
# DUNE_DIR_LOCATIONS=
# Extra flags forwarded verbatim to `cargo creusot prove`
# Add `--features <name>` here only if your downstream proof crate explicitly
# requires a feature for Creusot builds.
# CREUSOT_FLAGS=