//! Mechanism Contract Proof of Concept
//!
//! Demonstrates verifying elicitation *mechanisms* themselves,
//! not just the types being elicited.
//!
//! # The Vision
//!
//! Two-layer verification:
//! 1. **Mechanism layer**: Survey returns valid enum variant
//! 2. **Type layer**: Variant satisfies type constraints
//!
//! When both proven, the entire elicitation chain is proven.

#![cfg(feature = "verification")]

use elicitation::verification::{
    Contract,
    contracts::{I32Positive, StringNonEmpty},
    mechanisms::{
        AffirmReturnsBoolean, MechanismWithType, NumericReturnsValid, TextReturnsNonEmpty,
    },
};

fn main() {
    println!("=== Mechanism Contract Proof of Concept ===\n");

    // Layer 1: Mechanism Contracts
    println!("## Layer 1: Mechanism Contracts\n");

    println!("These verify the elicitation PROCESS works correctly:\n");

    println!("1. Affirm Mechanism");
    println!("   Contract: Returns boolean");
    let affirm_result = true;
    println!("   Input: {}", affirm_result);
    println!(
        "   Verified: {}",
        AffirmReturnsBoolean::ensures(&affirm_result, &true)
    );
    println!();

    println!("2. Text Mechanism");
    println!("   Contract: Returns non-empty string");
    let text_input = String::new();
    let text_result = String::from("hello");
    println!("   Input: {:?}", text_input);
    println!("   Output: {:?}", text_result);
    println!(
        "   Verified: {}",
        TextReturnsNonEmpty::ensures(&text_input, &text_result)
    );
    println!();

    println!("3. Numeric Mechanism");
    println!("   Contract: Returns valid i32");
    let num_input = 0i32;
    let num_result = 42i32;
    println!("   Input: {}", num_input);
    println!("   Output: {}", num_result);
    println!(
        "   Verified: {}",
        NumericReturnsValid::<i32>::ensures(&num_input, &num_result)
    );
    println!();

    // Layer 2: Type Contracts
    println!("## Layer 2: Type Contracts\n");

    println!("These verify the VALUES satisfy constraints:\n");

    println!("1. Positive Integer");
    println!("   Contract: i32 > 0");
    let positive = 42i32;
    let negative = -1i32;
    println!("   Positive (42): {}", I32Positive::requires(&positive));
    println!("   Negative (-1): {}", I32Positive::requires(&negative));
    println!();

    println!("2. Non-Empty String");
    println!("   Contract: String length > 0");
    let non_empty = String::from("hello");
    let empty = String::new();
    println!("   Non-empty: {}", StringNonEmpty::requires(&non_empty));
    println!("   Empty: {}", StringNonEmpty::requires(&empty));
    println!();

    // Layer 3: Composition
    println!("## Layer 3: Composed Verification\n");

    println!("Mechanism + Type = End-to-End Proof\n");

    println!("Example: Numeric mechanism returns positive i32\n");

    let mechanism = NumericReturnsValid::<i32>::new();
    let type_contract = I32Positive;
    let composed = MechanismWithType::new(mechanism, type_contract);

    println!("Test Case 1: Positive value (42)");
    let positive_input = 42i32;
    let positive_output = 42i32;
    let both_hold = MechanismWithType::<NumericReturnsValid<i32>, I32Positive>::ensures(
        &positive_input,
        &positive_output,
    );
    println!(
        "   Mechanism verified: {}",
        NumericReturnsValid::<i32>::ensures(&positive_input, &positive_output)
    );
    println!(
        "   Type verified: {}",
        I32Positive::ensures(&positive_input, &positive_output)
    );
    println!("   BOTH verified: {} ✓", both_hold);
    println!();

    println!("Test Case 2: Negative value (-1)");
    let negative_input = -1i32;
    let negative_output = -1i32;
    let mechanism_ok = NumericReturnsValid::<i32>::ensures(&negative_input, &negative_output);
    let type_ok = I32Positive::ensures(&negative_input, &negative_output);
    let both_ok = MechanismWithType::<NumericReturnsValid<i32>, I32Positive>::ensures(
        &negative_input,
        &negative_output,
    );
    println!("   Mechanism verified: {} ✓", mechanism_ok);
    println!("   Type verified: {} ✗", type_ok);
    println!("   BOTH verified: {} ✗", both_ok);
    println!();

    println!("=== The Proof Chain ===\n");
    println!("For any elicited value `v`:");
    println!();
    println!("  1. Mechanism contract guarantees:");
    println!("     ∀v: Numeric(v) ⇒ v ∈ [i32::MIN, i32::MAX]");
    println!();
    println!("  2. Type contract guarantees:");
    println!("     ∀v: Positive(v) ⇒ v > 0");
    println!();
    println!("  3. Composed contract guarantees:");
    println!("     ∀v: Numeric(v) ∧ Positive(v) ⇒ v > 0 ∧ v ∈ [i32::MIN, i32::MAX]");
    println!();
    println!("  Therefore: All elicited values are PROVEN positive integers ∎");
    println!();

    println!("=== Why This Matters ===\n");
    println!("✓ Mechanism verification: Process correctness");
    println!("✓ Type verification: Value correctness");
    println!("✓ Composition: End-to-end mathematical proof");
    println!("✓ No runtime errors: Type system + formal verification");
    println!();

    println!("=== Next Steps ===\n");
    println!("1. Add mechanism contracts for Survey (enum elicitation)");
    println!("2. Verify derived types inherit verification");
    println!("3. Create Kani harnesses proving composition");
    println!("4. Extend to all elicitation mechanisms");
    println!();

    println!("Invariant check: {}", composed.invariant());
}
