//! Prusti proofs for URL contract types (from url crate).

#![cfg(feature = "verify-prusti")]
#![allow(unused_imports)]

use crate::verification::types::{
    UrlCanBeBase, UrlHttp, UrlHttps, UrlValid, UrlWithHost, ValidationError,
};
use prusti_contracts::*;

// URL Contract Proofs
// ============================================================================

#[cfg(all(prusti, feature = "url"))]
/// Prove that UrlHttps construction succeeds for HTTPS URLs.
#[requires(value.starts_with("https://"))]
#[ensures(result.is_ok() || result.is_err())]
pub fn verify_url_https_valid(value: &str) -> Result<UrlHttps, ValidationError> {
    UrlHttps::new(value)
}

#[cfg(all(prusti, feature = "url"))]
/// Prove that UrlHttps construction fails for non-HTTPS URLs.
#[requires(value.starts_with("http://") && !value.starts_with("https://"))]
#[ensures(result.is_err())]
pub fn verify_url_https_rejects_http(value: &str) -> Result<UrlHttps, ValidationError> {
    UrlHttps::new(value)
}

#[cfg(all(prusti, feature = "url"))]
/// Prove that UrlHttp construction succeeds for HTTP URLs.
#[requires(value.starts_with("http://") && !value.starts_with("https://"))]
#[ensures(result.is_ok() || result.is_err())]
pub fn verify_url_http_valid(value: &str) -> Result<UrlHttp, ValidationError> {
    UrlHttp::new(value)
}

#[cfg(all(prusti, feature = "url"))]
/// Prove that UrlHttp construction fails for HTTPS URLs.
#[requires(value.starts_with("https://"))]
#[ensures(result.is_err())]
pub fn verify_url_http_rejects_https(value: &str) -> Result<UrlHttp, ValidationError> {
    UrlHttp::new(value)
}

#[cfg(all(prusti, feature = "url"))]
/// Prove that UrlValid construction works for well-formed URLs.
#[ensures(match result {
    Ok(_) => true,
    Err(_) => true,
})]
pub fn verify_url_valid_construction(value: &str) -> Result<UrlValid, ValidationError> {
    UrlValid::new(value)
}

#[cfg(all(prusti, feature = "url"))]
/// Prove that UrlWithHost requires a host component.
#[ensures(match result {
    Ok(ref url) => url.get().host().is_some(),
    Err(_) => true,
})]
pub fn verify_url_with_host_requirement(value: &str) -> Result<UrlWithHost, ValidationError> {
    UrlWithHost::new(value)
}

#[cfg(all(prusti, feature = "url"))]
/// Prove that UrlCanBeBase rejects cannot-be-base URLs.
#[ensures(match result {
    Ok(ref url) => !url.get().cannot_be_a_base(),
    Err(_) => true,
})]
pub fn verify_url_can_be_base_check(value: &str) -> Result<UrlCanBeBase, ValidationError> {
    UrlCanBeBase::new(value)
}

#[cfg(all(prusti, feature = "url"))]
/// Prove URL trenchcoat pattern: wrap → unwrap preserves value.
#[requires(value.starts_with("https://"))]
#[ensures(match result {
    Ok(ref wrapped) => wrapped.clone().into_inner().as_str() == value,
    Err(_) => false,
})]
pub fn verify_url_trenchcoat(value: &str) -> Result<UrlHttps, ValidationError> {
    UrlHttps::new(value)
}

// ============================================================================
