tools-creusot-coq-install

When do you need this?

Creusot's SMT solvers (alt-ergo, z3, cvc5, cvc4) handle the vast majority of verification conditions automatically. Coq is needed only for goals that fall outside their decidable fragment — most commonly modular arithmetic with a variable divisor, e.g. proving (a - b) % n = 0 given a % n = 0 and b % n = 0 for a runtime n.

Coq does not replace the SMT solvers — it complements them for the rare hard goals. Run tools-creusot-install first if Creusot is not yet installed.

---

Prerequisites

• Creusot already installed (cargo creusot version succeeds)
• opam switch at ~/.local/share/creusot/_opam exists (created by the Creusot installer)

---

Installation Steps

All steps run inside the existing Creusot opam switch — no separate switch needed.

Step 1 — Activate the switch

eval $(opam env --switch=/home/cornel/.local/share/creusot --set-switch)

Step 2 — Install Coq 8.20.1

opam install coq.8.20.1 -y

Takes 10–20 minutes — Coq compiles from source against the switch's OCaml 5.x. Verify: coqtop --version should print The Coq Proof Assistant, version 8.20.1.

Step 3 — Compile Why3's Coq support libraries

Why3 ships Coq .v source files for its integer/modular arithmetic theories. They must be compiled against the installed Coq before Why3 can use them.

WHY3_COQ_SRC=~/.local/share/creusot/_opam/.opam-switch/sources/why3/lib/coq
WHY3_COQ_DST=~/.local/share/creusot/_opam/share/why3/coq

find $WHY3_COQ_SRC -name "*.v" \
  | grep -v "real/Truncate\|real/Trigonometry\|ieee_float\|floating_point" \
  | sort \
  | while read f; do
      rel=${f#$WHY3_COQ_SRC/}
      dir=$(dirname $rel)
      mkdir -p $WHY3_COQ_DST/$dir
      (cd $WHY3_COQ_SRC && coqc -R . Why3 "$rel" 2>/dev/null \
        && cp "${rel%.v}.vo" "$WHY3_COQ_DST/${rel%.v}.vo" 2>/dev/null)
    done

echo "8.20.1" > $WHY3_COQ_DST/version

Expect ~51 .vo files compiled. The floating-point theories are excluded because they require the Flocq library which is not needed for our proofs.

Step 4 — Register Coq in ~/.config/creusot/why3.conf

This is the config file cargo creusot uses. Add the following block (after the existing [partial_prover] entries):

[prover]
command = "/home/cornel/.local/share/creusot/_opam/bin/coqtop \
           -batch -R /home/cornel/.local/share/creusot/_opam/share/why3/coq \
           Why3 -l %f"
driver   = "/home/cornel/.local/share/creusot/_opam/share/why3/drivers/coq.drv"
editor   = "coqide"
in_place = false
interactive = false
name     = "Coq"
shortcut = "coq"
version  = "8.20.1"

Also change memlimit = 1000 to memlimit = 0 in the [main] section. Why: OCaml 5.x (used by Coq 8.20) reserves ~64 GB of virtual address space for its GC at startup. Why3's default 1 GB memory limit kills the process before it starts. Setting memlimit = 0 disables the limit; physical RAM usage remains low.

Step 5 — Add Coq to the verification crate's why3find.json

"provers": [ "alt-ergo", "z3", "cvc5", "cvc4", "Coq@8.20.1" ]

Step 6 — Verify

eval $(opam env --switch=/home/cornel/.local/share/creusot --set-switch)
WHY3_COQ=~/.local/share/creusot/_opam/share/why3/coq
echo "Require Import Why3.BuiltIn. Check True." \
  | coqtop -batch -R $WHY3_COQ Why3

No output = success. Coq is now available as a prover.

---

Writing a hand-written Coq proof

Coq in this setup runs in batch replay mode — it does not discover proofs automatically. A human writes the proof once using Coq tactics; why3find then replays it on every subsequent cargo creusot run.

For goals where you want automatic proof discovery, consider installing CoqHammer (coq-hammer via the coq-released opam repo + E-prover). CoqHammer calls external ATPs and reconstructs proofs automatically.

Workflow

1. Generate the .v file Why3 would produce for the failing VC:

   WHY3=~/.local/share/creusot/_opam/bin/why3
   WHY3_DRV=~/.local/share/creusot/_opam/share/why3/drivers/coq.drv
   $WHY3 prove --driver $WHY3_DRV --output /tmp/coq_goals my_theory.why
   

2. Fill in the proof between Proof. and Qed. using Coq tactics:

   • lia — linear integer arithmetic (handles +, -, comparisons)
   • ring — ring equalities, rearrangement with *
   • unfold <def>; lia — unfold a definition, then discharge with lia
   • See tools/creusot/certus-segment-verif/coq/mod_sub_lemma.v for a full example

3. Verify the proof compiles:

   coqtop -batch -R $WHY3_COQ Why3 -l my_proof.v
   # No output = proof accepted
   

4. Bridge into Creusot via a #[trusted] lemma:

   // Proved by hand in Coq — see coq/my_proof.v
   #[trusted]
   #[logic]
   #[requires(n@ > 0)]
   #[requires(a@ % n@ == 0)]
   #[requires(b@ % n@ == 0)]
   #[ensures(result)]
   fn lemma_mod_sub(a: usize, b: usize, n: usize) -> bool {
       pearlite! { (a@ - b@) % n@ == 0 }
   }
   

5. Call the lemma at the point in the proof where the fact is needed:

   proof_assert!(lemma_mod_sub(remaining, length, ss));
   

What #[trusted] means

#[trusted] tells why3find to assume the postcondition without discharging a VC for the function body. It is not a cheat — the Coq .v file is the evidence. This is the standard practice in hybrid SMT + ITP verification workflows.