CONTRIBUTING: document the test coverage tool (#2566)

Author: mmcloughlin

CONTRIBUTING.md

@@ -141,6 +141,25 @@ background, and it's invalidating the build cache. To prevent this, you need
 to configure your IDE for Verus development. See above for how to do
 this for VS Code.
 
+### Measuring test coverage
+
+`tools/coverage.sh` reports how much of the verifier the `rust_verify_test`
+suite exercises. Run it from `source/`:
+
+```
+./tools/coverage.sh                    # whole suite
+./tools/coverage.sh --test bitvector   # narrow to one suite
+```
+
+This writes the reports to `coverage/`. Open `coverage/index.html` in a browser
+for the annotated source view, or read the text summary with `cat
+coverage/coverage.txt`. An `lcov` file (`coverage/coverage.lcov`) is also
+written for external tools.
+
+The tests run the verifier as a spawned subprocess, so the script instruments
+that `rust_verify` binary (not the test binary), and gathers coverage from those
+processes.
+
 ## Contributing to the standard library (`vstd`)
 
 ### What to contribute