Cannot reproduce errors found by Kani

[ChristopherRabotin]

In a somewhat complicated constructor that requires two sin() functions, Kani seems to be able to find bugs that I cannot reproduce by re-running the test manually with the values Kani reports cause a failure.

Here is a permalink to the Kani test: https://github.com/nyx-space/hifitime/blob/475428d4d117e9a5ecb688e71ebbd57443f34e09/src/epoch.rs#L2991-L3016 , pasted below for posteriority.

#[cfg(kani)]
#[kani::proof]
// #[test]
fn formal_epoch_reciprocity_tdb() {
    let duration: Duration = kani::any();
    // let duration = Duration::from_parts(19510, 3155759999999997938);

    // TDB
    let ts_offset = TimeScale::TDB.ref_epoch() - TimeScale::TAI.ref_epoch();
    if duration > Duration::MIN + ts_offset && duration < Duration::MAX - ts_offset {
        // We guard TDB from durations that are would hit the MIN or the MAX.
        // TDB is centered on J2000 but the Epoch is on J1900. So on initialization, we offset by one century and twelve hours.
        // If the duration is too close to the Duration bounds, then the TDB initialization and retrieval will fail (because the bounds will have been hit).

        let time_scale: TimeScale = TimeScale::TDB;
        let epoch: Epoch = Epoch::from_duration(duration, time_scale);
        let out_duration = epoch.to_duration_in_time_scale(time_scale);
        assert_eq!(out_duration.centuries, duration.centuries);
        if out_duration.nanoseconds > duration.nanoseconds {
            assert!(out_duration.nanoseconds - duration.nanoseconds < 500_000);
        } else if out_duration.nanoseconds < duration.nanoseconds {
            assert!(duration.nanoseconds - out_duration.nanoseconds < 500_000);
        }
        // Else: they match and we're happy.
    }
}

This will call the following constructor: https://github.com/nyx-space/hifitime/blob/475428d4d117e9a5ecb688e71ebbd57443f34e09/src/epoch.rs#L527-L540 . And here are where the trigonometry functions are called: https://github.com/nyx-space/hifitime/blob/475428d4d117e9a5ecb688e71ebbd57443f34e09/src/epoch.rs#L1078-L1083 .

When running the test, Kani reports that if the duration is defined as Duration::from_parts(19510, 3155759999999997938);, then the assertions fail.

However, when un-commenting this line and converting the function to a normal test case, the test succeeds (in fact, the values match exactly).

This happens when using the following command line invocation:

$ cargo kani --harness formal_epoch_reciprocity_tdb --visualize

with Kani version: 0.18.0

I expected that the issues Kani found be reproducible in a normal test case (this has been my typical debugging strategy).

Kani visualization report:

report-epoch-formal_epoch_reciprocity_tdb.tar.gz

[zhassan-aws]

Hi @ChristopherRabotin. Thanks for the bug report. Unfortunately, trigonometric functions are currently abstracted in CBMC, and thus the values reported by Kani are not sufficient to cause a normal test to fail. This can be reproduced on this small program:

#[kani::proof]
fn main() {
    let x: f64 = kani::any();
    let y = x.sin();
    assert_ne!(y, 0.5);
}

See #1342 for more details.

Is it possible to provide stubs for those trigonometric functions?

[ChristopherRabotin]

That makes a lot of sense. The code needs these trig functions, but that's OK. I'll track #1342 instead, and close this issue.

Thanks for the quick response.