minerva 0.2.0

//! Kani proof harnesses for the `Clock` fold and its packed state (S86).
//!
//! Compiled only under `cargo kani` (`cfg(kani)`). Single-threaded harnesses: the
//! CAS loop commits on its first attempt, so these prove the *fold* (the pure
//! next-state computation) over fully symbolic readings and stamps; the loop's
//! retry behavior under contention is the concurrency model's concern, exercised
//! by the threaded tests and Miri. Run with
//! `RUSTFLAGS="--cfg portable_atomic_no_asm"` so `portable-atomic` takes its
//! asm-free fallback, which Kani can interpret; under a single thread every
//! correct atomic has the same sequential semantics, so the fold proofs are
//! unaffected by the substitution.
//!
//! The ceiling precondition on the harnesses is the documented saturation edge:
//! strict domination is proven for every remote stamp with
//! `physical() < u64::MAX`; at the absolute physical ceiling the clock pins
//! (saturates, never wraps) and strictness is arithmetically impossible.

extern crate alloc;

use core::sync::atomic::Ordering;

use super::super::stamp::Kairos;
use super::super::time::VirtualTimeSource;
use super::state::ClockState;
use super::{Clock, ClockConfig};

/// An arbitrary stamp below the physical ceiling (the documented saturation edge).
fn any_sub_ceiling_stamp() -> Kairos {
    let stamp = Kairos::new(kani::any(), kani::any(), kani::any(), kani::any::<u16>());
    kani::assume(stamp.physical() < u64::MAX);
    stamp
}

/// The packed state roundtrips for all `(physical, logical)`, the uninitialized
/// tag reads back as `None`, and no minted pair can forge the uninitialized word.
#[kani::proof]
fn clock_state_roundtrips_and_init_tag_is_unforgeable() {
    let physical: u64 = kani::any();
    let logical: u16 = kani::any();
    let minted = ClockState::minted(physical, logical);
    assert_eq!(minted.last(), Some((physical, logical)));
    assert!(ClockState::UNINIT.last().is_none());
    assert_ne!(minted.0, ClockState::UNINIT.0);
}

/// Successive `now` mints strictly increase, whatever the two time-source
/// readings: forward jump, freeze, or arbitrary backward skew.
#[kani::proof]
#[kani::unwind(3)]
fn now_strictly_increases_under_any_skew() {
    let source = VirtualTimeSource::new(kani::any());
    let driver = source.clone();
    let clock = Clock::new(source, 1, ClockConfig::default()).unwrap();
    let first = clock.now(0u16);
    driver.set(kani::any());
    let second = clock.now(0u16);
    assert!(second > first, "per-clock monotonicity must hold");
}

/// `now` monotonicity across a state poisoned by an arbitrary observed stamp:
/// receive any sub-ceiling remote, then two mints under two arbitrary readings.
#[kani::proof]
#[kani::unwind(3)]
fn now_strictly_increases_after_arbitrary_observe() {
    let remote = any_sub_ceiling_stamp();
    let source = VirtualTimeSource::new(kani::any());
    let driver = source.clone();
    let clock = Clock::new(source, 1, ClockConfig::default()).unwrap();
    clock.observe(remote);
    driver.set(kani::any());
    let first = clock.now(0u16);
    driver.set(kani::any());
    let second = clock.now(0u16);
    assert!(
        second > first,
        "monotonicity must survive any received stamp"
    );
}

/// `after(prev)` strictly dominates `prev` on a fresh clock, for every
/// sub-ceiling previous stamp, reading, and minted kairotic. This harness found
/// the S86 uninitialized-arm bug: before the fix, `prev.logical == u16::MAX`
/// minted a `(physical, logical)` tie whose kairotic/station tiebreak could
/// order the mint *below* `prev`.
#[kani::proof]
#[kani::unwind(3)]
fn after_dominates_previous_on_fresh_clock() {
    let previous = any_sub_ceiling_stamp();
    let source = VirtualTimeSource::new(kani::any());
    let clock = Clock::new(source, 1, ClockConfig::default()).unwrap();
    let minted = clock.after(previous, kani::any::<u16>());
    assert!(minted > previous, "after must strictly dominate its input");
}

/// `after(prev)` strictly dominates `prev` on a clock that has already minted,
/// under a second arbitrary reading: the initialized arm of the same law.
#[kani::proof]
#[kani::unwind(3)]
fn after_dominates_previous_on_warm_clock() {
    let previous = any_sub_ceiling_stamp();
    let source = VirtualTimeSource::new(kani::any());
    let driver = source.clone();
    let clock = Clock::new(source, 1, ClockConfig::default()).unwrap();
    let _ = clock.now(0u16);
    driver.set(kani::any());
    let minted = clock.after(previous, kani::any::<u16>());
    assert!(minted > previous, "after must strictly dominate its input");
}

/// The HLC receive rule: after `observe(remote)`, the next mint strictly exceeds
/// `remote`, for every sub-ceiling remote and every pair of readings.
#[kani::proof]
#[kani::unwind(3)]
fn observe_then_now_dominates_remote() {
    let remote = any_sub_ceiling_stamp();
    let source = VirtualTimeSource::new(kani::any());
    let driver = source.clone();
    let clock = Clock::new(source, 1, ClockConfig::default()).unwrap();
    clock.observe(remote);
    driver.set(kani::any());
    let minted = clock.now(0u16);
    assert!(
        minted > remote,
        "every stamp after a receive must exceed it"
    );
}

/// The bounded receive is all-or-nothing: on rejection the packed state word is
/// bit-for-bit unchanged, from both the uninitialized and the minted state.
#[kani::proof]
#[kani::unwind(3)]
fn try_observe_rejection_leaves_clock_unchanged() {
    let source = VirtualTimeSource::new(kani::any());
    let clock = Clock::new(source, 1, ClockConfig::default()).unwrap();
    if kani::any() {
        let _ = clock.now(0u16);
    }
    let before = clock.state.load(Ordering::SeqCst);
    let remote = Kairos::new(kani::any(), kani::any(), kani::any(), kani::any::<u16>());
    let bound: u64 = kani::any();
    if clock.try_observe(remote, bound).is_err() {
        let after = clock.state.load(Ordering::SeqCst);
        assert_eq!(before, after, "a rejected receive must not move the clock");
    }
}

/// The bounded receive's admit path keeps the receive rule: on `Ok` the next
/// mint strictly exceeds the remote, exactly as the unbounded `observe`.
#[kani::proof]
#[kani::unwind(3)]
fn try_observe_admission_dominates_remote() {
    let remote = any_sub_ceiling_stamp();
    let source = VirtualTimeSource::new(kani::any());
    let driver = source.clone();
    let clock = Clock::new(source, 1, ClockConfig::default()).unwrap();
    let bound: u64 = kani::any();
    if clock.try_observe(remote, bound).is_ok() {
        driver.set(kani::any());
        let minted = clock.now(0u16);
        assert!(
            minted > remote,
            "an admitted receive must behave as observe"
        );
    }
}

/// The run mint is the iterated send: for any committed state (or none) and
/// one frozen reading, `advance_run`'s first stamp is `advance`'s, its
/// committed pair is what `len` successive `advance` calls against the same
/// reading commit, and each intermediate member is the closed-form
/// `rank_offset` of the first. Saturation needs no precondition here: the
/// saturating carry composes, so the closed form and the iterated steps pin
/// identically at the ceiling.
#[kani::proof]
#[kani::unwind(6)]
fn run_mint_equals_iterated_sends_over_a_frozen_reading() {
    let last: Option<(u64, u16)> = if kani::any() {
        Some((kani::any(), kani::any()))
    } else {
        None
    };
    let reading: u64 = kani::any();
    let len: u32 = kani::any();
    kani::assume(len >= 1 && len <= 4);

    let run = super::fold::advance_run(last, reading, len);

    let mut state = last;
    let mut first = (0u64, 0u16);
    let mut max_forward: u64 = 0;
    let mut max_backward: u64 = 0;
    let mut i: u32 = 0;
    while i < len {
        let step = super::fold::advance(state, reading, None);
        if i == 0 {
            first = (step.physical, step.logical);
        }
        if step.forward_skew > max_forward {
            max_forward = step.forward_skew;
        }
        if step.backward_skew > max_backward {
            max_backward = step.backward_skew;
        }
        assert_eq!(
            super::fold::rank_offset(first.0, first.1, u64::from(i)),
            (step.physical, step.logical),
            "member i must be the closed-form offset of the first"
        );
        state = Some((step.physical, step.logical));
        i += 1;
    }

    assert_eq!(
        (run.first_physical, run.first_logical),
        first,
        "the run's first stamp must be the single mint's"
    );
    assert_eq!(
        Some((run.physical, run.logical)),
        state,
        "the run must commit exactly the last iterated send"
    );
    // The run's reported skews are the very maxima the iterated mints
    // would have folded into the shell's stats (the S211 gate review's
    // finding: a unit-crossing run must not under-report the lead and lag
    // it created against its one reading).
    assert_eq!(
        run.forward_skew, max_forward,
        "the run reports the iterated forward-skew maximum"
    );
    assert_eq!(
        run.backward_skew, max_backward,
        "the run reports the iterated backward-skew maximum"
    );
}

/// Run members strictly ascend while the carry stays below the physical
/// ceiling: for every sub-sentinel first pair and member index whose
/// successor's carry does not saturate, member `i + 1` strictly dominates
/// member `i` as full stamps (same station and kairotic, the run's own
/// shape). At the documented `u64::MAX` pin the clock saturates and
/// strictness is arithmetically impossible, exactly as for single mints.
#[kani::proof]
fn run_members_strictly_ascend_below_the_ceiling() {
    let physical: u64 = kani::any();
    let logical: u16 = kani::any();
    kani::assume(logical < u16::MAX);
    let len: u32 = kani::any();
    kani::assume(len >= 2);
    let index: u32 = kani::any();
    kani::assume(index < len - 1);
    // The no-saturation precondition: the successor member's carry fits.
    let total = u64::from(logical) + u64::from(index) + 1;
    kani::assume(physical.checked_add(total / u64::from(u16::MAX)).is_some());

    let first = Kairos::new(physical, logical, kani::any(), kani::any::<u16>());
    let run = super::run::KairosRun::new(first, len);
    let member = run.get(index).unwrap();
    let successor = run.get(index + 1).unwrap();
    assert!(
        successor > member,
        "run members must strictly ascend below the ceiling"
    );
}

/// After a run mint, the next mint strictly dominates every member (the
/// committed pair is the run's last stamp), for every sub-ceiling run and
/// every follow-up reading: the reservation is real, so no later stamp can
/// land inside it.
#[kani::proof]
#[kani::unwind(5)]
fn now_after_a_run_dominates_every_member() {
    let source = VirtualTimeSource::new(kani::any());
    let driver = source.clone();
    let clock = Clock::new(source, 1, ClockConfig::default()).unwrap();
    let len: u32 = kani::any();
    kani::assume(len >= 1 && len <= 3);
    let run = clock.now_run(core::num::NonZeroU32::new(len).unwrap(), 0u16);
    kani::assume(run.last().physical() < u64::MAX);
    driver.set(kani::any());
    let next = clock.now(0u16);
    let mut i: u32 = 0;
    while i < len {
        assert!(
            next > run.get(i).unwrap(),
            "a mint after a run must dominate every reserved member"
        );
        i += 1;
    }
}

/// The snapshot codec's rank-successor rule is the clock fold's own send
/// step, for every committed pair: minting at a frozen reading commits
/// exactly what the codec's step-zero record decodes. This is the axis-12
/// basis-mismatch hazard closed by proof where the dual-homed core cannot
/// share the function object itself (ruling R-25): a codec successor that
/// drifted from the fold would decode stamp successions the clock never
/// mints, and this harness turns that drift into a failing proof.
#[kani::proof]
fn snapshot_rank_step_matches_the_clock_fold() {
    let physical: u64 = kani::any();
    let logical: u16 = kani::any();
    let advance = super::fold::advance(Some((physical, logical)), physical, None);
    assert_eq!(
        crate::metis::rank_successor(physical, logical),
        (advance.physical, advance.logical),
        "the codec successor must be the fold's frozen-reading commit"
    );
}