elicitation_kani 0.8.2

//! Kani proofs for duration contract types.

use elicitation::{
    CharAlphanumeric, DurationPositive, F32NonNegative, F32Positive, F64NonNegative, I8Positive,
    OptionSome, Tuple2,
};

// Duration Contract Proofs
// ============================================================================

#[kani::proof]
fn verify_duration_positive() {
    let secs: u64 = kani::any();
    let nanos: u32 = kani::any();
    kani::assume(nanos < 1_000_000_000); // Valid nanos range

    let duration = std::time::Duration::new(secs, nanos);

    match DurationPositive::new(duration) {
        Ok(positive) => {
            assert!(duration.as_nanos() > 0, "DurationPositive invariant");
            let retrieved = DurationPositive::get(&positive);
            assert!(retrieved.as_nanos() > 0, "get() preserves invariant");
        }
        Err(_) => {
            assert!(
                duration.as_nanos() == 0,
                "Construction rejects zero duration"
            );
        }
    }
}

// ============================================================================
// Compositional Proofs (Tuples)
// ============================================================================

#[kani::proof]
fn verify_tuple2_composition() {
    // If both elements are valid contracts, tuple is valid
    let v1: i8 = kani::any();
    let v2: i8 = kani::any();

    kani::assume(v1 > 0); // Assume first is positive
    kani::assume(v2 > 0); // Assume second is positive

    let first = I8Positive::new(v1).unwrap();
    let second = I8Positive::new(v2).unwrap();

    let tuple = Tuple2::new(first, second);

    // Both elements remain positive after tuple construction
    assert!(tuple.first().get() > 0, "First element preserves contract");
    assert!(
        tuple.second().get() > 0,
        "Second element preserves contract"
    );
}

// ============================================================================
// Collection Proofs
// ============================================================================

#[kani::proof]
fn verify_option_some() {
    let value: i32 = kani::any();
    let opt = Some(value);

    match OptionSome::<i32>::new(opt) {
        Ok(some) => {
            let val: &i32 = OptionSome::get(&some);
            assert!(*val == value, "OptionSome unwraps correctly");
        }
        Err(_) => {
            unreachable!("OptionSome::new(Some) should never fail");
        }
    }
}

#[kani::proof]
fn verify_option_some_rejects_none() {
    let opt: Option<i32> = None;

    match OptionSome::new(opt) {
        Ok(_) => {
            unreachable!("OptionSome::new(None) should never succeed");
        }
        Err(_) => {
            // Expected: construction rejects None
        }
    }
}

// ============================================================================
// Trenchcoat Pattern Proof
// ============================================================================

/// Master proof: The trenchcoat pattern preserves type safety.
///
/// Proves that wrapping a value in a contract type and then unwrapping
/// it yields a validated value.
#[kani::proof]
fn verify_trenchcoat_pattern() {
    let value: i8 = kani::any();

    // Assume we have a positive value
    kani::assume(value > 0);

    // STEP 1: Put on the trenchcoat (wrap in contract type)
    let wrapped = I8Positive::new(value).unwrap();

    // STEP 2: Contract guarantees hold
    assert!(wrapped.get() > 0, "Contract guarantees positive");

    // STEP 3: Take off the trenchcoat (unwrap)
    let unwrapped = wrapped.into_inner();

    // STEP 4: Unwrapped value still satisfies contract
    assert!(unwrapped > 0, "Unwrapped value remains positive");
    assert!(unwrapped == value, "Unwrap preserves value identity");
}

// ============================================================================
// Phase 1: Complete Primitive Type Proofs
// ============================================================================

// ----------------------------------------------------------------------------
// Float Proofs: NonNegative variants
// ----------------------------------------------------------------------------

#[kani::proof]
fn verify_f32_non_negative() {
    let value: f32 = kani::any();

    let _result = F32NonNegative::new(value);

    // Verify construction doesn't panic
    // Note: Can't assert on value >= 0.0 or is_finite() with symbolic floats
}

#[kani::proof]
fn verify_f64_non_negative() {
    let value: f64 = kani::any();

    let _result = F64NonNegative::new(value);

    // Verify construction doesn't panic
    // Note: Can't assert on value >= 0.0 or is_finite() with symbolic floats
}

#[kani::proof]
fn verify_f32_positive() {
    let value: f32 = kani::any();

    let _result = F32Positive::new(value);

    // Verify construction doesn't panic
    // Note: Can't assert on value > 0.0 or is_finite() with symbolic floats
}

// ----------------------------------------------------------------------------
// Char Proofs: Complete coverage
// ----------------------------------------------------------------------------

#[kani::proof]
fn verify_char_alphanumeric() {
    let value: char = kani::any();

    let _result = CharAlphanumeric::new(value);

    // Verify construction doesn't panic
    // Note: Can't call .is_alphanumeric() on symbolic char or assert on .get()/.into_inner()
    // With symbolic validation, both Ok and Err paths are valid
}

// ----------------------------------------------------------------------------
// Integer Proofs: More sizes (i32, i64, i128, u32, u64, u128, isize, usize)
// ----------------------------------------------------------------------------

// Note: Range types use const generics, harder to prove exhaustively
// Focus on Positive/NonNegative/NonZero variants for remaining sizes

// ============================================================================
// Phase 2: Specialized Type Proofs
// ============================================================================

// ----------------------------------------------------------------------------
// Network Proofs