Skip to content

Commit

Permalink
Improve u16::carrying_mul harness performance (rust-lang#230)
Browse files Browse the repository at this point in the history
This harness takes between 22-25 minutes in CI. Change the harnesses's
macro to use kissat solver instead, which brings verification time down
to ~7 seconds.

As an aside, I noticed this problem because the partition 1 runner in
rust-lang#229 is taking ~55 minutes, where the other partitions are taking ~30
minutes. This harness accounts for almost the entire difference. One
nice consequence of partitioning verification is that it will make
performance issues like this more noticeable.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
carolynzech authored Dec 19, 2024
1 parent 67e2f1c commit 5da586f
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions library/core/src/num/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1759,6 +1759,7 @@ mod verify {
($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => {
$(
#[kani::proof]
#[kani::solver(kissat)]
pub fn $harness_name() {
let lhs: $type = kani::any::<$type>();
let rhs: $type = kani::any::<$type>();
Expand Down

0 comments on commit 5da586f

Please sign in to comment.