The pinned Kani reports a failed compare_exchange as a success #673

The Kani commit pinned in tool_config/kani-version.toml (d4df833) always reports
atomic_cxchg as successful. When the comparison fails, memory is left unchanged, but
compare_exchange returns Ok instead of Err.

This is kani#4537, fixed by
kani#4542. The fix is on Kani main,
but is not in the pinned commit or the latest release, 0.67.0.

Reproduction with Kani 0.67.0

use std::sync::atomic::{AtomicU8, Ordering};

#[kani::proof] // Passes: positive control
fn cas_witness_success() {
    let a = AtomicU8::new(7);
    assert_eq!(a.compare_exchange(7, 9, Ordering::SeqCst, Ordering::SeqCst), Ok(7));
    assert_eq!(a.load(Ordering::SeqCst), 9);
}

#[kani::proof] // Fails: `r` is `Ok(7)` instead of `Err(7)`
fn cas_comparison_fails() {
    let a = AtomicU8::new(7);
    let r = a.compare_exchange(8, 9, Ordering::SeqCst, Ordering::SeqCst);
    assert_eq!(a.load(Ordering::SeqCst), 7);
    assert_eq!(r, Err(7));
}

Impact on this repository

Challenge 27 covers library/alloc/src/sync.rs, where methods such as
Arc::try_unwrap depend on the result of compare_exchange.

This harness also fails with the pinned model:

#[kani::proof]
fn arc_try_unwrap_two_owners() {
    let a = Arc::new(7u8);
    let b = Arc::clone(&a);
    assert!(Arc::try_unwrap(a).is_err());
    drop(b);
}

#587 generates _unique, _shared, and _weak_present harnesses for each type. The
_shared harness calls Arc::try_unwrap, but discards its result:

#[kani::proof]
pub fn $shared() {
    let arc: Arc<$ty, Global> = Arc::new_in($expr, Global);
    let shared = Arc::clone(&arc);
    let _result = Arc::<$ty, Global>::try_unwrap(arc);
    core::mem::forget(shared);
}

With the pinned Kani commit, this harness takes the success path even though another
strong reference exists. All three variants therefore take the success path, so their
names do not reflect a checked outcome.

Suggested fix

Could we update the Kani pin to include kani#4542? If that is not possible yet, the
limitation should at least be documented in the harness requirements discussed in #617.

I also have 44 mutation-tested harnesses for challenge 7, parts 1 and 2, and can open a
PR if that would be useful.