// Copyright 2025-present Harīṣh Tummalachērla
// SPDX-License-Identifier: Apache-2.0

//! Runtime contracts that panic when Lean invariants are violated.
//!
//! Every check here mirrors a theorem or axiom from the Lean proofs. If you hit
//! a contract violation, your code is wrong - not the check. The proofs guarantee
//! these invariants are satisfiable; the contracts catch when you fail to satisfy them.
//!
//! **Zero-cost in release builds.** All checks use `debug_assert!`, so they compile
//! away when you ship. Run tests in debug mode to catch violations.
//!
//! # Lean Correspondence
//!
//! | Contract                       | Lean Specification                    |
//! |--------------------------------|---------------------------------------|
//! | `check_suffix_entry_valid`     | `SuffixEntry.WellFormed`              |
//! | `check_suffix_array_sorted`    | `SuffixArray.Sorted`                  |
//! | `check_index_well_formed`      | `SearchIndex.WellFormed`              |
//! | `check_field_hierarchy`        | `Scoring.title_beats_heading`         |
//! | `check_lcp_correct`            | `SuffixArray.LcpCorrect`              |
//!
//! # Don't Remove These
//!
//! Yes, removing these checks makes the code "faster" in debug builds. But you're
//! also removing your only runtime feedback that the Lean invariants hold. The next
//! bug you introduce will silently corrupt results instead of panicking loudly.

// ============================================================================
// COMPILE-TIME ASSERTIONS (evaluated at build time)
// ============================================================================

/// Compile-time proof that field type dominance holds.
///
/// If someone changes the scoring constants without thinking, this fails at
/// `cargo build`, not at runtime. The math is trivial, but having the compiler
/// enforce it means you can't ship broken ranking.
const _: () = {
    const TITLE: f64 = 100.0;
    const HEADING: f64 = 10.0;
    const CONTENT: f64 = 1.0;
    const MAX_BOOST: f64 = 0.5;

    // INVARIANT: title_beats_heading (from Scoring.lean)
    // worst_title > best_heading
    const WORST_TITLE: f64 = TITLE - MAX_BOOST;
    const BEST_HEADING: f64 = HEADING + MAX_BOOST;
    assert!(WORST_TITLE > BEST_HEADING); // 99.5 > 10.5 ✓

    // INVARIANT: heading_beats_content (from Scoring.lean)
    // worst_heading > best_content
    const WORST_HEADING: f64 = HEADING - MAX_BOOST;
    const BEST_CONTENT: f64 = CONTENT + MAX_BOOST;
    assert!(WORST_HEADING > BEST_CONTENT); // 9.5 > 1.5 ✓
};

use crate::types::{FieldType, SearchIndex, SuffixEntry};
use crate::util::normalize::common_prefix_len;

// ============================================================================
// SUFFIX ENTRY CONTRACTS
// ============================================================================

/// Does this suffix entry point to a valid location?
///
/// A suffix entry is well-formed if `doc_id` indexes a real document and `offset`
/// points inside that document's text. Strict inequality on offset because we're
/// indexing non-empty suffixes - pointing to the end of a string gives an empty suffix.
///
/// **Lean**: `SuffixEntry.WellFormed` in `Types.lean`
///
/// # Panics (debug builds only)
/// If `doc_id >= texts.len()` or `offset >= texts[doc_id].len()`.
#[inline]
pub fn check_suffix_entry_valid(entry: &SuffixEntry, texts: &[String]) {
    debug_assert!(
        entry.doc_id < texts.len(),
        "Contract violation: SuffixEntry.WellFormed - doc_id {} >= texts.len() {}",
        entry.doc_id,
        texts.len()
    );

    if entry.doc_id < texts.len() {
        debug_assert!(
            entry.offset < texts[entry.doc_id].len(),
            "Contract violation: SuffixEntry.WellFormed - offset {} >= texts[{}].len() {}",
            entry.offset,
            entry.doc_id,
            texts[entry.doc_id].len()
        );
    }
}

/// Batch validation for all suffix entries.
///
/// Loops through the entire array and panics at the first invalid entry.
/// Not the most efficient approach, but you only run this in debug builds anyway.
#[inline]
pub fn check_all_entries_valid(suffix_array: &[SuffixEntry], texts: &[String]) {
    for (i, entry) in suffix_array.iter().enumerate() {
        debug_assert!(
            entry.doc_id < texts.len(),
            "Contract violation: suffix_array[{}].doc_id {} >= texts.len() {}",
            i,
            entry.doc_id,
            texts.len()
        );

        if entry.doc_id < texts.len() {
            debug_assert!(
                entry.offset < texts[entry.doc_id].len(),
                "Contract violation: suffix_array[{}].offset {} >= texts[{}].len() {}",
                i,
                entry.offset,
                entry.doc_id,
                texts[entry.doc_id].len()
            );
        }
    }
}

// ============================================================================
// SUFFIX ARRAY CONTRACTS
// ============================================================================

/// Is the suffix array sorted? Binary search correctness depends on this.
///
/// We check adjacent pairs only - O(n) instead of O(n²) for all pairs.
/// If adjacent pairs are ordered, transitivity gives us the full property.
///
/// **Lean**: `SuffixArray.Sorted` in `SuffixArray.lean`
///
/// # Panics (debug builds only)
/// If any `suffix_array[i-1] > suffix_array[i]`.
#[inline]
pub fn check_suffix_array_sorted(texts: &[String], suffix_array: &[SuffixEntry]) {
    for i in 1..suffix_array.len() {
        let prev = &suffix_array[i - 1];
        let curr = &suffix_array[i];

        let prev_suffix = texts
            .get(prev.doc_id)
            .and_then(|t| t.get(prev.offset..))
            .unwrap_or("");
        let curr_suffix = texts
            .get(curr.doc_id)
            .and_then(|t| t.get(curr.offset..))
            .unwrap_or("");

        debug_assert!(
            prev_suffix <= curr_suffix,
            "Contract violation: SuffixArray.Sorted - \
             suffix_array[{}] ('{}') > suffix_array[{}] ('{}')",
            i - 1,
            prev_suffix.chars().take(20).collect::<String>(),
            i,
            curr_suffix.chars().take(20).collect::<String>()
        );
    }
}

/// Every suffix should be in the array. This checks for gaps.
///
/// O(n × m) where n = suffix array length, m = total character count.
/// You probably don't want to run this on large indexes, but it's invaluable
/// for catching off-by-one errors during development.
///
/// # Lean Specification
/// ```lean
/// def Complete (sa : Array SuffixEntry) (texts : Array String) : Prop :=
///   ∀ doc_id : Nat, (hd : doc_id < texts.size) →
///   ∀ offset : Nat, offset < (texts[doc_id]).length →
///     ∃ i : Nat, i < sa.size ∧ sa[i].doc_id = doc_id ∧ sa[i].offset = offset
/// ```
///
/// # Panics (debug builds only)
/// If any `(doc_id, offset)` pair is missing from the suffix array.
#[inline]
pub fn check_suffix_array_complete(texts: &[String], suffix_array: &[SuffixEntry]) {
    for (doc_id, text) in texts.iter().enumerate() {
        for offset in 0..text.len() {
            let found = suffix_array
                .iter()
                .any(|e| e.doc_id == doc_id && e.offset == offset);

            debug_assert!(
                found,
                "Contract violation: SuffixArray.Complete - \
                 missing entry for doc_id={}, offset={} (suffix: '{}')",
                doc_id,
                offset,
                text.get(offset..)
                    .unwrap_or("")
                    .chars()
                    .take(20)
                    .collect::<String>()
            );
        }
    }
}

// ============================================================================
// LCP ARRAY CONTRACTS
// ============================================================================

/// Verify the LCP (longest common prefix) array is correct.
///
/// Each `lcp[i]` should equal the common prefix length between adjacent suffixes
/// `suffix_array[i-1]` and `suffix_array[i]`. The first entry is always 0 because
/// there's no previous suffix to compare against.
///
/// # Lean Specification
/// ```lean
/// def LcpCorrect (sa : Array SuffixEntry) (lcp : Array Nat) (texts : Array String) : Prop :=
///   lcp.size = sa.size ∧
///   (sa.size > 0 → lcp[0] = 0) ∧
///   ∀ i : Nat, (hi : i < sa.size) → i > 0 →
///     lcp[i] = (String.commonPrefix (suffixAt texts sa[i-1]) (suffixAt texts sa[i])).length
/// ```
///
/// # Panics (debug builds only)
/// If `lcp.len() != suffix_array.len()` or any LCP value is wrong.
#[inline]
pub fn check_lcp_correct(texts: &[String], suffix_array: &[SuffixEntry], lcp: &[usize]) {
    debug_assert_eq!(
        lcp.len(),
        suffix_array.len(),
        "Contract violation: LcpCorrect - lcp.len() {} != suffix_array.len() {}",
        lcp.len(),
        suffix_array.len()
    );

    if !lcp.is_empty() {
        debug_assert_eq!(
            lcp[0], 0,
            "Contract violation: LcpCorrect - lcp[0] = {} (expected 0)",
            lcp[0]
        );
    }

    for i in 1..suffix_array.len() {
        let prev = &suffix_array[i - 1];
        let curr = &suffix_array[i];

        let prev_suffix = texts
            .get(prev.doc_id)
            .and_then(|t| t.get(prev.offset..))
            .unwrap_or("");
        let curr_suffix = texts
            .get(curr.doc_id)
            .and_then(|t| t.get(curr.offset..))
            .unwrap_or("");

        let expected = common_prefix_len(prev_suffix, curr_suffix);

        debug_assert_eq!(
            lcp[i], expected,
            "Contract violation: LcpCorrect - lcp[{}] = {} (expected {})",
            i, lcp[i], expected
        );
    }
}

// ============================================================================
// SEARCH INDEX CONTRACTS
// ============================================================================

/// The main index validation: checks all the structural invariants.
///
/// This verifies that `docs` and `texts` are aligned, that `lcp` and `suffix_array`
/// are the same length, that all suffix entries point to valid locations, and that
/// the suffix array is sorted. If any of these fail, the index is corrupt.
///
/// # Lean Specification
/// ```lean
/// def SearchIndex.WellFormed (idx : SearchIndex) : Prop :=
///   idx.docs.size = idx.texts.size ∧
///   idx.lcp.size = idx.suffix_array.size ∧
///   Sorted idx.suffix_array idx.texts ∧
///   (∀ e ∈ idx.suffix_array, SuffixEntry.WellFormed e idx.texts)
/// ```
///
/// # Panics (debug builds only)
/// If any structural invariant is violated.
#[inline]
pub fn check_index_well_formed(index: &SearchIndex) {
    // docs.size = texts.size
    debug_assert_eq!(
        index.docs.len(),
        index.texts.len(),
        "Contract violation: SearchIndex.WellFormed - \
         docs.len() {} != texts.len() {}",
        index.docs.len(),
        index.texts.len()
    );

    // lcp.size = suffix_array.size
    debug_assert_eq!(
        index.lcp.len(),
        index.suffix_array.len(),
        "Contract violation: SearchIndex.WellFormed - \
         lcp.len() {} != suffix_array.len() {}",
        index.lcp.len(),
        index.suffix_array.len()
    );

    // All entries well-formed
    check_all_entries_valid(&index.suffix_array, &index.texts);

    // Suffix array sorted
    check_suffix_array_sorted(&index.texts, &index.suffix_array);
}

/// The paranoid validation: checks everything including completeness.
///
/// This adds the O(n × m) completeness check on top of `check_index_well_formed`.
/// Useful for debugging when you suspect missing suffixes, but way too slow for
/// production test suites on large indexes.
#[inline]
pub fn check_index_complete(index: &SearchIndex) {
    check_index_well_formed(index);
    check_suffix_array_complete(&index.texts, &index.suffix_array);
    check_lcp_correct(&index.texts, &index.suffix_array, &index.lcp);
}

// ============================================================================
// SCORING CONTRACTS
// ============================================================================

/// Verify that title > heading > content in all cases.
///
/// The scoring constants must be chosen so that even the worst title score beats
/// the best heading score. This is what makes field-type search ranking predictable:
/// a title match always surfaces above a content match, regardless of position boosts.
///
/// # Lean Specification
/// ```lean
/// theorem title_beats_heading :
///     baseScore .title - maxPositionBoost > baseScore .heading + maxPositionBoost
///
/// theorem heading_beats_content :
///     baseScore .heading - maxPositionBoost > baseScore .content + maxPositionBoost
/// ```
///
/// This is a static check - it should always pass unless someone "optimized" the
/// scoring constants without checking the math.
#[inline]
pub fn check_field_hierarchy() {
    const TITLE_BASE: f64 = 100.0;
    const HEADING_BASE: f64 = 10.0;
    const CONTENT_BASE: f64 = 1.0;
    const MAX_POSITION_BOOST: f64 = 0.5;

    // Title always beats heading
    let worst_title = TITLE_BASE - MAX_POSITION_BOOST;
    let best_heading = HEADING_BASE + MAX_POSITION_BOOST;
    debug_assert!(
        worst_title > best_heading,
        "Contract violation: title_beats_heading - \
         worst title ({}) <= best heading ({})",
        worst_title,
        best_heading
    );

    // Heading always beats content
    let worst_heading = HEADING_BASE - MAX_POSITION_BOOST;
    let best_content = CONTENT_BASE + MAX_POSITION_BOOST;
    debug_assert!(
        worst_heading > best_content,
        "Contract violation: heading_beats_content - \
         worst heading ({}) <= best content ({})",
        worst_heading,
        best_content
    );
}

/// Runtime check that two scores respect field type dominance.
///
/// Given scores for two field types, this verifies the higher-ranked field has
/// the higher score. Useful for catching ranking bugs in search results.
#[inline]
pub fn check_score_dominance(score1: f64, field1: &FieldType, score2: f64, field2: &FieldType) {
    use std::cmp::Ordering;

    let cmp = match (field1, field2) {
        (FieldType::Title, FieldType::Heading) => Some(Ordering::Greater),
        (FieldType::Title, FieldType::Content) => Some(Ordering::Greater),
        (FieldType::Heading, FieldType::Content) => Some(Ordering::Greater),
        (FieldType::Heading, FieldType::Title) => Some(Ordering::Less),
        (FieldType::Content, FieldType::Title) => Some(Ordering::Less),
        (FieldType::Content, FieldType::Heading) => Some(Ordering::Less),
        _ => None, // Same field type, no dominance requirement
    };

    if let Some(expected) = cmp {
        let actual = score1.partial_cmp(&score2).unwrap_or(Ordering::Equal);
        debug_assert_eq!(
            actual, expected,
            "Contract violation: field_type_dominance - \
             {:?} score ({}) should {:?} {:?} score ({})",
            field1, score1, expected, field2, score2
        );
    }
}

// ============================================================================
// BINARY SEARCH CONTRACTS
// ============================================================================

/// Verify the suffix array is sorted before binary search.
///
/// Binary search on an unsorted array is a fun way to get wrong results fast.
/// This is just a wrapper around `check_suffix_array_sorted` - it exists for
/// semantic clarity at call sites.
#[inline]
pub fn check_binary_search_precondition(texts: &[String], suffix_array: &[SuffixEntry]) {
    check_suffix_array_sorted(texts, suffix_array);
}

/// Verify binary search returns a valid index.
///
/// The result must be in `[0, suffix_array.len()]`. Returning exactly `len()` is
/// valid - it means "nothing matched" (insertion point past the end).
///
/// # Lean Specification
/// ```lean
/// axiom findFirstGe_bounds (sa : Array SuffixEntry) (texts : Array String) (target : String) :
///     findFirstGe sa texts target ≤ sa.size
/// ```
#[inline]
pub fn check_binary_search_result(result: usize, suffix_array_len: usize) {
    debug_assert!(
        result <= suffix_array_len,
        "Contract violation: findFirstGe_bounds - \
         result {} > suffix_array.len() {}",
        result,
        suffix_array_len
    );
}

// ============================================================================
// LEVENSHTEIN CONTRACTS
// ============================================================================

/// Verify the early-exit optimization is sound.
///
/// Edit distance is at least `|len(a) - len(b)|` - you need at least that many
/// insertions or deletions. So if the length difference exceeds `max`, we can
/// skip the expensive DP computation entirely.
///
/// # Lean Specification
/// ```lean
/// axiom length_diff_lower_bound (a b : String) :
///     (a.length - b.length : Int).natAbs ≤ editDistance a b
/// ```
#[inline]
pub fn check_levenshtein_early_exit(a: &str, b: &str, max: usize, result: bool) {
    let len_diff = (a.len() as isize - b.len() as isize).unsigned_abs();

    // If we returned false due to early exit, length difference must exceed max
    if !result && len_diff > max {
        // This is the expected behavior - early exit is correct
    } else if !result {
        // We returned false but not due to early exit
        // The actual edit distance must be > max
        // (We can't easily verify this without computing full distance)
    }

    // If we returned true, the length difference must be <= max
    if result {
        debug_assert!(
            len_diff <= max,
            "Contract violation: levenshtein_within returned true but \
             |len('{}') - len('{}')| = {} > max = {}",
            a.chars().take(10).collect::<String>(),
            b.chars().take(10).collect::<String>(),
            len_diff,
            max
        );
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::index::build_index;
    use crate::testing::make_doc_simple;

    #[test]
    fn test_check_suffix_entry_valid() {
        let texts = vec!["hello".to_string()];
        let valid_entry = SuffixEntry {
            doc_id: 0,
            offset: 2,
        };

        // Should not panic
        check_suffix_entry_valid(&valid_entry, &texts);
    }

    #[test]
    #[should_panic(expected = "Contract violation")]
    fn test_check_suffix_entry_invalid_doc_id() {
        let texts = vec!["hello".to_string()];
        let invalid_entry = SuffixEntry {
            doc_id: 5,
            offset: 0,
        };

        check_suffix_entry_valid(&invalid_entry, &texts);
    }

    #[test]
    fn test_check_index_well_formed() {
        let docs = vec![make_doc_simple(0), make_doc_simple(1)];
        let texts = vec!["hello".to_string(), "world".to_string()];
        let index = build_index(docs, texts, vec![]);

        // Should not panic
        check_index_well_formed(&index);
    }

    #[test]
    fn test_check_field_hierarchy() {
        // Should not panic - scoring constants are correct
        check_field_hierarchy();
    }

    #[test]
    fn test_check_levenshtein_early_exit() {
        // Valid early exit
        check_levenshtein_early_exit("hello", "hi", 1, false);

        // Valid within bounds
        check_levenshtein_early_exit("hello", "hallo", 1, true);
    }
}
