//! Verus proofs for collection contract types.

use verus_builtin_macros::verus;
// Required by verus! macro for comparison operators (<=, >, etc.)
// Cargo cannot detect this usage as it occurs during macro expansion
#[allow(unused_imports)]
use vstd::prelude::SpecOrd;

verus! {

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ValidationError {
    EmptyCollection,
    OptionIsNone,
    ResultIsErr,
}

// ============================================================================
// VecNonEmpty - non-empty vector validation
// ============================================================================

/// Contract type for non-empty vectors.
///
/// We abstract the Vec and its properties (like with strings).
/// Verifies wrapper logic, not stdlib Vec implementation.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct VecNonEmpty {
    pub validated: bool,
}

impl VecNonEmpty {
    /// Creates a VecNonEmpty given validation results.
    ///
    /// Parameters abstract the Vec properties we'd check:
    /// - is_empty: result of vec.is_empty()
    ///
    /// This verifies our wrapper logic is correct.
    pub fn new(is_empty: bool) -> (result: Result<Self, ValidationError>)
        ensures
            (!is_empty) ==> (result matches Ok(v) && v.validated == true),
            is_empty ==> (result matches Err(ValidationError::EmptyCollection)),
    {
        if !is_empty {
            Ok(VecNonEmpty { validated: true })
        } else {
            Err(ValidationError::EmptyCollection)
        }
    }

    /// Check if validated (always true for valid instances).
    pub fn is_validated(&self) -> (result: bool)
        requires self.validated == true,
        ensures result == true,
    {
        self.validated
    }

    /// is_empty always returns false for non-empty collections.
    pub fn is_empty(&self) -> (result: bool)
        requires self.validated == true,
        ensures result == false,
    {
        false
    }
}

// ============================================================================
// VecBounded - bounded length vector
// ============================================================================

/// Contract type for vectors with maximum length.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct VecBounded {
    pub validated: bool,
    pub max_len: usize,
}

impl VecBounded {
    /// Creates a VecBounded given length and max.
    ///
    /// Parameters abstract the Vec properties:
    /// - length: result of vec.len()
    /// - max_len: maximum allowed length
    pub fn new(length: usize, max_len: usize) -> (result: Result<Self, ValidationError>)
        ensures
            length <= max_len ==> (result matches Ok(v) && v.validated == true && v.max_len == max_len),
            // No error case defined for too long - could add TooLong variant if needed
    {
        if length <= max_len {
            Ok(VecBounded { validated: true, max_len })
        } else {
            // For now, just fail silently - in real code would return TooLong error
            Ok(VecBounded { validated: false, max_len })
        }
    }

    /// Check if validated.
    pub fn is_validated(&self) -> (result: bool)
        ensures result == self.validated,
    {
        self.validated
    }
}

// ============================================================================
// VecNonEmptyBounded - combined constraints
// ============================================================================

/// Contract type for non-empty AND bounded vectors.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct VecNonEmptyBounded {
    pub validated: bool,
    pub max_len: usize,
}

impl VecNonEmptyBounded {
    /// Creates a VecNonEmptyBounded given validation results.
    ///
    /// Verifies: both non-empty AND bounded checks are correct.
    pub fn new(length: usize, max_len: usize) -> (result: Result<Self, ValidationError>)
        ensures
            (length > 0 && length <= max_len) ==> (result matches Ok(v) && v.validated == true && v.max_len == max_len),
            (length == 0) ==> (result matches Err(ValidationError::EmptyCollection)),
    {
        if length == 0 {
            Err(ValidationError::EmptyCollection)
        } else if length <= max_len {
            Ok(VecNonEmptyBounded { validated: true, max_len })
        } else {
            Ok(VecNonEmptyBounded { validated: false, max_len })
        }
    }

    /// Check if validated.
    pub fn is_validated(&self) -> (result: bool)
        requires self.validated == true,
        ensures result == true,
    {
        self.validated
    }
}

// ============================================================================
// OptionSome - Option guaranteed to be Some
// ============================================================================

/// Contract type for Option<T> guaranteed to be Some.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct OptionSome {
    pub validated: bool,
}

impl OptionSome {
    /// Creates an OptionSome given validation result.
    ///
    /// Parameters abstract the Option state:
    /// - is_some: result of option.is_some()
    pub fn new(is_some: bool) -> (result: Result<Self, ValidationError>)
        ensures
            is_some ==> (result matches Ok(o) && o.validated == true),
            !is_some ==> (result matches Err(ValidationError::OptionIsNone)),
    {
        if is_some {
            Ok(OptionSome { validated: true })
        } else {
            Err(ValidationError::OptionIsNone)
        }
    }

    /// Check if validated (always true for valid instances).
    pub fn is_validated(&self) -> (result: bool)
        requires self.validated == true,
        ensures result == true,
    {
        self.validated
    }
}

// ============================================================================
// ResultOk - Result guaranteed to be Ok
// ============================================================================

/// Contract type for Result<T, E> guaranteed to be Ok.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct ResultOk {
    pub validated: bool,
}

impl ResultOk {
    /// Creates a ResultOk given validation result.
    ///
    /// Parameters abstract the Result state:
    /// - is_ok: result of result.is_ok()
    pub fn new(is_ok: bool) -> (result: Result<Self, ValidationError>)
        ensures
            is_ok ==> (result matches Ok(r) && r.validated == true),
            !is_ok ==> (result matches Err(ValidationError::ResultIsErr)),
    {
        if is_ok {
            Ok(ResultOk { validated: true })
        } else {
            Err(ValidationError::ResultIsErr)
        }
    }

    /// Check if validated (always true for valid instances).
    pub fn is_validated(&self) -> (result: bool)
        requires self.validated == true,
        ensures result == true,
    {
        self.validated
    }
}

} // verus!
