elicitation/verification/types/
strings.rs

1//! String contract types.
2
3use super::{Utf8Bytes, ValidationError};
4use crate::{ElicitCommunicator, ElicitResult, Elicitation, Prompt};
5use anodized::spec;
6use elicitation_derive::contract_type;
7#[cfg(not(kani))]
8use elicitation_macros::instrumented_impl;
9use serde::{Deserialize, Serialize};
10
11// ============================================================================
12
13/// Contract type for non-empty String values with bounded length.
14///
15/// Built on top of `Utf8Bytes<N>` foundation, adding non-empty constraint.
16///
17/// # Type Parameters
18///
19/// * `MAX_LEN` - Maximum byte length (default: 4096)
20///
21/// # Invariants
22///
23/// 1. Content is valid UTF-8 (inherited from `Utf8Bytes`)
24/// 2. Length is > 0 (non-empty)
25/// 3. Length <= MAX_LEN (bounded)
26///
27/// Validates on construction, then can unwrap to stdlib String via `into_inner()`.
28#[contract_type(requires = "!value.is_empty()", ensures = "!result.get().is_empty()")]
29#[derive(Debug, Clone, PartialEq, Eq, Hash)]
30pub struct StringNonEmpty<const MAX_LEN: usize = 4096> {
31    utf8: Utf8Bytes<MAX_LEN>,
32}
33
34#[cfg_attr(not(kani), instrumented_impl)]
35impl<const MAX_LEN: usize> StringNonEmpty<MAX_LEN> {
36    /// Constructs a non-empty, bounded String from stdlib String.
37    ///
38    /// # Errors
39    ///
40    /// Returns `ValidationError` if:
41    /// - String is empty
42    /// - String length exceeds MAX_LEN bytes
43    /// - String is not valid UTF-8 (should never happen for stdlib String)
44    #[spec(requires: [!value.is_empty(), value.len() <= MAX_LEN])]
45    pub fn new(value: String) -> Result<Self, ValidationError> {
46        if value.is_empty() {
47            return Err(ValidationError::EmptyString);
48        }
49
50        let bytes = value.as_bytes();
51        if bytes.len() > MAX_LEN {
52            return Err(ValidationError::TooLong {
53                max: MAX_LEN,
54                actual: bytes.len(),
55            });
56        }
57
58        // Copy into fixed array
59        let mut array = [0u8; MAX_LEN];
60        array[..bytes.len()].copy_from_slice(bytes);
61
62        let utf8 = Utf8Bytes::new(array, bytes.len())?;
63
64        Ok(Self { utf8 })
65    }
66
67    /// Gets the wrapped value as a string slice.
68    pub fn get(&self) -> &str {
69        self.utf8.as_str()
70    }
71
72    /// Gets the byte length of the string.
73    pub fn len(&self) -> usize {
74        self.utf8.len()
75    }
76
77    /// Checks if the string is empty (always false due to invariant).
78    pub fn is_empty(&self) -> bool {
79        false // Guaranteed by non-empty invariant
80    }
81
82    /// Unwraps to stdlib String (trenchcoat off).
83    pub fn into_inner(self) -> String {
84        self.utf8.to_string()
85    }
86}
87
88crate::default_style!(StringNonEmpty<4096> => StringNonEmptyStyle);
89
90impl<const MAX_LEN: usize> Serialize for StringNonEmpty<MAX_LEN> {
91    fn serialize<S: serde::Serializer>(&self, s: S) -> Result<S::Ok, S::Error> {
92        self.get().serialize(s)
93    }
94}
95
96impl<'de, const MAX_LEN: usize> Deserialize<'de> for StringNonEmpty<MAX_LEN> {
97    fn deserialize<D: serde::Deserializer<'de>>(d: D) -> Result<Self, D::Error> {
98        let s = String::deserialize(d)?;
99        Self::new(s).map_err(serde::de::Error::custom)
100    }
101}
102
103impl<const MAX_LEN: usize> schemars::JsonSchema for StringNonEmpty<MAX_LEN> {
104    fn schema_name() -> ::std::borrow::Cow<'static, str> {
105        format!("StringNonEmpty<{MAX_LEN}>").into()
106    }
107    fn json_schema(_gen: &mut schemars::SchemaGenerator) -> schemars::Schema {
108        schemars::json_schema!({
109            "type": "string",
110            "minLength": 1,
111            "description": "Non-empty string"
112        })
113    }
114}
115
116#[cfg_attr(not(kani), instrumented_impl)]
117impl<const MAX_LEN: usize> Prompt for StringNonEmpty<MAX_LEN> {
118    fn prompt() -> Option<&'static str> {
119        Some("Please enter a non-empty string:")
120    }
121}
122
123#[cfg_attr(not(kani), instrumented_impl)]
124impl<const MAX_LEN: usize> Elicitation for StringNonEmpty<MAX_LEN> {
125    type Style = StringNonEmptyStyle;
126
127    #[tracing::instrument(skip(communicator), fields(type_name = "StringNonEmpty", max_len = MAX_LEN))]
128    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
129        tracing::debug!(
130            max_len = MAX_LEN,
131            "Eliciting StringNonEmpty (non-empty, bounded string)"
132        );
133
134        loop {
135            let value = String::elicit(communicator).await?;
136
137            match Self::new(value) {
138                Ok(non_empty) => {
139                    tracing::debug!(
140                        value = %non_empty.get(),
141                        len = non_empty.len(),
142                        max_len = MAX_LEN,
143                        "Valid StringNonEmpty constructed"
144                    );
145                    return Ok(non_empty);
146                }
147                Err(e) => {
148                    tracing::warn!(error = %e, max_len = MAX_LEN, "Invalid StringNonEmpty, re-prompting");
149                }
150            }
151        }
152    }
153
154    fn kani_proof() -> proc_macro2::TokenStream {
155        crate::verification::proof_helpers::kani_string_non_empty()
156    }
157
158    fn verus_proof() -> proc_macro2::TokenStream {
159        proc_macro2::TokenStream::new()
160    }
161
162    fn creusot_proof() -> proc_macro2::TokenStream {
163        proc_macro2::TokenStream::new()
164    }
165}
166
167#[cfg(test)]
168mod string_nonempty_tests {
169    use super::*;
170
171    #[test]
172    fn string_nonempty_new_valid() {
173        let result: Result<StringNonEmpty, _> = StringNonEmpty::new("hello".to_string());
174        assert!(result.is_ok());
175        let non_empty = result.unwrap();
176        assert_eq!(non_empty.get(), "hello");
177        assert_eq!(non_empty.len(), 5);
178        assert!(!non_empty.is_empty());
179    }
180
181    #[test]
182    fn string_nonempty_new_empty_invalid() {
183        let result = StringNonEmpty::<1024>::new(String::new());
184        assert!(result.is_err());
185        assert!(matches!(result.unwrap_err(), ValidationError::EmptyString));
186    }
187
188    #[test]
189    fn string_nonempty_into_inner() {
190        let non_empty: StringNonEmpty = StringNonEmpty::new("world".to_string()).unwrap();
191        let value: String = non_empty.into_inner();
192        assert_eq!(value, "world");
193    }
194
195    #[test]
196    fn string_nonempty_respects_max_len() {
197        // Should accept string at limit
198        let at_limit = "a".repeat(100);
199        let result = StringNonEmpty::<100>::new(at_limit);
200        assert!(result.is_ok());
201
202        // Should reject string over limit
203        let over_limit = "a".repeat(101);
204        let result = StringNonEmpty::<100>::new(over_limit);
205        assert!(result.is_err());
206        assert!(matches!(
207            result.unwrap_err(),
208            ValidationError::TooLong {
209                max: 100,
210                actual: 101
211            }
212        ));
213    }
214
215    #[test]
216    fn string_nonempty_default_max_len() {
217        // Default should be 4096
218        let large = "a".repeat(4096);
219        let result: Result<StringNonEmpty, _> = StringNonEmpty::new(large);
220        assert!(result.is_ok());
221
222        let too_large = "a".repeat(4097);
223        let result: Result<StringNonEmpty, _> = StringNonEmpty::new(too_large);
224        assert!(result.is_err());
225    }
226
227    #[test]
228    fn string_nonempty_utf8_preserved() {
229        let emoji = "Hello 👋 世界 🌍".to_string();
230        let non_empty: StringNonEmpty = StringNonEmpty::new(emoji.clone()).unwrap();
231        assert_eq!(non_empty.get(), emoji);
232        assert_eq!(non_empty.into_inner(), emoji);
233    }
234}
235
236// ============================================================================
237
238/// Default string wrapper for MCP elicitation.
239///
240/// Provides JSON Schema validation and serialization for strings.
241/// No constraints - accepts any valid string.
242#[derive(
243    Debug, Clone, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize, schemars::JsonSchema,
244)]
245#[schemars(description = "A string value")]
246pub struct StringDefault(#[schemars(description = "String content")] String);
247
248impl StringDefault {
249    /// Creates a new string wrapper.
250    pub fn new(s: String) -> Self {
251        Self(s)
252    }
253
254    /// Returns the inner string.
255    pub fn get(&self) -> &str {
256        &self.0
257    }
258
259    /// Converts to inner string.
260    pub fn into_inner(self) -> String {
261        self.0
262    }
263}
264
265// Mark as elicit-safe for rmcp
266rmcp::elicit_safe!(StringDefault);
267
268crate::default_style!(StringDefault => StringDefaultStyle);
269
270impl Prompt for StringDefault {
271    fn prompt() -> Option<&'static str> {
272        Some("Please enter a string:")
273    }
274}
275
276impl Elicitation for StringDefault {
277    type Style = StringDefaultStyle;
278
279    #[tracing::instrument(skip(communicator))]
280    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
281        // Consult style context for a custom prompt, fall back to default
282        let prompt = communicator
283            .style_context()
284            .prompt_for_type::<Self>("value", "String", &crate::style::PromptContext::new(0, 1))?
285            .unwrap_or_else(|| Self::prompt().unwrap().to_string());
286
287        tracing::debug!(prompt = %prompt, "Eliciting StringDefault");
288
289        let params = crate::mcp::text_params(&prompt);
290
291        let result = communicator
292            .call_tool(
293                rmcp::model::CallToolRequestParams::new(crate::mcp::tool_names::elicit_text())
294                    .with_arguments(params),
295            )
296            .await?;
297
298        let value = crate::mcp::extract_value(result)?;
299
300        // Use serde to deserialize directly into wrapper type
301        // Preserves error source via From<serde_json::Error> chain
302        Ok(serde_json::from_value(value)?)
303    }
304
305    fn kani_proof() -> proc_macro2::TokenStream {
306        proc_macro2::TokenStream::new()
307    }
308
309    fn verus_proof() -> proc_macro2::TokenStream {
310        proc_macro2::TokenStream::new()
311    }
312
313    fn creusot_proof() -> proc_macro2::TokenStream {
314        proc_macro2::TokenStream::new()
315    }
316}
317
318// ── ToCodeLiteral impls ───────────────────────────────────────────────────────
319
320mod emit_impls {
321    use super::*;
322    use crate::emit_code::ToCodeLiteral;
323    use proc_macro2::TokenStream;
324
325    impl<const MAX_LEN: usize> ToCodeLiteral for StringNonEmpty<MAX_LEN> {
326        fn to_code_literal(&self) -> TokenStream {
327            let s = self.get();
328            quote::quote! {
329                elicitation::StringNonEmpty::<#MAX_LEN>::new(#s.to_string())
330                    .expect("valid StringNonEmpty")
331            }
332        }
333    }
334}
335
336// ── ElicitIntrospect impls ────────────────────────────────────────────────────
337
338impl<const MAX_LEN: usize> crate::ElicitIntrospect for StringNonEmpty<MAX_LEN> {
339    fn pattern() -> crate::ElicitationPattern {
340        crate::ElicitationPattern::Primitive
341    }
342    fn metadata() -> crate::TypeMetadata {
343        crate::TypeMetadata {
344            type_name: "StringNonEmpty",
345            description: <Self as crate::Prompt>::prompt(),
346            details: crate::PatternDetails::Primitive,
347        }
348    }
349}
350
351impl crate::ElicitIntrospect for StringDefault {
352    fn pattern() -> crate::ElicitationPattern {
353        crate::ElicitationPattern::Primitive
354    }
355    fn metadata() -> crate::TypeMetadata {
356        crate::TypeMetadata {
357            type_name: "StringDefault",
358            description: <Self as crate::Prompt>::prompt(),
359            details: crate::PatternDetails::Primitive,
360        }
361    }
362}
elicitation/verification/types/strings.rs

elicitation/verification/types/
strings.rs
