elicitation 0.8.0

Conversational elicitation of strongly-typed Rust values via MCP
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139

//! Kani model checker adapter for formal verification.
//!
//! This module adapts the generic [`Contract`](super::Contract) trait for use
//! with the [Kani Rust Verifier](https://github.com/model-checking/kani).
//!
//! # Kani Integration
//!
//! Kani uses **bounded model checking** to formally verify Rust programs:
//! - Symbolic execution of all possible inputs
//! - SMT solver verification of assertions
//! - Compile-time proofs (not runtime tests)
//!
//! # Example
//!
//! ```rust,ignore
//! use elicitation::verification::{Contract, kani::Tool};
//!
//! struct ValidateEmail;
//!
//! impl Contract for ValidateEmail {
//!     type Input = String;
//!     type Output = String;
//!     
//!     fn requires(input: &String) -> bool {
//!         input.contains('@')
//!     }
//!     
//!     fn ensures(_input: &String, output: &String) -> bool {
//!         output.contains('@')
//!     }
//! }
//!
//! #[async_trait::async_trait]
//! impl Tool for ValidateEmail {
//!     async fn execute(&self, input: String) -> ElicitResult<String> {
//!         // Implementation
//!         Ok(input)
//!     }
//! }
//!
//! // Kani proof harness
//! #[cfg(kani)]
//! #[kani::proof]
//! fn verify_email_contract() {
//!     let input = String::from("test@example.com");
//!     kani::assume(ValidateEmail::requires(&input));
//!     assert!(input.contains('@')); // ✅ PROVEN
//! }
//! ```
//!
//! # Key Features
//!
//! - **Model Checking**: Explores all possible execution paths
//! - **Bounded Verification**: With `#[kani::unwind(n)]` for loops
//! - **Symbolic Execution**: `kani::any()` for symbolic values
//! - **Contract Checking**: Runtime verification with `verify_and_execute`

use super::Contract;
use crate::ElicitResult;

// Re-export Contract as KaniContract for backwards compatibility
pub use super::Contract as KaniContract;

/// Executable tool with Kani contract verification.
///
/// Extends [`Contract`] with async execution and runtime contract checking.
///
/// # Example
///
/// ```rust,ignore
/// #[async_trait::async_trait]
/// impl Tool for MyTool {
///     async fn execute(&self, input: Self::Input) -> ElicitResult<Self::Output> {
///         // Implementation
///     }
/// }
/// ```
#[async_trait::async_trait]
pub trait Tool: Contract + Sync {
    /// Execute the tool.
    ///
    /// Implementations should focus on the core logic. Contract verification
    /// is handled by [`verify_and_execute`](Tool::verify_and_execute).
    async fn execute(&self, input: Self::Input) -> ElicitResult<Self::Output>;

    /// Verify and execute with contract checking.
    ///
    /// This is the primary execution method. It ensures:
    /// 1. Preconditions hold before execution
    /// 2. Postconditions hold after execution
    /// 3. Invariants hold throughout
    async fn verify_and_execute(&self, input: Self::Input) -> ElicitResult<Self::Output> {
        tracing::debug!("Verifying preconditions");

        // In debug/test builds, check contracts at runtime
        #[cfg(debug_assertions)]
        {
            if !Self::requires(&input) {
                tracing::error!("Precondition violated");
                return Err(crate::ElicitErrorKind::ParseError(
                    "Tool precondition violated".to_string(),
                )
                .into());
            }
        }

        // With Kani, verify contracts formally
        #[cfg(kani)]
        {
            kani::assume(Self::requires(&input));
        }

        tracing::debug!("Executing tool");
        let output = self.execute(input.clone()).await?;

        // Verify postconditions
        #[cfg(debug_assertions)]
        {
            if !Self::ensures(&input, &output) {
                tracing::error!("Postcondition violated");
                return Err(crate::ElicitErrorKind::ParseError(
                    "Tool postcondition violated".to_string(),
                )
                .into());
            }
        }

        #[cfg(kani)]
        {
            assert!(
                Self::ensures(&input, &output),
                "Postcondition must hold after execution",
            );
        }

        tracing::debug!("Tool execution successful");
        Ok(output)
    }
}