Support for powf operations #2966
Description
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_);
}
}