use verus_builtin_macros::verus;

verus! {

// ============================================================================
// Regex (regex crate)
// ============================================================================

/// Proof that Regex can be constructed when compilation succeeds.
///
/// Parameters:
/// - compiles: whether Regex::new(pattern) succeeds
pub fn verify_regex_construction(compiles: bool) -> (result: bool)
    ensures result == compiles,
{
    compiles
}

/// Proof that case-insensitive Regex can be constructed.
pub fn verify_regex_case_insensitive_construction(compiles: bool) -> (result: bool)
    ensures result == compiles,
{
    compiles
}

// ============================================================================
// Url (url crate)
// ============================================================================

/// Proof that Url can be constructed when parsing succeeds.
///
/// Parameters:
/// - parses: whether Url::parse(string) succeeds
pub fn verify_url_construction(parses: bool) -> (result: bool)
    ensures result == parses,
{
    parses
}

/// Proof that HTTPS URL can be constructed.
pub fn verify_url_https_construction(parses: bool, is_https: bool) -> (result: bool)
    ensures result == (parses && is_https),
{
    parses && is_https
}

/// Proof that HTTP URL can be constructed.
pub fn verify_url_http_construction(parses: bool, is_http: bool) -> (result: bool)
    ensures result == (parses && is_http),
{
    parses && is_http
}

// ============================================================================
// UUID (uuid crate)
// ============================================================================

/// Proof that UUID can be constructed when parsing succeeds.
pub fn verify_uuid_construction(parses: bool) -> (result: bool)
    ensures result == parses,
{
    parses
}

/// Proof that UUID v4 can be constructed.
pub fn verify_uuid_v4_construction(parses: bool, is_v4: bool) -> (result: bool)
    ensures result == (parses && is_v4),
{
    parses && is_v4
}

/// Proof that non-nil UUID can be constructed.
pub fn verify_uuid_non_nil_construction(parses: bool, is_nil: bool) -> (result: bool)
    ensures result == (parses && !is_nil),
{
    parses && !is_nil
}

// ============================================================================
// DateTime (chrono crate)
// ============================================================================

/// Proof that DateTime can be constructed when parsing succeeds.
pub fn verify_datetime_construction(parses: bool) -> (result: bool)
    ensures result == parses,
{
    parses
}

/// Proof that DateTime after threshold can be constructed.
pub fn verify_datetime_after_construction(parses: bool, is_after: bool) -> (result: bool)
    ensures result == (parses && is_after),
{
    parses && is_after
}

/// Proof that DateTime before threshold can be constructed.
pub fn verify_datetime_before_construction(parses: bool, is_before: bool) -> (result: bool)
    ensures result == (parses && is_before),
{
    parses && is_before
}

// ============================================================================
// IP Address (std::net)
// ============================================================================

/// Proof that IpAddr can be constructed when parsing succeeds.
pub fn verify_ipaddr_construction(parses: bool) -> (result: bool)
    ensures result == parses,
{
    parses
}

/// Proof that private IP can be constructed.
pub fn verify_ip_private_construction(parses: bool, is_private: bool) -> (result: bool)
    ensures result == (parses && is_private),
{
    parses && is_private
}

/// Proof that public IP can be constructed.
pub fn verify_ip_public_construction(parses: bool, is_public: bool) -> (result: bool)
    ensures result == (parses && is_public),
{
    parses && is_public
}

/// Proof that IPv4 can be constructed.
pub fn verify_ipv4_construction(parses: bool) -> (result: bool)
    ensures result == parses,
{
    parses
}

/// Proof that IPv6 can be constructed.
pub fn verify_ipv6_construction(parses: bool) -> (result: bool)
    ensures result == parses,
{
    parses
}

// ============================================================================
// PathBuf (std::path)
// ============================================================================

/// Proof that PathBuf can be constructed.
pub fn verify_pathbuf_construction(is_empty: bool) -> (result: bool)
    ensures result == !is_empty,
{
    !is_empty
}

/// Proof that absolute path can be identified.
pub fn verify_path_absolute_construction(is_absolute: bool) -> (result: bool)
    ensures result == is_absolute,
{
    is_absolute
}

/// Proof that relative path can be identified.
pub fn verify_path_relative_construction(is_relative: bool) -> (result: bool)
    ensures result == is_relative,
{
    is_relative
}

// ============================================================================
// Duration (std::time)
// ============================================================================

/// Proof that Duration can be constructed.
pub fn verify_duration_construction() -> (result: bool)
    ensures result == true,
{
    true
}

/// Proof that positive Duration can be constructed.
pub fn verify_duration_positive_construction(is_positive: bool) -> (result: bool)
    ensures result == is_positive,
{
    is_positive
}

// ============================================================================
// serde_json::Value
// ============================================================================

/// Proof that JSON Value can be constructed.
pub fn verify_json_value_construction() -> (result: bool)
    ensures result == true,
{
    true
}

/// Proof that JSON object can be constructed.
pub fn verify_json_object_construction(is_object: bool) -> (result: bool)
    ensures result == is_object,
{
    is_object
}

/// Proof that JSON array can be constructed.
pub fn verify_json_array_construction(is_array: bool) -> (result: bool)
    ensures result == is_array,
{
    is_array
}

/// Proof that non-null JSON value can be constructed.
pub fn verify_json_non_null_construction(is_null: bool) -> (result: bool)
    ensures result == !is_null,
{
    !is_null
}

} // verus!
