How to integrate distributed-verification into verify-rust-std?

[zjp-CN]

run-kani.sh is well written and not so difficult to read. But it's not robust and extensible.

distributed-verification (dv) a tool proposed as GSoC 2025 helps verify-rust-std (kani) skip any harness that is unmodified, and make verification workloads into multiple VMs.

dv can tell which harnesses should be really run based on function hash difference. The hash is computed through source code of function, and all traversed calls inside.

The rest of work is to integrate it into verify-rust-std. But here are some choices to achieve it:

• keep run-kani.sh as full check, and create another script as partial check
• keep run-kani.sh, and add partial check logics (i.e. invoking dv) to current code, almost needing a big surgery
• move functionalities from run-kani.sh into verify_rust_std a CLI used by dv to operate on verify-rust-std (from kani's perspective for now), currently it only invokes cargo build with RUSTC_WRAPPER as dv, but I'd like to implement what run-kani.sh does now, and handle the switch between full checks and partial checks. Also there is a TODO in run-kani.sh to make argument parsing better:

verify-rust-std/scripts/run-kani.sh

Line 23 in 8f55686

# TODO: Improve parsing with getopts

What do you think?

[tautschnig]

With apologies for the late response: I'd suggest to keep run-kani.sh as it is for the time being and introduce another script that uses the dv infrastructure. That will allow people to keep their existing workflows as they are and we can eventually tell everyone to migrate to the new script once we are confident it is the better solution for (almost) everyone. In the same vein, we can add new jobs to CI using dv while retaining the existing ones. Thereby, we can demonstrate how much better (i.e., faster) the approach via dv is for each and every pull request.