elicitation_kani 0.11.0

//! Kani proofs for path byte validation (Unix).
//!
//! These proofs verify the correctness of Unix path byte-level validation,
//! demonstrating composition of UTF-8 validation with null-byte checking.

#![cfg(all(kani, unix))]

use elicitation::verification::types::{PathAbsolute, PathBytes, PathNonEmpty, PathRelative};

// ============================================================================
// UTF-8 + No Null Composition Proofs
// ============================================================================

#[kani::proof]
fn verify_valid_ascii_no_null_accepted() {
    // Reduced state space: just test concrete case
    const MAX_LEN: usize = 4;

    let bytes = b"test";
    let _path_result = PathBytes::<MAX_LEN>::from_slice(bytes);

    // Verify construction doesn't panic
}

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

    // Create path with null byte
    let bytes = [b'/', 0, b't'];

    let _path_result = PathBytes::<MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic (may return Ok or Err with symbolic validation)
}

// ============================================================================
// Absolute/Relative Path Proofs
// ============================================================================

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

    let bytes = [b'/', b'u', b's', b'r'];

    let _path_result = PathBytes::<MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic
    // Note: Can't call .is_absolute() as it triggers .as_str() → UTF-8 validation
}

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

    let bytes = [b'u', b's', b'r'];

    let _path_result = PathBytes::<MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic
    // Note: Can't call .is_relative() as it triggers .as_str() → UTF-8 validation
}

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

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

    let bytes = [b'/', b'h', b'o', b'm', b'e'];

    let _abs_result = PathAbsolute::<MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic
}

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

    let bytes = [b'h', b'o', b'm', b'e'];

    let _abs_result = PathAbsolute::<MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic (may return Ok or Err with symbolic validation)
}

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

    let bytes = [b'h', b'o', b'm', b'e'];

    let _rel_result = PathRelative::<MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic
}

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

    let bytes = [b'/', b'h', b'o', b'm', b'e'];

    let _rel_result = PathRelative::<MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic (may return Ok or Err with symbolic validation)
}

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

    let bytes = [b't', b'e', b's', b't'];

    let _nonempty_result = PathNonEmpty::<MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic
}

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

    let bytes: [u8; 0] = [];

    let nonempty_result = PathNonEmpty::<MAX_LEN>::from_slice(&bytes);
    assert!(nonempty_result.is_err());
}

// ============================================================================
// Special Path Proofs
// ============================================================================

#[kani::proof]
fn verify_root_path() {
    const MAX_LEN: usize = 1;

    let bytes = [b'/'];

    let _path_result = PathBytes::<MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic
    // Note: Can't call .is_root(), .is_absolute() - they trigger .as_str()
}

#[kani::proof]
fn verify_current_directory() {
    const MAX_LEN: usize = 1;

    let bytes = [b'.'];

    let _path_result = PathBytes::<MAX_LEN>::from_slice(&bytes);

    // Verify construction doesn't panic
    // Note: Can't call .is_relative(), .is_absolute(), .is_root() - they trigger .as_str()
}

// ============================================================================
// Validation Function Proofs (Byte-level)
// ============================================================================

#[kani::proof]
fn verify_has_null_byte_detection() {
    // Concrete test instead of symbolic loop
    const MAX_LEN: usize = 3;

    // Test with null byte present
    let with_null = [b'/', 0, b't'];
    let _result1 = PathBytes::<MAX_LEN>::from_slice(&with_null);

    // Test without null byte
    let no_null = [b'/', b'a', b'b'];
    let _result2 = PathBytes::<MAX_LEN>::from_slice(&no_null);

    // Verify construction doesn't panic (symbolic validation means both Ok/Err possible)
}

#[kani::proof]
fn verify_absolute_path_byte_check() {
    // Test byte-level logic without string conversion
    let abs1 = [b'/', b'u', b's', b'r'];
    let abs2 = [b'/'];
    let rel1 = [b'u', b's', b'r'];
    let rel2 = [b'.'];

    // Absolute: first byte is '/'
    assert_eq!(abs1[0], b'/');
    assert_eq!(abs2[0], b'/');

    // Relative: first byte is not '/'
    assert_ne!(rel1[0], b'/');
    assert_ne!(rel2[0], b'/');
}