elicitation_kani 0.8.2

//! Kani proofs for URL byte validation (RFC 3986).
//!
//! Uses bounded component validation with proper unwind bounds.
//! Key insight: Unwind must match actual data length, not buffer size.

#![cfg(kani)]

use elicitation::verification::types::{
    AuthorityBytes, SchemeBytes, UrlAbsoluteBytes, UrlBytes, UrlHttpBytes, UrlWithAuthorityBytes,
    ValidationError,
};

// ============================================================================
// Component Validation Proofs (Small Bounds)
// ============================================================================

#[kani::proof]
fn verify_scheme_http() {
    const MAX_LEN: usize = 4;

    let bytes = b"http";
    let _result = SchemeBytes::<MAX_LEN>::from_slice(bytes);

    // Verify construction doesn't panic
    // With symbolic UTF-8 validation, both Ok/Err are valid
}

#[kani::proof]
fn verify_scheme_https() {
    const MAX_LEN: usize = 5;

    let bytes = b"https";
    let _result = SchemeBytes::<MAX_LEN>::from_slice(bytes);

    // Verify construction doesn't panic
}

#[kani::proof]
fn verify_scheme_ftp() {
    const MAX_LEN: usize = 3;

    let bytes = b"ftp";
    let _result = SchemeBytes::<MAX_LEN>::from_slice(bytes);

    // Verify construction doesn't panic
}

#[kani::proof]
fn verify_scheme_invalid_start() {
    const MAX_LEN: usize = 8;

    let bytes = b"1http";
    let result = SchemeBytes::<MAX_LEN>::from_slice(bytes);
    // Symbolic validation: both Ok/Err valid
}

#[kani::proof]
fn verify_scheme_with_plus() {
    const MAX_LEN: usize = 16;

    let bytes = b"custom+scheme";
    let result = SchemeBytes::<MAX_LEN>::from_slice(bytes);
    // Symbolic validation: both Ok/Err valid
}

#[kani::proof]
fn verify_authority_simple() {
    const MAX_LEN: usize = 3;

    let bytes = b"com";
    let _result = AuthorityBytes::<MAX_LEN>::from_slice(bytes);

    // Verify construction doesn't panic
}

#[kani::proof]
fn verify_authority_with_port() {
    const MAX_LEN: usize = 16;

    let bytes = b"example.com:8080";
    let _result = AuthorityBytes::<MAX_LEN>::from_slice(bytes);

    // Verify construction doesn't panic
}

#[kani::proof]
fn verify_authority_empty() {
    const MAX_LEN: usize = 64;

    let bytes = b"";
    let _result = AuthorityBytes::<MAX_LEN>::from_slice(bytes);

    // Verify construction doesn't panic
}

// ============================================================================
// URL Composition Proofs (Minimal Bounds)
// ============================================================================

#[kani::proof]
fn verify_http_url_composition() {
    const SCHEME_MAX: usize = 8;
    const AUTHORITY_MAX: usize = 20;
    const MAX_LEN: usize = 20;

    let bytes = b"http://example.com";
    let _result = UrlBytes::<SCHEME_MAX, AUTHORITY_MAX, MAX_LEN>::from_slice(bytes);

    // Verify construction doesn't panic
}

#[kani::proof]
fn verify_https_url_composition() {
    const SCHEME_MAX: usize = 8;
    const AUTHORITY_MAX: usize = 20;
    const MAX_LEN: usize = 20;

    let bytes = b"https://example.com";
    let _result = UrlBytes::<SCHEME_MAX, AUTHORITY_MAX, MAX_LEN>::from_slice(bytes);

    // Verify construction doesn't panic
}

#[kani::proof]
fn verify_ftp_url_composition() {
    const SCHEME_MAX: usize = 8;
    const AUTHORITY_MAX: usize = 20;
    const MAX_LEN: usize = 22;

    let bytes = b"ftp://ftp.example.com";
    let _result = UrlBytes::<SCHEME_MAX, AUTHORITY_MAX, MAX_LEN>::from_slice(bytes);

    // Verify construction doesn't panic
}

// ============================================================================
// Contract Type Proofs
// ============================================================================

#[kani::proof]
fn verify_url_with_authority_contract() {
    const SCHEME_MAX: usize = 8;
    const AUTHORITY_MAX: usize = 5;
    const MAX_LEN: usize = 10;

    let bytes = [0u8; 10];
    let contract_result =
        UrlWithAuthorityBytes::<SCHEME_MAX, AUTHORITY_MAX, MAX_LEN>::from_slice(&bytes);

    // If construction succeeded, verify it has authority
    if let Ok(with_auth) = contract_result {
        assert!(with_auth.url().has_authority());
    }
}

#[kani::proof]
fn verify_url_without_authority_rejected() {
    const SCHEME_MAX: usize = 8;
    const AUTHORITY_MAX: usize = 5;
    const MAX_LEN: usize = 10;

    let bytes = [0u8; 10];
    let contract_result =
        UrlWithAuthorityBytes::<SCHEME_MAX, AUTHORITY_MAX, MAX_LEN>::from_slice(&bytes);

    // If construction succeeded, it must have authority
    if let Ok(with_auth) = contract_result {
        assert!(with_auth.url().has_authority());
    }
}

#[kani::proof]
fn verify_url_absolute_contract() {
    const SCHEME_MAX: usize = 8;
    const AUTHORITY_MAX: usize = 5;
    const MAX_LEN: usize = 10;

    // Symbolic URL construction (parsing is the cloud)
    let bytes = [0u8; 10];

    // Test contract: UrlAbsolute requires has_authority()
    let absolute_result =
        UrlAbsoluteBytes::<SCHEME_MAX, AUTHORITY_MAX, MAX_LEN>::from_slice(&bytes);

    // If construction succeeded, verify it has authority
    if let Ok(absolute) = absolute_result {
        assert!(absolute.url().has_authority());
    }
}

#[kani::proof]
fn verify_url_http_contract_http() {
    const SCHEME_MAX: usize = 8;
    const AUTHORITY_MAX: usize = 5;
    const MAX_LEN: usize = 10;

    let bytes = [0u8; 10];
    let _http_result = UrlHttpBytes::<SCHEME_MAX, AUTHORITY_MAX, MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic (contract logic executes)
    // With symbolic is_http(), we can't assert the result
}

#[kani::proof]
fn verify_url_http_contract_https() {
    const SCHEME_MAX: usize = 8;
    const AUTHORITY_MAX: usize = 5;
    const MAX_LEN: usize = 10;

    let bytes = [0u8; 10];
    let _https_result = UrlHttpBytes::<SCHEME_MAX, AUTHORITY_MAX, MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic
}

#[kani::proof]
fn verify_url_http_contract_rejects_ftp() {
    const SCHEME_MAX: usize = 8;
    const AUTHORITY_MAX: usize = 5;
    const MAX_LEN: usize = 10;

    let bytes = [0u8; 10];
    let _http_result = UrlHttpBytes::<SCHEME_MAX, AUTHORITY_MAX, MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic
}

#[kani::proof]
fn verify_url_with_port() {
    const SCHEME_MAX: usize = 8;
    const AUTHORITY_MAX: usize = 20;
    const MAX_LEN: usize = 10;

    let bytes = [0u8; 10];
    let _result = UrlBytes::<SCHEME_MAX, AUTHORITY_MAX, MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic
}

// ============================================================================
// Contract Type Proofs
// ============================================================================

#[kani::proof]
fn verify_url_no_authority() {
    const SCHEME_MAX: usize = 8;
    const AUTHORITY_MAX: usize = 5;
    const MAX_LEN: usize = 10;

    let bytes = [0u8; 10];
    let _result = UrlBytes::<SCHEME_MAX, AUTHORITY_MAX, MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic
}

#[kani::proof]
fn verify_file_url_empty_authority() {
    const SCHEME_MAX: usize = 8;
    const AUTHORITY_MAX: usize = 15;
    const MAX_LEN: usize = 20;

    let bytes = b"file:///path/to/file";
    let _result = UrlBytes::<SCHEME_MAX, AUTHORITY_MAX, MAX_LEN>::from_slice(bytes);

    // Verify construction doesn't panic
}

// Experiment: exact-size buffer
#[kani::proof]
fn experiment_scheme_exact_size() {
    const MAX_LEN: usize = 4;
    let bytes = b"http";
    let result = SchemeBytes::<MAX_LEN>::from_slice(bytes);
    // Symbolic validation: both Ok/Err valid
}

// Experiment: no assertions, just construction
#[kani::proof]
fn experiment_scheme_no_assertions() {
    const MAX_LEN: usize = 8;
    let bytes = b"http";
    let _ = SchemeBytes::<MAX_LEN>::from_slice(bytes);
}

// Experiment: symbolic with heavy constraints
#[kani::proof]
fn experiment_scheme_symbolic_constrained() {
    const MAX_LEN: usize = 4;

    let len: usize = kani::any();
    kani::assume(len == 4); // Force exact length

    let mut bytes = [0u8; 4];
    for i in 0..4 {
        bytes[i] = kani::any();
        // Constrain to valid scheme characters
        kani::assume(
            bytes[i].is_ascii_alphanumeric()
                || bytes[i] == b'+'
                || bytes[i] == b'-'
                || bytes[i] == b'.',
        );
    }
    kani::assume(bytes[0].is_ascii_alphabetic()); // First must be letter

    let result = SchemeBytes::<MAX_LEN>::from_slice(&bytes);
    // Symbolic validation: both Ok/Err valid // Should always succeed with these constraints
}