Repository navigation
How to integrate distributed-verification into verify-rust-std? #409
Description
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 buildwith 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
What do you think?
Activity
tautschnig commentedon Jul 22, 2025
With apologies for the late response: I'd suggest to keep
run-kani.shas 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.