elicitation 0.8.0

//! Kani verification harnesses for formal contract verification.
//!
//! These harnesses verify that contract properties hold under symbolic execution.
//!
//! # Organization
//!
//! - **Primitive Contracts**: String, i32, bool
//! - **Complex Contracts**: Email, NonEmpty, etc.
//! - **Composition**: Multiple contracts together

#![cfg(kani)]

use crate::verification::Contract;
use crate::verification::contracts::{BoolValid, I32Positive, StringNonEmpty};

// ============================================================================
// Phase 1: Primitive Type Contracts
// ============================================================================

/// Verify StringNonEmpty contract with symbolic execution.
///
/// **Property:** Non-empty strings remain non-empty.
#[kani::proof]
fn verify_string_non_empty_contract() {
    // Create various concrete strings to test
    let inputs = [
        String::from("a"),
        String::from("hello"),
        String::from("test string"),
        String::from("x".repeat(50)),
    ];

    for input in inputs.iter() {
        // Assume precondition
        kani::assume(StringNonEmpty::requires(input));

        // Property 1: Input is non-empty
        assert!(!input.is_empty());
        assert!(input.len() > 0);

        // Property 2: Identity transformation preserves non-emptiness
        let output = input.clone();
        assert!(StringNonEmpty::ensures(input, &output));
        assert!(!output.is_empty());
    }
}

/// Verify I32Positive contract with symbolic execution.
///
/// **Property:** Positive numbers remain positive.
#[kani::proof]
fn verify_i32_positive_contract() {
    // Symbolic i32
    let input: i32 = kani::any();

    // Assume precondition
    kani::assume(I32Positive::requires(&input));

    // Property 1: Input is positive
    assert!(input > 0);

    // Property 2: Identity transformation preserves positivity
    let output = input;
    assert!(I32Positive::ensures(&input, &output));
    assert!(output > 0);
}

/// Verify BoolValid contract (trivial).
///
/// **Property:** All booleans are valid.
#[kani::proof]
fn verify_bool_valid_contract() {
    // Symbolic bool
    let input: bool = kani::any();

    // Property: All booleans satisfy precondition
    assert!(BoolValid::requires(&input));

    // Property: All transformations are valid
    let output = !input; // Even negation is valid
    assert!(BoolValid::ensures(&input, &output));
}

// ============================================================================
// Legacy Examples (for reference)
// ============================================================================

/// Contract that ensures output is non-empty when input is non-empty.
struct NonEmptyString;

impl Contract for NonEmptyString {
    type Input = String;
    type Output = String;

    fn requires(input: &String) -> bool {
        !input.is_empty()
    }

    fn ensures(_input: &String, output: &String) -> bool {
        !output.is_empty()
    }
}

/// Contract that validates email format.
struct ValidEmail;

impl Contract for ValidEmail {
    type Input = String;
    type Output = String;

    fn requires(input: &String) -> bool {
        input.contains('@') && input.len() > 2
    }

    fn ensures(_input: &String, output: &String) -> bool {
        output.contains('@')
    }
}

/// Contract for number validation (positive only).
struct PositiveNumber;

impl Contract for PositiveNumber {
    type Input = i32;
    type Output = i32;

    fn requires(input: &i32) -> bool {
        *input > 0
    }

    fn ensures(_input: &i32, output: &i32) -> bool {
        *output > 0
    }
}

// ============================================================================
// Kani Verification Harnesses
// ============================================================================

#[kani::proof]
fn verify_non_empty_string_contract() {
    // Symbolic string input
    let input = String::from("test");

    // Assume precondition
    kani::assume(NonEmptyString::requires(&input));

    // Property: precondition guarantees non-empty
    assert!(!input.is_empty());
}

#[kani::proof]
fn verify_email_requires_at_symbol() {
    // Symbolic string
    let input = String::from("user@example.com");

    // Assume precondition holds
    kani::assume(ValidEmail::requires(&input));

    // Property: valid emails must contain @
    assert!(input.contains('@'));
    assert!(input.len() > 2);
}

#[kani::proof]
fn verify_positive_number_contract() {
    // Symbolic integer
    let input: i32 = kani::any();

    // Assume precondition
    kani::assume(PositiveNumber::requires(&input));

    // Property: precondition guarantees positive
    assert!(input > 0);
}

#[kani::proof]
fn verify_contract_composition_preconditions() {
    // Verify that if Contract A's postcondition holds,
    // and Contract B's precondition requires what A ensures,
    // then composition is valid.

    let email = String::from("user@example.com");

    // Contract A (ValidEmail) postcondition
    kani::assume(ValidEmail::ensures(&email, &email));

    // Verify email still has @ (preserved property)
    assert!(email.contains('@'));

    // Contract B (NonEmptyString) can accept this
    assert!(NonEmptyString::requires(&email));
}

// ============================================================================
// Phase 4: Contract Primitives Verification (New System)
// ============================================================================

/// Verify that Established proofs are zero-sized.
///
/// **Property:** All proof markers compile away completely.
#[kani::proof]
fn verify_proof_zero_sized() {
    use crate::contracts::{Established, Is};

    let proof: Established<Is<String>> = Established::assert();
    assert_eq!(std::mem::size_of_val(&proof), 0);

    let proof_i32: Established<Is<i32>> = Established::assert();
    assert_eq!(std::mem::size_of_val(&proof_i32), 0);
}

/// Verify conjunction is commutative (at the logical level).
///
/// **Property:** both(p, q) contains both proofs.
#[kani::proof]
fn verify_conjunction_projects() {
    use crate::contracts::{Established, Is, both, fst, snd};

    let p: Established<Is<String>> = Established::assert();
    let q: Established<Is<i32>> = Established::assert();

    let pq = both(p, q);

    // Can project left
    let _p2: Established<Is<String>> = fst(pq);

    // Can project right
    let _q2: Established<Is<i32>> = snd(pq);
}

/// Verify reflexive implication works.
///
/// **Property:** Every proposition implies itself.
#[kani::proof]
fn verify_reflexive_implies() {
    use crate::contracts::{Established, Is};

    let proof: Established<Is<String>> = Established::assert();
    let same: Established<Is<String>> = proof.weaken();

    // Both are zero-sized
    assert_eq!(std::mem::size_of_val(&same), 0);
}

/// Verify True axiom is always available.
///
/// **Property:** True::axiom() never fails.
#[kani::proof]
fn verify_true_axiom() {
    use crate::tool::True;

    let _proof1 = True::axiom();
    let _proof2 = True::axiom();
    let _proof3 = True::axiom();

    // All are zero-sized
    let proof = True::axiom();
    assert_eq!(std::mem::size_of_val(&proof), 0);
}

/// Verify InVariant is zero-sized.
///
/// **Property:** Enum variant proofs compile away.
#[kani::proof]
fn verify_invariant_zero_sized() {
    use crate::contracts::{Established, InVariant};

    enum State {
        Active,
        Inactive,
    }
    struct ActiveVariant;

    let proof: Established<InVariant<State, ActiveVariant>> = Established::assert();
    assert_eq!(std::mem::size_of_val(&proof), 0);
}

/// Verify conjunction chaining works.
///
/// **Property:** Can nest conjunctions arbitrarily.
#[kani::proof]
fn verify_conjunction_associative() {
    use crate::contracts::{And, Established, Is, both};

    struct P;
    struct Q;
    struct R;
    impl crate::contracts::Prop for P {}
    impl crate::contracts::Prop for Q {}
    impl crate::contracts::Prop for R {}

    let p: Established<P> = Established::assert();
    let q: Established<Q> = Established::assert();
    let r: Established<R> = Established::assert();

    // Can nest: (P ∧ Q) ∧ R
    let pq = both(p, q);
    let _pqr: Established<And<And<P, Q>, R>> = both(pq, r);
}

// ============================================================================
// Phase 4.2: Tool Chain Verification
// ============================================================================

/// Verify that tools require precondition proofs.
///
/// **Property:** Cannot call tool without establishing precondition.
#[kani::proof]
fn verify_tool_requires_precondition() {
    use crate::contracts::{Established, Prop};
    use crate::tool::True;

    struct Validated;
    impl Prop for Validated {}

    // Mock tool that requires validation
    fn mock_tool(_input: String, _pre: Established<Validated>) -> (String, Established<True>) {
        // Tool implementation would validate
        ("output".to_string(), True::axiom())
    }

    // Must provide proof
    let proof: Established<Validated> = Established::assert();
    let (_result, _post) = mock_tool("input".to_string(), proof);

    // This would not compile without proof:
    // let (_result, _post) = mock_tool("input".to_string());  // ERROR!
}

/// Verify that True axiom is always available (no preconditions).
///
/// **Property:** True::axiom() can be called without any preconditions.
#[kani::proof]
fn verify_true_always_available() {
    use crate::tool::True;

    // Can create True proofs anytime
    let _proof1 = True::axiom();
    let _proof2 = True::axiom();

    // Mock unconstrained tool
    fn unconstrained_tool(_input: String, _pre: crate::contracts::Established<True>) -> String {
        "result".to_string()
    }

    let _result = unconstrained_tool("input".to_string(), True::axiom());
}

/// Verify tool composition maintains invariants.
///
/// **Property:** Chaining tools with `then()` preserves type safety.
#[kani::proof]
fn verify_tool_chain_composition() {
    use crate::contracts::{Established, Implies, Prop};
    use crate::tool::True;

    struct InputValid;
    struct OutputTransformed;
    impl Prop for InputValid {}
    impl Prop for OutputTransformed {}
    impl Implies<OutputTransformed> for InputValid {} // First's post implies second's pre

    // Tool 1: Validate input
    fn validate(_input: String, _pre: Established<True>) -> (String, Established<InputValid>) {
        ("validated".to_string(), Established::assert())
    }

    // Tool 2: Transform (requires validation)
    fn transform(
        _input: String,
        _pre: Established<OutputTransformed>,
    ) -> (String, Established<True>) {
        ("transformed".to_string(), True::axiom())
    }

    // Chain: validate then transform
    let (_validated, proof1) = validate("input".to_string(), True::axiom());
    let proof2: Established<OutputTransformed> = proof1.weaken(); // Post → Pre
    let (_result, _proof_final) = transform("validated".to_string(), proof2);

    // Type system enforces: cannot skip validation
}

/// Verify parallel composition maintains both contracts.
///
/// **Property:** both_tools() requires both preconditions, establishes both postconditions.
#[kani::proof]
fn verify_parallel_composition() {
    use crate::contracts::{And, Established, Prop, both, fst, snd};
    use crate::tool::True;

    struct EmailValidated;
    struct PhoneValidated;
    impl Prop for EmailValidated {}
    impl Prop for PhoneValidated {}

    // Tool 1: Validate email
    fn validate_email(
        _email: String,
        _pre: Established<True>,
    ) -> (String, Established<EmailValidated>) {
        ("email@example.com".to_string(), Established::assert())
    }

    // Tool 2: Validate phone
    fn validate_phone(
        _phone: String,
        _pre: Established<True>,
    ) -> (String, Established<PhoneValidated>) {
        ("+1234567890".to_string(), Established::assert())
    }

    // Must provide both preconditions
    let pre1 = True::axiom();
    let pre2 = True::axiom();
    let combined_pre = both(pre1, pre2);

    // Simulate both_tools behavior
    let p1 = fst(combined_pre);
    let p2 = snd(combined_pre);

    let (_email, email_proof) = validate_email("test@example.com".to_string(), p1);
    let (_phone, phone_proof) = validate_phone("1234567890".to_string(), p2);

    let _combined_post: Established<And<EmailValidated, PhoneValidated>> =
        both(email_proof, phone_proof);

    // Both postconditions established
}

/// Verify refinement downcast is sound.
///
/// **Property:** If Refined refines Base, then Is<Refined> implies Is<Base>.
#[kani::proof]
fn verify_refinement_soundness() {
    use crate::contracts::{Established, Implies, Is, Refines, downcast};

    struct NonEmptyString(String);
    impl Refines<String> for NonEmptyString {}
    impl Implies<Is<String>> for Is<NonEmptyString> {}

    // Have proof of refined type
    let refined_proof: Established<Is<NonEmptyString>> = Established::assert();

    // Can safely downcast to base
    let _base_proof: Established<Is<String>> = downcast(refined_proof);

    // Kani verifies this is safe (refinement preserves inhabitation)
}

/// Verify conjunction projection preserves properties.
///
/// **Property:** If (P ∧ Q) holds, then both P and Q hold.
#[kani::proof]
fn verify_conjunction_soundness() {
    use crate::contracts::{And, Established, Prop, both, fst, snd};

    struct P;
    struct Q;
    impl Prop for P {}
    impl Prop for Q {}

    let p: Established<P> = Established::assert();
    let q: Established<Q> = Established::assert();

    // Establish conjunction
    let pq: Established<And<P, Q>> = both(p, q);

    // Project left: P holds
    let _p_again: Established<P> = fst(pq);

    // Project right: Q holds
    let _q_again: Established<Q> = snd(pq);

    // Kani verifies projections are sound
}

/// Verify InVariant for enum state machines.
///
/// **Property:** Variant proofs enforce state machine transitions.
#[kani::proof]
fn verify_invariant_state_machine() {
    use crate::contracts::{Established, InVariant};

    enum State {
        Draft,
        Approved,
    }
    struct DraftVariant;
    struct ApprovedVariant;

    // State-specific function requires draft proof
    fn edit_draft(_state: State, _proof: Established<InVariant<State, DraftVariant>>) {
        // Can only call in Draft state
    }

    // Transition function returns new proof
    fn approve(
        _state: State,
        _draft: Established<InVariant<State, DraftVariant>>,
    ) -> Established<InVariant<State, ApprovedVariant>> {
        Established::assert()
    }

    let draft_proof: Established<InVariant<State, DraftVariant>> = Established::assert();
    edit_draft(State::Draft, draft_proof);

    let approved_proof = approve(State::Draft, draft_proof);
    let _final_state = (State::Approved, approved_proof);

    // Cannot call edit_draft with approved_proof (type error)
}