Spurious failure on Prost check_duration_roundtrip

[danielsn]

I tried this code:

1. Checkout prost https://github.com/tokio-rs/prost at commit bff66a665fc2d5a0cbb826e446f8050450cbd8a2
2. Follow the instructions to setup PropProof https://github.com/tokio-rs/prost/blob/master/KANI.md

3.  cd prost-types; 
    cargo kani --tests --default-unwind 3 --output-format terse --harness "check_duration_roundtrip" --enable-unstable --concrete-playback print
   

with Kani version: 0.20.0

I expected to see this happen: Passed with no errors

Instead, this happened:

Checking harness tests::check_duration_roundtrip...
Concrete playback unit test for `tests::check_duration_roundtrip`:
#[test]
fn kani_concrete_playback_check_duration_roundtrip_18095432521536020068() {
    let concrete_vals: Vec<Vec<u8>> = vec![
        // 18446744073709551608ul
        vec![248, 255, 255, 255, 255, 255, 255, 255],
        // 999999918
        vec![174, 201, 154, 59]
    ];
    kani::concrete_playback_run(concrete_vals, check_duration_roundtrip);
}
INFO: To automatically add the concrete playback unit test `kani_concrete_playback_check_duration_roundtrip_18095432521536020068` to the src code, run Kani with `--concrete-playback=inplace`.

VERIFICATION RESULT:
 ** 1 of 371 failed (6 unreachable)
Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime
 File: "/Users/dsn/.rustup/toolchains/nightly-2022-12-11-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/result.rs", line 1791, in std::result::unwrap_failed

VERIFICATION:- FAILED
Verification Time: 16.392767s

I created the following concrete test from the values

    #[test]
    fn check_duration_roundtrip_concrete(
    ) {
        let seconds = 18446744073709551608;
        let nanos = 999999918;
        let std_duration = time::Duration::new(seconds, nanos);
        let prost_duration = match Duration::try_from(std_duration) {
            Ok(duration) => duration,
            Err(_) => return,
        };
        assert_eq!(time::Duration::try_from(prost_duration.clone()).unwrap(), std_duration);

        if std_duration != time::Duration::default() {
            let neg_prost_duration = Duration {
                seconds: -prost_duration.seconds,
                nanos: -prost_duration.nanos,
            };

            assert!(
                matches!(
                    time::Duration::try_from(neg_prost_duration),
                    Err(DurationError::NegativeDuration(d)) if d == std_duration,
                )
            )
        }
    }

And it passes.

╰─$ cargo test check_duration_roundtrip_concrete                                                                                            101 ↵
    Blocking waiting for file lock on build directory
   Compiling prost-types v0.11.6 (/Users/dsn/ws/prost/prost-types)
    Finished test [unoptimized + debuginfo] target(s) in 18.80s
     Running unittests src/lib.rs (/Users/dsn/ws/prost/target/debug/deps/prost_types-39fbb536841d5b48)

running 1 test
test tests::check_duration_roundtrip_concrete ... ok

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 16 filtered out; finished in 0.00s

This suggests to me that there is a spurious counterexample. I'd guess this has to do with niche optimization, but I'm not certain.