Support for powf operations

[nickgarfield]

Requested feature: powf
Use case: I want to verify a function that uses powf
Link to relevant documentation (Rust reference, Nomicon, RFC): https://doc.rust-lang.org/std/primitive.f64.html#method.powf

Test case:

pub fn f(a: u64) -> u64 {
    const C: f64 = 0.618;
    (a as f64).powf(C) as u64
}

#[cfg(kani)]
mod verification {
    use super::*;

    #[kani::proof]
    fn verify_f() {
        const LIMIT: u64 = 10;
        let x: u64 = kani::any();
        let y: u64 = kani::any();
        kani::assume(x < LIMIT || x > u64::MAX - LIMIT);
        kani::assume(y < LIMIT || y > u64::MAX - LIMIT);
        kani::assume(x > y);
        let x_ = f(x);
        let y_ = f(y);
        assert!(x_ >= y_);
    }
}

[nickgarfield]

The docs suggest Numerics are fully supported. Without floats, I think "partial" would be more appropriate.

[zhassan-aws]

Thanks for creating this issue, @nickgarfield.

This is related to #2763. Now that support has been added in CBMC (diffblue/cbmc#7906), this should be doable.

[adpaco-aws]

Hi @nickgarfield , do you mind explaining the test case you attached? Does it test a well-known numerical property or why do you think it should pass?

The reason I'm asking is that I have a development version with the powf64 intrinsic, but the result I'm getting is not the one you're expecting:

SUMMARY:
 ** 1 of 89 failed
Failed Checks: assertion failed: x_ >= y_
 File: "powf_example.rs", line 20, in verification::verify_f

VERIFICATION:- FAILED
Verification Time: 0.59359556s

Concrete playback returns these inputs:

#[test]
fn kani_concrete_playback_verify_f_9913905681601751135() {
    let concrete_vals: Vec<Vec<u8>> = vec![
        // 18446744073709551608ul
        vec![248, 255, 255, 255, 255, 255, 255, 255],
        // 18446744073709551606ul
        vec![246, 255, 255, 255, 255, 255, 255, 255],
    ];
    kani::concrete_playback_run(concrete_vals, verify_f);
}

Running the test case with those inputs doesn't cause it to panic. It's possible that the intrinsic is over-approximating too much, but first I'd like to know more about your test case.

[adpaco-aws]

The docs suggest Numerics are fully supported. Without floats, I think "partial" would be more appropriate.

I don't agree with this assessment. What we're missing support for are the pow* intrinsics which appear as "Not supported" in the table summarizing support for intrinsics.

[nickgarfield]

Does it test a well-known numerical property or why do you think it should pass?

I drafted this example rather quickly. It might have some bugs. I was trying to write a proof to show f(x) > f(y) if x > y.

[adpaco-aws]

We were discussing this issue now. We suspect it's a spurious failure due to over-approximation, but haven't determined it yet.

@celinval notes that, for the intrinsics that over-approximate, we should find a way to alert the user about such behaviors. This isn't the first time users are confused, see #1342 for another example.